Mathlib.Algebra.Ring.Submonoid.Pointwise

AddSubmonoid.one definition

: One (AddSubmonoid R)

Full source

/-- If `R` is an additive monoid with one (e.g., a semiring), then `1 : AddSubmonoid R` is the range
of `Nat.cast : ℕ → R`. -/
protected def one : One (AddSubmonoid R) := ⟨AddMonoidHom.mrange (Nat.castAddMonoidHom R)⟩

Additive submonoid generated by natural numbers

Informal description

Given an additive monoid $R$ with a multiplicative identity (e.g., a semiring), the element $1$ in the additive submonoid of $R$ is defined as the range of the canonical homomorphism from the natural numbers to $R$, i.e., the set $\{ n \mid n \in \mathbb{N} \}$ where $n$ is interpreted in $R$ via the natural inclusion.

AddSubmonoid.one_eq_mrange theorem

: (1 : AddSubmonoid R) = AddMonoidHom.mrange (Nat.castAddMonoidHom R)

Full source

lemma one_eq_mrange : (1 : AddSubmonoid R) = AddMonoidHom.mrange (Nat.castAddMonoidHom R) := rfl

Additive Submonoid One as Range of Natural Number Homomorphism

Informal description

The additive submonoid $1$ in $R$ is equal to the range of the canonical homomorphism from the natural numbers to $R$, i.e., \[ (1 : \text{AddSubmonoid } R) = \text{range}(\text{Nat.castAddMonoidHom } R). \]

AddSubmonoid.natCast_mem_one theorem

(n : ℕ) : (n : R) ∈ (1 : AddSubmonoid R)

Full source

lemma natCast_mem_one (n : ℕ) : (n : R) ∈ (1 : AddSubmonoid R) := ⟨_, rfl⟩

Natural numbers belong to the additive submonoid generated by 1

Informal description

For any natural number $n$ and any additive monoid $R$ with a multiplicative identity, the element $n$ (interpreted in $R$ via the canonical homomorphism from $\mathbb{N}$ to $R$) belongs to the additive submonoid generated by the natural numbers in $R$.

AddSubmonoid.mem_one theorem

{x : R} : x ∈ (1 : AddSubmonoid R) ↔ ∃ n : ℕ, ↑n = x

Full source

@[simp] lemma mem_one {x : R} : x ∈ (1 : AddSubmonoid R)x ∈ (1 : AddSubmonoid R) ↔ ∃ n : ℕ, ↑n = x := .rfl

Characterization of Elements in the Additive Submonoid Generated by 1

Informal description

An element $x$ of an additive monoid $R$ belongs to the additive submonoid generated by the multiplicative identity if and only if there exists a natural number $n$ such that the canonical inclusion of $n$ into $R$ equals $x$. In other words: $$ x \in (1 : \text{AddSubmonoid } R) \leftrightarrow \exists n \in \mathbb{N}, n = x $$

AddSubmonoid.one_eq_closure theorem

: (1 : AddSubmonoid R) = closure { 1 }

Full source

lemma one_eq_closure : (1 : AddSubmonoid R) = closure {1} := by
  rw [closure_singleton_eq, one_eq_mrange]; congr 1; ext; simp

Additive Submonoid Generated by One Equals Closure of Singleton One

Informal description

The additive submonoid generated by the multiplicative identity $1$ in an additive monoid $R$ is equal to the closure of the singleton set $\{1\}$.

AddSubmonoid.one_eq_closure_one_set theorem

: (1 : AddSubmonoid R) = closure 1

Full source

lemma one_eq_closure_one_set : (1 : AddSubmonoid R) = closure 1 := one_eq_closure

Additive Submonoid Generated by One Equals Closure of Singleton One

Informal description

The additive submonoid generated by the multiplicative identity $1$ in an additive monoid $R$ is equal to the closure of the singleton set $\{1\}$ under addition.

AddSubmonoid.smul definition

: SMul (AddSubmonoid R) (AddSubmonoid A)

Full source

/-- For `M : Submonoid R` and `N : AddSubmonoid A`, `M • N` is the additive submonoid
generated by all `m • n` where `m ∈ M` and `n ∈ N`. -/
protected def smul : SMul (AddSubmonoid R) (AddSubmonoid A) where
  smul M N := ⨆ s : M, N.map (DistribSMul.toAddMonoidHom A s.1)

