# mathlib3documentation

algebra.direct_sum.internal

# Internally graded rings and algebras #

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

This module provides gsemiring and gcomm_semiring instances for a collection of subobjects A when a set_like.graded_monoid instance is available:

• set_like.gnon_unital_non_assoc_semiring
• set_like.gsemiring
• set_like.gcomm_semiring

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

• direct_sum.coe_ring_hom (a ring_hom version of direct_sum.coe_add_monoid_hom)
• direct_sum.coe_alg_hom (an alg_hom version of direct_sum.submodule_coe)

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

When complete_lattice.independent (set.range A) (a weaker condition than direct_sum.is_internal A), these provide a grading 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 #

@[protected, instance]
def add_comm_monoid.of_submonoid_on_semiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [semiring R] [ R] [ R] (A : ι σ) (i : ι) :
Equations
@[protected, instance]
def add_comm_group.of_subgroup_on_ring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [ring R] [ R] [ R] (A : ι σ) (i : ι) :
Equations
• = λ (i : ι),
theorem set_like.algebra_map_mem_graded {ι : Type u_1} {S : Type u_3} {R : Type u_4} [has_zero ι] [semiring R] [ R] (A : ι R) (s : S) :
R) s A 0
theorem set_like.nat_cast_mem_graded {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [has_zero ι] [ R] [ R] (A : ι σ) (n : ) :
n A 0
theorem set_like.int_cast_mem_graded {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [has_zero ι] [ R] [ R] (A : ι σ) (z : ) :
z A 0

#### From add_submonoids and add_subgroups #

@[protected, instance]
def set_like.gnon_unital_non_assoc_semiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [has_add ι] [ R] [ R] (A : ι σ)  :

Build a gnon_unital_non_assoc_semiring instance for a collection of additive submonoids.

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

Build a gsemiring instance for a collection of additive submonoids.

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

Build a gcomm_semiring instance for a collection of additive submonoids.

Equations
@[protected, instance]
def set_like.gring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [add_monoid ι] [ring R] [ R] [ R] (A : ι σ)  :
direct_sum.gring (λ (i : ι), (A i))

Build a gring instance for a collection of additive subgroups.

Equations
@[protected, instance]
def set_like.gcomm_ring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [comm_ring R] [ R] [ R] (A : ι σ)  :
direct_sum.gcomm_ring (λ (i : ι), (A i))

Build a gcomm_semiring instance for a collection of additive submonoids.

Equations
def direct_sum.coe_ring_hom {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) [add_monoid ι]  :
(λ (i : ι), (A i)) →+* R

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

Equations
@[simp]
theorem direct_sum.coe_ring_hom_of {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) [add_monoid ι] (i : ι) (x : (A i)) :
((direct_sum.of (λ (i : ι), (A i)) i) x) = x

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

theorem direct_sum.coe_mul_apply {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) [add_monoid ι] [Π (i : ι) (x : (A i)), decidable (x 0)] (r r' : (λ (i : ι), (A i))) (n : ι) :
((r * r') n) = (finset.filter (λ (ij : ι × ι), ij.fst + ij.snd = n) .sum (λ (ij : ι × ι), (r ij.fst) * (r' ij.snd))
theorem direct_sum.coe_mul_apply_eq_dfinsupp_sum {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) [add_monoid ι] [Π (i : ι) (x : (A i)), decidable (x 0)] (r r' : (λ (i : ι), (A i))) (n : ι) :
((r * r') n) = (λ (i : ι) (ri : (λ (i : ι), (A i)) i), (λ (j : ι) (rj : (λ (i : ι), (A i)) j), ite (i + j = n) (ri * rj) 0))
theorem direct_sum.coe_of_mul_apply_aux {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) [add_monoid ι] {i : ι} (r : (A i)) (r' : (λ (i : ι), (A i))) {j n : ι} (H : (x : ι), i + x = n x = j) :
(((direct_sum.of (λ {i : ι}, (A i)) i) r * r') n) = r * (r' j)
theorem direct_sum.coe_mul_of_apply_aux {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) [add_monoid ι] (r : (λ (i : ι), (A i))) {i : ι} (r' : (A i)) {j n : ι} (H : (x : ι), x + i = n x = j) :
((r * (direct_sum.of (λ {i : ι}, (A i)) i) r') n) = (r j) * r'
theorem direct_sum.coe_of_mul_apply_add {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) {i : ι} (r : (A i)) (r' : (λ (i : ι), (A i))) (j : ι) :
(((direct_sum.of (λ {i : ι}, (A i)) i) r * r') (i + j)) = r * (r' j)
theorem direct_sum.coe_mul_of_apply_add {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) (r : (λ (i : ι), (A i))) {i : ι} (r' : (A i)) (j : ι) :
((r * (direct_sum.of (λ {i : ι}, (A i)) i) r') (j + i)) = (r j) * r'
theorem direct_sum.coe_of_mul_apply_of_not_le {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) {i : ι} (r : (A i)) (r' : (λ (i : ι), (A i))) (n : ι) (h : ¬i n) :
(((direct_sum.of (λ {i : ι}, (A i)) i) r * r') n) = 0
theorem direct_sum.coe_mul_of_apply_of_not_le {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) (r : (λ (i : ι), (A i))) {i : ι} (r' : (A i)) (n : ι) (h : ¬i n) :
((r * (direct_sum.of (λ {i : ι}, (A i)) i) r') n) = 0
theorem direct_sum.coe_mul_of_apply_of_le {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) [has_sub ι] (r : (λ (i : ι), (A i))) {i : ι} (r' : (A i)) (n : ι) (h : i n) :
((r * (direct_sum.of (λ {i : ι}, (A i)) i) r') n) = (r (n - i)) * r'
theorem direct_sum.coe_of_mul_apply_of_le {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) [has_sub ι] {i : ι} (r : (A i)) (r' : (λ (i : ι), (A i))) (n : ι) (h : i n) :
(((direct_sum.of (λ {i : ι}, (A i)) i) r * r') n) = r * (r' (n - i))
theorem direct_sum.coe_mul_of_apply {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) [has_sub ι] (r : (λ (i : ι), (A i))) {i : ι} (r' : (A i)) (n : ι) [decidable (i n)] :
((r * (direct_sum.of (λ {i : ι}, (A i)) i) r') n) = ite (i n) ((r (n - i)) * r') 0
theorem direct_sum.coe_of_mul_apply {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [decidable_eq ι] [semiring R] [ R] [ R] (A : ι σ) [has_sub ι] {i : ι} (r : (A i)) (r' : (λ (i : ι), (A i))) (n : ι) [decidable (i n)] :
(((direct_sum.of (λ {i : ι}, (A i)) i) r * r') n) = ite (i n) (r * (r' (n - i))) 0

#### From submodules #

@[protected, instance]
def submodule.galgebra {ι : Type u_1} {S : Type u_3} {R : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring R] [ R] (A : ι R)  :
(λ (i : ι), (A i))

Build a galgebra instance for a collection of submodules.

Equations
@[simp]
theorem submodule.set_like.coe_galgebra_to_fun {ι : Type u_1} {S : Type u_3} {R : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring R] [ R] (A : ι R) (s : S) :
= R) s
@[protected, instance]
def submodule.nat_power_graded_monoid {S : Type u_3} {R : Type u_4} [semiring R] [ R] (p : R) :
set_like.graded_monoid (λ (i : ), p ^ i)

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

def direct_sum.coe_alg_hom {ι : Type u_1} {S : Type u_3} {R : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring R] [ R] (A : ι R)  :
(λ (i : ι), (A i)) →ₐ[S] R

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

Equations
• = (λ (i : ι), (A i)) (λ (i : ι), (A i).subtype) _ _ _
theorem submodule.supr_eq_to_submodule_range {ι : Type u_1} {S : Type u_3} {R : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring R] [ R] (A : ι R)  :
( (i : ι), A i) =

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

@[simp]
theorem direct_sum.coe_alg_hom_of {ι : Type u_1} {S : Type u_3} {R : Type u_4} [decidable_eq ι] [add_monoid ι] [semiring R] [ R] (A : ι R) (i : ι) (x : (A i)) :
((direct_sum.of (λ (i : ι), (A i)) i) x) = x
theorem set_like.is_homogeneous_zero_submodule {ι : Type u_1} {S : Type u_3} {R : Type u_4} [has_zero ι] [semiring S] [ R] (A : ι R) :
theorem set_like.is_homogeneous.smul {ι : Type u_1} {S : Type u_3} {R : Type u_4} [semiring R] [ R] {A : ι R} {s : S} {r : R} (hr : r) :
(s r)