# Operations on Subsemigroups #

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

## Main definitions #

### Conversion between multiplicative and additive definitions #

• Subsemigroup.toAddSubsemigroup, Subsemigroup.toAddSubsemigroup', AddSubsemigroup.toSubsemigroup, AddSubsemigroup.toSubsemigroup': convert between multiplicative and additive subsemigroups of M, Multiplicative M, and Additive M. These are stated as OrderIsos.

### (Commutative) semigroup structure on a subsemigroup #

• Subsemigroup.toSemigroup, Subsemigroup.toCommSemigroup: a subsemigroup inherits a (commutative) semigroup structure.

### Operations on subsemigroups #

• Subsemigroup.comap: preimage of a subsemigroup under a semigroup homomorphism as a subsemigroup of the domain;
• Subsemigroup.map: image of a subsemigroup under a semigroup homomorphism as a subsemigroup of the codomain;
• Subsemigroup.prod: product of two subsemigroups s : Subsemigroup M and t : Subsemigroup N as a subsemigroup of M × N;

### Semigroup homomorphisms between subsemigroups #

• Subsemigroup.subtype: embedding of a subsemigroup into the ambient semigroup.
• Subsemigroup.inclusion: given two subsemigroups S, T such that S ≤ T, S.inclusion T is the inclusion of S into T as a semigroup homomorphism;
• MulEquiv.subsemigroupCongr: converts a proof of S = T into a semigroup isomorphism between S and T.
• Subsemigroup.prodEquiv: semigroup isomorphism between s.prod t and s × t;

### Operations on MulHoms #

• MulHom.srange: range of a semigroup homomorphism as a subsemigroup of the codomain;
• MulHom.restrict: restrict a semigroup homomorphism to a subsemigroup;
• MulHom.codRestrict: restrict the codomain of a semigroup homomorphism to a subsemigroup;
• MulHom.srangeRestrict: restrict a semigroup homomorphism to its range;

### 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} [Mul M] (S : ) :
@[simp]
theorem Subsemigroup.toAddSubsemigroup_symm_apply_coe {M : Type u_1} [Mul M] (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.
Instances For
@[reducible, inline]

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

Equations
Instances For
theorem Subsemigroup.toAddSubsemigroup_closure {M : Type u_1} [Mul M] (S : Set M) :
theorem AddSubsemigroup.toSubsemigroup'_closure {M : Type u_1} [Mul M] (S : Set ()) :
@[simp]
theorem AddSubsemigroup.toSubsemigroup_apply_coe {A : Type u_5} [Add A] (S : ) :
@[simp]
theorem AddSubsemigroup.toSubsemigroup_symm_apply_coe {A : Type u_5} [Add A] (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.
Instances For
@[reducible, inline]

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

Equations
Instances For
theorem AddSubsemigroup.toSubsemigroup_closure {A : Type u_5} [Add A] (S : Set A) :
theorem Subsemigroup.toAddSubsemigroup'_closure {A : Type u_5} [Add A] (S : ) :

### comap and map#

theorem AddSubsemigroup.comap.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : ) :
∀ {a b : M}, a f ⁻¹' Sb f ⁻¹' Sf (a + b) S
def AddSubsemigroup.comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : ) :

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

Equations
• = { carrier := f ⁻¹' S, add_mem' := }
Instances For
def Subsemigroup.comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : ) :

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

Equations
• = { carrier := f ⁻¹' S, mul_mem' := }
Instances For
@[simp]
theorem AddSubsemigroup.coe_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : ) (f : AddHom M N) :
() = f ⁻¹' S
@[simp]
theorem Subsemigroup.coe_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : ) (f : M →ₙ* N) :
() = f ⁻¹' S
@[simp]
theorem AddSubsemigroup.mem_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {S : } {f : AddHom M N} {x : M} :
f x S
@[simp]
theorem Subsemigroup.mem_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {S : } {f : M →ₙ* N} {x : M} :
x f x S
theorem AddSubsemigroup.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [Add P] (S : ) (g : AddHom N P) (f : AddHom M N) :
theorem Subsemigroup.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul M] [Mul N] [Mul P] (S : ) (g : N →ₙ* P) (f : M →ₙ* N) :
= Subsemigroup.comap (g.comp f) S
@[simp]
theorem AddSubsemigroup.comap_id {P : Type u_3} [Add P] (S : ) :
= S
@[simp]
theorem Subsemigroup.comap_id {P : Type u_3} [Mul P] (S : ) :
= S
theorem AddSubsemigroup.map.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (S : ) :
∀ {a b : N}, a f '' Sb f '' Sa + b f '' S
def AddSubsemigroup.map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : ) :

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

Equations
• = { carrier := f '' S, add_mem' := }
Instances For
def Subsemigroup.map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : ) :

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

