Mathlib.Algebra.Group.Subsemigroup.Operations

Subsemigroup.toAddSubsemigroup definition

: Subsemigroup M ≃o AddSubsemigroup (Additive M)

Full source

/-- Subsemigroups of semigroup `M` are isomorphic to additive subsemigroups of `Additive M`. -/
@[simps]
def Subsemigroup.toAddSubsemigroup : SubsemigroupSubsemigroup M ≃o AddSubsemigroup (Additive M) where
  toFun S :=
    { carrier := Additive.toMulAdditive.toMul ⁻¹' S
      add_mem' := S.mul_mem' }
  invFun S :=
    { carrier := Additive.ofMulAdditive.ofMul ⁻¹' S
      mul_mem' := S.add_mem' }
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' := Iff.rfl

Subsemigroup to AddSubsemigroup Order Isomorphism

Informal description

The order isomorphism between the lattice of subsemigroups of a multiplicative semigroup $M$ and the lattice of additive subsemigroups of the additive semigroup $\text{Additive } M$. Specifically: - The forward map takes a subsemigroup $S \subseteq M$ to the additive subsemigroup $\{x \in \text{Additive } M \mid \text{Additive.toMul}(x) \in S\}$. - The inverse map takes an additive subsemigroup $T \subseteq \text{Additive } M$ to the subsemigroup $\{x \in M \mid \text{Additive.ofMul}(x) \in T\}$. This isomorphism preserves the order structure (inclusion relations) between subsemigroups.

AddSubsemigroup.toSubsemigroup' abbrev

: AddSubsemigroup (Additive M) ≃o Subsemigroup M

Full source

/-- Additive subsemigroups of an additive semigroup `Additive M` are isomorphic to subsemigroups
of `M`. -/
abbrev AddSubsemigroup.toSubsemigroup' : AddSubsemigroupAddSubsemigroup (Additive M) ≃o Subsemigroup M :=
  Subsemigroup.toAddSubsemigroup.symm

Additive Subsemigroup to Subsemigroup Order Isomorphism ($\text{AddSubsemigroup}(\text{Additive } M) \simeq_o \text{Subsemigroup } M$)

Informal description

The order isomorphism between the lattice of additive subsemigroups of the additive semigroup $\text{Additive } M$ and the lattice of subsemigroups of the multiplicative semigroup $M$. Specifically: - The forward map takes an additive subsemigroup $T \subseteq \text{Additive } M$ to the subsemigroup $\{x \in M \mid \text{Additive.ofMul}(x) \in T\}$. - The inverse map takes a subsemigroup $S \subseteq M$ to the additive subsemigroup $\{x \in \text{Additive } M \mid \text{Additive.toMul}(x) \in S\}$. This isomorphism preserves the order structure (inclusion relations) between subsemigroups.

Subsemigroup.toAddSubsemigroup_closure theorem

 (S : Set M) : Subsemigroup.toAddSubsemigroup (Subsemigroup.closure S) = AddSubsemigroup.closure (Additive.toMul ⁻¹' S)

Full source

theorem Subsemigroup.toAddSubsemigroup_closure (S : Set M) :
    Subsemigroup.toAddSubsemigroup (Subsemigroup.closure S) =
    AddSubsemigroup.closure (Additive.toMulAdditive.toMul ⁻¹' S) :=
  le_antisymm
    (Subsemigroup.toAddSubsemigroup.le_symm_apply.1 <|
      Subsemigroup.closure_le.2 (AddSubsemigroup.subset_closure (M := Additive M)))
    (AddSubsemigroup.closure_le.2 (Subsemigroup.subset_closure (M := M)))

Closure Preservation under Subsemigroup to AddSubsemigroup Isomorphism: $\text{toAddSubsemigroup}(\text{closure}(S)) = \text{closure}(\text{toMul}^{-1}(S))$

Informal description

For any subset $S$ of a multiplicative semigroup $M$, the image of the subsemigroup generated by $S$ under the order isomorphism $\text{Subsemigroup.toAddSubsemigroup}$ is equal to the additive subsemigroup generated by the preimage of $S$ under the bijection $\text{Additive.toMul} : \text{Additive } M \to M$. In other words, \[ \text{Subsemigroup.toAddSubsemigroup}(\text{closure}(S)) = \text{AddSubsemigroup.closure}(\text{Additive.toMul}^{-1}(S)). \]

AddSubsemigroup.toSubsemigroup'_closure theorem

 (S : Set (Additive M)) :
  AddSubsemigroup.toSubsemigroup' (AddSubsemigroup.closure S) = Subsemigroup.closure (Additive.ofMul ⁻¹' S)

Full source

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

Closure Preservation under Additive to Multiplicative Subsemigroup Isomorphism

Informal description

For any subset $S$ of the additive semigroup $\text{Additive } M$, the image of the additive subsemigroup generated by $S$ under the order isomorphism $\text{AddSubsemigroup.toSubsemigroup'}$ is equal to the multiplicative subsemigroup generated by the preimage of $S$ under the bijection $\text{Additive.ofMul} : M \to \text{Additive } M$. In other words, \[ \text{AddSubsemigroup.toSubsemigroup'}(\text{closure}(S)) = \text{Subsemigroup.closure}(\text{Additive.ofMul}^{-1}(S)). \]

AddSubsemigroup.toSubsemigroup definition

: AddSubsemigroup A ≃o Subsemigroup (Multiplicative A)

Full source

/-- Additive subsemigroups of an additive semigroup `A` are isomorphic to
multiplicative subsemigroups of `Multiplicative A`. -/
@[simps]
def AddSubsemigroup.toSubsemigroup : AddSubsemigroupAddSubsemigroup A ≃o Subsemigroup (Multiplicative A) where
  toFun S :=
    { carrier := Multiplicative.toAddMultiplicative.toAdd ⁻¹' S
      mul_mem' := S.add_mem' }
  invFun S :=
    { carrier := Multiplicative.ofAddMultiplicative.ofAdd ⁻¹' S
      add_mem' := S.mul_mem' }
  left_inv _ := rfl
  right_inv _ := rfl
  map_rel_iff' := Iff.rfl

Isomorphism between additive subsemigroups and multiplicative subsemigroups via type tags

Informal description

The order isomorphism $\text{AddSubsemigroup}\,A \simeq_o \text{Subsemigroup}\,(\text{Multiplicative}\,A)$ converts between additive subsemigroups of an additive semigroup $A$ and multiplicative subsemigroups of the multiplicative type tag $\text{Multiplicative}\,A$. Specifically: - The forward map takes an additive subsemigroup $S \subseteq A$ and constructs the multiplicative subsemigroup consisting of all $x \in \text{Multiplicative}\,A$ whose underlying element in $A$ belongs to $S$. - The inverse map takes a multiplicative subsemigroup $T \subseteq \text{Multiplicative}\,A$ and constructs the additive subsemigroup consisting of all $x \in A$ whose tagged version in $\text{Multiplicative}\,A$ belongs to $T$. This isomorphism preserves the inclusion order in both directions.

Subsemigroup.toAddSubsemigroup' abbrev

: Subsemigroup (Multiplicative A) ≃o AddSubsemigroup A

Full source

/-- Subsemigroups of a semigroup `Multiplicative A` are isomorphic to additive subsemigroups
of `A`. -/
abbrev Subsemigroup.toAddSubsemigroup' : SubsemigroupSubsemigroup (Multiplicative A) ≃o AddSubsemigroup A :=
  AddSubsemigroup.toSubsemigroup.symm

Isomorphism between multiplicative subsemigroups and additive subsemigroups via type tags

Informal description

The order isomorphism $\text{Subsemigroup}\,(\text{Multiplicative}\,A) \simeq_o \text{AddSubsemigroup}\,A$ converts between multiplicative subsemigroups of the multiplicative type tag $\text{Multiplicative}\,A$ and additive subsemigroups of the additive semigroup $A$. Specifically: - The forward map takes a multiplicative subsemigroup $S \subseteq \text{Multiplicative}\,A$ and constructs the additive subsemigroup consisting of all $x \in A$ whose tagged version in $\text{Multiplicative}\,A$ belongs to $S$. - The inverse map takes an additive subsemigroup $T \subseteq A$ and constructs the multiplicative subsemigroup consisting of all $x \in \text{Multiplicative}\,A$ whose underlying element in $A$ belongs to $T$. This isomorphism preserves the inclusion order in both directions.

