Mathlib.Algebra.Group.Submonoid.Operations

Submonoid.toAddSubmonoid definition

: Submonoid M ≃o AddSubmonoid (Additive M)

Full source

/-- Submonoids of monoid `M` are isomorphic to additive submonoids of `Additive M`. -/
@[simps]
def Submonoid.toAddSubmonoid : SubmonoidSubmonoid M ≃o AddSubmonoid (Additive M) where
  toFun S :=
    { carrier := Additive.toMulAdditive.toMul ⁻¹' S
      zero_mem' := S.one_mem'
      add_mem' := fun ha hb => S.mul_mem' ha hb }
  invFun S :=
    { carrier := Additive.ofMulAdditive.ofMul ⁻¹' S
      one_mem' := S.zero_mem'
      mul_mem' := fun ha hb => S.add_mem' ha hb}
  left_inv x := by cases x; rfl
  right_inv x := by cases x; rfl
  map_rel_iff' := Iff.rfl

Order isomorphism between submonoids and additive submonoids

Informal description

The order isomorphism `Submonoid.toAddSubmonoid` establishes a bijection between submonoids of a monoid `M` and additive submonoids of the additive monoid `Additive M`. Specifically: - The forward map takes a submonoid $S \subseteq M$ to the additive submonoid $\{x \mid \text{Additive.toMul}(x) \in S\}$. - The inverse map takes an additive submonoid $T \subseteq \text{Additive } M$ to the submonoid $\{x \mid \text{Additive.ofMul}(x) \in T\}$. This isomorphism preserves the order structure (inclusion of submonoids).

AddSubmonoid.toSubmonoid' abbrev

: AddSubmonoid (Additive M) ≃o Submonoid M

Full source

/-- Additive submonoids of an additive monoid `Additive M` are isomorphic to submonoids of `M`. -/
abbrev AddSubmonoid.toSubmonoid' : AddSubmonoidAddSubmonoid (Additive M) ≃o Submonoid M :=
  Submonoid.toAddSubmonoid.symm

Order isomorphism between additive submonoids and submonoids

Informal description

