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.submodule_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.submodule_is_internal for providing an explicit decomposition function.

When complete_lattice.independent (set.range A) (a weaker condition than direct_sum.submodule_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

From add_submonoids #

@[protected, instance]
def add_submonoid.gsemiring {ι : Type u_1} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring R] (A : ι → add_submonoid R) [set_like.graded_monoid A] :
direct_sum.gsemiring (λ (i : ι), (A i))

Build a gsemiring instance for a collection of add_submonoids.

Equations
@[protected, instance]
def add_submonoid.gcomm_semiring {ι : Type u_1} {R : Type u_3} [decidable_eq ι] [add_comm_monoid ι] [comm_semiring R] (A : ι → add_submonoid R) [set_like.graded_monoid A] :
direct_sum.gcomm_semiring (λ (i : ι), (A i))

Build a gcomm_semiring instance for a collection of add_submonoids.

Equations
def direct_sum.submonoid_coe_ring_hom {ι : Type u_1} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring R] (A : ι → add_submonoid R) [h : set_like.graded_monoid A] :
(⨁ (i : ι), (A i)) →+* R

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

Equations
@[simp]
theorem direct_sum.submonoid_coe_ring_hom_of {ι : Type u_1} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring R] (A : ι → add_submonoid R) [h : set_like.graded_monoid A] (i : ι) (x : (A i)) :

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

theorem direct_sum.coe_mul_apply_add_submonoid {ι : Type u_1} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [semiring R] (A : ι → add_submonoid R) [set_like.graded_monoid A] [Π (i : ι) (x : (A i)), decidable (x 0)] (r r' : ⨁ (i : ι), (A i)) (i : ι) :
((r * r') i) = ∑ (ij : ι × ι) in finset.filter (λ (ij : ι × ι), ij.fst + ij.snd = i) ((dfinsupp.support r).product (dfinsupp.support r')), ((r ij.fst)) * (r' ij.snd)

From add_subgroups #

@[protected, instance]
def add_subgroup.gsemiring {ι : Type u_1} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [ring R] (A : ι → add_subgroup R) [h : set_like.graded_monoid A] :
direct_sum.gsemiring (λ (i : ι), (A i))

Build a gsemiring instance for a collection of add_subgroups.

Equations
@[protected, instance]
def add_subgroup.gcomm_semiring {ι : Type u_1} {R : Type u_3} [decidable_eq ι] [add_comm_group ι] [comm_ring R] (A : ι → add_subgroup R) [h : set_like.graded_monoid A] :
direct_sum.gsemiring (λ (i : ι), (A i))

Build a gcomm_semiring instance for a collection of add_subgroups.

Equations
def direct_sum.subgroup_coe_ring_hom {ι : Type u_1} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [ring R] (A : ι → add_subgroup R) [set_like.graded_monoid A] :
(⨁ (i : ι), (A i)) →+* R

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

Equations
@[simp]
theorem direct_sum.subgroup_coe_ring_hom_of {ι : Type u_1} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [ring R] (A : ι → add_subgroup R) [set_like.graded_monoid A] (i : ι) (x : (A i)) :
theorem direct_sum.coe_mul_apply_add_subgroup {ι : Type u_1} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [ring R] (A : ι → add_subgroup R) [set_like.graded_monoid A] [Π (i : ι) (x : (A i)), decidable (x 0)] (r r' : ⨁ (i : ι), (A i)) (i : ι) :
((r * r') i) = ∑ (ij : ι × ι) in finset.filter (λ (ij : ι × ι), ij.fst + ij.snd = i) ((dfinsupp.support r).product (dfinsupp.support r')), ((r ij.fst)) * (r' ij.snd)

From submoduless #

@[protected, instance]
def submodule.gsemiring {ι : Type u_1} {S : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring S] [semiring R] [algebra S R] (A : ι → submodule S R) [h : set_like.graded_monoid A] :
direct_sum.gsemiring (λ (i : ι), (A i))

Build a gsemiring instance for a collection of submodules.

Equations
@[protected, instance]
def submodule.gcomm_semiring {ι : Type u_1} {S : Type u_2} {R : Type u_3} [decidable_eq ι] [add_comm_monoid ι] [comm_semiring S] [comm_semiring R] [algebra S R] (A : ι → submodule S R) [h : set_like.graded_monoid A] :
direct_sum.gcomm_semiring (λ (i : ι), (A i))

Build a gsemiring instance for a collection of submodules.

Equations
@[protected, instance]
def submodule.galgebra {ι : Type u_1} {S : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring S] [semiring R] [algebra S R] (A : ι → submodule S R) [h : 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_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring S] [semiring R] [algebra S R] (A : ι → submodule S R) [h : set_like.graded_monoid A] (s : S) :
@[protected, instance]
def submodule.nat_power_graded_monoid {S : Type u_2} {R : Type u_3} [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.submodule_coe_alg_hom {ι : Type u_1} {S : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring S] [semiring R] [algebra S R] (A : ι → submodule S R) [h : set_like.graded_monoid A] :
(⨁ (i : ι), (A i)) →ₐ[S] R

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

Equations
@[simp]
theorem direct_sum.submodule_coe_alg_hom_of {ι : Type u_1} {S : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring S] [semiring R] [algebra S R] (A : ι → submodule S R) [h : set_like.graded_monoid A] (i : ι) (x : (A i)) :
theorem direct_sum.coe_mul_apply_submodule {ι : Type u_1} {S : Type u_2} {R : Type u_3} [decidable_eq ι] [add_monoid ι] [comm_semiring S] [semiring R] [algebra S R] (A : ι → submodule S R) [Π (i : ι) (x : (A i)), decidable (x 0)] [set_like.graded_monoid A] (r r' : ⨁ (i : ι), (A i)) (i : ι) :
((r * r') i) = ∑ (ij : ι × ι) in finset.filter (λ (ij : ι × ι), ij.fst + ij.snd = i) ((dfinsupp.support r).product (dfinsupp.support r')), ((r ij.fst)) * (r' ij.snd)
theorem set_like.is_homogeneous_zero_submodule {ι : Type u_1} {S : Type u_2} {R : Type u_3} [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_2} {R : Type u_3} [comm_semiring S] [semiring R] [algebra S R] {A : ι → submodule S R} {s : S} {r : R} (hr : set_like.is_homogeneous A r) :