Equations
• = { carrier := f '' S, mul_mem' := }
Instances For
@[simp]
theorem AddSubsemigroup.coe_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : ) :
() = f '' S
@[simp]
theorem Subsemigroup.coe_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : ) :
() = f '' S
@[simp]
theorem AddSubsemigroup.mem_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {S : } {y : N} :
y xS, f x = y
@[simp]
theorem Subsemigroup.mem_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {S : } {y : N} :
y xS, f x = y
theorem AddSubsemigroup.mem_map_of_mem {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) {S : } {x : M} (hx : x S) :
f x
theorem Subsemigroup.mem_map_of_mem {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) {S : } {x : M} (hx : x S) :
f x
theorem AddSubsemigroup.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : ) (x : S) :
f x
theorem Subsemigroup.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : ) (x : S) :
f x
theorem AddSubsemigroup.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [Add P] (S : ) (g : AddHom N P) (f : AddHom M N) :
theorem Subsemigroup.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul M] [Mul N] [Mul P] (S : ) (g : N →ₙ* P) (f : M →ₙ* N) :
= Subsemigroup.map (g.comp f) S
@[simp]
theorem AddSubsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) {S : } {x : M} :
f x x S
@[simp]
theorem Subsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) {S : } {x : M} :
f x x S
theorem AddSubsemigroup.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {S : } {T : } :
T
theorem Subsemigroup.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {S : } {T : } :
T S
theorem Subsemigroup.gc_map_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
theorem AddSubsemigroup.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : ) {T : } {f : AddHom M N} :
T
theorem Subsemigroup.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : ) {T : } {f : M →ₙ* N} :
S T
theorem AddSubsemigroup.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : ) {T : } {f : AddHom M N} :
T
theorem Subsemigroup.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : ) {T : } {f : M →ₙ* N} :
TS
theorem AddSubsemigroup.le_comap_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : ) {f : AddHom M N} :
theorem Subsemigroup.le_comap_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : ) {f : M →ₙ* N} :
S
theorem AddSubsemigroup.map_comap_le {M : Type u_1} {N : Type u_2} [Add M] [Add N] {S : } {f : AddHom M N} :
theorem Subsemigroup.map_comap_le {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {S : } {f : M →ₙ* N} :
S
theorem Subsemigroup.monotone_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} :
theorem Subsemigroup.monotone_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} :
@[simp]
theorem AddSubsemigroup.map_comap_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : ) {f : AddHom M N} :
@[simp]
theorem Subsemigroup.map_comap_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : ) {f : M →ₙ* N} :
=
@[simp]
theorem AddSubsemigroup.comap_map_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {S : } {f : AddHom M N} :
@[simp]
theorem Subsemigroup.comap_map_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {S : } {f : M →ₙ* N} :
=
theorem AddSubsemigroup.map_sup {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : ) (T : ) (f : AddHom M N) :
theorem Subsemigroup.map_sup {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : ) (T : ) (f : M →ₙ* N) :
theorem AddSubsemigroup.map_iSup {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Sort u_5} (f : AddHom M N) (s : ι) :
= ⨆ (i : ι), AddSubsemigroup.map f (s i)
theorem Subsemigroup.map_iSup {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Sort u_5} (f : M →ₙ* N) (s : ι) :
Subsemigroup.map f (iSup s) = ⨆ (i : ι), Subsemigroup.map f (s i)
theorem AddSubsemigroup.comap_inf {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : ) (T : ) (f : AddHom M N) :
theorem Subsemigroup.comap_inf {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : ) (T : ) (f : M →ₙ* N) :
theorem AddSubsemigroup.comap_iInf {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Sort u_5} (f : AddHom M N) (s : ι) :
= ⨅ (i : ι), AddSubsemigroup.comap f (s i)
theorem Subsemigroup.comap_iInf {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Sort u_5} (f : M →ₙ* N) (s : ι) :
= ⨅ (i : ι), Subsemigroup.comap f (s i)
@[simp]
@[simp]
theorem Subsemigroup.map_bot {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
@[simp]
@[simp]
theorem Subsemigroup.comap_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
abbrev AddSubsemigroup.map_id.match_1 {M : Type u_1} [Add M] (S : ) :
∀ (x : M) (motive : x Prop) (x_1 : x ), (∀ (h : x S), motive )motive x_1
Equations
• =
Instances For
@[simp]
theorem AddSubsemigroup.map_id {M : Type u_1} [Add M] (S : ) :
= S
@[simp]
theorem Subsemigroup.map_id {M : Type u_1} [Mul M] (S : ) :
= S
theorem AddSubsemigroup.gciMapComap.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) (S : ) (x : M) :
x S
def AddSubsemigroup.gciMapComap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) :

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

Equations
• = .toGaloisCoinsertion
Instances For
def Subsemigroup.gciMapComap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) :

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

