Mathlib.Algebra.Group.Submonoid.Pointwise

coe_mul_coe theorem

[SetLike S M] [SubmonoidClass S M] (H : S) : H * H = (H : Set M)

Full source

@[to_additive (attr := simp, norm_cast)]
lemma coe_mul_coe [SetLike S M] [SubmonoidClass S M] (H : S) : H * H = (H : Set M) := by
  aesop (add simp mem_mul)

Pointwise Product of Submonoid Equals Itself

Informal description

For any subset $H$ of a monoid $M$ that is closed under multiplication and contains the multiplicative identity, the pointwise product $H * H$ is equal to $H$ as a set.

coe_set_pow theorem

[SetLike S M] [SubmonoidClass S M] : ∀ {n} (hn : n ≠ 0) (H : S), (H ^ n : Set M) = H

Full source

@[to_additive (attr := simp)]
lemma coe_set_pow [SetLike S M] [SubmonoidClass S M] :
    ∀ {n} (hn : n ≠ 0) (H : S), (H ^ n : Set M) = H
  | 1, _, H => by simp
  | n + 2, _, H => by rw [pow_succ, coe_set_pow n.succ_ne_zero, coe_mul_coe]

Pointwise Power of Submonoid Equals Itself for Nonzero Exponents

Informal description

For any subset $H$ of a monoid $M$ that is closed under multiplication and contains the multiplicative identity, and for any nonzero natural number $n$, the $n$-th pointwise power of $H$ is equal to $H$ as a set, i.e., $H^n = H$.

Submonoid.mul_subset theorem

{S : Submonoid M} (hs : s ⊆ S) (ht : t ⊆ S) : s * t ⊆ S

Full source

@[to_additive]
theorem mul_subset {S : Submonoid M} (hs : s ⊆ S) (ht : t ⊆ S) : s * t ⊆ S :=
  mul_subset_iff.2 fun _x hx _y hy ↦ mul_mem (hs hx) (ht hy)

Submonoid Closure Under Pointwise Product of Subsets

Informal description

Let $M$ be a monoid and $S$ a submonoid of $M$. For any subsets $s$ and $t$ of $M$ such that $s \subseteq S$ and $t \subseteq S$, the pointwise product $s * t$ is contained in $S$.

Submonoid.mul_subset_closure theorem

(hs : s ⊆ u) (ht : t ⊆ u) : s * t ⊆ Submonoid.closure u

Full source

@[to_additive]
theorem mul_subset_closure (hs : s ⊆ u) (ht : t ⊆ u) : s * t ⊆ Submonoid.closure u :=
  mul_subset (Subset.trans hs Submonoid.subset_closure) (Subset.trans ht Submonoid.subset_closure)

Pointwise product of subsets is contained in submonoid closure

Informal description

Let $M$ be a monoid and $u$ a subset of $M$. For any subsets $s$ and $t$ of $M$ such that $s \subseteq u$ and $t \subseteq u$, the pointwise product $s * t$ is contained in the submonoid generated by $u$.

Submonoid.coe_mul_self_eq theorem

(s : Submonoid M) : (s : Set M) * s = s

Full source

@[to_additive]
theorem coe_mul_self_eq (s : Submonoid M) : (s : Set M) * s = s := by
  ext x
  refine ⟨?_, fun h => ⟨x, h, 1, s.one_mem, mul_one x⟩⟩
  rintro ⟨a, ha, b, hb, rfl⟩
  exact s.mul_mem ha hb

Submonoid's set product with itself equals itself

Informal description

For any submonoid $S$ of a monoid $M$, the pointwise product of the underlying set of $S$ with itself equals $S$ itself, i.e., $S \cdot S = S$ where $S \cdot S = \{x \cdot y \mid x, y \in S\}$.

Submonoid.closure_mul_le theorem

(S T : Set M) : closure (S * T) ≤ closure S ⊔ closure T

Full source

@[to_additive]
theorem closure_mul_le (S T : Set M) : closure (S * T) ≤ closureclosure S ⊔ closure T :=
  sInf_le fun _x ⟨_s, hs, _t, ht, hx⟩ => hx ▸
    (closureclosure S ⊔ closure T).mul_mem (SetLike.le_def.mp le_sup_left <| subset_closure hs)
      (SetLike.le_def.mp le_sup_right <| subset_closure ht)

