The trivial grading of an algebra #
The trivial grading TauCeti.trivialGrading of TauCeti.Algebra.Module.GradedModule.Trivial,
concentrated in degree zero, is an internal GradedAlgebra when the module is an algebra. This
file records that instance, whose decomposition and degree projection come from the module-level
file. This grading is the canonical target for augmentations of integer-graded algebras and the
grading of coefficients in degree-zero examples.
Main results #
TauCeti.instGradedAlgebraTrivialGrading: the trivial grading of an algebra is a graded algebra.
@[instance_reducible]
instance
TauCeti.instGradedAlgebraTrivialGrading
(R : Type u_1)
(A : Type u_2)
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
GradedAlgebra (trivialGrading R A)
The trivial grading is an internal grading: an element is its own degree-zero component, and all nonzero-degree components vanish.