# Documentation

Mathlib.Algebra.DirectSum.Ring

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

This module provides a set of heterogeneous typeclasses for defining a multiplicative structure over ⨁ i, A i such that (*) : A i → A j → A (i + j); that is to say, A forms an additively-graded ring. The typeclasses are:

• DirectSum.GNonUnitalNonAssocSemiring A
• DirectSum.GSemiring A
• DirectSum.GRing A
• DirectSum.GCommSemiring A
• DirectSum.GCommRing A

Respectively, these imbue the external direct sum ⨁ i, A i with:

• DirectSum.nonUnitalNonAssocSemiring, DirectSum.nonUnitalNonAssocRing
• DirectSum.semiring
• DirectSum.ring
• DirectSum.commSemiring
• DirectSum.commRing

the base ring A 0 with:

• DirectSum.GradeZero.nonUnitalNonAssocSemiring, DirectSum.GradeZero.nonUnitalNonAssocRing
• DirectSum.GradeZero.semiring
• DirectSum.GradeZero.ring
• DirectSum.GradeZero.commSemiring
• DirectSum.GradeZero.commRing

and the ith grade A i with A 0-actions (•) defined as left-multiplication:

• DirectSum.GradeZero.smul (A 0), DirectSum.GradeZero.smulWithZero (A 0)
• DirectSum.GradeZero.module (A 0)
• (nothing)
• (nothing)
• (nothing)

Note that in the presence of these instances, ⨁ i, A i itself inherits an A 0-action.

DirectSum.ofZeroRingHom : A 0 →+* ⨁ i, A i provides DirectSum.of A 0 as a ring homomorphism.

DirectSum.toSemiring extends DirectSum.toAddMonoid to produce a RingHom.

## Direct sums of subobjects #

Additionally, this module provides helper functions to construct GSemiring and GCommSemiring instances for:

• A : ι → Submonoid S: DirectSum.GSemiring.ofAddSubmonoids, DirectSum.GCommSemiring.ofAddSubmonoids.
• A : ι → Subgroup S: DirectSum.GSemiring.ofAddSubgroups, DirectSum.GCommSemiring.ofAddSubgroups.
• A : ι → Submodule S: DirectSum.GSemiring.ofSubmodules, DirectSum.GCommSemiring.ofSubmodules.

If CompleteLattice.independent (Set.range A), these provide a gradation of ⨆ i, A i, and the mapping ⨁ i, A i →+ ⨆ i, A i can be obtained as DirectSum.toMonoid (fun i ↦ AddSubmonoid.inclusion \$ le_iSup A i).

## tags #

### Typeclasses #

class DirectSum.GNonUnitalNonAssocSemiring {ι : Type u_1} (A : ιType u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] extends :
Type (max u_1 u_2)
• mul : {i j : ι} → A iA jA (i + j)
• mul_zero : ∀ {i j : ι} (a : A i),

Multiplication from the right with any graded component's zero vanishes.

• zero_mul : ∀ {i j : ι} (b : A j),

Multiplication from the left with any graded component's zero vanishes.

• mul_add : ∀ {i j : ι} (a : A i) (b c : A j), GradedMonoid.GMul.mul a (b + c) =

Multiplication from the right between graded components distributes with respect to addition.

• add_mul : ∀ {i j : ι} (a b : A i) (c : A j), GradedMonoid.GMul.mul (a + b) c =

Multiplication from the left between graded components distributes with respect to addition.

A graded version of NonUnitalNonAssocSemiring.

Instances
class DirectSum.GSemiring {ι : Type u_1} (A : ιType u_2) [] [(i : ι) → AddCommMonoid (A i)] extends , :
Type (max u_1 u_2)
• mul : {i j : ι} → A iA jA (i + j)
• mul_zero : ∀ {i j : ι} (a : A i),
• zero_mul : ∀ {i j : ι} (b : A j),
• mul_add : ∀ {i j : ι} (a : A i) (b c : A j), GradedMonoid.GMul.mul a (b + c) =
• add_mul : ∀ {i j : ι} (a b : A i) (c : A j), GradedMonoid.GMul.mul (a + b) c =
• one : A 0
• one_mul : ∀ (a : ), 1 * a = a

Multiplication by one on the left is the identity

• mul_one : ∀ (a : ), a * 1 = a

Multiplication by one on the right is the identity