Equations
• = .toGaloisCoinsertion
Instances For
theorem AddSubsemigroup.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) (S : ) :
theorem Subsemigroup.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) (S : ) :
= S
theorem AddSubsemigroup.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) :
theorem Subsemigroup.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) :
theorem AddSubsemigroup.map_injective_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) :
theorem Subsemigroup.map_injective_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) :
theorem AddSubsemigroup.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) (S : ) (T : ) :
= S T
theorem Subsemigroup.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) (S : ) (T : ) :
theorem AddSubsemigroup.comap_iInf_map_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Type u_5} {f : AddHom M N} (hf : ) (S : ι) :
AddSubsemigroup.comap f (⨅ (i : ι), AddSubsemigroup.map f (S i)) = iInf S
theorem Subsemigroup.comap_iInf_map_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : ) (S : ι) :
Subsemigroup.comap f (⨅ (i : ι), Subsemigroup.map f (S i)) = iInf S
theorem AddSubsemigroup.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) (S : ) (T : ) :
= S T
theorem Subsemigroup.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) (S : ) (T : ) :
theorem AddSubsemigroup.comap_iSup_map_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Type u_5} {f : AddHom M N} (hf : ) (S : ι) :
AddSubsemigroup.comap f (⨆ (i : ι), AddSubsemigroup.map f (S i)) = iSup S
theorem Subsemigroup.comap_iSup_map_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : ) (S : ι) :
Subsemigroup.comap f (⨆ (i : ι), Subsemigroup.map f (S i)) = iSup S
theorem AddSubsemigroup.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) {S : } {T : } :
S T
theorem Subsemigroup.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) {S : } {T : } :
S T
theorem AddSubsemigroup.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) :
theorem Subsemigroup.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) :
abbrev AddSubsemigroup.giMapComap.match_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (x : N) (motive : (∃ (a : M), f a = x)Prop) :
∀ (x_1 : ∃ (a : M), f a = x), (∀ (y : M) (hy : f y = x), motive )motive x_1
Equations
• =
Instances For
theorem AddSubsemigroup.giMapComap.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] {f : AddHom M N} (hf : ) (S : ) (x : N) (h : x S) :
def AddSubsemigroup.giMapComap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) :

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

Equations
• = .toGaloisInsertion
Instances For
def Subsemigroup.giMapComap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) :

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

