# Documentation

Mathlib.Algebra.DirectSum.Internal

# Internally graded rings and algebras #

This module provides DirectSum.GSemiring and DirectSum.GCommSemiring instances for a collection of subobjects A when a SetLike.GradedMonoid instance is available:

• SetLike.gnonUnitalNonAssocSemiring
• SetLike.gsemiring
• SetLike.gcommSemiring

With these instances in place, it provides the bundled canonical maps out of a direct sum of subobjects into their carrier type:

• DirectSum.coeRingHom (a RingHom version of DirectSum.coeAddMonoidHom)
• DirectSum.coeAlgHom (an AlgHom version of DirectSum.coeLinearMap)

Strictly the definitions in this file are not sufficient to fully define an "internal" direct sum; to represent this case, (h : DirectSum.IsInternal A) [SetLike.GradedMonoid A] is needed. In the future there will likely be a data-carrying, constructive, typeclass version of DirectSum.IsInternal for providing an explicit decomposition function.

When CompleteLattice.Independent (Set.range A) (a weaker condition than DirectSum.IsInternal A), these provide a grading of ⨆ i, A i, and the mapping ⨁ i, A i →+ ⨆ i, A i can be obtained as DirectSum.toAddMonoid (fun i ↦ AddSubmonoid.inclusion \$ le_iSup A i).

## tags #

instance AddCommMonoid.ofSubmonoidOnSemiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [SetLike σ R] [] (A : ισ) (i : ι) :
AddCommMonoid { x // x A i }
instance AddCommGroup.ofSubgroupOnRing {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Ring R] [SetLike σ R] [] (A : ισ) (i : ι) :
AddCommGroup { x // x A i }
theorem SetLike.algebraMap_mem_graded {ι : Type u_1} {S : Type u_3} {R : Type u_4} [Zero ι] [] [] [Algebra S R] (A : ι) (s : S) :
↑() s A 0
theorem SetLike.nat_cast_mem_graded {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Zero ι] [] [SetLike σ R] [] (A : ισ) (n : ) :
n A 0
theorem SetLike.int_cast_mem_graded {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Zero ι] [] [SetLike σ R] [] (A : ισ) (z : ) :
z A 0

#### From AddSubmonoids and AddSubgroups #

instance SetLike.gnonUnitalNonAssocSemiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Add ι] [SetLike σ R] [] (A : ισ) :

Build a DirectSum.GNonUnitalNonAssocSemiring instance for a collection of additive submonoids.

instance SetLike.gsemiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) :
DirectSum.GSemiring fun i => { x // x A i }

Build a DirectSum.GSemiring instance for a collection of additive submonoids.

instance SetLike.gcommSemiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) :
DirectSum.GCommSemiring fun i => { x // x A i }

Build a DirectSum.GCommSemiring instance for a collection of additive submonoids.

instance SetLike.gring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [Ring R] [SetLike σ R] [] (A : ισ) :
DirectSum.GRing fun i => { x // x A i }

Build a DirectSum.GRing instance for a collection of additive subgroups.

instance SetLike.gcommRing {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) :
DirectSum.GCommRing fun i => { x // x A i }

Build a DirectSum.GCommRing instance for a collection of additive submonoids.

def DirectSum.coeRingHom {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) [] :
(⨁ (i : ι), { x // x A i }) →+* R

The canonical ring isomorphism between ⨁ i, A i and R

Instances For
@[simp]
theorem DirectSum.coeRingHom_of {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) [] (i : ι) (x : { x // x A i }) :
↑() (↑(DirectSum.of (fun i => { x // x A i }) i) x) = x

The canonical ring isomorphism between ⨁ i, A i and R

theorem DirectSum.coe_mul_apply {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) [] [(i : ι) → (x : { x // x A i }) → Decidable (x 0)] (r : ⨁ (i : ι), { x // x A i }) (r' : ⨁ (i : ι), { x // x A i }) (n : ι) :
↑(↑(r * r') n) = Finset.sum (Finset.filter (fun ij => ij.fst + ij.snd = n) ()) fun ij => ↑(r ij.fst) * ↑(r' ij.snd)
theorem DirectSum.coe_mul_apply_eq_dfinsupp_sum {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) [] [(i : ι) → (x : { x // x A i }) → Decidable (x 0)] (r : ⨁ (i : ι), { x // x A i }) (r' : ⨁ (i : ι), { x // x A i }) (n : ι) :
↑(↑(r * r') n) = DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ri * rj else 0
theorem DirectSum.coe_of_mul_apply_aux {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) [] {i : ι} (r : { x // x A i }) (r' : ⨁ (i : ι), { x // x A i }) {j : ι} {n : ι} (H : ∀ (x : ι), i + x = n x = j) :
↑(↑(↑(DirectSum.of (fun i => { x // x A i }) i) r * r') n) = r * ↑(r' j)
theorem DirectSum.coe_mul_of_apply_aux {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) [] (r : ⨁ (i : ι), { x // x A i }) {i : ι} (r' : { x // x A i }) {j : ι} {n : ι} (H : ∀ (x : ι), x + i = n x = j) :
↑(↑(r * ↑(DirectSum.of (fun i => { x // x A i }) i) r') n) = ↑(r j) * r'
theorem DirectSum.coe_of_mul_apply_add {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) {i : ι} (r : { x // x A i }) (r' : ⨁ (i : ι), { x // x A i }) (j : ι) :
↑(↑(↑(DirectSum.of (fun i => { x // x A i }) i) r * r') (i + j)) = r * ↑(r' j)
theorem DirectSum.coe_mul_of_apply_add {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) (r : ⨁ (i : ι), { x // x A i }) {i : ι} (r' : { x // x A i }) (j : ι) :
↑(↑(r * ↑(DirectSum.of (fun i => { x // x A i }) i) r') (j + i)) = ↑(r j) * r'
theorem DirectSum.coe_of_mul_apply_of_not_le {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) {i : ι} (r : { x // x A i }) (r' : ⨁ (i : ι), { x // x A i }) (n : ι) (h : ¬i n) :
↑(↑(↑(DirectSum.of (fun i => { x // x A i }) i) r * r') n) = 0
theorem DirectSum.coe_mul_of_apply_of_not_le {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) (r : ⨁ (i : ι), { x // x A i }) {i : ι} (r' : { x // x A i }) (n : ι) (h : ¬i n) :
↑(↑(r * ↑(DirectSum.of (fun i => { x // x A i }) i) r') n) = 0
theorem DirectSum.coe_mul_of_apply_of_le {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) [Sub ι] [] [ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x x_1] (r : ⨁ (i : ι), { x // x A i }) {i : ι} (r' : { x // x A i }) (n : ι) (h : i n) :
↑(↑(r * ↑(DirectSum.of (fun i => { x // x A i }) i) r') n) = ↑(r (n - i)) * r'
theorem DirectSum.coe_of_mul_apply_of_le {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) [Sub ι] [] [ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x x_1] {i : ι} (r : { x // x A i }) (r' : ⨁ (i : ι), { x // x A i }) (n : ι) (h : i n) :
↑(↑(↑(DirectSum.of (fun i => { x // x A i }) i) r * r') n) = r * ↑(r' (n - i))
theorem DirectSum.coe_mul_of_apply {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) [Sub ι] [] [ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x x_1] (r : ⨁ (i : ι), { x // x A i }) {i : ι} (r' : { x // x A i }) (n : ι) [Decidable (i n)] :
↑(↑(r * ↑(DirectSum.of (fun i => { x // x A i }) i) r') n) = if i n then ↑(r (n - i)) * r' else 0
theorem DirectSum.coe_of_mul_apply {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [] [] [SetLike σ R] [] (A : ισ) [Sub ι] [] [ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x x_1] {i : ι} (r : { x // x A i }) (r' : ⨁ (i : ι), { x // x A i }) (n : ι) [Decidable (i n)] :
↑(↑(↑(DirectSum.of (fun i => { x // x A i }) i) r * r') n) = if i n then r * ↑(r' (n - i)) else 0

#### From Submodules #

instance Submodule.galgebra {ι : Type u_1} {S : Type u_3} {R : Type u_4} [] [] [] [] [Algebra S R] (A : ι) :
DirectSum.GAlgebra S fun i => { x // x A i }

Build a DirectSum.GAlgebra instance for a collection of Submodules.

@[simp]
theorem Submodule.setLike.coe_galgebra_toFun {ι : Type u_1} {S : Type u_3} {R : Type u_4} [] [] [] [] [Algebra S R] (A : ι) (s : S) :
↑(DirectSum.GAlgebra.toFun s) = ↑() s
instance Submodule.nat_power_gradedMonoid {S : Type u_3} {R : Type u_4} [] [] [Algebra S R] (p : ) :
SetLike.GradedMonoid fun i => p ^ i

A direct sum of powers of a submodule of an algebra has a multiplicative structure.

def DirectSum.coeAlgHom {ι : Type u_1} {S : Type u_3} {R : Type u_4} [] [] [] [] [Algebra S R] (A : ι) :
(⨁ (i : ι), { x // x A i }) →ₐ[S] R

The canonical algebra isomorphism between ⨁ i, A i and R.

Instances For
theorem Submodule.iSup_eq_toSubmodule_range {ι : Type u_1} {S : Type u_3} {R : Type u_4} [] [] [] [] [Algebra S R] (A : ι) :
⨆ (i : ι), A i = Subalgebra.toSubmodule ()

The supremum of submodules that form a graded monoid is a subalgebra, and equal to the range of DirectSum.coeAlgHom.

@[simp]
theorem DirectSum.coeAlgHom_of {ι : Type u_1} {S : Type u_3} {R : Type u_4} [] [] [] [] [Algebra S R] (A : ι) (i : ι) (x : { x // x A i }) :
↑() (↑(DirectSum.of (fun i => { x // x A i }) i) x) = x
theorem SetLike.homogeneous_zero_submodule {ι : Type u_1} {S : Type u_3} {R : Type u_4} [Zero ι] [] [] [Module S R] (A : ι) :
theorem SetLike.Homogeneous.smul {ι : Type u_1} {S : Type u_3} {R : Type u_4} [] [] [Algebra S R] {A : ι} {s : S} {r : R} (hr : ) :