Submonoid Closure of Product is Contained in Join of Closures

Informal description

For any subsets $S$ and $T$ of a monoid $M$, the submonoid generated by their pointwise product $S \cdot T$ is contained in the join (supremum) of the submonoids generated by $S$ and $T$ individually. That is, $\text{closure}(S \cdot T) \leq \text{closure}(S) \sqcup \text{closure}(T)$.

Submonoid.closure_pow_le theorem

: ∀ {n}, n ≠ 0 → closure (s ^ n) ≤ closure s

Full source

@[to_additive]
lemma closure_pow_le : ∀ {n}, n ≠ 0 → closure (s ^ n) ≤ closure s
  | 1, _ => by simp
  | n + 2, _ =>
    calc
      closure (s ^ (n + 2))
      _ = closure (s ^ (n + 1) * s) := by rw [pow_succ]
      _ ≤ closure (s ^ (n + 1)) ⊔ closure s := closure_mul_le ..
      _ ≤ closure s ⊔ closure s := by gcongr ?_ ⊔ _; exact closure_pow_le n.succ_ne_zero
      _ = closure s := sup_idem _

Submonoid closure of powers is contained in original closure

Informal description

For any subset $s$ of a monoid $M$ and any nonzero natural number $n$, the submonoid generated by the $n$-th power set $s^n$ is contained in the submonoid generated by $s$ itself, i.e., $\text{closure}(s^n) \leq \text{closure}(s)$.

Submonoid.closure_pow theorem

