English
There is a graded algebra structure on a family of submodules, assembling into a DirectSum GAlgebra.
Русский
Существуют структура градиированной алгебры на семействе подпространств, образующая DirectSum GAlgebra.
LaTeX
$$$$ DirectSum.GAlgebra\; S\; (i \mapsto A_i) $$$$
Lean4
/-- Build a `DirectSum.GAlgebra` instance for a collection of `Submodule`s. -/
instance galgebra [AddMonoid ι] [CommSemiring S] [Semiring R] [Algebra S R] (A : ι → Submodule S R)
[SetLike.GradedMonoid A] : DirectSum.GAlgebra S fun i => A i
where
toFun := ((Algebra.linearMap S R).codRestrict (A 0) <| SetLike.algebraMap_mem_graded A).toAddMonoidHom
map_one := Subtype.ext <| (algebraMap S R).map_one
map_mul _x _y := Sigma.subtype_ext (add_zero 0).symm <| (algebraMap S R).map_mul _ _
commutes := fun _r ⟨i, _xi⟩ => Sigma.subtype_ext ((zero_add i).trans (add_zero i).symm) <| Algebra.commutes _ _
smul_def := fun _r ⟨i, _xi⟩ => Sigma.subtype_ext (zero_add i).symm <| Algebra.smul_def _ _
