Operations on `Subsemigroup`s #

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 `MulHom`s #

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` #

source

def Subsemigroup.toAddSubsemigroup {M : Type u_1} [Mul M] :

Subsemigroup M ≃o AddSubsemigroup (Additive M)

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

source

@[simp]

theorem Subsemigroup.coe_toAddSubsemigroup_symm_apply {M : Type u_1} [Mul M] (S : AddSubsemigroup (Additive M)) :

↑((RelIso.symm Subsemigroup.toAddSubsemigroup) S) = ⇑Additive.ofMul ⁻¹' ↑S

source

@[simp]

theorem Subsemigroup.coe_toAddSubsemigroup_apply {M : Type u_1} [Mul M] (S : Subsemigroup M) :

↑(Subsemigroup.toAddSubsemigroup S) = ⇑Additive.toMul ⁻¹' ↑S

source

@[reducible, inline]

abbrev AddSubsemigroup.toSubsemigroup' {M : Type u_1} [Mul M] :

AddSubsemigroup (Additive M) ≃o Subsemigroup M

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

Equations

AddSubsemigroup.toSubsemigroup' = Subsemigroup.toAddSubsemigroup.symm

Instances For

source

theorem Subsemigroup.toAddSubsemigroup_closure {M : Type u_1} [Mul M] (S : Set M) :

Subsemigroup.toAddSubsemigroup (Subsemigroup.closure S) = AddSubsemigroup.closure (⇑Additive.toMul ⁻¹' S)

source

theorem AddSubsemigroup.toSubsemigroup'_closure {M : Type u_1} [Mul M] (S : Set (Additive M)) :

AddSubsemigroup.toSubsemigroup' (AddSubsemigroup.closure S) = Subsemigroup.closure (⇑Additive.ofMul ⁻¹' S)

source

def AddSubsemigroup.toSubsemigroup {A : Type u_5} [Add A] :

AddSubsemigroup A ≃o Subsemigroup (Multiplicative A)

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

source

@[simp]

theorem AddSubsemigroup.coe_toSubsemigroup_symm_apply {A : Type u_5} [Add A] (S : Subsemigroup (Multiplicative A)) :

↑((RelIso.symm AddSubsemigroup.toSubsemigroup) S) = ⇑Multiplicative.ofAdd ⁻¹' ↑S

source

@[simp]

theorem AddSubsemigroup.coe_toSubsemigroup_apply {A : Type u_5} [Add A] (S : AddSubsemigroup A) :

↑(AddSubsemigroup.toSubsemigroup S) = ⇑Multiplicative.toAdd ⁻¹' ↑S

source

@[reducible, inline]

abbrev Subsemigroup.toAddSubsemigroup' {A : Type u_5} [Add A] :

Subsemigroup (Multiplicative A) ≃o AddSubsemigroup A

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

Equations

Subsemigroup.toAddSubsemigroup' = AddSubsemigroup.toSubsemigroup.symm

Instances For

source

theorem AddSubsemigroup.toSubsemigroup_closure {A : Type u_5} [Add A] (S : Set A) :

AddSubsemigroup.toSubsemigroup (AddSubsemigroup.closure S) = Subsemigroup.closure (⇑Multiplicative.toAdd ⁻¹' S)

source

theorem Subsemigroup.toAddSubsemigroup'_closure {A : Type u_5} [Add A] (S : Set (Multiplicative A)) :

Subsemigroup.toAddSubsemigroup' (Subsemigroup.closure S) = AddSubsemigroup.closure (⇑Multiplicative.ofAdd ⁻¹' S)

`comap` and `map` #

source

def Subsemigroup.comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : Subsemigroup N) :

Subsemigroup M

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

Equations

Subsemigroup.comap f S = { carrier := ⇑f ⁻¹' ↑S, mul_mem' := ⋯ }

Instances For

source

def AddSubsemigroup.comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (S : AddSubsemigroup N) :

AddSubsemigroup M

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

Equations

AddSubsemigroup.comap f S = { carrier := ⇑f ⁻¹' ↑S, add_mem' := ⋯ }

Instances For

source

@[simp]

theorem Subsemigroup.coe_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup N) (f : M →ₙ* N) :

↑(Subsemigroup.comap f S) = ⇑f ⁻¹' ↑S

source

@[simp]

theorem AddSubsemigroup.coe_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup N) (f : M →ₙ+ N) :

↑(AddSubsemigroup.comap f S) = ⇑f ⁻¹' ↑S

source

@[simp]

theorem Subsemigroup.mem_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {S : Subsemigroup N} {f : M →ₙ* N} {x : M} :

x ∈ Subsemigroup.comap f S ↔ f x ∈ S

source

@[simp]

theorem AddSubsemigroup.mem_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {S : AddSubsemigroup N} {f : M →ₙ+ N} {x : M} :

x ∈ AddSubsemigroup.comap f S ↔ f x ∈ S

source

theorem Subsemigroup.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul M] [Mul N] [Mul P] (S : Subsemigroup P) (g : N →ₙ* P) (f : M →ₙ* N) :

Subsemigroup.comap f (Subsemigroup.comap g S) = Subsemigroup.comap (g.comp f) S

source

theorem AddSubsemigroup.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [Add P] (S : AddSubsemigroup P) (g : N →ₙ+ P) (f : M →ₙ+ N) :

AddSubsemigroup.comap f (AddSubsemigroup.comap g S) = AddSubsemigroup.comap (g.comp f) S

source

@[simp]

theorem Subsemigroup.comap_id {P : Type u_3} [Mul P] (S : Subsemigroup P) :

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

source

@[simp]

theorem AddSubsemigroup.comap_id {P : Type u_3} [Add P] (S : AddSubsemigroup P) :

AddSubsemigroup.comap (AddHom.id P) S = S

source

def Subsemigroup.map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : Subsemigroup M) :

Subsemigroup N

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

Equations

Subsemigroup.map f S = { carrier := ⇑f '' ↑S, mul_mem' := ⋯ }

Instances For

source

def AddSubsemigroup.map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (S : AddSubsemigroup M) :

AddSubsemigroup N

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

Equations

AddSubsemigroup.map f S = { carrier := ⇑f '' ↑S, add_mem' := ⋯ }

Instances For

source

@[simp]

theorem Subsemigroup.coe_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : Subsemigroup M) :

↑(Subsemigroup.map f S) = ⇑f '' ↑S

source

@[simp]

theorem AddSubsemigroup.coe_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (S : AddSubsemigroup M) :

↑(AddSubsemigroup.map f S) = ⇑f '' ↑S

source

@[simp]

theorem Subsemigroup.mem_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {S : Subsemigroup M} {y : N} :

y ∈ Subsemigroup.map f S ↔ ∃ x ∈ S, f x = y

source

@[simp]

theorem AddSubsemigroup.mem_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} {S : AddSubsemigroup M} {y : N} :

y ∈ AddSubsemigroup.map f S ↔ ∃ x ∈ S, f x = y

source

theorem Subsemigroup.mem_map_of_mem {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) {S : Subsemigroup M} {x : M} (hx : x ∈ S) :

f x ∈ Subsemigroup.map f S

source

theorem AddSubsemigroup.mem_map_of_mem {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) {S : AddSubsemigroup M} {x : M} (hx : x ∈ S) :

f x ∈ AddSubsemigroup.map f S

source

theorem Subsemigroup.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : Subsemigroup M) (x : ↥S) :

f ↑x ∈ Subsemigroup.map f S

source

theorem AddSubsemigroup.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (S : AddSubsemigroup M) (x : ↥S) :

f ↑x ∈ AddSubsemigroup.map f S

source

theorem Subsemigroup.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul M] [Mul N] [Mul P] (S : Subsemigroup M) (g : N →ₙ* P) (f : M →ₙ* N) :

Subsemigroup.map g (Subsemigroup.map f S) = Subsemigroup.map (g.comp f) S

source

theorem AddSubsemigroup.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [Add P] (S : AddSubsemigroup M) (g : N →ₙ+ P) (f : M →ₙ+ N) :

AddSubsemigroup.map g (AddSubsemigroup.map f S) = AddSubsemigroup.map (g.comp f) S

source

@[simp]

theorem Subsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Injective ⇑f) {S : Subsemigroup M} {x : M} :

f x ∈ Subsemigroup.map f S ↔ x ∈ S

source

@[simp]

theorem AddSubsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Injective ⇑f) {S : AddSubsemigroup M} {x : M} :

f x ∈ AddSubsemigroup.map f S ↔ x ∈ S

source

theorem Subsemigroup.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {S : Subsemigroup M} {T : Subsemigroup N} :

Subsemigroup.map f S ≤ T ↔ S ≤ Subsemigroup.comap f T

source

theorem AddSubsemigroup.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} {S : AddSubsemigroup M} {T : AddSubsemigroup N} :

AddSubsemigroup.map f S ≤ T ↔ S ≤ AddSubsemigroup.comap f T

source

theorem Subsemigroup.gc_map_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :

GaloisConnection (Subsemigroup.map f) (Subsemigroup.comap f)

source

theorem AddSubsemigroup.gc_map_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :

GaloisConnection (AddSubsemigroup.map f) (AddSubsemigroup.comap f)

source

theorem Subsemigroup.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) {T : Subsemigroup N} {f : M →ₙ* N} :

S ≤ Subsemigroup.comap f T → Subsemigroup.map f S ≤ T

source

theorem AddSubsemigroup.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) {T : AddSubsemigroup N} {f : M →ₙ+ N} :

S ≤ AddSubsemigroup.comap f T → AddSubsemigroup.map f S ≤ T

source

theorem Subsemigroup.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) {T : Subsemigroup N} {f : M →ₙ* N} :

Subsemigroup.map f S ≤ T → S ≤ Subsemigroup.comap f T

source

theorem AddSubsemigroup.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) {T : AddSubsemigroup N} {f : M →ₙ+ N} :

AddSubsemigroup.map f S ≤ T → S ≤ AddSubsemigroup.comap f T

source

theorem Subsemigroup.le_comap_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) {f : M →ₙ* N} :

S ≤ Subsemigroup.comap f (Subsemigroup.map f S)

source

theorem AddSubsemigroup.le_comap_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) {f : M →ₙ+ N} :

S ≤ AddSubsemigroup.comap f (AddSubsemigroup.map f S)

source

theorem Subsemigroup.map_comap_le {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {S : Subsemigroup N} {f : M →ₙ* N} :

Subsemigroup.map f (Subsemigroup.comap f S) ≤ S

source

theorem AddSubsemigroup.map_comap_le {M : Type u_1} {N : Type u_2} [Add M] [Add N] {S : AddSubsemigroup N} {f : M →ₙ+ N} :

AddSubsemigroup.map f (AddSubsemigroup.comap f S) ≤ S

source

theorem Subsemigroup.monotone_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} :

Monotone (Subsemigroup.map f)

source

theorem AddSubsemigroup.monotone_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} :

Monotone (AddSubsemigroup.map f)

source

theorem Subsemigroup.monotone_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} :

Monotone (Subsemigroup.comap f)

source

theorem AddSubsemigroup.monotone_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} :

Monotone (AddSubsemigroup.comap f)

source

@[simp]

theorem Subsemigroup.map_comap_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) {f : M →ₙ* N} :

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

source

@[simp]

theorem AddSubsemigroup.map_comap_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) {f : M →ₙ+ N} :

AddSubsemigroup.map f (AddSubsemigroup.comap f (AddSubsemigroup.map f S)) = AddSubsemigroup.map f S

source

@[simp]

theorem Subsemigroup.comap_map_comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {S : Subsemigroup N} {f : M →ₙ* N} :

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

source

@[simp]

theorem AddSubsemigroup.comap_map_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {S : AddSubsemigroup N} {f : M →ₙ+ N} :

AddSubsemigroup.comap f (AddSubsemigroup.map f (AddSubsemigroup.comap f S)) = AddSubsemigroup.comap f S

source

theorem Subsemigroup.map_sup {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S T : Subsemigroup M) (f : M →ₙ* N) :

Subsemigroup.map f (S ⊔ T) = Subsemigroup.map f S ⊔ Subsemigroup.map f T

source

theorem AddSubsemigroup.map_sup {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S T : AddSubsemigroup M) (f : M →ₙ+ N) :

AddSubsemigroup.map f (S ⊔ T) = AddSubsemigroup.map f S ⊔ AddSubsemigroup.map f T

source

theorem Subsemigroup.map_iSup {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Sort u_5} (f : M →ₙ* N) (s : ι → Subsemigroup M) :

Subsemigroup.map f (iSup s) = ⨆ (i : ι), Subsemigroup.map f (s i)

source

theorem AddSubsemigroup.map_iSup {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Sort u_5} (f : M →ₙ+ N) (s : ι → AddSubsemigroup M) :

AddSubsemigroup.map f (iSup s) = ⨆ (i : ι), AddSubsemigroup.map f (s i)

source

theorem Subsemigroup.map_inf {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S T : Subsemigroup M) (f : M →ₙ* N) (hf : Function.Injective ⇑f) :

Subsemigroup.map f (S ⊓ T) = Subsemigroup.map f S ⊓ Subsemigroup.map f T

source

theorem AddSubsemigroup.map_inf {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S T : AddSubsemigroup M) (f : M →ₙ+ N) (hf : Function.Injective ⇑f) :

AddSubsemigroup.map f (S ⊓ T) = AddSubsemigroup.map f S ⊓ AddSubsemigroup.map f T

source

theorem Subsemigroup.map_iInf {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Sort u_5} [Nonempty ι] (f : M →ₙ* N) (hf : Function.Injective ⇑f) (s : ι → Subsemigroup M) :

Subsemigroup.map f (iInf s) = ⨅ (i : ι), Subsemigroup.map f (s i)

source

theorem AddSubsemigroup.map_iInf {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Sort u_5} [Nonempty ι] (f : M →ₙ+ N) (hf : Function.Injective ⇑f) (s : ι → AddSubsemigroup M) :

AddSubsemigroup.map f (iInf s) = ⨅ (i : ι), AddSubsemigroup.map f (s i)

source

theorem Subsemigroup.comap_inf {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S T : Subsemigroup N) (f : M →ₙ* N) :

Subsemigroup.comap f (S ⊓ T) = Subsemigroup.comap f S ⊓ Subsemigroup.comap f T

source

theorem AddSubsemigroup.comap_inf {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S T : AddSubsemigroup N) (f : M →ₙ+ N) :

AddSubsemigroup.comap f (S ⊓ T) = AddSubsemigroup.comap f S ⊓ AddSubsemigroup.comap f T

source

theorem Subsemigroup.comap_iInf {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {ι : Sort u_5} (f : M →ₙ* N) (s : ι → Subsemigroup N) :

Subsemigroup.comap f (iInf s) = ⨅ (i : ι), Subsemigroup.comap f (s i)

source

theorem AddSubsemigroup.comap_iInf {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Sort u_5} (f : M →ₙ+ N) (s : ι → AddSubsemigroup N) :

AddSubsemigroup.comap f (iInf s) = ⨅ (i : ι), AddSubsemigroup.comap f (s i)

source

@[simp]

theorem Subsemigroup.map_bot {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :

Subsemigroup.map f ⊥ = ⊥

source

@[simp]

theorem AddSubsemigroup.map_bot {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :

AddSubsemigroup.map f ⊥ = ⊥

source

@[simp]

theorem Subsemigroup.comap_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :

Subsemigroup.comap f ⊤ = ⊤

source

@[simp]

theorem AddSubsemigroup.comap_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :

AddSubsemigroup.comap f ⊤ = ⊤

source

@[simp]

theorem Subsemigroup.map_id {M : Type u_1} [Mul M] (S : Subsemigroup M) :

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

source

@[simp]

theorem AddSubsemigroup.map_id {M : Type u_1} [Add M] (S : AddSubsemigroup M) :

AddSubsemigroup.map (AddHom.id M) S = S

source

def Subsemigroup.gciMapComap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Injective ⇑f) :

GaloisCoinsertion (Subsemigroup.map f) (Subsemigroup.comap f)

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

Equations

Subsemigroup.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯

Instances For

source

def AddSubsemigroup.gciMapComap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Injective ⇑f) :

GaloisCoinsertion (AddSubsemigroup.map f) (AddSubsemigroup.comap f)

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

Equations

AddSubsemigroup.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯

Instances For

source

theorem Subsemigroup.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Injective ⇑f) (S : Subsemigroup M) :

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

source

theorem AddSubsemigroup.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Injective ⇑f) (S : AddSubsemigroup M) :

AddSubsemigroup.comap f (AddSubsemigroup.map f S) = S

source

theorem Subsemigroup.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Injective ⇑f) :

Function.Surjective (Subsemigroup.comap f)

source

theorem AddSubsemigroup.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Injective ⇑f) :

Function.Surjective (AddSubsemigroup.comap f)

source

theorem Subsemigroup.map_injective_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Injective ⇑f) :

Function.Injective (Subsemigroup.map f)

source

theorem AddSubsemigroup.map_injective_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Injective ⇑f) :

Function.Injective (AddSubsemigroup.map f)

source

theorem Subsemigroup.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Injective ⇑f) (S T : Subsemigroup M) :

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

source

theorem AddSubsemigroup.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Injective ⇑f) (S T : AddSubsemigroup M) :

AddSubsemigroup.comap f (AddSubsemigroup.map f S ⊓ AddSubsemigroup.map f T) = S ⊓ T

source

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 : Function.Injective ⇑f) (S : ι → Subsemigroup M) :

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

source

theorem AddSubsemigroup.comap_iInf_map_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Type u_5} {f : M →ₙ+ N} (hf : Function.Injective ⇑f) (S : ι → AddSubsemigroup M) :

AddSubsemigroup.comap f (⨅ (i : ι), AddSubsemigroup.map f (S i)) = iInf S

source

theorem Subsemigroup.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Injective ⇑f) (S T : Subsemigroup M) :

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

source

theorem AddSubsemigroup.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Injective ⇑f) (S T : AddSubsemigroup M) :

AddSubsemigroup.comap f (AddSubsemigroup.map f S ⊔ AddSubsemigroup.map f T) = S ⊔ T

source

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 : Function.Injective ⇑f) (S : ι → Subsemigroup M) :

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

source

theorem AddSubsemigroup.comap_iSup_map_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Type u_5} {f : M →ₙ+ N} (hf : Function.Injective ⇑f) (S : ι → AddSubsemigroup M) :

AddSubsemigroup.comap f (⨆ (i : ι), AddSubsemigroup.map f (S i)) = iSup S

source

theorem Subsemigroup.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Injective ⇑f) {S T : Subsemigroup M} :

Subsemigroup.map f S ≤ Subsemigroup.map f T ↔ S ≤ T

source

theorem AddSubsemigroup.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Injective ⇑f) {S T : AddSubsemigroup M} :

AddSubsemigroup.map f S ≤ AddSubsemigroup.map f T ↔ S ≤ T

source

theorem Subsemigroup.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Injective ⇑f) :

StrictMono (Subsemigroup.map f)

source

theorem AddSubsemigroup.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Injective ⇑f) :

StrictMono (AddSubsemigroup.map f)

source

def Subsemigroup.giMapComap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Surjective ⇑f) :

GaloisInsertion (Subsemigroup.map f) (Subsemigroup.comap f)

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

Equations

Subsemigroup.giMapComap hf = ⋯.toGaloisInsertion ⋯

Instances For

source

def AddSubsemigroup.giMapComap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Surjective ⇑f) :

GaloisInsertion (AddSubsemigroup.map f) (AddSubsemigroup.comap f)

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

Equations

AddSubsemigroup.giMapComap hf = ⋯.toGaloisInsertion ⋯

Instances For

source

theorem Subsemigroup.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Surjective ⇑f) (S : Subsemigroup N) :

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

source

theorem AddSubsemigroup.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Surjective ⇑f) (S : AddSubsemigroup N) :

AddSubsemigroup.map f (AddSubsemigroup.comap f S) = S

source

theorem Subsemigroup.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Surjective ⇑f) :

Function.Surjective (Subsemigroup.map f)

source

theorem AddSubsemigroup.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Surjective ⇑f) :

Function.Surjective (AddSubsemigroup.map f)

source

theorem Subsemigroup.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Surjective ⇑f) :

Function.Injective (Subsemigroup.comap f)

source

theorem AddSubsemigroup.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Surjective ⇑f) :

Function.Injective (AddSubsemigroup.comap f)

source

theorem Subsemigroup.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Surjective ⇑f) (S T : Subsemigroup N) :

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

source

theorem AddSubsemigroup.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Surjective ⇑f) (S T : AddSubsemigroup N) :

AddSubsemigroup.map f (AddSubsemigroup.comap f S ⊓ AddSubsemigroup.comap f T) = S ⊓ T

source

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 : Function.Surjective ⇑f) (S : ι → Subsemigroup N) :

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

source

theorem AddSubsemigroup.map_iInf_comap_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Type u_5} {f : M →ₙ+ N} (hf : Function.Surjective ⇑f) (S : ι → AddSubsemigroup N) :

AddSubsemigroup.map f (⨅ (i : ι), AddSubsemigroup.comap f (S i)) = iInf S

source

theorem Subsemigroup.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Surjective ⇑f) (S T : Subsemigroup N) :

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

source

theorem AddSubsemigroup.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Surjective ⇑f) (S T : AddSubsemigroup N) :

AddSubsemigroup.map f (AddSubsemigroup.comap f S ⊔ AddSubsemigroup.comap f T) = S ⊔ T

source

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 : Function.Surjective ⇑f) (S : ι → Subsemigroup N) :

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

source

theorem AddSubsemigroup.map_iSup_comap_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Type u_5} {f : M →ₙ+ N} (hf : Function.Surjective ⇑f) (S : ι → AddSubsemigroup N) :

AddSubsemigroup.map f (⨆ (i : ι), AddSubsemigroup.comap f (S i)) = iSup S

source

theorem Subsemigroup.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Surjective ⇑f) {S T : Subsemigroup N} :

Subsemigroup.comap f S ≤ Subsemigroup.comap f T ↔ S ≤ T

source

theorem AddSubsemigroup.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Surjective ⇑f) {S T : AddSubsemigroup N} :

AddSubsemigroup.comap f S ≤ AddSubsemigroup.comap f T ↔ S ≤ T

source

theorem Subsemigroup.comap_strictMono_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} (hf : Function.Surjective ⇑f) :

StrictMono (Subsemigroup.comap f)

source

theorem AddSubsemigroup.comap_strictMono_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} (hf : Function.Surjective ⇑f) :

StrictMono (AddSubsemigroup.comap f)

source

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

source

def AddSubsemigroup.topEquiv {M : Type u_1} [Add M] :

↥⊤ ≃+ M

The top additive subsemigroup is isomorphic to the additive semigroup.

Equations

AddSubsemigroup.topEquiv = { toFun := fun (x : ↥⊤) => ↑x, invFun := fun (x : M) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem Subsemigroup.topEquiv_apply {M : Type u_1} [Mul M] (x : ↥⊤) :

Subsemigroup.topEquiv x = ↑x

source

@[simp]

theorem AddSubsemigroup.topEquiv_symm_apply_coe {M : Type u_1} [Add M] (x : M) :

↑(AddSubsemigroup.topEquiv.symm x) = x

source

@[simp]

theorem Subsemigroup.topEquiv_symm_apply_coe {M : Type u_1} [Mul M] (x : M) :

↑(Subsemigroup.topEquiv.symm x) = x

source

@[simp]

theorem AddSubsemigroup.topEquiv_apply {M : Type u_1} [Add M] (x : ↥⊤) :

AddSubsemigroup.topEquiv x = ↑x

source

@[simp]

theorem Subsemigroup.topEquiv_toMulHom {M : Type u_1} [Mul M] :

↑Subsemigroup.topEquiv = MulMemClass.subtype ⊤

source

@[simp]

theorem AddSubsemigroup.topEquiv_toAddHom {M : Type u_1} [Add M] :

↑AddSubsemigroup.topEquiv = AddMemClass.subtype ⊤

source

noncomputable def Subsemigroup.equivMapOfInjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) (f : M →ₙ* N) (hf : Function.Injective ⇑f) :

↥S ≃* ↥(Subsemigroup.map f S)

A subsemigroup is isomorphic to its image under an injective function

Equations

S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_mul' := ⋯ }

Instances For

source

noncomputable def AddSubsemigroup.equivMapOfInjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) (f : M →ₙ+ N) (hf : Function.Injective ⇑f) :

↥S ≃+ ↥(AddSubsemigroup.map f S)

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

Equations

S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_add' := ⋯ }

Instances For

source

@[simp]

theorem Subsemigroup.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) (f : M →ₙ* N) (hf : Function.Injective ⇑f) (x : ↥S) :

↑((S.equivMapOfInjective f hf) x) = f ↑x

source

@[simp]

theorem AddSubsemigroup.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) (f : M →ₙ+ N) (hf : Function.Injective ⇑f) (x : ↥S) :

↑((S.equivMapOfInjective f hf) x) = f ↑x

source

@[simp]

theorem Subsemigroup.closure_closure_coe_preimage {M : Type u_1} [Mul M] {s : Set M} :

Subsemigroup.closure (Subtype.val ⁻¹' s) = ⊤

source

@[simp]

theorem AddSubsemigroup.closure_closure_coe_preimage {M : Type u_1} [Add M] {s : Set M} :

AddSubsemigroup.closure (Subtype.val ⁻¹' s) = ⊤

source

def Subsemigroup.prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup M) (t : Subsemigroup N) :

Subsemigroup (M × N)

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

source

def AddSubsemigroup.prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :

AddSubsemigroup (M × N)

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

source

theorem Subsemigroup.coe_prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup M) (t : Subsemigroup N) :

↑(s.prod t) = ↑s ×ˢ ↑t

source

theorem AddSubsemigroup.coe_prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :

↑(s.prod t) = ↑s ×ˢ ↑t

source

theorem Subsemigroup.mem_prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {s : Subsemigroup M} {t : Subsemigroup N} {p : M × N} :

p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t

source

theorem AddSubsemigroup.mem_prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] {s : AddSubsemigroup M} {t : AddSubsemigroup N} {p : M × N} :

p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t

source

theorem Subsemigroup.prod_mono {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {s₁ s₂ : Subsemigroup M} {t₁ t₂ : Subsemigroup N} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :

s₁.prod t₁ ≤ s₂.prod t₂

source

theorem AddSubsemigroup.prod_mono {M : Type u_1} {N : Type u_2} [Add M] [Add N] {s₁ s₂ : AddSubsemigroup M} {t₁ t₂ : AddSubsemigroup N} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :

s₁.prod t₁ ≤ s₂.prod t₂

source

theorem Subsemigroup.prod_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup M) :

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

source

theorem AddSubsemigroup.prod_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) :

s.prod ⊤ = AddSubsemigroup.comap (AddHom.fst M N) s

source

theorem Subsemigroup.top_prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup N) :

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

source

theorem AddSubsemigroup.top_prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup N) :

⊤.prod s = AddSubsemigroup.comap (AddHom.snd M N) s

source

@[simp]

theorem Subsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] :

⊤.prod ⊤ = ⊤

source

@[simp]

theorem AddSubsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] :

⊤.prod ⊤ = ⊤

source

theorem Subsemigroup.bot_prod_bot {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] :

⊥.prod ⊥ = ⊥

source

theorem AddSubsemigroup.bot_prod_bot {M : Type u_1} {N : Type u_2} [Add M] [Add N] :

⊥.prod ⊥ = ⊥

source

def Subsemigroup.prodEquiv {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup M) (t : Subsemigroup N) :

↥(s.prod t) ≃* ↥s × ↥t

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

Equations

s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_mul' := ⋯ }

Instances For

source

def AddSubsemigroup.prodEquiv {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :

↥(s.prod t) ≃+ ↥s × ↥t

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

Equations

s.prodEquiv t = { toEquiv := Equiv.Set.prod ↑s ↑t, map_add' := ⋯ }

Instances For

source

theorem Subsemigroup.mem_map_equiv {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M ≃* N} {K : Subsemigroup M} {x : N} :

x ∈ Subsemigroup.map (↑f) K ↔ f.symm x ∈ K

source

theorem AddSubsemigroup.mem_map_equiv {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M ≃+ N} {K : AddSubsemigroup M} {x : N} :

x ∈ AddSubsemigroup.map (↑f) K ↔ f.symm x ∈ K

source

theorem Subsemigroup.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M ≃* N) (K : Subsemigroup M) :

Subsemigroup.map (↑f) K = Subsemigroup.comap (↑f.symm) K

source

theorem AddSubsemigroup.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M ≃+ N) (K : AddSubsemigroup M) :

AddSubsemigroup.map (↑f) K = AddSubsemigroup.comap (↑f.symm) K

source

theorem Subsemigroup.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : N ≃* M) (K : Subsemigroup M) :

Subsemigroup.comap (↑f) K = Subsemigroup.map (↑f.symm) K

source

theorem AddSubsemigroup.comap_equiv_eq_map_symm {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : N ≃+ M) (K : AddSubsemigroup M) :

AddSubsemigroup.comap (↑f) K = AddSubsemigroup.map (↑f.symm) K

source

@[simp]

theorem Subsemigroup.map_equiv_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M ≃* N) :

Subsemigroup.map ↑f ⊤ = ⊤

source

@[simp]

theorem AddSubsemigroup.map_equiv_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M ≃+ N) :

AddSubsemigroup.map ↑f ⊤ = ⊤

source

theorem Subsemigroup.le_prod_iff {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {s : Subsemigroup M} {t : Subsemigroup N} {u : Subsemigroup (M × N)} :

u ≤ s.prod t ↔ Subsemigroup.map (MulHom.fst M N) u ≤ s ∧ Subsemigroup.map (MulHom.snd M N) u ≤ t

source

theorem AddSubsemigroup.le_prod_iff {M : Type u_1} {N : Type u_2} [Add M] [Add N] {s : AddSubsemigroup M} {t : AddSubsemigroup N} {u : AddSubsemigroup (M × N)} :

u ≤ s.prod t ↔ AddSubsemigroup.map (AddHom.fst M N) u ≤ s ∧ AddSubsemigroup.map (AddHom.snd M N) u ≤ t

source

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

Subsemigroup N

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

Equations

f.srange = (Subsemigroup.map f ⊤).copy (Set.range ⇑f) ⋯

Instances For

source

def AddHom.srange {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :

AddSubsemigroup N

The range of an AddHom is an AddSubsemigroup.

Equations

f.srange = (AddSubsemigroup.map f ⊤).copy (Set.range ⇑f) ⋯

Instances For

source

@[simp]

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

↑f.srange = Set.range ⇑f

source

@[simp]

theorem AddHom.coe_srange {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :

↑f.srange = Set.range ⇑f

source

@[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

source

@[simp]

theorem AddHom.mem_srange {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : M →ₙ+ N} {y : N} :

y ∈ f.srange ↔ ∃ (x : M), f x = y

source

@[simp]

theorem MulHom.srange_mk {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M → N) (hf : ∀ (x y : M), f (x * y) = f x * f y) :

{ toFun := f, map_mul' := hf }.srange = { carrier := Set.range f, mul_mem' := ⋯ }

source

@[simp]

theorem AddHom.srange_mk {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M → N) (hf : ∀ (x y : M), f (x + y) = f x + f y) :

{ toFun := f, map_add' := hf }.srange = { carrier := Set.range f, add_mem' := ⋯ }

source

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

f.srange = Subsemigroup.map f ⊤

source

theorem AddHom.srange_eq_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :

f.srange = AddSubsemigroup.map f ⊤

source

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

source

theorem AddHom.map_srange {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [Add P] (g : N →ₙ+ P) (f : M →ₙ+ N) :

AddSubsemigroup.map g f.srange = (g.comp f).srange

source

theorem MulHom.srange_eq_top_iff_surjective {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] {f : M →ₙ* N} :

f.srange = ⊤ ↔ Function.Surjective ⇑f

source

theorem AddHom.srange_eq_top_iff_surjective {M : Type u_1} [Add M] {N : Type u_5} [Add N] {f : M →ₙ+ N} :

f.srange = ⊤ ↔ Function.Surjective ⇑f

source

@[deprecated MulHom.srange_eq_top_iff_surjective (since := "2024-11-11")]

theorem MulHom.srange_top_iff_surjective {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] {f : M →ₙ* N} :

f.srange = ⊤ ↔ Function.Surjective ⇑f

Alias of MulHom.srange_eq_top_iff_surjective.

source

@[simp]

theorem MulHom.srange_eq_top_of_surjective {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] (f : M →ₙ* N) (hf : Function.Surjective ⇑f) :

f.srange = ⊤

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

source

@[simp]

theorem AddHom.srange_eq_top_of_surjective {M : Type u_1} [Add M] {N : Type u_5} [Add N] (f : M →ₙ+ N) (hf : Function.Surjective ⇑f) :

f.srange = ⊤

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

source

@[deprecated MulHom.srange_eq_top_of_surjective (since := "2024-11-11")]

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

f.srange = ⊤

Alias of MulHom.srange_eq_top_of_surjective.

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

source

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

Subsemigroup.closure (⇑f ⁻¹' s) ≤ Subsemigroup.comap f (Subsemigroup.closure s)

source

theorem AddHom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (s : Set N) :

AddSubsemigroup.closure (⇑f ⁻¹' s) ≤ AddSubsemigroup.comap f (AddSubsemigroup.closure s)

source

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

Subsemigroup.map f (Subsemigroup.closure s) = Subsemigroup.closure (⇑f '' s)

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

source

theorem AddHom.map_mclosure {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (s : Set M) :

AddSubsemigroup.map f (AddSubsemigroup.closure s) = AddSubsemigroup.closure (⇑f '' s)

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

source

def MulHom.restrict {M : Type u_1} {σ : Type u_4} [Mul M] {N : Type u_5} [Mul N] [SetLike σ M] [MulMemClass σ M] (f : M →ₙ* N) (S : σ) :

↥S →ₙ* N

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

Equations

f.restrict S = f.comp (MulMemClass.subtype S)

Instances For

source

def AddHom.restrict {M : Type u_1} {σ : Type u_4} [Add M] {N : Type u_5} [Add N] [SetLike σ M] [AddMemClass σ M] (f : M →ₙ+ N) (S : σ) :

↥S →ₙ+ N

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

Equations

f.restrict S = f.comp (AddMemClass.subtype S)

Instances For

source

@[simp]

theorem MulHom.restrict_apply {M : Type u_1} {σ : Type u_4} [Mul M] {N : Type u_5} [Mul N] [SetLike σ M] [MulMemClass σ M] (f : M →ₙ* N) {S : σ} (x : ↥S) :

(f.restrict S) x = f ↑x

source

@[simp]

theorem AddHom.restrict_apply {M : Type u_1} {σ : Type u_4} [Add M] {N : Type u_5} [Add N] [SetLike σ M] [AddMemClass σ M] (f : M →ₙ+ N) {S : σ} (x : ↥S) :

(f.restrict S) x = f ↑x

source

def MulHom.codRestrict {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Mul M] [Mul N] [SetLike σ N] [MulMemClass σ 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

source

def AddHom.codRestrict {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Add M] [Add N] [SetLike σ N] [AddMemClass σ N] (f : M →ₙ+ N) (S : σ) (h : ∀ (x : M), f x ∈ S) :

M →ₙ+ ↥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

source

@[simp]

theorem MulHom.codRestrict_apply_coe {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Mul M] [Mul N] [SetLike σ N] [MulMemClass σ N] (f : M →ₙ* N) (S : σ) (h : ∀ (x : M), f x ∈ S) (n : M) :

↑((f.codRestrict S h) n) = f n

source

@[simp]

theorem AddHom.codRestrict_apply_coe {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Add M] [Add N] [SetLike σ N] [AddMemClass σ N] (f : M →ₙ+ N) (S : σ) (h : ∀ (x : M), f x ∈ S) (n : M) :

↑((f.codRestrict S h) n) = f n

source

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

source

def AddHom.srangeRestrict {M : Type u_1} [Add M] {N : Type u_5} [Add N] (f : M →ₙ+ N) :

M →ₙ+ ↥f.srange

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

Equations

f.srangeRestrict = f.codRestrict f.srange ⋯

Instances For

source

@[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

source

@[simp]

theorem AddHom.coe_srangeRestrict {M : Type u_1} [Add M] {N : Type u_5} [Add N] (f : M →ₙ+ N) (x : M) :

↑(f.srangeRestrict x) = f x

source

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

Function.Surjective ⇑f.srangeRestrict

source

theorem AddHom.srangeRestrict_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) :

Function.Surjective ⇑f.srangeRestrict

source

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 : Subsemigroup N) (S' : Subsemigroup N') :

Subsemigroup.comap (f.prodMap g) (S.prod S') = (Subsemigroup.comap f S).prod (Subsemigroup.comap g S')

source

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 : M →ₙ+ N) (g : M' →ₙ+ N') (S : AddSubsemigroup N) (S' : AddSubsemigroup N') :

AddSubsemigroup.comap (f.prodMap g) (S.prod S') = (AddSubsemigroup.comap f S).prod (AddSubsemigroup.comap g S')

source

def MulHom.subsemigroupComap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (N' : Subsemigroup N) :

↥(Subsemigroup.comap f N') →ₙ* ↥N'

The MulHom from the preimage of a subsemigroup to itself.

Equations

f.subsemigroupComap N' = { toFun := fun (x : ↥(Subsemigroup.comap f N')) => ⟨f ↑x, ⋯⟩, map_mul' := ⋯ }

Instances For

source

def AddHom.subsemigroupComap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (N' : AddSubsemigroup N) :

↥(AddSubsemigroup.comap f N') →ₙ+ ↥N'

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

Equations

f.subsemigroupComap N' = { toFun := fun (x : ↥(AddSubsemigroup.comap f N')) => ⟨f ↑x, ⋯⟩, map_add' := ⋯ }

Instances For

source

@[simp]

theorem AddHom.subsemigroupComap_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (N' : AddSubsemigroup N) (x : ↥(AddSubsemigroup.comap f N')) :

↑((f.subsemigroupComap N') x) = f ↑x

source

@[simp]

theorem MulHom.subsemigroupComap_apply_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (N' : Subsemigroup N) (x : ↥(Subsemigroup.comap f N')) :

↑((f.subsemigroupComap N') x) = f ↑x

source

def MulHom.subsemigroupMap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (M' : Subsemigroup M) :

↥M' →ₙ* ↥(Subsemigroup.map f 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

source

def AddHom.subsemigroupMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (M' : AddSubsemigroup M) :

↥M' →ₙ+ ↥(AddSubsemigroup.map f 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

source

@[simp]

theorem AddHom.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (M' : AddSubsemigroup M) (x : ↥M') :

↑((f.subsemigroupMap M') x) = f ↑x

source

@[simp]

theorem MulHom.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (M' : Subsemigroup M) (x : ↥M') :

↑((f.subsemigroupMap M') x) = f ↑x

source

theorem MulHom.subsemigroupMap_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (M' : Subsemigroup M) :

Function.Surjective ⇑(f.subsemigroupMap M')

source

theorem AddHom.subsemigroupMap_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (M' : AddSubsemigroup M) :

Function.Surjective ⇑(f.subsemigroupMap M')

source

@[simp]

theorem Subsemigroup.srange_fst {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] [Nonempty N] :

(MulHom.fst M N).srange = ⊤

source

@[simp]

theorem AddSubsemigroup.srange_fst {M : Type u_1} {N : Type u_2} [Add M] [Add N] [Nonempty N] :

(AddHom.fst M N).srange = ⊤

source

@[simp]

theorem Subsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] [Nonempty M] :

(MulHom.snd M N).srange = ⊤

source

@[simp]

theorem AddSubsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [Add M] [Add N] [Nonempty M] :

(AddHom.snd M N).srange = ⊤

source

theorem Subsemigroup.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] [Nonempty M] [Nonempty N] {s : Subsemigroup M} {t : Subsemigroup N} :

s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

source

theorem AddSubsemigroup.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [Add M] [Add N] [Nonempty M] [Nonempty N] {s : AddSubsemigroup M} {t : AddSubsemigroup N} :

s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤

source

def Subsemigroup.inclusion {M : Type u_1} [Mul M] {S T : Subsemigroup M} (h : S ≤ T) :

↥S →ₙ* ↥T

The semigroup hom associated to an inclusion of subsemigroups.

Equations

Subsemigroup.inclusion h = (MulMemClass.subtype S).codRestrict T ⋯

Instances For

source

def AddSubsemigroup.inclusion {M : Type u_1} [Add M] {S T : AddSubsemigroup M} (h : S ≤ T) :

↥S →ₙ+ ↥T

The AddSemigroup hom associated to an inclusion of subsemigroups.

Equations

AddSubsemigroup.inclusion h = (AddMemClass.subtype S).codRestrict T ⋯

Instances For

source

@[simp]

theorem Subsemigroup.range_subtype {M : Type u_1} [Mul M] (s : Subsemigroup M) :

(MulMemClass.subtype s).srange = s

source

@[simp]

theorem AddSubsemigroup.range_subtype {M : Type u_1} [Add M] (s : AddSubsemigroup M) :

(AddMemClass.subtype s).srange = s

source

theorem Subsemigroup.eq_top_iff' {M : Type u_1} [Mul M] (S : Subsemigroup M) :

S = ⊤ ↔ ∀ (x : M), x ∈ S

source

theorem AddSubsemigroup.eq_top_iff' {M : Type u_1} [Add M] (S : AddSubsemigroup M) :

S = ⊤ ↔ ∀ (x : M), x ∈ S

source

def MulEquiv.subsemigroupCongr {M : Type u_1} [Mul M] {S T : Subsemigroup M} (h : S = T) :

↥S ≃* ↥T

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

Equations

MulEquiv.subsemigroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯ }

Instances For

source

def AddEquiv.subsemigroupCongr {M : Type u_1} [Add M] {S T : AddSubsemigroup M} (h : S = T) :

↥S ≃+ ↥T

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

Equations

AddEquiv.subsemigroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_add' := ⋯ }

Instances For

source

def MulEquiv.ofLeftInverse {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) {g : N → M} (h : Function.LeftInverse g ⇑f) :

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

MulEquiv.ofLeftInverse f h = { toFun := ⇑f.srangeRestrict, invFun := g ∘ ⇑(MulMemClass.subtype f.srange), left_inv := h, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source

def AddEquiv.ofLeftInverse {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) {g : N → M} (h : Function.LeftInverse g ⇑f) :

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

AddEquiv.ofLeftInverse f h = { toFun := ⇑f.srangeRestrict, invFun := g ∘ ⇑(AddMemClass.subtype f.srange), left_inv := h, right_inv := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem AddEquiv.ofLeftInverse_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) {g : N → M} (h : Function.LeftInverse g ⇑f) (a : M) :

(AddEquiv.ofLeftInverse f h) a = f.srangeRestrict a

source

@[simp]

theorem MulEquiv.ofLeftInverse_symm_apply {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) {g : N → M} (h : Function.LeftInverse g ⇑f) (a✝ : ↥f.srange) :

(MulEquiv.ofLeftInverse f h).symm a✝ = g ↑a✝

source

@[simp]

theorem AddEquiv.ofLeftInverse_symm_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) {g : N → M} (h : Function.LeftInverse g ⇑f) (a✝ : ↥f.srange) :

(AddEquiv.ofLeftInverse f h).symm a✝ = g ↑a✝

source

@[simp]

theorem MulEquiv.ofLeftInverse_apply {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) {g : N → M} (h : Function.LeftInverse g ⇑f) (a : M) :

(MulEquiv.ofLeftInverse f h) a = f.srangeRestrict a

source

def MulEquiv.subsemigroupMap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (e : M ≃* N) (S : Subsemigroup M) :

↥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

e.subsemigroupMap S = { toFun := fun (x : ↥S) => ⟨e ↑x, ⋯⟩, invFun := fun (x : ↥(Subsemigroup.map (↑e) S)) => ⟨e.symm ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source

def AddEquiv.subsemigroupMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) :

↥S ≃+ ↥(AddSubsemigroup.map (↑e) 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

e.subsemigroupMap S = { toFun := fun (x : ↥S) => ⟨e ↑x, ⋯⟩, invFun := fun (x : ↥(AddSubsemigroup.map (↑e) S)) => ⟨e.symm ↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }