# Documentation

Mathlib.Algebra.DirectSum.Algebra

# Additively-graded algebra structures on ⨁ i, A i#

This file provides R-algebra structures on external direct sums of R-modules.

Recall that if A i are a family of AddCommMonoids indexed by an AddMonoid, then an instance of DirectSum.GMonoid A is a multiplication A i → A j → A (i + j) giving ⨁ i, A i the structure of a semiring. In this file, we introduce the DirectSum.GAlgebra R A class for the case where all A i are R-modules. This is the extra structure needed to promote ⨁ i, A i to an R-algebra.

## Main definitions #

• DirectSum.GAlgebra R A, the typeclass.
• DirectSum.toAlgebra extends DirectSum.toSemiring to produce an AlgHom.
class DirectSum.GAlgebra {ι : Type uι} (R : Type uR) (A : ιType uA) [] [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [] :
Type (max uA uR)
• toFun : R →+ A 0
• map_one : DirectSum.GAlgebra.toFun 1 = GradedMonoid.GOne.one
• map_mul : ∀ (r s_1 : R), GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun (r * s_1)) = { fst := 0 + 0, snd := GradedMonoid.GMul.mul (DirectSum.GAlgebra.toFun r) (DirectSum.GAlgebra.toFun s_1) }
• commutes : ∀ (r : R) (x : ), GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun r) * x = x * { fst := 0, snd := DirectSum.GAlgebra.toFun r }
• smul_def : ∀ (r : R) (x : ), GradedMonoid.mk x.fst (r x.snd) = { fst := 0, snd := DirectSum.GAlgebra.toFun r } * x

A graded version of Algebra. An instance of DirectSum.GAlgebra R A endows (⨁ i, A i) with an R-algebra structure.

Instances
instance DirectSum.instAlgebraDirectSumSemiring {ι : Type uι} (R : Type uR) (A : ιType uA) [] [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [] [] :
Algebra R (⨁ (i : ι), A i)
theorem DirectSum.algebraMap_apply {ι : Type uι} (R : Type uR) (A : ιType uA) [] [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [] [] (r : R) :
↑(algebraMap R (⨁ (i : ι), A i)) r = ↑() (DirectSum.GAlgebra.toFun r)
theorem DirectSum.algebraMap_toAddMonoid_hom {ι : Type uι} (R : Type uR) (A : ιType uA) [] [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [] [] :
↑(algebraMap R (⨁ (i : ι), A i)) = AddMonoidHom.comp () DirectSum.GAlgebra.toFun
@[simp]
theorem DirectSum.toAlgebra_apply {ι : Type uι} (R : Type uR) (A : ιType uA) {B : Type uB} [] [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [] [] [] [Algebra R B] (f : (i : ι) → A i →ₗ[R] B) (hone : ↑(f 0) GradedMonoid.GOne.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ↑(f (i + j)) () = ↑(f i) ai * ↑(f j) aj) (hcommutes : ∀ (r : R), ↑(f 0) (DirectSum.GAlgebra.toFun r) = ↑() r) (a : ⨁ (i : ι), A i) :
↑(DirectSum.toAlgebra R A f hone hmul hcommutes) a = ↑(DirectSum.toSemiring (fun i => ) hone hmul) a
def DirectSum.toAlgebra {ι : Type uι} (R : Type uR) (A : ιType uA) {B : Type uB} [] [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [] [] [] [Algebra R B] (f : (i : ι) → A i →ₗ[R] B) (hone : ↑(f 0) GradedMonoid.GOne.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ↑(f (i + j)) () = ↑(f i) ai * ↑(f j) aj) (hcommutes : ∀ (r : R), ↑(f 0) (DirectSum.GAlgebra.toFun r) = ↑() r) :
(⨁ (i : ι), A i) →ₐ[R] B

A family of LinearMaps preserving DirectSum.GOne.one and DirectSum.GMul.mul describes an AlgHom on ⨁ i, A i. This is a stronger version of DirectSum.toSemiring.

Of particular interest is the case when A i are bundled subojects, f is the family of coercions such as Submodule.subtype (A i), and the [GMonoid A] structure originates from DirectSum.GMonoid.ofAddSubmodules, in which case the proofs about GOne and GMul can be discharged by rfl.

Instances For
theorem DirectSum.algHom_ext' {ι : Type uι} (R : Type uR) (A : ιType uA) {B : Type uB} [] [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [] [] [] [Algebra R B] ⦃f : (⨁ (i : ι), A i) →ₐ[R] B ⦃g : (⨁ (i : ι), A i) →ₐ[R] B (h : ∀ (i : ι), LinearMap.comp () (DirectSum.lof R ι A i) = LinearMap.comp () (DirectSum.lof R ι A i)) :
f = g

Two AlgHoms out of a direct sum are equal if they agree on the generators.

See note [partially-applied ext lemmas].

theorem DirectSum.algHom_ext {ι : Type uι} (R : Type uR) (A : ιType uA) {B : Type uB} [] [] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [] [] [] [Algebra R B] ⦃f : (⨁ (i : ι), A i) →ₐ[R] B ⦃g : (⨁ (i : ι), A i) →ₐ[R] B (h : ∀ (i : ι) (x : A i), f (↑() x) = g (↑() x)) :
f = g

### Concrete instances #

@[simp]
theorem Algebra.directSumGAlgebra_toFun_apply {ι : Type uι} {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] :
∀ (a : R), DirectSum.GAlgebra.toFun a = OneHom.toFun (↑()) a
instance Algebra.directSumGAlgebra {ι : Type uι} {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] :
DirectSum.GAlgebra R fun x => A

A direct sum of copies of an Algebra inherits the algebra structure.