The external direct sum of a graded algebra as an internally graded algebra

Let M : ι → Type* be a family of R-modules. Its external direct sum ⨁ i, M i is the internal direct sum of its summands DirectSum.summand R M i, the copies DirectSum.lof R ι M i of the M i (DirectSum.isInternal_summand). When M is a graded R-algebra, that is [DirectSum.GSemiring M] [DirectSum.GAlgebra R M], these submodules make ⨁ i, M i an internally graded algebra in the sense of GradedAlgebra.

Mathlib's constructions with graded rings, such as homogeneous localization and the projective spectrum AlgebraicGeometry.Proj, take an internal grading 𝒜 : ι → Submodule R A of a ring A. The summand grading is how they apply to a graded ring given externally as a family of homogeneous components with a graded multiplication, for instance the graded ring ⨁ n, Γ(Aₙ, U) of sections of a graded algebra on a scheme.

Main definitions

• DirectSum.instGradedAlgebraSummand: for a graded R-algebra M, the summands are a grading of the algebra ⨁ i, M i.

instance DirectSum.instGradedMonoidSummand {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddMonoid ι] [GSemiring M] : SetLike.GradedMonoid (summand R M)

The summands of the direct sum of a graded algebra are closed under the graded multiplication.

@[instance_reducible]

noncomputable instance DirectSum.instGradedAlgebraSummand {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddMonoid ι] [GSemiring M] [GAlgebra R M] : GradedAlgebra (summand R M)

The direct sum of a graded algebra is internally graded by its summands.