Gradings with a homogeneous basis #
For a graded algebra with a basis of homogeneous vectors: the coordinates of a homogeneous element vanish off its degree, and a bilinear map is homogeneous of a given degree (or character) as soon as its values on pairs of basis vectors are.
theorem
MultiplicativeBasisDeformations.LenGrading.isHom_smul'
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
(G : LenGrading k Λ)
{d : ℕ}
(c : k)
{x : Λ}
(hx : G.IsHom d x)
:
G.IsHom d (c • x)
theorem
MultiplicativeBasisDeformations.LenGrading.isHom_zero'
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
(G : LenGrading k Λ)
(d : ℕ)
:
G.IsHom d 0
theorem
MultiplicativeBasisDeformations.LenGrading.repr_eq_zero_of_isHom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
(G : LenGrading k Λ)
{ι : Type u_1}
[Fintype ι]
(β : Module.Basis ι k Λ)
(δ : ι → ℕ)
(hβ : ∀ (i : ι), G.IsHom (δ i) (β i))
{d : ℕ}
{a : Λ}
(ha : G.IsHom d a)
{i : ι}
(hi : δ i ≠ d)
:
(β.repr a) i = 0
The coordinates of a homogeneous element vanish off its degree.
theorem
MultiplicativeBasisDeformations.LenGrading.hasDeg₂_of_basis
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
(G : LenGrading k Λ)
{ι : Type u_1}
[Fintype ι]
(β : Module.Basis ι k Λ)
(δ : ι → ℕ)
(hβ : ∀ (i : ι), G.IsHom (δ i) (β i))
(q : ℕ)
(μ : Λ →ₗ[k] Λ →ₗ[k] Λ)
(h : ∀ (i j : ι), G.IsHom (δ i + δ j + q) ((μ (β i)) (β j)))
:
G.HasDeg₂ q μ
A bilinear map homogeneous on basis pairs is homogeneous.
theorem
MultiplicativeBasisDeformations.LatGrading.repr_eq_zero_of_isHom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{ι : Type u_1}
[Fintype ι]
(β : Module.Basis ι k Λ)
(ω : ι → L)
(hβ : ∀ (i : ι), W.IsHom (ω i) (β i))
{l : L}
{a : Λ}
(ha : W.IsHom l a)
{i : ι}
(hi : ω i ≠ l)
:
(β.repr a) i = 0
theorem
MultiplicativeBasisDeformations.LatGrading.char₂_of_basis
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{ι : Type u_1}
[Fintype ι]
(β : Module.Basis ι k Λ)
(ω : ι → L)
(hβ : ∀ (i : ι), W.IsHom (ω i) (β i))
(χ : L)
(μ : Λ →ₗ[k] Λ →ₗ[k] Λ)
(h : ∀ (i j : ι), W.IsHom (ω i + ω j + χ) ((μ (β i)) (β j)))
:
W.Char₂ χ μ
A bilinear map of character χ on basis pairs has character χ.