The order isomorphism $\text{AddSubmonoid.toSubmonoid'}$ establishes a bijection between additive submonoids of the additive monoid $\text{Additive } M$ and submonoids of the original monoid $M$. Specifically: - The forward map takes an additive submonoid $T \subseteq \text{Additive } M$ to the submonoid $\{x \mid \text{Additive.ofMul}(x) \in T\}$. - The inverse map takes a submonoid $S \subseteq M$ to the additive submonoid $\{x \mid \text{Additive.toMul}(x) \in S\}$. This isomorphism preserves the order structure (inclusion of submonoids).

Submonoid.toAddSubmonoid_closure theorem

(S : Set M) : Submonoid.toAddSubmonoid (Submonoid.closure S) = AddSubmonoid.closure (Additive.toMul ⁻¹' S)

Full source

theorem Submonoid.toAddSubmonoid_closure (S : Set M) :
    Submonoid.toAddSubmonoid (Submonoid.closure S)
      = AddSubmonoid.closure (Additive.toMulAdditive.toMul ⁻¹' S) :=
  le_antisymm
    (Submonoid.toAddSubmonoid.le_symm_apply.1 <|
      Submonoid.closure_le.2 (AddSubmonoid.subset_closure (M := Additive M)))
    (AddSubmonoid.closure_le.2 <| Submonoid.subset_closure (M := M))

Submonoid closure commutes with conversion to additive submonoid

Informal description

For any subset $S$ of a monoid $M$, the image of the submonoid generated by $S$ under the order isomorphism `Submonoid.toAddSubmonoid` is equal to the additive submonoid generated by the preimage of $S$ under the map `Additive.toMul`. In symbols: $$\text{Submonoid.toAddSubmonoid}(\text{closure}(S)) = \text{AddSubmonoid.closure}(\text{Additive.toMul}^{-1}(S))$$

AddSubmonoid.toSubmonoid'_closure theorem

 (S : Set (Additive M)) : AddSubmonoid.toSubmonoid' (AddSubmonoid.closure S) = Submonoid.closure (Additive.ofMul ⁻¹' S)

Full source

theorem AddSubmonoid.toSubmonoid'_closure (S : Set (Additive M)) :
    AddSubmonoid.toSubmonoid' (AddSubmonoid.closure S)
      = Submonoid.closure (Additive.ofMulAdditive.ofMul ⁻¹' S) :=
  le_antisymm
    (AddSubmonoid.toSubmonoid'.le_symm_apply.1 <|
      AddSubmonoid.closure_le.2 (Submonoid.subset_closure (M := M)))
    (Submonoid.closure_le.2 <| AddSubmonoid.subset_closure (M := Additive M))

Closure Preservation under Conversion between Additive and Multiplicative Submonoids

Informal description

For any subset $S$ of the additive monoid $\text{Additive } M$, the submonoid obtained by converting the additive submonoid closure of $S$ via the order isomorphism $\text{AddSubmonoid.toSubmonoid'}$ is equal to the submonoid closure of the preimage of $S$ under the map $\text{Additive.ofMul}$. In symbols: $$\text{AddSubmonoid.toSubmonoid'}(\text{AddSubmonoid.closure}(S)) = \text{Submonoid.closure}(\text{Additive.ofMul}^{-1}(S))$$

AddSubmonoid.toSubmonoid definition

: AddSubmonoid A ≃o Submonoid (Multiplicative A)

Full source

/-- Additive submonoids of an additive monoid `A` are isomorphic to
multiplicative submonoids of `Multiplicative A`. -/
@[simps]
def AddSubmonoid.toSubmonoid : AddSubmonoidAddSubmonoid A ≃o Submonoid (Multiplicative A) where
  toFun S :=
    { carrier := Multiplicative.toAddMultiplicative.toAdd ⁻¹' S
      one_mem' := S.zero_mem'
      mul_mem' := fun ha hb => S.add_mem' ha hb }
  invFun S :=
    { carrier := Multiplicative.ofAddMultiplicative.ofAdd ⁻¹' S
      zero_mem' := S.one_mem'
      add_mem' := fun ha hb => S.mul_mem' ha hb}
  left_inv x := by cases x; rfl
  right_inv x := by cases x; rfl
  map_rel_iff' := Iff.rfl

Order isomorphism between additive submonoids and multiplicative submonoids

Informal description

The function `AddSubmonoid.toSubmonoid` establishes an order isomorphism between additive submonoids of an additive monoid `A` and multiplicative submonoids of the multiplicative monoid `Multiplicative A`. Specifically, it maps an additive submonoid `S` of `A` to the multiplicative submonoid of `Multiplicative A` consisting of all elements whose underlying additive elements belong to `S`. The inverse operation maps a multiplicative submonoid `T` of `Multiplicative A` back to the additive submonoid of `A` consisting of all elements whose multiplicative counterparts belong to `T`. This isomorphism preserves the order structure, meaning that for any two additive submonoids `S₁` and `S₂`, we have `S₁ ≤ S₂` if and only if their corresponding multiplicative submonoids satisfy the same inequality.

Submonoid.toAddSubmonoid' abbrev

: Submonoid (Multiplicative A) ≃o AddSubmonoid A

Full source

/-- Submonoids of a monoid `Multiplicative A` are isomorphic to additive submonoids of `A`. -/
abbrev Submonoid.toAddSubmonoid' : SubmonoidSubmonoid (Multiplicative A) ≃o AddSubmonoid A :=
  AddSubmonoid.toSubmonoid.symm

Order isomorphism between multiplicative submonoids and additive submonoids

Informal description

The function `Submonoid.toAddSubmonoid'` establishes an order isomorphism between multiplicative submonoids of the monoid `Multiplicative A` and additive submonoids of the additive monoid `A`. Specifically, it maps a multiplicative submonoid `S` of `Multiplicative A` to the additive submonoid of `A` consisting of all elements whose multiplicative counterparts belong to `S`. This isomorphism preserves the order structure, meaning that for any two multiplicative submonoids `S₁` and `S₂`, we have `S₁ ≤ S₂` if and only if their corresponding additive submonoids satisfy the same inequality.

AddSubmonoid.toSubmonoid_closure theorem

(S : Set A) : (AddSubmonoid.toSubmonoid) (AddSubmonoid.closure S) = Submonoid.closure (Multiplicative.toAdd ⁻¹' S)

Full source

theorem AddSubmonoid.toSubmonoid_closure (S : Set A) :
    (AddSubmonoid.toSubmonoid) (AddSubmonoid.closure S)
      = Submonoid.closure (Multiplicative.toAddMultiplicative.toAdd ⁻¹' S) :=
  le_antisymm
    (AddSubmonoid.toSubmonoid.to_galoisConnection.l_le <|
      AddSubmonoid.closure_le.2 <| Submonoid.subset_closure (M := Multiplicative A))
    (Submonoid.closure_le.2 <| AddSubmonoid.subset_closure (M := A))

Closure Preservation under Additive-Multiplicative Submonoid Isomorphism

Informal description

For any subset $S$ of an additive monoid $A$, the image of the additive submonoid generated by $S$ under the order isomorphism `AddSubmonoid.toSubmonoid` is equal to the multiplicative submonoid generated by the preimage of $S$ under the canonical map from the multiplicative monoid `Multiplicative A` to $A$. In symbols: $$ \text{AddSubmonoid.toSubmonoid}(\text{AddSubmonoid.closure}(S)) = \text{Submonoid.closure}(\text{Multiplicative.toAdd}^{-1}(S)) $$

Submonoid.toAddSubmonoid'_closure theorem

 (S : Set (Multiplicative A)) :
  Submonoid.toAddSubmonoid' (Submonoid.closure S) = AddSubmonoid.closure (Multiplicative.ofAdd ⁻¹' S)

Full source

theorem Submonoid.toAddSubmonoid'_closure (S : Set (Multiplicative A)) :
    Submonoid.toAddSubmonoid' (Submonoid.closure S)
      = AddSubmonoid.closure (Multiplicative.ofAddMultiplicative.ofAdd ⁻¹' S) :=
  le_antisymm
    (Submonoid.toAddSubmonoid'.to_galoisConnection.l_le <|
      Submonoid.closure_le.2 <| AddSubmonoid.subset_closure (M := A))
    (AddSubmonoid.closure_le.2 <| Submonoid.subset_closure (M := Multiplicative A))

Closure Preservation under Multiplicative-to-Additive Submonoid Isomorphism

Informal description

For any subset $S$ of the multiplicative monoid $\text{Multiplicative } A$, the image under the order isomorphism $\text{Submonoid.toAddSubmonoid'}$ of the submonoid generated by $S$ is equal to the additive submonoid generated by the preimage of $S$ under the map $\text{Multiplicative.ofAdd}$. In symbols: $$\text{Submonoid.toAddSubmonoid'}(\text{closure}(S)) = \text{closure}(\text{Multiplicative.ofAdd}^{-1}(S)).$$

Submonoid.comap definition

(f : F) (S : Submonoid N) : Submonoid M

Full source

/-- The preimage of a submonoid along a monoid homomorphism is a submonoid. -/
@[to_additive
      "The preimage of an `AddSubmonoid` along an `AddMonoid` homomorphism is an `AddSubmonoid`."]
def comap (f : F) (S : Submonoid N) :
    Submonoid M where
  carrier := f ⁻¹' S
  one_mem' := show f 1 ∈ S by rw [map_one]; exact S.one_mem
  mul_mem' ha hb := show f (_ * _) ∈ S by rw [map_mul]; exact S.mul_mem ha hb

Preimage of a submonoid under a monoid homomorphism

Informal description

Given a monoid homomorphism $ f : M \to N $ and a submonoid $ S $ of $ N $, the preimage $ f^{-1}(S) $ forms a submonoid of $ M $. This submonoid consists of all elements $ x \in M $ such that $ f(x) \in S $, and it inherits the monoid structure from $ M $.

Submonoid.coe_comap theorem

(S : Submonoid N) (f : F) : (S.comap f : Set M) = f ⁻¹' S

Full source

@[to_additive (attr := simp)]
theorem coe_comap (S : Submonoid N) (f : F) : (S.comap f : Set M) = f ⁻¹' S :=
  rfl

Preimage Submonoid as Set Preimage

Informal description

For a submonoid $S$ of $N$ and a monoid homomorphism $f \colon M \to N$, the underlying set of the preimage submonoid $f^{-1}(S)$ is equal to the preimage of $S$ under $f$, i.e., $$(f^{-1}(S) : \text{Set } M) = f^{-1}(S).$$

Submonoid.mem_comap theorem

{S : Submonoid N} {f : F} {x : M} : x ∈ S.comap f ↔ f x ∈ S

Full source

@[to_additive (attr := simp)]
theorem mem_comap {S : Submonoid N} {f : F} {x : M} : x ∈ S.comap fx ∈ S.comap f ↔ f x ∈ S :=
  Iff.rfl

Characterization of Elements in the Preimage Submonoid

Informal description

For a submonoid $S$ of $N$ and a monoid homomorphism $f : M \to N$, an element $x \in M$ belongs to the preimage submonoid $f^{-1}(S)$ if and only if its image $f(x)$ belongs to $S$.

Submonoid.comap_comap theorem

(S : Submonoid P) (g : N →* P) (f : M →* N) : (S.comap g).comap f = S.comap (g.comp f)

Full source

@[to_additive]
theorem comap_comap (S : Submonoid P) (g : N →* P) (f : M →* N) :
    (S.comap g).comap f = S.comap (g.comp f) :=
  rfl

Preimage of Submonoid under Composition of Homomorphisms

Informal description

Let $M$, $N$, and $P$ be monoids, and let $f \colon M \to N$ and $g \colon N \to P$ be monoid homomorphisms. For any submonoid $S$ of $P$, the preimage of $S$ under the composition $g \circ f$ is equal to the preimage under $f$ of the preimage of $S$ under $g$. In other words, $(S.comap\ g).comap\ f = S.comap\ (g \circ f)$.

Submonoid.comap_id theorem

(S : Submonoid P) : S.comap (MonoidHom.id P) = S

Full source

@[to_additive (attr := simp)]
theorem comap_id (S : Submonoid P) : S.comap (MonoidHom.id P) = S :=
  ext (by simp)

Preimage of Submonoid under Identity Homomorphism is Itself

Informal description

For any submonoid $S$ of a monoid $P$, the preimage of $S$ under the identity monoid homomorphism $\text{id}_P \colon P \to P$ is equal to $S$ itself, i.e., $\text{id}_P^{-1}(S) = S$.

Submonoid.map definition

(f : F) (S : Submonoid M) : Submonoid N

Full source

/-- The image of a submonoid along a monoid homomorphism is a submonoid. -/
@[to_additive
      "The image of an `AddSubmonoid` along an `AddMonoid` homomorphism is an `AddSubmonoid`."]
def map (f : F) (S : Submonoid M) :
    Submonoid N where
  carrier := f '' S
  one_mem' := ⟨1, S.one_mem, map_one f⟩
  mul_mem' := by
    rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
    exact ⟨x * y, S.mul_mem hx hy, by rw [map_mul]⟩

Image of a submonoid under a monoid homomorphism

Informal description

Given a monoid homomorphism $f \colon M \to N$ and a submonoid $S$ of $M$, the image of $S$ under $f$ is the submonoid of $N$ consisting of all elements of the form $f(x)$ for $x \in S$.

Submonoid.coe_map theorem

(f : F) (S : Submonoid M) : (S.map f : Set N) = f '' S

Full source

@[to_additive (attr := simp)]
theorem coe_map (f : F) (S : Submonoid M) : (S.map f : Set N) = f '' S :=
  rfl

Image of Submonoid Under Homomorphism Equals Function Image

Informal description

For any monoid homomorphism $f \colon M \to N$ and any submonoid $S$ of $M$, the underlying set of the image submonoid $S.map f$ is equal to the image of $S$ under $f$, i.e., $(S.map f : \text{Set } N) = f '' S$.

Submonoid.map_coe_toMonoidHom theorem

(f : F) (S : Submonoid M) : S.map (f : M →* N) = S.map f

Full source

@[to_additive (attr := simp)]
theorem map_coe_toMonoidHom (f : F) (S : Submonoid M) : S.map (f : M →* N) = S.map f :=
  rfl

Equality of Submonoid Images under Monoid Homomorphism and Function

Informal description

For any monoid homomorphism $f \colon M \to N$ and any submonoid $S$ of $M$, the image of $S$ under $f$ as a monoid homomorphism is equal to the image of $S$ under $f$ as a function.

Submonoid.map_coe_toMulEquiv theorem

{F} [EquivLike F M N] [MulEquivClass F M N] (f : F) (S : Submonoid M) : S.map (f : M ≃* N) = S.map f

Full source

@[to_additive (attr := simp)]
theorem map_coe_toMulEquiv {F} [EquivLike F M N] [MulEquivClass F M N] (f : F) (S : Submonoid M) :
    S.map (f : M ≃* N) = S.map f :=
  rfl

Equality of Submonoid Images under Multiplicative Equivalence and Function

Informal description

Let $M$ and $N$ be monoids, and let $F$ be a type equipped with an equivalence-like structure between $M$ and $N$ that is also a multiplicative equivalence class. For any multiplicative equivalence $f \colon M \simeq N$ in $F$ and any submonoid $S$ of $M$, the image of $S$ under $f$ as a multiplicative equivalence equals the image of $S$ under $f$ as a function.

Submonoid.mem_map theorem

{f : F} {S : Submonoid M} {y : N} : y ∈ S.map f ↔ ∃ x ∈ S, f x = y

Full source

@[to_additive (attr := simp)]
theorem mem_map {f : F} {S : Submonoid M} {y : N} : y ∈ S.map fy ∈ S.map f ↔ ∃ x ∈ S, f x = y := Iff.rfl

Characterization of Elements in the Image of a Submonoid under a Homomorphism

Informal description

Let $M$ and $N$ be monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a monoid homomorphism. For any element $y \in N$, we have $y \in f(S)$ if and only if there exists $x \in S$ such that $f(x) = y$.

Submonoid.mem_map_of_mem theorem

(f : F) {S : Submonoid M} {x : M} (hx : x ∈ S) : f x ∈ S.map f

Full source

@[to_additive]
theorem mem_map_of_mem (f : F) {S : Submonoid M} {x : M} (hx : x ∈ S) : f x ∈ S.map f :=
  mem_image_of_mem f hx

Image of submonoid element under homomorphism

Informal description

Let $f \colon M \to N$ be a monoid homomorphism, $S$ a submonoid of $M$, and $x \in M$. If $x \in S$, then $f(x)$ belongs to the image of $S$ under $f$.

Submonoid.apply_coe_mem_map theorem

(f : F) (S : Submonoid M) (x : S) : f x ∈ S.map f

Full source

@[to_additive]
theorem apply_coe_mem_map (f : F) (S : Submonoid M) (x : S) : f x ∈ S.map f :=
  mem_map_of_mem f x.2

Image of Submonoid Element under Homomorphism Belongs to Image Submonoid

Informal description

Let $M$ and $N$ be monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a monoid homomorphism. For any element $x \in S$, the image $f(x)$ belongs to the image submonoid $f(S)$.

Submonoid.map_map theorem

(g : N →* P) (f : M →* N) : (S.map f).map g = S.map (g.comp f)

Full source

@[to_additive]
theorem map_map (g : N →* P) (f : M →* N) : (S.map f).map g = S.map (g.comp f) :=
  SetLike.coe_injective <| image_image _ _ _

Image of Submonoid under Composition of Homomorphisms Equals Composition of Images

Informal description

Let $M$, $N$, and $P$ be monoids, and let $f \colon M \to N$ and $g \colon N \to P$ be monoid homomorphisms. For any submonoid $S$ of $M$, the image of $S$ under the composition $g \circ f$ is equal to the image under $g$ of the image of $S$ under $f$. In other words, $(S.map\, f).map\, g = S.map\, (g \circ f)$.

Submonoid.mem_map_iff_mem theorem

{f : F} (hf : Function.Injective f) {S : Submonoid M} {x : M} : f x ∈ S.map f ↔ x ∈ S

Full source

@[to_additive (attr := simp 1100, nolint simpNF)]
theorem mem_map_iff_mem {f : F} (hf : Function.Injective f) {S : Submonoid M} {x : M} :
    f x ∈ S.map ff x ∈ S.map f ↔ x ∈ S :=
  hf.mem_set_image

Characterization of Membership in Image Submonoid via Injectivity

Informal description

Let $f \colon M \to N$ be an injective monoid homomorphism, $S$ a submonoid of $M$, and $x \in M$. Then $f(x)$ belongs to the image submonoid $f(S)$ if and only if $x$ belongs to $S$.

Submonoid.map_le_iff_le_comap theorem

{f : F} {S : Submonoid M} {T : Submonoid N} : S.map f ≤ T ↔ S ≤ T.comap f

Full source

@[to_additive]
theorem map_le_iff_le_comap {f : F} {S : Submonoid M} {T : Submonoid N} :
    S.map f ≤ T ↔ S ≤ T.comap f :=
  image_subset_iff

Image-Preimage Containment Relation for Submonoids

Informal description

Let $f \colon M \to N$ be a monoid homomorphism, $S$ a submonoid of $M$, and $T$ a submonoid of $N$. Then the image of $S$ under $f$ is contained in $T$ if and only if $S$ is contained in the preimage of $T$ under $f$. In other words, $f(S) \subseteq T \leftrightarrow S \subseteq f^{-1}(T)$.

Submonoid.gc_map_comap theorem

(f : F) : GaloisConnection (map f) (comap f)

Full source

@[to_additive]
theorem gc_map_comap (f : F) : GaloisConnection (map f) (comap f) := fun _ _ => map_le_iff_le_comap

Galois Connection Between Image and Preimage of Submonoids

Informal description

For any monoid homomorphism $f \colon M \to N$, the pair of functions `map f` (image under $f$) and `comap f` (preimage under $f$) form a Galois connection between the complete lattices of submonoids of $M$ and $N$. This means that for any submonoid $S$ of $M$ and any submonoid $T$ of $N$, we have: \[ f(S) \subseteq T \quad \text{if and only if} \quad S \subseteq f^{-1}(T). \]

Submonoid.map_le_of_le_comap theorem

{T : Submonoid N} {f : F} : S ≤ T.comap f → S.map f ≤ T

Full source

@[to_additive]
theorem map_le_of_le_comap {T : Submonoid N} {f : F} : S ≤ T.comap f → S.map f ≤ T :=
  (gc_map_comap f).l_le

Image containment under monoid homomorphism via preimage condition

Informal description

Let $f \colon M \to N$ be a monoid homomorphism, $S$ a submonoid of $M$, and $T$ a submonoid of $N$. If $S$ is contained in the preimage of $T$ under $f$ (i.e., $S \subseteq f^{-1}(T)$), then the image of $S$ under $f$ is contained in $T$ (i.e., $f(S) \subseteq T$).

Submonoid.le_comap_of_map_le theorem

{T : Submonoid N} {f : F} : S.map f ≤ T → S ≤ T.comap f

Full source

@[to_additive]
theorem le_comap_of_map_le {T : Submonoid N} {f : F} : S.map f ≤ T → S ≤ T.comap f :=
  (gc_map_comap f).le_u

Inclusion of Submonoid in Preimage Given Image Inclusion

Informal description

Let $S$ be a submonoid of $M$ and $T$ a submonoid of $N$. For any monoid homomorphism $f \colon M \to N$, if the image of $S$ under $f$ is contained in $T$, then $S$ is contained in the preimage of $T$ under $f$. In other words: \[ f(S) \subseteq T \implies S \subseteq f^{-1}(T). \]

Submonoid.le_comap_map theorem

{f : F} : S ≤ (S.map f).comap f

Full source

@[to_additive]
theorem le_comap_map {f : F} : S ≤ (S.map f).comap f :=
  (gc_map_comap f).le_u_l _

Inclusion of Submonoid in Preimage of Its Image

Informal description

For any submonoid $S$ of a monoid $M$ and any monoid homomorphism $f \colon M \to N$, the submonoid $S$ is contained in the preimage of its image under $f$, i.e., $S \subseteq f^{-1}(f(S))$.

Submonoid.map_comap_le theorem

{S : Submonoid N} {f : F} : (S.comap f).map f ≤ S

Full source

@[to_additive]
theorem map_comap_le {S : Submonoid N} {f : F} : (S.comap f).map f ≤ S :=
  (gc_map_comap f).l_u_le _

Image of Preimage is Contained in Original Submonoid

Informal description

For any submonoid $S$ of $N$ and any monoid homomorphism $f \colon M \to N$, the image under $f$ of the preimage of $S$ under $f$ is contained in $S$. In other words: \[ f(f^{-1}(S)) \subseteq S. \]

Submonoid.monotone_map theorem

{f : F} : Monotone (map f)

Full source

@[to_additive]
theorem monotone_map {f : F} : Monotone (map f) :=
  (gc_map_comap f).monotone_l

Monotonicity of Submonoid Image Under Homomorphism

Informal description

For any monoid homomorphism $f \colon M \to N$, the image function $\mathrm{map}\, f$ that sends a submonoid $S$ of $M$ to its image under $f$ is monotone. That is, if $S_1 \subseteq S_2$ are submonoids of $M$, then $f(S_1) \subseteq f(S_2)$ as submonoids of $N$.

Submonoid.monotone_comap theorem

{f : F} : Monotone (comap f)

Full source

@[to_additive]
theorem monotone_comap {f : F} : Monotone (comap f) :=
  (gc_map_comap f).monotone_u

Monotonicity of Submonoid Preimage under Homomorphism

Informal description

For any monoid homomorphism $f \colon M \to N$, the preimage function $\operatorname{comap} f$ mapping submonoids of $N$ to submonoids of $M$ is monotone. That is, for any two submonoids $S_1, S_2$ of $N$ with $S_1 \subseteq S_2$, we have $\operatorname{comap} f(S_1) \subseteq \operatorname{comap} f(S_2)$.

Submonoid.map_comap_map theorem

{f : F} : ((S.map f).comap f).map f = S.map f

Full source

@[to_additive (attr := simp)]
theorem map_comap_map {f : F} : ((S.map f).comap f).map f = S.map f :=
  (gc_map_comap f).l_u_l_eq_l _

Image-Preimage-Image Identity for Submonoids

Informal description

For any monoid homomorphism $f \colon M \to N$ and any submonoid $S$ of $M$, the image under $f$ of the preimage under $f$ of the image of $S$ under $f$ is equal to the image of $S$ under $f$. In other words, $f(f^{-1}(f(S))) = f(S)$.

Submonoid.comap_map_comap theorem

{S : Submonoid N} {f : F} : ((S.comap f).map f).comap f = S.comap f

Full source

@[to_additive (attr := simp)]
theorem comap_map_comap {S : Submonoid N} {f : F} : ((S.comap f).map f).comap f = S.comap f :=
  (gc_map_comap f).u_l_u_eq_u _

Triple Preimage-Image-Preimage Identity for Submonoids

Informal description

Let $M$ and $N$ be monoids, $f \colon M \to N$ a monoid homomorphism, and $S$ a submonoid of $N$. Then the preimage under $f$ of the image under $f$ of the preimage of $S$ under $f$ equals the preimage of $S$ under $f$. In symbols: \[ f^{-1}(f(f^{-1}(S))) = f^{-1}(S). \]

Submonoid.map_sup theorem

(S T : Submonoid M) (f : F) : (S ⊔ T).map f = S.map f ⊔ T.map f

Full source

@[to_additive]
theorem map_sup (S T : Submonoid M) (f : F) : (S ⊔ T).map f = S.map f ⊔ T.map f :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).l_sup

Image of Submonoid Join under Homomorphism Equals Join of Images

Informal description

Let $M$ and $N$ be monoids, $S$ and $T$ be submonoids of $M$, and $f \colon M \to N$ be a monoid homomorphism. Then the image of the join $S \sqcup T$ under $f$ equals the join of the images of $S$ and $T$ under $f$, i.e., \[ f(S \sqcup T) = f(S) \sqcup f(T). \]

Submonoid.map_iSup theorem

{ι : Sort*} (f : F) (s : ι → Submonoid M) : (iSup s).map f = ⨆ i, (s i).map f

Full source

@[to_additive]
theorem map_iSup {ι : Sort*} (f : F) (s : ι → Submonoid M) : (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).l_iSup

Image of Supremum of Submonoids Equals Supremum of Images

Informal description

Let $M$ and $N$ be monoids, $\{S_i\}_{i \in \iota}$ be a family of submonoids of $M$, and $f \colon M \to N$ be a monoid homomorphism. Then the image of the supremum $\bigsqcup_i S_i$ under $f$ equals the supremum of the images $\bigsqcup_i f(S_i)$. In other words, \[ f\left(\bigcup_i S_i\right) = \bigcup_i f(S_i), \] where the closure operation is applied to both sides to form submonoids.

Submonoid.map_inf theorem

(S T : Submonoid M) (f : F) (hf : Function.Injective f) : (S ⊓ T).map f = S.map f ⊓ T.map f

Full source

@[to_additive]
theorem map_inf (S T : Submonoid M) (f : F) (hf : Function.Injective f) :
    (S ⊓ T).map f = S.map f ⊓ T.map f := SetLike.coe_injective (Set.image_inter hf)

Image of Submonoid Intersection under Injective Homomorphism

Informal description

Let $M$ and $N$ be monoids, $S$ and $T$ be submonoids of $M$, and $f \colon M \to N$ be an injective monoid homomorphism. Then the image of the intersection $S \cap T$ under $f$ equals the intersection of the images of $S$ and $T$ under $f$, i.e., \[ f(S \cap T) = f(S) \cap f(T). \]

Submonoid.map_iInf theorem

 {ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f) (s : ι → Submonoid M) : (iInf s).map f = ⨅ i, (s i).map f

Full source

@[to_additive]
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f)
    (s : ι → Submonoid M) : (iInf s).map f = ⨅ i, (s i).map f := by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coeSetLike.coe ∘ s)

Image of Infimum of Submonoids under Injective Homomorphism Equals Infimum of Images

Informal description

Let $M$ and $N$ be monoids, $\{S_i\}_{i \in \iota}$ be a nonempty family of submonoids of $M$, and $f \colon M \to N$ be an injective monoid homomorphism. Then the image of the infimum $\bigsqcap_i S_i$ under $f$ equals the infimum of the images $\bigsqcap_i f(S_i)$. In other words, \[ f\left(\bigcap_i S_i\right) = \bigcap_i f(S_i). \]

Submonoid.comap_inf theorem

(S T : Submonoid N) (f : F) : (S ⊓ T).comap f = S.comap f ⊓ T.comap f

Full source

@[to_additive]
theorem comap_inf (S T : Submonoid N) (f : F) : (S ⊓ T).comap f = S.comap f ⊓ T.comap f :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).u_inf

Preimage of Submonoid Intersection Equals Intersection of Preimages

Informal description

For any monoid homomorphism $f \colon M \to N$ and any two submonoids $S$ and $T$ of $N$, the preimage of the intersection $S \cap T$ under $f$ is equal to the intersection of the preimages of $S$ and $T$ under $f$, i.e., \[ f^{-1}(S \cap T) = f^{-1}(S) \cap f^{-1}(T). \]

Submonoid.comap_iInf theorem

{ι : Sort*} (f : F) (s : ι → Submonoid N) : (iInf s).comap f = ⨅ i, (s i).comap f

Full source

@[to_additive]
theorem comap_iInf {ι : Sort*} (f : F) (s : ι → Submonoid N) :
    (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).u_iInf

Preimage of Infimum of Submonoids Equals Infimum of Preimages

Informal description

Let $M$ and $N$ be monoids, $\{S_i\}_{i \in \iota}$ be a family of submonoids of $N$, and $f \colon M \to N$ be a monoid homomorphism. Then the preimage of the infimum $\bigcap_i S_i$ under $f$ equals the infimum of the preimages $\bigcap_i f^{-1}(S_i)$. In other words, \[ f^{-1}\left(\bigcap_i S_i\right) = \bigcap_i f^{-1}(S_i). \]

Submonoid.map_bot theorem

(f : F) : (⊥ : Submonoid M).map f = ⊥

Full source

@[to_additive (attr := simp)]
theorem map_bot (f : F) : (⊥ : Submonoid M).map f = ⊥ :=
  (gc_map_comap f).l_bot

Image of Trivial Submonoid is Trivial

Informal description

For any monoid homomorphism $f \colon M \to N$, the image of the trivial submonoid $\bot$ of $M$ under $f$ is the trivial submonoid $\bot$ of $N$.

Submonoid.comap_top theorem

(f : F) : (⊤ : Submonoid N).comap f = ⊤

Full source

@[to_additive (attr := simp)]
theorem comap_top (f : F) : (⊤ : Submonoid N).comap f = ⊤ :=
  (gc_map_comap f).u_top

Preimage of Top Submonoid is Top Submonoid

Informal description

For any monoid homomorphism $f \colon M \to N$, the preimage of the top submonoid of $N$ under $f$ is the top submonoid of $M$. In other words, $f^{-1}(N) = M$.

Submonoid.map_id theorem

(S : Submonoid M) : S.map (MonoidHom.id M) = S

Full source

@[to_additive (attr := simp)]
theorem map_id (S : Submonoid M) : S.map (MonoidHom.id M) = S :=
  ext fun _ => ⟨fun ⟨_, h, rfl⟩ => h, fun h => ⟨_, h, rfl⟩⟩

Image of Submonoid under Identity Homomorphism is Itself

Informal description

For any submonoid $S$ of a monoid $M$, the image of $S$ under the identity monoid homomorphism $\mathrm{id}_M \colon M \to M$ is equal to $S$ itself.

Submonoid.gciMapComap definition

(hf : Function.Injective f) : GaloisCoinsertion (map f) (comap f)

Full source

/-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective. -/
@[to_additive "`map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective."]
def gciMapComap (hf : Function.Injective f) : GaloisCoinsertion (map f) (comap f) :=
  (gc_map_comap f).toGaloisCoinsertion fun S x => by simp [mem_comap, mem_map, hf.eq_iff]

Galois coinsertion between image and preimage for injective monoid homomorphisms

Informal description

For an injective monoid homomorphism $ f : M \to N $, the pair of functions `map f` (image under $ f $) and `comap f` (preimage under $ f $) form a Galois coinsertion between the complete lattices of submonoids of $ M $ and $ N $. This means that for any submonoid $ S $ of $ M $, the preimage of the image of $ S $ under $ f $ is equal to $ S $ itself, i.e., $ f^{-1}(f(S)) = S $.

Submonoid.comap_map_eq_of_injective theorem

(S : Submonoid M) : (S.map f).comap f = S

Full source

@[to_additive]
theorem comap_map_eq_of_injective (S : Submonoid M) : (S.map f).comap f = S :=
  (gciMapComap hf).u_l_eq _

Preimage of Image Equals Original Submonoid for Injective Homomorphisms

Informal description

Let $f \colon M \to N$ be an injective monoid homomorphism and let $S$ be a submonoid of $M$. Then the preimage under $f$ of the image of $S$ under $f$ is equal to $S$ itself, i.e., $f^{-1}(f(S)) = S$.

Submonoid.comap_surjective_of_injective theorem

: Function.Surjective (comap f)

Full source

@[to_additive]
theorem comap_surjective_of_injective : Function.Surjective (comap f) :=
  (gciMapComap hf).u_surjective

Surjectivity of Submonoid Preimage for Injective Homomorphisms

Informal description

If a monoid homomorphism $f \colon M \to N$ is injective, then the preimage function $\mathrm{comap}\, f$ from submonoids of $N$ to submonoids of $M$ is surjective. That is, for every submonoid $S$ of $M$, there exists a submonoid $T$ of $N$ such that $S = f^{-1}(T)$.

Submonoid.map_injective_of_injective theorem

: Function.Injective (map f)

Full source

@[to_additive]
theorem map_injective_of_injective : Function.Injective (map f) :=
  (gciMapComap hf).l_injective

Injectivity of Submonoid Image Map for Injective Monoid Homomorphisms

Informal description

If $f \colon M \to N$ is an injective monoid homomorphism, then the induced map $\mathrm{map}_f$ from submonoids of $M$ to submonoids of $N$ is injective. That is, for any two submonoids $S, T \subseteq M$, if $\mathrm{map}_f(S) = \mathrm{map}_f(T)$, then $S = T$.

Submonoid.comap_inf_map_of_injective theorem

(S T : Submonoid M) : (S.map f ⊓ T.map f).comap f = S ⊓ T

Full source

@[to_additive]
theorem comap_inf_map_of_injective (S T : Submonoid M) : (S.map f ⊓ T.map f).comap f = S ⊓ T :=
  (gciMapComap hf).u_inf_l _ _

Preimage of Intersection of Images Equals Intersection for Injective Monoid Homomorphisms

Informal description

Let $f \colon M \to N$ be an injective monoid homomorphism, and let $S$ and $T$ be submonoids of $M$. Then the preimage under $f$ of the intersection of the images of $S$ and $T$ equals the intersection of $S$ and $T$, i.e., \[ f^{-1}(f(S) \cap f(T)) = S \cap T. \]

Submonoid.comap_iInf_map_of_injective theorem

(S : ι → Submonoid M) : (⨅ i, (S i).map f).comap f = iInf S

Full source

@[to_additive]
theorem comap_iInf_map_of_injective (S : ι → Submonoid M) : (⨅ i, (S i).map f).comap f = iInf S :=
  (gciMapComap hf).u_iInf_l _

Preimage of Infimum of Images Equals Infimum for Injective Monoid Homomorphism

Informal description

Let $M$ and $N$ be monoids, $f : M \to N$ an injective monoid homomorphism, and $(S_i)_{i \in \iota}$ a family of submonoids of $M$. Then the preimage under $f$ of the infimum of the images of the submonoids $S_i$ equals the infimum of the submonoids $S_i$: $$f^{-1}\left(\bigsqcap_{i} f(S_i)\right) = \bigsqcap_{i} S_i.$$

Submonoid.comap_sup_map_of_injective theorem

(S T : Submonoid M) : (S.map f ⊔ T.map f).comap f = S ⊔ T

Full source

@[to_additive]
theorem comap_sup_map_of_injective (S T : Submonoid M) : (S.map f ⊔ T.map f).comap f = S ⊔ T :=
  (gciMapComap hf).u_sup_l _ _

Preimage of Join of Images Equals Join for Injective Monoid Homomorphisms

Informal description

Let $f \colon M \to N$ be an injective monoid homomorphism, and let $S$ and $T$ be submonoids of $M$. Then the preimage under $f$ of the join (supremum) of the images of $S$ and $T$ is equal to the join of $S$ and $T$ in $M$, i.e., \[ f^{-1}(f(S) \vee f(T)) = S \vee T. \]

Submonoid.comap_iSup_map_of_injective theorem

(S : ι → Submonoid M) : (⨆ i, (S i).map f).comap f = iSup S

Full source

@[to_additive]
theorem comap_iSup_map_of_injective (S : ι → Submonoid M) : (⨆ i, (S i).map f).comap f = iSup S :=
  (gciMapComap hf).u_iSup_l _

Preimage of Supremum of Images Equals Supremum for Injective Monoid Homomorphism

Informal description

Let $f \colon M \to N$ be an injective monoid homomorphism and let $(S_i)_{i \in \iota}$ be a family of submonoids of $M$. Then the preimage under $f$ of the supremum of the images of $S_i$ equals the supremum of the submonoids $S_i$, i.e., \[ f^{-1}\left(\bigsqcup_i f(S_i)\right) = \bigsqcup_i S_i. \]

Submonoid.map_le_map_iff_of_injective theorem

{S T : Submonoid M} : S.map f ≤ T.map f ↔ S ≤ T

Full source

@[to_additive]
theorem map_le_map_iff_of_injective {S T : Submonoid M} : S.map f ≤ T.map f ↔ S ≤ T :=
  (gciMapComap hf).l_le_l_iff

Injective Monoid Homomorphism Preserves Submonoid Inclusion Order

Informal description

Let $f \colon M \to N$ be an injective monoid homomorphism, and let $S$ and $T$ be submonoids of $M$. The image of $S$ under $f$ is contained in the image of $T$ under $f$ if and only if $S$ is contained in $T$. In other words, $f(S) \subseteq f(T) \leftrightarrow S \subseteq T$.

Submonoid.map_strictMono_of_injective theorem

: StrictMono (map f)

Full source

@[to_additive]
theorem map_strictMono_of_injective : StrictMono (map f) :=
  (gciMapComap hf).strictMono_l

Strict Monotonicity of Submonoid Image under Injective Homomorphism

Informal description

If $f \colon M \to N$ is an injective monoid homomorphism, then the function that maps a submonoid $S$ of $M$ to its image $f(S)$ under $f$ is strictly monotone with respect to the inclusion order on submonoids. That is, for any two submonoids $S$ and $T$ of $M$, if $S \subseteq T$, then $f(S) \subseteq f(T)$, and the inclusion is strict if $S \subsetneq T$.

Submonoid.giMapComap definition

(hf : Function.Surjective f) : GaloisInsertion (map f) (comap f)

Full source

/-- `map f` and `comap f` form a `GaloisInsertion` when `f` is surjective. -/
@[to_additive "`map f` and `comap f` form a `GaloisInsertion` when `f` is surjective."]
def giMapComap (hf : Function.Surjective f) : GaloisInsertion (map f) (comap f) :=
  (gc_map_comap f).toGaloisInsertion fun S x h =>
    let ⟨y, hy⟩ := hf x
    mem_map.2 ⟨y, by simp [hy, h]⟩

Galois insertion between image and preimage of submonoids under a surjective homomorphism

Informal description

Given a surjective monoid homomorphism $ f : M \to N $, the pair of functions `map f` (image under $ f $) and `comap f` (preimage under $ f $) form a Galois insertion between the complete lattices of submonoids of $ M $ and $ N $. This means that for any submonoid $ S $ of $ N $, the image of its preimage under $ f $ is equal to $ S $ itself, i.e., $ f(f^{-1}(S)) = S $.

Submonoid.map_comap_eq_of_surjective theorem

(S : Submonoid N) : (S.comap f).map f = S

Full source

@[to_additive]
theorem map_comap_eq_of_surjective (S : Submonoid N) : (S.comap f).map f = S :=
  (giMapComap hf).l_u_eq _

Image of Preimage Equals Original for Surjective Monoid Homomorphism

Informal description

Let $f \colon M \to N$ be a surjective monoid homomorphism and let $S$ be a submonoid of $N$. Then the image under $f$ of the preimage of $S$ under $f$ equals $S$ itself, i.e., $f(f^{-1}(S)) = S$.

Submonoid.map_surjective_of_surjective theorem

: Function.Surjective (map f)

Full source

@[to_additive]
theorem map_surjective_of_surjective : Function.Surjective (map f) :=
  (giMapComap hf).l_surjective

Surjectivity of Submonoid Map Induced by a Surjective Homomorphism

Informal description

If a monoid homomorphism $f \colon M \to N$ is surjective, then the induced map on submonoids $S \mapsto f(S)$ is also surjective. That is, every submonoid of $N$ is the image under $f$ of some submonoid of $M$.

Submonoid.comap_injective_of_surjective theorem

: Function.Injective (comap f)

Full source

@[to_additive]
theorem comap_injective_of_surjective : Function.Injective (comap f) :=
  (giMapComap hf).u_injective

Injectivity of Submonoid Preimage under Surjective Homomorphism

Informal description

If a monoid homomorphism $f \colon M \to N$ is surjective, then the preimage map $\mathrm{comap}\, f$ from submonoids of $N$ to submonoids of $M$ is injective.

Submonoid.map_inf_comap_of_surjective theorem

(S T : Submonoid N) : (S.comap f ⊓ T.comap f).map f = S ⊓ T

Full source

@[to_additive]
theorem map_inf_comap_of_surjective (S T : Submonoid N) : (S.comap f ⊓ T.comap f).map f = S ⊓ T :=
  (giMapComap hf).l_inf_u _ _

Image of Intersection of Preimages Equals Intersection for Surjective Monoid Homomorphism

Informal description

Let $f \colon M \to N$ be a surjective monoid homomorphism, and let $S$ and $T$ be submonoids of $N$. Then the image under $f$ of the intersection of the preimages of $S$ and $T$ equals the intersection of $S$ and $T$, i.e., \[ f(f^{-1}(S) \cap f^{-1}(T)) = S \cap T. \]

Submonoid.map_iInf_comap_of_surjective theorem

(S : ι → Submonoid N) : (⨅ i, (S i).comap f).map f = iInf S

Full source

@[to_additive]
theorem map_iInf_comap_of_surjective (S : ι → Submonoid N) : (⨅ i, (S i).comap f).map f = iInf S :=
  (giMapComap hf).l_iInf_u _

Image of Infimum of Preimages Equals Infimum of Images for Surjective Monoid Homomorphism

Informal description

Let $f \colon M \to N$ be a surjective monoid homomorphism, and let $(S_i)_{i \in \iota}$ be a family of submonoids of $N$. Then the image under $f$ of the infimum of the preimages of the $S_i$ equals the infimum of the family $S_i$, i.e., \[ f\left(\bigcap_{i} f^{-1}(S_i)\right) = \bigcap_{i} S_i. \]

Submonoid.map_sup_comap_of_surjective theorem

(S T : Submonoid N) : (S.comap f ⊔ T.comap f).map f = S ⊔ T

Full source

@[to_additive]
theorem map_sup_comap_of_surjective (S T : Submonoid N) : (S.comap f ⊔ T.comap f).map f = S ⊔ T :=
  (giMapComap hf).l_sup_u _ _

Image of Supremum of Preimages Equals Supremum of Images for Surjective Monoid Homomorphism

Informal description

Let $f \colon M \to N$ be a surjective monoid homomorphism, and let $S, T$ be submonoids of $N$. Then the image under $f$ of the supremum of the preimages of $S$ and $T$ equals the supremum of $S$ and $T$, i.e., \[ f(f^{-1}(S) \sqcup f^{-1}(T)) = S \sqcup T. \]

Submonoid.map_iSup_comap_of_surjective theorem

(S : ι → Submonoid N) : (⨆ i, (S i).comap f).map f = iSup S

Full source

@[to_additive]
theorem map_iSup_comap_of_surjective (S : ι → Submonoid N) : (⨆ i, (S i).comap f).map f = iSup S :=
  (giMapComap hf).l_iSup_u _

Image of Supremum of Preimages Equals Supremum of Images for Surjective Monoid Homomorphism

Informal description

Let $f \colon M \to N$ be a surjective monoid homomorphism and let $(S_i)_{i \in \iota}$ be a family of submonoids of $N$. Then the image under $f$ of the supremum of the preimages $(f^{-1}(S_i))_{i \in \iota}$ equals the supremum of the family $(S_i)_{i \in \iota}$. In symbols: \[ f\left(\bigsqcup_{i \in \iota} f^{-1}(S_i)\right) = \bigsqcup_{i \in \iota} S_i. \]

Submonoid.comap_le_comap_iff_of_surjective theorem

{S T : Submonoid N} : S.comap f ≤ T.comap f ↔ S ≤ T

Full source

@[to_additive]
theorem comap_le_comap_iff_of_surjective {S T : Submonoid N} : S.comap f ≤ T.comap f ↔ S ≤ T :=
  (giMapComap hf).u_le_u_iff

Preimage Order Preserving under Surjective Homomorphism

Informal description

Let $f \colon M \to N$ be a surjective monoid homomorphism, and let $S$ and $T$ be submonoids of $N$. Then the preimage of $S$ under $f$ is contained in the preimage of $T$ under $f$ if and only if $S$ is contained in $T$. In other words, $f^{-1}(S) \leq f^{-1}(T) \leftrightarrow S \leq T$.

Submonoid.comap_strictMono_of_surjective theorem

: StrictMono (comap f)

Full source

@[to_additive]
theorem comap_strictMono_of_surjective : StrictMono (comap f) :=
  (giMapComap hf).strictMono_u

Strict Monotonicity of Submonoid Preimage under Surjective Homomorphism

Informal description

Given a surjective monoid homomorphism $f \colon M \to N$, the function that maps each submonoid $S$ of $N$ to its preimage $f^{-1}(S)$ in $M$ is strictly monotone. That is, for any two submonoids $S$ and $T$ of $N$, if $S \subseteq T$, then $f^{-1}(S) \subseteq f^{-1}(T)$, and the inclusion is strict if $S \subsetneq T$.

Submonoid.topEquiv definition

: (⊤ : Submonoid M) ≃* M

Full source

/-- The top submonoid is isomorphic to the monoid. -/
@[to_additive (attr := simps) "The top additive submonoid is isomorphic to the additive monoid."]
def topEquiv : (⊤ : Submonoid M) ≃* M where
  toFun x := x
  invFun x := ⟨x, mem_top x⟩
  left_inv x := x.eta _
  right_inv _ := rfl
  map_mul' _ _ := rfl

Isomorphism between top submonoid and monoid

Informal description

The monoid isomorphism between the top submonoid (the entire monoid) and the monoid itself, where the isomorphism maps each element to itself and its inverse maps each element to the corresponding element in the top submonoid.

Submonoid.topEquiv_toMonoidHom theorem

: ((topEquiv : _ ≃* M) : _ →* M) = (⊤ : Submonoid M).subtype

Full source

@[to_additive (attr := simp)]
theorem topEquiv_toMonoidHom : ((topEquiv : _ ≃* M) : _ →* M) = (⊤ : Submonoid M).subtype :=
  rfl

Top Submonoid Isomorphism Yields Inclusion Homomorphism

Informal description

The monoid homomorphism obtained from the isomorphism `topEquiv` between the top submonoid of $M$ and $M$ itself is equal to the inclusion homomorphism of the top submonoid into $M$.

Submonoid.equivMapOfInjective definition

(f : M →* N) (hf : Function.Injective f) : S ≃* S.map f

Full source

/-- A subgroup is isomorphic to its image under an injective function. If you have an isomorphism,
use `MulEquiv.submonoidMap` for better definitional equalities. -/
@[to_additive "An additive subgroup is isomorphic to its image under an injective function. If you
have an isomorphism, use `AddEquiv.addSubmonoidMap` for better definitional equalities."]
noncomputable def equivMapOfInjective (f : M →* N) (hf : Function.Injective f) : S ≃* S.map f :=
  { Equiv.Set.image f S hf with map_mul' := fun _ _ => Subtype.ext (f.map_mul _ _) }

Isomorphism between a submonoid and its image under an injective homomorphism

Informal description

Given an injective monoid homomorphism $ f \colon M \to N $ and a submonoid $ S $ of $ M $, there is a monoid isomorphism between $ S $ and its image $ f(S) $ under $ f $. The isomorphism maps each $ x \in S $ to $ f(x) \in f(S) $, and its inverse maps each $ y \in f(S) $ to the unique $ x \in S $ such that $ f(x) = y $.

Submonoid.coe_equivMapOfInjective_apply theorem

(f : M →* N) (hf : Function.Injective f) (x : S) : (equivMapOfInjective S f hf x : N) = f x

Full source

@[to_additive (attr := simp)]
theorem coe_equivMapOfInjective_apply (f : M →* N) (hf : Function.Injective f) (x : S) :
    (equivMapOfInjective S f hf x : N) = f x :=
  rfl

Image of Submonoid Element under Injective Homomorphism Equals Original Image

Informal description

Let $f \colon M \to N$ be an injective monoid homomorphism and let $S$ be a submonoid of $M$. For any element $x \in S$, the image of $x$ under the isomorphism $\text{equivMapOfInjective}\, S\, f\, hf$ (from $S$ to $f(S)$) is equal to $f(x)$ in $N$.

Submonoid.closure_closure_coe_preimage theorem

{s : Set M} : closure (((↑) : closure s → M) ⁻¹' s) = ⊤

Full source

@[to_additive (attr := simp)]
theorem closure_closure_coe_preimage {s : Set M} : closure (((↑) : closure s → M) ⁻¹' s) = ⊤ :=
  eq_top_iff.2 fun x _ ↦ Subtype.recOn x fun _ hx' ↦
    closure_induction (fun _ h ↦ subset_closure h) (one_mem _) (fun _ _ _ _ ↦ mul_mem) hx'

Closure of Preimage in Generated Submonoid Equals Trivial Submonoid

Informal description

For any subset $s$ of a monoid $M$, the submonoid generated by the preimage of $s$ under the natural inclusion map from the submonoid closure of $s$ to $M$ is equal to the trivial submonoid (the entire closure submonoid).

Submonoid.prod definition

(s : Submonoid M) (t : Submonoid N) : Submonoid (M × N)

Full source

/-- Given submonoids `s`, `t` of monoids `M`, `N` respectively, `s × t` as a submonoid
of `M × N`. -/
@[to_additive prod
      "Given `AddSubmonoid`s `s`, `t` of `AddMonoid`s `A`, `B` respectively, `s × t`
      as an `AddSubmonoid` of `A × B`."]
def prod (s : Submonoid M) (t : Submonoid N) :
    Submonoid (M × N) where
  carrier := s ×ˢ t
  one_mem' := ⟨s.one_mem, t.one_mem⟩
  mul_mem' hp hq := ⟨s.mul_mem hp.1 hq.1, t.mul_mem hp.2 hq.2⟩

Product of submonoids

Informal description

Given submonoids $s$ of a monoid $M$ and $t$ of a monoid $N$, the product submonoid $s \times t$ is defined as the submonoid of $M \times N$ consisting of all pairs $(m, n)$ where $m \in s$ and $n \in t$. This submonoid contains the identity element $(1, 1)$ and is closed under multiplication.

Submonoid.coe_prod theorem

(s : Submonoid M) (t : Submonoid N) : (s.prod t : Set (M × N)) = (s : Set M) ×ˢ (t : Set N)

Full source

@[to_additive coe_prod]
theorem coe_prod (s : Submonoid M) (t : Submonoid N) :
    (s.prod t : Set (M × N)) = (s : Set M) ×ˢ (t : Set N) :=
  rfl

Underlying Set of Product Submonoid Equals Cartesian Product of Underlying Sets

Informal description

For any submonoids $s$ of a monoid $M$ and $t$ of a monoid $N$, the underlying set of the product submonoid $s \times t$ is equal to the Cartesian product of the underlying sets of $s$ and $t$, i.e., $(s \times t) = s \timesˢ t$.

Submonoid.mem_prod theorem

{s : Submonoid M} {t : Submonoid N} {p : M × N} : p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t

Full source

@[to_additive mem_prod]
theorem mem_prod {s : Submonoid M} {t : Submonoid N} {p : M × N} :
    p ∈ s.prod tp ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t :=
  Iff.rfl

Membership Criterion for Product Submonoid

Informal description

For submonoids $s$ of a monoid $M$ and $t$ of a monoid $N$, and for any element $p = (m, n) \in M \times N$, we have $p \in s \times t$ if and only if $m \in s$ and $n \in t$.

Submonoid.prod_mono theorem

 {s₁ s₂ : Submonoid M} {t₁ t₂ : Submonoid N} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) : s₁.prod t₁ ≤ s₂.prod t₂

Full source

@[to_additive prod_mono]
theorem prod_mono {s₁ s₂ : Submonoid M} {t₁ t₂ : Submonoid N} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :
    s₁.prod t₁ ≤ s₂.prod t₂ :=
  Set.prod_mono hs ht

Monotonicity of Submonoid Product with Respect to Inclusion

Informal description

For any submonoids $s_1, s_2$ of a monoid $M$ and $t_1, t_2$ of a monoid $N$, if $s_1 \subseteq s_2$ and $t_1 \subseteq t_2$, then the product submonoid $s_1 \times t_1$ is contained in the product submonoid $s_2 \times t_2$.

Submonoid.prod_top theorem

(s : Submonoid M) : s.prod (⊤ : Submonoid N) = s.comap (MonoidHom.fst M N)

Full source

@[to_additive prod_top]
theorem prod_top (s : Submonoid M) : s.prod (⊤ : Submonoid N) = s.comap (MonoidHom.fst M N) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_fst]

Product Submonoid with Full Submonoid Equals Preimage under First Projection

Informal description

For any submonoid $s$ of a monoid $M$, the product submonoid $s \times N$ (where $N$ is the full submonoid of $N$) is equal to the preimage of $s$ under the first projection homomorphism $\pi_1 \colon M \times N \to M$.

Submonoid.top_prod theorem

(s : Submonoid N) : (⊤ : Submonoid M).prod s = s.comap (MonoidHom.snd M N)

Full source

@[to_additive top_prod]
theorem top_prod (s : Submonoid N) : (⊤ : Submonoid M).prod s = s.comap (MonoidHom.snd M N) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_snd]

Product of Top Submonoid with a Submonoid Equals Preimage under Second Projection

Informal description

For any submonoid $s$ of a monoid $N$, the product of the top submonoid of $M$ (i.e., the entire monoid $M$) with $s$ is equal to the preimage of $s$ under the second projection monoid homomorphism $\operatorname{snd} \colon M \times N \to N$.

Submonoid.top_prod_top theorem

: (⊤ : Submonoid M).prod (⊤ : Submonoid N) = ⊤

Full source

@[to_additive (attr := simp) top_prod_top]
theorem top_prod_top : (⊤ : Submonoid M).prod (⊤ : Submonoid N) = ⊤ :=
  (top_prod _).trans <| comap_top _

Product of Top Submonoids is Top Submonoid of Product

Informal description

The product of the top submonoid of a monoid $M$ and the top submonoid of a monoid $N$ is equal to the top submonoid of the product monoid $M \times N$.

Submonoid.bot_prod_bot theorem

: (⊥ : Submonoid M).prod (⊥ : Submonoid N) = ⊥

Full source

@[to_additive bot_prod_bot]
theorem bot_prod_bot : (⊥ : Submonoid M).prod (⊥ : Submonoid N) = ⊥ :=
  SetLike.coe_injective <| by simp [coe_prod]

Product of Trivial Submonoids is Trivial

Informal description

The product of the trivial submonoids of $M$ and $N$ is equal to the trivial submonoid of $M \times N$, i.e., $\bot \times \bot = \bot$ where $\bot$ denotes the trivial submonoid in each case.

Submonoid.prodEquiv definition

(s : Submonoid M) (t : Submonoid N) : s.prod t ≃* s × t

Full source

/-- The product of submonoids is isomorphic to their product as monoids. -/
@[to_additive prodEquiv
      "The product of additive submonoids is isomorphic to their product as additive monoids"]
def prodEquiv (s : Submonoid M) (t : Submonoid N) : s.prod t ≃* s × t :=
  { (Equiv.Set.prod (s : Set M) (t : Set N)) with
    map_mul' := fun _ _ => rfl }

Isomorphism between product submonoid and direct product of submonoids

Informal description

Given submonoids $s$ of a monoid $M$ and $t$ of a monoid $N$, the product submonoid $s \times t$ is isomorphic as a monoid to the direct product of the submonoids $s$ and $t$. The isomorphism is given by the natural equivalence between the underlying sets.

Submonoid.map_inl theorem

(s : Submonoid M) : s.map (inl M N) = s.prod ⊥

Full source

@[to_additive]
theorem map_inl (s : Submonoid M) : s.map (inl M N) = s.prod ⊥ :=
  ext fun p =>
    ⟨fun ⟨_, hx, hp⟩ => hp ▸ ⟨hx, Set.mem_singleton 1⟩, fun ⟨hps, hp1⟩ =>
      ⟨p.1, hps, Prod.ext rfl <| (Set.eq_of_mem_singleton hp1).symm⟩⟩

Image of Submonoid under Left Inclusion Equals Product with Trivial Submonoid

Informal description

For any submonoid $s$ of a monoid $M$, the image of $s$ under the left inclusion homomorphism $\mathrm{inl} \colon M \to M \times N$ is equal to the product submonoid $s \times \{\bot\}$, where $\bot$ denotes the trivial submonoid of $N$.

Submonoid.map_inr theorem

(s : Submonoid N) : s.map (inr M N) = prod ⊥ s

Full source

@[to_additive]
theorem map_inr (s : Submonoid N) : s.map (inr M N) = prod ⊥ s :=
  ext fun p =>
    ⟨fun ⟨_, hx, hp⟩ => hp ▸ ⟨Set.mem_singleton 1, hx⟩, fun ⟨hp1, hps⟩ =>
      ⟨p.2, hps, Prod.ext (Set.eq_of_mem_singleton hp1).symm rfl⟩⟩

Image of Submonoid under Right Inclusion Equals Product with Trivial Submonoid

Informal description

For any submonoid $s$ of a monoid $N$, the image of $s$ under the inclusion homomorphism $\text{inr} \colon N \to M \times N$ (which maps $y \in N$ to $(1, y)$ where $1$ is the identity of $M$) is equal to the product submonoid $\{1\} \times s$ in $M \times N$.

Submonoid.prod_bot_sup_bot_prod theorem

(s : Submonoid M) (t : Submonoid N) : (prod s ⊥) ⊔ (prod ⊥ t) = prod s t

Full source

@[to_additive (attr := simp) prod_bot_sup_bot_prod]
theorem prod_bot_sup_bot_prod (s : Submonoid M) (t : Submonoid N) :
    (prod s ⊥) ⊔ (prod ⊥ t) = prod s t :=
  (le_antisymm (sup_le (prod_mono (le_refl s) bot_le) (prod_mono bot_le (le_refl t))))
    fun p hp => Prod.fst_mul_snd p ▸ mul_mem
        ((le_sup_left : prod s ⊥ ≤ prodprod s ⊥ ⊔ prod ⊥ t) ⟨hp.1, Set.mem_singleton 1⟩)
        ((le_sup_right : prod ⊥ t ≤ prodprod s ⊥ ⊔ prod ⊥ t) ⟨Set.mem_singleton 1, hp.2⟩)

Supremum of Trivial Product Submonoids Equals Full Product Submonoid

Informal description

For any submonoid $s$ of a monoid $M$ and any submonoid $t$ of a monoid $N$, the supremum of the product submonoids $s \times \{\bot\}$ and $\{\bot\} \times t$ is equal to the product submonoid $s \times t$, i.e., \[ (s \times \{\bot\}) \sqcup (\{\bot\} \times t) = s \times t. \]

Submonoid.mem_map_equiv theorem

{f : M ≃* N} {K : Submonoid M} {x : N} : x ∈ K.map f.toMonoidHom ↔ f.symm x ∈ K

Full source

@[to_additive]
theorem mem_map_equiv {f : M ≃* N} {K : Submonoid M} {x : N} :
    x ∈ K.map f.toMonoidHomx ∈ K.map f.toMonoidHom ↔ f.symm x ∈ K :=
  Set.mem_image_equiv

Characterization of Image Membership via Monoid Isomorphism Inverse

Informal description

Let $f \colon M \to N$ be a monoid isomorphism, $K$ a submonoid of $M$, and $x \in N$. Then $x$ belongs to the image of $K$ under $f$ if and only if $f^{-1}(x)$ belongs to $K$, i.e., \[ x \in f(K) \leftrightarrow f^{-1}(x) \in K. \]

Submonoid.map_equiv_eq_comap_symm theorem

(f : M ≃* N) (K : Submonoid M) : K.map f = K.comap f.symm

Full source

@[to_additive]
theorem map_equiv_eq_comap_symm (f : M ≃* N) (K : Submonoid M) :
    K.map f = K.comap f.symm :=
  SetLike.coe_injective (f.toEquiv.image_eq_preimage K)

Image of Submonoid under Isomorphism Equals Preimage under Inverse

Informal description

For any monoid isomorphism $f \colon M \simeq N$ and any submonoid $K$ of $M$, the image of $K$ under $f$ is equal to the preimage of $K$ under the inverse isomorphism $f^{-1}$, i.e., \[ f(K) = f^{-1}^{-1}(K). \]

Submonoid.comap_equiv_eq_map_symm theorem

(f : N ≃* M) (K : Submonoid M) : K.comap f = K.map f.symm

Full source

@[to_additive]
theorem comap_equiv_eq_map_symm (f : N ≃* M) (K : Submonoid M) :
    K.comap f = K.map f.symm :=
  (map_equiv_eq_comap_symm f.symm K).symm

Preimage-Image Duality for Submonoids under Monoid Isomorphism

Informal description

For any monoid isomorphism $f \colon N \simeq M$ and any submonoid $K$ of $M$, the preimage of $K$ under $f$ is equal to the image of $K$ under the inverse isomorphism $f^{-1}$, i.e., \[ f^{-1}(K) = f^{-1}(K). \]

Submonoid.map_equiv_top theorem

(f : M ≃* N) : (⊤ : Submonoid M).map f = ⊤

Full source

@[to_additive (attr := simp)]
theorem map_equiv_top (f : M ≃* N) : (⊤ : Submonoid M).map f = ⊤ :=
  SetLike.coe_injective <| Set.image_univ.trans f.surjective.range_eq

Image of Top Submonoid under Monoid Isomorphism is Top Submonoid

Informal description

For any monoid isomorphism $f \colon M \cong N$, the image of the top submonoid of $M$ under $f$ is equal to the top submonoid of $N$. In other words, $f(\top_M) = \top_N$.

Submonoid.le_prod_iff theorem

 {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} : u ≤ s.prod t ↔ u.map (fst M N) ≤ s ∧ u.map (snd M N) ≤ t

Full source

@[to_additive le_prod_iff]
theorem le_prod_iff {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} :
    u ≤ s.prod t ↔ u.map (fst M N) ≤ s ∧ u.map (snd M N) ≤ t := by
  constructor
  · intro h
    constructor
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).1
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).2
  · rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
    exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

Criterion for Submonoid Containment in Product: $u \leq s \times t \leftrightarrow \pi_1(u) \leq s \land \pi_2(u) \leq t$

Informal description

Let $M$ and $N$ be monoids, with submonoids $s \subseteq M$, $t \subseteq N$, and $u \subseteq M \times N$. Then $u$ is contained in the product submonoid $s \times t$ if and only if the image of $u$ under the first projection is contained in $s$ and the image of $u$ under the second projection is contained in $t$. In other words: $$u \leq s \times t \leftrightarrow \pi_1(u) \leq s \land \pi_2(u) \leq t$$ where $\pi_1: M \times N \to M$ and $\pi_2: M \times N \to N$ are the projection homomorphisms.

Submonoid.prod_le_iff theorem

 {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} : s.prod t ≤ u ↔ s.map (inl M N) ≤ u ∧ t.map (inr M N) ≤ u

Full source

@[to_additive prod_le_iff]
theorem prod_le_iff {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} :
    s.prod t ≤ u ↔ s.map (inl M N) ≤ u ∧ t.map (inr M N) ≤ u := by
  constructor
  · intro h
    constructor
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨hx, Submonoid.one_mem _⟩
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨Submonoid.one_mem _, hx⟩
  · rintro ⟨hH, hK⟩ ⟨x1, x2⟩ ⟨h1, h2⟩
    have h1' : inlinl M N x1 ∈ u := by
      apply hH
      simpa using h1
    have h2' : inrinr M N x2 ∈ u := by
      apply hK
      simpa using h2
    simpa using Submonoid.mul_mem _ h1' h2'

Product Submonoid Containment Criterion via Inclusion Maps

Informal description

For submonoids $s$ of $M$, $t$ of $N$, and $u$ of $M \times N$, the product submonoid $s \times t$ is contained in $u$ if and only if the image of $s$ under the left inclusion homomorphism $M \to M \times N$ is contained in $u$ and the image of $t$ under the right inclusion homomorphism $N \to M \times N$ is contained in $u$.

Submonoid.closure_prod theorem

{s : Set M} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) : closure (s ×ˢ t) = (closure s).prod (closure t)

Full source

@[to_additive closure_prod]
theorem closure_prod {s : Set M} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) :
    closure (s ×ˢ t) = (closure s).prod (closure t) :=
  le_antisymm
    (closure_le.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, subset_closure⟩)
    (prod_le_iff.2 ⟨
      map_le_of_le_comap _ <| closure_le.2 fun _x hx => subset_closure ⟨hx, ht⟩,
      map_le_of_le_comap _ <| closure_le.2 fun _y hy => subset_closure ⟨hs, hy⟩⟩)

