Documentation

Mathlib.GroupTheory.Subsemigroup.Operations

Operations on Subsemigroups #

In this file we define various operations on Subsemigroups and MulHoms.

Main definitions #

Conversion between multiplicative and additive definitions #

(Commutative) semigroup structure on a subsemigroup #

Operations on subsemigroups #

Semigroup homomorphisms between subsemigroups #

Operations on mul_homs #

Implementation notes #

This file follows closely GroupTheory/Submonoid/Operations.lean, omitting only that which is necessary.

Tags #

subsemigroup, range, product, map, comap

Conversion to/from Additive/Multiplicative #

@[simp]
theorem Subsemigroup.toAddSubsemigroup_apply_coe {M : Type u_1} [inst : Mul M] (S : Subsemigroup M) :
↑((RelIso.toRelEmbedding Subsemigroup.toAddSubsemigroup).toEmbedding S) = Additive.toMul ⁻¹' S
@[simp]
theorem Subsemigroup.toAddSubsemigroup_symm_apply_coe {M : Type u_1} [inst : Mul M] (S : AddSubsemigroup (Additive M)) :
↑((RelIso.toRelEmbedding (RelIso.symm Subsemigroup.toAddSubsemigroup)).toEmbedding S) = Additive.ofMul ⁻¹' S

Subsemigroups of semigroup M are isomorphic to additive subsemigroups of Additive M.

Equations
  • One or more equations did not get rendered due to their size.
@[inline]

Additive subsemigroups of an additive semigroup Additive M are isomorphic to subsemigroups of M.

Equations
  • AddSubsemigroup.toSubsemigroup' = OrderIso.symm Subsemigroup.toAddSubsemigroup
