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:
direct_sum.has_onedirect_sum.mul_zero_class,direct_sum.distribdirect_sum.semiring,direct_sum.ringdirect_sum.comm_semiring,direct_sum.comm_ring
the base ring A 0 with:
direct_sum.grade_zero.has_onedirect_sum.grade_zero.mul_zero_class,direct_sum.grade_zero.distribdirect_sum.grade_zero.semiring,direct_sum.grade_zero.ringdirect_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:
- (nothing)
direct_sum.grade_zero.has_scalar (A 0),direct_sum.grade_zero.smul_with_zero (A 0)direct_sum.grade_zero.module (A 0)- (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 gmonoid and gcomm_monoid
instances for:
A : ι → submonoid S:direct_sum.ghas_one.of_add_submonoids,direct_sum.ghas_mul.of_add_submonoids,direct_sum.gmonoid.of_add_submonoids,direct_sum.gcomm_monoid.of_add_submonoids.A : ι → subgroup S:direct_sum.ghas_one.of_add_subgroups,direct_sum.ghas_mul.of_add_subgroups,direct_sum.gmonoid.of_add_subgroups,direct_sum.gcomm_monoid.of_add_subgroups.A : ι → submodule S:direct_sum.ghas_one.of_submodules,direct_sum.ghas_mul.of_submodules,direct_sum.gmonoid.of_submodules,direct_sum.gcomm_monoid.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 #
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)
A graded version of has_mul that also subsumes distrib and mul_zero_class 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
- direct_sum.ghas_one.to_sigma_has_one = {one := ⟨0, direct_sum.ghas_one.one _inst_3⟩}
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.
@[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.
@[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)
- to_gmonoid : direct_sum.gmonoid A
- mul_comm : ∀ (a b : Σ (i : ι), A i), a * b = b * a
A graded version of comm_monoid.
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) :
direct_sum.ghas_one.one = ⟨1, one_mem⟩
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
- direct_sum.ghas_one.of_add_submonoids carriers one_mem = {one := ⟨1, one_mem⟩}
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.
@[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
- direct_sum.gmonoid.of_add_submonoids carriers one_mem mul_mem = {to_ghas_mul := {mul := direct_sum.ghas_mul.mul (direct_sum.ghas_mul.of_add_submonoids carriers mul_mem)}, to_ghas_one := {one := direct_sum.ghas_one.one (direct_sum.ghas_one.of_add_submonoids carriers one_mem)}, one_mul := _, mul_one := _, mul_assoc := _}
@[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)) :
direct_sum.gmonoid.to_ghas_mul = direct_sum.ghas_mul.of_add_submonoids carriers mul_mem
@[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)) :
direct_sum.gmonoid.to_ghas_one = direct_sum.ghas_one.of_add_submonoids carriers one_mem
@[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)) :
direct_sum.gcomm_monoid.to_gmonoid = direct_sum.gmonoid.of_add_submonoids carriers one_mem mul_mem
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
- direct_sum.gcomm_monoid.of_add_submonoids carriers one_mem mul_mem = {to_gmonoid := {to_ghas_mul := direct_sum.gmonoid.to_ghas_mul (direct_sum.gmonoid.of_add_submonoids carriers one_mem mul_mem), to_ghas_one := direct_sum.gmonoid.to_ghas_one (direct_sum.gmonoid.of_add_submonoids carriers one_mem mul_mem), one_mul := _, mul_one := _, mul_assoc := _}, mul_comm := _}
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) :
direct_sum.ghas_one.one = ⟨1, one_mem⟩
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
- direct_sum.ghas_one.of_add_subgroups carriers one_mem = direct_sum.ghas_one.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) one_mem
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
- direct_sum.ghas_mul.of_add_subgroups carriers mul_mem = direct_sum.ghas_mul.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) mul_mem
@[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)) :
direct_sum.gmonoid.to_ghas_mul = direct_sum.ghas_mul.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) mul_mem
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
- direct_sum.gmonoid.of_add_subgroups carriers one_mem mul_mem = direct_sum.gmonoid.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) one_mem mul_mem
@[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)) :
direct_sum.gmonoid.to_ghas_one = direct_sum.ghas_one.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) one_mem
@[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)) :
direct_sum.gcomm_monoid.to_gmonoid = direct_sum.gmonoid.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) one_mem mul_mem
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
- direct_sum.gcomm_monoid.of_add_subgroups carriers one_mem mul_mem = direct_sum.gcomm_monoid.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) one_mem mul_mem
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
- direct_sum.ghas_one.of_submodules carriers one_mem = direct_sum.ghas_one.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) one_mem
@[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) :
direct_sum.ghas_one.one = ⟨1, one_mem⟩
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
- direct_sum.ghas_mul.of_submodules carriers mul_mem = direct_sum.ghas_mul.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) mul_mem
@[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)) :
direct_sum.gmonoid.to_ghas_one = direct_sum.ghas_one.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) one_mem
@[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)) :
direct_sum.gmonoid.to_ghas_mul = direct_sum.ghas_mul.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) mul_mem
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
- direct_sum.gmonoid.of_submodules carriers one_mem mul_mem = direct_sum.gmonoid.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) one_mem mul_mem
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
- direct_sum.gcomm_monoid.of_submodules carriers one_mem mul_mem = direct_sum.gcomm_monoid.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) one_mem mul_mem
@[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)) :
direct_sum.gcomm_monoid.to_gmonoid = direct_sum.gmonoid.of_add_submonoids (λ (i : ι), (carriers i).to_add_submonoid) one_mem mul_mem
Instances for ⨁ i, A i #
@[protected, 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
- direct_sum.has_one A = {one := ⇑(direct_sum.of (λ (i : ι), A i) 0) direct_sum.ghas_one.one}
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] :
The multiplication from the has_mul instance, as a bundled homomorphism.
Equations
- direct_sum.mul_hom A = direct_sum.to_add_monoid (λ (i : ι), (direct_sum.to_add_monoid (λ (j : ι), ((⇑add_monoid_hom.comp_hom (direct_sum.of A (i + j))).comp direct_sum.ghas_mul.mul).flip)).flip)
@[protected, instance]
def
direct_sum.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)
Equations
- direct_sum.has_mul A = {mul := λ (a b : ⨁ (i : ι), A i), ⇑(⇑(direct_sum.mul_hom A) a) b}
@[protected, instance]
def
direct_sum.mul_zero_class
{ι : Type u_1}
[decidable_eq ι]
(A : ι → Type u_2)
[has_add ι]
[Π (i : ι), add_comm_monoid (A i)]
[direct_sum.ghas_mul A] :
mul_zero_class (⨁ (i : ι), A i)
Equations
- direct_sum.mul_zero_class A = {mul := has_mul.mul (direct_sum.has_mul (λ (i : ι), A i)), zero := 0, zero_mul := _, mul_zero := _}
@[protected, instance]
def
direct_sum.distrib
{ι : Type u_1}
[decidable_eq ι]
(A : ι → Type u_2)
[has_add ι]
[Π (i : ι), add_comm_monoid (A i)]
[direct_sum.ghas_mul A] :
distrib (⨁ (i : ι), A i)
Equations
- direct_sum.distrib A = {mul := has_mul.mul (direct_sum.has_mul (λ (i : ι), A i)), add := has_add.add (add_zero_class.to_has_add (⨁ (i : ι), A i)), left_distrib := _, right_distrib := _}
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)
@[protected, 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
- direct_sum.semiring A = {add := has_add.add (distrib.to_has_add (⨁ (i : ι), A i)), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (direct_sum.add_comm_monoid ι (λ (i : ι), A i)), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul (direct_sum.has_mul (λ (i : ι), A i)), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid_with_zero.npow._default 1 has_mul.mul _ _, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
@[protected, 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
- direct_sum.comm_semiring A = {add := has_add.add (distrib.to_has_add (⨁ (i : ι), A i)), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := semiring.nsmul (direct_sum.semiring (λ (i : ι), A i)), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul (direct_sum.has_mul (λ (i : ι), A i)), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := semiring.npow (direct_sum.semiring (λ (i : ι), A i)), npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[protected, 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
- direct_sum.ring A = {add := has_add.add (distrib.to_has_add (⨁ (i : ι), A i)), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := semiring.nsmul (direct_sum.semiring (λ (i : ι), A i)), nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg (sub_neg_monoid.to_has_neg (⨁ (i : ι), A i)), sub := add_comm_group.sub (direct_sum.add_comm_group (λ (i : ι), A i)), sub_eq_add_neg := _, gsmul := add_comm_group.gsmul (direct_sum.add_comm_group (λ (i : ι), A i)), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul (direct_sum.has_mul (λ (i : ι), A i)), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := semiring.npow (direct_sum.semiring (λ (i : ι), A i)), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[protected, 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
- direct_sum.comm_ring A = {add := has_add.add (distrib.to_has_add (⨁ (i : ι), A i)), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := ring.nsmul (direct_sum.ring (λ (i : ι), A i)), nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg (sub_neg_monoid.to_has_neg (⨁ (i : ι), A i)), sub := ring.sub (direct_sum.ring (λ (i : ι), A i)), sub_eq_add_neg := _, gsmul := ring.gsmul (direct_sum.ring (λ (i : ι), A i)), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul (direct_sum.has_mul (λ (i : ι), A i)), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := ring.npow (direct_sum.ring (λ (i : ι), A i)), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
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.
@[protected, 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
- direct_sum.grade_zero.has_one A = {one := direct_sum.ghas_one.one _inst_3}
@[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)] :
⇑(direct_sum.of A 0) 1 = 1
@[protected, 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
- direct_sum.grade_zero.has_scalar A i = {smul := λ (x : A 0) (y : A i), eq.rec (⇑(⇑direct_sum.ghas_mul.mul x) y) _}
@[protected, 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) :
@[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) :
⇑(direct_sum.of A i) (a • b) = (⇑(direct_sum.of A 0) a) * ⇑(direct_sum.of A i) b
@[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
@[protected, instance]
def
direct_sum.grade_zero.mul_zero_class
{ι : Type u_1}
[decidable_eq ι]
(A : ι → Type u_2)
[add_monoid ι]
[Π (i : ι), add_comm_monoid (A i)]
[direct_sum.ghas_mul A] :
mul_zero_class (A 0)
Equations
@[protected, instance]
def
direct_sum.grade_zero.distrib
{ι : Type u_1}
[decidable_eq ι]
(A : ι → Type u_2)
[add_monoid ι]
[Π (i : ι), add_comm_monoid (A i)]
[direct_sum.ghas_mul A] :
distrib (A 0)
Equations
@[protected, 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
- direct_sum.grade_zero.smul_with_zero A i = let _inst : smul_with_zero (A 0) (⨁ (i : ι), A i) := smul_with_zero.comp_hom (⨁ (i : ι), A i) (direct_sum.of A 0).to_zero_hom in function.injective.smul_with_zero (direct_sum.of A i).to_zero_hom _ _
@[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 ι]
[direct_sum.gmonoid A] :
semiring (A 0)
The semiring structure derived from gmonoid A.
Equations
- direct_sum.grade_zero.semiring A = function.injective.semiring ⇑(direct_sum.of A 0) _ _ _ _ _
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
- direct_sum.of_zero_ring_hom A = {to_fun := (direct_sum.of A 0).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[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 ι]
[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
- direct_sum.grade_zero.module A = let _inst : module (A 0) (⨁ (i : ι), A i) := module.comp_hom (⨁ (i : ι), A i) (direct_sum.of_zero_ring_hom A) in function.injective.module (A 0) (direct_sum.of A i) _ _
@[protected, 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] :
comm_semiring (A 0)
The comm_semiring structure derived from gcomm_monoid A.
Equations
- direct_sum.grade_zero.comm_semiring A = function.injective.comm_semiring ⇑(direct_sum.of A 0) _ _ _ _ _
@[protected, 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
- direct_sum.grade_zero.ring A = function.injective.ring ⇑(direct_sum.of A 0) _ _ _ _ _ _ _
@[protected, 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
- direct_sum.grade_zero.comm_ring A = function.injective.comm_ring ⇑(direct_sum.of A 0) _ _ _ _ _ _ _
@[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.
@[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) :
⇑(direct_sum.to_semiring f hone hmul) ᾰ = ⇑(direct_sum.to_add_monoid f) ᾰ
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
- direct_sum.to_semiring f hone hmul = {to_fun := ⇑(direct_sum.to_add_monoid f), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[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) :
↑(direct_sum.to_semiring f hone hmul) = direct_sum.to_add_monoid f
@[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 : ι) :
↑(⇑(direct_sum.lift_ring_hom.symm) F) = ↑F.comp (direct_sum.of A 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] :
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
- direct_sum.lift_ring_hom = {to_fun := λ (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}), direct_sum.to_semiring f.val _ _, inv_fun := λ (F : (⨁ (i : ι), A i) →+* R), ⟨λ (i : ι), ↑F.comp (direct_sum.of A i), _⟩, left_inv := _, right_inv := _}
Concrete instances #
@[protected, 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
- semiring.direct_sum_gmonoid = {to_ghas_mul := {mul := λ (i j : ι), add_monoid_hom.mul}, to_ghas_one := {one := 1}, one_mul := _, mul_one := _, mul_assoc := _}
@[simp]
theorem
semiring.direct_sum_mul
{ι : Type u_1}
[decidable_eq ι]
{R : Type u_2}
[add_monoid ι]
[semiring R]
{i j : ι}
(x y : R) :
⇑(⇑direct_sum.ghas_mul.mul x) y = x * y
@[protected, 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
@[protected, 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
- S.nat_power_direct_sum_gmonoid = direct_sum.gmonoid.of_submodules (λ (i : ℕ), S ^ i) _ _
@[protected, 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
- S.nat_power_direct_sum_gcomm_monoid = direct_sum.gcomm_monoid.of_submodules (λ (i : ℕ), S ^ i) _ _