Closure of Cartesian Product of Submonoid Generators Equals Product of Closures

Informal description

For any subsets $s \subseteq M$ and $t \subseteq N$ of monoids $M$ and $N$ respectively, if $1 \in s$ and $1 \in t$, then the submonoid generated by the Cartesian product $s \times t$ is equal to the product of the submonoids generated by $s$ and $t$: $$\text{closure}(s \times t) = \text{closure}(s) \times \text{closure}(t)$$

Submonoid.closure_prod_one theorem

(s : Set M) : closure (s ×ˢ ({ 1 } : Set N)) = (closure s).prod ⊥

Full source

@[to_additive (attr := simp) closure_prod_zero]
lemma closure_prod_one (s : Set M) : closure (s ×ˢ ({1} : Set N)) = (closure s).prod ⊥ :=
  le_antisymm
    (closure_le.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨subset_closure, .rfl⟩)
    (prod_le_iff.2 ⟨
      map_le_of_le_comap _ <| closure_le.2 fun _x hx => subset_closure ⟨hx, rfl⟩,
      by simp⟩)

Submonoid Generation of Product with Identity: $\text{closure}(s \times \{1\}) = \text{closure}(s) \times \bot$

Informal description

For any subset $s$ of a monoid $M$, the submonoid generated by the product set $s \times \{1\}$ in $M \times N$ is equal to the product of the submonoid generated by $s$ in $M$ and the trivial submonoid $\bot$ in $N$. In symbols: $$\text{closure}(s \times \{1\}) = \text{closure}(s) \times \bot$$