AddSubsemigroup.toSubsemigroup_closure theorem

 (S : Set A) :
  AddSubsemigroup.toSubsemigroup (AddSubsemigroup.closure S) = Subsemigroup.closure (Multiplicative.toAdd ⁻¹' S)

Full source

theorem AddSubsemigroup.toSubsemigroup_closure (S : Set A) :
    AddSubsemigroup.toSubsemigroup (AddSubsemigroup.closure S) =
      Subsemigroup.closure (Multiplicative.toAddMultiplicative.toAdd ⁻¹' S) :=
  le_antisymm
    (AddSubsemigroup.toSubsemigroup.to_galoisConnection.l_le <|
      AddSubsemigroup.closure_le.2 <| Subsemigroup.subset_closure (M := Multiplicative A))
    (Subsemigroup.closure_le.2 <| AddSubsemigroup.subset_closure (M := A))

Closure Preservation under Additive-Multiplicative Subsemigroup Isomorphism

Informal description

For any subset $S$ of an additive semigroup $A$, the image of the additive subsemigroup closure of $S$ under the isomorphism $\text{AddSubsemigroup}\,A \simeq_o \text{Subsemigroup}\,(\text{Multiplicative}\,A)$ is equal to the multiplicative subsemigroup closure of the preimage of $S$ under the projection $\text{Multiplicative.toAdd} : \text{Multiplicative}\,A \to A$. In other words, the following diagram commutes: $$\text{closure}_{\text{add}}(S) \xrightarrow{\text{toSubsemigroup}} \text{closure}_{\text{mul}}(\text{Multiplicative.toAdd}^{-1}(S))$$ where $\text{closure}_{\text{add}}$ and $\text{closure}_{\text{mul}}$ denote the additive and multiplicative subsemigroup closures respectively.

Subsemigroup.toAddSubsemigroup'_closure theorem

 (S : Set (Multiplicative A)) :
  Subsemigroup.toAddSubsemigroup' (Subsemigroup.closure S) = AddSubsemigroup.closure (Multiplicative.ofAdd ⁻¹' S)

Full source

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

Closure Preservation under Multiplicative-Additive Subsemigroup Isomorphism

Informal description

For any subset $S$ of the multiplicative type tag $\text{Multiplicative}\,A$, the image of the multiplicative subsemigroup closure of $S$ under the isomorphism $\text{Subsemigroup}\,(\text{Multiplicative}\,A) \simeq_o \text{AddSubsemigroup}\,A$ is equal to the additive subsemigroup closure of the preimage of $S$ under the embedding $\text{Multiplicative.ofAdd} : A \to \text{Multiplicative}\,A$. In other words, the following diagram commutes: $$\text{closure}_{\text{mul}}(S) \xrightarrow{\text{toAddSubsemigroup}'} \text{closure}_{\text{add}}(\text{Multiplicative.ofAdd}^{-1}(S))$$ where $\text{closure}_{\text{mul}}$ and $\text{closure}_{\text{add}}$ denote the multiplicative and additive subsemigroup closures respectively.

Subsemigroup.comap definition

(f : M →ₙ* N) (S : Subsemigroup N) : Subsemigroup M

Full source

/-- The preimage of a subsemigroup along a semigroup homomorphism is a subsemigroup. -/
@[to_additive
      "The preimage of an `AddSubsemigroup` along an `AddSemigroup` homomorphism is an
      `AddSubsemigroup`."]
def comap (f : M →ₙ* N) (S : Subsemigroup N) :
    Subsemigroup M where
  carrier := f ⁻¹' S
  mul_mem' ha hb := show f (_ * _) ∈ S by rw [map_mul]; exact mul_mem ha hb

Preimage of a subsemigroup under a semigroup homomorphism

Informal description

Given a semigroup homomorphism $ f : M \to N $ and a subsemigroup $ S $ of $ N $, the preimage $ f^{-1}(S) $ forms a subsemigroup of $ M $. Specifically, for any $ x, y \in M $, if $ f(x) \in S $ and $ f(y) \in S $, then $ f(x \cdot y) \in S $.

Subsemigroup.coe_comap theorem

(S : Subsemigroup N) (f : M →ₙ* N) : (S.comap f : Set M) = f ⁻¹' S

Full source

@[to_additive (attr := simp)]
theorem coe_comap (S : Subsemigroup N) (f : M →ₙ* N) : (S.comap f : Set M) = f ⁻¹' S :=
  rfl

Preimage of Subsemigroup Under Homomorphism Equals Set Preimage

Informal description

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

Subsemigroup.mem_comap theorem

{S : Subsemigroup N} {f : M →ₙ* N} {x : M} : x ∈ S.comap f ↔ f x ∈ S

Full source

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

Characterization of Elements in Preimage of Subsemigroup

Informal description

Let $M$ and $N$ be semigroups, $S$ a subsemigroup of $N$, and $f : M \to N$ a semigroup homomorphism. For any $x \in M$, we have $x \in f^{-1}(S)$ if and only if $f(x) \in S$.

Subsemigroup.comap_comap theorem

(S : Subsemigroup 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 : Subsemigroup P) (g : N →ₙ* P) (f : M →ₙ* N) :
    (S.comap g).comap f = S.comap (g.comp f) :=
  rfl

Compatibility of Subsemigroup Preimages with Homomorphism Composition

Informal description

Let $M$, $N$, and $P$ be semigroups, $S$ a subsemigroup of $P$, and $g : N \to P$ and $f : M \to N$ semigroup homomorphisms. Then the preimage of the preimage of $S$ under $g$ and $f$ is equal to the preimage of $S$ under the composition $g \circ f$, i.e., $(S.\text{comap}\,g).\text{comap}\,f = S.\text{comap}\,(g \circ f)$.

Subsemigroup.comap_id theorem

(S : Subsemigroup P) : S.comap (MulHom.id _) = S

Full source

@[to_additive (attr := simp)]
theorem comap_id (S : Subsemigroup P) : S.comap (MulHom.id _) = S :=
  ext (by simp)

Preimage of Subsemigroup under Identity Homomorphism is Itself

Informal description

For any subsemigroup $S$ of a semigroup $P$, the preimage of $S$ under the identity homomorphism $\text{id}_P \colon P \to P$ is equal to $S$ itself. In other words, $\text{id}_P^{-1}(S) = S$.

Subsemigroup.map definition

(f : M →ₙ* N) (S : Subsemigroup M) : Subsemigroup N

Full source

/-- The image of a subsemigroup along a semigroup homomorphism is a subsemigroup. -/
@[to_additive
      "The image of an `AddSubsemigroup` along an `AddSemigroup` homomorphism is
      an `AddSubsemigroup`."]
def map (f : M →ₙ* N) (S : Subsemigroup M) : Subsemigroup N where
  carrier := f '' S
  mul_mem' := by
    rintro _ _ ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
    exact ⟨x * y, @mul_mem (Subsemigroup M) M _ _ _ _ _ _ hx hy, by rw [map_mul]⟩

Image of a subsemigroup under a semigroup homomorphism

Informal description

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

Subsemigroup.coe_map theorem

(f : M →ₙ* N) (S : Subsemigroup M) : (S.map f : Set N) = f '' S

Full source

@[to_additive (attr := simp)]
theorem coe_map (f : M →ₙ* N) (S : Subsemigroup M) : (S.map f : Set N) = f '' S :=
  rfl

Image of Subsemigroup Under Homomorphism Equals Function Image

Informal description

For any semigroup homomorphism $f \colon M \to N$ and any subsemigroup $S$ of $M$, the underlying set of the image subsemigroup $S.map f$ is equal to the image of $S$ under $f$, i.e., $(S.map f : Set N) = f(S)$.

Subsemigroup.mem_map theorem

{f : M →ₙ* N} {S : Subsemigroup M} {y : N} : y ∈ S.map f ↔ ∃ x ∈ S, f x = y

Full source

@[to_additive (attr := simp)]
theorem mem_map {f : M →ₙ* N} {S : Subsemigroup M} {y : N} : y ∈ S.map fy ∈ S.map f ↔ ∃ x ∈ S, f x = y :=
  mem_image _ _ _

Characterization of Membership in the Image of a Subsemigroup

Informal description

For a semigroup homomorphism $f \colon M \to N$, a subsemigroup $S$ of $M$, and an element $y \in N$, we have $y \in f(S)$ if and only if there exists $x \in S$ such that $f(x) = y$.

Subsemigroup.mem_map_of_mem theorem

(f : M →ₙ* N) {S : Subsemigroup M} {x : M} (hx : x ∈ S) : f x ∈ S.map f

Full source

@[to_additive]
theorem mem_map_of_mem (f : M →ₙ* N) {S : Subsemigroup M} {x : M} (hx : x ∈ S) : f x ∈ S.map f :=
  mem_image_of_mem f hx

Image of subsemigroup element under homomorphism is in image subsemigroup

Informal description

Let $f \colon M \to N$ be a semigroup homomorphism, $S$ a subsemigroup of $M$, and $x \in M$ an element of $S$. Then the image $f(x)$ belongs to the image subsemigroup $f(S)$ of $N$.

Subsemigroup.apply_coe_mem_map theorem

(f : M →ₙ* N) (S : Subsemigroup M) (x : S) : f x ∈ S.map f

Full source

@[to_additive]
theorem apply_coe_mem_map (f : M →ₙ* N) (S : Subsemigroup M) (x : S) : f x ∈ S.map f :=
  mem_map_of_mem f x.prop

Image of Subsemigroup Element under Homomorphism is in Image Subsemigroup

Informal description

Let $f \colon M \to N$ be a semigroup homomorphism, $S$ a subsemigroup of $M$, and $x$ an element of $S$. Then the image $f(x)$ belongs to the image subsemigroup $f(S)$ of $N$.

Subsemigroup.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 Image Subsemigroup Equals Image under Composition

Informal description

Let $M$, $N$, and $P$ be semigroups, $S$ a subsemigroup of $M$, and $f \colon M \to N$ and $g \colon N \to P$ semigroup homomorphisms. Then the image of the image of $S$ under $f$ under $g$ is equal to the image of $S$ under the composition $g \circ f$. In symbols: $$g(f(S)) = (g \circ f)(S).$$

Subsemigroup.mem_map_iff_mem theorem

{f : M →ₙ* N} (hf : Function.Injective f) {S : Subsemigroup M} {x : M} : f x ∈ S.map f ↔ x ∈ S

Full source

@[to_additive (attr := simp, nolint simpNF)]
theorem mem_map_iff_mem {f : M →ₙ* N} (hf : Function.Injective f) {S : Subsemigroup M} {x : M} :
    f x ∈ S.map ff x ∈ S.map f ↔ x ∈ S :=
  hf.mem_set_image

Characterization of Membership in Image Subsemigroup via Injective Homomorphism

Informal description

Let $f \colon M \to N$ be an injective semigroup homomorphism between semigroups $M$ and $N$, and let $S$ be a subsemigroup of $M$. For any element $x \in M$, the image $f(x)$ belongs to the image subsemigroup $f(S)$ if and only if $x$ belongs to $S$. In symbols: \[ f(x) \in f(S) \leftrightarrow x \in S. \]

Subsemigroup.map_le_iff_le_comap theorem

{f : M →ₙ* N} {S : Subsemigroup M} {T : Subsemigroup N} : S.map f ≤ T ↔ S ≤ T.comap f

Full source

@[to_additive]
theorem map_le_iff_le_comap {f : M →ₙ* N} {S : Subsemigroup M} {T : Subsemigroup N} :
    S.map f ≤ T ↔ S ≤ T.comap f :=
  image_subset_iff

Image-Preimage Containment Equivalence for Subsemigroups

Informal description

Let $f \colon M \to N$ be a semigroup homomorphism, $S$ a subsemigroup of $M$, and $T$ a subsemigroup 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 symbols: \[ f(S) \subseteq T \leftrightarrow S \subseteq f^{-1}(T). \]

Subsemigroup.gc_map_comap theorem

(f : M →ₙ* N) : GaloisConnection (map f) (comap f)

Full source

@[to_additive]
theorem gc_map_comap (f : M →ₙ* N) : GaloisConnection (map f) (comap f) := fun _ _ =>
  map_le_iff_le_comap

Galois Connection Between Image and Preimage Operations on Subsemigroups

Informal description

For any semigroup homomorphism $f \colon M \to N$, the pair of functions `map f` (taking a subsemigroup of $M$ to its image under $f$) and `comap f` (taking a subsemigroup of $N$ to its preimage under $f$) forms a Galois connection between the complete lattices of subsemigroups of $M$ and $N$. In other words, for any subsemigroup $S$ of $M$ and any subsemigroup $T$ of $N$, we have: \[ f(S) \subseteq T \leftrightarrow S \subseteq f^{-1}(T). \]

Subsemigroup.map_le_of_le_comap theorem

{T : Subsemigroup N} {f : M →ₙ* N} : S ≤ T.comap f → S.map f ≤ T

Full source

@[to_additive]
theorem map_le_of_le_comap {T : Subsemigroup N} {f : M →ₙ* N} : S ≤ T.comap f → S.map f ≤ T :=
  (gc_map_comap f).l_le

Image Containment from Preimage Containment for Subsemigroups

Informal description

Let $f \colon M \to N$ be a semigroup homomorphism, $S$ a subsemigroup of $M$, and $T$ a subsemigroup of $N$. If $S$ is contained in the preimage of $T$ under $f$, then the image of $S$ under $f$ is contained in $T$. In symbols: \[ S \subseteq f^{-1}(T) \implies f(S) \subseteq T. \]

Subsemigroup.le_comap_of_map_le theorem

{T : Subsemigroup N} {f : M →ₙ* N} : S.map f ≤ T → S ≤ T.comap f

Full source

@[to_additive]
theorem le_comap_of_map_le {T : Subsemigroup N} {f : M →ₙ* N} : S.map f ≤ T → S ≤ T.comap f :=
  (gc_map_comap f).le_u

Inclusion of Subsemigroup in Preimage Given Image Inclusion

Informal description

For any subsemigroups $S$ of $M$ and $T$ of $N$, and any semigroup 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). \]

Subsemigroup.le_comap_map theorem

{f : M →ₙ* N} : S ≤ (S.map f).comap f

Full source

@[to_additive]
theorem le_comap_map {f : M →ₙ* N} : S ≤ (S.map f).comap f :=
  (gc_map_comap f).le_u_l _

Inclusion of Subsemigroup in Preimage of its Image

Informal description

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

Subsemigroup.map_comap_le theorem

{S : Subsemigroup N} {f : M →ₙ* N} : (S.comap f).map f ≤ S

Full source

@[to_additive]
theorem map_comap_le {S : Subsemigroup N} {f : M →ₙ* N} : (S.comap f).map f ≤ S :=
  (gc_map_comap f).l_u_le _

Image of Preimage is Contained in Original Subsemigroup

Informal description

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

Subsemigroup.monotone_map theorem

{f : M →ₙ* N} : Monotone (map f)

Full source

@[to_additive]
theorem monotone_map {f : M →ₙ* N} : Monotone (map f) :=
  (gc_map_comap f).monotone_l

Monotonicity of Subsemigroup Image under Homomorphism

Informal description

For any semigroup homomorphism $f \colon M \to N$, the image function $\mathrm{map}\, f$ that sends a subsemigroup $S$ of $M$ to its image under $f$ is monotone. That is, if $S \leq T$ are subsemigroups of $M$, then $f(S) \leq f(T)$ as subsemigroups of $N$.

Subsemigroup.monotone_comap theorem

{f : M →ₙ* N} : Monotone (comap f)

Full source

@[to_additive]
theorem monotone_comap {f : M →ₙ* N} : Monotone (comap f) :=
  (gc_map_comap f).monotone_u

Monotonicity of Subsemigroup Preimage under Homomorphism

Informal description

For any semigroup homomorphism $f \colon M \to N$, the preimage operation $\operatorname{comap}(f)$ is monotone. That is, for any two subsemigroups $S, T$ of $N$ with $S \subseteq T$, we have $\operatorname{comap}(f)(S) \subseteq \operatorname{comap}(f)(T)$.

Subsemigroup.map_comap_map theorem

{f : M →ₙ* N} : ((S.map f).comap f).map f = S.map f

Full source

@[to_additive (attr := simp)]
theorem map_comap_map {f : M →ₙ* N} : ((S.map f).comap f).map f = S.map f :=
  (gc_map_comap f).l_u_l_eq_l _

Idempotence of Image-Preimage-Image Operation for Subsemigroups

Informal description

For any semigroup homomorphism $f \colon M \to N$ and any subsemigroup $S$ of $M$, the image of the preimage 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)$.

Subsemigroup.comap_map_comap theorem

{S : Subsemigroup N} {f : M →ₙ* N} : ((S.comap f).map f).comap f = S.comap f

Full source

@[to_additive (attr := simp)]
theorem comap_map_comap {S : Subsemigroup N} {f : M →ₙ* N} :
    ((S.comap f).map f).comap f = S.comap f :=
  (gc_map_comap f).u_l_u_eq_u _

Idempotence of Preimage-Image-Preimage Composition for Subsemigroups

Informal description

For any subsemigroup $S$ of $N$ and any semigroup homomorphism $f \colon M \to N$, the preimage of the image of the preimage of $S$ under $f$ equals the preimage of $S$ under $f$. In other words: \[ f^{-1}(f(f^{-1}(S))) = f^{-1}(S). \]

Subsemigroup.map_sup theorem

(S T : Subsemigroup M) (f : M →ₙ* N) : (S ⊔ T).map f = S.map f ⊔ T.map f

Full source

@[to_additive]
theorem map_sup (S T : Subsemigroup M) (f : M →ₙ* N) : (S ⊔ T).map f = S.map f ⊔ T.map f :=
  (gc_map_comap f).l_sup

Image of Join of Subsemigroups Equals Join of Images

Informal description

Let $M$ and $N$ be semigroups, $S$ and $T$ be subsemigroups of $M$, and $f \colon M \to N$ be a semigroup homomorphism. Then the image of the join $S \vee T$ under $f$ equals the join of the images of $S$ and $T$ under $f$, i.e., \[ f(S \vee T) = f(S) \vee f(T). \]

Subsemigroup.map_iSup theorem

{ι : Sort*} (f : M →ₙ* N) (s : ι → Subsemigroup M) : (iSup s).map f = ⨆ i, (s i).map f

Full source

@[to_additive]
theorem map_iSup {ι : Sort*} (f : M →ₙ* N) (s : ι → Subsemigroup M) :
    (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f).l_iSup

Image of Supremum of Subsemigroups Equals Supremum of Images

Informal description

Let $M$ and $N$ be semigroups, $\iota$ an index set, $f \colon M \to N$ a semigroup homomorphism, and $(S_i)_{i \in \iota}$ a family of subsemigroups of $M$. Then the image of the supremum of the family $(S_i)$ under $f$ equals the supremum of their images: \[ f\left(\bigsqcup_{i \in \iota} S_i\right) = \bigsqcup_{i \in \iota} f(S_i). \]

Subsemigroup.map_inf theorem

(S T : Subsemigroup M) (f : M →ₙ* N) (hf : Function.Injective f) : (S ⊓ T).map f = S.map f ⊓ T.map f

Full source

@[to_additive]
theorem map_inf (S T : Subsemigroup M) (f : M →ₙ* N) (hf : Function.Injective f) :
    (S ⊓ T).map f = S.map f ⊓ T.map f := SetLike.coe_injective (Set.image_inter hf)

Image of Intersection of Subsemigroups under Injective Homomorphism Equals Intersection of Images

Informal description

Let $M$ and $N$ be semigroups, $S$ and $T$ be subsemigroups of $M$, and $f \colon M \to N$ be an injective semigroup 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). \]

