# mathlib3documentation

algebra.direct_sum.ring

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

• direct_sum.gnon_unital_non_assoc_semiring A
• direct_sum.gsemiring A
• direct_sum.gring A
• direct_sum.gcomm_semiring A
• direct_sum.gcomm_ring A

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

• direct_sum.non_unital_non_assoc_semiring, direct_sum.non_unital_non_assoc_ring
• direct_sum.semiring
• direct_sum.ring
• direct_sum.comm_semiring
• direct_sum.comm_ring

the base ring A 0 with:

• direct_sum.grade_zero.non_unital_non_assoc_semiring, direct_sum.grade_zero.non_unital_non_assoc_ring
• direct_sum.grade_zero.semiring
• direct_sum.grade_zero.ring
• direct_sum.grade_zero.comm_semiring
• direct_sum.grade_zero.comm_ring

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

• direct_sum.grade_zero.has_smul (A 0), direct_sum.grade_zero.smul_with_zero (A 0)
• direct_sum.grade_zero.module (A 0)
• (nothing)
• (nothing)
• (nothing)

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

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

direct_sum.to_semiring extends direct_sum.to_add_monoid to produce a ring_hom.

## Direct sums of subobjects #

Additionally, this module provides helper functions to construct gsemiring and gcomm_semiring instances for:

• A : ι → submonoid S: direct_sum.gsemiring.of_add_submonoids, direct_sum.gcomm_semiring.of_add_submonoids.
• A : ι → subgroup S: direct_sum.gsemiring.of_add_subgroups, direct_sum.gcomm_semiring.of_add_subgroups.
• A : ι → submodule S: direct_sum.gsemiring.of_submodules, direct_sum.gcomm_semiring.of_submodules.

If complete_lattice.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 direct_sum.to_monoid (λ i, add_submonoid.inclusion \$ le_supr A i).

## tags #

### Typeclasses #

@[instance]
def direct_sum.gnon_unital_non_assoc_semiring.to_ghas_mul {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)]  :
@[class]
structure direct_sum.gnon_unital_non_assoc_semiring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] :
Type (max u_1 u_2)
• mul : Π {i j : ι}, A i A j A (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),
• add_mul : {i j : ι} (a b : A i) (c : A j),

A graded version of non_unital_non_assoc_semiring.

Instances of this typeclass
Instances of other typeclasses for direct_sum.gnon_unital_non_assoc_semiring
• direct_sum.gnon_unital_non_assoc_semiring.has_sizeof_inst
@[class]
structure direct_sum.gsemiring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] :
Type (max u_1 u_2)
• mul : Π {i j : ι}, A i A j A (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), (b + c) =
• add_mul : {i j : ι} (a b : A i) (c : A j), 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 i A (n i)
• gnpow_zero' : ( (a : , graded_monoid.mk (0 a.fst) = 1) . "apply_gnpow_rec_zero_tac"
• gnpow_succ' : ( (n : ) (a : , graded_monoid.mk (n.succ a.fst) = a * n a.fst, ⟩) . "apply_gnpow_rec_succ_tac"
• nat_cast : A 0
• nat_cast_zero :
• nat_cast_succ :

A graded version of semiring.