Submonoid.closure_one_prod theorem

(t : Set N) : closure (({ 1 } : Set M) ×ˢ t) = .prod ⊥ (closure t)

Full source

@[to_additive (attr := simp) closure_zero_prod]
lemma closure_one_prod (t : Set N) : closure (({1} : Set M) ×ˢ t) = .prod ⊥ (closure t) :=
  le_antisymm
    (closure_le.2 <| Set.prod_subset_prod_iff.2 <| .inl ⟨.rfl, subset_closure⟩)
    (prod_le_iff.2 ⟨by simp,
      map_le_of_le_comap _ <| closure_le.2 fun _y hy => subset_closure ⟨rfl, hy⟩⟩)

Submonoid Generation of $\{1\} \times t$ Equals Trivial Submonoid Product with $\text{closure}(t)$

Informal description

For any subset $t$ of a monoid $N$, the submonoid generated by the Cartesian product $\{1\} \times t$ in $M \times N$ is equal to the product of the trivial submonoid of $M$ and the submonoid generated by $t$ in $N$. In symbols: $$\text{closure}(\{1\} \times t) = \bot \times \text{closure}(t)$$ where $\bot$ denotes the trivial submonoid of $M$.

MonoidHom.mrange definition

(f : F) : Submonoid N

Full source