Subsemigroup.map_iInf theorem

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

Full source

@[to_additive]
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : M →ₙ* N) (hf : Function.Injective f)
    (s : ι → Subsemigroup 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 Subsemigroups under Injective Homomorphism Equals Infimum of Images

Informal description

Let $M$ and $N$ be semigroups, $\iota$ a nonempty index set, and $f \colon M \to N$ an injective semigroup homomorphism. For any family of subsemigroups $(S_i)_{i \in \iota}$ of $M$, the image of their infimum under $f$ equals the infimum of their images: \[ f\left(\bigsqcap_{i \in \iota} S_i\right) = \bigsqcap_{i \in \iota} f(S_i). \]

Subsemigroup.comap_inf theorem

(S T : Subsemigroup N) (f : M →ₙ* N) : (S ⊓ T).comap f = S.comap f ⊓ T.comap f

Full source

@[to_additive]
theorem comap_inf (S T : Subsemigroup N) (f : M →ₙ* N) : (S ⊓ T).comap f = S.comap f ⊓ T.comap f :=
  (gc_map_comap f).u_inf

Preimage of Intersection of Subsemigroups Equals Intersection of Preimages

Informal description

For any subsemigroups $S$ and $T$ of a semigroup $N$ and any semigroup homomorphism $f \colon M \to 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). \]

