Finite normalization of an associative family #
Theorem 7.7 (thm:finite-family-normalization,
characteristic-two-construction.tex). Let Λ be graded with Λ₀ = S
spanned by vertex idempotents, μ_i normalized S-relative two-cocycles of
positive degrees whose classes span HH²(Λ)_{>0}, and m_t = m + Σ t_i μ_i
associative. Then every positive filtered deformation of Λ is isomorphic to a
fibre m_λ, by a filtered map with identity leading terms fixing the lifted
vertex idempotents.
"By Lemma 6.4, after lifting the vertex idempotents and splitting the
filtration, the deformation has multiplication ⋆ on the vector space Λ […]
Suppose it agrees with m_λ in degrees less than q […] Let φ_q be the
degree-q part of ⋆ - m_λ. […] The remaining equation is dφ_q = 0. The
spanning assumption therefore gives scalars c_i and a normalized one-cochain
f_q of degree q such that φ_q = Σ_{q_i = q} c_iμ_i + df_q. Assign
λ_i = c_i for q_i = q […] Pull ⋆ back by 1 - f_q."
Here the stage invariant is Stage (the error ⋆_g - m_λ raises degree by
q); degPart_cocycle is dφ_q = 0, stage_succ the change of variables.
The associativity of m_t over k[t] is used only through its specializations
(FamilyHyp.assoc).
theorem
MultiplicativeBasisDeformations.LenGrading.proj_e
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
(V : G.Vertices)
(i : Fin V.n)
(d : ℕ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.IsRel₂.degPart_rel
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{μ : Λ →ₗ[k] Λ →ₗ[k] Λ}
(hμ : IsRel₂ V μ)
(q : ℕ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.isCocycle₂_of_hom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{μ : Λ →ₗ[k] Λ →ₗ[k] Λ}
(h :
∀ (d e l : ℕ) (a b c : Λ),
G.IsHom d a → G.IsHom e b → G.IsHom l c → a * (μ b) c - (μ (a * b)) c + (μ a) (b * c) - (μ a) b * c = 0)
:
The cocycle expression is additive in each argument, so it suffices to check it on homogeneous elements.
theorem
MultiplicativeBasisDeformations.LenGrading.proj_eq_zero_of_ge
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{m t : ℕ}
{x : Λ}
(hx : G.Ge m x)
(ht : t < m)
:
(G.proj t) x = 0
def
MultiplicativeBasisDeformations.LenGrading.mLam
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{n : ℕ}
(μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ)
(lam : Fin n → k)
:
Λ →ₗ[k] Λ →ₗ[k] Λ
m_λ = m + Σ λ_i μ_i.
Instances For
theorem
MultiplicativeBasisDeformations.LenGrading.mLam_apply
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{n : ℕ}
(μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ)
(lam : Fin n → k)
(a b : Λ)
:
((mLam μ lam) a) b = a * b + ∑ i : Fin n, lam i • ((μ i) a) b
structure
MultiplicativeBasisDeformations.LenGrading.FamilyHyp
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
(V : G.Vertices)
{n : ℕ}
(μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ)
(qd : Fin n → ℕ)
:
The hypotheses of Theorem 7.8.
Instances For
def
MultiplicativeBasisDeformations.LenGrading.conj
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
(g : Λ ≃ₗ[k] Λ)
(T : Λ →ₗ[k] Λ →ₗ[k] Λ)
:
Λ →ₗ[k] Λ →ₗ[k] Λ
Conjugation of a product by a linear automorphism: g⁻¹(T(ga, gb)).
Instances For
theorem
MultiplicativeBasisDeformations.LenGrading.conj_apply
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
(g : Λ ≃ₗ[k] Λ)
(T : Λ →ₗ[k] Λ →ₗ[k] Λ)
(a b : Λ)
:
((conj g T) a) b = g.symm ((T (g a)) (g b))
def
MultiplicativeBasisDeformations.LenGrading.star
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{B : Type w}
[Ring B]
[Algebra k B]
(φ : Λ ≃ₗ[k] B)
:
Λ →ₗ[k] Λ →ₗ[k] Λ
The transported product a ⋆ b = φ⁻¹(φa φb).
Instances For
theorem
MultiplicativeBasisDeformations.LenGrading.star_e_left
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{B : Type w}
[Ring B]
[Algebra k B]
{φ : Λ ≃ₗ[k] B}
(hφl : ∀ (i : Fin V.n) (a : Λ), φ (V.e i * a) = φ (V.e i) * φ a)
(i : Fin V.n)
(b : Λ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.star_e_right
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{B : Type w}
[Ring B]
[Algebra k B]
{φ : Λ ≃ₗ[k] B}
(hφr : ∀ (i : Fin V.n) (a : Λ), φ (a * V.e i) = φ a * φ (V.e i))
(i : Fin V.n)
(a : Λ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.mem_F_of_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}
{φ : Λ ≃ₗ[k] B}
(hFφ : ∀ (d : ℕ), Submodule.map (↑φ) (G.geSub d) = P.F d)
{d : ℕ}
{a : Λ}
(ha : G.Ge d a)
:
φ a ∈ P.F d
theorem
MultiplicativeBasisDeformations.LenGrading.ge_of_mem_F
{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}
{φ : Λ ≃ₗ[k] B}
(hFφ : ∀ (d : ℕ), Submodule.map (↑φ) (G.geSub d) = P.F d)
{d : ℕ}
{x : B}
(hx : x ∈ P.F d)
:
G.Ge d (φ.symm x)
theorem
MultiplicativeBasisDeformations.LenGrading.star_raises
{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}
{φ : Λ ≃ₗ[k] B}
(hσφ : ∀ (d : ℕ) (a : Λ), G.IsHom d a → (P.σ d) (φ a) = a)
(hFφ : ∀ (d : ℕ), Submodule.map (↑φ) (G.geSub d) = P.F d)
:
The transported product differs from m in positive degrees (Lemma 6.4).
structure
MultiplicativeBasisDeformations.LenGrading.Stage
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
{B : Type w}
[Ring B]
[Algebra k B]
{φ : Λ ≃ₗ[k] B}
(q : ℕ)
(g : Λ ≃ₗ[k] Λ)
(lam : Fin n → k)
:
The stage invariant: after the change of variables g, the product
agrees with m_λ below degree q.
- lead : G.Raises₁ 1 (↑g - LinearMap.id)
- leadInv : G.Raises₁ 1 (↑g.symm - LinearMap.id)
- zero (i : Fin n) : q ≤ qd i → lam i = 0
Instances For
theorem
MultiplicativeBasisDeformations.LenGrading.mLam_left
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
(H : FamilyHyp V μ qd)
(lam : Fin n → k)
(i : Fin V.n)
(a b : Λ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.mLam_mid
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
(H : FamilyHyp V μ qd)
(lam : Fin n → k)
(i : Fin V.n)
(a b : Λ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.mLam_right
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
(H : FamilyHyp V μ qd)
(lam : Fin n → k)
(i : Fin V.n)
(a b : Λ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.mLam_e_left
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
(H : FamilyHyp V μ qd)
(lam : Fin n → k)
(i : Fin V.n)
(b : Λ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.mLam_e_right
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
(H : FamilyHyp V μ qd)
(lam : Fin n → k)
(i : Fin V.n)
(a : Λ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.mLam_sub_mul
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
(H : FamilyHyp V μ qd)
(lam : Fin n → k)
:
theorem
MultiplicativeBasisDeformations.LenGrading.T_e_left
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
{B : Type w}
[Ring B]
[Algebra k B]
{φ : Λ ≃ₗ[k] B}
(hφl : ∀ (i : Fin V.n) (a : Λ), φ (V.e i * a) = φ (V.e i) * φ a)
{q : ℕ}
{g : Λ ≃ₗ[k] Λ}
{lam : Fin n → k}
(hS : Stage q g lam)
(i : Fin V.n)
(b : Λ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.T_e_right
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
{B : Type w}
[Ring B]
[Algebra k B]
{φ : Λ ≃ₗ[k] B}
(hφr : ∀ (i : Fin V.n) (a : Λ), φ (a * V.e i) = φ a * φ (V.e i))
{q : ℕ}
{g : Λ ≃ₗ[k] Λ}
{lam : Fin n → k}
(hS : Stage q g lam)
(i : Fin V.n)
(a : Λ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.err_rel
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
(H : FamilyHyp V μ qd)
{B : Type w}
[Ring B]
[Algebra k B]
{φ : Λ ≃ₗ[k] B}
(hφl : ∀ (i : Fin V.n) (a : Λ), φ (V.e i * a) = φ (V.e i) * φ a)
(hφr : ∀ (i : Fin V.n) (a : Λ), φ (a * V.e i) = φ a * φ (V.e i))
{q : ℕ}
{g : Λ ≃ₗ[k] Λ}
{lam : Fin n → k}
(hS : Stage q g lam)
:
The error ⋆_g - m_λ is a normalized relative two-cochain.
theorem
MultiplicativeBasisDeformations.LenGrading.T_sub_mul_raises
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
(H : FamilyHyp V μ qd)
{B : Type w}
[Ring B]
[Algebra k B]
{φ : Λ ≃ₗ[k] B}
{q : ℕ}
{g : Λ ≃ₗ[k] Λ}
{lam : Fin n → k}
(hS : Stage q g lam)
(hq : 1 ≤ q)
:
theorem
MultiplicativeBasisDeformations.LenGrading.stage_cocycle
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
(H : FamilyHyp V μ qd)
{B : Type w}
[Ring B]
[Algebra k B]
{φ : Λ ≃ₗ[k] B}
{q : ℕ}
{g : Λ ≃ₗ[k] Λ}
{lam : Fin n → k}
(hS : Stage q g lam)
(hq : 1 ≤ q)
:
IsCocycle₂ (degPart q (conj g (star φ) - mLam μ lam))
dφ_q = 0: the degree-q part of the error is a cocycle.
theorem
MultiplicativeBasisDeformations.LenGrading.ge_of_N_eq_zero
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
(hN : G.N = 0)
(m : ℕ)
(x : Λ)
:
G.Ge m x
theorem
MultiplicativeBasisDeformations.LenGrading.Raises₁.pow
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{q : ℕ}
{f : Λ →ₗ[k] Λ}
(hf : G.Raises₁ q f)
(m : ℕ)
:
G.Raises₁ (m * q) (f ^ m)
theorem
MultiplicativeBasisDeformations.LenGrading.Raises₁.pow_eq_zero
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{q : ℕ}
{f : Λ →ₗ[k] Λ}
(hf : G.Raises₁ q f)
(hq : 1 ≤ q)
:
f ^ (G.N + 1) = 0
def
MultiplicativeBasisDeformations.LenGrading.oneSub
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{q : ℕ}
(f : Λ →ₗ[k] Λ)
(hf : G.Raises₁ q f)
(hq : 1 ≤ q)
:
Λ ≃ₗ[k] Λ
1 - f for a degree-raising f, with inverse Σ fⁱ.
Instances For
theorem
MultiplicativeBasisDeformations.LenGrading.oneSub_apply
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{q : ℕ}
(f : Λ →ₗ[k] Λ)
(hf : G.Raises₁ q f)
(hq : 1 ≤ q)
(a : Λ)
:
(oneSub f hf hq) a = a - f a
theorem
MultiplicativeBasisDeformations.LenGrading.oneSub_symm_apply
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{q : ℕ}
(f : Λ →ₗ[k] Λ)
(hf : G.Raises₁ q f)
(hq : 1 ≤ q)
(a : Λ)
:
theorem
MultiplicativeBasisDeformations.LenGrading.stage_succ
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
(H : FamilyHyp V μ qd)
{B : Type w}
[Ring B]
[Algebra k B]
{φ : Λ ≃ₗ[k] B}
(hφl : ∀ (i : Fin V.n) (a : Λ), φ (V.e i * a) = φ (V.e i) * φ a)
(hφr : ∀ (i : Fin V.n) (a : Λ), φ (a * V.e i) = φ a * φ (V.e i))
{q : ℕ}
{g : Λ ≃ₗ[k] Λ}
{lam : Fin n → k}
(hS : Stage q g lam)
(hq : 1 ≤ q)
:
∃ (g' : Λ ≃ₗ[k] Λ) (lam' : Fin n → k), Stage (q + 1) g' lam'
The change of variables 1 - f_q: the stage invariant passes from q
to q + 1.
theorem
MultiplicativeBasisDeformations.LenGrading.stage_one
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{φ : Λ ≃ₗ[k] B}
(hσφ : ∀ (d : ℕ) (a : Λ), G.IsHom d a → (P.σ d) (φ a) = a)
(hFφ : ∀ (d : ℕ), Submodule.map (↑φ) (G.geSub d) = P.F d)
:
Stage 1 (LinearEquiv.refl k Λ) 0
theorem
MultiplicativeBasisDeformations.LenGrading.exists_stage
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
(H : FamilyHyp V μ qd)
{B : Type w}
[Ring B]
[Algebra k B]
{P : PosFiltration G B}
{φ : Λ ≃ₗ[k] B}
(hφl : ∀ (i : Fin V.n) (a : Λ), φ (V.e i * a) = φ (V.e i) * φ a)
(hφr : ∀ (i : Fin V.n) (a : Λ), φ (a * V.e i) = φ a * φ (V.e i))
(hσφ : ∀ (d : ℕ) (a : Λ), G.IsHom d a → (P.σ d) (φ a) = a)
(hFφ : ∀ (d : ℕ), Submodule.map (↑φ) (G.geSub d) = P.F d)
(m : ℕ)
:
∃ (g : Λ ≃ₗ[k] Λ) (lam : Fin n → k), Stage (m + 1) g lam
theorem
MultiplicativeBasisDeformations.LenGrading.finiteFamilyNormalization
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{V : G.Vertices}
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
(H : FamilyHyp V μ qd)
{B : Type w}
[Ring B]
[Algebra k B]
(P : PosFiltration G B)
:
Theorem 7.7 (finite normalization of an associative family).