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 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 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)
[GradedOne A]
(s : S)
:
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 : ℕ)
:
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 : ℤ)
:
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
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
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
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
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
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
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))
:
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 : ι)
:
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)
:
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)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
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 : ι)
:
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)
:
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)
:
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)
:
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)
:
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)]
:
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)]
:
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
@[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)
:
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.
Equations
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]
:
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))
:
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]
:
The subsemiring A 0 of R.
Equations
Instances For
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
@[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 : ℕ)
:
@[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]
:
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
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
Instances For
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
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 : ℤ)
:
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
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
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)
[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)
[GradedMonoid A]
(s : 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
@[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))
:
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 : 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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
: