The dimension of a positive filtered deformation #
A positive filtered deformation B of Λ (Definition 6.2) has dim B = dim Λ: each layer
F^d/F^{d+1} is identified with Λ_d by the leading-term map.
theorem
MultiplicativeBasisDeformations.LenGrading.finrank_eq_sum
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
[FiniteDimensional k Λ]
(G : LenGrading k Λ)
:
A graded algebra is the sum of its components.
theorem
MultiplicativeBasisDeformations.PosFiltration.finrank_step
{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)
[FiniteDimensional k B]
(d : ℕ)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.finrank_F_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)
[FiniteDimensional k B]
(n : ℕ)
:
theorem
MultiplicativeBasisDeformations.PosFiltration.finrank_eq
{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)
[FiniteDimensional k B]
[FiniteDimensional k Λ]
:
Module.finrank k B = Module.finrank k Λ
A positive filtered deformation has the dimension of Λ.