/-- The range of a monoid homomorphism is a submonoid. See Note [range copy pattern]. -/
@[to_additive "The range of an `AddMonoidHom` is an `AddSubmonoid`."]
def mrange (f : F) : Submonoid N :=
  ((⊤ : Submonoid M).map f).copy (Set.range f) Set.image_univ.symm

Range of a monoid homomorphism

Informal description

The range of a monoid homomorphism $f \colon M \to N$ is the submonoid of $N$ consisting of all elements that are images of elements of $M$ under $f$.

MonoidHom.coe_mrange theorem

(f : F) : (mrange f : Set N) = Set.range f

Full source

@[to_additive (attr := simp)]
theorem coe_mrange (f : F) : (mrange f : Set N) = Set.range f :=
  rfl

Equality of Monoid Homomorphism Range as Submonoid and as Set

Informal description

For any monoid homomorphism $f \colon M \to N$, the underlying set of the range of $f$ (as a submonoid of $N$) is equal to the range of $f$ as a function (i.e., the set of all images of elements of $M$ under $f$). In symbols: $$ \text{mrange}(f) = \text{range}(f) $$ where $\text{mrange}(f)$ denotes the range as a submonoid and $\text{range}(f)$ denotes the range as a set.

MonoidHom.mem_mrange theorem

{f : F} {y : N} : y ∈ mrange f ↔ ∃ x, f x = y

Full source

@[to_additive (attr := simp)]
theorem mem_mrange {f : F} {y : N} : y ∈ mrange fy ∈ mrange f ↔ ∃ x, f x = y :=
  Iff.rfl

Characterization of Elements in the Range of a Monoid Homomorphism

Informal description

For a monoid homomorphism $f \colon M \to N$ and an element $y \in N$, $y$ belongs to the range of $f$ if and only if there exists an element $x \in M$ such that $f(x) = y$. In symbols: $$ y \in \text{mrange}(f) \leftrightarrow \exists x \in M, f(x) = y $$

MonoidHom.mrange_comp theorem

{O : Type*} [MulOneClass O] (f : N →* O) (g : M →* N) : mrange (f.comp g) = (mrange g).map f

Full source

@[to_additive]
lemma mrange_comp {O : Type*} [MulOneClass O] (f : N →* O) (g : M →* N) :
    mrange (f.comp g) = (mrange g).map f := SetLike.coe_injective <| Set.range_comp f _

Range of Composition of Monoid Homomorphisms Equals Image of Range

Informal description

Let $M$, $N$, and $O$ be monoids, and let $f \colon N \to O$ and $g \colon M \to N$ be monoid homomorphisms. Then the range of the composition $f \circ g$ is equal to the image of the range of $g$ under $f$. In symbols: $$ \text{mrange}(f \circ g) = f(\text{mrange}(g)) $$

MonoidHom.mrange_eq_map theorem

(f : F) : mrange f = (⊤ : Submonoid M).map f

Full source

@[to_additive]
theorem mrange_eq_map (f : F) : mrange f = (⊤ : Submonoid M).map f :=
  Submonoid.copy_eq _

Range of a Monoid Homomorphism as Image of the Top Submonoid

Informal description

For any monoid homomorphism $f \colon M \to N$, the range of $f$ is equal to the image of the top submonoid of $M$ under $f$. That is, $\mathrm{range}(f) = f(\top_M)$, where $\top_M$ denotes the maximal submonoid of $M$.

MonoidHom.mrange_id theorem

: mrange (MonoidHom.id M) = ⊤

Full source

@[to_additive (attr := simp)]
theorem mrange_id : mrange (MonoidHom.id M) = ⊤ := by
  simp [mrange_eq_map]

Range of Identity Monoid Homomorphism is Top Submonoid

Informal description

The range of the identity monoid homomorphism $\mathrm{id}_M \colon M \to M$ is equal to the top submonoid of $M$, i.e., $\mathrm{range}(\mathrm{id}_M) = \top_M$.

MonoidHom.map_mrange theorem

(g : N →* P) (f : M →* N) : (mrange f).map g = mrange (comp g f)

Full source

@[to_additive]
theorem map_mrange (g : N →* P) (f : M →* N) : (mrange f).map g = mrange (comp g f) := by
  simpa only [mrange_eq_map] using (⊤ : Submonoid M).map_map g f

Range Image under Composition of Monoid Homomorphisms

Informal description

Let $M$, $N$, and $P$ be monoids, and let $f \colon M \to N$ and $g \colon N \to P$ be monoid homomorphisms. The image under $g$ of the range of $f$ is equal to the range of the composition $g \circ f$. That is, $g(\mathrm{range}(f)) = \mathrm{range}(g \circ f)$.

MonoidHom.mrange_eq_top theorem

{f : F} : mrange f = (⊤ : Submonoid N) ↔ Surjective f

Full source

@[to_additive]
theorem mrange_eq_top {f : F} : mrangemrange f = (⊤ : Submonoid N) ↔ Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_mrange, coe_top]) Set.range_eq_univ

Range of Monoid Homomorphism is Entire Codomain if and only if Surjective

Informal description

For a monoid homomorphism $f \colon M \to N$, the range of $f$ is equal to the entire submonoid $N$ if and only if $f$ is surjective. In symbols: $$ \text{mrange}(f) = N \leftrightarrow \text{Surjective}(f) $$

MonoidHom.mrange_eq_top_of_surjective theorem

(f : F) (hf : Function.Surjective f) : mrange f = (⊤ : Submonoid N)

Full source

/-- The range of a surjective monoid hom is the whole of the codomain. -/
@[to_additive (attr := simp)
  "The range of a surjective `AddMonoid` hom is the whole of the codomain."]
