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:
- on
add_submonoid Rs:add_submonoid.gsemiring,add_submonoid.gcomm_semiring. - on
add_subgroup Rs:add_subgroup.gsemiring,add_subgroup.gcomm_semiring. - on
submodule S Rs:submodule.gsemiring,submodule.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.add_submonoid_coe_ring_hom(aring_homversion ofdirect_sum.add_submonoid_coe)direct_sum.add_subgroup_coe_ring_hom(aring_homversion ofdirect_sum.add_subgroup_coe)direct_sum.submodule_coe_alg_hom(analg_homversion ofdirect_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.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
- add_submonoid.gsemiring A = {mul := graded_monoid.gmonoid.mul (set_like.gmonoid A), mul_zero := _, zero_mul := _, mul_add := _, add_mul := _, one := graded_monoid.gmonoid.one (set_like.gmonoid A), one_mul := _, mul_one := _, mul_assoc := _, gnpow := graded_monoid.gmonoid.gnpow (set_like.gmonoid A), gnpow_zero' := _, gnpow_succ' := _}
@[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
- add_submonoid.gcomm_semiring A = {mul := graded_monoid.gcomm_monoid.mul (set_like.gcomm_monoid A), mul_zero := _, zero_mul := _, mul_add := _, add_mul := _, one := graded_monoid.gcomm_monoid.one (set_like.gcomm_monoid A), one_mul := _, mul_one := _, mul_assoc := _, gnpow := graded_monoid.gcomm_monoid.gnpow (set_like.gcomm_monoid A), gnpow_zero' := _, gnpow_succ' := _, mul_comm := _}
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] :
The canonical ring isomorphism between ⨁ i, A i and R
Equations
- direct_sum.submonoid_coe_ring_hom A = direct_sum.to_semiring (λ (i : ι), (A i).subtype) _ _
@[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)) :
⇑(direct_sum.submonoid_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_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 : ι) :
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
- add_subgroup.gsemiring A = have i' : set_like.graded_monoid (λ (i : ι), (A i).to_add_submonoid), from _, add_submonoid.gsemiring (λ (i : ι), (A i).to_add_submonoid) i'
@[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
- add_subgroup.gcomm_semiring A = have i' : set_like.graded_monoid (λ (i : ι), (A i).to_add_submonoid), from _, add_submonoid.gsemiring (λ (i : ι), (A i).to_add_submonoid) i'
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] :
The canonical ring isomorphism between ⨁ i, A i and R.
Equations
- direct_sum.subgroup_coe_ring_hom A = direct_sum.to_semiring (λ (i : ι), (A i).subtype) _ _
@[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)) :
⇑(direct_sum.subgroup_coe_ring_hom A) (⇑(direct_sum.of (λ (i : ι), ↥(A i)) i) x) = ↑x
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 : ι) :
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
- submodule.gsemiring A = have i' : set_like.graded_monoid (λ (i : ι), (A i).to_add_submonoid), from _, add_submonoid.gsemiring (λ (i : ι), (A i).to_add_submonoid) i'
@[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
- submodule.gcomm_semiring A = have i' : set_like.graded_monoid (λ (i : ι), (A i).to_add_submonoid), from _, add_submonoid.gcomm_semiring (λ (i : ι), (A i).to_add_submonoid) i'
@[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
- submodule.galgebra A = {to_fun := (linear_map.cod_restrict (A 0) (algebra.linear_map S R) _).to_add_monoid_hom, map_one := _, map_mul := _, commutes := _, smul_def := _}
@[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) :
↑(⇑direct_sum.galgebra.to_fun s) = ⇑(algebra_map S R) 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] :
The canonical algebra isomorphism between ⨁ i, A i and R.
Equations
- direct_sum.submodule_coe_alg_hom A = direct_sum.to_algebra S (λ (i : ι), ↥(A i)) (λ (i : ι), (A i).subtype) _ _ _
theorem
submodule.supr_eq_to_submodule_range
{ι : 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)
[set_like.graded_monoid A] :
(⨆ (i : ι), A i) = (direct_sum.submodule_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.submodule_coe_alg_hom.
@[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)) :
⇑(direct_sum.submodule_coe_alg_hom A) (⇑(direct_sum.of (λ (i : ι), ↥(A i)) i) x) = ↑x
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 : ι) :
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) :
set_like.is_homogeneous A (s • r)