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 iSupIndep (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 to
  • SetLike.GradeZero.instSemiring
  • SetLike.GradeZero.instCommSemiring
• SetLike.GradeZero.subring, which leads to
  • SetLike.GradeZero.instRing
  • SetLike.GradeZero.instCommRing
• SetLike.GradeZero.subalgebra, which leads to
  • SetLike.GradeZero.instAlgebra

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) [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 : ι → σ) [GradedOne A] (n : ℕ) : ↑n ∈ A 0

theorem SetLike.intCast_mem_graded {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Zero ι] [AddGroupWithOne R] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) [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 : ι → σ) [GradedMul A] : DirectSum.GNonUnitalNonAssocSemiring fun (i : ι) => ↥(A i)

Build a DirectSum.GNonUnitalNonAssocSemiring instance for a collection of additive submonoids.

Equations

• SetLike.gnonUnitalNonAssocSemiring A = { toGMul := SetLike.gMul A, mul_zero := ⋯, zero_mul := ⋯, mul_add := ⋯, add_mul := ⋯ }

instance SetLike.gsemiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddMonoid ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [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 : ι → σ) [GradedMonoid A] : DirectSum.GCommSemiring fun (i : ι) => ↥(A i)

Build a DirectSum.GCommSemiring instance for a collection of additive submonoids.

Equations

• One or more equations did not get rendered due to their size.

instance SetLike.gring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddMonoid ι] [Ring R] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) [GradedMonoid A] : DirectSum.GRing fun (i : ι) => ↥(A i)

Build a DirectSum.GRing instance for a collection of additive subgroups.

Equations

• SetLike.gring A = { toGSemiring := SetLike.gsemiring A, intCast := fun (z : ℤ) => ⟨↑z, ⋯⟩, intCast_ofNat := ⋯, intCast_negSucc_ofNat := ⋯ }

instance SetLike.gcommRing {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddCommMonoid ι] [CommRing R] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) [GradedMonoid A] : DirectSum.GCommRing fun (i : ι) => ↥(A i)

Build a DirectSum.GCommRing instance for a collection of additive submonoids.

Equations