Scalar multiplication of additive submonoids

Informal description

Given a scalar type `R` and an additive monoid `A` with a distributive scalar multiplication operation `• : R → A → A`, the operation `SMul (AddSubmonoid R) (AddSubmonoid A)` is defined as follows: for any additive submonoids `M` of `R` and `N` of `A`, the scalar multiplication `M • N` is the additive submonoid of `A` generated by all elements of the form `m • n` where `m ∈ M` and `n ∈ N`. More precisely, `M • N` is the supremum (join) of the images of `N` under the additive monoid homomorphisms induced by scalar multiplication with each element `m ∈ M`. That is, \[ M • N = \bigsqcup_{m \in M} \{ m • n \mid n \in N \}. \]

AddSubmonoid.smul_mem_smul theorem

(hm : m ∈ M) (hn : n ∈ N) : m • n ∈ M • N

Full source

lemma smul_mem_smul (hm : m ∈ M) (hn : n ∈ N) : m • n ∈ M • N :=
  (le_iSup _ ⟨m, hm⟩ : _ ≤ M • N) ⟨n, hn, by rfl⟩

Scalar multiplication preserves membership in additive submonoids

Informal description

For any elements $m \in M$ and $n \in N$ of additive submonoids $M$ and $N$ respectively, the scalar product $m \bullet n$ belongs to the scalar product submonoid $M \bullet N$.

AddSubmonoid.smul_le theorem

: M • N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m • n ∈ P

Full source

lemma smul_le : M • N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m • n ∈ P :=
  ⟨fun H _m hm _n hn => H <| smul_mem_smul hm hn, fun H =>
    iSup_le fun ⟨m, hm⟩ => map_le_iff_le_comap.2 fun n hn => H m hm n hn⟩

Characterization of Scalar Product Submonoid Containment via Elementwise Condition

Informal description

For additive submonoids $M$ of $R$, $N$ of $A$, and $P$ of $A$, the scalar product submonoid $M \bullet N$ is contained in $P$ if and only if for every $m \in M$ and $n \in N$, the scalar product $m \bullet n$ belongs to $P$.

AddSubmonoid.smul_induction_on theorem

 {C : A → Prop} {a : A} (ha : a ∈ M • N) (hm : ∀ m ∈ M, ∀ n ∈ N, C (m • n)) (hadd : ∀ x y, C x → C y → C (x + y)) : C a

Full source

@[elab_as_elim]
protected lemma smul_induction_on {C : A → Prop} {a : A} (ha : a ∈ M • N)
    (hm : ∀ m ∈ M, ∀ n ∈ N, C (m • n)) (hadd : ∀ x y, C x → C y → C (x + y)) : C a :=
  (@smul_le _ _ _ _ _ _ _ ⟨⟨setOf C, hadd _ _⟩, by
    simpa only [smul_zero] using hm _ (zero_mem _) _ (zero_mem _)⟩).2 hm ha

Induction Principle for Scalar Product of Additive Submonoids

Informal description

Let $M$ be an additive submonoid of a scalar type $R$, $N$ an additive submonoid of an additive monoid $A$, and $C : A \to \mathrm{Prop}$ a predicate on $A$. For any element $a \in M \bullet N$, if: 1. For all $m \in M$ and $n \in N$, the predicate $C$ holds for the scalar product $m \bullet n$, and 2. For any $x, y \in A$, if $C(x)$ and $C(y)$ hold, then $C(x + y)$ holds, then $C(a)$ holds.

AddSubmonoid.addSubmonoid_smul_bot theorem

(S : AddSubmonoid R) : S • (⊥ : AddSubmonoid A) = ⊥

Full source

@[simp]
lemma addSubmonoid_smul_bot (S : AddSubmonoid R) : S • (⊥ : AddSubmonoid A) = ⊥ :=
  eq_bot_iff.2 <| smul_le.2 fun m _ n hn => by
    rw [AddSubmonoid.mem_bot] at hn ⊢; rw [hn, smul_zero]

Scalar multiplication with trivial submonoid yields trivial submonoid

Informal description