• mul_assoc : ∀ (a b c : ), a * b * c = a * (b * c)

Multiplication is associative

• gnpow : (n : ) → {i : ι} → A iA (n i)

Optional field to allow definitional control of natural powers

• gnpow_zero' : ∀ (a : ), GradedMonoid.mk (0 a.fst) () = 1

The zeroth power will yield 1

• gnpow_succ' : ∀ (n : ) (a : ), GradedMonoid.mk ( a.fst) (DirectSum.GSemiring.gnpow () a.snd) = a * { fst := n a.fst, snd := }

Successor powers behave as expected

• natCast : A 0

The canonical map from ℕ to the zeroth component of a graded semiring.

• natCast_zero :

The canonical map from ℕ to a graded semiring respects zero.

• natCast_succ : ∀ (n : ), = + GradedMonoid.GOne.one

The canonical map from ℕ to a graded semiring respects successors.

A graded version of Semiring.

Instances
class DirectSum.GCommSemiring {ι : Type u_1} (A : ιType u_2) [] [(i : ι) → AddCommMonoid (A i)] extends :
Type (max u_1 u_2)
• mul : {i j : ι} → A iA jA (i + j)
• mul_zero : ∀ {i j : ι} (a : A i),
• zero_mul : ∀ {i j : ι} (b : A j),
• mul_add : ∀ {i j : ι} (a : A i) (b c : A j), GradedMonoid.GMul.mul a (b + c) =
• add_mul : ∀ {i j : ι} (a b : A i) (c : A j), GradedMonoid.GMul.mul (a + b) c =
• one : A 0
• one_mul : ∀ (a : ), 1 * a = a
• mul_one : ∀ (a : ), a * 1 = a
• mul_assoc : ∀ (a b c : ), a * b * c = a * (b * c)
• gnpow : (n : ) → {i : ι} → A iA (n i)
• gnpow_zero' : ∀ (a : ), GradedMonoid.mk (0 a.fst) () = 1
• gnpow_succ' : ∀ (n : ) (a : ), GradedMonoid.mk ( a.fst) (DirectSum.GSemiring.gnpow () a.snd) = a * { fst := n a.fst, snd := }
• natCast : A 0
• natCast_zero :
• natCast_succ : ∀ (n : ), = + GradedMonoid.GOne.one
• mul_comm : ∀ (a b : ), a * b = b * a

Multiplication is commutative

A graded version of CommSemiring.

Instances
class DirectSum.GRing {ι : Type u_1} (A : ιType u_2) [] [(i : ι) → AddCommGroup (A i)] extends :
Type (max u_1 u_2)
• mul : {i j : ι} → A iA jA (i + j)
• mul_zero : ∀ {i j : ι} (a : A i),
• zero_mul : ∀ {i j : ι} (b : A j),
• mul_add : ∀ {i j : ι} (a : A i) (b c : A j), GradedMonoid.GMul.mul a (b + c) =
• add_mul : ∀ {i j : ι} (a b : A i) (c : A j), GradedMonoid.GMul.mul (a + b) c =
• one : A 0
• one_mul : ∀ (a : ), 1 * a = a
• mul_one : ∀ (a : ), a * 1 = a
• mul_assoc : ∀ (a b c : ), a * b * c = a * (b * c)
• gnpow : (n : ) → {i : ι} → A iA (n i)
• gnpow_zero' : ∀ (a : ), GradedMonoid.mk (0 a.fst) () = 1
• gnpow_succ' : ∀ (n : ) (a : ), GradedMonoid.mk ( a.fst) (DirectSum.GSemiring.gnpow () a.snd) = a * { fst := n a.fst, snd := }
• natCast : A 0
• natCast_zero :
• natCast_succ : ∀ (n : ), = + GradedMonoid.GOne.one
• intCast : A 0

The canonical map from ℤ to the zeroth component of a graded ring.

• intCast_ofNat : ∀ (n : ),

The canonical map from ℤ to a graded ring extends the canonical map from ℕ to the underlying graded semiring.

• intCast_negSucc_ofNat : ∀ (n : ),

On negative integers, the canonical map from ℤ to a graded ring is the negative extension of the canonical map from ℕ to the underlying graded semiring.

A graded version of Ring.

