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:

• SetLike.gnonUnitalNonAssocSemiring
• SetLike.gsemiring
• SetLike.gcommSemiring

With these instances in place, it provides the bundled canonical maps out of a direct sum of subobjects into their carrier type:

• DirectSum.coeRingHom (a RingHom version of DirectSum.coeAddMonoidHom)
• DirectSum.coeAlgHom (an AlgHom version of DirectSum.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

• SetLike.gnonUnitalNonAssocSemiring A = let __src := SetLike.gMul A; DirectSum.GNonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

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 = let __src := SetLike.gMonoid A; DirectSum.GSemiring.mk ⋯ ⋯ ⋯ GradedMonoid.GMonoid.gnpow ⋯ ⋯ (fun (n : ℕ) => { val := ↑n, property := ⋯ }) ⋯ ⋯

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 ⋯

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 = let __src := SetLike.gsemiring A; DirectSum.GRing.mk (fun (z : ℤ) => { val := ↑z, property := ⋯ }) ⋯ ⋯

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 ⋯

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] : (DirectSum ι fun (i : ι) => ↥(A i)) →+* R

The canonical ring isomorphism between ⨁ i, A i and R

Equations

• DirectSum.coeRingHom A = DirectSum.toSemiring (fun (i : ι) => AddSubmonoidClass.subtype (A i)) ⋯ ⋯

@[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)] : ↑((r * (DirectSum.of (fun (i : ι) => ↥(A i)) i) r') n) = if i ≤ n then ↑(r (n - i)) * ↑r' else 0

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)] : ↑(((DirectSum.of (fun (i : ι) => ↥(A i)) i) r * r') n) = if i ≤ n then ↑r * ↑(r' (n - i)) else 0

From Submodules

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

• Submodule.galgebra A = { toFun := LinearMap.toAddMonoidHom (LinearMap.codRestrict (A 0) (Algebra.linearMap S R) ⋯), map_one := ⋯, map_mul := ⋯, commutes := ⋯, smul_def := ⋯ }

@[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

• ⋯ = ⋯

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] : (DirectSum ι fun (i : ι) => ↥(A i)) →ₐ[S] R

The canonical algebra isomorphism between ⨁ i, A i and R.

Equations

• DirectSum.coeAlgHom A = DirectSum.toAlgebra S (fun (i : ι) => ↥(A i)) (fun (i : ι) => Submodule.subtype (A i)) ⋯ ⋯

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) : SetLike.Homogeneous A 0

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)