Subsemigroup.comap_iInf theorem

{ι : Sort*} (f : M →ₙ* N) (s : ι → Subsemigroup N) : (iInf s).comap f = ⨅ i, (s i).comap f

Full source

@[to_additive]
theorem comap_iInf {ι : Sort*} (f : M →ₙ* N) (s : ι → Subsemigroup N) :
    (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f).u_iInf

Preimage of Infimum of Subsemigroups Equals Infimum of Preimages

Informal description

Let $M$ and $N$ be semigroups, $\iota$ an index set, and $f \colon M \to N$ a semigroup homomorphism. For any family of subsemigroups $(S_i)_{i \in \iota}$ of $N$, the preimage of their infimum under $f$ equals the infimum of their preimages: \[ f^{-1}\left(\bigsqcap_{i \in \iota} S_i\right) = \bigsqcap_{i \in \iota} f^{-1}(S_i). \]

Subsemigroup.map_bot theorem

(f : M →ₙ* N) : (⊥ : Subsemigroup M).map f = ⊥

Full source

@[to_additive (attr := simp)]
theorem map_bot (f : M →ₙ* N) : (⊥ : Subsemigroup M).map f = ⊥ :=
  (gc_map_comap f).l_bot

Image of Bottom Subsemigroup is Bottom

Informal description

For any semigroup homomorphism $f \colon M \to N$, the image of the bottom subsemigroup $\bot$ of $M$ under $f$ is the bottom subsemigroup $\bot$ of $N$.

Subsemigroup.comap_top theorem

(f : M →ₙ* N) : (⊤ : Subsemigroup N).comap f = ⊤

Full source

@[to_additive (attr := simp)]
theorem comap_top (f : M →ₙ* N) : (⊤ : Subsemigroup N).comap f = ⊤ :=
  (gc_map_comap f).u_top

Preimage of Top Subsemigroup is Top

Informal description

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

Subsemigroup.map_id theorem

(S : Subsemigroup M) : S.map (MulHom.id M) = S

Full source

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

Image of Subsemigroup under Identity Homomorphism is Itself

Informal description

For any subsemigroup $S$ of a semigroup $M$, the image of $S$ under the identity multiplicative homomorphism $\mathrm{id}_M \colon M \to M$ is equal to $S$ itself. That is, $S.\mathrm{map}(\mathrm{id}_M) = S$.

Subsemigroup.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 maps for injective semigroup homomorphisms

Informal description

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

Subsemigroup.comap_map_eq_of_injective theorem

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

Full source

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

Preimage of Image Equals Original Subsemigroup for Injective Homomorphisms

Informal description

For any subsemigroup $S$ of a semigroup $M$ and any injective semigroup homomorphism $f \colon M \to N$, the preimage of the image of $S$ under $f$ equals $S$ itself, i.e., $f^{-1}(f(S)) = S$.

Subsemigroup.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 Preimage Map for Injective Semigroup Homomorphisms

Informal description

Given an injective semigroup homomorphism $f \colon M \to N$, the preimage map $\operatorname{comap} f$ from subsemigroups of $N$ to subsemigroups of $M$ is surjective. That is, for every subsemigroup $S$ of $M$, there exists a subsemigroup $T$ of $N$ such that $S = f^{-1}(T)$.

Subsemigroup.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 Subsemigroup Image Map for Injective Homomorphisms

Informal description

If a semigroup homomorphism $f \colon M \to N$ is injective, then the induced map on subsemigroups $\mathrm{map}\, f \colon \mathrm{Subsemigroup}\, M \to \mathrm{Subsemigroup}\, N$ is also injective. That is, for any two subsemigroups $S, T \subseteq M$, if $f(S) = f(T)$ as subsemigroups of $N$, then $S = T$.

Subsemigroup.comap_inf_map_of_injective theorem

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

Full source

@[to_additive]
theorem comap_inf_map_of_injective (S T : Subsemigroup 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 Homomorphisms

Informal description

Let $f \colon M \to N$ be an injective semigroup homomorphism, and let $S$ and $T$ be subsemigroups 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. \]

Subsemigroup.comap_iInf_map_of_injective theorem

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

Full source

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

Preimage of Infimum of Images Equals Infimum of Preimages for Injective Semigroup Homomorphisms

Informal description

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

Subsemigroup.comap_sup_map_of_injective theorem

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

Full source