• One or more equations did not get rendered due to their size.

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)) : (coeRingHom A) ((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 ∈ DFinsupp.support r ×ˢ DFinsupp.support r' with ij.1 + ij.2 = n, ↑(r ij.1) * ↑(r' ij.2)

theorem DirectSum.coe_mul_apply_eq_dfinsuppSum {ι : 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

@[deprecated DirectSum.coe_mul_apply_eq_dfinsuppSum (since := "2025-04-06")]

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

Alias of DirectSum.coe_mul_apply_eq_dfinsuppSum.

theorem DirectSum.coe_mul_apply_eq_sum_antidiagonal {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddMonoid ι] [Finset.HasAntidiagonal ι] [SetLike.GradedMonoid A] (r r' : DirectSum ι fun (i : ι) => ↥(A i)) (n : ι) : ↑((r * r') n) = ∑ ij ∈ Finset.antidiagonal n, ↑(r ij.1) * ↑(r' ij.2)

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) : ↑(((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 * (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 : ι) : ↑(((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 * (of (fun (i : ι) => ↥(A i)) i) r') (j + i)) = ↑(r j) * ↑r'

theorem DirectSum.coe_of_mul_apply_of_mem_zero {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [AddMonoid ι] [SetLike.GradedMonoid A] (r : ↥(A 0)) (r' : DirectSum ι fun (i : ι) => ↥(A i)) (j : ι) : ↑(((of (fun (i : ι) => ↥(A i)) 0) r * r') j) = ↑r * ↑(r' j)

theorem DirectSum.coe_mul_of_apply_of_mem_zero {ι : 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)) (r' : ↥(A 0)) (j : ι) : ↑((r * (of (fun (i : ι) => ↥(A i)) 0) r') j) = ↑(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 : ι → σ) [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike.GradedMonoid A] {i : ι} (r : ↥(A i)) (r' : DirectSum ι fun (i : ι) => ↥(A i)) (n : ι) (h : ¬i ≤ n) : ↑(((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 : ι → σ) [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike.GradedMonoid A] (r : DirectSum ι fun (i : ι) => ↥(A i)) {i : ι} (r' : ↥(A i)) (n : ι) (h : ¬i ≤ n) : ↑((r * (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 : ι → σ) [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike.GradedMonoid A] [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (r : DirectSum ι fun (i : ι) => ↥(A i)) {i : ι} (r' : ↥(A i)) (n : ι) (h : i ≤ n) : ↑((r * (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 : ι → σ) [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike.GradedMonoid A] [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] {i : ι} (r : ↥(A i)) (r' : DirectSum ι fun (i : ι) => ↥(A i)) (n : ι) (h : i ≤ n) : ↑(((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 : ι → σ) [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike.GradedMonoid A] [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] (r : DirectSum ι fun (i : ι) => ↥(A i)) {i : ι} (r' : ↥(A i)) (n : ι) [Decidable (i ≤ n)] : ↑((r * (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 : ι → σ) [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike.GradedMonoid A] [Sub ι] [OrderedSub ι] [AddLeftReflectLE ι] {i : ι} (r : ↥(A i)) (r' : DirectSum ι fun (i : ι) => ↥(A i)) (n : ι) [Decidable (i ≤ n)] : ↑(((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} [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.

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 : ι) => (A i).subtype) ⋯ ⋯

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)) : (coeAlgHom A) ((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 : ι → σ) [GradedMonoid A] : Subsemiring R

The subsemiring A 0 of R.

Equations

• SetLike.GradeZero.subsemiring A = { carrier := ↑(A 0), mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

instance SetLike.GradeZero.instSemiring {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Semiring R] [AddMonoid ι] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [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 : ι → σ) [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 : ι → σ) [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] [AddMonoid ι] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ) [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 : ι → σ) [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' := ⋯ }

instance SetLike.GradeZero.instRing {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [Ring R] [AddMonoid ι] [SetLike σ R] [AddSubgroupClass σ R] (A : ι → σ) [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 : ι → σ) [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 : ι → σ) [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) [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' := ⋯ }

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) [GradedMonoid A] : Algebra S ↥(A 0)

The S-algebra A 0 inherited from R in the presence of SetLike.GradedMonoid A.

Equations

• SetLike.GradeZero.instAlgebra A = inferInstanceAs (Algebra S ↥(SetLike.GradeZero.subalgebra A))

@[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) [GradedMonoid A] (s : S) : ↑((algebraMap S ↥(A 0)) s) = (algebraMap S R) s

instance SetLike.GradeZero.instAlgebraSubtypeMemSubmoduleOfNat {ι : Type u_1} {S : Type u_3} {R : Type u_4} [CommSemiring S] [CommSemiring R] [Algebra S R] [AddCommMonoid ι] (A : ι → Submodule S R) [GradedMonoid A] : Algebra (↥(A 0)) R

Equations

• SetLike.GradeZero.instAlgebraSubtypeMemSubmoduleOfNat A = (SetLike.GradeZero.subalgebra A).toAlgebra

@[simp]

theorem SetLike.GradeZero.algebraMap_apply {ι : Type u_1} {S : Type u_3} {R : Type u_4} [CommSemiring S] [CommSemiring R] [Algebra S R] [AddCommMonoid ι] (A : ι → Submodule S R) [GradedMonoid A] (x : ↥(A 0)) : (algebraMap (↥(A 0)) R) 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) : IsHomogeneousElem 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 : IsHomogeneousElem A r) : IsHomogeneousElem A (s • r)

Gradings by canonically linearly ordered additive monoids

theorem mul_apply_eq_zero {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddCommMonoid ι] [LinearOrder ι] [IsOrderedAddMonoid ι] [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] {A : ι → σ} [SetLike.GradedMonoid A] {r r' : DirectSum ι fun (i : ι) => ↥(A i)} {m n : ι} (hr : ∀ i < m, r i = 0) (hr' : ∀ i < n, r' i = 0) ⦃k : ι⦄ (hk : k < m + n) : (r * r') k = 0

theorem listProd_apply_eq_zero' {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddCommMonoid ι] [LinearOrder ι] [IsOrderedAddMonoid ι] [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] {A : ι → σ} [SetLike.GradedMonoid A] [CanonicallyOrderedAdd ι] {l : List ((DirectSum ι fun (i : ι) => ↥(A i)) × ι)} (hl : ∀ xn ∈ l, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < (List.map Prod.snd l).sum) : (List.map Prod.fst l).prod n = 0

The difference with DirectSum.listProd_apply_eq_zero is that the indices at which the terms of the list are zero is allowed to vary.

theorem listProd_apply_eq_zero {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddCommMonoid ι] [LinearOrder ι] [IsOrderedAddMonoid ι] [DecidableEq ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] {A : ι → σ} [SetLike.GradedMonoid A] [CanonicallyOrderedAdd ι] {l : List (DirectSum ι fun (i : ι) => ↥(A i))} {m : ι} (hl : ∀ x ∈ l, ∀ k < m, x k = 0) ⦃n : ι⦄ (hn : n < l.length • m) : l.prod n = 0

theorem multisetProd_apply_eq_zero' {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddCommMonoid ι] [LinearOrder ι] [IsOrderedAddMonoid ι] [DecidableEq ι] [CanonicallyOrderedAdd ι] [CommSemiring R] [SetLike σ R] [AddSubmonoidClass σ R] {A : ι → σ} [SetLike.GradedMonoid A] {s : Multiset ((DirectSum ι fun (i : ι) => ↥(A i)) × ι)} (hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < (Multiset.map Prod.snd s).sum) : (Multiset.map Prod.fst s).prod n = 0

The difference with DirectSum.multisetProd_apply_eq_zero is that the indices at which the terms of the multiset are zero is allowed to vary.

theorem multisetProd_apply_eq_zero {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddCommMonoid ι] [LinearOrder ι] [IsOrderedAddMonoid ι] [DecidableEq ι] [CanonicallyOrderedAdd ι] [CommSemiring R] [SetLike σ R] [AddSubmonoidClass σ R] {A : ι → σ} [SetLike.GradedMonoid A] {s : Multiset (DirectSum ι fun (i : ι) => ↥(A i))} {m : ι} (hs : ∀ x ∈ s, ∀ k < m, x k = 0) ⦃n : ι⦄ (hn : n < s.card • m) : s.prod n = 0

theorem finsetProd_apply_eq_zero' {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddCommMonoid ι] [LinearOrder ι] [IsOrderedAddMonoid ι] [DecidableEq ι] [CanonicallyOrderedAdd ι] [CommSemiring R] [SetLike σ R] [AddSubmonoidClass σ R] {A : ι → σ} [SetLike.GradedMonoid A] {s : Finset ((DirectSum ι fun (i : ι) => ↥(A i)) × ι)} (hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < ∑ xn ∈ s, xn.2) : (∏ xn ∈ s, xn.1) n = 0

The difference with DirectSum.finsetProd_apply_eq_zero is that the indices at which the terms of the multiset are zero is allowed to vary.

theorem finsetProd_apply_eq_zero {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [AddCommMonoid ι] [LinearOrder ι] [IsOrderedAddMonoid ι] [DecidableEq ι] [CanonicallyOrderedAdd ι] [CommSemiring R] [SetLike σ R] [AddSubmonoidClass σ R] {A : ι → σ} [SetLike.GradedMonoid A] {s : Finset (DirectSum ι fun (i : ι) => ↥(A i))} {m : ι} (hs : ∀ x ∈ s, ∀ k < m, x k = 0) ⦃n : ι⦄ (hn : n < s.card • m) : (∏ x ∈ s, x) n = 0