Instances of this typeclass
Instances of other typeclasses for direct_sum.gsemiring
• direct_sum.gsemiring.has_sizeof_inst
@[instance]
@[instance]
def direct_sum.gsemiring.to_gmonoid {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [self : direct_sum.gsemiring A] :
@[instance]
def direct_sum.gcomm_semiring.to_gsemiring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [self : direct_sum.gcomm_semiring A] :
@[instance]
def direct_sum.gcomm_semiring.to_gcomm_monoid {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [self : direct_sum.gcomm_semiring A] :
@[class]
structure direct_sum.gcomm_semiring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] :
Type (max u_1 u_2)
• mul : Π {i j : ι}, A i A j A (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),
• add_mul : {i j : ι} (a b : A i) (c : A j),
• 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 i A (n i)
• gnpow_zero' : ( (a : , graded_monoid.mk (0 a.fst) = 1) . "apply_gnpow_rec_zero_tac"
• gnpow_succ' : ( (n : ) (a : , graded_monoid.mk (n.succ a.fst) = a * n a.fst, ⟩) . "apply_gnpow_rec_succ_tac"
• nat_cast : A 0
• nat_cast_zero :
• nat_cast_succ :
• mul_comm : (a b : , a * b = b * a

A graded version of comm_semiring.

Instances of this typeclass
Instances of other typeclasses for direct_sum.gcomm_semiring
• direct_sum.gcomm_semiring.has_sizeof_inst
@[instance]
def direct_sum.gring.to_gsemiring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [add_monoid ι] [Π (i : ι), add_comm_group (A i)] [self : direct_sum.gring A] :
@[class]
structure direct_sum.gring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [add_monoid ι] [Π (i : ι), add_comm_group (A i)] :
Type (max u_1 u_2)

A graded version of ring.

Instances of this typeclass
Instances of other typeclasses for direct_sum.gring
• direct_sum.gring.has_sizeof_inst
@[instance]
def direct_sum.gcomm_ring.to_gring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_group (A i)] [self : direct_sum.gcomm_ring A] :
@[instance]
def direct_sum.gcomm_ring.to_gcomm_semiring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_group (A i)] [self : direct_sum.gcomm_ring A] :
@[class]
structure direct_sum.gcomm_ring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_group (A i)] :
Type (max u_1 u_2)
• mul : Π {i j : ι}, A i A j A (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),
• add_mul : {i j : ι} (a b : A i) (c : A j),
• 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 i A (n i)
• gnpow_zero' : ( (a : , graded_monoid.mk (0 a.fst) = 1) . "apply_gnpow_rec_zero_tac"
• gnpow_succ' : ( (n : ) (a : , graded_monoid.mk (n.succ a.fst) = a * n a.fst, ⟩) . "apply_gnpow_rec_succ_tac"
• nat_cast : A 0
• nat_cast_zero :
• nat_cast_succ :
• int_cast : A 0
• int_cast_of_nat :
• int_cast_neg_succ_of_nat : (n : ),
• mul_comm : (a b : , a * b = b * a

A graded version of comm_ring.

Instances of this typeclass
Instances of other typeclasses for direct_sum.gcomm_ring
• direct_sum.gcomm_ring.has_sizeof_inst
theorem direct_sum.of_eq_of_graded_monoid_eq {ι : Type u_1} [decidable_eq ι] {A : ι Type u_2} [Π (i : ι), add_comm_monoid (A i)] {i j : ι} {a : A i} {b : A j} (h : = ) :
i) a = j) b

### Instances for ⨁ i, A i#

@[protected, instance]
def direct_sum.has_one {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [has_zero ι] [Π (i : ι), add_comm_monoid (A i)] :
has_one (λ (i : ι), A i))
Equations
@[simp]
theorem direct_sum.gmul_hom_apply_apply {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] {i j : ι} (a : A i) (b : A j) :
( a) b =
def direct_sum.gmul_hom {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] {i j : ι} :
A i →+ A j →+ A (i + j)

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

Equations
def direct_sum.mul_hom {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)]  :
(λ (i : ι), A i) →+ (λ (i : ι), A i) →+ (λ (i : ι), A i)

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

Equations
@[protected, instance]
def direct_sum.non_unital_non_assoc_semiring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)]  :
non_unital_non_assoc_semiring (λ (i : ι), A i))
Equations
theorem direct_sum.mul_hom_of_of {ι : Type u_1} [decidable_eq ι] {A : ι Type u_2} [has_add ι] [Π (i : ι), add_comm_monoid (A i)] {i j : ι} (a : A i) (b : A j) :
( ((direct_sum.of (λ {i : ι}, A i) i) a)) ((direct_sum.of (λ {j : ι}, A j) j) b) = (direct_sum.of (λ {i : ι}, A i) (i + j))
theorem direct_sum.of_mul_of {ι : Type u_1} [decidable_eq ι] {A : ι Type u_2} [has_add ι] [Π (i : ι), add_comm_monoid (A i)] {i j : ι} (a : A i) (b : A j) :
(direct_sum.of (λ {i : ι}, A i) i) a * (direct_sum.of (λ {j : ι}, A j) j) b = (direct_sum.of (λ {i : ι}, A i) (i + j))
@[protected, instance]
def direct_sum.semiring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι]  :
semiring (λ (i : ι), A i))

The semiring structure derived from gsemiring A.