@[to_additive]
theorem comap_sup_map_of_injective (S T : Subsemigroup 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 Semigroup Homomorphisms

Informal description

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

Subsemigroup.comap_iSup_map_of_injective theorem

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

Full source

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

Preimage of Supremum of Images Equals Supremum of Preimages for Injective Semigroup Homomorphisms

Informal description

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

Subsemigroup.map_le_map_iff_of_injective theorem

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

Full source

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

Image Inclusion Criterion for Injective Semigroup Homomorphisms: $f(S) \subseteq f(T) \leftrightarrow S \subseteq T$

Informal description

Let $f \colon M \to N$ be an injective semigroup homomorphism, and let $S$ and $T$ be subsemigroups 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$.

Subsemigroup.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 Subsemigroup Image under Injective Homomorphism

Informal description

Given an injective semigroup homomorphism $f \colon M \to N$, the image map $\text{map } f$ on subsemigroups of $M$ is strictly monotone. That is, for any two subsemigroups $S$ and $T$ of $M$, if $S < T$ (strict inclusion), then $f(S) < f(T)$ as subsemigroups of $N$.

Subsemigroup.giMapComap definition

: 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 : 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 operations for surjective semigroup homomorphisms

Informal description

Given a surjective semigroup homomorphism $ f : M \to N $, the pair of functions `map f` (taking a subsemigroup of $ M $ to its image under $ f $) and `comap f` (taking a subsemigroup of $ N $ to its preimage under $ f $) forms a Galois insertion. This means: 1. They form a Galois connection (where $ \text{map } f(S) \subseteq T \leftrightarrow S \subseteq \text{comap } f(T) $ for any subsemigroups $ S $ of $ M $ and $ T $ of $ N $) 2. The composition $ \text{map } f \circ \text{comap } f $ is the identity on subsemigroups of $ N $

Subsemigroup.map_comap_eq_of_surjective theorem

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

Full source

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

Image of Preimage Equals Original for Surjective Semigroup Homomorphisms

Informal description

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

Subsemigroup.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 Subsemigroup Image Map for Surjective Homomorphisms

Informal description

Given a surjective semigroup homomorphism $f \colon M \to N$, the function that maps a subsemigroup of $M$ to its image under $f$ is surjective. That is, for every subsemigroup $S$ of $N$, there exists a subsemigroup $T$ of $M$ such that $f(T) = S$.

Subsemigroup.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 Preimage Operation for Surjective Semigroup Homomorphisms

Informal description

If a semigroup homomorphism $f \colon M \to N$ is surjective, then the preimage operation $\text{comap}\, f$ that maps subsemigroups of $N$ to subsemigroups of $M$ is injective. In other words, for any subsemigroups $S, T$ of $N$, if $f^{-1}(S) = f^{-1}(T)$, then $S = T$.

Subsemigroup.map_inf_comap_of_surjective theorem

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

Full source

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

Image of Preimage Intersection Equals Intersection for Surjective Homomorphism

Informal description

Let $f \colon M \to N$ be a surjective semigroup homomorphism, and let $S$ and $T$ be subsemigroups 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. $$

Subsemigroup.map_iInf_comap_of_surjective theorem

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

Full source

@[to_additive]
theorem map_iInf_comap_of_surjective (S : ι → Subsemigroup 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 Semigroup Homomorphism

Informal description

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

Subsemigroup.map_sup_comap_of_surjective theorem

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

Full source

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

Image of Supremum of Preimages Equals Supremum for Surjective Semigroup Homomorphism

Informal description

Let $f \colon M \to N$ be a surjective semigroup homomorphism. For any two subsemigroups $S$ and $T$ of $N$, the image under $f$ of the supremum of their preimages equals the supremum of $S$ and $T$, i.e., \[ f(S \cap f^{-1} \sqcup T \cap f^{-1}) = S \sqcup T. \]

Subsemigroup.map_iSup_comap_of_surjective theorem

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

Full source

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

Image of Supremum of Preimages Equals Supremum for Surjective Semigroup Homomorphism

Informal description

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

Subsemigroup.comap_le_comap_iff_of_surjective theorem

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

Full source

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

Preimage Order Preservation for Surjective Semigroup Homomorphisms: $f^{-1}(S) \leq f^{-1}(T) \leftrightarrow S \leq T$

Informal description

Let $f \colon M \to N$ be a surjective semigroup homomorphism. For any two subsemigroups $S$ and $T$ of $N$, 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 $$

Subsemigroup.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 Subsemigroup Preimage for Surjective Homomorphisms

Informal description

Given a surjective semigroup homomorphism $f \colon M \to N$, the preimage function $\text{comap}_f \colon \text{Subsemigroup}(N) \to \text{Subsemigroup}(M)$ is strictly monotone. That is, for any two subsemigroups $S, T$ of $N$, if $S < T$ then $\text{comap}_f(S) < \text{comap}_f(T)$.

Subsemigroup.topEquiv definition

: (⊤ : Subsemigroup M) ≃* M

Full source

/-- The top subsemigroup is isomorphic to the semigroup. -/
@[to_additive (attr := simps)
  "The top additive subsemigroup is isomorphic to the additive semigroup."]
def topEquiv : (⊤ : Subsemigroup 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 the top subsemigroup and the semigroup

Informal description

The multiplicative equivalence between the top subsemigroup (the entire semigroup $M$) and $M$ itself. This isomorphism maps each element $x$ in the top subsemigroup to itself in $M$, and its inverse maps each element $x$ in $M$ to the element $\langle x, \text{mem\_top}\ x \rangle$ in the top subsemigroup, where $\text{mem\_top}\ x$ is a proof that $x$ belongs to the top subsemigroup. The isomorphism preserves the multiplication operation.

Subsemigroup.topEquiv_toMulHom theorem

: ((topEquiv : _ ≃* M) : _ →ₙ* M) = MulMemClass.subtype (⊤ : Subsemigroup M)

Full source

@[to_additive (attr := simp)]
theorem topEquiv_toMulHom :
    ((topEquiv : _ ≃* M) : _ →ₙ* M) = MulMemClass.subtype (⊤ : Subsemigroup M) :=
  rfl

Top subsemigroup isomorphism coincides with inclusion homomorphism

Informal description

The underlying multiplicative homomorphism of the isomorphism between the top subsemigroup of $M$ and $M$ itself is equal to the inclusion homomorphism from the top subsemigroup into $M$.

Subsemigroup.equivMapOfInjective definition

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

Full source

/-- A subsemigroup is isomorphic to its image under an injective function -/
@[to_additive "An additive subsemigroup is isomorphic to its image under an injective function"]
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 (map_mul f _ _) }

Isomorphism between a subsemigroup and its image under an injective homomorphism

Informal description

Given an injective semigroup homomorphism $ f : M \to N $ and a subsemigroup $ S $ of $ M $, the subsemigroup $ S $ is isomorphic to its image $ f(S) $ under $ f $. The isomorphism is given by the bijection between $ S $ and $ f(S) $ that preserves the multiplication operation.

Subsemigroup.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 Element under Subsemigroup Isomorphism via Injective Homomorphism

Informal description

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

Subsemigroup.closure_closure_coe_preimage theorem

{s : Set M} : closure ((Subtype.val : closure s → M) ⁻¹' s) = ⊤

Full source

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

Closure of Preimage in Subsemigroup Closure is Top

Informal description

For any subset $s$ of a semigroup $M$, the subsemigroup generated by the preimage of $s$ under the inclusion map from the subsemigroup closure of $s$ is the entire closure subsemigroup, i.e., $\text{closure}(\text{closure}(s)^{-1}(s)) = \top$.

Subsemigroup.prod definition

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

Full source

/-- Given `Subsemigroup`s `s`, `t` of semigroups `M`, `N` respectively, `s × t` as a subsemigroup
of `M × N`. -/
@[to_additive prod
      "Given `AddSubsemigroup`s `s`, `t` of `AddSemigroup`s `A`, `B` respectively,
      `s × t` as an `AddSubsemigroup` of `A × B`."]
def prod (s : Subsemigroup M) (t : Subsemigroup N) : Subsemigroup (M × N) where
  carrier := s ×ˢ t
  mul_mem' hp hq := ⟨s.mul_mem hp.1 hq.1, t.mul_mem hp.2 hq.2⟩

Product of subsemigroups

Informal description

Given subsemigroups $s$ of a semigroup $M$ and $t$ of a semigroup $N$, the product subsemigroup $s \times t$ is the subsemigroup of $M \times N$ consisting of all pairs $(m, n)$ where $m \in s$ and $n \in t$, and is closed under the componentwise multiplication operation.

Subsemigroup.coe_prod theorem

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

Full source

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

Underlying Set of Product Subsemigroup Equals Cartesian Product of Underlying Sets

Informal description

For subsemigroups $s$ of a semigroup $M$ and $t$ of a semigroup $N$, the underlying set of the product subsemigroup $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$ as subsets of $M \times N$.

Subsemigroup.mem_prod theorem

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

Full source

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

Membership Criterion for Product of Subsemigroups: $(m, n) \in s \times t \leftrightarrow m \in s \land n \in t$

Informal description

For any subsemigroups $s$ of a semigroup $M$ and $t$ of a semigroup $N$, and any pair $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$.

Subsemigroup.prod_mono theorem

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

Full source

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

Monotonicity of Subsemigroup Product with Respect to Inclusion

Informal description

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

Subsemigroup.prod_top theorem

(s : Subsemigroup M) : s.prod (⊤ : Subsemigroup N) = s.comap (MulHom.fst M N)

Full source

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

Product of Subsemigroup with Full Subsemigroup Equals Preimage under First Projection

Informal description

For any subsemigroup $s$ of a semigroup $M$, the product subsemigroup $s \times N$ (where $N$ is the full subsemigroup of a semigroup $N$) is equal to the preimage of $s$ under the first projection homomorphism $\text{fst} : M \times N \to M$.

Subsemigroup.top_prod theorem

(s : Subsemigroup N) : (⊤ : Subsemigroup M).prod s = s.comap (MulHom.snd M N)

Full source

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

Product of Top Subsemigroup with Another Subsemigroup Equals Preimage Under Second Projection

Informal description

For any subsemigroup $s$ of a semigroup $N$, the product of the top subsemigroup of $M$ with $s$ is equal to the preimage of $s$ under the second projection homomorphism $\operatorname{snd} : M \times N \to N$.

Subsemigroup.top_prod_top theorem

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

Full source

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

Product of Top Subsemigroups is Top

Informal description

The product of the top subsemigroup of $M$ and the top subsemigroup of $N$ is equal to the top subsemigroup of $M \times N$, i.e., $M \times N = M \times N$.

Subsemigroup.bot_prod_bot theorem

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

Full source

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

Product of Bottom Subsemigroups is Bottom

Informal description

The product of the bottom subsemigroup of $M$ and the bottom subsemigroup of $N$ is equal to the bottom subsemigroup of $M \times N$, i.e., $\bot \times \bot = \bot$.

Subsemigroup.prodEquiv definition

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

Full source

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

Isomorphism between product subsemigroup and product of subsemigroups

Informal description

Given subsemigroups $s$ of a semigroup $M$ and $t$ of a semigroup $N$, the multiplicative equivalence (isomorphism) between the product subsemigroup $s \times t$ (as a subsemigroup of $M \times N$) and the direct product of subsemigroups $s \times t$ (as a product type). The isomorphism preserves the multiplication operation in both directions.

Subsemigroup.mem_map_equiv theorem

{f : M ≃* N} {K : Subsemigroup M} {x : N} : x ∈ K.map (f : M →ₙ* N) ↔ f.symm x ∈ K

Full source

@[to_additive]
theorem mem_map_equiv {f : M ≃* N} {K : Subsemigroup M} {x : N} :
    x ∈ K.map (f : M →ₙ* N)x ∈ K.map (f : M →ₙ* N) ↔ f.symm x ∈ K :=
  @Set.mem_image_equiv _ _ (K : Set M) f.toEquiv x

Characterization of Image Membership via Multiplicative Isomorphism Inverse

Informal description

Let $f \colon M \simeq^* N$ be a multiplicative isomorphism between semigroups $M$ and $N$, $K$ be a subsemigroup of $M$, and $x$ be an element of $N$. Then $x$ belongs to the image of $K$ under $f$ if and only if the inverse isomorphism $f^{-1}$ maps $x$ back into $K$, i.e., \[ x \in f(K) \leftrightarrow f^{-1}(x) \in K. \]

Subsemigroup.map_equiv_eq_comap_symm theorem

(f : M ≃* N) (K : Subsemigroup M) : K.map (f : M →ₙ* N) = K.comap (f.symm : N →ₙ* M)

Full source

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

Image of Subsemigroup under Isomorphism Equals Preimage under Inverse

Informal description

Let $f \colon M \simeq^* N$ be a multiplicative isomorphism between semigroups $M$ and $N$, and let $K$ be a subsemigroup of $M$. Then the image of $K$ under $f$ is equal to the preimage of $K$ under $f^{-1}$, i.e., \[ f(K) = f^{-1}^{-1}(K). \]

Subsemigroup.comap_equiv_eq_map_symm theorem

(f : N ≃* M) (K : Subsemigroup M) : K.comap (f : N →ₙ* M) = K.map (f.symm : M →ₙ* N)

Full source

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

Preimage of Subsemigroup under Isomorphism Equals Image under Inverse

Informal description

Let $f \colon N \simeq^* M$ be a multiplicative isomorphism between semigroups $N$ and $M$, and let $K$ be a subsemigroup of $M$. Then the preimage of $K$ under $f$ is equal to the image of $K$ under $f^{-1}$, i.e., \[ f^{-1}(K) = f^{-1}(K). \]

Subsemigroup.map_equiv_top theorem

(f : M ≃* N) : (⊤ : Subsemigroup M).map (f : M →ₙ* N) = ⊤

Full source

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

Image of Top Subsemigroup under Multiplicative Isomorphism is Top Subsemigroup

Informal description

For any multiplicative isomorphism $f \colon M \simeq^* N$ between semigroups $M$ and $N$, the image of the top subsemigroup of $M$ under $f$ is equal to the top subsemigroup of $N$.

Subsemigroup.le_prod_iff theorem

 {s : Subsemigroup M} {t : Subsemigroup N} {u : Subsemigroup (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 : Subsemigroup M} {t : Subsemigroup N} {u : Subsemigroup (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⟩⟩

Characterization of Subsemigroup Inclusion in Product via Projections

Informal description

For subsemigroups $s$ of $M$, $t$ of $N$, and $u$ of $M \times N$, the following are equivalent: 1. $u$ is contained in the product subsemigroup $s \times t$; 2. 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$ if and only if $\pi_1(u) \leq s$ and $\pi_2(u) \leq t$, where $\pi_1$ and $\pi_2$ are the first and second projection homomorphisms respectively.

MulHom.srange definition

(f : M →ₙ* N) : Subsemigroup N

Full source

/-- The range of a semigroup homomorphism is a subsemigroup. See Note [range copy pattern]. -/
@[to_additive "The range of an `AddHom` is an `AddSubsemigroup`."]
def srange (f : M →ₙ* N) : Subsemigroup N :=
  ((⊤ : Subsemigroup M).map f).copy (Set.range f) Set.image_univ.symm

Range of a semigroup homomorphism

Informal description

Given a semigroup homomorphism $f \colon M \to N$, the range of $f$ is the subsemigroup of $N$ consisting of all elements of the form $f(x)$ for some $x \in M$.

MulHom.coe_srange theorem

(f : M →ₙ* N) : (f.srange : Set N) = Set.range f

Full source

@[to_additive (attr := simp)]
theorem coe_srange (f : M →ₙ* N) : (f.srange : Set N) = Set.range f :=
  rfl

Range of Semigroup Homomorphism as a Set

Informal description

For any semigroup homomorphism $f \colon M \to N$, the underlying set of the range subsemigroup of $f$ is equal to the range of $f$ as a function, i.e., $\{f(x) \mid x \in M\}$.

MulHom.mem_srange theorem

{f : M →ₙ* N} {y : N} : y ∈ f.srange ↔ ∃ x, f x = y

Full source

@[to_additive (attr := simp)]
theorem mem_srange {f : M →ₙ* N} {y : N} : y ∈ f.srangey ∈ f.srange ↔ ∃ x, f x = y :=
  Iff.rfl

Characterization of Elements in the Range of a Semigroup Homomorphism

Informal description

For any semigroup homomorphism $f \colon M \to N$ and any 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$.

MulHom.srange_mk theorem

(f : M → N) (hf) : srange ⟨f, hf⟩ = ⟨Set.range f, srange_mk_aux_mul hf⟩

Full source

@[to_additive (attr := simp)] theorem srange_mk (f : M → N) (hf) :
    srange ⟨f, hf⟩ = ⟨Set.range f, srange_mk_aux_mul hf⟩ := rfl

Range of Semigroup Homomorphism Constructed from Operation-Preserving Function

Informal description

Given a function $f \colon M \to N$ that preserves the semigroup operation (i.e., $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M$), the range of the semigroup homomorphism $\langle f, hf \rangle$ (where $hf$ is the proof that $f$ preserves the operation) is equal to the subsemigroup of $N$ generated by the set-theoretic range of $f$.

MulHom.srange_eq_map theorem

(f : M →ₙ* N) : f.srange = (⊤ : Subsemigroup M).map f

Full source

@[to_additive]
theorem srange_eq_map (f : M →ₙ* N) : f.srange = (⊤ : Subsemigroup M).map f :=
  copy_eq _

Range of Semigroup Homomorphism Equals Image of Top Subsemigroup

Informal description

For any semigroup homomorphism $f \colon M \to N$, the range of $f$ is equal to the image of the top subsemigroup of $M$ under $f$. In other words, $f.srange = (\top : \text{Subsemigroup } M).map f$.

MulHom.map_srange theorem

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

Full source

@[to_additive]
theorem map_srange (g : N →ₙ* P) (f : M →ₙ* N) : f.srange.map g = (g.comp f).srange := by
  simpa only [srange_eq_map] using (⊤ : Subsemigroup M).map_map g f

Image of Range under Homomorphism Equals Range of Composition

Informal description

Let $M$, $N$, and $P$ be semigroups, and let $f \colon M \to N$ and $g \colon N \to P$ be semigroup homomorphisms. Then the image of the range of $f$ under $g$ is equal to the range of the composition $g \circ f$. In symbols: $$g(f.srange) = (g \circ f).srange.$$

MulHom.srange_eq_top_iff_surjective theorem

{N} [Mul N] {f : M →ₙ* N} : f.srange = (⊤ : Subsemigroup N) ↔ Function.Surjective f

Full source

@[to_additive]
theorem srange_eq_top_iff_surjective {N} [Mul N] {f : M →ₙ* N} :
    f.srange = (⊤ : Subsemigroup N) ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_srange, coe_top]) Set.range_eq_univ

Range Equals Top Subsemigroup iff Homomorphism is Surjective

Informal description

For a non-unital multiplicative homomorphism $f \colon M \to N$ between semigroups, the range of $f$ is equal to the entire subsemigroup $N$ if and only if $f$ is surjective. In other words, $f.srange = \top \leftrightarrow \text{Surjective}(f)$.

MulHom.srange_eq_top_of_surjective theorem

{N} [Mul N] (f : M →ₙ* N) (hf : Function.Surjective f) : f.srange = (⊤ : Subsemigroup N)

Full source

/-- The range of a surjective semigroup hom is the whole of the codomain. -/
@[to_additive (attr := simp)
  "The range of a surjective `AddSemigroup` hom is the whole of the codomain."]
theorem srange_eq_top_of_surjective {N} [Mul N] (f : M →ₙ* N) (hf : Function.Surjective f) :
    f.srange = (⊤ : Subsemigroup N) :=
  srange_eq_top_iff_surjective.2 hf

Surjective Homomorphism Has Full Range

Informal description

For a semigroup homomorphism $f \colon M \to N$, if $f$ is surjective, then the range of $f$ is equal to the entire subsemigroup $N$, i.e., $f.\text{srange} = \top$.

MulHom.mclosure_preimage_le theorem

(f : M →ₙ* N) (s : Set N) : closure (f ⁻¹' s) ≤ (closure s).comap f

Full source

@[to_additive]
theorem mclosure_preimage_le (f : M →ₙ* N) (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

Subsemigroup closure of preimage is contained in preimage of closure

Informal description

Let $M$ and $N$ be semigroups, $f : M \to N$ a semigroup homomorphism, and $s \subseteq N$ a subset. Then the subsemigroup generated by the preimage $f^{-1}(s)$ is contained in the preimage of the subsemigroup generated by $s$. In other words, $\text{closure}(f^{-1}(s)) \leq f^{-1}(\text{closure}(s))$.

MulHom.map_mclosure theorem

(f : M →ₙ* N) (s : Set M) : (closure s).map f = closure (f '' s)

Full source

/-- The image under a semigroup hom of the subsemigroup generated by a set equals the subsemigroup
generated by the image of the set. -/
@[to_additive
      "The image under an `AddSemigroup` hom of the `AddSubsemigroup` generated by a set
      equals the `AddSubsemigroup` generated by the image of the set."]
theorem map_mclosure (f : M →ₙ* N) (s : Set M) : (closure s).map f = closure (f '' s) :=
  Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Subsemigroup.gi N).gc (Subsemigroup.gi M).gc
    fun _ ↦ rfl

Image of Generated Subsemigroup Equals Generated Image

Informal description

Let $M$ and $N$ be semigroups and $f : M \to N$ be a semigroup homomorphism. For any subset $s \subseteq M$, the image under $f$ of the subsemigroup generated by $s$ is equal to the subsemigroup generated by the image $f(s)$ in $N$. That is, \[ f(\langle s \rangle) = \langle f(s) \rangle. \]

MulHom.restrict definition

{N : Type*} [Mul N] [SetLike σ M] [MulMemClass σ M] (f : M →ₙ* N) (S : σ) : S →ₙ* N

Full source

/-- Restriction of a semigroup hom to a subsemigroup of the domain. -/
@[to_additive "Restriction of an AddSemigroup hom to an `AddSubsemigroup` of the domain."]
def restrict {N : Type*} [Mul N] [SetLike σ M] [MulMemClass σ M] (f : M →ₙ* N) (S : σ) : S →ₙ* N :=
  f.comp (MulMemClass.subtype S)

Restriction of a semigroup homomorphism to a subsemigroup

Informal description

Given a semigroup homomorphism $ f \colon M \to N $ between multiplicative structures and a subsemigroup $ S $ of $ M $, the restriction of $ f $ to $ S $ is a semigroup homomorphism from $ S $ to $ N $. This is obtained by composing $ f $ with the canonical inclusion $ S \hookrightarrow M $.

MulHom.restrict_apply theorem

{N : Type*} [Mul N] [SetLike σ M] [MulMemClass σ M] (f : M →ₙ* N) {S : σ} (x : S) : f.restrict S x = f x

Full source

@[to_additive (attr := simp)]
theorem restrict_apply {N : Type*} [Mul N] [SetLike σ M] [MulMemClass σ M] (f : M →ₙ* N) {S : σ}
    (x : S) : f.restrict S x = f x :=
  rfl

Restriction of Homomorphism Evaluates as Original

Informal description

Let $M$ and $N$ be multiplicative structures, and let $\sigma$ be a set-like structure on $M$ with a multiplicative membership class. Given a semigroup homomorphism $f \colon M \to N$ and a subsemigroup $S$ of $M$ (where $S$ is an element of $\sigma$), for any element $x \in S$, the restriction of $f$ to $S$ evaluated at $x$ equals $f(x)$, i.e., \[ f|_S(x) = f(x). \]

MulHom.codRestrict definition

[SetLike σ N] [MulMemClass σ N] (f : M →ₙ* N) (S : σ) (h : ∀ x, f x ∈ S) : M →ₙ* S

Full source

/-- Restriction of a semigroup hom to a subsemigroup of the codomain. -/
@[to_additive (attr := simps)
  "Restriction of an `AddSemigroup` hom to an `AddSubsemigroup` of the codomain."]
def codRestrict [SetLike σ N] [MulMemClass σ N] (f : M →ₙ* N) (S : σ) (h : ∀ x, f x ∈ S) :
    M →ₙ* S where
  toFun n := ⟨f n, h n⟩
  map_mul' x y := Subtype.eq (map_mul f x y)

Restriction of a semigroup homomorphism to a subsemigroup of the codomain

Informal description

Given a semigroup homomorphism $ f \colon M \to N $ and a subsemigroup $ S $ of $ N $ such that $ f(x) \in S $ for all $ x \in M $, the function $ f $ can be restricted to a homomorphism from $ M $ to $ S $.

MulHom.srangeRestrict definition

{N} [Mul N] (f : M →ₙ* N) : M →ₙ* f.srange

Full source

/-- Restriction of a semigroup hom to its range interpreted as a subsemigroup. -/
@[to_additive "Restriction of an `AddSemigroup` hom to its range interpreted as a subsemigroup."]
def srangeRestrict {N} [Mul N] (f : M →ₙ* N) : M →ₙ* f.srange :=
  (f.codRestrict f.srange) fun x => ⟨x, rfl⟩

Restriction of a semigroup homomorphism to its range

Informal description

Given a semigroup homomorphism $ f \colon M \to N $, the restriction of $ f $ to its range is a homomorphism from $ M $ to the subsemigroup $ \text{srange}(f) $ of $ N $, where $ \text{srange}(f) $ consists of all elements of the form $ f(x) $ for $ x \in M $.

MulHom.coe_srangeRestrict theorem

{N} [Mul N] (f : M →ₙ* N) (x : M) : (f.srangeRestrict x : N) = f x

Full source

@[to_additive (attr := simp)]
theorem coe_srangeRestrict {N} [Mul N] (f : M →ₙ* N) (x : M) : (f.srangeRestrict x : N) = f x :=
  rfl

Range-Restricted Homomorphism Recovers Original Value: $(f_{\text{srange}}(x) : N) = f(x)$

Informal description

For any semigroup homomorphism $f \colon M \to N$ and any element $x \in M$, the image of $x$ under the range-restricted homomorphism $f_{\text{srange}}$ (viewed as an element of $N$) is equal to $f(x)$. In other words, the inclusion map from the range of $f$ back into $N$ recovers the original value of $f(x)$.

MulHom.srangeRestrict_surjective theorem

(f : M →ₙ* N) : Function.Surjective f.srangeRestrict

Full source

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

Surjectivity of the Range-Restricted Semigroup Homomorphism

Informal description

For any semigroup homomorphism $f \colon M \to N$, the restricted homomorphism $f_{\text{srange}} \colon M \to \text{srange}(f)$ is surjective, where $\text{srange}(f) = \{f(x) \mid x \in M\}$ is the range of $f$ viewed as a subsemigroup of $N$.

MulHom.prod_map_comap_prod' theorem

 {M' : Type*} {N' : Type*} [Mul M'] [Mul N'] (f : M →ₙ* N) (g : M' →ₙ* N') (S : Subsemigroup N) (S' : Subsemigroup 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*} [Mul M'] [Mul N'] (f : M →ₙ* N)
    (g : M' →ₙ* N') (S : Subsemigroup N) (S' : Subsemigroup 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 Subsemigroup under Product Homomorphism Equals Product of Preimages

Informal description

Let $M, M', N, N'$ be semigroups, and let $f \colon M \to N$ and $g \colon M' \to N'$ be semigroup homomorphisms. For any subsemigroups $S \subseteq N$ and $S' \subseteq N'$, the preimage of the product subsemigroup $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, $$(f \times g)^{-1}(S \times S') = f^{-1}(S) \times g^{-1}(S').$$

MulHom.subsemigroupComap definition

(f : M →ₙ* N) (N' : Subsemigroup N) : N'.comap f →ₙ* N'

Full source

/-- The `MulHom` from the preimage of a subsemigroup to itself. -/
@[to_additive (attr := simps)
  "The `AddHom` from the preimage of an additive subsemigroup to itself."]
def subsemigroupComap (f : M →ₙ* N) (N' : Subsemigroup N) :
    N'.comap f →ₙ* N' where
  toFun x := ⟨f x, x.prop⟩
  map_mul' x y := Subtype.eq <| map_mul (M := M) (N := N) f x y

Restriction of a multiplicative homomorphism to a preimage subsemigroup

Informal description

Given a multiplicative homomorphism $ f : M \to N $ and a subsemigroup $ N' $ of $ N $, the function $ f $ restricts to a homomorphism from the preimage subsemigroup $ f^{-1}(N') $ to $ N' $. Specifically, for any $ x \in f^{-1}(N') $, the image $ f(x) $ lies in $ N' $, and this restriction preserves the multiplicative structure.

MulHom.subsemigroupMap definition

(f : M →ₙ* N) (M' : Subsemigroup M) : M' →ₙ* M'.map f

Full source

/-- The `MulHom` from a subsemigroup to its image.
See `MulEquiv.subsemigroupMap` for a variant for `MulEquiv`s. -/
@[to_additive (attr := simps)
      "the `AddHom` from an additive subsemigroup to its image. See
      `AddEquiv.addSubsemigroupMap` for a variant for `AddEquiv`s."]
def subsemigroupMap (f : M →ₙ* N) (M' : Subsemigroup M) :
    M' →ₙ* M'.map f where
  toFun x := ⟨f x, ⟨x, x.prop, rfl⟩⟩
  map_mul' x y := Subtype.eq <| map_mul (M := M) (N := N) f x y

Restriction of a semigroup homomorphism to a subsemigroup and its image

Informal description

Given a semigroup homomorphism $f \colon M \to N$ and a subsemigroup $M'$ of $M$, the function `MulHom.subsemigroupMap` restricts $f$ to $M'$ and maps it to the image subsemigroup $f(M')$ in $N$. Specifically, for any $x \in M'$, the function sends $x$ to $f(x) \in f(M')$, preserving the multiplicative structure.

MulHom.subsemigroupMap_surjective theorem

(f : M →ₙ* N) (M' : Subsemigroup M) : Function.Surjective (f.subsemigroupMap M')

Full source

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

Surjectivity of Restricted Semigroup Homomorphism on Image Subsemigroup

Informal description

Given a semigroup homomorphism $f \colon M \to N$ and a subsemigroup $M'$ of $M$, the restricted homomorphism $f|_{M'} \colon M' \to f(M')$ is surjective. That is, for every $y \in f(M')$, there exists an $x \in M'$ such that $f(x) = y$.

Subsemigroup.srange_fst theorem

[Nonempty N] : (fst M N).srange = ⊤

Full source

@[to_additive (attr := simp)]
theorem srange_fst [Nonempty N] : (fst M N).srange = ⊤ :=
  (fst M N).srange_eq_top_of_surjective <| Prod.fst_surjective

First Projection Homomorphism Has Full Range for Nonempty Second Component

Informal description

For any nonempty type $N$, the range of the first projection homomorphism $\operatorname{fst} : M \times N \to M$ is the entire subsemigroup $M$, i.e., $\operatorname{srange}(\operatorname{fst}) = \top$.

Subsemigroup.srange_snd theorem

[Nonempty M] : (snd M N).srange = ⊤

Full source

@[to_additive (attr := simp)]
theorem srange_snd [Nonempty M] : (snd M N).srange = ⊤ :=
  (snd M N).srange_eq_top_of_surjective <| Prod.snd_surjective

Range of Second Projection Homomorphism is Full Subsemigroup for Nonempty Types

Informal description

For nonempty types $M$ and $N$, the range of the second projection homomorphism $\operatorname{snd} : M \times N \to N$ is equal to the entire subsemigroup $N$, i.e., $\operatorname{snd}.\text{srange} = \top$.

Subsemigroup.prod_eq_top_iff theorem

[Nonempty M] [Nonempty N] {s : Subsemigroup M} {t : Subsemigroup N} : s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

Full source

@[to_additive prod_eq_top_iff]
theorem prod_eq_top_iff [Nonempty M] [Nonempty N] {s : Subsemigroup M} {t : Subsemigroup N} :
    s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤ := by
  simp only [eq_top_iff, le_prod_iff, ← (gc_map_comap _).le_iff_le, ← srange_eq_map, srange_fst,
    srange_snd]

Product Subsemigroup is Top if and only if Both Components are Top

Informal description

For nonempty semigroups $M$ and $N$, and subsemigroups $s$ of $M$ and $t$ of $N$, the product subsemigroup $s \times t$ is equal to the top subsemigroup of $M \times N$ if and only if both $s$ is the top subsemigroup of $M$ and $t$ is the top subsemigroup of $N$.

Subsemigroup.inclusion definition

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

Full source

/-- The semigroup hom associated to an inclusion of subsemigroups. -/
@[to_additive "The `AddSemigroup` hom associated to an inclusion of subsemigroups."]
def inclusion {S T : Subsemigroup M} (h : S ≤ T) : S →ₙ* T :=
  (MulMemClass.subtype S).codRestrict _ fun x => h x.2

Inclusion homomorphism of subsemigroups

Informal description

Given two subsemigroups $S$ and $T$ of a semigroup $M$ such that $S$ is contained in $T$ (i.e., $S \leq T$), the inclusion map from $S$ to $T$ is a semigroup homomorphism. This is constructed by restricting the canonical inclusion homomorphism of $S$ into $M$ to have codomain $T$.

Subsemigroup.range_subtype theorem

(s : Subsemigroup M) : (MulMemClass.subtype s).srange = s

Full source

@[to_additive (attr := simp)]
theorem range_subtype (s : Subsemigroup M) : (MulMemClass.subtype s).srange = s :=
  SetLike.coe_injective <| (coe_srange _).trans <| Subtype.range_coe

Range of Subsemigroup Inclusion Equals Itself

Informal description

For any subsemigroup $s$ of a semigroup $M$, the range of the canonical inclusion homomorphism $\text{subtype} \colon s \to M$ is equal to $s$ itself. In other words, the image of $s$ under the inclusion map is exactly $s$.

MulEquiv.subsemigroupCongr definition

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

Full source

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

Multiplicative isomorphism between equal subsemigroups

Informal description

Given two subsemigroups $S$ and $T$ of a multiplicative semigroup that are equal ($S = T$), the function constructs a multiplicative isomorphism (equivalence) between $S$ and $T$ by using the identity map.

MulEquiv.ofLeftInverse definition

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

Full source

/-- A semigroup homomorphism `f : M →ₙ* N` with a left-inverse `g : N → M` defines a multiplicative
equivalence between `M` and `f.srange`.

This is a bidirectional version of `MulHom.srangeRestrict`. -/
@[to_additive (attr := simps +simpRhs)
      "An additive semigroup homomorphism `f : M →+ N` with a left-inverse
      `g : N → M` defines an additive equivalence between `M` and `f.srange`.
      This is a bidirectional version of `AddHom.srangeRestrict`. "]
def ofLeftInverse (f : M →ₙ* N) {g : N → M} (h : Function.LeftInverse g f) : M ≃* f.srange :=
  { f.srangeRestrict with
    toFun := f.srangeRestrict
    invFun := g ∘ MulMemClass.subtype f.srange
    left_inv := h
    right_inv := fun x =>
      Subtype.ext <|
        let ⟨x', hx'⟩ := MulHom.mem_srange.mp x.prop
        show f (g x) = x by rw [← hx', h x'] }

Multiplicative equivalence from a homomorphism with left inverse

Informal description

Given a semigroup 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 between $ M $ and the range $ \text{srange}(f) $ of $ f $. This equivalence is constructed by restricting $ f $ to its range and using $ g $ to define the inverse map.

MulEquiv.subsemigroupMap definition

(e : M ≃* N) (S : Subsemigroup M) : S ≃* S.map (e : M →ₙ* N)

Full source

/-- A `MulEquiv` `φ` between two semigroups `M` and `N` induces a `MulEquiv` between
a subsemigroup `S ≤ M` and the subsemigroup `φ(S) ≤ N`.
See `MulHom.subsemigroupMap` for a variant for `MulHom`s. -/
@[to_additive (attr := simps)
      "An `AddEquiv` `φ` between two additive semigroups `M` and `N` induces an `AddEquiv`
      between a subsemigroup `S ≤ M` and the subsemigroup `φ(S) ≤ N`.
      See `AddHom.addSubsemigroupMap` for a variant for `AddHom`s."]
def subsemigroupMap (e : M ≃* N) (S : Subsemigroup M) : S ≃* S.map (e : M →ₙ* N) :=
  { -- we restate this for `simps` to avoid `⇑e.symm.toEquiv x`
    (e : M →ₙ* N).subsemigroupMap S,
    (e : M ≃ N).image S with
    toFun := fun x => ⟨e x, _⟩
    invFun := fun x => ⟨e.symm x, _⟩ }

Multiplicative isomorphism between a subsemigroup and its image under a multiplicative isomorphism

Informal description

Given a multiplicative isomorphism $e \colon M \simeq^* N$ between semigroups $M$ and $N$, and a subsemigroup $S$ of $M$, the function constructs a multiplicative isomorphism between $S$ and the image subsemigroup $e(S)$ in $N$. The isomorphism maps each element $x \in S$ to $e(x) \in e(S)$, and its inverse maps each $y \in e(S)$ back to $e^{-1}(y) \in S$, preserving the multiplicative structure in both directions.

Subsemigroup.map_comap_eq theorem

(f : M →ₙ* N) (S : Subsemigroup N) : (S.comap f).map f = S ⊓ f.srange

Full source

@[to_additive]
theorem map_comap_eq (f : M →ₙ* N) (S : Subsemigroup N) : (S.comap f).map f = S ⊓ f.srange :=
  SetLike.coe_injective Set.image_preimage_eq_inter_range

Image-Preimage Identity for Semigroup Homomorphisms: $f(f^{-1}(S)) = S \cap \mathrm{range}(f)$

Informal description

Let $f \colon M \to N$ be a semigroup homomorphism and $S$ be a subsemigroup of $N$. Then the image of the preimage of $S$ under $f$ is equal to the intersection of $S$ with the range of $f$, i.e., $$ f(f^{-1}(S)) = S \cap \mathrm{range}(f). $$

Subsemigroup.map_comap_eq_self theorem

{f : M →ₙ* N} {S : Subsemigroup N} (h : S ≤ f.srange) : (S.comap f).map f = S

Full source

@[to_additive]
theorem map_comap_eq_self {f : M →ₙ* N} {S : Subsemigroup N} (h : S ≤ f.srange) :
    (S.comap f).map f = S := by
  simpa only [inf_of_le_left h] using map_comap_eq f S

Image-Preimage Identity for Surjective-Like Subsemigroups: $f(f^{-1}(S)) = S$ when $S \subseteq \mathrm{range}(f)$

Informal description

Let $f \colon M \to N$ be a semigroup homomorphism and $S$ be a subsemigroup 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. $$

Mathlib.Algebra.Group.Subsemigroup.Operations

Main definitions

Conversion between multiplicative and additive definitions

(Commutative) semigroup structure on a subsemigroup

Operations on subsemigroups

Semigroup homomorphisms between subsemigroups

Operations on `MulHom`s

Implementation notes

Tags

Main definitions

Conversion between multiplicative and additive definitions

(Commutative) semigroup structure on a subsemigroup

Operations on subsemigroups

Semigroup homomorphisms between subsemigroups

Operations on MulHoms

Implementation notes

Tags

Operations on `MulHom`s