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).
This file also provides some extra structure on A 0, namely:
SetLike.GradeZero.subsemiring, which leads toSetLike.GradeZero.subring, which leads toSetLike.GradeZero.subalgebra, which leads to
Tags #
internally graded ring
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.natCast_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
@[deprecated SetLike.natCast_mem_graded]
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
Alias of SetLike.natCast_mem_graded.
theorem
SetLike.intCast_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
@[deprecated SetLike.intCast_mem_graded]
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
Alias of SetLike.intCast_mem_graded.
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 : ι) => ↥(A i)
Build a DirectSum.GNonUnitalNonAssocSemiring instance for a collection of additive
submonoids.
Equations
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 : ι) => ↥(A i)
Build a DirectSum.GSemiring instance for a collection of additive submonoids.
Equations
- SetLike.gsemiring A = DirectSum.GSemiring.mk ⋯ ⋯ ⋯ GradedMonoid.GMonoid.gnpow ⋯ ⋯ (fun (n : ℕ) => ⟨↑n, ⋯⟩) ⋯ ⋯
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 : ι) => ↥(A i)
Build a DirectSum.GCommSemiring instance for a collection of additive submonoids.
Equations
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 : ι) => ↥(A i)
Build a DirectSum.GRing instance for a collection of additive subgroups.
Equations
- SetLike.gring A = DirectSum.GRing.mk (fun (z : ℤ) => ⟨↑z, ⋯⟩) ⋯ ⋯
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 : ι) => ↥(A i)
Build a DirectSum.GCommRing instance for a collection of additive submonoids.
Equations
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
Equations
- DirectSum.coeRingHom A = DirectSum.toSemiring (fun (i : ι) => AddSubmonoidClass.subtype (A i)) ⋯ ⋯
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 : ↥(A i))
:
(DirectSum.coeRingHom A) ((DirectSum.of (fun (i : ι) => ↥(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 : ↥(A i)) → Decidable (x ≠ 0)]
(r r' : DirectSum ι fun (i : ι) => ↥(A i))
(n : ι)
:
↑((r * r') n) = ∑ ij ∈ Finset.filter (fun (ij : ι × ι) => ij.1 + ij.2 = n) (DFinsupp.support r ×ˢ DFinsupp.support r'),
↑(r ij.1) * ↑(r' ij.2)
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 : ↥(A i)) → Decidable (x ≠ 0)]
(r r' : DirectSum ι fun (i : ι) => ↥(A i))
(n : ι)
:
↑((r * r') n) = DFinsupp.sum r fun (i : ι) (ri : ↥(A i)) =>
DFinsupp.sum r' fun (j : ι) (rj : ↥(A j)) => 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 : ↥(A i))
(r' : DirectSum ι fun (i : ι) => ↥(A i))
{j n : ι}
(H : ∀ (x : ι), i + x = n ↔ x = j)
:
↑(((DirectSum.of (fun (i : ι) => ↥(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 : DirectSum ι fun (i : ι) => ↥(A i))
{i : ι}
(r' : ↥(A i))
{j n : ι}
(H : ∀ (x : ι), x + i = n ↔ x = j)
:
↑((r * (DirectSum.of (fun (i : ι) => ↥(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 : ↥(A i))
(r' : DirectSum ι fun (i : ι) => ↥(A i))
(j : ι)
:
↑(((DirectSum.of (fun (i : ι) => ↥(A i)) i) r * r') (i + j)) = ↑r * ↑(r' 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 : DirectSum ι fun (i : ι) => ↥(A i))
{i : ι}
(r' : ↥(A i))
(j : ι)
:
↑((r * (DirectSum.of (fun (i : ι) => ↥(A i)) i) r') (j + i)) = ↑(r j) * ↑r'
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 : ι → σ)
[CanonicallyOrderedAddCommMonoid ι]
[SetLike.GradedMonoid A]
{i : ι}
(r : ↥(A i))
(r' : DirectSum ι fun (i : ι) => ↥(A i))
(n : ι)
(h : ¬i ≤ n)
:
↑(((DirectSum.of (fun (i : ι) => ↥(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 : ι → σ)
[CanonicallyOrderedAddCommMonoid ι]
[SetLike.GradedMonoid A]
(r : DirectSum ι fun (i : ι) => ↥(A i))
{i : ι}
(r' : ↥(A i))
(n : ι)
(h : ¬i ≤ n)
:
↑((r * (DirectSum.of (fun (i : ι) => ↥(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 : ι → σ)
[CanonicallyOrderedAddCommMonoid ι]
[SetLike.GradedMonoid A]
[Sub ι]
[OrderedSub ι]
[AddLeftReflectLE ι]
(r : DirectSum ι fun (i : ι) => ↥(A i))
{i : ι}
(r' : ↥(A i))
(n : ι)
(h : i ≤ n)
:
↑((r * (DirectSum.of (fun (i : ι) => ↥(A i)) i) r') n) = ↑(r (n - i)) * ↑r'
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 : ι → σ)
[CanonicallyOrderedAddCommMonoid ι]
[SetLike.GradedMonoid A]
[Sub ι]
[OrderedSub ι]
[AddLeftReflectLE ι]
{i : ι}
(r : ↥(A i))
(r' : DirectSum ι fun (i : ι) => ↥(A i))
(n : ι)
(h : i ≤ n)
:
↑(((DirectSum.of (fun (i : ι) => ↥(A i)) i) r * r') n) = ↑r * ↑(r' (n - i))
theorem
DirectSum.coe_mul_of_apply
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[DecidableEq ι]
[Semiring R]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[CanonicallyOrderedAddCommMonoid ι]
[SetLike.GradedMonoid A]
[Sub ι]
[OrderedSub ι]
[AddLeftReflectLE ι]
(r : DirectSum ι fun (i : ι) => ↥(A i))
{i : ι}
(r' : ↥(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 : ι → σ)
[CanonicallyOrderedAddCommMonoid ι]
[SetLike.GradedMonoid A]
[Sub ι]
[OrderedSub ι]
[AddLeftReflectLE ι]
{i : ι}
(r : ↥(A i))
(r' : DirectSum ι fun (i : ι) => ↥(A i))
(n : ι)
[Decidable (i ≤ n)]
:
instance
Submodule.galgebra
{ι : Type u_1}
{S : Type u_3}
{R : Type u_4}
[AddMonoid ι]
[CommSemiring S]
[Semiring R]
[Algebra S R]
(A : ι → Submodule S R)
[SetLike.GradedMonoid A]
:
DirectSum.GAlgebra S fun (i : ι) => ↥(A i)
Build a DirectSum.GAlgebra instance for a collection of Submodules.
Equations
- Submodule.galgebra A = { toFun := (LinearMap.codRestrict (A 0) (Algebra.linearMap S R) ⋯).toAddMonoidHom, map_one := ⋯, map_mul := ⋯, commutes := ⋯, smul_def := ⋯ }
@[simp]
theorem
Submodule.setLike.coe_galgebra_toFun
{S : Type u_3}
{R : Type u_4}
{ι : Type u_5}
[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.
Equations
- ⋯ = ⋯
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.
Equations
- DirectSum.coeAlgHom A = DirectSum.toAlgebra S (fun (i : ι) => ↥(A i)) (fun (i : ι) => (A i).subtype) ⋯ ⋯
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 (DirectSum.coeAlgHom A).range
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 : ↥(A i))
:
(DirectSum.coeAlgHom A) ((DirectSum.of (fun (i : ι) => ↥(A i)) i) x) = ↑x
Facts about grade zero #
def
SetLike.GradeZero.subsemiring
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[Semiring R]
[AddMonoid ι]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[SetLike.GradedMonoid A]
:
The subsemiring A 0 of R.
Equations
- SetLike.GradeZero.subsemiring A = { carrier := ↑(A 0), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
instance
SetLike.GradeZero.instSemiring
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[Semiring R]
[AddMonoid ι]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[SetLike.GradedMonoid A]
:
Semiring ↥(A 0)
The semiring A 0 inherited from R in the presence of SetLike.GradedMonoid A.
Equations
- SetLike.GradeZero.instSemiring A = (SetLike.GradeZero.subsemiring A).toSemiring
@[simp]
theorem
SetLike.GradeZero.coe_natCast
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[Semiring R]
[AddMonoid ι]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[SetLike.GradedMonoid A]
(n : ℕ)
:
↑↑n = ↑n
@[simp]
theorem
SetLike.GradeZero.coe_ofNat
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[Semiring R]
[AddMonoid ι]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[SetLike.GradedMonoid A]
(n : ℕ)
[n.AtLeastTwo]
:
↑(OfNat.ofNat n) = OfNat.ofNat n
instance
SetLike.GradeZero.instCommSemiring
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[CommSemiring R]
[AddCommMonoid ι]
[SetLike σ R]
[AddSubmonoidClass σ R]
(A : ι → σ)
[SetLike.GradedMonoid A]
:
CommSemiring ↥(A 0)
The commutative semiring A 0 inherited from R in the presence of SetLike.GradedMonoid A.
Equations
- SetLike.GradeZero.instCommSemiring A = (SetLike.GradeZero.subsemiring A).toCommSemiring
def
SetLike.GradeZero.subring
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[Ring R]
[AddMonoid ι]
[SetLike σ R]
[AddSubgroupClass σ R]
(A : ι → σ)
[SetLike.GradedMonoid A]
:
Subring R
The subring A 0 of R.
Equations
- SetLike.GradeZero.subring A = { carrier := ↑(A 0), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
instance
SetLike.GradeZero.instRing
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[Ring R]
[AddMonoid ι]
[SetLike σ R]
[AddSubgroupClass σ R]
(A : ι → σ)
[SetLike.GradedMonoid A]
:
Ring ↥(A 0)
The ring A 0 inherited from R in the presence of SetLike.GradedMonoid A.
Equations
- SetLike.GradeZero.instRing A = (SetLike.GradeZero.subring A).toRing
theorem
SetLike.GradeZero.coe_intCast
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[Ring R]
[AddMonoid ι]
[SetLike σ R]
[AddSubgroupClass σ R]
(A : ι → σ)
[SetLike.GradedMonoid A]
(z : ℤ)
:
↑↑z = ↑z
instance
SetLike.GradeZero.instCommRing
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[CommRing R]
[AddCommMonoid ι]
[SetLike σ R]
[AddSubgroupClass σ R]
(A : ι → σ)
[SetLike.GradedMonoid A]
:
CommRing ↥(A 0)
The commutative ring A 0 inherited from R in the presence of SetLike.GradedMonoid A.
Equations
- SetLike.GradeZero.instCommRing A = (SetLike.GradeZero.subring A).toCommRing
def
SetLike.GradeZero.subalgebra
{ι : Type u_1}
{S : Type u_3}
{R : Type u_4}
[CommSemiring S]
[Semiring R]
[Algebra S R]
[AddMonoid ι]
(A : ι → Submodule S R)
[SetLike.GradedMonoid A]
:
Subalgebra S R
The subalgebra A 0 of R.
Equations
- SetLike.GradeZero.subalgebra A = { carrier := ↑(A 0), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }
Instances For
instance
SetLike.GradeZero.instAlgebra
{ι : Type u_1}
{S : Type u_3}
{R : Type u_4}
[CommSemiring S]
[Semiring R]
[Algebra S R]
[AddMonoid ι]
(A : ι → Submodule S R)
[SetLike.GradedMonoid A]
:
Algebra S ↥(A 0)
The S-algebra A 0 inherited from R in the presence of SetLike.GradedMonoid A.
Equations
@[simp]
theorem
SetLike.GradeZero.coe_algebraMap
{ι : Type u_1}
{S : Type u_3}
{R : Type u_4}
[CommSemiring S]
[Semiring R]
[Algebra S R]
[AddMonoid ι]
(A : ι → Submodule S R)
[SetLike.GradedMonoid A]
(s : S)
:
↑((algebraMap S ↥(A 0)) s) = (algebraMap S R) s
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)