English
The construction DirectSum.IsInternal provides a framework to regard the ambient algebra as a graded algebra with homogeneous parts M(i).
Русский
Конструкция DirectSum.IsInternal задаёт рамку для восприятия окружающей алгебры как градуированной, имеющей однородные части M(i).
LaTeX
$$$DirectSum.IsInternal M \Rightarrow GradedAlgebra M$.$$
Lean4
/-- Given an `R`-algebra `A` and a family `ι → Submodule R A` of submodules
parameterized by an additive monoid `ι`
and satisfying `SetLike.GradedMonoid M` (essentially, is multiplicative)
such that `DirectSum.IsInternal M` (`A` is the direct sum of the `M i`),
we endow `A` with the structure of a graded algebra.
The submodules are the *homogeneous* parts. -/
noncomputable def gradedAlgebra (hM : DirectSum.IsInternal M) : GradedAlgebra M :=
{
(inferInstance : SetLike.GradedMonoid
M) with
decompose' := hM.coeAlgEquiv.symm
left_inv := hM.coeAlgEquiv.symm.left_inv
right_inv := hM.coeAlgEquiv.left_inv }
