Internally graded rings and algebras #
This module provides DirectSum.GSemiring and DirectSum.GCommSemiring instances for a collection
of subobjects A when a SetLike.GradedMonoid 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:
DirectSum.coeRingHom(aRingHomversion ofDirectSum.coeAddMonoidHom)DirectSum.coeAlgHom(anAlgHomversion ofDirectSum.coeLinearMap)
Strictly the definitions in this file are not sufficient to fully define an "internal" direct sum;
to represent this case, (h : DirectSum.IsInternal A) [SetLike.GradedMonoid A] is
needed. In the future there will likely be a data-carrying, constructive, typeclass version of
DirectSum.IsInternal for providing an explicit decomposition function.
When CompleteLattice.Independent (Set.range A) (a weaker condition than
DirectSum.IsInternal A), these provide a grading of ⨆ i, A i, and the
mapping ⨁ i, A i →+ ⨆ i, A i can be obtained as
DirectSum.toAddMonoid (fun i ↦ AddSubmonoid.inclusion $ le_iSup A i).
tags #
internally graded ring
instance
AddCommMonoid.ofSubmonoidOnSemiring
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
(i : ι)
:
AddCommMonoid { x // x ∈ A i }
instance
AddCommGroup.ofSubgroupOnRing
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[Ring R]
[SetLike σ R]
[AddSubgroupClass σ R]
(A : ι → σ)
(i : ι)
:
AddCommGroup { x // x ∈ A i }
theorem
SetLike.algebraMap_mem_graded
{ι : Type u_1}
{S : Type u_3}
{R : Type u_4}
[Zero ι]
[CommSemiring S]
[Semiring R]
[Algebra S R]
(A : ι → Submodule S R)
[SetLike.GradedOne A]
(s : S)
:
↑(algebraMap S R) s ∈ A 0
theorem
SetLike.nat_cast_mem_graded
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[Zero ι]
[AddMonoidWithOne R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[SetLike.GradedOne A]
(n : ℕ)
:
↑n ∈ A 0
theorem
SetLike.int_cast_mem_graded
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[Zero ι]
[AddGroupWithOne R]
[SetLike σ R]
[AddSubgroupClass σ R]
(A : ι → σ)
[SetLike.GradedOne A]
(z : ℤ)
:
↑z ∈ A 0
From AddSubmonoids and AddSubgroups #
instance
SetLike.gnonUnitalNonAssocSemiring
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[Add ι]
[NonUnitalNonAssocSemiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[SetLike.GradedMul A]
:
DirectSum.GNonUnitalNonAssocSemiring fun i => { x // x ∈ A i }
Build a DirectSum.GNonUnitalNonAssocSemiring instance for a collection of additive
submonoids.
instance
SetLike.gsemiring
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[AddMonoid ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[SetLike.GradedMonoid A]
:
DirectSum.GSemiring fun i => { x // x ∈ A i }
Build a DirectSum.GSemiring instance for a collection of additive submonoids.
instance
SetLike.gcommSemiring
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[AddCommMonoid ι]
[CommSemiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[SetLike.GradedMonoid A]
:
DirectSum.GCommSemiring fun i => { x // x ∈ A i }
Build a DirectSum.GCommSemiring instance for a collection of additive submonoids.
instance
SetLike.gring
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[AddMonoid ι]
[Ring R]
[SetLike σ R]
[AddSubgroupClass σ R]
(A : ι → σ)
[SetLike.GradedMonoid A]
:
DirectSum.GRing fun i => { x // x ∈ A i }
Build a DirectSum.GRing instance for a collection of additive subgroups.
instance
SetLike.gcommRing
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[AddCommMonoid ι]
[CommRing R]
[SetLike σ R]
[AddSubgroupClass σ R]
(A : ι → σ)
[SetLike.GradedMonoid A]
:
DirectSum.GCommRing fun i => { x // x ∈ A i }
Build a DirectSum.GCommRing instance for a collection of additive submonoids.
def
DirectSum.coeRingHom
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[AddMonoid ι]
[SetLike.GradedMonoid A]
:
The canonical ring isomorphism between ⨁ i, A i and R
Instances For
@[simp]
theorem
DirectSum.coeRingHom_of
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[AddMonoid ι]
[SetLike.GradedMonoid A]
(i : ι)
(x : { x // x ∈ A i })
:
↑(DirectSum.coeRingHom A) (↑(DirectSum.of (fun i => { x // x ∈ A i }) i) x) = ↑x
The canonical ring isomorphism between ⨁ i, A i and R
theorem
DirectSum.coe_mul_apply
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[AddMonoid ι]
[SetLike.GradedMonoid A]
[(i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)]
(r : ⨁ (i : ι), { x // x ∈ A i })
(r' : ⨁ (i : ι), { x // x ∈ A i })
(n : ι)
:
↑(↑(r * r') n) = Finset.sum (Finset.filter (fun ij => ij.fst + ij.snd = n) (DFinsupp.support r ×ˢ DFinsupp.support r')) fun ij =>
↑(↑r ij.fst) * ↑(↑r' ij.snd)
theorem
DirectSum.coe_mul_apply_eq_dfinsupp_sum
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[AddMonoid ι]
[SetLike.GradedMonoid A]
[(i : ι) → (x : { x // x ∈ A i }) → Decidable (x ≠ 0)]
(r : ⨁ (i : ι), { x // x ∈ A i })
(r' : ⨁ (i : ι), { x // x ∈ A i })
(n : ι)
:
↑(↑(r * r') n) = DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0
theorem
DirectSum.coe_of_mul_apply_aux
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[AddMonoid ι]
[SetLike.GradedMonoid A]
{i : ι}
(r : { x // x ∈ A i })
(r' : ⨁ (i : ι), { x // x ∈ A i })
{j : ι}
{n : ι}
(H : ∀ (x : ι), i + x = n ↔ x = j)
:
↑(↑(↑(DirectSum.of (fun i => { x // x ∈ A i }) i) r * r') n) = ↑r * ↑(↑r' j)
theorem
DirectSum.coe_mul_of_apply_aux
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[AddMonoid ι]
[SetLike.GradedMonoid A]
(r : ⨁ (i : ι), { x // x ∈ A i })
{i : ι}
(r' : { x // x ∈ A i })
{j : ι}
{n : ι}
(H : ∀ (x : ι), x + i = n ↔ x = j)
:
↑(↑(r * ↑(DirectSum.of (fun i => { x // x ∈ A i }) i) r') n) = ↑(↑r j) * ↑r'
theorem
DirectSum.coe_of_mul_apply_add
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[AddLeftCancelMonoid ι]
[SetLike.GradedMonoid A]
{i : ι}
(r : { x // x ∈ A i })
(r' : ⨁ (i : ι), { x // x ∈ A i })
(j : ι)
:
theorem
DirectSum.coe_mul_of_apply_add
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[AddRightCancelMonoid ι]
[SetLike.GradedMonoid A]
(r : ⨁ (i : ι), { x // x ∈ A i })
{i : ι}
(r' : { x // x ∈ A i })
(j : ι)
:
theorem
DirectSum.coe_of_mul_apply_of_not_le
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[CanonicallyOrderedAddMonoid ι]
[SetLike.GradedMonoid A]
{i : ι}
(r : { x // x ∈ A i })
(r' : ⨁ (i : ι), { x // x ∈ A i })
(n : ι)
(h : ¬i ≤ n)
:
↑(↑(↑(DirectSum.of (fun i => { x // x ∈ A i }) i) r * r') n) = 0
theorem
DirectSum.coe_mul_of_apply_of_not_le
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[CanonicallyOrderedAddMonoid ι]
[SetLike.GradedMonoid A]
(r : ⨁ (i : ι), { x // x ∈ A i })
{i : ι}
(r' : { x // x ∈ A i })
(n : ι)
(h : ¬i ≤ n)
:
↑(↑(r * ↑(DirectSum.of (fun i => { x // x ∈ A i }) i) r') n) = 0
theorem
DirectSum.coe_mul_of_apply_of_le
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[CanonicallyOrderedAddMonoid ι]
[SetLike.GradedMonoid A]
[Sub ι]
[OrderedSub ι]
[ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(r : ⨁ (i : ι), { x // x ∈ A i })
{i : ι}
(r' : { x // x ∈ A i })
(n : ι)
(h : i ≤ n)
:
theorem
DirectSum.coe_of_mul_apply_of_le
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[CanonicallyOrderedAddMonoid ι]
[SetLike.GradedMonoid A]
[Sub ι]
[OrderedSub ι]
[ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{i : ι}
(r : { x // x ∈ A i })
(r' : ⨁ (i : ι), { x // x ∈ A i })
(n : ι)
(h : i ≤ n)
:
theorem
DirectSum.coe_mul_of_apply
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[CanonicallyOrderedAddMonoid ι]
[SetLike.GradedMonoid A]
[Sub ι]
[OrderedSub ι]
[ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(r : ⨁ (i : ι), { x // x ∈ A i })
{i : ι}
(r' : { x // x ∈ A i })
(n : ι)
[Decidable (i ≤ n)]
:
theorem
DirectSum.coe_of_mul_apply
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[CanonicallyOrderedAddMonoid ι]
[SetLike.GradedMonoid A]
[Sub ι]
[OrderedSub ι]
[ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{i : ι}
(r : { x // x ∈ A i })
(r' : ⨁ (i : ι), { x // x ∈ A i })
(n : ι)
[Decidable (i ≤ n)]
:
instance
Submodule.galgebra
{ι : Type u_1}
{S : Type u_3}
{R : Type u_4}
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring S]
[Semiring R]
[Algebra S R]
(A : ι → Submodule S R)
[SetLike.GradedMonoid A]
:
DirectSum.GAlgebra S fun i => { x // x ∈ A i }
Build a DirectSum.GAlgebra instance for a collection of Submodules.
@[simp]
theorem
Submodule.setLike.coe_galgebra_toFun
{ι : Type u_1}
{S : Type u_3}
{R : Type u_4}
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring S]
[Semiring R]
[Algebra S R]
(A : ι → Submodule S R)
[SetLike.GradedMonoid A]
(s : S)
:
↑(↑DirectSum.GAlgebra.toFun s) = ↑(algebraMap S R) s
instance
Submodule.nat_power_gradedMonoid
{S : Type u_3}
{R : Type u_4}
[CommSemiring S]
[Semiring R]
[Algebra S R]
(p : Submodule S R)
:
SetLike.GradedMonoid fun i => p ^ i
A direct sum of powers of a submodule of an algebra has a multiplicative structure.
def
DirectSum.coeAlgHom
{ι : Type u_1}
{S : Type u_3}
{R : Type u_4}
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring S]
[Semiring R]
[Algebra S R]
(A : ι → Submodule S R)
[SetLike.GradedMonoid A]
:
The canonical algebra isomorphism between ⨁ i, A i and R.
Instances For
theorem
Submodule.iSup_eq_toSubmodule_range
{ι : Type u_1}
{S : Type u_3}
{R : Type u_4}
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring S]
[Semiring R]
[Algebra S R]
(A : ι → Submodule S R)
[SetLike.GradedMonoid A]
:
⨆ (i : ι), A i = ↑Subalgebra.toSubmodule (AlgHom.range (DirectSum.coeAlgHom A))
The supremum of submodules that form a graded monoid is a subalgebra, and equal to the range of
DirectSum.coeAlgHom.
@[simp]
theorem
DirectSum.coeAlgHom_of
{ι : Type u_1}
{S : Type u_3}
{R : Type u_4}
[DecidableEq ι]
[AddMonoid ι]
[CommSemiring S]
[Semiring R]
[Algebra S R]
(A : ι → Submodule S R)
[SetLike.GradedMonoid A]
(i : ι)
(x : { x // x ∈ A i })
:
↑(DirectSum.coeAlgHom A) (↑(DirectSum.of (fun i => { x // x ∈ A i }) i) x) = ↑x
theorem
SetLike.homogeneous_zero_submodule
{ι : Type u_1}
{S : Type u_3}
{R : Type u_4}
[Zero ι]
[Semiring S]
[AddCommMonoid R]
[Module S R]
(A : ι → Submodule S R)
:
theorem
SetLike.Homogeneous.smul
{ι : Type u_1}
{S : Type u_3}
{R : Type u_4}
[CommSemiring S]
[Semiring R]
[Algebra S R]
{A : ι → Submodule S R}
{s : S}
{r : R}
(hr : SetLike.Homogeneous A r)
:
SetLike.Homogeneous A (s • r)