Internally-graded algebras #
This file defines the typeclass
graded_algebra 𝒜, for working with an algebra
A that is
internally graded by a collection of submodules
𝒜 : ι → submodule R A.
See the docstring of that typeclass for more information.
Main definitions #
graded_algebra 𝒜: the typeclass, which is a combination of
set_like.graded_monoid, and a constructive version of
graded_algebra.decompose : A ≃ₐ[R] ⨁ i, 𝒜 i, which breaks apart an element of the algebra into its constituent pieces.
graded_algebra.proj 𝒜 iis the linear map from
Ato its degree
i : ιcomponent, such that
proj 𝒜 i x = decompose 𝒜 x i.
graded_algebra.support 𝒜 ris the
finset ιcontaining the
i : ιsuch that the degree
ris not zero.
Implementation notes #
For now, we do not have internally-graded semirings and internally-graded rings; these can be
𝒜 : ι → submodule ℕ A and
𝒜 : ι → submodule ℤ A respectively, since all
semirings are ℕ-algebras via
algebra_nat, and all
graded algebra, graded ring, graded semiring, decomposition
- to_graded_monoid : set_like.graded_monoid 𝒜
- decompose' : A → (⨁ (i : ι), ↥(𝒜 i))
- left_inv : function.left_inverse graded_algebra.decompose' ⇑(direct_sum.submodule_coe 𝒜)
- right_inv : function.right_inverse graded_algebra.decompose' ⇑(direct_sum.submodule_coe 𝒜)
A is one that can be decomposed into a collection
submodule R As indexed by
ι such that the canonical map
A → ⨁ i, 𝒜 i is bijective and
respects multiplication, i.e. the product of an element of degree
i and an element of degree
is an element of degree
i + j.
Note that the fact that
A is internally-graded,
graded_algebra 𝒜, implies an externally-graded
direct_sum.galgebra R (λ i, ↥(𝒜 i)), which in turn makes available an
algebra R (⨁ i, 𝒜 i) instance.
A helper to construct a
graded_algebra when the
set_like.graded_monoid structure is already
available. This makes the
left_inv condition easier to prove, and phrases the
condition in a way that allows custom
@[ext] lemmas to apply.
A is graded by
ι with degree
𝒜 i, then it is isomorphic as
an algebra to a direct sum of components.
The projection maps of graded algebra
The support of
r is the
proj R A i r ≠ 0 ↔ i ∈ r.support