For any additive submonoid $S$ of $R$, the scalar multiplication of $S$ with the trivial additive submonoid $\bot$ of $A$ is equal to $\bot$, i.e., $S \bullet \bot = \bot$.

AddSubmonoid.smul_le_smul theorem

(h : M ≤ M') (hnp : N ≤ P) : M • N ≤ M' • P

Full source

lemma smul_le_smul (h : M ≤ M') (hnp : N ≤ P) : M • N ≤ M' • P :=
  smul_le.2 fun _m hm _n hn => smul_mem_smul (h hm) (hnp hn)

Monotonicity of Scalar Product for Additive Submonoids

Informal description

Let $M$ and $M'$ be additive submonoids of $R$, and $N$ and $P$ be additive submonoids of $A$. If $M \subseteq M'$ and $N \subseteq P$, then the scalar product submonoid $M \bullet N$ is contained in $M' \bullet P$.

AddSubmonoid.smul_le_smul_left theorem

(h : M ≤ M') : M • P ≤ M' • P

Full source

lemma smul_le_smul_left (h : M ≤ M') : M • P ≤ M' • P := smul_le_smul h le_rfl

Left Monotonicity of Scalar Product for Additive Submonoids

Informal description

Let $M$ and $M'$ be additive submonoids of $R$ such that $M \subseteq M'$, and let $P$ be an additive submonoid of $A$. Then the scalar product submonoid $M \bullet P$ is contained in $M' \bullet P$.

AddSubmonoid.smul_le_smul_right theorem

(h : N ≤ P) : M • N ≤ M • P

Full source

lemma smul_le_smul_right (h : N ≤ P) : M • N ≤ M • P := smul_le_smul le_rfl h

Right Monotonicity of Scalar Product for Additive Submonoids

Informal description

For additive submonoids $N$ and $P$ of an additive monoid $A$, if $N \subseteq P$, then for any additive submonoid $M$ of $R$, the scalar product submonoid $M \bullet N$ is contained in $M \bullet P$.

AddSubmonoid.smul_subset_smul theorem

: (↑M : Set R) • (↑N : Set A) ⊆ (↑(M • N) : Set A)

Full source

lemma smul_subset_smul : (↑M : Set R) • (↑N : Set A) ⊆ (↑(M • N) : Set A) :=
  smul_subset_iff.2 fun _i hi _j hj ↦ smul_mem_smul hi hj

Inclusion of Pointwise Product in Scalar Product Submonoid

Informal description

For additive submonoids $M$ of $R$ and $N$ of $A$, the pointwise scalar multiplication of their underlying sets is contained in the underlying set of their scalar product submonoid. That is, \[ M \cdot N \subseteq M \bullet N \] where $M \cdot N$ denotes the pointwise product $\{m \cdot n \mid m \in M, n \in N\}$ and $M \bullet N$ denotes the additive submonoid generated by these products.

AddSubmonoid.addSubmonoid_smul_sup theorem

: M • (N ⊔ P) = M • N ⊔ M • P

Full source

lemma addSubmonoid_smul_sup : M • (N ⊔ P) = M • N ⊔ M • P :=
  le_antisymm (smul_le.mpr fun m hm np hnp ↦ by
    refine closure_induction (motive := (fun _ ↦ _ • · ∈ _)) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp)
    · rintro x (hx | hx)
      exacts [le_sup_left (a := M • N) (smul_mem_smul hm hx),
        le_sup_right (a := M • N) (smul_mem_smul hm hx)]
    · apply (smul_zero (A := A) m).symm ▸ (M • N ⊔ M • P).zero_mem
    · intros _ _ _ _ h1 h2; rw [smul_add]; exact add_mem h1 h2)
  (sup_le (smul_le_smul_right le_sup_left) <| smul_le_smul_right le_sup_right)

Distributivity of Scalar Product over Supremum of Additive Submonoids

Informal description

For additive submonoids $M$ of $R$ and $N, P$ of $A$, the scalar product submonoid $M \bullet (N \sqcup P)$ is equal to the supremum of the scalar product submonoids $M \bullet N$ and $M \bullet P$, i.e., $$ M \bullet (N \sqcup P) = (M \bullet N) \sqcup (M \bullet P). $$

AddSubmonoid.smul_iSup theorem

(T : AddSubmonoid R) (S : ι → AddSubmonoid A) : (T • ⨆ i, S i) = ⨆ i, T • S i

Full source

lemma smul_iSup (T : AddSubmonoid R) (S : ι → AddSubmonoid A) : (T • ⨆ i, S i) = ⨆ i, T • S i :=
  le_antisymm (smul_le.mpr fun t ht s hs ↦ iSup_induction _ (motive := (t • · ∈ _)) hs
    (fun i s hs ↦ mem_iSup_of_mem i <| smul_mem_smul ht hs)
    (by simp_rw [smul_zero]; apply zero_mem) fun x y ↦ by simp_rw [smul_add]; apply add_mem)
  (iSup_le fun i ↦ smul_le_smul_right <| le_iSup _ i)

Distributivity of Scalar Multiplication over Supremum of Additive Submonoids

Informal description

Let $R$ be a type equipped with a scalar multiplication operation on an additive monoid $A$, and let $T$ be an additive submonoid of $R$. For any family of additive submonoids $(S_i)_{i \in \iota}$ of $A$, the scalar product submonoid $T \bullet \left( \bigsqcup_{i \in \iota} S_i \right)$ is equal to the supremum of the scalar product submonoids $\bigsqcup_{i \in \iota} (T \bullet S_i)$. In other words, scalar multiplication by $T$ distributes over the supremum of the family $(S_i)_{i \in \iota}$: $$ T \bullet \left( \bigsqcup_{i \in \iota} S_i \right) = \bigsqcup_{i \in \iota} (T \bullet S_i). $$

AddSubmonoid.mul definition

: Mul (AddSubmonoid R)

Full source

/-- Multiplication of additive submonoids of a semiring R. The additive submonoid `S * T` is the
smallest R-submodule of `R` containing the elements `s * t` for `s ∈ S` and `t ∈ T`. -/
protected def mul : Mul (AddSubmonoid R) := ⟨fun M N => ⨆ s : M, N.map (AddMonoidHom.mul s.1)⟩

Multiplication of additive submonoids

Informal description

The multiplication operation on additive submonoids of a semiring $R$ is defined as follows: for any additive submonoids $M$ and $N$ of $R$, their product $M * N$ is the smallest additive submonoid containing all elements of the form $m * n$ where $m \in M$ and $n \in N$. More precisely, $M * N$ is defined as the supremum (join) of the family of submonoids obtained by mapping $N$ under left multiplication by each element $s \in M$, i.e., $M * N = \bigsqcup_{s \in M} (N \text{ mapped by } s \cdot \_)$.

AddSubmonoid.mul_mem_mul theorem

{m n : R} (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N

Full source

lemma mul_mem_mul {m n : R} (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N := smul_mem_smul hm hn

Product of elements in additive submonoids remains in their product submonoid

Informal description

For any elements $m \in M$ and $n \in N$ of additive submonoids $M$ and $N$ in a semiring $R$, the product $m \cdot n$ belongs to the product submonoid $M \cdot N$.

AddSubmonoid.mul_le theorem

: M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P

Full source

lemma mul_le : M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P := smul_le

Containment Criterion for Product of Additive Submonoids

Informal description

For additive submonoids $M$, $N$, and $P$ of a semiring $R$, the product submonoid $M \cdot N$ is contained in $P$ if and only if for every $m \in M$ and $n \in N$, the product $m \cdot n$ belongs to $P$.

AddSubmonoid.mul_induction_on theorem

 {C : R → Prop} {r : R} (hr : r ∈ M * N) (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)) (ha : ∀ x y, C x → C y → C (x + y)) : C r

Full source

@[elab_as_elim]
protected lemma mul_induction_on {C : R → Prop} {r : R} (hr : r ∈ M * N)
    (hm : ∀ m ∈ M, ∀ n ∈ N, C (m * n)) (ha : ∀ x y, C x → C y → C (x + y)) : C r :=
  AddSubmonoid.smul_induction_on hr hm ha

Induction Principle for Products in Additive Submonoids

Informal description

Let $M$ and $N$ be additive submonoids of a semiring $R$, and let $C : R \to \mathrm{Prop}$ be a predicate on $R$. For any element $r \in M \cdot N$, if: 1. For all $m \in M$ and $n \in N$, the predicate $C$ holds for the product $m \cdot n$, and 2. For any $x, y \in R$, if $C(x)$ and $C(y)$ hold, then $C(x + y)$ holds, then $C(r)$ holds.

AddSubmonoid.closure_mul_closure theorem

(S T : Set R) : closure S * closure T = closure (S * T)

Full source

lemma closure_mul_closure (S T : Set R) : closure S * closure T = closure (S * T) := by
  apply le_antisymm
  · refine mul_le.2 fun a ha b hb => ?_
    rw [← AddMonoidHom.mulRight_apply, ← AddSubmonoid.mem_comap]
    refine (closure_le.2 fun a' ha' => ?_) ha
    change b ∈ (closure (S * T)).comap (AddMonoidHom.mulLeft a')
    refine (closure_le.2 fun b' hb' => ?_) hb
    change a' * b' ∈ closure (S * T)
    exact subset_closure (Set.mul_mem_mul ha' hb')
  · rw [closure_le]
    rintro _ ⟨a, ha, b, hb, rfl⟩
    exact mul_mem_mul (subset_closure ha) (subset_closure hb)

Closure of Product of Sets Equals Product of Closures for Additive Submonoids

Informal description

For any subsets $S$ and $T$ of a semiring $R$, the product of the additive submonoids generated by $S$ and $T$ equals the additive submonoid generated by the pointwise product set $S \cdot T = \{s \cdot t \mid s \in S, t \in T\}$. In symbols: $$\langle S \rangle \cdot \langle T \rangle = \langle S \cdot T \rangle$$ where $\langle \cdot \rangle$ denotes the additive submonoid closure operation.

AddSubmonoid.mul_eq_closure_mul_set theorem

(M N : AddSubmonoid R) : M * N = closure (M * N : Set R)

Full source

lemma mul_eq_closure_mul_set (M N : AddSubmonoid R) : M * N = closure (M * N : Set R) := by
  rw [← closure_mul_closure, closure_eq, closure_eq]

Product of Additive Submonoids as Closure of Pointwise Product

Informal description

For any additive submonoids $M$ and $N$ of a non-unital non-associative semiring $R$, the product $M \cdot N$ is equal to the additive submonoid generated by the pointwise product set $\{m \cdot n \mid m \in M, n \in N\}$.

AddSubmonoid.mul_bot theorem

(S : AddSubmonoid R) : S * ⊥ = ⊥

Full source

@[simp] lemma mul_bot (S : AddSubmonoid R) : S * ⊥ = ⊥ := addSubmonoid_smul_bot S

Multiplication of Additive Submonoid with Trivial Submonoid Yields Trivial Submonoid

Informal description

For any additive submonoid $S$ of a non-unital non-associative semiring $R$, the product of $S$ with the trivial additive submonoid $\bot$ is equal to $\bot$, i.e., $S \cdot \bot = \bot$.

AddSubmonoid.bot_mul theorem

(S : AddSubmonoid R) : ⊥ * S = ⊥

Full source

@[simp]
lemma bot_mul (S : AddSubmonoid R) : ⊥ * S = ⊥ :=
  eq_bot_iff.2 <| mul_le.2 fun m hm n _ => by rw [AddSubmonoid.mem_bot] at hm ⊢; rw [hm, zero_mul]

Product with Bottom Additive Submonoid is Bottom

Informal description

For any additive submonoid $S$ of a semiring $R$, the product of the bottom additive submonoid $\bot$ with $S$ is equal to $\bot$.

AddSubmonoid.mul_le_mul theorem

(hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q

Full source

@[mono, gcongr] lemma mul_le_mul (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q := smul_le_smul hmp hnq

Monotonicity of Submonoid Multiplication under Inclusion

Informal description

For additive submonoids $M, N, P, Q$ of a non-unital non-associative semiring $R$, if $M \subseteq P$ and $N \subseteq Q$, then the product submonoid $M * N$ is contained in $P * Q$.

AddSubmonoid.mul_le_mul_left theorem

(h : M ≤ N) : M * P ≤ N * P

Full source

@[gcongr] lemma mul_le_mul_left (h : M ≤ N) : M * P ≤ N * P := smul_le_smul_left h

Left Monotonicity of Additive Submonoid Multiplication

Informal description

For additive submonoids $M$, $N$, and $P$ of a non-unital non-associative semiring $R$, if $M$ is contained in $N$, then the product submonoid $M * P$ is contained in $N * P$.

AddSubmonoid.mul_le_mul_right theorem

(h : N ≤ P) : M * N ≤ M * P

Full source

@[gcongr] lemma mul_le_mul_right (h : N ≤ P) : M * N ≤ M * P := smul_le_smul_right h

Right Monotonicity of Additive Submonoid Multiplication

Informal description

For additive submonoids $M, N, P$ of a non-unital non-associative semiring $R$, if $N$ is contained in $P$, then the product submonoid $M * N$ is contained in $M * P$.

AddSubmonoid.mul_subset_mul theorem

: (↑M : Set R) * (↑N : Set R) ⊆ (↑(M * N) : Set R)

Full source

lemma mul_subset_mul : (↑M : Set R) * (↑N : Set R) ⊆ (↑(M * N) : Set R) := smul_subset_smul

Inclusion of Pointwise Product in Additive Submonoid Product

Informal description

For additive submonoids $M$ and $N$ of a semiring $R$, the pointwise product of their underlying sets is contained in the underlying set of their product submonoid. That is, \[ M \cdot N \subseteq M * N \] where $M \cdot N$ denotes the set $\{m \cdot n \mid m \in M, n \in N\}$ and $M * N$ denotes the additive submonoid generated by these products.

AddSubmonoid.mul_sup theorem

: M * (N ⊔ P) = M * N ⊔ M * P

Full source

lemma mul_sup : M * (N ⊔ P) = M * N ⊔ M * P := addSubmonoid_smul_sup

Distributivity of Additive Submonoid Multiplication over Supremum

Informal description

For additive submonoids $M$, $N$, and $P$ of a non-unital non-associative semiring $R$, the product of $M$ with the supremum of $N$ and $P$ equals the supremum of the products $M * N$ and $M * P$, i.e., $$ M * (N \sqcup P) = (M * N) \sqcup (M * P). $$

AddSubmonoid.sup_mul theorem

: (M ⊔ N) * P = M * P ⊔ N * P

Full source

lemma sup_mul : (M ⊔ N) * P = M * P ⊔ N * P :=
  le_antisymm (mul_le.mpr fun mn hmn p hp ↦ by
    obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn
    rw [right_distrib]; exact add_mem_sup (mul_mem_mul hm hp) <| mul_mem_mul hn hp)
    (sup_le (mul_le_mul_left le_sup_left) <| mul_le_mul_left le_sup_right)

Right Distributivity of Additive Submonoid Multiplication over Supremum

Informal description

For additive submonoids $M$, $N$, and $P$ of a semiring $R$, the product of the supremum of $M$ and $N$ with $P$ is equal to the supremum of the products $M * P$ and $N * P$. That is, $$(M \sqcup N) * P = (M * P) \sqcup (N * P).$$

AddSubmonoid.iSup_mul theorem

(S : ι → AddSubmonoid R) (T : AddSubmonoid R) : (⨆ i, S i) * T = ⨆ i, S i * T

Full source

lemma iSup_mul (S : ι → AddSubmonoid R) (T : AddSubmonoid R) : (⨆ i, S i) * T = ⨆ i, S i * T :=
  le_antisymm (mul_le.mpr fun s hs t ht ↦ iSup_induction _ (motive := (· * t ∈ _)) hs
      (fun i s hs ↦ mem_iSup_of_mem i <| mul_mem_mul hs ht) (by simp_rw [zero_mul]; apply zero_mem)
      fun _ _ ↦ by simp_rw [right_distrib]; apply add_mem) <|
    iSup_le fun i ↦ mul_le_mul_left (le_iSup _ i)

Supremum of Additive Submonoids Distributes Over Multiplication

Informal description

Let $R$ be a semiring and $\{S_i\}_{i \in \iota}$ be a family of additive submonoids of $R$. For any additive submonoid $T$ of $R$, the product of the supremum of the family $\{S_i\}$ with $T$ equals the supremum of the family of products $\{S_i * T\}_{i \in \iota}$. In other words: $$\left(\bigsqcup_{i \in \iota} S_i\right) * T = \bigsqcup_{i \in \iota} (S_i * T)$$

AddSubmonoid.mul_iSup theorem

(T : AddSubmonoid R) (S : ι → AddSubmonoid R) : (T * ⨆ i, S i) = ⨆ i, T * S i

Full source

lemma mul_iSup (T : AddSubmonoid R) (S : ι → AddSubmonoid R) : (T * ⨆ i, S i) = ⨆ i, T * S i :=
  smul_iSup T S

Left Multiplication Distributes over Supremum of Additive Submonoids

Informal description

Let $R$ be a semiring and let $T$ be an additive submonoid of $R$. For any family of additive submonoids $(S_i)_{i \in \iota}$ of $R$, the product of $T$ with the supremum of the family $(S_i)$ equals the supremum of the family of products $(T * S_i)$. That is, $$ T * \left(\bigsqcup_{i \in \iota} S_i\right) = \bigsqcup_{i \in \iota} (T * S_i). $$

AddSubmonoid.mul_comm_of_commute theorem

(h : ∀ m ∈ M, ∀ n ∈ N, Commute m n) : M * N = N * M

Full source

lemma mul_comm_of_commute (h : ∀ m ∈ M, ∀ n ∈ N, Commute m n) : M * N = N * M :=
  le_antisymm (mul_le.mpr fun m hm n hn ↦ h m hm n hn ▸ mul_mem_mul hn hm)
    (mul_le.mpr fun n hn m hm ↦ h m hm n hn ▸ mul_mem_mul hm hn)

Commutativity of Additive Submonoid Product Under Elementwise Commutation

Informal description

Let $M$ and $N$ be additive submonoids of a semiring $R$. If every element of $M$ commutes with every element of $N$ (i.e., for all $m \in M$ and $n \in N$, $m * n = n * m$), then the product submonoids satisfy $M * N = N * M$.

AddSubmonoid.hasDistribNeg definition

: HasDistribNeg (AddSubmonoid R)

Full source

/-- `AddSubmonoid.neg` distributes over multiplication.

This is available as an instance in the `Pointwise` locale. -/
protected def hasDistribNeg : HasDistribNeg (AddSubmonoid R) where
  neg_mul x y := by
    refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_) <;>
        simp only [AddSubmonoid.mem_neg, ← neg_mul] at *
    · exact mul_mem_mul hm hn
    · exact mul_mem_mul (neg_mem_neg.2 hm) hn
  mul_neg x y := by
    refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_) <;>
        simp only [AddSubmonoid.mem_neg, ← mul_neg] at *
    · exact mul_mem_mul hm hn
    · exact mul_mem_mul hm (neg_mem_neg.2 hn)

Distributivity of negation over multiplication in additive submonoids

Informal description

The negation operation distributes over multiplication in the lattice of additive submonoids of a semiring $R$. Specifically, for any additive submonoids $M$ and $N$ of $R$, we have: 1. $- (M * N) = (-M) * N$ 2. $- (M * N) = M * (-N)$ where $M * N$ denotes the product submonoid consisting of all elements $m * n$ for $m \in M$ and $n \in N$.

AddSubmonoid.mulOneClass definition

: MulOneClass (AddSubmonoid R)

Full source

/-- A `MulOneClass` structure on additive submonoids of a (possibly, non-associative) semiring. -/
protected def mulOneClass : MulOneClass (AddSubmonoid R) where
  one_mul M := by rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, one_mul]
  mul_one M := by rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, mul_one]

Multiplicative structure with identity on additive submonoids

Informal description

The structure `MulOneClass (AddSubmonoid R)` equips the additive submonoids of a (possibly non-associative) semiring $R$ with a multiplicative structure that includes a multiplicative identity element (1) and satisfies the axioms $1 * M = M$ and $M * 1 = M$ for any additive submonoid $M$ of $R$.

AddSubmonoid.semigroup definition

: Semigroup (AddSubmonoid R)

Full source

/-- Semigroup structure on additive submonoids of a (possibly, non-unital) semiring. -/
protected def semigroup : Semigroup (AddSubmonoid R) where
  mul_assoc _M _N _P :=
    le_antisymm
      (mul_le.2 fun _mn hmn p hp => AddSubmonoid.mul_induction_on hmn
        (fun m hm n hn ↦ mul_assoc m n p ▸ mul_mem_mul hm <| mul_mem_mul hn hp)
        fun x y ↦ (add_mul x y p).symm ▸ add_mem)
      (mul_le.2 fun m hm _np hnp => AddSubmonoid.mul_induction_on hnp
        (fun n hn p hp ↦ mul_assoc m n p ▸ mul_mem_mul (mul_mem_mul hm hn) hp)
        fun x y ↦ (mul_add m x y) ▸ add_mem)

Semigroup structure on additive submonoids

Informal description

The semigroup structure on the additive submonoids of a (possibly non-unital) semiring $R$, where the multiplication operation is defined as the pointwise product of submonoids.

AddSubmonoid.monoid definition

: Monoid (AddSubmonoid R)

Full source

/-- Monoid structure on additive submonoids of a semiring. -/
protected def monoid : Monoid (AddSubmonoid R) where

Monoid structure on additive submonoids of a semiring

Informal description

The monoid structure on the additive submonoids of a semiring $R$, where the multiplication operation is defined as the pointwise product of submonoids and includes a multiplicative identity element (1). This structure extends the semigroup structure on additive submonoids by adding the multiplicative identity and its properties.

AddSubmonoid.closure_pow theorem

(s : Set R) : ∀ n : ℕ, closure s ^ n = closure (s ^ n)

Full source

lemma closure_pow (s : Set R) : ∀ n : ℕ, closure s ^ n = closure (s ^ n)
  | 0 => by rw [pow_zero, pow_zero, one_eq_closure_one_set]
  | n + 1 => by rw [pow_succ, pow_succ, closure_pow s n, closure_mul_closure]

Power of Additive Submonoid Closure Equals Closure of Power Set: $(\langle s \rangle)^n = \langle s^n \rangle$

Informal description

For any subset $s$ of a semiring $R$ and any natural number $n$, the $n$-th power of the additive submonoid generated by $s$ is equal to the additive submonoid generated by the $n$-th power of $s$ (where $s^n$ denotes the $n$-fold pointwise product of $s$ with itself). In symbols: $$(\langle s \rangle)^n = \langle s^n \rangle$$ where $\langle \cdot \rangle$ denotes the additive submonoid closure operation.

AddSubmonoid.pow_eq_closure_pow_set theorem

(s : AddSubmonoid R) (n : ℕ) : s ^ n = closure ((s : Set R) ^ n)

Full source

lemma pow_eq_closure_pow_set (s : AddSubmonoid R) (n : ℕ) :
    s ^ n = closure ((s : Set R) ^ n) := by
  rw [← closure_pow, closure_eq]

Power of Additive Submonoid Equals Closure of Power Set: $s^n = \langle s^n \rangle$

Informal description

For any additive submonoid $s$ of a semiring $R$ and any natural number $n$, the $n$-th power of $s$ is equal to the additive submonoid generated by the $n$-th power of the underlying set of $s$. In symbols: $$s^n = \langle s^n \rangle$$ where $\langle \cdot \rangle$ denotes the additive submonoid closure operation and $s^n$ denotes the $n$-fold pointwise product of the set $s$ with itself.

AddSubmonoid.pow_subset_pow theorem

{s : AddSubmonoid R} {n : ℕ} : (↑s : Set R) ^ n ⊆ ↑(s ^ n)

Full source

lemma pow_subset_pow {s : AddSubmonoid R} {n : ℕ} : (↑s : Set R) ^ n ⊆ ↑(s ^ n) :=
  (pow_eq_closure_pow_set s n).symm ▸ subset_closure

Set Power Contained in Submonoid Power: $(s : \text{Set } R)^n \subseteq s^n$

Informal description

For any additive submonoid $s$ of a semiring $R$ and any natural number $n$, the $n$-th power of the underlying set of $s$ is contained in the underlying set of the $n$-th power of $s$. In symbols: $$(s : \text{Set } R)^n \subseteq (s^n : \text{Set } R)$$ where $s^n$ denotes the $n$-fold pointwise product of the additive submonoid $s$ with itself.

Implementation notes