theorem Subsemigroup.toAddSubsemigroup_closure {M : Type u_1} [inst : Mul M] (S : Set M) :
(RelIso.toRelEmbedding Subsemigroup.toAddSubsemigroup).toEmbedding (Subsemigroup.closure S) = AddSubsemigroup.closure (Additive.toMul ⁻¹' S)
theorem AddSubsemigroup.toSubsemigroup'_closure {M : Type u_1} [inst : Mul M] (S : Set (Additive M)) :
(RelIso.toRelEmbedding AddSubsemigroup.toSubsemigroup').toEmbedding (AddSubsemigroup.closure S) = Subsemigroup.closure (Multiplicative.ofAdd ⁻¹' S)
@[simp]
theorem AddSubsemigroup.toSubsemigroup_symm_apply_coe {A : Type u_1} [inst : Add A] (S : Subsemigroup (Multiplicative A)) :
↑((RelIso.toRelEmbedding (RelIso.symm AddSubsemigroup.toSubsemigroup)).toEmbedding S) = Multiplicative.ofAdd ⁻¹' S
@[simp]
theorem AddSubsemigroup.toSubsemigroup_apply_coe {A : Type u_1} [inst : Add A] (S : AddSubsemigroup A) :
↑((RelIso.toRelEmbedding AddSubsemigroup.toSubsemigroup).toEmbedding S) = Multiplicative.toAdd ⁻¹' S

Additive subsemigroups of an additive semigroup A are isomorphic to multiplicative subsemigroups of Multiplicative A.

Equations
  • One or more equations did not get rendered due to their size.
@[inline]

Subsemigroups of a semigroup Multiplicative A are isomorphic to additive subsemigroups of A.

Equations
  • Subsemigroup.toAddSubsemigroup' = OrderIso.symm AddSubsemigroup.toSubsemigroup
theorem AddSubsemigroup.toSubsemigroup_closure {A : Type u_1} [inst : Add A] (S : Set A) :
(RelIso.toRelEmbedding AddSubsemigroup.toSubsemigroup).toEmbedding (AddSubsemigroup.closure S) = Subsemigroup.closure (Multiplicative.toAdd ⁻¹' S)
theorem Subsemigroup.toAddSubsemigroup'_closure {A : Type u_1} [inst : Add A] (S : Set (Multiplicative A)) :
(RelIso.toRelEmbedding Subsemigroup.toAddSubsemigroup').toEmbedding (Subsemigroup.closure S) = AddSubsemigroup.closure (Additive.ofMul ⁻¹' S)

comap and map #

def AddSubsemigroup.comap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (S : AddSubsemigroup N) :

The preimage of an AddSubsemigroup along an AddSemigroup homomorphism is an AddSubsemigroup.

Equations
def AddSubsemigroup.comap.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (S : AddSubsemigroup N) :
∀ {a b : M}, a f ⁻¹' Sb f ⁻¹' Sf (a + b) S
Equations
  • (_ : f (a + b) S) = (_ : f (a + b) S)
def Subsemigroup.comap {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (S : Subsemigroup N) :

The preimage of a subsemigroup along a semigroup homomorphism is a subsemigroup.

Equations
@[simp]
theorem AddSubsemigroup.coe_comap {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (S : AddSubsemigroup N) (f : AddHom M N) :
↑(AddSubsemigroup.comap f S) = f ⁻¹' S
@[simp]
theorem Subsemigroup.coe_comap {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] (S : Subsemigroup N) (f : M →ₙ* N) :
↑(Subsemigroup.comap f S) = f ⁻¹' S
@[simp]
theorem AddSubsemigroup.mem_comap {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {S : AddSubsemigroup N} {f : AddHom M N} {x : M} :
@[simp]
theorem Subsemigroup.mem_comap {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {S : Subsemigroup N} {f : M →ₙ* N} {x : M} :
x Subsemigroup.comap f S f x S
theorem AddSubsemigroup.comap_comap {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : Add M] [inst : Add N] [inst : Add P] (S : AddSubsemigroup P) (g : AddHom N P) (f : AddHom M N) :
theorem Subsemigroup.comap_comap {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : Mul M] [inst : Mul N] [inst : Mul P] (S : Subsemigroup P) (g : N →ₙ* P) (f : M →ₙ* N) :
@[simp]
theorem AddSubsemigroup.comap_id {P : Type u_1} [inst : Add P] (S : AddSubsemigroup P) :
@[simp]
theorem Subsemigroup.comap_id {P : Type u_1} [inst : Mul P] (S : Subsemigroup P) :
def AddSubsemigroup.map {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (S : AddSubsemigroup M) :

The image of an AddSubsemigroup along an AddSemigroup homomorphism is an AddSubsemigroup.

Equations
def AddSubsemigroup.map.proof_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (f : AddHom M N) (S : AddSubsemigroup M) :
∀ {a b : N}, a f '' Sb f '' Sa + b f '' S
Equations
def Subsemigroup.map {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (S : Subsemigroup M) :

The image of a subsemigroup along a semigroup homomorphism is a subsemigroup.

Equations
@[simp]
theorem AddSubsemigroup.coe_map {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (S : AddSubsemigroup M) :
↑(AddSubsemigroup.map f S) = f '' S
@[simp]
theorem Subsemigroup.coe_map {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (S : Subsemigroup M) :
↑(Subsemigroup.map f S) = f '' S
@[simp]
theorem AddSubsemigroup.mem_map {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} {S : AddSubsemigroup M} {y : N} :
y AddSubsemigroup.map f S x, x S f x = y
@[simp]
theorem Subsemigroup.mem_map {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} {S : Subsemigroup M} {y : N} :
y Subsemigroup.map f S x, x S f x = y
theorem AddSubsemigroup.mem_map_of_mem {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) {S : AddSubsemigroup M} {x : M} (hx : x S) :
theorem Subsemigroup.mem_map_of_mem {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) {S : Subsemigroup M} {x : M} (hx : x S) :
theorem AddSubsemigroup.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (S : AddSubsemigroup M) (x : { x // x S }) :
f x AddSubsemigroup.map f S
theorem Subsemigroup.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (S : Subsemigroup M) (x : { x // x S }) :
f x Subsemigroup.map f S
theorem AddSubsemigroup.map_map {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : Add M] [inst : Add N] [inst : Add P] (S : AddSubsemigroup M) (g : AddHom N P) (f : AddHom M N) :
theorem Subsemigroup.map_map {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : Mul M] [inst : Mul N] [inst : Mul P] (S : Subsemigroup M) (g : N →ₙ* P) (f : M →ₙ* N) :
theorem AddSubsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective f) {S : AddSubsemigroup M} {x : M} :
theorem Subsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Injective f) {S : Subsemigroup M} {x : M} :
f x Subsemigroup.map f S x S
theorem AddSubsemigroup.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} {S : AddSubsemigroup M} {T : AddSubsemigroup N} :
theorem Subsemigroup.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} {S : Subsemigroup M} {T : Subsemigroup N} :
theorem AddSubsemigroup.gc_map_comap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :
theorem Subsemigroup.gc_map_comap {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) :
theorem AddSubsemigroup.map_le_of_le_comap {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) {T : AddSubsemigroup N} {f : AddHom M N} :
theorem Subsemigroup.map_le_of_le_comap {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] (S : Subsemigroup M) {T : Subsemigroup N} {f : M →ₙ* N} :
theorem AddSubsemigroup.le_comap_of_map_le {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) {T : AddSubsemigroup N} {f : AddHom M N} :
theorem Subsemigroup.le_comap_of_map_le {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] (S : Subsemigroup M) {T : Subsemigroup N} {f : M →ₙ* N} :
theorem AddSubsemigroup.le_comap_map {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) {f : AddHom M N} :
theorem Subsemigroup.le_comap_map {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (S : Subsemigroup M) {f : M →ₙ* N} :
theorem AddSubsemigroup.map_comap_le {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {S : AddSubsemigroup N} {f : AddHom M N} :
theorem Subsemigroup.map_comap_le {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {S : Subsemigroup N} {f : M →ₙ* N} :
theorem AddSubsemigroup.monotone_map {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} :
theorem Subsemigroup.monotone_map {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} :
theorem AddSubsemigroup.monotone_comap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} :
theorem Subsemigroup.monotone_comap {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} :
@[simp]
theorem AddSubsemigroup.map_comap_map {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) {f : AddHom M N} :
@[simp]
theorem Subsemigroup.map_comap_map {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (S : Subsemigroup M) {f : M →ₙ* N} :
@[simp]
theorem Subsemigroup.comap_map_comap {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {S : Subsemigroup N} {f : M →ₙ* N} :
theorem AddSubsemigroup.map_sup {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) (T : AddSubsemigroup M) (f : AddHom M N) :
theorem Subsemigroup.map_sup {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (S : Subsemigroup M) (T : Subsemigroup M) (f : M →ₙ* N) :
theorem AddSubsemigroup.map_supᵢ {M : Type u_2} {N : Type u_3} [inst : Add M] [inst : Add N] {ι : Sort u_1} (f : AddHom M N) (s : ιAddSubsemigroup M) :
theorem Subsemigroup.map_supᵢ {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst : Mul N] {ι : Sort u_1} (f : M →ₙ* N) (s : ιSubsemigroup M) :
theorem AddSubsemigroup.comap_inf {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (S : AddSubsemigroup N) (T : AddSubsemigroup N) (f : AddHom M N) :
theorem Subsemigroup.comap_inf {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] (S : Subsemigroup N) (T : Subsemigroup N) (f : M →ₙ* N) :
theorem AddSubsemigroup.comap_infᵢ {M : Type u_2} {N : Type u_3} [inst : Add M] [inst : Add N] {ι : Sort u_1} (f : AddHom M N) (s : ιAddSubsemigroup N) :
theorem Subsemigroup.comap_infᵢ {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst : Mul N] {ι : Sort u_1} (f : M →ₙ* N) (s : ιSubsemigroup N) :
@[simp]
theorem AddSubsemigroup.map_bot {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :
@[simp]
theorem Subsemigroup.map_bot {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) :
@[simp]
theorem AddSubsemigroup.comap_top {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :
@[simp]
theorem Subsemigroup.comap_top {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) :
abbrev AddSubsemigroup.map_id.match_1 {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M) :
(x : M) → ∀ (motive : x AddSubsemigroup.map (AddHom.id M) SProp) (x_1 : x AddSubsemigroup.map (AddHom.id M) S), (∀ (h : x S), motive (_ : a, a S ↑(AddHom.id M) a = x)) → motive x_1
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubsemigroup.map_id {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M) :
@[simp]
theorem Subsemigroup.map_id {M : Type u_1} [inst : Mul M] (S : Subsemigroup M) :
def AddSubsemigroup.gciMapComap.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective f) (S : AddSubsemigroup M) (x : M) :
Equations
def AddSubsemigroup.gciMapComap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective f) :

map f and comap f form a GaloisCoinsertion when f is injective.

Equations
  • One or more equations did not get rendered due to their size.
def Subsemigroup.gciMapComap {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Injective f) :

map f and comap f form a GaloisCoinsertion when f is injective.

Equations
  • One or more equations did not get rendered due to their size.
theorem AddSubsemigroup.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective f) (S : AddSubsemigroup M) :
theorem Subsemigroup.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Injective f) (S : Subsemigroup M) :
theorem Subsemigroup.comap_surjective_of_injective {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Injective f) :
theorem AddSubsemigroup.map_injective_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective f) :
theorem Subsemigroup.map_injective_of_injective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Injective f) :
theorem Subsemigroup.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Injective f) (S : Subsemigroup M) (T : Subsemigroup M) :
theorem AddSubsemigroup.comap_infᵢ_map_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {ι : Type u_3} {f : AddHom M N} (hf : Function.Injective f) (S : ιAddSubsemigroup M) :
theorem Subsemigroup.comap_infᵢ_map_of_injective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {ι : Type u_3} {f : M →ₙ* N} (hf : Function.Injective f) (S : ιSubsemigroup M) :
theorem Subsemigroup.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Injective f) (S : Subsemigroup M) (T : Subsemigroup M) :
theorem AddSubsemigroup.comap_supᵢ_map_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {ι : Type u_3} {f : AddHom M N} (hf : Function.Injective f) (S : ιAddSubsemigroup M) :
theorem Subsemigroup.comap_supᵢ_map_of_injective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {ι : Type u_3} {f : M →ₙ* N} (hf : Function.Injective f) (S : ιSubsemigroup M) :
theorem AddSubsemigroup.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective f) {S : AddSubsemigroup M} {T : AddSubsemigroup M} :
theorem Subsemigroup.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Injective f) {S : Subsemigroup M} {T : Subsemigroup M} :
theorem AddSubsemigroup.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective f) :
theorem Subsemigroup.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Injective f) :
abbrev AddSubsemigroup.giMapComap.match_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (x : N) (motive : (a, f a = x) → Prop) :
(x : a, f a = x) → ((y : M) → (hy : f y = x) → motive (_ : a, f a = x)) → motive x
Equations
def AddSubsemigroup.giMapComap.proof_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Surjective f) (S : AddSubsemigroup N) (x : N) (h : x S) :
Equations
def AddSubsemigroup.giMapComap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Surjective f) :

map f and comap f form a GaloisInsertion when f is surjective.

Equations
  • One or more equations did not get rendered due to their size.
def Subsemigroup.giMapComap {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Surjective f) :

map f and comap f form a GaloisInsertion when f is surjective.

Equations
  • One or more equations did not get rendered due to their size.
theorem AddSubsemigroup.map_comap_eq_of_surjective {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Surjective f) (S : AddSubsemigroup N) :
theorem Subsemigroup.map_comap_eq_of_surjective {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Surjective f) (S : Subsemigroup N) :
theorem Subsemigroup.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Surjective f) :
theorem Subsemigroup.comap_injective_of_surjective {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Surjective f) :
theorem Subsemigroup.map_inf_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Surjective f) (S : Subsemigroup N) (T : Subsemigroup N) :
theorem AddSubsemigroup.map_infᵢ_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {ι : Type u_3} {f : AddHom M N} (hf : Function.Surjective f) (S : ιAddSubsemigroup N) :
theorem Subsemigroup.map_infᵢ_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {ι : Type u_3} {f : M →ₙ* N} (hf : Function.Surjective f) (S : ιSubsemigroup N) :
theorem Subsemigroup.map_sup_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Surjective f) (S : Subsemigroup N) (T : Subsemigroup N) :
theorem AddSubsemigroup.map_supᵢ_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {ι : Type u_3} {f : AddHom M N} (hf : Function.Surjective f) (S : ιAddSubsemigroup N) :
theorem Subsemigroup.map_supᵢ_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {ι : Type u_3} {f : M →ₙ* N} (hf : Function.Surjective f) (S : ιSubsemigroup N) :
theorem Subsemigroup.comap_le_comap_iff_of_surjective {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Surjective f) {S : Subsemigroup N} {T : Subsemigroup N} :
theorem AddSubsemigroup.comap_strictMono_of_surjective {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Surjective f) :
theorem Subsemigroup.comap_strictMono_of_surjective {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} (hf : Function.Surjective f) :
instance AddMemClass.add {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) :
Add { x // x S' }

An additive submagma of an additive magma inherits an addition.

Equations
def AddMemClass.add.proof_1 {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) (a : { x // x S' }) (b : { x // x S' }) :
a + b S'
Equations
  • (_ : a + b S') = (_ : a + b S')
instance MulMemClass.mul {M : Type u_1} {A : Type u_2} [inst : Mul M] [inst : SetLike A M] [hA : MulMemClass A M] (S' : A) :
Mul { x // x S' }

A submagma of a magma inherits a multiplication.

Equations
@[simp]
theorem AddMemClass.coe_add {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) (x : { x // x S' }) (y : { x // x S' }) :
↑(x + y) = x + y
@[simp]
theorem MulMemClass.coe_mul {M : Type u_1} {A : Type u_2} [inst : Mul M] [inst : SetLike A M] [hA : MulMemClass A M] (S' : A) (x : { x // x S' }) (y : { x // x S' }) :
↑(x * y) = x * y
@[simp]
theorem AddMemClass.mk_add_mk {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) (x : M) (y : M) (hx : x S') (hy : y S') :
{ val := x, property := hx } + { val := y, property := hy } = { val := x + y, property := (_ : x + y S') }
@[simp]
theorem MulMemClass.mk_mul_mk {M : Type u_1} {A : Type u_2} [inst : Mul M] [inst : SetLike A M] [hA : MulMemClass A M] (S' : A) (x : M) (y : M) (hx : x S') (hy : y S') :
{ val := x, property := hx } * { val := y, property := hy } = { val := x * y, property := (_ : x * y S') }
theorem AddMemClass.add_def {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) (x : { x // x S' }) (y : { x // x S' }) :
x + y = { val := x + y, property := (_ : x + y S') }
theorem MulMemClass.mul_def {M : Type u_1} {A : Type u_2} [inst : Mul M] [inst : SetLike A M] [hA : MulMemClass A M] (S' : A) (x : { x // x S' }) (y : { x // x S' }) :
x * y = { val := x * y, property := (_ : x * y S') }
def AddMemClass.toAddSemigroup.proof_2 {M : Type u_1} [inst : AddSemigroup M] {A : Type u_2} [inst : SetLike A M] [inst : AddMemClass A M] (S : A) :
∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
Equations
  • (_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))
def AddMemClass.toAddSemigroup.proof_1 {M : Type u_1} {A : Type u_2} [inst : SetLike A M] (S : A) :
Function.Injective fun a => a
Equations
instance AddMemClass.toAddSemigroup {M : Type u_1} [inst : AddSemigroup M] {A : Type u_2} [inst : SetLike A M] [inst : AddMemClass A M] (S : A) :
AddSemigroup { x // x S }

An AddSubsemigroup of an AddSemigroup inherits an AddSemigroup structure.

Equations
instance MulMemClass.toSemigroup {M : Type u_1} [inst : Semigroup M] {A : Type u_2} [inst : SetLike A M] [inst : MulMemClass A M] (S : A) :
Semigroup { x // x S }

A subsemigroup of a semigroup inherits a semigroup structure.

Equations
def AddMemClass.toAddCommSemigroup.proof_1 {M : Type u_1} {A : Type u_2} [inst : SetLike A M] (S : A) :
Function.Injective fun a => a
Equations
instance AddMemClass.toAddCommSemigroup {M : Type u_1} [inst : AddCommSemigroup M] {A : Type u_2} [inst : SetLike A M] [inst : AddMemClass A M] (S : A) :
AddCommSemigroup { x // x S }

An AddSubsemigroup of an AddCommSemigroup is an AddCommSemigroup.

Equations
def AddMemClass.toAddCommSemigroup.proof_2 {M : Type u_1} [inst : AddCommSemigroup M] {A : Type u_2} [inst : SetLike A M] [inst : AddMemClass A M] (S : A) :
∀ (x x_1 : { x // x S }), ↑(x + x_1) = ↑(x + x_1)
Equations
  • (_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))
instance MulMemClass.toCommSemigroup {M : Type u_1} [inst : CommSemigroup M] {A : Type u_2} [inst : SetLike A M] [inst : MulMemClass A M] (S : A) :
CommSemigroup { x // x S }

A subsemigroup of a CommSemigroup is a CommSemigroup.

Equations
def AddMemClass.subtype.proof_1 {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) :
∀ (x x_1 : { x // x S' }), ↑(x + x_1) = ↑(x + x_1)
Equations
  • (_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))
def AddMemClass.subtype {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) :
AddHom { x // x S' } M

The natural semigroup hom from an AddSubsemigroup of AddSubsemigroup M to M.

Equations
def MulMemClass.subtype {M : Type u_1} {A : Type u_2} [inst : Mul M] [inst : SetLike A M] [hA : MulMemClass A M] (S' : A) :
{ x // x S' } →ₙ* M

The natural semigroup hom from a subsemigroup of semigroup M to M.

Equations
@[simp]
theorem AddMemClass.coe_subtype {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) :
↑(AddMemClass.subtype S') = Subtype.val
@[simp]
theorem MulMemClass.coe_subtype {M : Type u_1} {A : Type u_2} [inst : Mul M] [inst : SetLike A M] [hA : MulMemClass A M] (S' : A) :
↑(MulMemClass.subtype S') = Subtype.val
def AddSubsemigroup.topEquiv.proof_1 {M : Type u_1} [inst : Add M] (x : { x // x }) :
{ val := x, property := (_ : (fun x => x) x ) } = x
Equations
  • (_ : { val := x, property := (_ : (fun x => x) x ) } = x) = (_ : { val := x, property := (_ : (fun x => x) x ) } = x)
def AddSubsemigroup.topEquiv.proof_3 {M : Type u_1} [inst : Add M] :
∀ (x x_1 : { x // x }), Equiv.toFun { toFun := fun x => x, invFun := fun x => { val := x, property := (_ : x ) }, left_inv := (_ : ∀ (x : { x // x }), { val := x, property := (_ : (fun x => x) x ) } = x), right_inv := (_ : ∀ (x : M), (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x) = (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x)) } (x + x_1) = Equiv.toFun { toFun := fun x => x, invFun := fun x => { val := x, property := (_ : x ) }, left_inv := (_ : ∀ (x : { x // x }), { val := x, property := (_ : (fun x => x) x ) } = x), right_inv := (_ : ∀ (x : M), (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x) = (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x)) } (x + x_1)
Equations
  • One or more equations did not get rendered due to their size.
def AddSubsemigroup.topEquiv.proof_2 {M : Type u_1} [inst : Add M] :
∀ (x : M), (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x) = (fun x => x) ((fun x => { val := x, property := (_ : x ) }) x)
Equations
  • One or more equations did not get rendered due to their size.
def AddSubsemigroup.topEquiv {M : Type u_1} [inst : Add M] :
{ x // x } ≃+ M

The top additive subsemigroup is isomorphic to the additive semigroup.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubsemigroup.topEquiv_apply {M : Type u_1} [inst : Add M] (x : { x // x }) :
AddSubsemigroup.topEquiv x = x
@[simp]
theorem Subsemigroup.topEquiv_apply {M : Type u_1} [inst : Mul M] (x : { x // x }) :
Subsemigroup.topEquiv x = x
@[simp]
theorem AddSubsemigroup.topEquiv_symm_apply_coe {M : Type u_1} [inst : Add M] (x : M) :
↑(↑(AddEquiv.symm AddSubsemigroup.topEquiv) x) = x
@[simp]
theorem Subsemigroup.topEquiv_symm_apply_coe {M : Type u_1} [inst : Mul M] (x : M) :
↑(↑(MulEquiv.symm Subsemigroup.topEquiv) x) = x
def Subsemigroup.topEquiv {M : Type u_1} [inst : Mul M] :
{ x // x } ≃* M

The top subsemigroup is isomorphic to the semigroup.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubsemigroup.topEquiv_toAddHom {M : Type u_1} [inst : Add M] :
AddEquiv.toAddHom AddSubsemigroup.topEquiv = AddMemClass.subtype
@[simp]
theorem Subsemigroup.topEquiv_toMulHom {M : Type u_1} [inst : Mul M] :
def AddSubsemigroup.equivMapOfInjective.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective f) :
Function.LeftInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun
Equations
  • One or more equations did not get rendered due to their size.
def AddSubsemigroup.equivMapOfInjective.proof_3 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective f) :
∀ (x x_1 : { x // x S }), Equiv.toFun { toFun := (Equiv.Set.image (f) (S) hf).toFun, invFun := (Equiv.Set.image (f) (S) hf).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.Set.image (f) (S) hf).toFun, invFun := (Equiv.Set.image (f) (S) hf).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun) } x + Equiv.toFun { toFun := (Equiv.Set.image (f) (S) hf).toFun, invFun := (Equiv.Set.image (f) (S) hf).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun) } x_1
Equations
  • One or more equations did not get rendered due to their size.
noncomputable def AddSubsemigroup.equivMapOfInjective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective f) :
{ x // x S } ≃+ { x // x AddSubsemigroup.map f S }

An additive subsemigroup is isomorphic to its image under an injective function

Equations
  • One or more equations did not get rendered due to their size.
def AddSubsemigroup.equivMapOfInjective.proof_2 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective f) :
Function.RightInverse (Equiv.Set.image (f) (S) hf).invFun (Equiv.Set.image (f) (S) hf).toFun
Equations
  • One or more equations did not get rendered due to their size.
noncomputable def Subsemigroup.equivMapOfInjective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (S : Subsemigroup M) (f : M →ₙ* N) (hf : Function.Injective f) :
{ x // x S } ≃* { x // x Subsemigroup.map f S }

A subsemigroup is isomorphic to its image under an injective function

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubsemigroup.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective f) (x : { x // x S }) :
↑(↑(AddSubsemigroup.equivMapOfInjective S f hf) x) = f x
@[simp]
theorem Subsemigroup.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (S : Subsemigroup M) (f : M →ₙ* N) (hf : Function.Injective f) (x : { x // x S }) :
↑(↑(Subsemigroup.equivMapOfInjective S f hf) x) = f x
@[simp]
theorem AddSubsemigroup.closure_closure_coe_preimage {M : Type u_1} [inst : Add M] {s : Set M} :
@[simp]
theorem Subsemigroup.closure_closure_coe_preimage {M : Type u_1} [inst : Mul M] {s : Set M} :
def AddSubsemigroup.prod {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :

Given AddSubsemigroups s, t of AddSemigroups A, B respectively, s × t× t as an AddSubsemigroup of A × B× B.

Equations
def AddSubsemigroup.prod.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
∀ {a b : M × N}, a s ×ˢ tb s ×ˢ t(a + b).fst s (a + b).snd t
Equations
def Subsemigroup.prod {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (s : Subsemigroup M) (t : Subsemigroup N) :

Given Subsemigroups s, t of semigroups M, N respectively, s × t× t as a subsemigroup of M × N× N.

Equations
theorem AddSubsemigroup.coe_prod {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
↑(AddSubsemigroup.prod s t) = s ×ˢ t
theorem Subsemigroup.coe_prod {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (s : Subsemigroup M) (t : Subsemigroup N) :
↑(Subsemigroup.prod s t) = s ×ˢ t
theorem AddSubsemigroup.mem_prod {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {s : AddSubsemigroup M} {t : AddSubsemigroup N} {p : M × N} :
p AddSubsemigroup.prod s t p.fst s p.snd t
theorem Subsemigroup.mem_prod {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {s : Subsemigroup M} {t : Subsemigroup N} {p : M × N} :
p Subsemigroup.prod s t p.fst s p.snd t
theorem AddSubsemigroup.prod_mono {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {s₁ : AddSubsemigroup M} {s₂ : AddSubsemigroup M} {t₁ : AddSubsemigroup N} {t₂ : AddSubsemigroup N} (hs : s₁ s₂) (ht : t₁ t₂) :
theorem Subsemigroup.prod_mono {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {s₁ : Subsemigroup M} {s₂ : Subsemigroup M} {t₁ : Subsemigroup N} {t₂ : Subsemigroup N} (hs : s₁ s₂) (ht : t₁ t₂) :
theorem AddSubsemigroup.prod_top {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (s : AddSubsemigroup M) :
theorem Subsemigroup.prod_top {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (s : Subsemigroup M) :
theorem AddSubsemigroup.top_prod {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (s : AddSubsemigroup N) :
theorem Subsemigroup.top_prod {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] (s : Subsemigroup N) :
@[simp]
theorem AddSubsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] :
@[simp]
theorem Subsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] :
theorem AddSubsemigroup.bot_prod_bot {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] :
theorem Subsemigroup.bot_prod_bot {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] :
def AddSubsemigroup.prodEquiv.proof_3 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
Function.RightInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun
Equations
def AddSubsemigroup.prodEquiv.proof_2 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
Function.LeftInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun
Equations
def AddSubsemigroup.prodEquiv.proof_4 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
∀ (x x_1 : { x // x AddSubsemigroup.prod s t }), Equiv.toFun { toFun := (Equiv.Set.prod s t).toFun, invFun := (Equiv.Set.prod s t).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.Set.prod s t).toFun, invFun := (Equiv.Set.prod s t).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.prod s t).invFun (Equiv.Set.prod s t).toFun) } (x + x_1)
Equations
  • One or more equations did not get rendered due to their size.
def AddSubsemigroup.prodEquiv {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
{ x // x AddSubsemigroup.prod s t } ≃+ { x // x s } × { x // x t }

The product of additive subsemigroups is isomorphic to their product as additive semigroups

Equations
  • One or more equations did not get rendered due to their size.
def AddSubsemigroup.prodEquiv.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] :
Equations
def Subsemigroup.prodEquiv {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (s : Subsemigroup M) (t : Subsemigroup N) :
{ x // x Subsemigroup.prod s t } ≃* { x // x s } × { x // x t }

The product of subsemigroups is isomorphic to their product as semigroups.

Equations
  • One or more equations did not get rendered due to their size.
theorem AddSubsemigroup.mem_map_equiv {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : M ≃+ N} {K : AddSubsemigroup M} {x : N} :
theorem Subsemigroup.mem_map_equiv {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M ≃* N} {K : Subsemigroup M} {x : N} :
@[simp]
theorem AddSubsemigroup.map_equiv_top {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : M ≃+ N) :
@[simp]
theorem Subsemigroup.map_equiv_top {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M ≃* N) :
theorem Subsemigroup.le_prod_iff {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {s : Subsemigroup M} {t : Subsemigroup N} {u : Subsemigroup (M × N)} :
def AddHom.srange {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :

The range of an AddHom is an AddSubsemigroup.

Equations
def AddHom.srange.proof_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (f : AddHom M N) :
Set.range f = f '' Set.univ
Equations
def MulHom.srange {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) :

The range of a semigroup homomorphism is a subsemigroup. See Note [range copy pattern].

Equations
@[simp]
theorem AddHom.coe_srange {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :
@[simp]
theorem MulHom.coe_srange {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) :
@[simp]
theorem AddHom.mem_srange {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} {y : N} :
y AddHom.srange f x, f x = y
@[simp]
theorem MulHom.mem_srange {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} {y : N} :
y MulHom.srange f x, f x = y
theorem AddHom.srange_eq_map {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :
theorem MulHom.srange_eq_map {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) :
theorem AddHom.map_srange {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : Add M] [inst : Add N] [inst : Add P] (g : AddHom N P) (f : AddHom M N) :
theorem MulHom.map_srange {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : Mul M] [inst : Mul N] [inst : Mul P] (g : N →ₙ* P) (f : M →ₙ* N) :
theorem AddHom.srange_top_iff_surjective {M : Type u_2} [inst : Add M] {N : Type u_1} [inst : Add N] {f : AddHom M N} :
theorem MulHom.srange_top_iff_surjective {M : Type u_2} [inst : Mul M] {N : Type u_1} [inst : Mul N] {f : M →ₙ* N} :
theorem AddHom.srange_top_of_surjective {M : Type u_2} [inst : Add M] {N : Type u_1} [inst : Add N] (f : AddHom M N) (hf : Function.Surjective f) :

The range of a surjective add_semigroup hom is the whole of the codomain.

theorem MulHom.srange_top_of_surjective {M : Type u_2} [inst : Mul M] {N : Type u_1} [inst : Mul N] (f : M →ₙ* N) (hf : Function.Surjective f) :

The range of a surjective semigroup hom is the whole of the codomain.

theorem AddHom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (s : Set N) :
theorem MulHom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (s : Set N) :
theorem AddHom.map_mclosure {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (s : Set M) :

The image under an AddSemigroup hom of the AddSubsemigroup generated by a set equals the AddSubsemigroup generated by the image of the set.

theorem MulHom.map_mclosure {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (s : Set M) :

The image under a semigroup hom of the subsemigroup generated by a set equals the subsemigroup generated by the image of the set.

def AddHom.restrict {M : Type u_1} {σ : Type u_2} [inst : Add M] {N : Type u_3} [inst : Add N] [inst : SetLike σ M] [inst : AddMemClass σ M] (f : AddHom M N) (S : σ) :
AddHom { x // x S } N

Restriction of an AddSemigroup hom to an AddSubsemigroup of the domain.

Equations
def MulHom.restrict {M : Type u_1} {σ : Type u_2} [inst : Mul M] {N : Type u_3} [inst : Mul N] [inst : SetLike σ M] [inst : MulMemClass σ M] (f : M →ₙ* N) (S : σ) :
{ x // x S } →ₙ* N

Restriction of a semigroup hom to a subsemigroup of the domain.

Equations
@[simp]
theorem AddHom.restrict_apply {M : Type u_3} {σ : Type u_2} [inst : Add M] {N : Type u_1} [inst : Add N] [inst : SetLike σ M] [inst : AddMemClass σ M] (f : AddHom M N) {S : σ} (x : { x // x S }) :
↑(AddHom.restrict f S) x = f x
@[simp]
theorem MulHom.restrict_apply {M : Type u_3} {σ : Type u_2} [inst : Mul M] {N : Type u_1} [inst : Mul N] [inst : SetLike σ M] [inst : MulMemClass σ M] (f : M →ₙ* N) {S : σ} (x : { x // x S }) :
↑(MulHom.restrict f S) x = f x
def AddHom.codRestrict {M : Type u_1} {N : Type u_2} {σ : Type u_3} [inst : Add M] [inst : Add N] [inst : SetLike σ N] [inst : AddMemClass σ N] (f : AddHom M N) (S : σ) (h : ∀ (x : M), f x S) :
AddHom M { x // x S }

Restriction of an AddSemigroup hom to an AddSubsemigroup of the codomain.

Equations
  • One or more equations did not get rendered due to their size.
def AddHom.codRestrict.proof_1 {M : Type u_3} {N : Type u_1} {σ : Type u_2} [inst : Add M] [inst : Add N] [inst : SetLike σ N] [inst : AddMemClass σ N] (f : AddHom M N) (S : σ) (h : ∀ (x : M), f x S) (x : M) (y : M) :
(fun n => { val := f n, property := h n }) (x + y) = (fun n => { val := f n, property := h n }) x + (fun n => { val := f n, property := h n }) y
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddHom.codRestrict_apply_coe {M : Type u_1} {N : Type u_2} {σ : Type u_3} [inst : Add M] [inst : Add N] [inst : SetLike σ N] [inst : AddMemClass σ N] (f : AddHom M N) (S : σ) (h : ∀ (x : M), f x S) (n : M) :
↑(↑(AddHom.codRestrict f S h) n) = f n
@[simp]
theorem MulHom.codRestrict_apply_coe {M : Type u_1} {N : Type u_2} {σ : Type u_3} [inst : Mul M] [inst : Mul N] [inst : SetLike σ N] [inst : MulMemClass σ N] (f : M →ₙ* N) (S : σ) (h : ∀ (x : M), f x S) (n : M) :
↑(↑(MulHom.codRestrict f S h) n) = f n
def MulHom.codRestrict {M : Type u_1} {N : Type u_2} {σ : Type u_3} [inst : Mul M] [inst : Mul N] [inst : SetLike σ N] [inst : MulMemClass σ N] (f : M →ₙ* N) (S : σ) (h : ∀ (x : M), f x S) :
M →ₙ* { x // x S }

Restriction of a semigroup hom to a subsemigroup of the codomain.

Equations
  • One or more equations did not get rendered due to their size.
def AddHom.srangeRestrict.proof_1 {M : Type u_1} [inst : Add M] {N : Type u_2} [inst : Add N] (f : AddHom M N) (x : M) :
y, f y = f x
Equations
  • (_ : y, f y = f x) = (_ : y, f y = f x)
def AddHom.srangeRestrict {M : Type u_1} [inst : Add M] {N : Type u_2} [inst : Add N] (f : AddHom M N) :
AddHom M { x // x AddHom.srange f }

Restriction of an AddSemigroup hom to its range interpreted as a subsemigroup.

Equations
def MulHom.srangeRestrict {M : Type u_1} [inst : Mul M] {N : Type u_2} [inst : Mul N] (f : M →ₙ* N) :
M →ₙ* { x // x MulHom.srange f }

Restriction of a semigroup hom to its range interpreted as a subsemigroup.

Equations
@[simp]
theorem AddHom.coe_srangeRestrict {M : Type u_2} [inst : Add M] {N : Type u_1} [inst : Add N] (f : AddHom M N) (x : M) :
↑(↑(AddHom.srangeRestrict f) x) = f x
@[simp]
theorem MulHom.coe_srangeRestrict {M : Type u_2} [inst : Mul M] {N : Type u_1} [inst : Mul N] (f : M →ₙ* N) (x : M) :
↑(↑(MulHom.srangeRestrict f) x) = f x
abbrev AddHom.srangeRestrict_surjective.match_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (f : AddHom M N) (motive : { x // x AddHom.srange f }Prop) :
(x : { x // x AddHom.srange f }) → ((x : M) → motive { val := f x, property := (_ : y, f y = f x) }) → motive x
Equations
  • One or more equations did not get rendered due to their size.
theorem AddHom.srangeRestrict_surjective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :
theorem MulHom.srangeRestrict_surjective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) :
theorem AddHom.prod_map_comap_prod' {M : Type u_3} {N : Type u_4} [inst : Add M] [inst : Add N] {M' : Type u_1} {N' : Type u_2} [inst : Add M'] [inst : Add N'] (f : AddHom M N) (g : AddHom M' N') (S : AddSubsemigroup N) (S' : AddSubsemigroup N') :
theorem MulHom.prod_map_comap_prod' {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst : Mul N] {M' : Type u_1} {N' : Type u_2} [inst : Mul M'] [inst : Mul N'] (f : M →ₙ* N) (g : M' →ₙ* N') (S : Subsemigroup N) (S' : Subsemigroup N') :
def AddHom.subsemigroupComap.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (N' : AddSubsemigroup N) (x : { x // x AddSubsemigroup.comap f N' }) :
Equations
def AddHom.subsemigroupComap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (N' : AddSubsemigroup N) :
AddHom { x // x AddSubsemigroup.comap f N' } { x // x N' }

The AddHom from the preimage of an additive subsemigroup to itself.

Equations
  • One or more equations did not get rendered due to their size.
def AddHom.subsemigroupComap.proof_2 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (N' : AddSubsemigroup N) (x : { x // x AddSubsemigroup.comap f N' }) (y : { x // x AddSubsemigroup.comap f N' }) :
(fun x => { val := f x, property := (_ : x AddSubsemigroup.comap f N') }) (x + y) = (fun x => { val := f x, property := (_ : x AddSubsemigroup.comap f N') }) x + (fun x => { val := f x, property := (_ : x AddSubsemigroup.comap f N') }) y
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem MulHom.subsemigroupComap_apply_coe {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (N' : Subsemigroup N) (x : { x // x Subsemigroup.comap f N' }) :
↑(↑(MulHom.subsemigroupComap f N') x) = f x
@[simp]
theorem AddHom.subsemigroupComap_apply_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (N' : AddSubsemigroup N) (x : { x // x AddSubsemigroup.comap f N' }) :
↑(↑(AddHom.subsemigroupComap f N') x) = f x
def MulHom.subsemigroupComap {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (N' : Subsemigroup N) :
{ x // x Subsemigroup.comap f N' } →ₙ* { x // x N' }

The MulHom from the preimage of a subsemigroup to itself.

Equations
  • One or more equations did not get rendered due to their size.
def AddHom.subsemigroupMap.proof_2 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (M' : AddSubsemigroup M) (x : { x // x M' }) (y : { x // x M' }) :
(fun x => { val := f x, property := (_ : a, a M' f a = f x) }) (x + y) = (fun x => { val := f x, property := (_ : a, a M' f a = f x) }) x + (fun x => { val := f x, property := (_ : a, a M' f a = f x) }) y
Equations
  • One or more equations did not get rendered due to their size.
def AddHom.subsemigroupMap.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (M' : AddSubsemigroup M) (x : { x // x M' }) :
a, a M' f a = f x
Equations
  • (_ : a, a M' f a = f x) = (_ : a, a M' f a = f x)
def AddHom.subsemigroupMap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (M' : AddSubsemigroup M) :
AddHom { x // x M' } { x // x AddSubsemigroup.map f M' }

the AddHom from an additive subsemigroup to its image. See AddEquiv.addSubsemigroupMap for a variant for AddEquivs.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddHom.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (M' : AddSubsemigroup M) (x : { x // x M' }) :
↑(↑(AddHom.subsemigroupMap f M') x) = f x
@[simp]
theorem MulHom.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (M' : Subsemigroup M) (x : { x // x M' }) :
↑(↑(MulHom.subsemigroupMap f M') x) = f x
def MulHom.subsemigroupMap {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (M' : Subsemigroup M) :
{ x // x M' } →ₙ* { x // x Subsemigroup.map f M' }

The MulHom from a subsemigroup to its image. See MulEquiv.subsemigroupMap for a variant for MulEquivs.

Equations
  • One or more equations did not get rendered due to their size.
theorem AddHom.subsemigroupMap_surjective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (M' : AddSubsemigroup M) :
theorem MulHom.subsemigroupMap_surjective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) (M' : Subsemigroup M) :
@[simp]
theorem AddSubsemigroup.srange_fst {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] [inst : Nonempty N] :
@[simp]
theorem Subsemigroup.srange_fst {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] [inst : Nonempty N] :
@[simp]
theorem AddSubsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] [inst : Nonempty M] :
@[simp]
theorem Subsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] [inst : Nonempty M] :
theorem AddSubsemigroup.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] [inst : Nonempty M] [inst : Nonempty N] {s : AddSubsemigroup M} {t : AddSubsemigroup N} :
theorem Subsemigroup.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] [inst : Nonempty M] [inst : Nonempty N] {s : Subsemigroup M} {t : Subsemigroup N} :
def AddSubsemigroup.inclusion.proof_1 {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S T) (x : { x // x S }) :
Equations
def AddSubsemigroup.inclusion {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S T) :
AddHom { x // x S } { x // x T }

The AddSemigroup hom associated to an inclusion of subsemigroups.

Equations
def Subsemigroup.inclusion {M : Type u_1} [inst : Mul M] {S : Subsemigroup M} {T : Subsemigroup M} (h : S T) :
{ x // x S } →ₙ* { x // x T }

The semigroup hom associated to an inclusion of subsemigroups.

Equations
@[simp]
theorem AddSubsemigroup.eq_top_iff' {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M) :
S = ∀ (x : M), x S
theorem Subsemigroup.eq_top_iff' {M : Type u_1} [inst : Mul M] (S : Subsemigroup M) :
S = ∀ (x : M), x S
def AddEquiv.subsemigroupCongr.proof_3 {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
Function.RightInverse (Equiv.setCongr (_ : S = T)).invFun (Equiv.setCongr (_ : S = T)).toFun
Equations
  • One or more equations did not get rendered due to their size.
def AddEquiv.subsemigroupCongr.proof_1 {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
S = T
Equations
  • (_ : S = T) = (_ : S = T)
def AddEquiv.subsemigroupCongr {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
{ x // x S } ≃+ { x // x T }

Makes the identity additive isomorphism from a proof two subsemigroups of an additive semigroup are equal.

Equations
  • One or more equations did not get rendered due to their size.
def AddEquiv.subsemigroupCongr.proof_2 {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
Function.LeftInverse (Equiv.setCongr (_ : S = T)).invFun (Equiv.setCongr (_ : S = T)).toFun
Equations
  • One or more equations did not get rendered due to their size.
def AddEquiv.subsemigroupCongr.proof_4 {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
∀ (x x_1 : { x // x S }), Equiv.toFun { toFun := (Equiv.setCongr (_ : S = T)).toFun, invFun := (Equiv.setCongr (_ : S = T)).invFun, left_inv := (_ : Function.LeftInverse (Equiv.setCongr (_ : S = T)).invFun (Equiv.setCongr (_ : S = T)).toFun), right_inv := (_ : Function.RightInverse (Equiv.setCongr (_ : S = T)).invFun (Equiv.setCongr (_ : S = T)).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.setCongr (_ : S = T)).toFun, invFun := (Equiv.setCongr (_ : S = T)).invFun, left_inv := (_ : Function.LeftInverse (Equiv.setCongr (_ : S = T)).invFun (Equiv.setCongr (_ : S = T)).toFun), right_inv := (_ : Function.RightInverse (Equiv.setCongr (_ : S = T)).invFun (Equiv.setCongr (_ : S = T)).toFun) } (x + x_1)
Equations
  • One or more equations did not get rendered due to their size.
def MulEquiv.subsemigroupCongr {M : Type u_1} [inst : Mul M] {S : Subsemigroup M} {T : Subsemigroup M} (h : S = T) :
{ x // x S } ≃* { x // x T }

Makes the identity isomorphism from a proof that two subsemigroups of a multiplicative semigroup are equal.

Equations
  • One or more equations did not get rendered due to their size.
def AddEquiv.ofLeftInverse.proof_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (f : AddHom M N) {g : NM} (h : Function.LeftInverse g f) (x : { x // x AddHom.srange f }) :
Equations
abbrev AddEquiv.ofLeftInverse.match_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (x : { x // x AddHom.srange f }) (motive : (x, f x = x) → Prop) :
(x : x, f x = x) → ((x' : M) → (hx' : f x' = x) → motive (_ : x, f x = x)) → motive x
Equations
def AddEquiv.ofLeftInverse.proof_2 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (f : AddHom M N) (x : M) (y : M) :
Equations
  • One or more equations did not get rendered due to their size.
def AddEquiv.ofLeftInverse {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) {g : NM} (h : Function.LeftInverse g f) :
M ≃+ { x // x AddHom.srange f }

An additive semigroup homomorphism f : M →+ N→+ N with a left-inverse g : N → M→ M defines an additive equivalence between M and f.srange. This is a bidirectional version of AddHom.srangeRestrict.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem MulEquiv.ofLeftInverse_symm_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) {g : NM} (h : Function.LeftInverse g f) :
∀ (a : { x // x MulHom.srange f }), ↑(MulEquiv.symm (MulEquiv.ofLeftInverse f h)) a = g a
@[simp]
theorem AddEquiv.ofLeftInverse_symm_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) {g : NM} (h : Function.LeftInverse g f) :
∀ (a : { x // x AddHom.srange f }), ↑(AddEquiv.symm (AddEquiv.ofLeftInverse f h)) a = g a
@[simp]
theorem MulEquiv.ofLeftInverse_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) {g : NM} (h : Function.LeftInverse g f) (a : M) :
@[simp]
theorem AddEquiv.ofLeftInverse_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) {g : NM} (h : Function.LeftInverse g f) (a : M) :
def MulEquiv.ofLeftInverse {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (f : M →ₙ* N) {g : NM} (h : Function.LeftInverse g f) :
M ≃* { x // x MulHom.srange f }

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

This is a bidirectional version of MulHom.srangeRestrict.

Equations
  • One or more equations did not get rendered due to their size.
def AddEquiv.subsemigroupMap.proof_4 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (S : AddSubsemigroup M) :
Function.RightInverse (Equiv.image e.toEquiv S).invFun (Equiv.image e.toEquiv S).toFun
Equations
def AddEquiv.subsemigroupMap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (S : AddSubsemigroup M) :
{ x // x S } ≃+ { x // x AddSubsemigroup.map (AddEquiv.toAddHom e) S }

An AddEquiv φ between two additive semigroups M and N induces an AddEquiv between a subsemigroup S ≤ M≤ M and the subsemigroup φ(S) ≤ N≤ N. See AddHom.addSubsemigroupMap for a variant for AddHoms.

Equations
  • One or more equations did not get rendered due to their size.
def AddEquiv.subsemigroupMap.proof_5 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : { x // x S }) (y : { x // x S }) :
Equations
  • One or more equations did not get rendered due to their size.
def AddEquiv.subsemigroupMap.proof_2 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : { x // x AddSubsemigroup.map (AddEquiv.toAddHom e) S }) :
↑(Equiv.invFun (Equiv.image e.toEquiv S) x) S
Equations
def AddEquiv.subsemigroupMap.proof_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : { x // x S }) :
Equations
def AddEquiv.subsemigroupMap.proof_3 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (S : AddSubsemigroup M) :
Function.LeftInverse (Equiv.image e.toEquiv S).invFun (Equiv.image e.toEquiv S).toFun
Equations
@[simp]
theorem AddEquiv.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : { x // x S }) :
↑(↑(AddEquiv.subsemigroupMap e S) x) = e x
@[simp]
theorem MulEquiv.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) (S : Subsemigroup M) (x : { x // x S }) :
↑(↑(MulEquiv.subsemigroupMap e S) x) = e x
@[simp]
theorem MulEquiv.subsemigroupMap_symm_apply_coe {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) (S : Subsemigroup M) (x : { x // x Subsemigroup.map (MulEquiv.toMulHom e) S }) :
@[simp]
theorem AddEquiv.subsemigroupMap_symm_apply_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : { x // x AddSubsemigroup.map (AddEquiv.toAddHom e) S }) :
def MulEquiv.subsemigroupMap {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) (S : Subsemigroup M) :
{ x // x S } ≃* { x // x Subsemigroup.map (MulEquiv.toMulHom e) S }

A MulEquiv φ between two semigroups M and N induces a MulEquiv between a subsemigroup S ≤ M≤ M and the subsemigroup φ(S) ≤ N≤ N. See MulHom.subsemigroupMap for a variant for MulHoms.

Equations
  • One or more equations did not get rendered due to their size.