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) [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [AddMonoid ι] [DirectSum.GSemiring A] : Type (max uA uR)

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

• toFun : R →+ A 0
• map_one : DirectSum.GAlgebra.toFun 1 = GradedMonoid.GOne.one
• map_mul : ∀ (r s : R), GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun (r * s)) = GradedMonoid.mk (0 + 0) (GradedMonoid.GMul.mul (DirectSum.GAlgebra.toFun r) (DirectSum.GAlgebra.toFun s))
• commutes : ∀ (r : R) (x : GradedMonoid A), GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun r) * x = x * GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun r)
• smul_def : ∀ (r : R) (x : GradedMonoid A), r • x = GradedMonoid.mk 0 (DirectSum.GAlgebra.toFun r) * x

instance GradedMonoid.smulCommClass_right {ι : Type uι} (R : Type uR) (A : ι → Type uA) [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [DirectSum.GAlgebra R A] : SMulCommClass R (GradedMonoid A) (GradedMonoid A)

Equations

• ⋯ = ⋯

instance GradedMonoid.isScalarTower_right {ι : Type uι} (R : Type uR) (A : ι → Type uA) [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [DirectSum.GAlgebra R A] : IsScalarTower R (GradedMonoid A) (GradedMonoid A)

Equations

• ⋯ = ⋯

instance DirectSum.instAlgebra {ι : Type uι} (R : Type uR) (A : ι → Type uA) [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [DirectSum.GAlgebra R A] [DecidableEq ι] : Algebra R (DirectSum ι fun (i : ι) => A i)

Equations

• DirectSum.instAlgebra R A = Algebra.mk { toFun := ⇑((DirectSum.of A 0).comp DirectSum.GAlgebra.toFun), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

theorem DirectSum.algebraMap_apply {ι : Type uι} (R : Type uR) (A : ι → Type uA) [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [DirectSum.GAlgebra R A] [DecidableEq ι] (r : R) : (algebraMap R (DirectSum ι fun (i : ι) => A i)) r = (DirectSum.of A 0) (DirectSum.GAlgebra.toFun r)

theorem DirectSum.algebraMap_toAddMonoid_hom {ι : Type uι} (R : Type uR) (A : ι → Type uA) [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [DirectSum.GAlgebra R A] [DecidableEq ι] : ↑(algebraMap R (DirectSum ι fun (i : ι) => A i)) = (DirectSum.of A 0).comp DirectSum.GAlgebra.toFun

def DirectSum.toAlgebra {ι : Type uι} (R : Type uR) (A : ι → Type uA) {B : Type uB} [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [Semiring B] [DirectSum.GAlgebra R A] [Algebra R B] [DecidableEq ι] (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)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) : (DirectSum ι fun (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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DirectSum.toAlgebra_apply {ι : Type uι} (R : Type uR) (A : ι → Type uA) {B : Type uB} [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [Semiring B] [DirectSum.GAlgebra R A] [Algebra R B] [DecidableEq ι] (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)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) (a : DirectSum ι fun (i : ι) => A i) : (DirectSum.toAlgebra R A f hone hmul) a = (DirectSum.toSemiring (fun (i : ι) => (f i).toAddMonoidHom) hone hmul) a

theorem DirectSum.algHom_ext' {ι : Type uι} (R : Type uR) (A : ι → Type uA) {B : Type uB} [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [Semiring B] [DirectSum.GAlgebra R A] [Algebra R B] [DecidableEq ι] ⦃f g : (DirectSum ι fun (i : ι) => A i) →ₐ[R] B⦄ (h : ∀ (i : ι), f.toLinearMap ∘ₗ DirectSum.lof R ι A i = g.toLinearMap ∘ₗ 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} [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [Semiring B] [DirectSum.GAlgebra R A] [Algebra R B] [DecidableEq ι] ⦃f g : (DirectSum ι fun (i : ι) => A i) →ₐ[R] B⦄ (h : ∀ (i : ι) (x : A i), f ((DirectSum.of A i) x) = g ((DirectSum.of A i) x)) : f = g

def DirectSum.gMulLHom {ι : Type uι} (R : Type uR) (A : ι → Type uA) [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [DirectSum.GAlgebra R A] {i j : ι} : A i →ₗ[R] A j →ₗ[R] A (i + j)

The piecewise multiplication from the Mul instance, as a bundled linear homomorphism.

This is the graded version of LinearMap.mul, and the linear version of DirectSum.gMulHom

Equations

• DirectSum.gMulLHom R A = { toFun := fun (a : A i) => { toFun := fun (b : A j) => GradedMonoid.GMul.mul a b, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem DirectSum.gMulLHom_apply_apply {ι : Type uι} (R : Type uR) (A : ι → Type uA) [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [AddMonoid ι] [DirectSum.GSemiring A] [DirectSum.GAlgebra R A] {i j : ι} (a : A i) (b : A j) : ((DirectSum.gMulLHom R A) a) b = GradedMonoid.GMul.mul a b

Concrete instances

instance Algebra.directSumGAlgebra {ι : Type uι} {R : Type u_1} {A : Type u_2} [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] : DirectSum.GAlgebra R fun (x : ι) => A

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

Equations

• Algebra.directSumGAlgebra = { toFun := (algebraMap R A).toAddMonoidHom, map_one := ⋯, map_mul := ⋯, commutes := ⋯, smul_def := ⋯ }

@[simp]

theorem Algebra.directSumGAlgebra_toFun_apply {ι : Type uι} {R : Type u_1} {A : Type u_2} [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] (a✝ : R) : DirectSum.GAlgebra.toFun a✝ = (↑↑(algebraMap R A)).toFun a✝