Twisted lifts satisfy the lifting identities (toward Proposition 12.8) #
If a family of lifted actions (assocErr) or of lifted maps (interErr) built at the fibre
t = 1 has all relative weights in the cone, then the twisted family satisfies the same identities
for the twisted deformation at every parameter t: on the torus the twist is conjugation by the
diagonal scalings, and the identities are polynomial in t (IsPoly.eq_zero_of_torus).
def
MultiplicativeBasisDeformations.GExt.evalAA
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{M : Type u_3}
[AddCommGroup M]
[Module k M]
(m : M)
(a b : Λ)
:
(M →ₗ[k] Λ →ₗ[k] M) →ₗ[k] (M →ₗ[k] Λ →ₗ[k] M) →ₗ[k] M
Evaluation of φ (ψ m a) b, bilinearly in (φ, ψ).
Instances For
def
MultiplicativeBasisDeformations.GExt.evalAM
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{M : Type u_3}
[AddCommGroup M]
[Module k M]
(m : M)
(a b : Λ)
:
(M →ₗ[k] Λ →ₗ[k] M) →ₗ[k] (Λ →ₗ[k] Λ →ₗ[k] Λ) →ₗ[k] M
Evaluation of φ m (ψ a b), bilinearly in (φ, ψ).
Instances For
def
MultiplicativeBasisDeformations.GExt.evalFA
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
(m : M)
(a : Λ)
:
(M →ₗ[k] N) →ₗ[k] (M →ₗ[k] Λ →ₗ[k] M) →ₗ[k] N
Evaluation of F (ν m a), bilinearly in (F, ν).
Instances For
def
MultiplicativeBasisDeformations.GExt.evalAF
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
(m : M)
(a : Λ)
:
(N →ₗ[k] Λ →ₗ[k] N) →ₗ[k] (M →ₗ[k] N) →ₗ[k] N
Evaluation of ν' (F m) a, bilinearly in (ν', F).
Instances For
theorem
MultiplicativeBasisDeformations.GExt.assocErr_twb
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{M : Type u_3}
[AddCommGroup M]
[Module k M]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{C : AddSubmonoid Wt}
(hC : ∀ γ ∈ C, ∀ (i : I), 0 ≤ coords γ i)
{wΛ : MGr k Wt Λ}
{wM : MGr k Wt M}
[Infinite k]
{ν : ℕ → M →ₗ[k] Λ →ₗ[k] M}
{μ : ℕ → Λ →ₗ[k] Λ →ₗ[k] Λ}
(hν : ∀ (i : ℕ), MGr.ConeBil 0 (ν i))
(hμ : ∀ (j : ℕ), MGr.ConeBil 0 (μ j))
{n : ℕ}
(h : ∀ (m : M) (a b : Λ), assocErr ν μ n m a b = 0)
(t : I → k)
(m : M)
(a b : Λ)
:
Twisting preserves the action identities.
theorem
MultiplicativeBasisDeformations.GExt.interErr_twl
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{C : AddSubmonoid Wt}
(hC : ∀ γ ∈ C, ∀ (i : I), 0 ≤ coords γ i)
{wΛ : MGr k Wt Λ}
{wM : MGr k Wt M}
{wN : MGr k Wt N}
[Infinite k]
{ρ : Wt}
{F : ℕ → M →ₗ[k] N}
{ν : ℕ → M →ₗ[k] Λ →ₗ[k] M}
{ν' : ℕ → N →ₗ[k] Λ →ₗ[k] N}
(hF : ∀ (i : ℕ), MGr.ConeLin ρ (F i))
(hν : ∀ (i : ℕ), MGr.ConeBil 0 (ν i))
(hν' : ∀ (i : ℕ), MGr.ConeBil 0 (ν' i))
{n : ℕ}
(h : ∀ (m : M) (a : Λ), interErr F ν ν' n m a = 0)
(t : I → k)
(m : M)
(a : Λ)
:
Twisting preserves the linearity identities of lifted maps.
Twisting total maps #
theorem
MultiplicativeBasisDeformations.GExt.twl_add
{k : Type u_1}
[Field k]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{wM : MGr k Wt M}
{wN : MGr k Wt N}
(t : I → k)
(ρ : Wt)
(f g : M →ₗ[k] N)
:
theorem
MultiplicativeBasisDeformations.GExt.twl_smul
{k : Type u_1}
[Field k]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{wM : MGr k Wt M}
{wN : MGr k Wt N}
(t : I → k)
(ρ : Wt)
(c : k)
(f : M →ₗ[k] N)
:
theorem
MultiplicativeBasisDeformations.GExt.twl_zero
{k : Type u_1}
[Field k]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{wM : MGr k Wt M}
{wN : MGr k Wt N}
(t : I → k)
(ρ : Wt)
:
MGr.twl coords wM wN t ρ 0 = 0
theorem
MultiplicativeBasisDeformations.GExt.twl_sub
{k : Type u_1}
[Field k]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{wM : MGr k Wt M}
{wN : MGr k Wt N}
(t : I → k)
(ρ : Wt)
(f g : M →ₗ[k] N)
:
theorem
MultiplicativeBasisDeformations.GExt.twl_sum
{k : Type u_1}
[Field k]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{wM : MGr k Wt M}
{wN : MGr k Wt N}
{κ : Type u_7}
(s : Finset κ)
(t : I → k)
(ρ : Wt)
(f : κ → M →ₗ[k] N)
:
theorem
MultiplicativeBasisDeformations.GExt.twb_add
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{M : Type u_3}
[AddCommGroup M]
[Module k M]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{wΛ : MGr k Wt Λ}
{wM : MGr k Wt M}
(t : I → k)
(ρ : Wt)
(φ ψ : M →ₗ[k] Λ →ₗ[k] M)
:
theorem
MultiplicativeBasisDeformations.GExt.twb_sum
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{M : Type u_3}
[AddCommGroup M]
[Module k M]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{wΛ : MGr k Wt Λ}
{wM : MGr k Wt M}
{κ : Type u_7}
(s : Finset κ)
(t : I → k)
(ρ : Wt)
(φ : κ → M →ₗ[k] Λ →ₗ[k] M)
:
theorem
MultiplicativeBasisDeformations.GExt.ConeLin.comp'
{k : Type u_1}
[Field k]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wM : MGr k Wt M}
{wN : MGr k Wt N}
{P : Type u_6}
[AddCommGroup P]
[Module k P]
{wP : MGr k Wt P}
{ρ ρ' : Wt}
{f : M →ₗ[k] N}
{g : N →ₗ[k] P}
(hf : MGr.ConeLin ρ f)
(hg : MGr.ConeLin ρ' g)
:
MGr.ConeLin (ρ + ρ') (g ∘ₗ f)
theorem
MultiplicativeBasisDeformations.GExt.twl_one
{k : Type u_1}
[Field k]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{wM : MGr k Wt M}
{wN : MGr k Wt N}
(ρ : Wt)
(f : M →ₗ[k] N)
:
MGr.twl coords wM wN (fun (x : I) => 1) ρ f = f
theorem
MultiplicativeBasisDeformations.GExt.twb_one
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{M : Type u_3}
[AddCommGroup M]
[Module k M]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{wΛ : MGr k Wt Λ}
{wM : MGr k Wt M}
(ρ : Wt)
(φ : M →ₗ[k] Λ →ₗ[k] M)
:
MGr.twb coords wM wΛ wM (fun (x : I) => 1) ρ φ = φ
theorem
MultiplicativeBasisDeformations.GExt.twl_comp
{k : Type u_1}
[Field k]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{C : AddSubmonoid Wt}
(hC : ∀ γ ∈ C, ∀ (i : I), 0 ≤ coords γ i)
{wM : MGr k Wt M}
{wN : MGr k Wt N}
[Infinite k]
{P : Type u_6}
[AddCommGroup P]
[Module k P]
{wP : MGr k Wt P}
{ρ ρ' : Wt}
{f : M →ₗ[k] N}
{g : N →ₗ[k] P}
(hf : MGr.ConeLin ρ f)
(hg : MGr.ConeLin ρ' g)
(t : I → k)
:
Twisting is multiplicative on maps in the cone.
theorem
MultiplicativeBasisDeformations.GExt.twl_lin
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{C : AddSubmonoid Wt}
(hC : ∀ γ ∈ C, ∀ (i : I), 0 ≤ coords γ i)
{wΛ : MGr k Wt Λ}
{wM : MGr k Wt M}
{wN : MGr k Wt N}
[Infinite k]
{ρ : Wt}
{g : M →ₗ[k] N}
{A : M →ₗ[k] Λ →ₗ[k] M}
{A' : N →ₗ[k] Λ →ₗ[k] N}
(hg : MGr.ConeLin ρ g)
(hA : MGr.ConeBil 0 A)
(hA' : MGr.ConeBil 0 A')
(h : ∀ (m : M) (a : Λ), g ((A m) a) = (A' (g m)) a)
(t : I → k)
(m : M)
(a : Λ)
:
Twisting preserves module-linearity of total maps.
theorem
MultiplicativeBasisDeformations.GExt.twl_id
{k : Type u_1}
[Field k]
{M : Type u_3}
[AddCommGroup M]
[Module k M]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{wM : MGr k Wt M}
(t : I → k)
:
MGr.twl coords wM wM t 0 LinearMap.id = LinearMap.id
theorem
MultiplicativeBasisDeformations.GExt.ch_add
{k : Type u_1}
[Field k]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{t : I → k}
{γ δ : Wt}
(hγ : ∀ (i : I), 0 ≤ coords γ i)
(hδ : ∀ (i : I), 0 ≤ coords δ i)
:
theorem
MultiplicativeBasisDeformations.GExt.twl_shift
{k : Type u_1}
[Field k]
{M : Type u_3}
{N : Type u_4}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{I : Type}
[Fintype I]
[DecidableEq I]
{coords : Wt →+ I → ℤ}
{C : AddSubmonoid Wt}
(hC : ∀ γ ∈ C, ∀ (i : I), 0 ≤ coords γ i)
{wM : MGr k Wt M}
{wN : MGr k Wt N}
{ρ γ : Wt}
{f : M →ₗ[k] N}
(hf : MGr.ConeLin (ρ + γ) f)
(hγ : γ ∈ C)
(t : I → k)
:
Moving the reference weight by a cone weight multiplies the twist by its character.
theorem
MultiplicativeBasisDeformations.GExt.coneBil_add
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{M : Type u_3}
[AddCommGroup M]
[Module k M]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr k Wt Λ}
{wM : MGr k Wt M}
{ρ : Wt}
{φ ψ : M →ₗ[k] Λ →ₗ[k] M}
(hφ : MGr.ConeBil ρ φ)
(hψ : MGr.ConeBil ρ ψ)
:
MGr.ConeBil ρ (φ + ψ)
theorem
MultiplicativeBasisDeformations.GExt.coneBil_sum
{k : Type u_1}
[Field k]
{Λ : Type u_2}
[Ring Λ]
[Algebra k Λ]
{M : Type u_3}
[AddCommGroup M]
[Module k M]
{Wt : Type u_5}
[AddCommGroup Wt]
[DecidableEq Wt]
{C : AddSubmonoid Wt}
{wΛ : MGr k Wt Λ}
{wM : MGr k Wt M}
{ρ : Wt}
{κ : Type u_7}
(s : Finset κ)
{φ : κ → M →ₗ[k] Λ →ₗ[k] M}
(hφ : ∀ j ∈ s, MGr.ConeBil ρ (φ j))
:
MGr.ConeBil ρ (∑ j ∈ s, φ j)