Equations
theorem direct_sum.of_pow {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] {i : ι} (a : A i) (n : ) :
(direct_sum.of (λ {i : ι}, A i) i) a ^ n = (direct_sum.of (λ {i : ι}, A i) (n i))
theorem direct_sum.of_list_dprod {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] {α : Type u_3} (l : list α) (fι : α ι) (fA : Π (a : α), A (fι a)) :
(l.dprod_index fι)) (l.dprod fA) = (list.map (λ (a : α), (fι a)) (fA a)) l).prod
theorem direct_sum.list_prod_of_fn_of_eq_dprod {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] (n : ) (fι : fin n ι) (fA : Π (a : fin n), A (fι a)) :
(list.of_fn (λ (a : fin n), (fι a)) (fA a))).prod = fι)) ((list.fin_range n).dprod fA)
theorem direct_sum.mul_eq_dfinsupp_sum {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [Π (i : ι) (x : A i), decidable (x 0)] (a a' : (λ (i : ι), A i)) :
a * a' = (λ (i : ι) (ai : (λ (i : ι), A i) i), (λ (j : ι) (aj : (λ (i : ι), A i) j), (direct_sum.of (λ (i : ι), A i) (i + j)) aj)))
theorem direct_sum.mul_eq_sum_support_ghas_mul {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [Π (i : ι) (x : A i), decidable (x 0)] (a a' : (λ (i : ι), A i)) :
a * a' = .sum (λ (ij : ι × ι), (ij.fst + ij.snd)) (graded_monoid.ghas_mul.mul (a ij.fst) (a' ij.snd)))

A heavily unfolded version of the definition of multiplication

@[protected, instance]
def direct_sum.comm_semiring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)]  :
comm_semiring (λ (i : ι), A i))

The comm_semiring structure derived from gcomm_semiring A.

Equations
@[protected, instance]
def direct_sum.non_assoc_ring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_group (A i)] [has_add ι]  :
non_unital_non_assoc_ring (λ (i : ι), A i))

The ring derived from gsemiring A.

Equations
@[protected, instance]
def direct_sum.ring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_group (A i)] [add_monoid ι]  :
ring (λ (i : ι), A i))

The ring derived from gsemiring A.

Equations
@[protected, instance]
def direct_sum.comm_ring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_group (A i)]  :
comm_ring (λ (i : ι), A i))

The comm_ring derived from gcomm_semiring A.

Equations

### Instances for A 0#

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

@[simp]
theorem direct_sum.of_zero_one {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [has_zero ι] [Π (i : ι), add_comm_monoid (A i)] :
0) 1 = 1
@[simp]
theorem direct_sum.of_zero_smul {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] {i : ι} (a : A 0) (b : A i) :
i) (a b) = 0) a * i) b
@[simp]
theorem direct_sum.of_zero_mul {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] (a b : A 0) :
0) (a * b) = 0) a * 0) b
@[protected, instance]
def direct_sum.grade_zero.non_unital_non_assoc_semiring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)]  :
Equations
@[protected, instance]
def direct_sum.grade_zero.smul_with_zero {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] (i : ι) :
smul_with_zero (A 0) (A i)
Equations
@[simp]
theorem direct_sum.of_zero_pow {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] (a : A 0) (n : ) :
0) (a ^ n) = 0) a ^ n
@[protected, instance]
def direct_sum.has_nat_cast {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι]  :
Equations
@[simp]
theorem direct_sum.of_nat_cast {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] (n : ) :
0) n = n
@[protected, instance]
def direct_sum.grade_zero.semiring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι]  :
semiring (A 0)

The semiring structure derived from gsemiring A.

Equations
• = _ _ _ _ _ _
def direct_sum.of_zero_ring_hom {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι]  :
A 0 →+* (λ (i : ι), A i)

of A 0 is a ring_hom, using the direct_sum.grade_zero.semiring structure.

Equations
@[protected, instance]
def direct_sum.grade_zero.module {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] {i : ι} :
module (A 0) (A i)

Each grade A i derives a A 0-module structure from gsemiring A. Note that this results in an overall module (A 0) (⨁ i, A i) structure via direct_sum.module.

Equations
@[protected, instance]
def direct_sum.grade_zero.comm_semiring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_monoid (A i)]  :

The comm_semiring structure derived from gcomm_semiring A.

Equations
• = _ _ _ _ _ _
@[protected, instance]
def direct_sum.grade_zero.non_unital_non_assoc_ring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_group (A i)]  :

The non_unital_non_assoc_ring derived from gnon_unital_non_assoc_semiring A.

Equations
@[protected, instance]
def direct_sum.has_int_cast {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_group (A i)] [add_monoid ι]  :
Equations
@[simp]
theorem direct_sum.of_int_cast {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_group (A i)] [add_monoid ι] (n : ) :
0) n = n
@[protected, instance]
def direct_sum.grade_zero.ring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_group (A i)] [add_monoid ι]  :
ring (A 0)

The ring derived from gsemiring A.

Equations
• = _ _ _ _ _ _ _ _ _ _ _
@[protected, instance]
def direct_sum.grade_zero.comm_ring {ι : Type u_1} [decidable_eq ι] (A : ι Type u_2) [Π (i : ι), add_comm_group (A i)]  :
comm_ring (A 0)

The comm_ring derived from gcomm_semiring A.

Equations
• = _ _ _ _ _ _ _ _ _ _
@[ext]
theorem direct_sum.ring_hom_ext' {ι : Type u_1} [decidable_eq ι] {A : ι Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [semiring R] ⦃F G : (λ (i : ι), A i) →+* R⦄ (h : (i : ι), F.comp i) = G.comp i)) :
F = G

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

theorem direct_sum.ring_hom_ext {ι : Type u_1} [decidable_eq ι] {A : ι Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [semiring R] ⦃f g : (λ (i : ι), A i) →+* R⦄ (h : (i : ι) (x : A i), f ( i) x) = g ( i) x)) :
f = g

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

@[simp]
theorem direct_sum.to_semiring_apply {ι : Type u_1} [decidable_eq ι] {A : ι Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [semiring R] (f : Π (i : ι), A i →+ R) (hone : = 1) (hmul : {i j : ι} (ai : A i) (aj : A j), (f (i + j)) aj) = (f i) ai * (f j) aj) (ᾰ : (λ (i : ι), (λ (i : ι), A i) i)) :
hone hmul) =
def direct_sum.to_semiring {ι : Type u_1} [decidable_eq ι] {A : ι Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [semiring R] (f : Π (i : ι), A i →+ R) (hone : = 1) (hmul : {i j : ι} (ai : A i) (aj : A j), (f (i + j)) aj) = (f i) ai * (f j) aj) :
(λ (i : ι), A i) →+* R

A family of add_monoid_homs preserving direct_sum.ghas_one.one and direct_sum.ghas_mul.mul describes a ring_homs on ⨁ i, A i. This is a stronger version of direct_sum.to_monoid.

Of particular interest is the case when A i are bundled subojects, f is the family of coercions such as add_submonoid.subtype (A i), and the [gsemiring A] structure originates from direct_sum.gsemiring.of_add_submonoids, in which case the proofs about ghas_one and ghas_mul can be discharged by rfl.

Equations
@[simp]
theorem direct_sum.to_semiring_of {ι : Type u_1} [decidable_eq ι] {A : ι Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [semiring R] (f : Π (i : ι), A i →+ R) (hone : = 1) (hmul : {i j : ι} (ai : A i) (aj : A j), (f (i + j)) aj) = (f i) ai * (f j) aj) (i : ι) (x : A i) :
hone hmul) ((direct_sum.of (λ (i : ι), A i) i) x) = (f i) x
@[simp]
theorem direct_sum.to_semiring_coe_add_monoid_hom {ι : Type u_1} [decidable_eq ι] {A : ι Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [semiring R] (f : Π (i : ι), A i →+ R) (hone : = 1) (hmul : {i j : ι} (ai : A i) (aj : A j), (f (i + j)) aj) = (f i) ai * (f j) aj) :
hone hmul) =
@[simp]
theorem direct_sum.lift_ring_hom_apply {ι : Type u_1} [decidable_eq ι] {A : ι Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [semiring R] (f : {f // {i j : ι} (ai : A i) (aj : A j), f aj) = f ai * f aj}) :
= direct_sum.to_semiring (λ (_x : ι), f.val) _ _
@[simp]
theorem direct_sum.lift_ring_hom_symm_apply_coe {ι : Type u_1} [decidable_eq ι] {A : ι Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [semiring R] (F : (λ (i : ι), A i) →+* R) (i : ι) :
= F.comp i)
def direct_sum.lift_ring_hom {ι : Type u_1} [decidable_eq ι] {A : ι Type u_2} {R : Type u_3} [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [semiring R] :
{f // {i j : ι} (ai : A i) (aj : A j), f aj) = f ai * f aj} (λ (i : ι), A i) →+* R)

Families of add_monoid_homs preserving direct_sum.ghas_one.one and direct_sum.ghas_mul.mul are isomorphic to ring_homs on ⨁ i, A i. This is a stronger version of dfinsupp.lift_add_hom.

Equations

### Concrete instances #

@[protected, instance]

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

Equations
@[protected, instance]
def semiring.direct_sum_gsemiring (ι : Type u_1) [decidable_eq ι] {R : Type u_2} [add_monoid ι] [semiring R] :
direct_sum.gsemiring (λ (i : ι), R)

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

Equations
@[protected, instance]
def comm_semiring.direct_sum_gcomm_semiring (ι : Type u_1) [decidable_eq ι] {R : Type u_2}  :
direct_sum.gcomm_semiring (λ (i : ι), R)

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

Equations