DFinsupp and submonoids

This file mainly concerns the interaction between submonoids and products/sums of DFinsupps.

Main results

• AddSubmonoid.mem_iSup_iff_exists_dfinsupp: elements of the supremum of additive commutative monoids can be given by taking finite sums of elements of each monoid.
• AddSubmonoid.mem_bsupr_iff_exists_dfinsupp: elements of the supremum of additive commutative monoids can be given by taking finite sums of elements of each monoid.

theorem dfinsuppProd_mem {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {S : Type u_1} [SetLike S γ] [SubmonoidClass S γ] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → γ) (h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ s) : f.prod g ∈ s

theorem dfinsuppSum_mem {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [AddCommMonoid γ] {S : Type u_1} [SetLike S γ] [AddSubmonoidClass S γ] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → γ) (h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ s) : f.sum g ∈ s

@[deprecated dfinsuppProd_mem (since := "2025-04-06")]

theorem dfinsupp_prod_mem {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] [CommMonoid γ] {S : Type u_1} [SetLike S γ] [SubmonoidClass S γ] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → γ) (h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ s) : f.prod g ∈ s

Alias of dfinsuppProd_mem.

theorem dfinsuppSumAddHom_mem {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] {S : Type u_1} [SetLike S γ] [AddSubmonoidClass S γ] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ γ) (h : ∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s) : (DFinsupp.sumAddHom g) f ∈ s

@[deprecated dfinsuppSumAddHom_mem (since := "2025-04-06")]

theorem dfinsupp_sumAddHom_mem {ι : Type u} {γ : Type w} {β : ι → Type v} [DecidableEq ι] [(i : ι) → AddZeroClass (β i)] [AddCommMonoid γ] {S : Type u_1} [SetLike S γ] [AddSubmonoidClass S γ] (s : S) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ γ) (h : ∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s) : (DFinsupp.sumAddHom g) f ∈ s

Alias of dfinsuppSumAddHom_mem.

theorem AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom {ι : Type u} {γ : Type w} [DecidableEq ι] [AddCommMonoid γ] (S : ι → AddSubmonoid γ) : iSup S = AddMonoidHom.mrange (DFinsupp.sumAddHom fun (i : ι) => (S i).subtype)

The supremum of a family of commutative additive submonoids is equal to the range of DFinsupp.sumAddHom; that is, every element in the iSup can be produced from taking a finite number of non-zero elements of S i, coercing them to γ, and summing them.

theorem AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom {ι : Type u} {γ : Type w} [DecidableEq ι] (p : ι → Prop) [DecidablePred p] [AddCommMonoid γ] (S : ι → AddSubmonoid γ) : ⨆ (i : ι), ⨆ (_ : p i), S i = AddMonoidHom.mrange ((DFinsupp.sumAddHom fun (i : ι) => (S i).subtype).comp (DFinsupp.filterAddMonoidHom (fun (i : ι) => ↥(S i)) p))

The bounded supremum of a family of commutative additive submonoids is equal to the range of DFinsupp.sumAddHom composed with DFinsupp.filterAddMonoidHom; that is, every element in the bounded iSup can be produced from taking a finite number of non-zero elements from the S i that satisfy p i, coercing them to γ, and summing them.

@[deprecated AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom (since := "2025-04-06")]

theorem AddSubmonoid.bsupr_eq_mrange_dfinsupp_sumAddHom {ι : Type u} {γ : Type w} [DecidableEq ι] (p : ι → Prop) [DecidablePred p] [AddCommMonoid γ] (S : ι → AddSubmonoid γ) : ⨆ (i : ι), ⨆ (_ : p i), S i = AddMonoidHom.mrange ((DFinsupp.sumAddHom fun (i : ι) => (S i).subtype).comp (DFinsupp.filterAddMonoidHom (fun (i : ι) => ↥(S i)) p))

Alias of AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom.

---

The bounded supremum of a family of commutative additive submonoids is equal to the range of DFinsupp.sumAddHom composed with DFinsupp.filterAddMonoidHom; that is, every element in the bounded iSup can be produced from taking a finite number of non-zero elements from the S i that satisfy p i, coercing them to γ, and summing them.

theorem AddSubmonoid.mem_iSup_iff_exists_dfinsupp {ι : Type u} {γ : Type w} [DecidableEq ι] [AddCommMonoid γ] (S : ι → AddSubmonoid γ) (x : γ) : x ∈ iSup S ↔ ∃ (f : Π₀ (i : ι), ↥(S i)), (DFinsupp.sumAddHom fun (i : ι) => (S i).subtype) f = x

theorem AddSubmonoid.mem_iSup_iff_exists_dfinsupp' {ι : Type u} {γ : Type w} [DecidableEq ι] [AddCommMonoid γ] (S : ι → AddSubmonoid γ) [(i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)] (x : γ) : x ∈ iSup S ↔ ∃ (f : Π₀ (i : ι), ↥(S i)), (f.sum fun (x : ι) (xi : ↥(S x)) => ↑xi) = x

A variant of AddSubmonoid.mem_iSup_iff_exists_dfinsupp with the RHS fully unfolded.

theorem AddSubmonoid.mem_bsupr_iff_exists_dfinsupp {ι : Type u} {γ : Type w} [DecidableEq ι] (p : ι → Prop) [DecidablePred p] [AddCommMonoid γ] (S : ι → AddSubmonoid γ) (x : γ) : x ∈ ⨆ (i : ι), ⨆ (_ : p i), S i ↔ ∃ (f : Π₀ (i : ι), ↥(S i)), (DFinsupp.sumAddHom fun (i : ι) => (S i).subtype) (DFinsupp.filter p f) = x