Instances
class DirectSum.GCommRing {ι : Type u_1} (A : ιType u_2) [] [(i : ι) → AddCommGroup (A i)] extends :
Type (max u_1 u_2)
• mul : {i j : ι} → A iA jA (i + j)
• mul_zero : ∀ {i j : ι} (a : A i),
• zero_mul : ∀ {i j : ι} (b : A j),
• mul_add : ∀ {i j : ι} (a : A i) (b c : A j), GradedMonoid.GMul.mul a (b + c) =
• add_mul : ∀ {i j : ι} (a b : A i) (c : A j), GradedMonoid.GMul.mul (a + b) c =
• one : A 0
• one_mul : ∀ (a : ), 1 * a = a
• mul_one : ∀ (a : ), a * 1 = a
• mul_assoc : ∀ (a b c : ), a * b * c = a * (b * c)
• gnpow : (n : ) → {i : ι} → A iA (n i)
• gnpow_zero' : ∀ (a : ), GradedMonoid.mk (0 a.fst) () = 1
• gnpow_succ' : ∀ (n : ) (a : ), GradedMonoid.mk ( a.fst) (DirectSum.GSemiring.gnpow () a.snd) = a * { fst := n a.fst, snd := }
• natCast : A 0
• natCast_zero :
• natCast_succ : ∀ (n : ), = + GradedMonoid.GOne.one
• intCast : A 0
• intCast_ofNat : ∀ (n : ),
• intCast_negSucc_ofNat : ∀ (n : ),
• mul_comm : ∀ (a b : ), a * b = b * a

Multiplication is commutative

A graded version of CommRing.

Instances
theorem DirectSum.of_eq_of_gradedMonoid_eq {ι : Type u_1} [] {A : ιType u_2} [(i : ι) → AddCommMonoid (A i)] {i : ι} {j : ι} {a : A i} {b : A j} (h : = ) :
↑() a = ↑() b

### Instances for ⨁ i, A i#

instance DirectSum.instOneDirectSum {ι : Type u_1} [] (A : ιType u_2) [Zero ι] [(i : ι) → AddCommMonoid (A i)] :
One (⨁ (i : ι), A i)
@[simp]
theorem DirectSum.gMulHom_apply_apply {ι : Type u_1} (A : ιType u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] {i : ι} {j : ι} (a : A i) (b : A j) :
↑(↑() a) b =
def DirectSum.gMulHom {ι : Type u_1} (A : ιType u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] {i : ι} {j : ι} :
A i →+ A j →+ A (i + j)

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

