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 ↥(A i)
Equations
- AddCommMonoid.ofSubmonoidOnSemiring A i = inferInstance
instance
AddCommGroup.ofSubgroupOnRing
{ι : Type u_1}
{σ : Type u_2}
{R : Type u_4}
[Ring R]
[SetLike σ R]
[AddSubgroupClass σ R]
(A : ι → σ)
(i : ι)
:
AddCommGroup ↥(A i)
Equations
- AddCommGroup.ofSubgroupOnRing A i = inferInstance
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 : ι) => ↥(A i)
Build a DirectSum.GNonUnitalNonAssocSemiring instance for a collection of additive
submonoids.
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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
- SetLike.gcommSemiring A = let src := SetLike.gCommMonoid A; let src_1 := SetLike.gsemiring A; DirectSum.GCommSemiring.mk (_ : ∀ (a b : GradedMonoid fun (i : ι) => ↥(A i)), a * b = b * a)
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
- One or more equations did not get rendered due to their size.
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
- SetLike.gcommRing A = let src := SetLike.gCommMonoid A; let src_1 := SetLike.gring A; DirectSum.GCommRing.mk (_ : ∀ (a b : GradedMonoid fun (i : ι) => ↥(A i)), a * b = b * a)
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
- One or more equations did not get rendered due to their size.
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 : DirectSum ι fun (i : ι) => ↥(A i))
(r' : DirectSum ι fun (i : ι) => ↥(A i))
(n : ι)
:
↑((r * r') n) = Finset.sum (Finset.filter (fun (ij : ι × ι) => ij.1 + ij.2 = n) (DFinsupp.support r ×ˢ DFinsupp.support r'))
fun (ij : ι × ι) => ↑(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 : DirectSum ι fun (i : ι) => ↥(A i))
(r' : DirectSum ι fun (i : ι) => ↥(A i))
(n : ι)
:
↑((r * r') n) = DFinsupp.sum r fun (i : ι) (ri : (fun (i : ι) => ↥(A i)) i) =>
DFinsupp.sum r' fun (j : ι) (rj : (fun (i : ι) => ↥(A i)) 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 ι]
[ContravariantClass ι ι (fun (x x_1 : ι) => x + x_1) fun (x x_1 : ι) => x ≤ x_1]
(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 ι]
[ContravariantClass ι ι (fun (x x_1 : ι) => x + x_1) fun (x x_1 : ι) => x ≤ x_1]
{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 ι]
[ContravariantClass ι ι (fun (x x_1 : ι) => x + x_1) fun (x x_1 : ι) => x ≤ x_1]
(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 ι]
[ContravariantClass ι ι (fun (x x_1 : ι) => x + x_1) fun (x x_1 : ι) => x ≤ x_1]
{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}
[DecidableEq ι]
[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
- One or more equations did not get rendered due to their size.
@[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.
Equations
- (_ : SetLike.GradedMonoid fun (i : ℕ) => p ^ i) = (_ : SetLike.GradedMonoid fun (i : ℕ) => p ^ i)
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
- One or more equations did not get rendered due to their size.
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 : ↥(A i))
:
(DirectSum.coeAlgHom A) ((DirectSum.of (fun (i : ι) => ↥(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)