The split form of a positive filtered deformation (Lemma 6.4, as used in Proposition 6.5) #
positive-deformations.tex: "The resulting identification of B with Λ as
filtered vector spaces induces the prescribed identification gr B = Λ, and the multiplication
of B becomes μ₀ + Σ_{q>0} μ_q, where μ₀ is the multiplication of Λ and each μ_q raises
internal degree by q, […] and vanishes when an input belongs to S."
From a splitting φ : Λ ≅ B (Split, given by PosFiltration.exists_split) the transported
product a ⋆ b = φ⁻¹(φa φb) decomposes into homogeneous parts μ_q (Split.μ), which form a
positive deformation in split form (Split.posDef) with total product ⋆ (Split.tot_eq_star).
structure
MultiplicativeBasisDeformations.PosFiltration.Split
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
(P : PosFiltration G B)
:
Type (max v w)
A splitting of a positive filtered deformation (Lemma 6.4): a linear isomorphism
φ : Λ ≅ B preserving 1, mapping Λ_{≥d} onto F^d, with leading term the identity.
- φ : Λ ≃ₗ[k] B
- one : self.φ 1 = 1
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.nonempty_split
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
(P : PosFiltration G B)
(V : G.Vertices)
:
Nonempty P.Split
Lemma 6.4 gives a splitting.
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.mem_F_iff
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
{d : ℕ}
{a : Λ}
:
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.σ_ge
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
{d : ℕ}
{a : Λ}
(ha : G.Ge d a)
:
def
MultiplicativeBasisDeformations.PosFiltration.Split.star
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
:
Λ →ₗ[k] Λ →ₗ[k] Λ
The transported product a ⋆ b = φ⁻¹(φa φb).
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.star_apply
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(a b : Λ)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.φ_star
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(a b : Λ)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.star_ge
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
{d e : ℕ}
{a b : Λ}
(ha : G.Ge d a)
(hb : G.Ge e b)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.proj_star
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
{d e : ℕ}
{a b : Λ}
(ha : G.IsHom d a)
(hb : G.IsHom e b)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.star_assoc
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(a b c : Λ)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.star_one_left
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(a : Λ)
:
(S.star 1) a = a
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.star_one_right
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(a : Λ)
:
(S.star a) 1 = a
def
MultiplicativeBasisDeformations.PosFiltration.Split.μ
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(q : ℕ)
:
Λ →ₗ[k] Λ →ₗ[k] Λ
The degree-q part of the transported product.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.μ_hom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
{q d e : ℕ}
{a b : Λ}
(ha : G.IsHom d a)
(hb : G.IsHom e b)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.μ_isHom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
{q d e : ℕ}
{a b : Λ}
(ha : G.IsHom d a)
(hb : G.IsHom e b)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.μ_eq_zero
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
{q : ℕ}
(hq : G.N ≤ q)
:
S.μ q = 0
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.star_eq_sum_hom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
{d e : ℕ}
{a b : Λ}
(ha : G.IsHom d a)
(hb : G.IsHom e b)
:
a ⋆ b = Σ_q μ_q(a, b) for homogeneous a, b.
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.star_eq_sum
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(a b : Λ)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.μ_zero_apply
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(a b : Λ)
:
((S.μ 0) a) b = a * b
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.μ_unit_left
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
{q : ℕ}
(hq : 0 < q)
(h1 : G.IsHom 0 1)
(a : Λ)
:
((S.μ q) 1) a = 0
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.μ_unit_right
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
{q : ℕ}
(hq : 0 < q)
(h1 : G.IsHom 0 1)
(a : Λ)
:
((S.μ q) a) 1 = 0
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.proj_box
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
(d₀ : ℕ)
(X : ℕ → ℕ → Λ)
(hX : ∀ (q q' : ℕ), G.IsHom (d₀ + q + q') (X q q'))
(hz : ∀ (q q' : ℕ), G.N ≤ q ∨ G.N ≤ q' → X q q' = 0)
(n : ℕ)
:
Extracting the degree-d₀ + n part of a double sum of homogeneous terms.
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.μAssoc_hom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
{d e f : ℕ}
{a b c : Λ}
(ha : G.IsHom d a)
(hb : G.IsHom e b)
(hc : G.IsHom f c)
(n : ℕ)
:
GExt.μAssoc S.μ n a b c = 0
def
MultiplicativeBasisDeformations.PosFiltration.Split.μAssocL₁
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(n : ℕ)
(b c : Λ)
:
Λ →ₗ[k] Λ
μAssoc as a linear map in each argument.
Instances For
def
MultiplicativeBasisDeformations.PosFiltration.Split.μAssocL₂
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(n : ℕ)
(a c : Λ)
:
Λ →ₗ[k] Λ
Instances For
def
MultiplicativeBasisDeformations.PosFiltration.Split.μAssocL₃
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(n : ℕ)
(a b : Λ)
:
Λ →ₗ[k] Λ
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.μAssoc_eq_zero
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(n : ℕ)
(a b c : Λ)
:
GExt.μAssoc S.μ n a b c = 0
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.μ_hdeg
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(h1 : G.IsHom 0 1)
(q : ℕ)
:
GExt.HDeg (GExt.GAlg.ofLen G h1) (S.μ q) ↑q
def
MultiplicativeBasisDeformations.PosFiltration.Split.posDef
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(h1 : G.IsHom 0 1)
:
GExt.PosDef (GExt.GAlg.ofLen G h1)
The positive deformation in split form of a split positive filtered deformation.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.ofLen_nonneg
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
(h1 : G.IsHom 0 1)
(q : ℤ)
:
q ∈ (GExt.GAlg.ofLen G h1).gr.supp → 0 ≤ q
theorem
MultiplicativeBasisDeformations.PosFiltration.Split.tot_eq_star
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
(S : P.Split)
(h1 : G.IsHom 0 1)
(a b : Λ)
:
The total product of the split form is the transported product.
Filtered lifts of graded modules #
structure
MultiplicativeBasisDeformations.PosFiltration.FLift
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
(P : PosFiltration G B)
{M : Type u_1}
[AddCommGroup M]
[Module k M]
(h1 : G.IsHom 0 1)
(MM : GExt.GMod (GExt.GAlg.ofLen G h1) M)
:
Type (max u_1 w)
A filtered lift of M to B with associated graded module M
(positive-deformations.tex): a right B-action on the graded space M such that F^d B
raises internal degree by at least d, with leading term the action of Λ through σ_d.
- act : M →ₗ[k] B →ₗ[k] M
- one (m : M) : (self.act m) 1 = m
Instances For
def
MultiplicativeBasisDeformations.PosFiltration.Split.fLift
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(S : P.Split)
(L : GExt.ActFam (S.posDef h1) MM)
:
P.FLift h1 MM
The filtered lift of a lifted action family.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.exists_fLift_of_split
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(hS : Nonempty P.Split)
(hExt : ∀ (t : ℕ), 0 < t → GExt.ExtVanish MM MM 1 ↑t)
:
Nonempty (P.FLift h1 MM)
Proposition 6.5(1), existence: under Ext²_Λ(M, M)_t = 0 for t > 0, M has a
filtered lift to B with associated graded module M.
theorem
MultiplicativeBasisDeformations.PosFiltration.exists_fLift
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(V : G.Vertices)
(hExt : ∀ (t : ℕ), 0 < t → GExt.ExtVanish MM MM 1 ↑t)
:
Nonempty (P.FLift h1 MM)
theorem
MultiplicativeBasisDeformations.GExt.ZGr.proj_box
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
(g : ZGr M)
(d₀ : ℤ)
(K₁ K₂ : ℕ)
(X : ℕ → ℕ → M)
(hX : ∀ (i j : ℕ), g.IsHom (d₀ + ↑i + ↑j) (X i j))
(hz1 : ∀ (i j : ℕ), K₁ ≤ i → X i j = 0)
(hz2 : ∀ (i j : ℕ), K₂ ≤ j → X i j = 0)
(n : ℕ)
:
(g.proj (d₀ + ↑n)) (∑ i ∈ Finset.range K₁, ∑ j ∈ Finset.range K₂, X i j) = ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n, X x.1 x.2
Extracting the degree-d₀ + n part of a double sum of homogeneous terms.
theorem
MultiplicativeBasisDeformations.PosFiltration.bilin_ext
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{f g : M →ₗ[k] Λ →ₗ[k] N}
(h : ∀ (p : ℤ) (q : ℕ) (m : M) (a : Λ), MM.gr.IsHom p m → G.IsHom q a → (f m) a = (g m) a)
:
f = g
Bilinear maps agreeing on homogeneous inputs agree.
def
MultiplicativeBasisDeformations.PosFiltration.FLift.ν
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(S : P.Split)
(A : P.FLift h1 MM)
(n : ℕ)
:
M →ₗ[k] Λ →ₗ[k] M
The degree-n part of a filtered lift.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.FLift.ν_hom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(S : P.Split)
(A : P.FLift h1 MM)
(n : ℕ)
{p : ℤ}
{q : ℕ}
{m : M}
{a : Λ}
(hm : MM.gr.IsHom p m)
(ha : G.IsHom q a)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.FLift.act_eq_sum
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(S : P.Split)
(A : P.FLift h1 MM)
{p : ℤ}
{q : ℕ}
{m : M}
{a : Λ}
(hm : MM.gr.IsHom p m)
(ha : G.IsHom q a)
:
(A.act m) (S.φ a) = ∑ i ∈ Finset.range (2 * GExt.degBound MM.gr + 1), ((ν S A i) m) a
A filtered lift is the sum of its parts.
theorem
MultiplicativeBasisDeformations.PosFiltration.FLift.ν_shift
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(S : P.Split)
(A : P.FLift h1 MM)
(n : ℕ)
:
GExt.IsShift MM (↑n) (ν S A n)
theorem
MultiplicativeBasisDeformations.PosFiltration.FLift.ν_zero
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(S : P.Split)
(A : P.FLift h1 MM)
(m : M)
(a : Λ)
:
def
MultiplicativeBasisDeformations.PosFiltration.FLift.toActFam
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(S : P.Split)
(A : P.FLift h1 MM)
:
GExt.ActFam (S.posDef h1) MM
The action family of a filtered lift.
Instances For
theorem
MultiplicativeBasisDeformations.PosFiltration.FLift.toActFam_tot
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(S : P.Split)
(A : P.FLift h1 MM)
(m : M)
(a : Λ)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.fLift_unique_of_split
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(hS : Nonempty P.Split)
(hExt : ∀ (t : ℕ), 0 < t → GExt.ExtVanish MM MM 0 ↑t)
(A A' : P.FLift h1 MM)
:
Proposition 6.5(1), uniqueness: under Ext¹_Λ(M, M)_t = 0 for t > 0, two filtered
lifts of M are isomorphic by a B-linear isomorphism with leading term the identity.
theorem
MultiplicativeBasisDeformations.PosFiltration.fLift_map_of_split
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{NN : GExt.GMod (GExt.GAlg.ofLen G h1) N}
(hS : Nonempty P.Split)
(A : P.FLift h1 MM)
(A' : P.FLift h1 NN)
(r : ℕ)
(f : M →ₗ[k] N)
(hf : ∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a)
(hfd : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + ↑r) (f m))
(hExt : ∀ (t : ℕ), 0 < t → GExt.ExtVanish MM NN 0 (↑r + ↑t))
:
Proposition 6.5(2), lifts of maps: under Ext¹_Λ(M, N)_{r+t} = 0 for t > 0, a
homogeneous Λ-linear map of degree r ≥ 0 lifts to a B-linear map of the filtered lifts,
of filtration order r, with leading term the given map.
theorem
MultiplicativeBasisDeformations.PosFiltration.fLift_leading_of_split
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{NN : GExt.GMod (GExt.GAlg.ofLen G h1) N}
(hS : Nonempty P.Split)
(A : P.FLift h1 MM)
(A' : P.FLift h1 NN)
{r : ℤ}
(g : M →ₗ[k] N)
(hg : ∀ (m : M) (x : B), g ((A.act m) x) = (A'.act (g m)) x)
(hord : GExt.OrderGe MM NN r g)
(m : M)
(a : Λ)
:
Proposition 6.5(2), leading terms: the leading term of a B-linear map of filtration
order r between filtered lifts is a homogeneous Λ-linear map of degree r.
theorem
MultiplicativeBasisDeformations.PosFiltration.orderGe_bot
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{NN : GExt.GMod (GExt.GAlg.ofLen G h1) N}
(g : M →ₗ[k] N)
:
GExt.OrderGe MM NN (-↑(GExt.degBound MM.gr + GExt.degBound NN.gr + 1)) g
Every map of the lifts has some (negative) filtration order.
theorem
MultiplicativeBasisDeformations.PosFiltration.orderGe_succ
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{NN : GExt.GMod (GExt.GAlg.ofLen G h1) N}
{r : ℤ}
{g : M →ₗ[k] N}
(hord : GExt.OrderGe MM NN r g)
(h0 : MM.gr.comp NN.gr r g = 0)
:
GExt.OrderGe MM NN (r + 1) g
theorem
MultiplicativeBasisDeformations.PosFiltration.fLift_orderGe_zero_of_split
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{NN : GExt.GMod (GExt.GAlg.ofLen G h1) N}
(hS : Nonempty P.Split)
(A : P.FLift h1 MM)
(A' : P.FLift h1 NN)
(hneg :
∀ r < 0,
∀ (f : M →ₗ[k] N),
(∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a) →
(∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r) (f m)) → f = 0)
(g : M →ₗ[k] N)
(hg : ∀ (m : M) (x : B), g ((A.act m) x) = (A'.act (g m)) x)
:
GExt.OrderGe MM NN 0 g
Proposition 6.5(3), first part: if the graded Hom_Λ(M, N) vanishes in negative
degrees, every B-linear map of the lifts has filtration order ≥ 0.
theorem
MultiplicativeBasisDeformations.PosFiltration.fLift_gr_hom_of_split
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{NN : GExt.GMod (GExt.GAlg.ofLen G h1) N}
(hS : Nonempty P.Split)
(A : P.FLift h1 MM)
(A' : P.FLift h1 NN)
(r : ℕ)
(hExt : ∀ (t : ℕ), 0 < t → GExt.ExtVanish MM NN 0 (↑r + ↑t))
:
(∀ (g : M →ₗ[k] N), GExt.OrderGe MM NN (↑r) g → (MM.gr.comp NN.gr (↑r) g = 0 ↔ GExt.OrderGe MM NN (↑r + 1) g)) ∧ ∀ (f : M →ₗ[k] N),
(∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a) →
(∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + ↑r) (f m)) →
∃ (g : M →ₗ[k] N),
(∀ (m : M) (x : B), g ((A.act m) x) = (A'.act (g m)) x) ∧ GExt.OrderGe MM NN (↑r) g ∧ MM.gr.comp NN.gr (↑r) g = f
Proposition 6.5(2), the associated graded Hom spaces: for r ≥ 0, a B-linear map of
order r has leading term zero exactly when it has order r + 1, and every homogeneous
Λ-linear map of degree r is a leading term.
The forms with vertex idempotents (S = Λ₀ ≅ kⁿ); for a split semisimple S the splitting is
PosFiltration.nonempty_split_ss.
theorem
MultiplicativeBasisDeformations.PosFiltration.fLift_unique
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
[AddCommGroup M]
[Module k M]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
(V : G.Vertices)
(hExt : ∀ (t : ℕ), 0 < t → GExt.ExtVanish MM MM 0 ↑t)
(A A' : P.FLift h1 MM)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.fLift_map
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{NN : GExt.GMod (GExt.GAlg.ofLen G h1) N}
(V : G.Vertices)
(A : P.FLift h1 MM)
(A' : P.FLift h1 NN)
(r : ℕ)
(f : M →ₗ[k] N)
(hf : ∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a)
(hfd : ∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + ↑r) (f m))
(hExt : ∀ (t : ℕ), 0 < t → GExt.ExtVanish MM NN 0 (↑r + ↑t))
:
theorem
MultiplicativeBasisDeformations.PosFiltration.fLift_leading
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{NN : GExt.GMod (GExt.GAlg.ofLen G h1) N}
(V : G.Vertices)
(A : P.FLift h1 MM)
(A' : P.FLift h1 NN)
{r : ℤ}
(g : M →ₗ[k] N)
(hg : ∀ (m : M) (x : B), g ((A.act m) x) = (A'.act (g m)) x)
(hord : GExt.OrderGe MM NN r g)
(m : M)
(a : Λ)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.fLift_orderGe_zero
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{NN : GExt.GMod (GExt.GAlg.ofLen G h1) N}
(V : G.Vertices)
(A : P.FLift h1 MM)
(A' : P.FLift h1 NN)
(hneg :
∀ r < 0,
∀ (f : M →ₗ[k] N),
(∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a) →
(∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + r) (f m)) → f = 0)
(g : M →ₗ[k] N)
(hg : ∀ (m : M) (x : B), g ((A.act m) x) = (A'.act (g m)) x)
:
GExt.OrderGe MM NN 0 g
theorem
MultiplicativeBasisDeformations.PosFiltration.fLift_gr_hom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{M : Type u_1}
{N : Type u_2}
[AddCommGroup M]
[Module k M]
[AddCommGroup N]
[Module k N]
{h1 : G.IsHom 0 1}
{MM : GExt.GMod (GExt.GAlg.ofLen G h1) M}
{NN : GExt.GMod (GExt.GAlg.ofLen G h1) N}
(V : G.Vertices)
(A : P.FLift h1 MM)
(A' : P.FLift h1 NN)
(r : ℕ)
(hExt : ∀ (t : ℕ), 0 < t → GExt.ExtVanish MM NN 0 (↑r + ↑t))
:
(∀ (g : M →ₗ[k] N), GExt.OrderGe MM NN (↑r) g → (MM.gr.comp NN.gr (↑r) g = 0 ↔ GExt.OrderGe MM NN (↑r + 1) g)) ∧ ∀ (f : M →ₗ[k] N),
(∀ (m : M) (a : Λ), f ((MM.act m) a) = (NN.act (f m)) a) →
(∀ (p : ℤ) (m : M), MM.gr.IsHom p m → NN.gr.IsHom (p + ↑r) (f m)) →
∃ (g : M →ₗ[k] N),
(∀ (m : M) (x : B), g ((A.act m) x) = (A'.act (g m)) x) ∧ GExt.OrderGe MM NN (↑r) g ∧ MM.gr.comp NN.gr (↑r) g = f