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:
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(aring_homversion ofdirect_sum.coe_add_monoid_hom)direct_sum.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.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 : ι) :
add_comm_monoid ↥(A i)
Equations
- add_comm_monoid.of_submonoid_on_semiring A = λ (i : ι), add_submonoid_class.to_add_comm_monoid (A i)
@[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 : ι) :
add_comm_group ↥(A i)
Equations
- add_comm_group.of_subgroup_on_ring A = λ (i : ι), add_subgroup_class.to_add_comm_group (A i)
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 : ℕ) :
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 : ℤ) :
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] :
direct_sum.gnon_unital_non_assoc_semiring (λ (i : ι), ↥(A i))
Build a gnon_unital_non_assoc_semiring instance for a collection of additive submonoids.
Equations
- set_like.gnon_unital_non_assoc_semiring A = {mul := graded_monoid.ghas_mul.mul (set_like.ghas_mul A), mul_zero := _, zero_mul := _, mul_add := _, add_mul := _}
@[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
- set_like.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' := _, nat_cast := λ (n : ℕ), ⟨↑n, _⟩, nat_cast_zero := _, nat_cast_succ := _}
@[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
- set_like.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' := _, nat_cast := direct_sum.gsemiring.nat_cast (set_like.gsemiring A), nat_cast_zero := _, nat_cast_succ := _, mul_comm := _}
@[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
- set_like.gring A = {mul := direct_sum.gsemiring.mul (set_like.gsemiring A), mul_zero := _, zero_mul := _, mul_add := _, add_mul := _, one := direct_sum.gsemiring.one (set_like.gsemiring A), one_mul := _, mul_one := _, mul_assoc := _, gnpow := direct_sum.gsemiring.gnpow (set_like.gsemiring A), gnpow_zero' := _, gnpow_succ' := _, nat_cast := direct_sum.gsemiring.nat_cast (set_like.gsemiring A), nat_cast_zero := _, nat_cast_succ := _, int_cast := λ (z : ℤ), ⟨↑z, _⟩, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}
@[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
- set_like.gcomm_ring 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' := _, nat_cast := direct_sum.gring.nat_cast (set_like.gring A), nat_cast_zero := _, nat_cast_succ := _, int_cast := direct_sum.gring.int_cast (set_like.gring A), int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul_comm := _}
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
- direct_sum.coe_ring_hom A = direct_sum.to_semiring (λ (i : ι), add_submonoid_class.subtype (A i)) _ _
@[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 : ι) :
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 : ι) :
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) :
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) :
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 : ι) :
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 : ι) :
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) :
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) :
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) :
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) :
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)] :
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)] :
@[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
- 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_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) :
↑(⇑direct_sum.galgebra.to_fun s) = ⇑(algebra_map S R) 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
- direct_sum.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_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) = ⇑subalgebra.to_submodule (direct_sum.coe_alg_hom A).range
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) :
set_like.is_homogeneous A (s • r)