Mathlib.Data.DFinsupp.Submonoid

Module docstring

{"# 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. "}

dfinsuppProd_mem theorem

 [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {S : Type*} [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

Full source

@[to_additive]
theorem dfinsuppProd_mem [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
    [CommMonoid γ] {S : Type*} [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 :=
  prod_mem fun _ hi => h _ <| mem_support_iff.1 hi

Product of Finitely Supported Function Values Lies in Submonoid Under Pointwise Condition

Informal description

Let $\{\beta_i\}_{i \in \iota}$ be a family of types each equipped with a zero element and a decidable equality on non-zero elements, and let $\gamma$ be a commutative monoid. Given a submonoid $s$ of $\gamma$ (represented as a set-like structure with `SubmonoidClass`), a finitely supported dependent function $f \colon \Pi_{i} \beta_i$, and a family of functions $g_i \colon \beta_i \to \gamma$, if for every index $c$ where $f_c \neq 0$ we have $g_c(f_c) \in s$, then the product $\prod_{i \in \text{supp}(f)} g_i(f_i)$ belongs to $s$.

dfinsuppSumAddHom_mem theorem

 [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] {S : Type*} [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

Full source

theorem dfinsuppSumAddHom_mem [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] {S : Type*}
    [SetLike S γ] [AddSubmonoidClass S γ] (s : S) (f : Π₀ i, β i) (g : ∀ i, β i →+ γ)
    (h : ∀ c, f c ≠ 0 → g c (f c) ∈ s) : DFinsupp.sumAddHomDFinsupp.sumAddHom g f ∈ s := by
  classical
    rw [DFinsupp.sumAddHom_apply]
    exact dfinsuppSum_mem s f (g ·) h

Sum of Additive Homomorphisms over Finite Support Lies in Submonoid Under Pointwise Condition

Informal description

Let $\{\beta_i\}_{i \in I}$ be a family of additive zero classes, $\gamma$ an additive commutative monoid, and $S$ a set-like structure on $\gamma$ with `AddSubmonoidClass`. Given a submonoid $s \in S$, a finitely supported dependent function $f \in \Pi_{i} \beta_i$, and a family of additive monoid homomorphisms $g_i \colon \beta_i \to \gamma$, if for every index $c$ where $f_c \neq 0$ we have $g_c(f_c) \in s$, then the sum $\sum_{i} g_i(f_i)$ belongs to $s$.

AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom theorem

 [AddCommMonoid γ] (S : ι → AddSubmonoid γ) : iSup S = AddMonoidHom.mrange (DFinsupp.sumAddHom fun i => (S i).subtype)

Full source

/-- 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.iSup_eq_mrange_dfinsuppSumAddHom
    [AddCommMonoid γ] (S : ι → AddSubmonoid γ) :
    iSup S = AddMonoidHom.mrange (DFinsupp.sumAddHom fun i => (S i).subtype) := by
  apply le_antisymm
  · apply iSup_le _
    intro i y hy
    exact ⟨DFinsupp.single i ⟨y, hy⟩, DFinsupp.sumAddHom_single _ _ _⟩
  · rintro x ⟨v, rfl⟩
    exact dfinsuppSumAddHom_mem _ v _ fun i _ => (le_iSup S i : S i ≤ _) (v i).prop

Supremum of Additive Submonoids as Range of Summation Homomorphism

Informal description

Let $\gamma$ be an additive commutative monoid and $(S_i)_{i \in \iota}$ a family of additive submonoids of $\gamma$. The supremum of this family equals the range of the additive monoid homomorphism $\operatorname{sumAddHom} (\lambda i, (S_i).\text{subtype})$, where $(S_i).\text{subtype}$ denotes the inclusion map of $S_i$ into $\gamma$. In other words: \[ \bigsqcup_{i \in \iota} S_i = \text{range}\left(\sum_{i} (S_i \hookrightarrow \gamma)(f_i)\right) \] where the sum is taken over finitely supported functions $f \in \Pi_{i} S_i$.

AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom theorem

 (p : ι → Prop) [DecidablePred p] [AddCommMonoid γ] (S : ι → AddSubmonoid γ) :
  ⨆ (i) (_ : p i), S i = AddMonoidHom.mrange ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom _ p))

Full source

/-- 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.bsupr_eq_mrange_dfinsuppSumAddHom (p : ι → Prop) [DecidablePred p]
    [AddCommMonoid γ] (S : ι → AddSubmonoid γ) :
    ⨆ (i) (_ : p i), S i =
      AddMonoidHom.mrange ((sumAddHom fun i => (S i).subtype).comp (filterAddMonoidHom _ p)) := by
  apply le_antisymm
  · refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩
    rw [AddMonoidHom.comp_apply, filterAddMonoidHom_apply, filter_single_pos _ _ hi]
    exact sumAddHom_single _ _ _
  · rintro x ⟨v, rfl⟩
    refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_
    refine AddSubmonoid.mem_iSup_of_mem i ?_
    by_cases hp : p i
    · simp [hp]
    · simp [hp]

Bounded Supremum of Additive Submonoids as Range of Filtered Sum Homomorphism

Informal description

Let $\gamma$ be an additive commutative monoid, $S \colon \iota \to \text{AddSubmonoid} \gamma$ a family of additive submonoids indexed by $\iota$, and $p \colon \iota \to \text{Prop}$ a decidable predicate on $\iota$. The bounded supremum of the submonoids $S_i$ for which $p(i)$ holds is equal to the range of the composition of the sum of additive homomorphisms $\sum_{i} (S_i).\text{subtype}$ with the filter homomorphism for $p$. In other words, \[ \bigsqcup_{\substack{i \\ p(i)}} S_i = \text{range} \left( \left( \sum_{i} (S_i).\text{subtype} \right) \circ \text{filter}_p \right). \]

AddSubmonoid.mem_iSup_iff_exists_dfinsupp theorem

 [AddCommMonoid γ] (S : ι → AddSubmonoid γ) (x : γ) :
  x ∈ iSup S ↔ ∃ f : Π₀ i, S i, DFinsupp.sumAddHom (fun i => (S i).subtype) f = x

Full source

theorem AddSubmonoid.mem_iSup_iff_exists_dfinsupp [AddCommMonoid γ] (S : ι → AddSubmonoid γ)
    (x : γ) : x ∈ iSup Sx ∈ iSup S ↔ ∃ f : Π₀ i, S i, DFinsupp.sumAddHom (fun i => (S i).subtype) f = x :=
  SetLike.ext_iff.mp (AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom S) x

Characterization of Supremum Membership via Finitely Supported Sums in Additive Submonoids

Informal description

Let $\gamma$ be an additive commutative monoid and $(S_i)_{i \in \iota}$ a family of additive submonoids of $\gamma$. An element $x \in \gamma$ belongs to the supremum $\bigsqcup_{i \in \iota} S_i$ if and only if there exists a finitely supported dependent function $f \in \Pi_{i} S_i$ such that the sum of the images of $f_i$ under the inclusion maps $S_i \hookrightarrow \gamma$ equals $x$. In other words: \[ x \in \bigsqcup_{i \in \iota} S_i \iff \exists f \in \Pi_{i} S_i \text{ with finite support}, \sum_{i} f_i = x. \]

AddSubmonoid.mem_iSup_iff_exists_dfinsupp' theorem

 [AddCommMonoid γ] (S : ι → AddSubmonoid γ) [∀ (i) (x : S i), Decidable (x ≠ 0)] (x : γ) :
  x ∈ iSup S ↔ ∃ f : Π₀ i, S i, (f.sum fun _ xi => ↑xi) = x

Full source

/-- A variant of `AddSubmonoid.mem_iSup_iff_exists_dfinsupp` with the RHS fully unfolded. -/
theorem AddSubmonoid.mem_iSup_iff_exists_dfinsupp' [AddCommMonoid γ] (S : ι → AddSubmonoid γ)
    [∀ (i) (x : S i), Decidable (x ≠ 0)] (x : γ) :
    x ∈ iSup Sx ∈ iSup S ↔ ∃ f : Π₀ i, S i, (f.sum fun _ xi => ↑xi) = x := by
  rw [AddSubmonoid.mem_iSup_iff_exists_dfinsupp]
  simp_rw [sumAddHom_apply]
  rfl

Supremum Membership via Finite Sums in Additive Submonoids (Decidable Zero Variant)

Informal description

Let $\gamma$ be an additive commutative monoid and $(S_i)_{i \in \iota}$ a family of additive submonoids of $\gamma$, where for each $i$ and $x \in S_i$ it is decidable whether $x \neq 0$. An element $x \in \gamma$ belongs to the supremum $\bigsqcup_{i \in \iota} S_i$ if and only if there exists a finitely supported dependent function $f \in \Pi_{i} S_i$ such that the sum of the coefficients of $f$ equals $x$. In other words: \[ x \in \bigsqcup_{i \in \iota} S_i \iff \exists f \in \Pi_{i} S_i \text{ with finite support}, \sum_{i} f_i = x. \]

AddSubmonoid.mem_bsupr_iff_exists_dfinsupp theorem

 (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) (f.filter p) = x

Full source

theorem AddSubmonoid.mem_bsupr_iff_exists_dfinsupp (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) (f.filter p) = x :=
  SetLike.ext_iff.mp (AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom p S) x

Characterization of Elements in Bounded Supremum of Additive Submonoids via Finite Sums

Informal description

Let $\gamma$ be an additive commutative monoid, $S \colon \iota \to \text{AddSubmonoid} \gamma$ a family of additive submonoids indexed by $\iota$, and $p \colon \iota \to \text{Prop}$ a decidable predicate on $\iota$. For any element $x \in \gamma$, we have that $x$ belongs to the bounded supremum $\bigsqcup_{\substack{i \\ p(i)}} S_i$ if and only if there exists a dependently-typed function $f \colon \Pi_{i} S_i$ with finite support such that the sum of the inclusions $(S_i).\text{subtype}$ applied to the filtered function $f.\text{filter}(p)$ equals $x$. In other words, \[ x \in \bigsqcup_{\substack{i \\ p(i)}} S_i \iff \exists f \in \Pi_{i} S_i \text{ with finite support}, \left( \sum_{i} (S_i).\text{subtype} \right)(f.\text{filter}(p)) = x. \]