mathlib documentation

algebra.direct_sum_graded

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:

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

the base ring A 0 with:

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

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 gmonoid and gcomm_monoid instances for:

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 #

graded ring, filtered ring, direct sum, add_submonoid

Typeclasses #

@[class]
structure direct_sum.ghas_one {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_zero ι] :
Type u_2
  • one : A 0

A graded version of has_one, which must be of grade 0.

Instances
@[class]
structure direct_sum.ghas_mul {ι : 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)

A graded version of has_mul that also subsumes non_unital_non_assoc_semiring by requiring the multiplication be an add_monoid_hom. Multiplication combines grades additively, like add_monoid_algebra.

Instances
def direct_sum.ghas_one.to_sigma_has_one {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} [has_zero ι] [direct_sum.ghas_one A] :
has_one (Σ (i : ι), A i)

direct_sum.ghas_one implies a has_one (Σ i, A i), although this is only used as an instance locally to define notation in direct_sum.gmonoid.

Equations
def direct_sum.ghas_mul.to_sigma_has_mul {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] :
has_mul (Σ (i : ι), A i)

direct_sum.ghas_mul implies a has_mul (Σ i, A i), although this is only used as an instance locally to define notation in direct_sum.gmonoid.

Equations
@[class]
structure direct_sum.gmonoid {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] :
Type (max u_1 u_2)
  • to_ghas_mul : direct_sum.ghas_mul A
  • to_ghas_one : direct_sum.ghas_one A
  • one_mul : ∀ (a : Σ (i : ι), A i), 1 * a = a
  • mul_one : ∀ (a : Σ (i : ι), A i), a * 1 = a
  • mul_assoc : ∀ (a b c_1 : Σ (i : ι), A i), (a * b) * c_1 = a * b * c_1

A graded version of monoid.

Instances
@[class]
structure direct_sum.gcomm_monoid {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_comm_monoid ι] [Π (i : ι), add_comm_monoid (A i)] :
Type (max u_1 u_2)

A graded version of comm_monoid.

Instances

Shorthands for creating the above typeclasses #

From add_submonoids #

