Multiplicative bases

MultiplicativeBasisDeformations.Foundations.HomBasis

Homogeneous bases of graded vector spaces #

A finite-dimensional ℤ-graded vector space (GExt.ZGr) has a basis of homogeneous vectors (exists_homBasis): it is the internal direct sum of its homogeneous components.

source
@[reducible, inline]
abbrev MultiplicativeBasisDeformations.GExt.homPart {k : Type u_1} [Field k] {M : Type u_2} [AddCommGroup M] [Module k M] (g : ZGr M) (p : ↥g.supp) :
Submodule k M

The homogeneous component of degree p, indexed by the support.

Instances For
    source
    theorem MultiplicativeBasisDeformations.GExt.proj_homPart {k : Type u_1} [Field k] {M : Type u_2} [AddCommGroup M] [Module k M] (g : ZGr M) {p : ℤ} {q : ↥g.supp} {x : M} (hx : x ∈ homPart g q) :
    (g.proj p) x = if ↑q = p then x else 0
    source
    theorem MultiplicativeBasisDeformations.GExt.isInternal_homPart {k : Type u_1} [Field k] {M : Type u_2} [AddCommGroup M] [Module k M] (g : ZGr M) [DecidableEq ↥g.supp] :
    DirectSum.IsInternal (homPart g)
    source
    theorem MultiplicativeBasisDeformations.GExt.exists_homBasis {k : Type u_1} [Field k] {M : Type u_2} [AddCommGroup M] [Module k M] (g : ZGr M) [FiniteDimensional k M] :
    ∃ (n : ℕ) (β : Module.Basis (Fin n) k M) (dβ : Fin n → ℤ), ∀ (i : Fin n), g.IsHom (dβ i) (β i)

    Homogeneous bases.