mathlib documentation

algebra.direct_sum.internal

Internally graded rings and algebras #

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

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

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 #

internally graded ring

@[protected, instance]
def add_comm_monoid.of_submonoid_on_semiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [semiring R] [set_like σ R] [add_submonoid_class σ 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] [set_like σ R] [add_subgroup_class σ R] (A : ι → σ) (i : ι) :
Equations
theorem set_like.algebra_map_mem_graded {ι : Type u_1} {S : Type u_3} {R : Type u_4} [has_zero ι] [comm_semiring S] [semiring R] [algebra S R] (A : ι → submodule S R) [set_like.has_graded_one A] (s : S) :
(algebra_map S R) s A 0
theorem set_like.nat_cast_mem_graded {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [has_zero ι] [add_monoid_with_one R] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [set_like.has_graded_one A] (n : ) :
n A 0
theorem set_like.int_cast_mem_graded {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [has_zero ι] [add_group_with_one R] [set_like σ R] [add_subgroup_class σ R] (A : ι → σ) [set_like.has_graded_one 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 ι] [non_unital_non_assoc_semiring R] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [set_like.has_graded_mul 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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [set_like.graded_monoid 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 ι] [add_comm_monoid ι] [comm_semiring R] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [set_like.graded_monoid 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] [set_like σ R] [add_subgroup_class σ R] (A : ι → σ) [set_like.graded_monoid 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 ι] [add_comm_monoid ι] [comm_ring R] [set_like σ R] [add_subgroup_class σ R] (A : ι → σ) [set_like.graded_monoid 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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [add_monoid ι] [set_like.graded_monoid A] :
direct_sum ι (λ (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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [add_monoid ι] [set_like.graded_monoid A] (i : ι) (x : (A i)) :
(direct_sum.coe_ring_hom A) ((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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [add_monoid ι] [set_like.graded_monoid A] [Π (i : ι) (x : (A i)), decidable (x 0)] (r r' : direct_sum ι (λ (i : ι), (A i))) (n : ι) :
((r * r') n) = (finset.filter (λ (ij : ι × ι), ij.fst + ij.snd = n) (dfinsupp.support r ×ˢ dfinsupp.support r')).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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [add_monoid ι] [set_like.graded_monoid A] [Π (i : ι) (x : (A i)), decidable (x 0)] (r r' : direct_sum ι (λ (i : ι), (A i))) (n : ι) :
((r * r') n) = dfinsupp.sum r (λ (i : ι) (ri : (λ (i : ι), (A i)) i), dfinsupp.sum r' (λ (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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [add_monoid ι] [set_like.graded_monoid A] {i : ι} (r : (A i)) (r' : direct_sum ι (λ (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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [add_monoid ι] [set_like.graded_monoid A] (r : direct_sum ι (λ (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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [add_left_cancel_monoid ι] [set_like.graded_monoid A] {i : ι} (r : (A i)) (r' : direct_sum ι (λ (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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [add_right_cancel_monoid ι] [set_like.graded_monoid A] (r : direct_sum ι (λ (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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [canonically_ordered_add_monoid ι] [set_like.graded_monoid A] {i : ι} (r : (A i)) (r' : direct_sum ι (λ (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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [canonically_ordered_add_monoid ι] [set_like.graded_monoid A] (r : direct_sum ι (λ (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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [canonically_ordered_add_monoid ι] [set_like.graded_monoid A] [has_sub ι] [has_ordered_sub ι] [contravariant_class ι ι has_add.add has_le.le] (r : direct_sum ι (λ (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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [canonically_ordered_add_monoid ι] [set_like.graded_monoid A] [has_sub ι] [has_ordered_sub ι] [contravariant_class ι ι has_add.add has_le.le] {i : ι} (r : (A i)) (r' : direct_sum ι (λ (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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [canonically_ordered_add_monoid ι] [set_like.graded_monoid A] [has_sub ι] [has_ordered_sub ι] [contravariant_class ι ι has_add.add has_le.le] (r : direct_sum ι (λ (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] [set_like σ R] [add_submonoid_class σ R] (A : ι → σ) [canonically_ordered_add_monoid ι] [set_like.graded_monoid A] [has_sub ι] [has_ordered_sub ι] [contravariant_class ι ι has_add.add has_le.le] {i : ι} (r : (A i)) (r' : direct_sum ι (λ (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 ι] [comm_semiring S] [semiring R] [algebra S R] (A : ι → submodule S R) [set_like.graded_monoid A] :
direct_sum.galgebra S (λ (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 ι] [comm_semiring S] [semiring R] [algebra S R] (A : ι → submodule S R) [set_like.graded_monoid A] (s : S) :
@[protected, instance]
def submodule.nat_power_graded_monoid {S : Type u_3} {R : Type u_4} [comm_semiring S] [semiring R] [algebra S R] (p : submodule S 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 ι] [comm_semiring S] [semiring R] [algebra S R] (A : ι → submodule S R) [set_like.graded_monoid A] :
direct_sum ι (λ (i : ι), (A i)) →ₐ[S] R

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

Equations
theorem submodule.supr_eq_to_submodule_range {ι : Type u_1} {S : Type u_3} {R : Type u_4} [decidable_eq ι] [add_monoid ι] [comm_semiring S] [semiring R] [algebra S R] (A : ι → submodule S R) [set_like.graded_monoid A] :
(⨆ (i : ι), A i) = (direct_sum.coe_alg_hom A).range.to_submodule

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 ι] [comm_semiring S] [semiring R] [algebra S R] (A : ι → submodule S R) [set_like.graded_monoid A] (i : ι) (x : (A i)) :
(direct_sum.coe_alg_hom A) ((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] [add_comm_monoid R] [module S R] (A : ι → submodule S R) :
theorem set_like.is_homogeneous.smul {ι : Type u_1} {S : Type u_3} {R : Type u_4} [comm_semiring S] [semiring R] [algebra S R] {A : ι → submodule S R} {s : S} {r : R} (hr : set_like.is_homogeneous A r) :