theorem mrange_eq_top_of_surjective (f : F) (hf : Function.Surjective f) :
    mrange f = (⊤ : Submonoid N) :=
  mrange_eq_top.2 hf

Surjective Monoid Homomorphism has Full Range

Informal description

For a monoid homomorphism $f \colon M \to N$, if $f$ is surjective, then the range of $f$ is equal to the entire codomain $N$ (as a submonoid). In symbols: $$ \text{range}(f) = N $$

MonoidHom.mclosure_preimage_le theorem

(f : F) (s : Set N) : closure (f ⁻¹' s) ≤ (closure s).comap f

Full source

@[to_additive]
theorem mclosure_preimage_le (f : F) (s : Set N) : closure (f ⁻¹' s) ≤ (closure s).comap f :=
  closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

Submonoid Closure of Preimage is Contained in Preimage of Closure

Informal description

For a monoid homomorphism $f \colon M \to N$ and a subset $s \subseteq N$, the submonoid generated by the preimage $f^{-1}(s)$ is contained in the preimage of the submonoid generated by $s$ under $f$. In symbols: $$\text{closure}(f^{-1}(s)) \leq f^{-1}(\text{closure}(s))$$

MonoidHom.map_mclosure theorem

(f : F) (s : Set M) : (closure s).map f = closure (f '' s)

Full source

/-- The image under a monoid hom of the submonoid generated by a set equals the submonoid generated
    by the image of the set. -/
@[to_additive
      "The image under an `AddMonoid` hom of the `AddSubmonoid` generated by a set equals
      the `AddSubmonoid` generated by the image of the set."]
theorem map_mclosure (f : F) (s : Set M) : (closure s).map f = closure (f '' s) :=
  Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Submonoid.gi N).gc (Submonoid.gi M).gc
    fun _ ↦ rfl

Image of Generated Submonoid Equals Generated Image Submonoid

Informal description

Let $M$ and $N$ be monoids, $f : M \to N$ a monoid homomorphism, and $s \subseteq M$ a subset. The image under $f$ of the submonoid generated by $s$ equals the submonoid generated by the image $f(s)$ of $s$ under $f$. In symbols: $$ f(\langle s \rangle) = \langle f(s) \rangle $$ where $\langle \cdot \rangle$ denotes the submonoid generated by a set.

MonoidHom.mclosure_range theorem

(f : F) : closure (Set.range f) = mrange f

Full source

@[to_additive (attr := simp)]
theorem mclosure_range (f : F) : closure (Set.range f) = mrange f := by
  rw [← Set.image_univ, ← map_mclosure, mrange_eq_map, closure_univ]

Range of Monoid Homomorphism is Closed Under Generation

Informal description

For any monoid homomorphism $f \colon M \to N$, the submonoid generated by the range of $f$ equals the range of $f$ as a submonoid of $N$. In symbols: $$ \langle \mathrm{range}(f) \rangle = \mathrm{range}(f) $$

MonoidHom.restrict definition

{N S : Type*} [MulOneClass N] [SetLike S M] [SubmonoidClass S M] (f : M →* N) (s : S) : s →* N

Full source

/-- Restriction of a monoid hom to a submonoid of the domain. -/
@[to_additive "Restriction of an `AddMonoid` hom to an `AddSubmonoid` of the domain."]
def restrict {N S : Type*} [MulOneClass N] [SetLike S M] [SubmonoidClass S M] (f : M →* N)
    (s : S) : s →* N :=
  f.comp (SubmonoidClass.subtype _)

Restriction of a monoid homomorphism to a submonoid

Informal description

Given a monoid homomorphism $ f \colon M \to N $ and a submonoid $ S $ of $ M $, the restriction of $ f $ to $ S $ is a monoid homomorphism from $ S $ to $ N $, obtained by composing $ f $ with the inclusion map $ S \hookrightarrow M $.

MonoidHom.restrict_apply theorem

{N S : Type*} [MulOneClass N] [SetLike S M] [SubmonoidClass S M] (f : M →* N) (s : S) (x : s) : f.restrict s x = f x

Full source

@[to_additive (attr := simp)]
theorem restrict_apply {N S : Type*} [MulOneClass N] [SetLike S M] [SubmonoidClass S M]
    (f : M →* N) (s : S) (x : s) : f.restrict s x = f x :=
  rfl

Restriction of Monoid Homomorphism Preserves Evaluation

Informal description

Let $M$ and $N$ be monoids, $S$ a submonoid of $M$, and $f \colon M \to N$ a monoid homomorphism. For any $x \in S$, the restriction of $f$ to $S$ evaluated at $x$ equals $f(x)$, i.e., $f|_S(x) = f(x)$.

MonoidHom.restrict_mrange theorem

(f : M →* N) : mrange (f.restrict S) = S.map f

Full source

@[to_additive (attr := simp)]
theorem restrict_mrange (f : M →* N) : mrange (f.restrict S) = S.map f := by
  simp [SetLike.ext_iff]

Range-Restriction Equality for Monoid Homomorphisms

Informal description

For any monoid homomorphism $f \colon M \to N$ and any submonoid $S$ of $M$, the range of the restriction of $f$ to $S$ equals the image of $S$ under $f$.

MonoidHom.codRestrict definition

{S} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ x, f x ∈ s) : M →* s

Full source

/-- Restriction of a monoid hom to a submonoid of the codomain. -/
@[to_additive (attr := simps apply)
  "Restriction of an `AddMonoid` hom to an `AddSubmonoid` of the codomain."]
def codRestrict {S} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ x, f x ∈ s) :
    M →* s where
  toFun n := ⟨f n, h n⟩
  map_one' := Subtype.eq f.map_one
  map_mul' x y := Subtype.eq (f.map_mul x y)

Restriction of a monoid homomorphism to a submonoid of the codomain

Informal description

Given a monoid homomorphism $ f \colon M \to N $ and a submonoid $ s $ of $ N $ such that $ f(x) \in s $ for all $ x \in M $, the function `MonoidHom.codRestrict` restricts the codomain of $ f $ to $ s $, yielding a monoid homomorphism $ M \to s $. This is defined by mapping each $ n \in M $ to $ \langle f(n), h(n) \rangle $, where $ h $ is the proof that $ f(n) \in s $, and preserving the monoid structure (identity and multiplication).

MonoidHom.injective_codRestrict theorem

 {S} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ x, f x ∈ s) :
  Function.Injective (f.codRestrict s h) ↔ Function.Injective f

Full source

@[to_additive (attr := simp)]
lemma injective_codRestrict {S} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S)
    (h : ∀ x, f x ∈ s) : Function.InjectiveFunction.Injective (f.codRestrict s h) ↔ Function.Injective f :=
  ⟨fun H _ _ hxy ↦ H <| Subtype.eq hxy, fun H _ _ hxy ↦ H (congr_arg Subtype.val hxy)⟩

Injectivity of Codomain-Restricted Monoid Homomorphism

Informal description

Let $M$ and $N$ be monoids, $S$ a submonoid of $N$, and $f \colon M \to N$ a monoid homomorphism such that $f(x) \in S$ for all $x \in M$. Then the restricted homomorphism $f \colon M \to S$ is injective if and only if $f$ is injective.

MonoidHom.mrangeRestrict definition

{N} [MulOneClass N] (f : M →* N) : M →* (mrange f)

Full source

/-- Restriction of a monoid hom to its range interpreted as a submonoid. -/
@[to_additive "Restriction of an `AddMonoid` hom to its range interpreted as a submonoid."]
def mrangeRestrict {N} [MulOneClass N] (f : M →* N) : M →* (mrange f) :=
  (f.codRestrict (mrange f)) fun x => ⟨x, rfl⟩

Range restriction of a monoid homomorphism

Informal description

Given a monoid homomorphism $ f \colon M \to N $, the function `MonoidHom.mrangeRestrict` restricts $ f $ to its range, yielding a monoid homomorphism $ M \to \text{mrange } f $, where $\text{mrange } f$ is the submonoid of $ N $ consisting of all elements in the image of $ f $.

MonoidHom.coe_mrangeRestrict theorem

{N} [MulOneClass N] (f : M →* N) (x : M) : (f.mrangeRestrict x : N) = f x

Full source

@[to_additive (attr := simp)]
theorem coe_mrangeRestrict {N} [MulOneClass N] (f : M →* N) (x : M) :
    (f.mrangeRestrict x : N) = f x :=
  rfl

Range-Restricted Homomorphism Preserves Images

Informal description

For any monoid homomorphism $f \colon M \to N$ and any element $x \in M$, the image of $x$ under the range-restricted homomorphism $f \colon M \to \text{mrange } f$ (when viewed as an element of $N$) equals $f(x)$.

MonoidHom.mrangeRestrict_surjective theorem

(f : M →* N) : Function.Surjective f.mrangeRestrict

Full source

@[to_additive]
theorem mrangeRestrict_surjective (f : M →* N) : Function.Surjective f.mrangeRestrict :=
  fun ⟨_, ⟨x, rfl⟩⟩ => ⟨x, rfl⟩

Surjectivity of Range-Restricted Monoid Homomorphism

Informal description

For any monoid homomorphism $f \colon M \to N$, the restricted homomorphism $f_{\text{range}} \colon M \to \text{mrange}(f)$ is surjective, where $\text{mrange}(f)$ denotes the range of $f$ as a submonoid of $N$.

MonoidHom.mker definition

(f : F) : Submonoid M

Full source