Equations
• = .toGaloisInsertion
Instances For
theorem AddSubsemigroup.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) (S : ) :
theorem Subsemigroup.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) (S : ) :
= S
theorem AddSubsemigroup.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) :
theorem Subsemigroup.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) :
theorem AddSubsemigroup.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) :
theorem Subsemigroup.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) :
theorem AddSubsemigroup.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) (S : ) (T : ) :
= S T
theorem Subsemigroup.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) (S : ) (T : ) :
= S T
theorem AddSubsemigroup.map_iInf_comap_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Type u_5} {f : AddHom M N} (hf : ) (S : ι) :
AddSubsemigroup.map f (⨅ (i : ι), AddSubsemigroup.comap f (S i)) = iInf S
theorem Subsemigroup.map_iInf_comap_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : ) (S : ι) :
Subsemigroup.map f (⨅ (i : ι), Subsemigroup.comap f (S i)) = iInf S
theorem AddSubsemigroup.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) (S : ) (T : ) :
= S T
theorem Subsemigroup.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) (S : ) (T : ) :
= S T
theorem AddSubsemigroup.map_iSup_comap_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Type u_5} {f : AddHom M N} (hf : ) (S : ι) :
AddSubsemigroup.map f (⨆ (i : ι), AddSubsemigroup.comap f (S i)) = iSup S
theorem Subsemigroup.map_iSup_comap_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : ) (S : ι) :
Subsemigroup.map f (⨆ (i : ι), Subsemigroup.comap f (S i)) = iSup S
theorem AddSubsemigroup.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) {S : } {T : } :
S T
theorem Subsemigroup.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) {S : } {T : } :
S T
theorem AddSubsemigroup.comap_strictMono_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : ) :
theorem Subsemigroup.comap_strictMono_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : ) :
@[instance 900]
instance AddMemClass.add {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : ] (S' : A) :

Equations
• = { add := fun (a b : S') => a + b, }
theorem AddMemClass.add.proof_1 {M : Type u_1} {A : Type u_2} [Add M] [SetLike A M] [hA : ] (S' : A) (a : S') (b : S') :
a + b S'
@[instance 900]
instance MulMemClass.mul {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : ] (S' : A) :
Mul S'

A submagma of a magma inherits a multiplication.

Equations
• = { mul := fun (a b : S') => a * b, }
@[simp]
theorem AddMemClass.coe_add {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : ] (S' : A) (x : S') (y : S') :
(x + y) = x + y
@[simp]
theorem MulMemClass.coe_mul {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : ] (S' : A) (x : S') (y : S') :
(x * y) = x * y
@[simp]
theorem AddMemClass.mk_add_mk {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : ] (S' : A) (x : M) (y : M) (hx : x S') (hy : y S') :
x, hx + y, hy = x + y,
@[simp]
theorem MulMemClass.mk_mul_mk {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : ] (S' : A) (x : M) (y : M) (hx : x S') (hy : y S') :
x, hx * y, hy = x * y,
theorem AddMemClass.add_def {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : ] (S' : A) (x : S') (y : S') :
x + y = x + y,
theorem MulMemClass.mul_def {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : ] (S' : A) (x : S') (y : S') :
x * y = x * y,
theorem AddMemClass.toAddSemigroup.proof_2 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] (S : A) :
∀ (x x_1 : S), (x + x_1) = (x + x_1)
theorem AddMemClass.toAddSemigroup.proof_1 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
Function.Injective fun (a : S) => a
instance AddMemClass.toAddSemigroup {M : Type u_6} [] {A : Type u_7} [SetLike A M] [] (S : A) :

An AddSubsemigroup of an AddSemigroup inherits an AddSemigroup structure.

Equations
instance MulMemClass.toSemigroup {M : Type u_6} [] {A : Type u_7} [SetLike A M] [] (S : A) :

A subsemigroup of a semigroup inherits a semigroup structure.

Equations
instance AddMemClass.toAddCommSemigroup {M : Type u_7} [] {A : Type u_6} [SetLike A M] [] (S : A) :

An AddSubsemigroup of an AddCommSemigroup is an AddCommSemigroup.

Equations
theorem AddMemClass.toAddCommSemigroup.proof_1 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) :
Function.Injective fun (a : S) => a
theorem AddMemClass.toAddCommSemigroup.proof_2 {M : Type u_1} [] {A : Type u_2} [SetLike A M] [] (S : A) :
∀ (x x_1 : S), (x + x_1) = (x + x_1)
instance MulMemClass.toCommSemigroup {M : Type u_7} [] {A : Type u_6} [SetLike A M] [] (S : A) :

A subsemigroup of a CommSemigroup is a CommSemigroup.

Equations
def AddMemClass.subtype {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : ] (S' : A) :

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

Equations
• = { toFun := Subtype.val, map_add' := }
Instances For
theorem AddMemClass.subtype.proof_1 {M : Type u_1} {A : Type u_2} [Add M] [SetLike A M] [hA : ] (S' : A) :
∀ (x x_1 : S'), (x + x_1) = (x + x_1)
def MulMemClass.subtype {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : ] (S' : A) :
S' →ₙ* M

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

Equations
• = { toFun := Subtype.val, map_mul' := }
Instances For
@[simp]
theorem AddMemClass.coe_subtype {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : ] (S' : A) :
() = Subtype.val
@[simp]
theorem MulMemClass.coe_subtype {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : ] (S' : A) :
() = Subtype.val
∀ (x x_1 : ), { toFun := fun (x : ) => x, invFun := fun (x : M) => x, , left_inv := , right_inv := }.toFun (x + x_1) = { toFun := fun (x : ) => x, invFun := fun (x : M) => x, , left_inv := , right_inv := }.toFun (x + x_1)
∀ (x : M), (fun (x : ) => x) ((fun (x : M) => x, ) x) = (fun (x : ) => x) ((fun (x : M) => x, ) x)
≃+ M

Equations
• AddSubsemigroup.topEquiv = { toFun := fun (x : ) => x, invFun := fun (x : M) => x, , left_inv := , right_inv := , map_add' := }
Instances For
theorem AddSubsemigroup.topEquiv.proof_1 {M : Type u_1} [Add M] (x : ) :
x, = x
@[simp]
theorem Subsemigroup.topEquiv_symm_apply_coe {M : Type u_1} [Mul M] (x : M) :
(Subsemigroup.topEquiv.symm x) = x
@[simp]
theorem Subsemigroup.topEquiv_apply {M : Type u_1} [Mul M] (x : ) :
Subsemigroup.topEquiv x = x
@[simp]
theorem AddSubsemigroup.topEquiv_apply {M : Type u_1} [Add M] (x : ) :
@[simp]
theorem AddSubsemigroup.topEquiv_symm_apply_coe {M : Type u_1} [Add M] (x : M) :
def Subsemigroup.topEquiv {M : Type u_1} [Mul M] :
≃* M

The top subsemigroup is isomorphic to the semigroup.

Equations
• Subsemigroup.topEquiv = { toFun := fun (x : ) => x, invFun := fun (x : M) => x, , left_inv := , right_inv := , map_mul' := }
Instances For
@[simp]
@[simp]
theorem Subsemigroup.topEquiv_toMulHom {M : Type u_1} [Mul M] :
Subsemigroup.topEquiv =
theorem AddSubsemigroup.equivMapOfInjective.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : ) (f : AddHom M N) (hf : ) :
∀ (x x_1 : S), (Equiv.Set.image (f) (S) hf).toFun (x + x_1) = (Equiv.Set.image (f) (S) hf).toFun x + (Equiv.Set.image (f) (S) hf).toFun x_1
noncomputable def AddSubsemigroup.equivMapOfInjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : ) (f : AddHom M N) (hf : ) :
S ≃+ ()

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

Equations
• S.equivMapOfInjective f hf = let __src := Equiv.Set.image (f) (S) hf; { toEquiv := __src, map_add' := }
Instances For
noncomputable def Subsemigroup.equivMapOfInjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : ) (f : M →ₙ* N) (hf : ) :
S ≃* ()

A subsemigroup is isomorphic to its image under an injective function

Equations
• S.equivMapOfInjective f hf = let __src := Equiv.Set.image (f) (S) hf; { toEquiv := __src, map_mul' := }
Instances For
@[simp]
theorem AddSubsemigroup.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : ) (f : AddHom M N) (hf : ) (x : S) :
((S.equivMapOfInjective f hf) x) = f x
@[simp]
theorem Subsemigroup.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : ) (f : M →ₙ* N) (hf : ) (x : S) :
((S.equivMapOfInjective f hf) x) = f x
@[simp]
@[simp]
theorem Subsemigroup.closure_closure_coe_preimage {M : Type u_1} [Mul M] {s : Set M} :
theorem AddSubsemigroup.prod.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : ) (t : ) :
∀ {a b : M × N}, a s ×ˢ tb s ×ˢ t(a + b).1 s (a + b).2 t
def AddSubsemigroup.prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : ) (t : ) :

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

Equations
• s.prod t = { carrier := s ×ˢ t, add_mem' := }
Instances For
def Subsemigroup.prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : ) (t : ) :

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

Equations
• s.prod t = { carrier := s ×ˢ t, mul_mem' := }
Instances For
theorem AddSubsemigroup.coe_prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : ) (t : ) :
(s.prod t) = s ×ˢ t
theorem Subsemigroup.coe_prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : ) (t : ) :
(s.prod t) = s ×ˢ t
theorem AddSubsemigroup.mem_prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] {s : } {t : } {p : M × N} :
p s.prod t p.1 s p.2 t
theorem Subsemigroup.mem_prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {s : } {t : } {p : M × N} :
p s.prod t p.1 s p.2 t
theorem AddSubsemigroup.prod_mono {M : Type u_1} {N : Type u_2} [Add M] [Add N] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.prod t₁ s₂.prod t₂
theorem Subsemigroup.prod_mono {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.prod t₁ s₂.prod t₂
theorem AddSubsemigroup.prod_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : ) :
s.prod =
theorem Subsemigroup.prod_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : ) :
theorem AddSubsemigroup.top_prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : ) :
.prod s =
theorem Subsemigroup.top_prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : ) :
@[simp]
.prod =
@[simp]
theorem Subsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] :
.prod =
.prod =
theorem Subsemigroup.bot_prod_bot {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] :
.prod =
def AddSubsemigroup.prodEquiv {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : ) (t : ) :
(s.prod t) ≃+ s × t

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

Equations
• s.prodEquiv t = let __src := Equiv.Set.prod s t; { toEquiv := __src, map_add' := }
Instances For
theorem AddSubsemigroup.prodEquiv.proof_2 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : ) (t : ) :
∀ (x x_1 : (s.prod t)), (Equiv.Set.prod s t).toFun (x + x_1) = (Equiv.Set.prod s t).toFun (x + x_1)
def Subsemigroup.prodEquiv {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : ) (t : ) :
(s.prod t) ≃* s × t

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

Equations
• s.prodEquiv t = let __src := Equiv.Set.prod s t; { toEquiv := __src, map_mul' := }
Instances For
theorem AddSubsemigroup.mem_map_equiv {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M ≃+ N} {K : } {x : N} :
x AddSubsemigroup.map (f) K f.symm x K
theorem Subsemigroup.mem_map_equiv {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M ≃* N} {K : } {x : N} :
x Subsemigroup.map (f) K f.symm x K
theorem AddSubsemigroup.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M ≃+ N) (K : ) :
theorem Subsemigroup.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M ≃* N) (K : ) :
Subsemigroup.map (f) K = Subsemigroup.comap (f.symm) K
theorem AddSubsemigroup.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : N ≃+ M) (K : ) :
theorem Subsemigroup.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : N ≃* M) (K : ) :
Subsemigroup.comap (f) K = Subsemigroup.map (f.symm) K
@[simp]
theorem AddSubsemigroup.map_equiv_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M ≃+ N) :
@[simp]
theorem Subsemigroup.map_equiv_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M ≃* N) :
theorem AddSubsemigroup.le_prod_iff {M : Type u_1} {N : Type u_2} [Add M] [Add N] {s : } {t : } {u : AddSubsemigroup (M × N)} :
u s.prod t s t
theorem Subsemigroup.le_prod_iff {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {s : } {t : } {u : Subsemigroup (M × N)} :
= f '' Set.univ

The range of an AddHom is an AddSubsemigroup.

Equations
• f.srange = ().copy ()
Instances For
def MulHom.srange {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :

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

Equations
• f.srange = ().copy ()
Instances For
@[simp]
f.srange =
@[simp]
theorem MulHom.coe_srange {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
f.srange =
@[simp]
theorem AddHom.mem_srange {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {y : N} :
y f.srange ∃ (x : M), f x = y
@[simp]
theorem MulHom.mem_srange {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {y : N} :
y f.srange ∃ (x : M), f x = y
f.srange =
theorem MulHom.srange_eq_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
f.srange =
AddSubsemigroup.map g f.srange = (g.comp f).srange
theorem MulHom.map_srange {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul M] [Mul N] [Mul P] (g : N →ₙ* P) (f : M →ₙ* N) :
Subsemigroup.map g f.srange = (g.comp f).srange
f.srange =
theorem MulHom.srange_top_iff_surjective {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] {f : M →ₙ* N} :
f.srange =
@[simp]
theorem AddHom.srange_top_of_surjective {M : Type u_1} [Add M] {N : Type u_5} [Add N] (f : AddHom M N) (hf : ) :
f.srange =

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

@[simp]
theorem MulHom.srange_top_of_surjective {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] (f : M →ₙ* N) (hf : ) :
f.srange =

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} [Add M] [Add N] (f : AddHom M N) (s : Set N) :
theorem MulHom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (s : Set N) :
theorem AddHom.map_mclosure {M : Type u_1} {N : Type u_2} [Add M] [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} [Mul M] [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_4} [Add M] {N : Type u_5} [Add N] [SetLike σ M] [] (f : AddHom M N) (S : σ) :

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

Equations
• f.restrict S = f.comp
Instances For
def MulHom.restrict {M : Type u_1} {σ : Type u_4} [Mul M] {N : Type u_5} [Mul N] [SetLike σ M] [] (f : M →ₙ* N) (S : σ) :
S →ₙ* N

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

Equations
• f.restrict S = f.comp
Instances For
@[simp]
theorem AddHom.restrict_apply {M : Type u_1} {σ : Type u_4} [Add M] {N : Type u_5} [Add N] [SetLike σ M] [] (f : AddHom M N) {S : σ} (x : S) :
(f.restrict S) x = f x
@[simp]
theorem MulHom.restrict_apply {M : Type u_1} {σ : Type u_4} [Mul M] {N : Type u_5} [Mul N] [SetLike σ M] [] (f : M →ₙ* N) {S : σ} (x : S) :
(f.restrict S) x = f x
theorem AddHom.codRestrict.proof_1 {M : Type u_3} {N : Type u_1} {σ : Type u_2} [Add M] [Add N] [SetLike σ N] [] (f : AddHom M N) (S : σ) (h : ∀ (x : M), f x S) (x : M) (y : M) :
(fun (n : M) => f n, ) (x + y) = (fun (n : M) => f n, ) x + (fun (n : M) => f n, ) y
def AddHom.codRestrict {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Add M] [Add N] [SetLike σ N] [] (f : AddHom M N) (S : σ) (h : ∀ (x : M), f x S) :

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

Equations
• f.codRestrict S h = { toFun := fun (n : M) => f n, , map_add' := }
Instances For
@[simp]
theorem MulHom.codRestrict_apply_coe {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Mul M] [Mul N] [SetLike σ N] [] (f : M →ₙ* N) (S : σ) (h : ∀ (x : M), f x S) (n : M) :
((f.codRestrict S h) n) = f n
@[simp]
theorem AddHom.codRestrict_apply_coe {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Add M] [Add N] [SetLike σ N] [] (f : AddHom M N) (S : σ) (h : ∀ (x : M), f x S) (n : M) :
((f.codRestrict S h) n) = f n
def MulHom.codRestrict {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Mul M] [Mul N] [SetLike σ N] [] (f : M →ₙ* N) (S : σ) (h : ∀ (x : M), f x S) :
M →ₙ* S

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

Equations
• f.codRestrict S h = { toFun := fun (n : M) => f n, , map_mul' := }
Instances For

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

Equations
• f.srangeRestrict = f.codRestrict f.srange
Instances For
theorem AddHom.srangeRestrict.proof_1 {M : Type u_1} [Add M] {N : Type u_2} [Add N] (f : AddHom M N) (x : M) :
∃ (y : M), f y = f x
def MulHom.srangeRestrict {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] (f : M →ₙ* N) :
M →ₙ* f.srange

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

Equations
• f.srangeRestrict = f.codRestrict f.srange
Instances For
@[simp]
theorem AddHom.coe_srangeRestrict {M : Type u_1} [Add M] {N : Type u_5} [Add N] (f : AddHom M N) (x : M) :
(f.srangeRestrict x) = f x
@[simp]
theorem MulHom.coe_srangeRestrict {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] (f : M →ₙ* N) (x : M) :
(f.srangeRestrict x) = f x
abbrev AddHom.srangeRestrict_surjective.match_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (motive : f.srangeProp) :
∀ (x : f.srange), (∀ (x : M), motive f x, )motive x
Equations
• =
Instances For
Function.Surjective f.srangeRestrict
theorem MulHom.srangeRestrict_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
Function.Surjective f.srangeRestrict
theorem AddHom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [Add M] [Add N] {M' : Type u_5} {N' : Type u_6} [Add M'] [Add N'] (f : AddHom M N) (g : AddHom M' N') (S : ) (S' : ) :
AddSubsemigroup.comap (f.prodMap g) (S.prod S') = ().prod ()
theorem MulHom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {M' : Type u_5} {N' : Type u_6} [Mul M'] [Mul N'] (f : M →ₙ* N) (g : M' →ₙ* N') (S : ) (S' : ) :
Subsemigroup.comap (f.prodMap g) (S.prod S') = ().prod ()
theorem AddHom.subsemigroupComap.proof_2 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (N' : ) (x : ()) (y : ()) :
(fun (x : ()) => f x, ) (x + y) = (fun (x : ()) => f x, ) x + (fun (x : ()) => f x, ) y
def AddHom.subsemigroupComap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (N' : ) :

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

Equations
• f.subsemigroupComap N' = { toFun := fun (x : ()) => f x, , map_add' := }
Instances For
theorem AddHom.subsemigroupComap.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (N' : ) (x : ()) :
x
@[simp]
theorem AddHom.subsemigroupComap_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (N' : ) (x : ()) :
((f.subsemigroupComap N') x) = f x
@[simp]
theorem MulHom.subsemigroupComap_apply_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (N' : ) (x : ()) :
((f.subsemigroupComap N') x) = f x
def MulHom.subsemigroupComap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (N' : ) :
() →ₙ* N'

The MulHom from the preimage of a subsemigroup to itself.

Equations
• f.subsemigroupComap N' = { toFun := fun (x : ()) => f x, , map_mul' := }
Instances For
theorem AddHom.subsemigroupMap.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : ) (x : M') :
aM', f a = f x
theorem AddHom.subsemigroupMap.proof_2 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : ) (x : M') (y : M') :
(fun (x : M') => f x, ) (x + y) = (fun (x : M') => f x, ) x + (fun (x : M') => f x, ) y
def AddHom.subsemigroupMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : ) :

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

Equations
• f.subsemigroupMap M' = { toFun := fun (x : M') => f x, , map_add' := }
Instances For
@[simp]
theorem MulHom.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (M' : ) (x : M') :
((f.subsemigroupMap M') x) = f x
@[simp]
theorem AddHom.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : ) (x : M') :
((f.subsemigroupMap M') x) = f x
def MulHom.subsemigroupMap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (M' : ) :
M' →ₙ* ()

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

Equations
• f.subsemigroupMap M' = { toFun := fun (x : M') => f x, , map_mul' := }
Instances For
theorem AddHom.subsemigroupMap_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : ) :
Function.Surjective (f.subsemigroupMap M')
theorem MulHom.subsemigroupMap_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (M' : ) :
Function.Surjective (f.subsemigroupMap M')
@[simp]
().srange =
@[simp]
theorem Subsemigroup.srange_fst {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] [] :
().srange =
@[simp]
().srange =
@[simp]
theorem Subsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] [] :
().srange =
theorem AddSubsemigroup.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [Add M] [Add N] [] [] {s : } {t : } :
s.prod t = s = t =
theorem Subsemigroup.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] [] [] {s : } {t : } :
s.prod t = s = t =
def AddSubsemigroup.inclusion {M : Type u_1} [Add M] {S : } {T : } (h : S T) :

The AddSemigroup hom associated to an inclusion of subsemigroups.

Equations
• = .codRestrict T
Instances For
theorem AddSubsemigroup.inclusion.proof_1 {M : Type u_1} [Add M] {S : } {T : } (h : S T) (x : S) :
x T
def Subsemigroup.inclusion {M : Type u_1} [Mul M] {S : } {T : } (h : S T) :
S →ₙ* T

The semigroup hom associated to an inclusion of subsemigroups.

Equations
• = .codRestrict T
Instances For
@[simp]
theorem AddSubsemigroup.range_subtype {M : Type u_1} [Add M] (s : ) :
.srange = s
@[simp]
theorem Subsemigroup.range_subtype {M : Type u_1} [Mul M] (s : ) :
.srange = s
theorem AddSubsemigroup.eq_top_iff' {M : Type u_1} [Add M] (S : ) :
S = ∀ (x : M), x S
theorem Subsemigroup.eq_top_iff' {M : Type u_1} [Mul M] (S : ) :
S = ∀ (x : M), x S
def AddEquiv.subsemigroupCongr {M : Type u_1} [Add M] {S : } {T : } (h : S = T) :
S ≃+ T

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

Equations
• = let __src := ; { toEquiv := __src, map_add' := }
Instances For
theorem AddEquiv.subsemigroupCongr.proof_2 {M : Type u_1} [Add M] {S : } {T : } (h : S = T) :
∀ (x x_1 : S), ().toFun (x + x_1) = ().toFun (x + x_1)
theorem AddEquiv.subsemigroupCongr.proof_1 {M : Type u_1} [Add M] {S : } {T : } (h : S = T) :
S = T
def MulEquiv.subsemigroupCongr {M : Type u_1} [Mul M] {S : } {T : } (h : S = T) :
S ≃* T

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

Equations
• = let __src := ; { toEquiv := __src, map_mul' := }
Instances For
abbrev AddEquiv.ofLeftInverse.match_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (x : f.srange) (motive : (∃ (x_1 : M), f x_1 = x)Prop) :
∀ (x_1 : ∃ (x_1 : M), f x_1 = x), (∀ (x' : M) (hx' : f x' = x), motive )motive x_1
Equations
• =
Instances For
def AddEquiv.ofLeftInverse {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) {g : NM} (h : ) :
M ≃+ f.srange

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.

Equations
• = let __src := f.srangeRestrict; { toFun := f.srangeRestrict, invFun := g (AddMemClass.subtype f.srange), left_inv := h, right_inv := , map_add' := }
Instances For
theorem AddEquiv.ofLeftInverse.proof_2 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (x : M) (y : M) :
f.srangeRestrict.toFun (x + y) = f.srangeRestrict.toFun x + f.srangeRestrict.toFun y
theorem AddEquiv.ofLeftInverse.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) {g : NM} (h : ) (x : f.srange) :
f.srangeRestrict ((g (AddMemClass.subtype f.srange)) x) = x
@[simp]
theorem AddEquiv.ofLeftInverse_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) {g : NM} (h : ) (a : M) :
() a = f.srangeRestrict a
@[simp]
theorem MulEquiv.ofLeftInverse_symm_apply {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) {g : NM} (h : ) :
∀ (a : f.srange), ().symm a = g a
@[simp]
theorem AddEquiv.ofLeftInverse_symm_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) {g : NM} (h : ) :
∀ (a : f.srange), ().symm a = g a
@[simp]
theorem MulEquiv.ofLeftInverse_apply {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) {g : NM} (h : ) (a : M) :
() a = f.srangeRestrict a
def MulEquiv.ofLeftInverse {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) {g : NM} (h : ) :
M ≃* f.srange

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.

Equations
• = let __src := f.srangeRestrict; { toFun := f.srangeRestrict, invFun := g (MulMemClass.subtype f.srange), left_inv := h, right_inv := , map_mul' := }
Instances For
AddHomClass (M ≃+ N) M N
theorem AddEquiv.subsemigroupMap.proof_4 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : ) :
Function.LeftInverse ((e).image S).invFun ((e).image S).toFun
def AddEquiv.subsemigroupMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : ) :

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 AddHoms.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddEquiv.subsemigroupMap.proof_5 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : ) :
Function.RightInverse ((e).image S).invFun ((e).image S).toFun
theorem AddEquiv.subsemigroupMap.proof_2 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (e : M ≃+ N) (S : ) (x : S) :
e x e '' S
theorem AddEquiv.subsemigroupMap.proof_3 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : ) (x : (AddSubsemigroup.map (e) S)) :
(e).symm x S
theorem AddEquiv.subsemigroupMap.proof_6 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : ) (x : S) (y : S) :
((e).subsemigroupMap S).toFun (x + y) = ((e).subsemigroupMap S).toFun x + ((e).subsemigroupMap S).toFun y
@[simp]
theorem MulEquiv.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (e : M ≃* N) (S : ) (x : S) :
((e.subsemigroupMap S) x) = e x
@[simp]
theorem MulEquiv.subsemigroupMap_symm_apply_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (e : M ≃* N) (S : ) (x : (Subsemigroup.map (e) S)) :
((e.subsemigroupMap S).symm x) = e.symm x
@[simp]
theorem AddEquiv.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : ) (x : S) :
((e.subsemigroupMap S) x) = e x
@[simp]
theorem AddEquiv.subsemigroupMap_symm_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : ) (x : (AddSubsemigroup.map (e) S)) :
((e.subsemigroupMap S).symm x) = e.symm x
def MulEquiv.subsemigroupMap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (e : M ≃* N) (S : ) :
S ≃* (Subsemigroup.map (e) S)

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 MulHoms.

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