@[simp]
theorem direct_sum.ghas_one.of_add_submonoids_one {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [has_zero ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) :
def direct_sum.ghas_one.of_add_submonoids {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [has_zero ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) :
direct_sum.ghas_one (λ (i : ι), (carriers i))

Build a ghas_one instance for a collection of add_submonoids.

Equations
def direct_sum.ghas_mul.of_add_submonoids {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [has_add ι] (carriers : ι → add_submonoid R) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.ghas_mul (λ (i : ι), (carriers i))

Build a ghas_mul instance for a collection of add_submonoids.

Equations
@[simp]
theorem direct_sum.ghas_mul.of_add_submonoids_mul {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [has_add ι] (carriers : ι → add_submonoid R) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) {i j : ι} (a : (carriers i)) (b : (carriers j)) :
def direct_sum.gmonoid.of_add_submonoids {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [add_monoid ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.gmonoid (λ (i : ι), (carriers i))

Build a gmonoid instance for a collection of add_submonoids.

Equations
@[simp]
theorem direct_sum.gmonoid.of_add_submonoids_to_ghas_mul {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [add_monoid ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
@[simp]
theorem direct_sum.gmonoid.of_add_submonoids_to_ghas_one {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [semiring R] [add_monoid ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
@[simp]
theorem direct_sum.gcomm_monoid.of_add_submonoids_to_gmonoid {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [comm_semiring R] [add_comm_monoid ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
def direct_sum.gcomm_monoid.of_add_submonoids {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [comm_semiring R] [add_comm_monoid ι] (carriers : ι → add_submonoid R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.gcomm_monoid (λ (i : ι), (carriers i))

Build a gcomm_monoid instance for a collection of add_submonoids.

Equations

From add_subgroups #

@[simp]
theorem direct_sum.ghas_one.of_add_subgroups_one {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [has_zero ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) :
def direct_sum.ghas_one.of_add_subgroups {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [has_zero ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) :
direct_sum.ghas_one (λ (i : ι), (carriers i))

Build a ghas_one instance for a collection of add_subgroups.

Equations
def direct_sum.ghas_mul.of_add_subgroups {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [has_add ι] (carriers : ι → add_subgroup R) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.ghas_mul (λ (i : ι), (carriers i))

Build a ghas_mul instance for a collection of add_subgroups.

Equations
@[simp]
theorem direct_sum.ghas_mul.of_add_subgroups_mul {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [has_add ι] (carriers : ι → add_subgroup R) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) {i j : ι} (a : (carriers i)) (b : (carriers j)) :
@[simp]
theorem direct_sum.gmonoid.of_add_subgroups_to_ghas_mul {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [add_monoid ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
def direct_sum.gmonoid.of_add_subgroups {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [add_monoid ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.gmonoid (λ (i : ι), (carriers i))

Build a gmonoid instance for a collection of add_subgroups.

Equations
@[simp]
theorem direct_sum.gmonoid.of_add_subgroups_to_ghas_one {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [ring R] [add_monoid ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
@[simp]
theorem direct_sum.gcomm_monoid.of_add_subgroups_to_gmonoid {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [comm_ring R] [add_comm_monoid ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
def direct_sum.gcomm_monoid.of_add_subgroups {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [comm_ring R] [add_comm_monoid ι] (carriers : ι → add_subgroup R) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.gcomm_monoid (λ (i : ι), (carriers i))

Build a gcomm_monoid instance for a collection of add_subgroups.

Equations

From submoduless #

def direct_sum.ghas_one.of_submodules {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_zero ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) :
direct_sum.ghas_one (λ (i : ι), (carriers i))

Build a ghas_one instance for a collection of submodules.

Equations
@[simp]
theorem direct_sum.ghas_one.of_submodules_one {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_zero ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) :
def direct_sum.ghas_mul.of_submodules {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_add ι] (carriers : ι → submodule R A) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.ghas_mul (λ (i : ι), (carriers i))

Build a ghas_mul instance for a collection of submodules.

Equations
@[simp]
theorem direct_sum.ghas_mul.of_submodules_mul {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_add ι] (carriers : ι → submodule R A) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) {i j : ι} (a : (carriers i)) (b : (carriers j)) :
@[simp]
theorem direct_sum.gmonoid.of_submodules_to_ghas_one {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [add_monoid ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
@[simp]
theorem direct_sum.gmonoid.of_submodules_to_ghas_mul {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [add_monoid ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
def direct_sum.gmonoid.of_submodules {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [add_monoid ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.gmonoid (λ (i : ι), (carriers i))

Build a gmonoid instance for a collection of submoduless.

Equations
def direct_sum.gcomm_monoid.of_submodules {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :
direct_sum.gcomm_monoid (λ (i : ι), (carriers i))

Build a gcomm_monoid instance for a collection of submoduless.

Equations
@[simp]
theorem direct_sum.gcomm_monoid.of_submodules_to_gmonoid {ι : Type u_1} [decidable_eq ι] {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_semiring A] [algebra R A] [add_comm_monoid ι] (carriers : ι → submodule R A) (one_mem : 1 carriers 0) (mul_mem : ∀ ⦃i j : ι⦄ (gi : (carriers i)) (gj : (carriers j)), (gi) * gj carriers (i + j)) :

Instances for ⨁ i, A i #

@[instance]
def direct_sum.has_one {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_zero ι] [direct_sum.ghas_one A] [Π (i : ι), add_comm_monoid (A i)] :
has_one (⨁ (i : ι), A i)
Equations
def direct_sum.mul_hom {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] :
(⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i

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

Equations
@[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)] [direct_sum.ghas_mul A] :
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)] [direct_sum.ghas_mul A] {i j : ι} (a : A i) (b : A j) :
((direct_sum.mul_hom A) ((direct_sum.of (λ {i : ι}, A i) i) a)) ((direct_sum.of (λ {j : ι}, A j) j) b) = (direct_sum.of A (i + j)) ((direct_sum.ghas_mul.mul a) b)
theorem direct_sum.of_mul_of {ι : Type u_1} [decidable_eq ι] {A : ι → Type u_2} [has_add ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] {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 A (i + j)) ((direct_sum.ghas_mul.mul a) b)
@[instance]
def direct_sum.semiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gmonoid A] :
semiring (⨁ (i : ι), A i)

The semiring structure derived from gmonoid A.

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

The comm_semiring structure derived from gcomm_monoid A.

Equations
@[instance]
def direct_sum.ring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_group (A i)] [add_comm_monoid ι] [direct_sum.gmonoid A] :
ring (⨁ (i : ι), A i)

The ring derived from gmonoid A.

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

The comm_ring derived from gcomm_monoid 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.

@[nolint, instance]
def direct_sum.grade_zero.has_one {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_zero ι] [direct_sum.ghas_one A] [Π (i : ι), add_comm_monoid (A i)] :
has_one (A 0)

1 : A 0 is the value provided in direct_sum.ghas_one.one.

Equations
@[simp]
theorem direct_sum.of_zero_one {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [has_zero ι] [direct_sum.ghas_one A] [Π (i : ι), add_comm_monoid (A i)] :
@[instance]
def direct_sum.grade_zero.has_scalar {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] (i : ι) :
has_scalar (A 0) (A i)

(•) : A 0 → A i → A i is the value provided in direct_sum.ghas_mul.mul, composed with an eq.rec to turn A (0 + i) into A i.

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

(*) : A 0 → A 0 → A 0 is the value provided in direct_sum.ghas_mul.mul, composed with an eq.rec to turn A (0 + 0) into A 0.

Equations
@[simp]
theorem direct_sum.grade_zero.smul_eq_mul {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] (a b : A 0) :
a b = a * b
@[simp]
theorem direct_sum.of_zero_smul {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] {i : ι} (a : A 0) (b : A i) :
@[simp]
theorem direct_sum.of_zero_mul {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] (a b : A 0) :
(direct_sum.of A 0) (a * b) = ((direct_sum.of A 0) a) * (direct_sum.of A 0) b
@[instance]
def direct_sum.grade_zero.smul_with_zero {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [direct_sum.ghas_mul A] (i : ι) :
smul_with_zero (A 0) (A i)
Equations
@[instance]
def direct_sum.grade_zero.semiring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_monoid (A i)] [add_monoid ι] [direct_sum.gmonoid A] :
semiring (A 0)

The semiring structure derived from gmonoid 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 ι] [direct_sum.gmonoid A] :
A 0 →+* ⨁ (i : ι), A i

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

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

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

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

The comm_semiring structure derived from gcomm_monoid A.

Equations
@[instance]
def direct_sum.grade_zero.ring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_group (A i)] [add_comm_monoid ι] [direct_sum.gmonoid A] :
ring (A 0)

The ring derived from gmonoid A.

Equations
@[instance]
def direct_sum.grade_zero.comm_ring {ι : Type u_1} [decidable_eq ι] (A : ι → Type u_2) [Π (i : ι), add_comm_group (A i)] [add_comm_monoid ι] [direct_sum.gcomm_monoid A] :
comm_ring (A 0)

The comm_ring derived from gcomm_monoid 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 ι] [direct_sum.gmonoid A] [semiring R] (F G : (⨁ (i : ι), A i) →+* R) (h : ∀ (i : ι), F.comp (direct_sum.of (λ (i : ι), A i) i) = G.comp (direct_sum.of A i)) :
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].

@[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 ι] [direct_sum.gmonoid A] [semiring R] (f : Π (i : ι), A i →+ R) (hone : (f 0) direct_sum.ghas_one.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) ((direct_sum.ghas_mul.mul ai) aj) = ((f i) ai) * (f j) aj) (ᾰ : ⨁ (i : ι), (λ (i : ι), A i) i) :
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 ι] [direct_sum.gmonoid A] [semiring R] (f : Π (i : ι), A i →+ R) (hone : (f 0) direct_sum.ghas_one.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) ((direct_sum.ghas_mul.mul ai) 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 [gmonoid A] structure originates from direct_sum.gmonoid.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 ι] [direct_sum.gmonoid A] [semiring R] (f : Π (i : ι), A i →+ R) (hone : (f 0) direct_sum.ghas_one.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) ((direct_sum.ghas_mul.mul ai) aj) = ((f i) ai) * (f j) aj) (i : ι) (x : A i) :
(direct_sum.to_semiring f 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 ι] [direct_sum.gmonoid A] [semiring R] (f : Π (i : ι), A i →+ R) (hone : (f 0) direct_sum.ghas_one.one = 1) (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) ((direct_sum.ghas_mul.mul ai) aj) = ((f i) ai) * (f j) aj) :
@[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 ι] [direct_sum.gmonoid A] [semiring R] (f : {f // f direct_sum.ghas_one.one = 1 ∀ {i j : ι} (ai : A i) (aj : A j), f ((direct_sum.ghas_mul.mul ai) aj) = (f ai) * f aj}) :
@[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 ι] [direct_sum.gmonoid A] [semiring R] (F : (⨁ (i : ι), A i) →+* R) (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 ι] [direct_sum.gmonoid A] [semiring R] :
{f // f direct_sum.ghas_one.one = 1 ∀ {i j : ι} (ai : A i) (aj : A j), f ((direct_sum.ghas_mul.mul ai) 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 #

@[instance]
def semiring.direct_sum_gmonoid {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [add_monoid ι] [semiring R] :
direct_sum.gmonoid (λ (i : ι), R)

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

Equations
@[simp]
theorem semiring.direct_sum_mul {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [add_monoid ι] [semiring R] {i j : ι} (x y : R) :
@[instance]
def comm_semiring.direct_sum_gcomm_monoid {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [add_comm_monoid ι] [comm_semiring R] :
direct_sum.gcomm_monoid (λ (i : ι), R)

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

Equations
@[instance]
def submodule.nat_power_direct_sum_gmonoid {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] (S : submodule R A) :
direct_sum.gmonoid (λ (i : ), (S ^ i))

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

Equations
@[instance]
def submodule.nat_power_direct_sum_gcomm_monoid {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_semiring A] [algebra R A] (S : submodule R A) :
direct_sum.gcomm_monoid (λ (i : ), (S ^ i))

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

Equations