/-- The multiplicative kernel of a monoid hom is the submonoid of elements `x : G` such
that `f x = 1` -/
@[to_additive
      "The additive kernel of an `AddMonoid` hom is the `AddSubmonoid` of
      elements such that `f x = 0`"]
def mker (f : F) : Submonoid M :=
  (⊥ : Submonoid N).comap f

Kernel of a monoid homomorphism

Informal description

The kernel of a monoid homomorphism $ f : M \to N $ is the submonoid of $ M $ consisting of all elements $ x \in M $ such that $ f(x) = 1 $, where $ 1 $ is the identity element of $ N $.

MonoidHom.mem_mker theorem

{f : F} {x : M} : x ∈ mker f ↔ f x = 1

Full source

@[to_additive (attr := simp)]
theorem mem_mker {f : F} {x : M} : x ∈ mker fx ∈ mker f ↔ f x = 1 :=
  Iff.rfl

Characterization of Kernel Membership for Monoid Homomorphisms

Informal description

For a monoid homomorphism $f \colon M \to N$ and an element $x \in M$, $x$ belongs to the kernel of $f$ if and only if $f(x) = 1$, where $1$ is the identity element of $N$.

MonoidHom.coe_mker theorem

(f : F) : (mker f : Set M) = (f : M → N) ⁻¹' { 1 }

Full source

@[to_additive]
theorem coe_mker (f : F) : (mker f : Set M) = (f : M → N) ⁻¹' {1} :=
  rfl

Kernel of a Monoid Homomorphism as Preimage of Identity

Informal description

For a monoid homomorphism $f \colon M \to N$, the underlying set of the kernel $\ker f$ is equal to the preimage of the singleton set $\{1\}$ under $f$, i.e., \[ (\ker f : \text{Set } M) = f^{-1}(\{1\}). \]

MonoidHom.decidableMemMker instance

[DecidableEq N] (f : F) : DecidablePred (· ∈ mker f)

Full source

@[to_additive]
instance decidableMemMker [DecidableEq N] (f : F) : DecidablePred (· ∈ mker f) := fun x =>
  decidable_of_iff (f x = 1) mem_mker

Decidability of Kernel Membership for Monoid Homomorphisms

Informal description

For any monoid homomorphism $f \colon M \to N$ where $N$ has decidable equality, the predicate $x \in \ker f$ is decidable for any $x \in M$.

MonoidHom.comap_mker theorem

(g : N →* P) (f : M →* N) : (mker g).comap f = mker (comp g f)

Full source

@[to_additive]
theorem comap_mker (g : N →* P) (f : M →* N) : (mker g).comap f = mker (comp g f) :=
  rfl

Preimage of Kernel under Composition of Monoid Homomorphisms

Informal description

For any monoid homomorphisms $g \colon N \to P$ and $f \colon M \to N$, the preimage of the kernel of $g$ under $f$ is equal to the kernel of the composition $g \circ f$. In other words, $(g \circ f)^{-1}(1) = f^{-1}(g^{-1}(1))$.

MonoidHom.comap_bot' theorem

(f : F) : (⊥ : Submonoid N).comap f = mker f

Full source

@[to_additive (attr := simp)]
theorem comap_bot' (f : F) : (⊥ : Submonoid N).comap f = mker f :=
  rfl

Preimage of Trivial Submonoid Equals Kernel of Monoid Homomorphism

Informal description

For any monoid homomorphism $f \colon M \to N$, the preimage of the trivial submonoid $\{1_N\}$ under $f$ is equal to the kernel of $f$, i.e., $f^{-1}(\{1_N\}) = \ker f$.

MonoidHom.restrict_mker theorem

(f : M →* N) : mker (f.restrict S) = (MonoidHom.mker f).comap S.subtype

Full source

@[to_additive (attr := simp)]
theorem restrict_mker (f : M →* N) : mker (f.restrict S) = (MonoidHom.mker f).comap S.subtype :=
  rfl

Kernel of Restricted Homomorphism Equals Preimage of Kernel

Informal description

Let $f \colon M \to N$ be a monoid homomorphism and let $S$ be a submonoid of $M$. The kernel of the restriction of $f$ to $S$ is equal to the preimage of the kernel of $f$ under the inclusion map $S \hookrightarrow M$. In symbols: \[ \ker(f|_S) = \ker f \cap S \] where $f|_S$ denotes the restriction of $f$ to $S$.

MonoidHom.mrangeRestrict_mker theorem

(f : M →* N) : mker (mrangeRestrict f) = mker f

Full source

@[to_additive]
theorem mrangeRestrict_mker (f : M →* N) : mker (mrangeRestrict f) = mker f := by
  ext x
  change (⟨f x, _⟩ : mrange f) = ⟨1, _⟩ ↔ f x = 1
  simp

Kernel Equality for Range-Restricted Monoid Homomorphism

Informal description

For any monoid homomorphism $f \colon M \to N$, the kernel of the range-restricted homomorphism $f|_{\text{mrange } f} \colon M \to \text{mrange } f$ is equal to the kernel of $f$. In other words, $\ker(f|_{\text{range } f}) = \ker f$.

MonoidHom.mker_one theorem

: mker (1 : M →* N) = ⊤

Full source

@[to_additive (attr := simp)]
theorem mker_one : mker (1 : M →* N) = ⊤ := by
  ext
  simp [mem_mker]

Kernel of Constant Monoid Homomorphism is Entire Domain

Informal description

The kernel of the constant monoid homomorphism $1 \colon M \to N$ (which sends every element to the identity element of $N$) is the entire monoid $M$, i.e., $\ker(1) = M$.

MonoidHom.prod_map_comap_prod' theorem

 {M' : Type*} {N' : Type*} [MulOneClass M'] [MulOneClass N'] (f : M →* N) (g : M' →* N') (S : Submonoid N)
  (S' : Submonoid N') : (S.prod S').comap (prodMap f g) = (S.comap f).prod (S'.comap g)

Full source

@[to_additive prod_map_comap_prod']
theorem prod_map_comap_prod' {M' : Type*} {N' : Type*} [MulOneClass M'] [MulOneClass N']
    (f : M →* N) (g : M' →* N') (S : Submonoid N) (S' : Submonoid N') :
    (S.prod S').comap (prodMap f g) = (S.comap f).prod (S'.comap g) :=
  SetLike.coe_injective <| Set.preimage_prod_map_prod f g _ _

Preimage of Product Submonoid under Product Homomorphism

Informal description

Let $M, M', N, N'$ be monoids, and let $f \colon M \to N$ and $g \colon M' \to N'$ be monoid homomorphisms. For any submonoids $S \subseteq N$ and $S' \subseteq N'$, the preimage of the product submonoid $S \times S'$ under the product homomorphism $f \times g \colon M \times M' \to N \times N'$ is equal to the product of the preimages of $S$ under $f$ and $S'$ under $g$. That is, $$(S \times S').\text{comap}(f \times g) = S.\text{comap}(f) \times S'.\text{comap}(g).$$

MonoidHom.mker_prod_map theorem

 {M' : Type*} {N' : Type*} [MulOneClass M'] [MulOneClass N'] (f : M →* N) (g : M' →* N') :
  mker (prodMap f g) = (mker f).prod (mker g)

Full source

@[to_additive mker_prod_map]
theorem mker_prod_map {M' : Type*} {N' : Type*} [MulOneClass M'] [MulOneClass N'] (f : M →* N)
    (g : M' →* N') : mker (prodMap f g) = (mker f).prod (mker g) := by
  rw [← comap_bot', ← comap_bot', ← comap_bot', ← prod_map_comap_prod', bot_prod_bot]

Kernel of Product Homomorphism Equals Product of Kernels

Informal description

Let $M, M', N, N'$ be monoids, and let $f \colon M \to N$ and $g \colon M' \to N'$ be monoid homomorphisms. The kernel of the product homomorphism $f \times g \colon M \times M' \to N \times N'$ is equal to the product of the kernels of $f$ and $g$, i.e., $$\ker(f \times g) = \ker f \times \ker g.$$

MonoidHom.mker_inl theorem

: mker (inl M N) = ⊥

Full source

@[to_additive (attr := simp)]
theorem mker_inl : mker (inl M N) = ⊥ := by
  ext x
  simp [mem_mker]

Kernel of Left Inclusion Homomorphism is Trivial

Informal description

The kernel of the left inclusion monoid homomorphism $\text{inl} \colon M \to M \times N$ is the trivial submonoid $\bot$ of $M$.

MonoidHom.mker_inr theorem

: mker (inr M N) = ⊥

Full source

@[to_additive (attr := simp)]
theorem mker_inr : mker (inr M N) = ⊥ := by
  ext x
  simp [mem_mker]

Kernel of Right Inclusion Homomorphism is Trivial

Informal description

The kernel of the inclusion homomorphism $\text{inr} \colon N \to M \times N$ is the trivial submonoid $\{1\}$ of $N$.

MonoidHom.mker_fst theorem

: mker (fst M N) = .prod ⊥ ⊤

Full source

@[to_additive (attr := simp)]
lemma mker_fst : mker (fst M N) = .prod ⊥ ⊤ := SetLike.ext fun _ => (iff_of_eq (and_true _)).symm

Kernel of First Projection Homomorphism is Trivial Cross Full Submonoid

Informal description

The kernel of the first projection monoid homomorphism $\mathrm{fst} \colon M \times N \to M$ is equal to the product submonoid $\{1\} \times N$, where $\{1\}$ is the trivial submonoid of $M$ and $N$ is considered as a submonoid of itself.

MonoidHom.mker_snd theorem

: mker (snd M N) = .prod ⊤ ⊥

Full source

@[to_additive (attr := simp)]
lemma mker_snd : mker (snd M N) = .prod ⊤ ⊥ := SetLike.ext fun _ => (iff_of_eq (true_and _)).symm

Kernel of Second Projection Homomorphism is Product with Trivial Submonoid

Informal description

The kernel of the second projection monoid homomorphism $\mathrm{snd} \colon M \times N \to N$ is equal to the product submonoid $M \times \{1\}$, where $1$ is the identity element of $N$.

MonoidHom.submonoidComap definition

(f : M →* N) (N' : Submonoid N) : N'.comap f →* N'

Full source

/-- The `MonoidHom` from the preimage of a submonoid to itself. -/
@[to_additive (attr := simps)
      "the `AddMonoidHom` from the preimage of an additive submonoid to itself."]
def submonoidComap (f : M →* N) (N' : Submonoid N) :
    N'.comap f →* N' where
  toFun x := ⟨f x, x.2⟩
  map_one' := Subtype.eq f.map_one
  map_mul' x y := Subtype.eq (f.map_mul x y)

Restriction of a monoid homomorphism to the preimage of a submonoid

Informal description

Given a monoid homomorphism $ f \colon M \to N $ and a submonoid $ N' $ of $ N $, the function `MonoidHom.submonoidComap` constructs a monoid homomorphism from the preimage submonoid $ f^{-1}(N') $ to $ N' $. Specifically, it maps an element $ x $ of $ f^{-1}(N') $ to $ f(x) $ in $ N' $, preserving the monoid structure (identity and multiplication).

MonoidHom.submonoidComap_surjective_of_surjective theorem

(f : M →* N) (N' : Submonoid N) (hf : Surjective f) : Surjective (f.submonoidComap N')

Full source

@[to_additive]
lemma submonoidComap_surjective_of_surjective (f : M →* N) (N' : Submonoid N) (hf : Surjective f) :
    Surjective (f.submonoidComap N') := fun y ↦ by
  obtain ⟨x, hx⟩ := hf y
  use ⟨x, mem_comap.mpr (hx ▸ y.2)⟩
  apply Subtype.val_injective
  simp [hx]

Surjectivity of Restricted Homomorphism from Preimage Submonoid

Informal description

Let $f \colon M \to N$ be a surjective monoid homomorphism and let $N'$ be a submonoid of $N$. Then the restricted homomorphism $f|_{f^{-1}(N')} \colon f^{-1}(N') \to N'$ is also surjective.

MonoidHom.submonoidMap definition

(f : M →* N) (M' : Submonoid M) : M' →* M'.map f

Full source

/-- The `MonoidHom` from a submonoid to its image.
See `MulEquiv.SubmonoidMap` for a variant for `MulEquiv`s. -/
@[to_additive (attr := simps)
      "the `AddMonoidHom` from an additive submonoid to its image. See
      `AddEquiv.AddSubmonoidMap` for a variant for `AddEquiv`s."]
def submonoidMap (f : M →* N) (M' : Submonoid M) : M' →* M'.map f where
  toFun x := ⟨f x, ⟨x, x.2, rfl⟩⟩
  map_one' := Subtype.eq <| f.map_one
  map_mul' x y := Subtype.eq <| f.map_mul x y

Image of a submonoid under a monoid homomorphism

Informal description

Given a monoid homomorphism $ f \colon M \to N $ and a submonoid $ M' $ of $ M $, the function `MonoidHom.submonoidMap` maps $ M' $ to its image under $ f $, which is a submonoid of $ N $. Specifically, it sends each element $ x \in M' $ to $ f(x) $, ensuring that the image is a submonoid by preserving the identity and multiplication.

MonoidHom.submonoidMap_surjective theorem

(f : M →* N) (M' : Submonoid M) : Function.Surjective (f.submonoidMap M')

Full source

@[to_additive]
theorem submonoidMap_surjective (f : M →* N) (M' : Submonoid M) :
    Function.Surjective (f.submonoidMap M') := by
  rintro ⟨_, x, hx, rfl⟩
  exact ⟨⟨x, hx⟩, rfl⟩

Surjectivity of the Submonoid Map Induced by a Monoid Homomorphism

Informal description

For any monoid homomorphism $f \colon M \to N$ and any submonoid $M'$ of $M$, the induced homomorphism $f.submonoidMap M' \colon M' \to M'.map f$ is surjective. That is, for every element $y$ in the image submonoid $M'.map f$, there exists an element $x \in M'$ such that $f(x) = y$.

Submonoid.mrange_inl theorem

: mrange (inl M N) = prod ⊤ ⊥

Full source

@[to_additive]
theorem mrange_inl : mrange (inl M N) = prod ⊤ ⊥ := by simpa only [mrange_eq_map] using map_inl ⊤

Range of Left Inclusion Homomorphism Equals Product with Trivial Submonoid

Informal description

The range of the left inclusion monoid homomorphism $\mathrm{inl} \colon M \to M \times N$ is equal to the product submonoid $M \times \{1\}$, where $1$ is the identity element of $N$.

Submonoid.mrange_inr theorem

: mrange (inr M N) = prod ⊥ ⊤

Full source

@[to_additive]
theorem mrange_inr : mrange (inr M N) = prod ⊥ ⊤ := by simpa only [mrange_eq_map] using map_inr ⊤

Range of Right Inclusion Homomorphism Equals Product with Trivial Submonoid

Informal description

For monoids $M$ and $N$, the range of the right inclusion homomorphism $\text{inr} \colon N \to M \times N$ (which maps $y \in N$ to $(1, y)$ where $1$ is the identity of $M$) is equal to the product submonoid $\{1\} \times N$ in $M \times N$.

Submonoid.mrange_inl' theorem

: mrange (inl M N) = comap (snd M N) ⊥

Full source

@[to_additive]
theorem mrange_inl' : mrange (inl M N) = comap (snd M N) ⊥ :=
  mrange_inl.trans (top_prod _)

Range of Left Inclusion Homomorphism as Preimage under Second Projection

Informal description

For monoids $M$ and $N$, the range of the left inclusion homomorphism $\mathrm{inl} \colon M \to M \times N$ (which maps $x \in M$ to $(x,1)$ where $1$ is the identity of $N$) is equal to the preimage of the trivial submonoid $\{1\}$ under the second projection homomorphism $\mathrm{snd} \colon M \times N \to N$.

Submonoid.mrange_inr' theorem

: mrange (inr M N) = comap (fst M N) ⊥

Full source

@[to_additive]
theorem mrange_inr' : mrange (inr M N) = comap (fst M N) ⊥ :=
  mrange_inr.trans (prod_top _)

Range of Right Inclusion Equals Preimage of Trivial Submonoid under First Projection

Informal description

For monoids $M$ and $N$, the range of the right inclusion homomorphism $\mathrm{inr} \colon N \to M \times N$ (which maps $y \in N$ to $(1, y)$ where $1$ is the identity of $M$) is equal to the preimage of the trivial submonoid $\{1\}$ under the first projection homomorphism $\mathrm{fst} \colon M \times N \to M$.

Submonoid.mrange_fst theorem

: mrange (fst M N) = ⊤

Full source

@[to_additive (attr := simp)]
theorem mrange_fst : mrange (fst M N) = ⊤ :=
  mrange_eq_top_of_surjective (fst M N) <| @Prod.fst_surjective _ _ ⟨1⟩

First Projection Homomorphism has Full Range

Informal description

For any monoids $M$ and $N$, the range of the first projection homomorphism $\mathrm{fst} \colon M \times N \to M$ is equal to the entire monoid $M$.

Submonoid.mrange_snd theorem

: mrange (snd M N) = ⊤

Full source

@[to_additive (attr := simp)]
theorem mrange_snd : mrange (snd M N) = ⊤ :=
  mrange_eq_top_of_surjective (snd M N) <| @Prod.snd_surjective _ _ ⟨1⟩

Surjectivity of the Second Projection Monoid Homomorphism

Informal description

The range of the second projection monoid homomorphism $\operatorname{snd} \colon M \times N \to N$ is equal to the entire monoid $N$ (as a submonoid). In other words, the projection onto the second component is surjective.

Submonoid.prod_eq_bot_iff theorem

{s : Submonoid M} {t : Submonoid N} : s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥

Full source

@[to_additive prod_eq_bot_iff]
theorem prod_eq_bot_iff {s : Submonoid M} {t : Submonoid N} : s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥ := by
  simp only [eq_bot_iff, prod_le_iff, (gc_map_comap _).le_iff_le, comap_bot', mker_inl, mker_inr]

Product Submonoid is Trivial if and only if Both Factors are Trivial

Informal description

For submonoids $s$ of a monoid $M$ and $t$ of a monoid $N$, the product submonoid $s \times t$ is the trivial submonoid $\{1\}$ if and only if both $s$ and $t$ are trivial submonoids of their respective monoids.

Submonoid.prod_eq_top_iff theorem

{s : Submonoid M} {t : Submonoid N} : s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

Full source

@[to_additive prod_eq_top_iff]
theorem prod_eq_top_iff {s : Submonoid M} {t : Submonoid N} : s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤ := by
  simp only [eq_top_iff, le_prod_iff, ← (gc_map_comap _).le_iff_le, ← mrange_eq_map, mrange_fst,
    mrange_snd]

Product Submonoid is Entire if and only if Both Factors are Entire

Informal description

For submonoids $s$ of a monoid $M$ and $t$ of a monoid $N$, the product submonoid $s \times t$ is equal to the entire product monoid $M \times N$ if and only if $s$ is equal to $M$ and $t$ is equal to $N$.

Submonoid.mrange_inl_sup_mrange_inr theorem

: mrange (inl M N) ⊔ mrange (inr M N) = ⊤

Full source

@[to_additive (attr := simp)]
theorem mrange_inl_sup_mrange_inr : mrangemrange (inl M N) ⊔ mrange (inr M N) = ⊤ := by
  simp only [mrange_inl, mrange_inr, prod_bot_sup_bot_prod, top_prod_top]

Join of Inclusion Ranges Equals Full Product Monoid

Informal description

For monoids $M$ and $N$, the supremum of the ranges of the left and right inclusion homomorphisms $\mathrm{inl} \colon M \to M \times N$ and $\mathrm{inr} \colon N \to M \times N$ equals the top submonoid of $M \times N$. In other words, the join of the submonoids $\{(x,1) \mid x \in M\}$ and $\{(1,y) \mid y \in N\}$ is the entire product monoid $M \times N$.

Submonoid.inclusion definition

{S T : Submonoid M} (h : S ≤ T) : S →* T

Full source

/-- The monoid hom associated to an inclusion of submonoids. -/
@[to_additive
      "The `AddMonoid` hom associated to an inclusion of submonoids."]
def inclusion {S T : Submonoid M} (h : S ≤ T) : S →* T :=
  S.subtype.codRestrict _ fun x => h x.2

Inclusion homomorphism of submonoids

Informal description

Given two submonoids $ S $ and $ T $ of a monoid $ M $ such that $ S $ is contained in $ T $, the function `Submonoid.inclusion h` is the inclusion map from $ S $ to $ T $ as a monoid homomorphism. This is constructed by restricting the codomain of the canonical embedding $ S \hookrightarrow M $ to $ T $, ensuring that the inclusion preserves the monoid structure (identity and multiplication).

Submonoid.mrange_subtype theorem

(s : Submonoid M) : mrange s.subtype = s

Full source

@[to_additive (attr := simp)]
theorem mrange_subtype (s : Submonoid M) : mrange s.subtype = s :=
  SetLike.coe_injective <| (coe_mrange _).trans <| Subtype.range_coe

Range of Submonoid Inclusion Equals Submonoid

Informal description

For any submonoid $s$ of a monoid $M$, the range of the inclusion homomorphism $s \hookrightarrow M$ is equal to $s$ itself.

Submonoid.nontrivial_iff_exists_ne_one theorem

(S : Submonoid M) : Nontrivial S ↔ ∃ x ∈ S, x ≠ (1 : M)

Full source

@[to_additive]
theorem nontrivial_iff_exists_ne_one (S : Submonoid M) : NontrivialNontrivial S ↔ ∃ x ∈ S, x ≠ (1 : M) :=
  calc
    Nontrivial S ↔ ∃ x : S, x ≠ 1 := nontrivial_iff_exists_ne 1
    _ ↔ ∃ (x : _) (hx : x ∈ S), (⟨x, hx⟩ : S) ≠ ⟨1, S.one_mem⟩calc
    Nontrivial S ↔ ∃ x : S, x ≠ 1 := nontrivial_iff_exists_ne 1
    _ ↔ ∃ (x : _) (hx : x ∈ S), (⟨x, hx⟩ : S) ≠ ⟨1, S.one_mem⟩ := Subtype.exists
    _ ↔ ∃ x ∈ S, x ≠ (1 : M) := by simp [Ne]

Nontriviality Criterion for Submonoids: $\text{Nontrivial }S \leftrightarrow \exists x \in S, x \neq 1$

Informal description

A submonoid $S$ of a monoid $M$ is nontrivial if and only if there exists an element $x \in S$ such that $x \neq 1_M$.

Submonoid.bot_or_nontrivial theorem

(S : Submonoid M) : S = ⊥ ∨ Nontrivial S

Full source

/-- A submonoid is either the trivial submonoid or nontrivial. -/
@[to_additive "An additive submonoid is either the trivial additive submonoid or nontrivial."]
theorem bot_or_nontrivial (S : Submonoid M) : S = ⊥ ∨ Nontrivial S := by
  simp only [eq_bot_iff_forall, nontrivial_iff_exists_ne_one, ← not_forall, ← Classical.not_imp,
    Classical.em]

Submonoid is Trivial or Nontrivial

Informal description

For any submonoid $S$ of a monoid $M$, either $S$ is the trivial submonoid (i.e., $S = \{\1\}$) or $S$ is nontrivial (i.e., contains at least two distinct elements).

Submonoid.bot_or_exists_ne_one theorem

(S : Submonoid M) : S = ⊥ ∨ ∃ x ∈ S, x ≠ (1 : M)

Full source

/-- A submonoid is either the trivial submonoid or contains a nonzero element. -/
@[to_additive
      "An additive submonoid is either the trivial additive submonoid or contains a nonzero
      element."]
theorem bot_or_exists_ne_one (S : Submonoid M) : S = ⊥ ∨ ∃ x ∈ S, x ≠ (1 : M) :=
  S.bot_or_nontrivial.imp_right S.nontrivial_iff_exists_ne_one.mp

Submonoid is Trivial or Contains Non-Identity Element

Informal description

For any submonoid $S$ of a monoid $M$, either $S$ is the trivial submonoid (i.e., $S = \{\1\}$) or there exists an element $x \in S$ such that $x \neq 1_M$.

MulEquiv.submonoidCongr definition

(h : S = T) : S ≃* T

Full source

/-- Makes the identity isomorphism from a proof that two submonoids of a multiplicative
    monoid are equal. -/
@[to_additive
      "Makes the identity additive isomorphism from a proof two
      submonoids of an additive monoid are equal."]
def submonoidCongr (h : S = T) : S ≃* T :=
  { Equiv.setCongr <| congr_arg _ h with map_mul' := fun _ _ => rfl }

Multiplicative equivalence of equal submonoids

Informal description

Given two submonoids $ S $ and $ T $ of a multiplicative monoid $ M $ that are equal ($ S = T $), the function constructs a multiplicative equivalence (i.e., a monoid isomorphism) between $ S $ and $ T $. The equivalence preserves the multiplicative structure, meaning that for any $ x, y \in S $, the image of the product $ x \cdot y $ under the equivalence is equal to the product of the images of $ x $ and $ y $.

MulEquiv.ofLeftInverse' definition

(f : M →* N) {g : N → M} (h : Function.LeftInverse g f) : M ≃* MonoidHom.mrange f

Full source

/-- A monoid homomorphism `f : M →* N` with a left-inverse `g : N → M` defines a multiplicative
equivalence between `M` and `f.mrange`.
This is a bidirectional version of `MonoidHom.mrange_restrict`. -/
@[to_additive (attr := simps +simpRhs)
      "An additive monoid homomorphism `f : M →+ N` with a left-inverse `g : N → M`
      defines an additive equivalence between `M` and `f.mrange`.
      This is a bidirectional version of `AddMonoidHom.mrange_restrict`. "]
def ofLeftInverse' (f : M →* N) {g : N → M} (h : Function.LeftInverse g f) :
    M ≃* MonoidHom.mrange f :=
  { f.mrangeRestrict with
    toFun := f.mrangeRestrict
    invFun := g ∘ (MonoidHom.mrange f).subtype
    left_inv := h
    right_inv := fun x =>
      Subtype.ext <|
        let ⟨x', hx'⟩ := MonoidHom.mem_mrange.mp x.2
        show f (g x) = x by rw [← hx', h x'] }

Monoid isomorphism induced by a left-invertible homomorphism

Informal description

Given a monoid homomorphism $ f \colon M \to N $ with a left inverse $ g \colon N \to M $ (i.e., $ g \circ f = \text{id}_M $), there exists a multiplicative equivalence (monoid isomorphism) between $ M $ and the range of $ f $, denoted $ \text{mrange}\, f $. This equivalence is constructed by restricting $ f $ to its range and using $ g $ to define the inverse map.

MulEquiv.submonoidMap definition

(e : M ≃* N) (S : Submonoid M) : S ≃* S.map e

Full source

/-- A `MulEquiv` `φ` between two monoids `M` and `N` induces a `MulEquiv` between
a submonoid `S ≤ M` and the submonoid `φ(S) ≤ N`.
See `MonoidHom.submonoidMap` for a variant for `MonoidHom`s. -/
@[to_additive
      "An `AddEquiv` `φ` between two additive monoids `M` and `N` induces an `AddEquiv`
      between a submonoid `S ≤ M` and the submonoid `φ(S) ≤ N`. See
      `AddMonoidHom.addSubmonoidMap` for a variant for `AddMonoidHom`s."]
def submonoidMap (e : M ≃* N) (S : Submonoid M) : S ≃* S.map e :=
  { (e : M ≃ N).image S with map_mul' := fun _ _ => Subtype.ext (map_mul e _ _) }

Submonoid equivalence induced by a monoid isomorphism

Informal description

Given a multiplicative equivalence (monoid isomorphism) $e \colon M \simeq^* N$ between monoids $M$ and $N$, and a submonoid $S$ of $M$, there is an induced multiplicative equivalence between $S$ and the image submonoid $e(S) \subseteq N$. This equivalence maps each element $x \in S$ to $e(x) \in e(S)$, preserving the multiplicative structure.

MulEquiv.coe_submonoidMap_apply theorem

(e : M ≃* N) (S : Submonoid M) (g : S) : ((submonoidMap e S g : S.map (e : M →* N)) : N) = e g

Full source

@[to_additive (attr := simp)]
theorem coe_submonoidMap_apply (e : M ≃* N) (S : Submonoid M) (g : S) :
    ((submonoidMap e S g : S.map (e : M →* N)) : N) = e g :=
  rfl

Image of Submonoid Element under Induced Isomorphism Equals Original Image

Informal description

Let $e \colon M \simeq^* N$ be a monoid isomorphism, $S$ be a submonoid of $M$, and $g \in S$. Then the image of $g$ under the induced isomorphism $\text{submonoidMap}\, e\, S$ (when viewed as an element of $N$) equals $e(g)$.

MulEquiv.submonoidMap_symm_apply theorem

 (e : M ≃* N) (S : Submonoid M) (g : S.map (e : M →* N)) :
  (e.submonoidMap S).symm g = ⟨e.symm g, SetLike.mem_coe.1 <| Set.mem_image_equiv.1 g.2⟩

Full source

@[to_additive (attr := simp) AddEquiv.add_submonoid_map_symm_apply]
theorem submonoidMap_symm_apply (e : M ≃* N) (S : Submonoid M) (g : S.map (e : M →* N)) :
    (e.submonoidMap S).symm g = ⟨e.symm g, SetLike.mem_coe.1 <| Set.mem_image_equiv.1 g.2⟩ :=
  rfl

Inverse of Submonoid Map Induced by Monoid Isomorphism

Informal description

Let $e \colon M \simeq^* N$ be a monoid isomorphism between monoids $M$ and $N$, and let $S$ be a submonoid of $M$. For any element $g$ in the image submonoid $e(S) \subseteq N$, the inverse of the induced equivalence $e.submonoidMap S$ applied to $g$ is given by $\langle e^{-1}(g), h \rangle$, where $h$ is a proof that $e^{-1}(g)$ belongs to $S$, obtained via the characterization of image membership under the equivalence $e$. In other words, the inverse map $(e.submonoidMap S)^{-1}$ sends an element $g \in e(S)$ to the pair consisting of its preimage $e^{-1}(g) \in S$ and a proof that this preimage is indeed in $S$.

Submonoid.equivMapOfInjective_coe_mulEquiv theorem

(e : M ≃* N) : S.equivMapOfInjective (e : M →* N) (EquivLike.injective e) = e.submonoidMap S

Full source

@[to_additive (attr := simp)]
theorem Submonoid.equivMapOfInjective_coe_mulEquiv (e : M ≃* N) :
    S.equivMapOfInjective (e : M →* N) (EquivLike.injective e) = e.submonoidMap S := by
  ext
  rfl

Equivalence of Submonoid Mapping Constructions via Monoid Isomorphism

Informal description

Given a monoid isomorphism $e \colon M \simeq^* N$ and a submonoid $S$ of $M$, the isomorphism between $S$ and its image under $e$ (constructed via `equivMapOfInjective`) coincides with the isomorphism obtained by restricting $e$ to $S$ (via `submonoidMap`). In other words, the following diagram commutes: $$S \xrightarrow{\text{equivMapOfInjective } e} e(S) = S \xrightarrow{\text{submonoidMap } e} e(S)$$

Submonoid.faithfulSMul instance

{M' α : Type*} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} [FaithfulSMul M' α] : FaithfulSMul S α

Full source

@[to_additive]
instance Submonoid.faithfulSMul {M' α : Type*} [MulOneClass M'] [SMul M' α] {S : Submonoid M'}
    [FaithfulSMul M' α] : FaithfulSMul S α :=
  ⟨fun h => Subtype.ext <| eq_of_smul_eq_smul h⟩

Faithfulness of Scalar Multiplication Restricted to Submonoids

Informal description

For any submonoid $S$ of a monoid $M'$ with a scalar multiplication action on a type $\alpha$, if the action of $M'$ on $\alpha$ is faithful, then the restricted action of $S$ on $\alpha$ is also faithful.

Submonoid.unitsTypeEquivIsUnitSubmonoid definition

[Monoid M] : Mˣ ≃* IsUnit.submonoid M

Full source

/-- The multiplicative equivalence between the type of units of `M` and the submonoid of unit
elements of `M`. -/
@[to_additive (attr := simps!) " The additive equivalence between the type of additive units of `M`
  and the additive submonoid whose elements are the additive units of `M`. "]
noncomputable def unitsTypeEquivIsUnitSubmonoid [Monoid M] : MˣMˣ ≃* IsUnit.submonoid M where
  toFun x := ⟨x, Units.isUnit x⟩
  invFun x := x.prop.unit
  left_inv _ := IsUnit.unit_of_val_units _
  right_inv x := by simp_rw [IsUnit.unit_spec]
  map_mul' x y := by simp_rw [Units.val_mul]; rfl

Multiplicative equivalence between units and unit submonoid

Informal description

The multiplicative equivalence between the group of units $M^\times$ of a monoid $M$ and the submonoid of $M$ consisting of all unit elements (i.e., invertible elements) of $M$. The equivalence maps each unit $x \in M^\times$ to the submonoid element $\langle x, \text{isUnit } x \rangle$, and its inverse maps each submonoid element back to its corresponding unit in $M^\times$. The equivalence preserves the multiplicative structure.

Nat.addSubmonoid_closure_one theorem

: closure ({ 1 } : Set ℕ) = ⊤

Full source

@[simp] lemma addSubmonoid_closure_one : closure ({1} : Set ℕ) = ⊤ := by
  refine (eq_top_iff' _).2 <| Nat.rec (zero_mem _) ?_
  simp_rw [Nat.succ_eq_add_one]
  exact fun n hn ↦ AddSubmonoid.add_mem _ hn <| subset_closure <| Set.mem_singleton _

$\{1\}$ Generates the Additive Submonoid of Natural Numbers

Informal description

The additive submonoid of natural numbers generated by the singleton set $\{1\}$ is equal to the entire set of natural numbers, i.e., $\text{closure}(\{1\}) = \mathbb{N}$.

Submonoid.map_comap_eq theorem

(f : F) (S : Submonoid N) : (S.comap f).map f = S ⊓ MonoidHom.mrange f

Full source

@[to_additive]
theorem map_comap_eq (f : F) (S : Submonoid N) : (S.comap f).map f = S ⊓ MonoidHom.mrange f :=
  SetLike.coe_injective Set.image_preimage_eq_inter_range

Image-Preimage Equality for Submonoids: $f(f^{-1}(S)) = S \cap \operatorname{range}(f)$

Informal description

For a monoid homomorphism $f \colon M \to N$ and a submonoid $S$ of $N$, the image of the preimage of $S$ under $f$ equals the intersection of $S$ with the range of $f$, i.e., $$ f(f^{-1}(S)) = S \cap \operatorname{range}(f). $$

Submonoid.map_comap_eq_self theorem

{f : F} {S : Submonoid N} (h : S ≤ MonoidHom.mrange f) : (S.comap f).map f = S

Full source

@[to_additive]
theorem map_comap_eq_self {f : F} {S : Submonoid N} (h : S ≤ MonoidHom.mrange f) :
    (S.comap f).map f = S := by
  simpa only [inf_of_le_left h] using map_comap_eq f S

Image-Preimage Identity for Submonoids Contained in Range

Informal description

Let $f \colon M \to N$ be a monoid homomorphism and $S$ a submonoid of $N$ such that $S$ is contained in the range of $f$. Then the image of the preimage of $S$ under $f$ equals $S$ itself, i.e., $$ f(f^{-1}(S)) = S. $$

Submonoid.map_comap_eq_self_of_surjective theorem

{f : F} (h : Function.Surjective f) {S : Submonoid N} : map f (comap f S) = S

Full source

@[to_additive]
theorem map_comap_eq_self_of_surjective {f : F} (h : Function.Surjective f) {S : Submonoid N} :
    map f (comap f S) = S :=
  map_comap_eq_self (MonoidHom.mrange_eq_top_of_surjective _ h ▸ le_top)

Image-Preimage Identity for Submonoids under Surjective Homomorphism

Informal description

Let $f \colon M \to N$ be a surjective monoid homomorphism and $S$ a submonoid of $N$. Then the image of the preimage of $S$ under $f$ equals $S$ itself, i.e., $$ f(f^{-1}(S)) = S. $$

Mathlib.Algebra.Group.Submonoid.Operations

Main definitions

Conversion between multiplicative and additive definitions

(Commutative) monoid structure on a submonoid

Group actions by submonoids

Operations on submonoids

Monoid homomorphisms between submonoid

Operations on `MonoidHom`s

Tags

Main definitions

Conversion between multiplicative and additive definitions

(Commutative) monoid structure on a submonoid

Group actions by submonoids

Operations on submonoids

Monoid homomorphisms between submonoid

Operations on MonoidHoms

Tags

Operations on `MonoidHom`s