{n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : closure (s ^ n) = closure s

Full source

@[to_additive]
lemma closure_pow {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : closure (s ^ n) = closure s :=
  (closure_pow_le hn).antisymm <| by gcongr; exact subset_pow hs hn

Equality of Submonoid Closures for Powers and Original Set

Informal description

For any subset $s$ of a monoid $M$ containing the multiplicative identity $1$, and any nonzero natural number $n$, the submonoid generated by the $n$-th power set $s^n$ is equal to the submonoid generated by $s$ itself, i.e., $\text{closure}(s^n) = \text{closure}(s)$.

Submonoid.sup_eq_closure_mul theorem

(H K : Submonoid M) : H ⊔ K = closure ((H : Set M) * (K : Set M))

Full source

@[to_additive]
theorem sup_eq_closure_mul (H K : Submonoid M) : H ⊔ K = closure ((H : Set M) * (K : Set M)) :=
  le_antisymm
    (sup_le (fun h hh => subset_closure ⟨h, hh, 1, K.one_mem, mul_one h⟩) fun k hk =>
      subset_closure ⟨1, H.one_mem, k, hk, one_mul k⟩)
    ((closure_mul_le _ _).trans <| by rw [closure_eq, closure_eq])

Supremum of Submonoids Equals Closure of Their Product Set

Informal description

For any two submonoids $H$ and $K$ of a monoid $M$, the supremum $H \sqcup K$ in the lattice of submonoids is equal to the submonoid generated by the pointwise product set $H \cdot K = \{h \cdot k \mid h \in H, k \in K\}$.

Submonoid.pow_smul_mem_closure_smul theorem

 {N : Type*} [CommMonoid N] [MulAction M N] [IsScalarTower M N N] (r : M) (s : Set N) {x : N} (hx : x ∈ closure s) :
  ∃ n : ℕ, r ^ n • x ∈ closure (r • s)

Full source

@[to_additive]
theorem pow_smul_mem_closure_smul {N : Type*} [CommMonoid N] [MulAction M N] [IsScalarTower M N N]
    (r : M) (s : Set N) {x : N} (hx : x ∈ closure s) : ∃ n : ℕ, r ^ n • x ∈ closure (r • s) := by
  induction hx using closure_induction with
  | mem x hx => exact ⟨1, subset_closure ⟨_, hx, by rw [pow_one]⟩⟩
  | one => exact ⟨0, by simpa using one_mem _⟩
  | mul x y _ _ hx hy =>
    obtain ⟨⟨nx, hx⟩, ⟨ny, hy⟩⟩ := And.intro hx hy
    use ny + nx
    rw [pow_add, mul_smul, ← smul_mul_assoc, mul_comm, ← smul_mul_assoc]
    exact mul_mem hy hx

Existence of Power Scalar Multiple in Submonoid Closure under Scalar Action

Informal description

Let $M$ be a monoid acting on a commutative monoid $N$ such that the action is compatible with multiplication in $N$ (i.e., $M$ acts as a scalar tower over $N$). For any element $r \in M$, any subset $s \subseteq N$, and any element $x$ in the submonoid generated by $s$, there exists a natural number $n$ such that $r^n \cdot x$ is in the submonoid generated by the set $\{r \cdot y \mid y \in s\}$.

Submonoid.inv definition

: Inv (Submonoid G)

Full source

/-- The submonoid with every element inverted. -/
@[to_additive "The additive submonoid with every element negated."]
protected def inv : Inv (Submonoid G) where
  inv S :=
    { carrier := (S : Set G)⁻¹
      mul_mem' := fun ha hb => by rw [mem_inv, mul_inv_rev]; exact mul_mem hb ha
      one_mem' := mem_inv.2 <| by rw [inv_one]; exact S.one_mem' }

Inverse of a submonoid

Informal description

For a submonoid $S$ of a group $G$, the operation $S^{-1}$ constructs a new submonoid consisting of the inverses of all elements in $S$. Specifically, $S^{-1}$ is defined as the set $\{g^{-1} \mid g \in S\}$, which is closed under multiplication and contains the identity element.

Submonoid.coe_inv theorem

(S : Submonoid G) : ↑S⁻¹ = (S : Set G)⁻¹

Full source

@[to_additive (attr := simp)]
theorem coe_inv (S : Submonoid G) : ↑S⁻¹ = (S : Set G)⁻¹ :=
  rfl

Inverse Submonoid's Underlying Set Equals Pointwise Inverse of Original Submonoid's Set

Informal description

For any submonoid $S$ of a group $G$, the underlying set of the inverse submonoid $S^{-1}$ is equal to the pointwise inverse of the underlying set of $S$, i.e., $\overline{S^{-1}} = \{g^{-1} \mid g \in S\}$.

Submonoid.mem_inv theorem

{g : G} {S : Submonoid G} : g ∈ S⁻¹ ↔ g⁻¹ ∈ S

Full source

@[to_additive (attr := simp)]
theorem mem_inv {g : G} {S : Submonoid G} : g ∈ S⁻¹g ∈ S⁻¹ ↔ g⁻¹ ∈ S :=
  Iff.rfl

Membership in Inverse Submonoid Criterion

Informal description

For an element $g$ in a group $G$ and a submonoid $S$ of $G$, the element $g$ belongs to the inverse submonoid $S^{-1}$ if and only if its inverse $g^{-1}$ belongs to $S$.

Submonoid.involutiveInv definition

: InvolutiveInv (Submonoid G)

Full source

/-- Inversion is involutive on submonoids. -/
@[to_additive "Inversion is involutive on additive submonoids."]
def involutiveInv : InvolutiveInv (Submonoid G) :=
  SetLike.coe_injective.involutiveInv _ fun _ => rfl

Involutive property of inversion on submonoids

Informal description

The inversion operation on submonoids is involutive, meaning that for any submonoid $S$ of a group $G$, taking the inverse twice returns the original submonoid: $(S^{-1})^{-1} = S$.

Submonoid.inv_le_inv theorem

(S T : Submonoid G) : S⁻¹ ≤ T⁻¹ ↔ S ≤ T

Full source

@[to_additive (attr := simp)]
theorem inv_le_inv (S T : Submonoid G) : S⁻¹S⁻¹ ≤ T⁻¹ ↔ S ≤ T :=
  SetLike.coe_subset_coe.symm.trans Set.inv_subset_inv

Inclusion of Inverse Submonoids is Equivalent to Inclusion of Original Submonoids

Informal description

For any two submonoids $S$ and $T$ of a group $G$, the inverse submonoid $S^{-1}$ is contained in $T^{-1}$ if and only if $S$ is contained in $T$.

Submonoid.inv_le theorem

(S T : Submonoid G) : S⁻¹ ≤ T ↔ S ≤ T⁻¹

Full source

@[to_additive]
theorem inv_le (S T : Submonoid G) : S⁻¹S⁻¹ ≤ T ↔ S ≤ T⁻¹ :=
  SetLike.coe_subset_coe.symm.trans Set.inv_subset

Inclusion Relation between Submonoids and their Inverses: $S^{-1} \subseteq T \leftrightarrow S \subseteq T^{-1}$

Informal description

For any two submonoids $S$ and $T$ of a group $G$, the inverse submonoid $S^{-1}$ is contained in $T$ if and only if $S$ is contained in the inverse submonoid $T^{-1}$.

Submonoid.invOrderIso definition

: Submonoid G ≃o Submonoid G

Full source

/-- Pointwise inversion of submonoids as an order isomorphism. -/
@[to_additive (attr := simps!) "Pointwise negation of additive submonoids as an order isomorphism"]
def invOrderIso : SubmonoidSubmonoid G ≃o Submonoid G where
  toEquiv := Equiv.inv _
  map_rel_iff' := inv_le_inv _ _

Order isomorphism of submonoids under pointwise inversion

Informal description

The order isomorphism that maps a submonoid $S$ of a group $G$ to its pointwise inverse submonoid $S^{-1} = \{x^{-1} \mid x \in S\}$, preserving the inclusion order. Specifically, for any two submonoids $S$ and $T$ of $G$, we have $S^{-1} \subseteq T^{-1}$ if and only if $S \subseteq T$.

Submonoid.closure_inv theorem

(s : Set G) : closure s⁻¹ = (closure s)⁻¹

Full source

@[to_additive]
theorem closure_inv (s : Set G) : closure s⁻¹ = (closure s)⁻¹ := by
  apply le_antisymm
  · rw [closure_le, coe_inv, ← Set.inv_subset, inv_inv]
    exact subset_closure
  · rw [inv_le, closure_le, coe_inv, ← Set.inv_subset]
    exact subset_closure

Submonoid Closure of Inverses Equals Inverse of Submonoid Closure

Informal description

For any subset $s$ of a group $G$, the submonoid generated by the pointwise inverses of $s$ is equal to the pointwise inverse of the submonoid generated by $s$. In symbols: $$\text{closure}(s^{-1}) = (\text{closure}(s))^{-1}$$ where $s^{-1} = \{g^{-1} \mid g \in s\}$ and $(\text{closure}(s))^{-1} = \{g^{-1} \mid g \in \text{closure}(s)\}$.

Submonoid.mem_closure_inv theorem

(s : Set G) (x : G) : x ∈ closure s⁻¹ ↔ x⁻¹ ∈ closure s

Full source

@[to_additive]
lemma mem_closure_inv (s : Set G) (x : G) : x ∈ closure s⁻¹x ∈ closure s⁻¹ ↔ x⁻¹ ∈ closure s := by
  rw [closure_inv, mem_inv]

Membership Criterion in Submonoid Generated by Inverses

Informal description

For any subset $s$ of a group $G$ and any element $x \in G$, the element $x$ belongs to the submonoid generated by the set of inverses $s^{-1} = \{g^{-1} \mid g \in s\}$ if and only if its inverse $x^{-1}$ belongs to the submonoid generated by $s$.

Submonoid.inv_inf theorem

(S T : Submonoid G) : (S ⊓ T)⁻¹ = S⁻¹ ⊓ T⁻¹

Full source

@[to_additive (attr := simp)]
theorem inv_inf (S T : Submonoid G) : (S ⊓ T)⁻¹ = S⁻¹S⁻¹ ⊓ T⁻¹ :=
  SetLike.coe_injective Set.inter_inv

Inverse of Submonoid Intersection Equals Intersection of Inverses

Informal description

For any two submonoids $S$ and $T$ of a group $G$, the inverse of their intersection equals the intersection of their inverses, i.e., $(S \cap T)^{-1} = S^{-1} \cap T^{-1}$.

Submonoid.inv_sup theorem

(S T : Submonoid G) : (S ⊔ T)⁻¹ = S⁻¹ ⊔ T⁻¹

Full source

@[to_additive (attr := simp)]
theorem inv_sup (S T : Submonoid G) : (S ⊔ T)⁻¹ = S⁻¹S⁻¹ ⊔ T⁻¹ :=
  (invOrderIso : SubmonoidSubmonoid G ≃o Submonoid G).map_sup S T

Inverse of Submonoid Join Equals Join of Inverses

Informal description

For any two submonoids $S$ and $T$ of a group $G$, the inverse of their join equals the join of their inverses, i.e., $(S \sqcup T)^{-1} = S^{-1} \sqcup T^{-1}$.

Submonoid.inv_bot theorem

: (⊥ : Submonoid G)⁻¹ = ⊥

Full source

@[to_additive (attr := simp)]
theorem inv_bot : (⊥ : Submonoid G)⁻¹ = ⊥ :=
  SetLike.coe_injective <| (Set.inv_singleton 1).trans <| congr_arg _ inv_one

Inverse of Trivial Submonoid is Trivial

Informal description

For any group $G$, the inverse of the trivial submonoid $\{1\}$ is itself, i.e., $(\bot : \text{Submonoid } G)^{-1} = \bot$.

Submonoid.inv_top theorem

: (⊤ : Submonoid G)⁻¹ = ⊤

Full source

@[to_additive (attr := simp)]
theorem inv_top : (⊤ : Submonoid G)⁻¹ = ⊤ :=
  SetLike.coe_injective <| Set.inv_univ

Inverse of the Top Submonoid is Itself

Informal description

For any group $G$, the inverse of the top submonoid (the entire group $G$) is equal to itself, i.e., $(\top : \text{Submonoid } G)^{-1} = \top$.

Submonoid.inv_iInf theorem

{ι : Sort*} (S : ι → Submonoid G) : (⨅ i, S i)⁻¹ = ⨅ i, (S i)⁻¹

Full source

@[to_additive (attr := simp)]
theorem inv_iInf {ι : Sort*} (S : ι → Submonoid G) : (⨅ i, S i)⁻¹ = ⨅ i, (S i)⁻¹ :=
  (invOrderIso : SubmonoidSubmonoid G ≃o Submonoid G).map_iInf _

Inverse of Infimum of Submonoids Equals Infimum of Inverses

Informal description

For any family of submonoids $(S_i)_{i \in \iota}$ of a group $G$, the inverse of their infimum equals the infimum of their inverses. That is, $(\bigsqcap_i S_i)^{-1} = \bigsqcap_i S_i^{-1}$.

Submonoid.inv_iSup theorem

{ι : Sort*} (S : ι → Submonoid G) : (⨆ i, S i)⁻¹ = ⨆ i, (S i)⁻¹

Full source

@[to_additive (attr := simp)]
theorem inv_iSup {ι : Sort*} (S : ι → Submonoid G) : (⨆ i, S i)⁻¹ = ⨆ i, (S i)⁻¹ :=
  (invOrderIso : SubmonoidSubmonoid G ≃o Submonoid G).map_iSup _

Inverse of Supremum of Submonoids Equals Supremum of Inverses

Informal description

For any family of submonoids $\{S_i\}_{i \in \iota}$ of a group $G$, the inverse of their supremum is equal to the supremum of their inverses, i.e., $$ \left( \bigsqcup_{i} S_i \right)^{-1} = \bigsqcup_{i} S_i^{-1}. $$

Submonoid.pointwiseMulAction definition

: MulAction α (Submonoid M)

Full source

/-- The action on a submonoid corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseMulAction : MulAction α (Submonoid M) where
  smul a S := S.map (MulDistribMulAction.toMonoidEnd _ M a)
  one_smul S := by
    change S.map _ = S
    simpa only [map_one] using S.map_id
  mul_smul _ _ S :=
    (congr_arg (fun f : Monoid.End M => S.map f) (MonoidHom.map_mul _ _ _)).trans
      (S.map_map _ _).symm

Pointwise action on submonoids

Informal description

Given a monoid $M$ and a monoid action of $\alpha$ on $M$, the pointwise action of $\alpha$ on submonoids of $M$ is defined by applying the action to every element of the submonoid. Specifically, for $a \in \alpha$ and a submonoid $S \subseteq M$, the action $a \cdot S$ is the submonoid obtained by mapping each element $m \in S$ to $a \cdot m$ via the monoid endomorphism induced by $a$. This action satisfies the following properties: 1. The action by the identity element $1 \in \alpha$ leaves the submonoid unchanged: $1 \cdot S = S$. 2. The action is compatible with multiplication in $\alpha$: $(a \cdot b) \cdot S = a \cdot (b \cdot S)$.

Submonoid.coe_pointwise_smul theorem

(a : α) (S : Submonoid M) : ↑(a • S) = a • (S : Set M)

Full source

@[simp]
theorem coe_pointwise_smul (a : α) (S : Submonoid M) : ↑(a • S) = a • (S : Set M) :=
  rfl

Pointwise scalar multiplication commutes with submonoid coercion to sets

Informal description

For any element $a$ in a monoid $\alpha$ acting on a monoid $M$, and any submonoid $S$ of $M$, the underlying set of the pointwise scalar multiplication $a \cdot S$ is equal to the pointwise scalar multiplication of $a$ on the underlying set of $S$. That is, $$ (a \cdot S) = a \cdot (S : \text{Set } M). $$

Submonoid.smul_mem_pointwise_smul theorem

(m : M) (a : α) (S : Submonoid M) : m ∈ S → a • m ∈ a • S

Full source

theorem smul_mem_pointwise_smul (m : M) (a : α) (S : Submonoid M) : m ∈ S → a • m ∈ a • S :=
  (Set.smul_mem_smul_set : _ → _ ∈ a • (S : Set M))

Pointwise Action Preserves Submonoid Membership

Informal description

Let $M$ be a monoid with a monoid action of $\alpha$ on $M$. For any element $m \in M$, any element $a \in \alpha$, and any submonoid $S \subseteq M$, if $m$ belongs to $S$, then the action $a \cdot m$ belongs to the pointwise action $a \cdot S$.

Submonoid.instCovariantClassHSMulLe instance

: CovariantClass α (Submonoid M) HSMul.hSMul LE.le

Full source

instance : CovariantClass α (Submonoid M) HSMul.hSMul LE.le :=
  ⟨fun _ _ => image_subset _⟩

Covariance of Pointwise Scalar Multiplication on Submonoids with Respect to Subset Order

Informal description

For any monoid $M$ and a monoid action of $\alpha$ on $M$, the pointwise scalar multiplication action on submonoids of $M$ is covariant with respect to the subset order. That is, for any $a \in \alpha$ and submonoids $S, T \subseteq M$, if $S \subseteq T$, then $a \cdot S \subseteq a \cdot T$.

Submonoid.mem_smul_pointwise_iff_exists theorem

(m : M) (a : α) (S : Submonoid M) : m ∈ a • S ↔ ∃ s : M, s ∈ S ∧ a • s = m

Full source

theorem mem_smul_pointwise_iff_exists (m : M) (a : α) (S : Submonoid M) :
    m ∈ a • Sm ∈ a • S ↔ ∃ s : M, s ∈ S ∧ a • s = m :=
  (Set.mem_smul_set : m ∈ a • (S : Set M)m ∈ a • (S : Set M) ↔ _)

Characterization of Membership in Pointwise Action on Submonoids

Informal description

For any element $m$ in a monoid $M$, any element $a$ of a monoid $\alpha$ acting on $M$, and any submonoid $S$ of $M$, the element $m$ belongs to the pointwise action $a \cdot S$ if and only if there exists an element $s \in S$ such that $a \cdot s = m$.

Submonoid.smul_bot theorem

(a : α) : a • (⊥ : Submonoid M) = ⊥

Full source

@[simp]
theorem smul_bot (a : α) : a • (⊥ : Submonoid M) = ⊥ :=
  map_bot _

Pointwise Action Preserves Trivial Submonoid

Informal description

For any element $a$ of a monoid $\alpha$ acting on a monoid $M$, the pointwise action of $a$ on the trivial submonoid $\bot$ of $M$ is the trivial submonoid $\bot$.

Submonoid.smul_sup theorem

(a : α) (S T : Submonoid M) : a • (S ⊔ T) = a • S ⊔ a • T

Full source

theorem smul_sup (a : α) (S T : Submonoid M) : a • (S ⊔ T) = a • S ⊔ a • T :=
  map_sup _ _ _

Pointwise Action Distributes Over Submonoid Join

Informal description

Let $M$ be a monoid with a multiplicative action by a monoid $\alpha$. For any $a \in \alpha$ and any two submonoids $S, T$ of $M$, the pointwise action of $a$ on the join $S \sqcup T$ is equal to the join of the pointwise actions of $a$ on $S$ and $T$, i.e., \[ a \cdot (S \sqcup T) = (a \cdot S) \sqcup (a \cdot T). \]

Submonoid.smul_closure theorem

(a : α) (s : Set M) : a • closure s = closure (a • s)

Full source

theorem smul_closure (a : α) (s : Set M) : a • closure s = closure (a • s) :=
  MonoidHom.map_mclosure _ _

Pointwise Action Commutes with Submonoid Generation

Informal description

Let $M$ be a monoid with a multiplicative action by a monoid $\alpha$. For any $a \in \alpha$ and any subset $s \subseteq M$, the pointwise action of $a$ on the submonoid generated by $s$ is equal to the submonoid generated by the pointwise action of $a$ on $s$, i.e., \[ a \cdot \langle s \rangle = \langle a \cdot s \rangle, \] where $\langle \cdot \rangle$ denotes the submonoid generated by a set.

Submonoid.pointwise_isCentralScalar theorem

[MulDistribMulAction αᵐᵒᵖ M] [IsCentralScalar α M] : IsCentralScalar α (Submonoid M)

Full source

lemma pointwise_isCentralScalar [MulDistribMulAction αᵐᵒᵖ M] [IsCentralScalar α M] :
    IsCentralScalar α (Submonoid M) :=
  ⟨fun _ S => (congr_arg fun f : Monoid.End M => S.map f) <| MonoidHom.ext <| op_smul_eq_smul _⟩

Centrality of Pointwise Action on Submonoids

Informal description

Let $\alpha$ be a monoid acting distributively on a monoid $M$ via a multiplicative action, and suppose that the action of $\alpha$ on $M$ is central (i.e., the left and right actions coincide). Then the induced pointwise action of $\alpha$ on the submonoids of $M$ is also central.

Submonoid.smul_mem_pointwise_smul_iff theorem

{a : α} {S : Submonoid M} {x : M} : a • x ∈ a • S ↔ x ∈ S

Full source

@[simp]
theorem smul_mem_pointwise_smul_iff {a : α} {S : Submonoid M} {x : M} : a • x ∈ a • Sa • x ∈ a • S ↔ x ∈ S :=
  smul_mem_smul_set_iff

Membership in Pointwise Scaled Submonoid: $a \cdot x \in a \cdot S \leftrightarrow x \in S$

Informal description

For any element $a$ in a monoid $\alpha$ acting on a monoid $M$, any submonoid $S$ of $M$, and any element $x \in M$, the element $a \cdot x$ belongs to the pointwise action $a \cdot S$ if and only if $x$ belongs to $S$.

Submonoid.mem_pointwise_smul_iff_inv_smul_mem theorem

{a : α} {S : Submonoid M} {x : M} : x ∈ a • S ↔ a⁻¹ • x ∈ S

Full source

theorem mem_pointwise_smul_iff_inv_smul_mem {a : α} {S : Submonoid M} {x : M} :
    x ∈ a • Sx ∈ a • S ↔ a⁻¹ • x ∈ S :=
  mem_smul_set_iff_inv_smul_mem

Characterization of Membership in Scaled Submonoid via Inverse Action: $x \in a \cdot S \leftrightarrow a^{-1} \cdot x \in S$

Informal description

For any element $a$ in a group $\alpha$ acting on a monoid $M$, any submonoid $S$ of $M$, and any element $x \in M$, we have: \[ x \in a \cdot S \leftrightarrow a^{-1} \cdot x \in S. \]

Submonoid.mem_inv_pointwise_smul_iff theorem

{a : α} {S : Submonoid M} {x : M} : x ∈ a⁻¹ • S ↔ a • x ∈ S

Full source

theorem mem_inv_pointwise_smul_iff {a : α} {S : Submonoid M} {x : M} : x ∈ a⁻¹ • Sx ∈ a⁻¹ • S ↔ a • x ∈ S :=
  mem_inv_smul_set_iff

Characterization of Membership in Inversely Scaled Submonoid: $x \in a^{-1} \cdot S \leftrightarrow a \cdot x \in S$

Informal description

For any element $a$ in a group $\alpha$ acting on a monoid $M$, any submonoid $S$ of $M$, and any element $x \in M$, we have $x \in a^{-1} \cdot S$ if and only if $a \cdot x \in S$.

Submonoid.pointwise_smul_le_pointwise_smul_iff theorem

{a : α} {S T : Submonoid M} : a • S ≤ a • T ↔ S ≤ T

Full source

@[simp]
theorem pointwise_smul_le_pointwise_smul_iff {a : α} {S T : Submonoid M} : a • S ≤ a • T ↔ S ≤ T :=
  smul_set_subset_smul_set_iff

Pointwise scalar multiplication preserves submonoid inclusion: $a \cdot S \subseteq a \cdot T \leftrightarrow S \subseteq T$

Informal description

For any element $a$ of a monoid $\alpha$ acting on a monoid $M$, and for any submonoids $S$ and $T$ of $M$, the pointwise scalar multiplication $a \cdot S$ is contained in $a \cdot T$ if and only if $S$ is contained in $T$.

Submonoid.pointwise_smul_subset_iff theorem

{a : α} {S T : Submonoid M} : a • S ≤ T ↔ S ≤ a⁻¹ • T

Full source

theorem pointwise_smul_subset_iff {a : α} {S T : Submonoid M} : a • S ≤ T ↔ S ≤ a⁻¹ • T :=
  smul_set_subset_iff_subset_inv_smul_set

Pointwise Scalar Multiplication Subset Relation: $a \cdot S \subseteq T \leftrightarrow S \subseteq a^{-1} \cdot T$

Informal description

For any element $a$ in a monoid $\alpha$ and any submonoids $S$ and $T$ of a monoid $M$, the pointwise scalar multiplication $a \cdot S$ is contained in $T$ if and only if $S$ is contained in the pointwise scalar multiplication $a^{-1} \cdot T$.

Submonoid.subset_pointwise_smul_iff theorem

{a : α} {S T : Submonoid M} : S ≤ a • T ↔ a⁻¹ • S ≤ T

Full source

theorem subset_pointwise_smul_iff {a : α} {S T : Submonoid M} : S ≤ a • T ↔ a⁻¹ • S ≤ T :=
  subset_smul_set_iff

Submonoid inclusion under pointwise scalar multiplication: $S \subseteq a \cdot T \leftrightarrow a^{-1} \cdot S \subseteq T$

Informal description

For any element $a$ in a division monoid $\alpha$ and any submonoids $S$ and $T$ of a monoid $M$, the inclusion $S \subseteq a \cdot T$ holds if and only if $a^{-1} \cdot S \subseteq T$.

Set.IsPWO.submonoid_closure theorem

(hpos : ∀ x : α, x ∈ s → 1 ≤ x) (h : s.IsPWO) : IsPWO (Submonoid.closure s : Set α)

Full source

@[to_additive]
theorem submonoid_closure (hpos : ∀ x : α, x ∈ s → 1 ≤ x) (h : s.IsPWO) :
    IsPWO (Submonoid.closure s : Set α) := by
  rw [Submonoid.closure_eq_image_prod]
  refine (h.partiallyWellOrderedOn_sublistForall₂ (· ≤ ·)).image_of_monotone_on ?_
  exact fun l1 _ l2 hl2 h12 => h12.prod_le_prod' fun x hx => hpos x <| hl2 x hx

Partial Well-Ordering of Submonoid Generated by Partially Well-Ordered Set

Informal description

Let $\alpha$ be an ordered cancellative monoid, and let $s$ be a subset of $\alpha$ such that every element of $s$ is greater than or equal to the multiplicative identity $1$. If $s$ is partially well-ordered (i.e., every non-empty subset of $s$ has a minimal element), then the submonoid generated by $s$ is also partially well-ordered.

Implementation notes