Instances For
def DirectSum.mulHom {ι : Type u_1} [] (A : ιType u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] :
(⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i

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

Instances For
instance DirectSum.instNonUnitalNonAssocSemiringDirectSum {ι : Type u_1} [] (A : ιType u_2) [Add ι] [(i : ι) → AddCommMonoid (A i)] :
NonUnitalNonAssocSemiring (⨁ (i : ι), A i)
theorem DirectSum.mulHom_apply {ι : Type u_1} [] {A : ιType u_2} [Add ι] [(i : ι) → AddCommMonoid (A i)] (a : ⨁ (i : ι), A i) (b : ⨁ (i : ι), A i) :
↑(↑() a) b = a * b
theorem DirectSum.mulHom_of_of {ι : Type u_1} [] {A : ιType u_2} [Add ι] [(i : ι) → AddCommMonoid (A i)] {i : ι} {j : ι} (a : A i) (b : A j) :
↑(↑() (↑() a)) (↑() b) = ↑(DirectSum.of A (i + j)) ()
theorem DirectSum.of_mul_of {ι : Type u_1} [] {A : ιType u_2} [Add ι] [(i : ι) → AddCommMonoid (A i)] {i : ι} {j : ι} (a : A i) (b : A j) :
↑() a * ↑() b = ↑(DirectSum.of A (i + j)) ()
instance DirectSum.semiring {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] :
Semiring (⨁ (i : ι), A i)

The Semiring structure derived from GSemiring A.

theorem DirectSum.ofPow {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] {i : ι} (a : A i) (n : ) :
↑() a ^ n = ↑(DirectSum.of A (n i)) ()
theorem DirectSum.ofList_dProd {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] {α : Type u_3} (l : List α) (fι : αι) (fA : (a : α) → A ( a)) :
↑(DirectSum.of A ()) (List.dProd l fA) = List.prod (List.map (fun a => ↑(DirectSum.of A ( a)) (fA a)) l)
theorem DirectSum.list_prod_ofFn_of_eq_dProd {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] (n : ) (fι : Fin nι) (fA : (a : Fin n) → A ( a)) :
List.prod (List.ofFn fun a => ↑(DirectSum.of A ( a)) (fA a)) = ↑(DirectSum.of A ()) (List.dProd () fA)
theorem DirectSum.mul_eq_dfinsupp_sum {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] [(i : ι) → (x : A i) → Decidable (x 0)] (a : ⨁ (i : ι), A i) (a' : ⨁ (i : ι), A i) :
a * a' = DFinsupp.sum a fun i ai => DFinsupp.sum a' fun j aj => ↑(DirectSum.of A (i + j)) ()
theorem DirectSum.mul_eq_sum_support_ghas_mul {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] [(i : ι) → (x : A i) → Decidable (x 0)] (a : ⨁ (i : ι), A i) (a' : ⨁ (i : ι), A i) :
a * a' = Finset.sum () fun ij => ↑(DirectSum.of (fun i => (fun i => A i) i) (ij.fst + ij.snd)) (GradedMonoid.GMul.mul (a ij.fst) (a' ij.snd))

A heavily unfolded version of the definition of multiplication

instance DirectSum.commSemiring {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] :
CommSemiring (⨁ (i : ι), A i)

The CommSemiring structure derived from GCommSemiring A.

instance DirectSum.nonAssocRing {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [Add ι] :
NonUnitalNonAssocRing (⨁ (i : ι), A i)

The Ring derived from GSemiring A.

instance DirectSum.ring {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [] [] :
Ring (⨁ (i : ι), A i)

The Ring derived from GSemiring A.

instance DirectSum.commRing {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [] :
CommRing (⨁ (i : ι), A i)

The CommRing derived from GCommSemiring A.

### Instances for A 0#

The various G* instances are enough to promote the AddCommMonoid (A 0) structure to various types of multiplicative structure.

@[simp]
theorem DirectSum.of_zero_one {ι : Type u_1} [] (A : ιType u_2) [Zero ι] [(i : ι) → AddCommMonoid (A i)] :
↑() 1 = 1
@[simp]
theorem DirectSum.of_zero_smul {ι : Type u_1} [] (A : ιType u_2) [] [(i : ι) → AddCommMonoid (A i)] {i : ι} (a : A 0) (b : A i) :
↑() (a b) = ↑() a * ↑() b
@[simp]
theorem DirectSum.of_zero_mul {ι : Type u_1} [] (A : ιType u_2) [] [(i : ι) → AddCommMonoid (A i)] (a : A 0) (b : A 0) :
↑() (a * b) = ↑() a * ↑() b
instance DirectSum.GradeZero.nonUnitalNonAssocSemiring {ι : Type u_1} [] (A : ιType u_2) [] [(i : ι) → AddCommMonoid (A i)] :
instance DirectSum.GradeZero.smulWithZero {ι : Type u_1} [] (A : ιType u_2) [] [(i : ι) → AddCommMonoid (A i)] (i : ι) :
SMulWithZero (A 0) (A i)
@[simp]
theorem DirectSum.of_zero_pow {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] (a : A 0) (n : ) :
↑() (a ^ n) = ↑() a ^ n
instance DirectSum.instNatCastOfNatToOfNat0ToZero {ι : Type u_1} (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] :
NatCast (A 0)
@[simp]
theorem DirectSum.ofNatCast {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] (n : ) :
↑() n = n
instance DirectSum.GradeZero.semiring {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] :
Semiring (A 0)

The Semiring structure derived from GSemiring A.

def DirectSum.ofZeroRingHom {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] :
A 0 →+* ⨁ (i : ι), A i

of A 0 is a RingHom, using the DirectSum.GradeZero.semiring structure.

Instances For
instance DirectSum.GradeZero.module {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] {i : ι} :
Module (A 0) (A i)

Each grade A i derives an A 0-module structure from GSemiring A. Note that this results in an overall Module (A 0) (⨁ i, A i) structure via DirectSum.module.

instance DirectSum.GradeZero.commSemiring {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommMonoid (A i)] [] :

The CommSemiring structure derived from GCommSemiring A.

instance DirectSum.GradeZero.nonUnitalNonAssocRing {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [] :

The NonUnitalNonAssocRing derived from GNonUnitalNonAssocSemiring A.

instance DirectSum.instIntCastOfNatToOfNat0ToZero {ι : Type u_1} (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [] [] :
IntCast (A 0)
@[simp]
theorem DirectSum.ofIntCast {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [] [] (n : ) :
↑() n = n
instance DirectSum.GradeZero.ring {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [] [] :
Ring (A 0)

The Ring derived from GSemiring A.

instance DirectSum.GradeZero.commRing {ι : Type u_1} [] (A : ιType u_2) [(i : ι) → AddCommGroup (A i)] [] :
CommRing (A 0)

The CommRing derived from GCommSemiring A.

theorem DirectSum.ringHom_ext' {ι : Type u_1} [] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [] [] ⦃F : (⨁ (i : ι), A i) →+* R ⦃G : (⨁ (i : ι), A i) →+* R (h : ∀ (i : ι), AddMonoidHom.comp (F) () = AddMonoidHom.comp (G) ()) :
F = G

If two ring homomorphisms from ⨁ i, A i are equal on each of A i y, then they are equal.

See note [partially-applied ext lemmas].

theorem DirectSum.ringHom_ext {ι : Type u_1} [] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [] [] ⦃f : (⨁ (i : ι), A i) →+* R ⦃g : (⨁ (i : ι), A i) →+* R (h : ∀ (i : ι) (x : A i), f (↑() x) = g (↑() x)) :
f = g

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

@[simp]
theorem DirectSum.toSemiring_apply {ι : Type u_1} [] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [] [] (f : (i : ι) → A i →+ R) (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) (a : ⨁ (i : ι), A i) :
↑(DirectSum.toSemiring f hone hmul) a = ↑() a
def DirectSum.toSemiring {ι : Type u_1} [] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [] [] (f : (i : ι) → A i →+ R) (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) :
(⨁ (i : ι), A i) →+* R

A family of AddMonoidHoms preserving DirectSum.One.one and DirectSum.Mul.mul describes a RingHoms on ⨁ i, A i. This is a stronger version of DirectSum.toMonoid.

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

Instances For
theorem DirectSum.toSemiring_of {ι : Type u_1} [] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [] [] (f : (i : ι) → A i →+ R) (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) (i : ι) (x : A i) :
↑(DirectSum.toSemiring f hone hmul) (↑() x) = ↑(f i) x
@[simp]
theorem DirectSum.toSemiring_coe_addMonoidHom {ι : Type u_1} [] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [] [] (f : (i : ι) → A i →+ R) (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) :
↑(DirectSum.toSemiring f hone hmul) =
@[simp]
theorem DirectSum.liftRingHom_apply {ι : Type u_1} [] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [] [] (f : { f // f GradedMonoid.GOne.one = 1 ∀ {i j : ι} (ai : A i) (aj : A j), f () = f ai * f aj }) :
DirectSum.liftRingHom f = DirectSum.toSemiring (fun x => f) (_ : f GradedMonoid.GOne.one = 1) (_ : ∀ {i j : ι} (ai : A i) (aj : A j), f () = f ai * f aj)
@[simp]
theorem DirectSum.liftRingHom_symm_apply_coe {ι : Type u_1} [] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [] [] (F : (⨁ (i : ι), A i) →+* R) {i : ι} :
↑(DirectSum.liftRingHom.symm F) = AddMonoidHom.comp (F) ()
def DirectSum.liftRingHom {ι : Type u_1} [] {A : ιType u_2} {R : Type u_3} [(i : ι) → AddCommMonoid (A i)] [] [] :
{ f // f GradedMonoid.GOne.one = 1 ∀ {i j : ι} (ai : A i) (aj : A j), f () = f ai * f aj } ((⨁ (i : ι), A i) →+* R)

Families of AddMonoidHoms preserving DirectSum.One.one and DirectSum.Mul.mul are isomorphic to RingHoms on ⨁ i, A i. This is a stronger version of DFinsupp.liftAddHom.

Instances For

### Concrete instances #

A direct sum of copies of a Semiring inherits the multiplication structure.

instance Semiring.directSumGSemiring (ι : Type u_1) {R : Type u_2} [] [] :

A direct sum of copies of a Semiring inherits the multiplication structure.

instance CommSemiring.directSumGCommSemiring (ι : Type u_1) {R : Type u_2} [] [] :

A direct sum of copies of a CommSemiring inherits the commutative multiplication structure.