Documentation

Mathlib.GroupTheory.Subsemigroup.Operations

Operations on Subsemigroups #

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

Main definitions #

Conversion between multiplicative and additive definitions #

(Commutative) semigroup structure on a subsemigroup #

Operations on subsemigroups #

Semigroup homomorphisms between subsemigroups #

Operations on MulHoms #

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
@[simp]
theorem Subsemigroup.toAddSubsemigroup_apply_coe {M : Type u_1} [Mul M] (S : Subsemigroup M) :
↑(Subsemigroup.toAddSubsemigroup S) = ⇑Additive.toMul ⁻¹' ↑S
source
@[simp]
theorem Subsemigroup.toAddSubsemigroup_symm_apply_coe {M : Type u_1} [Mul M] (S : AddSubsemigroup (Additive M)) :
↑((RelIso.symm Subsemigroup.toAddSubsemigroup) S) = ⇑Additive.ofMul ⁻¹' ↑S
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.
source
@[inline, reducible]
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' = OrderIso.symm Subsemigroup.toAddSubsemigroup
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
@[simp]
theorem AddSubsemigroup.toSubsemigroup_apply_coe {A : Type u_5} [Add A] (S : AddSubsemigroup A) :
↑(AddSubsemigroup.toSubsemigroup S) = ⇑Multiplicative.toAdd ⁻¹' ↑S
source
@[simp]
theorem AddSubsemigroup.toSubsemigroup_symm_apply_coe {A : Type u_5} [Add A] (S : Subsemigroup (Multiplicative A)) :
↑((RelIso.symm AddSubsemigroup.toSubsemigroup) S) = ⇑Multiplicative.ofAdd ⁻¹' ↑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.
source
@[inline, reducible]
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' = OrderIso.symm AddSubsemigroup.toSubsemigroup
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
theorem AddSubsemigroup.comap.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : AddSubsemigroup N) :
∀ {a b : M}, a ∈ ⇑f ⁻¹' ↑S → b ∈ ⇑f ⁻¹' ↑S → f (a + b) ∈ S
source
def AddSubsemigroup.comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : AddSubsemigroup N) :
AddSubsemigroup M

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

Equations
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
source
@[simp]
theorem AddSubsemigroup.coe_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup N) (f : AddHom M N) :
↑(AddSubsemigroup.comap f S) = ⇑f ⁻¹' ↑S
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.mem_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {S : AddSubsemigroup N} {f : AddHom M N} {x : M} :
x ∈ AddSubsemigroup.comap f S ↔ f x ∈ 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
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 : AddHom N P) (f : AddHom M N) :
AddSubsemigroup.comap f (AddSubsemigroup.comap g S) = AddSubsemigroup.comap (AddHom.comp g f) 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 (MulHom.comp g f) S
source
@[simp]
theorem AddSubsemigroup.comap_id {P : Type u_3} [Add P] (S : AddSubsemigroup P) :
AddSubsemigroup.comap (AddHom.id P) S = S
source
@[simp]
theorem Subsemigroup.comap_id {P : Type u_3} [Mul P] (S : Subsemigroup P) :
Subsemigroup.comap (MulHom.id P) S = S
source
theorem AddSubsemigroup.map.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (S : AddSubsemigroup M) :
∀ {a b : N}, a ∈ ⇑f '' ↑S → b ∈ ⇑f '' ↑S → a + b ∈ ⇑f '' ↑S
source
def AddSubsemigroup.map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : AddSubsemigroup M) :
AddSubsemigroup N

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

Equations
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
source
@[simp]
theorem AddSubsemigroup.coe_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : AddSubsemigroup M) :
↑(AddSubsemigroup.map f S) = ⇑f '' ↑S
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.mem_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {S : AddSubsemigroup M} {y : N} :
y ∈ AddSubsemigroup.map f S ↔ ∃ x ∈ S, f x = y
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
theorem AddSubsemigroup.mem_map_of_mem {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) {S : AddSubsemigroup M} {x : M} (hx : x ∈ S) :
f x ∈ AddSubsemigroup.map f S
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.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (S : AddSubsemigroup M) (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.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [Add P] (S : AddSubsemigroup M) (g : AddHom N P) (f : AddHom M N) :
AddSubsemigroup.map g (AddSubsemigroup.map f S) = AddSubsemigroup.map (AddHom.comp g 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 (MulHom.comp g f) S
source
@[simp]
theorem AddSubsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Injective ⇑f) {S : AddSubsemigroup M} {x : M} :
f x ∈ AddSubsemigroup.map f S ↔ x ∈ 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
theorem AddSubsemigroup.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {S : AddSubsemigroup M} {T : AddSubsemigroup N} :
AddSubsemigroup.map f S ≤ T ↔ S ≤ AddSubsemigroup.comap f T
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.gc_map_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
GaloisConnection (AddSubsemigroup.map f) (AddSubsemigroup.comap f)
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.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) {T : AddSubsemigroup N} {f : AddHom M N} :
S ≤ AddSubsemigroup.comap f T → AddSubsemigroup.map f S ≤ T
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.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) {T : AddSubsemigroup N} {f : AddHom M N} :
AddSubsemigroup.map f S ≤ T → S ≤ AddSubsemigroup.comap f 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_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) {f : AddHom M N} :
S ≤ AddSubsemigroup.comap f (AddSubsemigroup.map f S)
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.map_comap_le {M : Type u_1} {N : Type u_2} [Add M] [Add N] {S : AddSubsemigroup N} {f : AddHom M N} :
AddSubsemigroup.map f (AddSubsemigroup.comap f S) ≤ 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.monotone_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} :
Monotone (AddSubsemigroup.map f)
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_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} :
Monotone (AddSubsemigroup.comap 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
@[simp]
theorem AddSubsemigroup.map_comap_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) {f : AddHom M N} :
AddSubsemigroup.map f (AddSubsemigroup.comap f (AddSubsemigroup.map f S)) = AddSubsemigroup.map f S
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.comap_map_comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {S : AddSubsemigroup N} {f : AddHom M N} :
AddSubsemigroup.comap f (AddSubsemigroup.map f (AddSubsemigroup.comap f S)) = AddSubsemigroup.comap 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
theorem AddSubsemigroup.map_sup {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) (T : AddSubsemigroup M) (f : AddHom M N) :
AddSubsemigroup.map f (S ⊔ T) = AddSubsemigroup.map f S ⊔ AddSubsemigroup.map f T
source
theorem Subsemigroup.map_sup {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup M) (T : Subsemigroup M) (f : M →ₙ* N) :
Subsemigroup.map f (S ⊔ T) = Subsemigroup.map f S ⊔ Subsemigroup.map f T
source
theorem AddSubsemigroup.map_iSup {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Sort u_5} (f : AddHom M N) (s : ι → AddSubsemigroup M) :
AddSubsemigroup.map f (iSup s) = ⨆ (i : ι), AddSubsemigroup.map f (s i)
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.comap_inf {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup N) (T : AddSubsemigroup N) (f : AddHom M N) :
AddSubsemigroup.comap f (S ⊓ T) = AddSubsemigroup.comap f S ⊓ AddSubsemigroup.comap f T
source
theorem Subsemigroup.comap_inf {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (S : Subsemigroup N) (T : Subsemigroup N) (f : M →ₙ* N) :
Subsemigroup.comap f (S ⊓ T) = Subsemigroup.comap f S ⊓ Subsemigroup.comap f T
source
theorem AddSubsemigroup.comap_iInf {M : Type u_1} {N : Type u_2} [Add M] [Add N] {ι : Sort u_5} (f : AddHom M N) (s : ι → AddSubsemigroup N) :
AddSubsemigroup.comap f (iInf s) = ⨅ (i : ι), AddSubsemigroup.comap f (s i)
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
@[simp]
theorem AddSubsemigroup.map_bot {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
AddSubsemigroup.map f ⊥ = ⊥
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.comap_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
AddSubsemigroup.comap 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
abbrev AddSubsemigroup.map_id.match_1 {M : Type u_1} [Add M] (S : AddSubsemigroup M) :
∀ (x : M) (motive : x ∈ AddSubsemigroup.map (AddHom.id M) S → Prop) (x_1 : x ∈ AddSubsemigroup.map (AddHom.id M) S), (∀ (h : x ∈ ↑S), motive ⋯) → motive x_1
Equations
  • ⋯ = ⋯
source
@[simp]
theorem AddSubsemigroup.map_id {M : Type u_1} [Add M] (S : AddSubsemigroup M) :
AddSubsemigroup.map (AddHom.id M) S = S
source
@[simp]
theorem Subsemigroup.map_id {M : Type u_1} [Mul M] (S : Subsemigroup M) :
Subsemigroup.map (MulHom.id M) S = S
source
theorem AddSubsemigroup.gciMapComap.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Injective ⇑f) (S : AddSubsemigroup M) (x : M) :
x ∈ AddSubsemigroup.comap f (AddSubsemigroup.map f S) → x ∈ S
source
def AddSubsemigroup.gciMapComap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom 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
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
source
theorem AddSubsemigroup.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Injective ⇑f) (S : AddSubsemigroup M) :
AddSubsemigroup.comap f (AddSubsemigroup.map f S) = S
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_surjective_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Injective ⇑f) :
Function.Surjective (AddSubsemigroup.comap f)
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.map_injective_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Injective ⇑f) :
Function.Injective (AddSubsemigroup.map 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.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Injective ⇑f) (S : AddSubsemigroup M) (T : AddSubsemigroup M) :
AddSubsemigroup.comap f (AddSubsemigroup.map f S ⊓ AddSubsemigroup.map f T) = S ⊓ T
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 : Subsemigroup M) (T : Subsemigroup M) :
Subsemigroup.comap f (Subsemigroup.map f S ⊓ Subsemigroup.map f T) = S ⊓ T
source
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 : Function.Injective ⇑f) (S : ι → AddSubsemigroup M) :
AddSubsemigroup.comap f (⨅ (i : ι), AddSubsemigroup.map f (S i)) = iInf S
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_sup_map_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Injective ⇑f) (S : AddSubsemigroup M) (T : AddSubsemigroup M) :
AddSubsemigroup.comap f (AddSubsemigroup.map f S ⊔ AddSubsemigroup.map f T) = S ⊔ T
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 : Subsemigroup M) (T : Subsemigroup M) :
Subsemigroup.comap f (Subsemigroup.map f S ⊔ Subsemigroup.map f T) = S ⊔ T
source
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 : Function.Injective ⇑f) (S : ι → AddSubsemigroup M) :
AddSubsemigroup.comap f (⨆ (i : ι), AddSubsemigroup.map f (S i)) = iSup S
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.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Injective ⇑f) {S : AddSubsemigroup M} {T : AddSubsemigroup M} :
AddSubsemigroup.map f S ≤ AddSubsemigroup.map f T ↔ S ≤ T
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 : Subsemigroup M} {T : Subsemigroup M} :
Subsemigroup.map f S ≤ Subsemigroup.map f T ↔ S ≤ T
source
theorem AddSubsemigroup.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Injective ⇑f) :
StrictMono (AddSubsemigroup.map f)
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
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
  • ⋯ = ⋯
source
theorem AddSubsemigroup.giMapComap.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] {f : AddHom M N} (hf : Function.Surjective ⇑f) (S : AddSubsemigroup N) (x : N) (h : x ∈ S) :
x ∈ AddSubsemigroup.map f (AddSubsemigroup.comap f S)
source
def AddSubsemigroup.giMapComap {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom 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
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
source
theorem AddSubsemigroup.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Surjective ⇑f) (S : AddSubsemigroup N) :
AddSubsemigroup.map f (AddSubsemigroup.comap f S) = S
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_surjective_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Surjective ⇑f) :
Function.Surjective (AddSubsemigroup.map f)
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.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Surjective ⇑f) :
Function.Injective (AddSubsemigroup.comap 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.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Surjective ⇑f) (S : AddSubsemigroup N) (T : AddSubsemigroup N) :
AddSubsemigroup.map f (AddSubsemigroup.comap f S ⊓ AddSubsemigroup.comap f T) = S ⊓ T
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 : Subsemigroup N) (T : Subsemigroup N) :
Subsemigroup.map f (Subsemigroup.comap f S ⊓ Subsemigroup.comap f T) = S ⊓ T
source
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 : Function.Surjective ⇑f) (S : ι → AddSubsemigroup N) :
AddSubsemigroup.map f (⨅ (i : ι), AddSubsemigroup.comap f (S i)) = iInf S
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_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Surjective ⇑f) (S : AddSubsemigroup N) (T : AddSubsemigroup N) :
AddSubsemigroup.map f (AddSubsemigroup.comap f S ⊔ AddSubsemigroup.comap f T) = S ⊔ T
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 : Subsemigroup N) (T : Subsemigroup N) :
Subsemigroup.map f (Subsemigroup.comap f S ⊔ Subsemigroup.comap f T) = S ⊔ T
source
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 : Function.Surjective ⇑f) (S : ι → AddSubsemigroup N) :
AddSubsemigroup.map f (⨆ (i : ι), AddSubsemigroup.comap f (S i)) = iSup S
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.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Surjective ⇑f) {S : AddSubsemigroup N} {T : AddSubsemigroup N} :
AddSubsemigroup.comap f S ≤ AddSubsemigroup.comap f T ↔ S ≤ T
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 : Subsemigroup N} {T : Subsemigroup N} :
Subsemigroup.comap f S ≤ Subsemigroup.comap f T ↔ S ≤ T
source
theorem AddSubsemigroup.comap_strictMono_of_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} (hf : Function.Surjective ⇑f) :
StrictMono (AddSubsemigroup.comap f)
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
instance AddMemClass.add {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) :
Add ↥S'

An additive submagma of an additive magma inherits an addition.

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

A submagma of a magma inherits a multiplication.

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

An AddSubsemigroup of an AddSemigroup inherits an AddSemigroup structure.

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

A subsemigroup of a semigroup inherits a semigroup structure.

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

An AddSubsemigroup of an AddCommSemigroup is an AddCommSemigroup.

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

A subsemigroup of a CommSemigroup is a CommSemigroup.

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

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

Equations
source
theorem AddMemClass.subtype.proof_1 {M : Type u_1} {A : Type u_2} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) :
∀ (x x_1 : ↥S'), ↑(x + x_1) = ↑(x + x_1)
source
def MulMemClass.subtype {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) :
↥S' →ₙ* M

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

Equations
source
@[simp]
theorem AddMemClass.coe_subtype {M : Type u_1} {A : Type u_5} [Add M] [SetLike A M] [hA : AddMemClass A M] (S' : A) :
⇑(AddMemClass.subtype S') = Subtype.val
source
@[simp]
theorem MulMemClass.coe_subtype {M : Type u_1} {A : Type u_5} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A) :
⇑(MulMemClass.subtype S') = Subtype.val
source
theorem AddSubsemigroup.topEquiv.proof_3 {M : Type u_1} [Add M] :
∀ (x x_1 : ↥⊤), { toFun := fun (x : ↥⊤) => ↑x, invFun := fun (x : M) => { val := x, property := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1) = { toFun := fun (x : ↥⊤) => ↑x, invFun := fun (x : M) => { val := x, property := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1)
source
theorem AddSubsemigroup.topEquiv.proof_2 {M : Type u_1} [Add M] :
∀ (x : M), (fun (x : ↥⊤) => ↑x) ((fun (x : M) => { val := x, property := ⋯ }) x) = (fun (x : ↥⊤) => ↑x) ((fun (x : M) => { val := x, property := ⋯ }) x)
source
def AddSubsemigroup.topEquiv {M : Type u_1} [Add M] :
↥⊤ ≃+ M

The top additive subsemigroup is isomorphic to the additive semigroup.

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

The top subsemigroup is isomorphic to the semigroup.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem AddSubsemigroup.topEquiv_toAddHom {M : Type u_1} [Add M] :
↑AddSubsemigroup.topEquiv = AddMemClass.subtype ⊤
source
@[simp]
theorem Subsemigroup.topEquiv_toMulHom {M : Type u_1} [Mul M] :
↑Subsemigroup.topEquiv = MulMemClass.subtype ⊤
source
theorem AddSubsemigroup.equivMapOfInjective.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective ⇑f) :
∀ (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
source
noncomputable def AddSubsemigroup.equivMapOfInjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective ⇑f) :
↥S ≃+ ↥(AddSubsemigroup.map f S)

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

Equations
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
source
@[simp]
theorem AddSubsemigroup.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective ⇑f) (x : ↥S) :
↑((AddSubsemigroup.equivMapOfInjective S f hf) x) = f ↑x
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) :
↑((Subsemigroup.equivMapOfInjective S f hf) x) = f ↑x
source
@[simp]
theorem AddSubsemigroup.closure_closure_coe_preimage {M : Type u_1} [Add M] {s : Set M} :
AddSubsemigroup.closure (Subtype.val ⁻¹' s) = ⊤
source
@[simp]
theorem Subsemigroup.closure_closure_coe_preimage {M : Type u_1} [Mul M] {s : Set M} :
Subsemigroup.closure (Subtype.val ⁻¹' s) = ⊤
source
theorem AddSubsemigroup.prod.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
∀ {a b : M × N}, a ∈ ↑s ×ˢ ↑t → b ∈ ↑s ×ˢ ↑t → (a + b).1 ∈ ↑s ∧ (a + b).2 ∈ ↑t
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
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
source
theorem AddSubsemigroup.coe_prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
↑(AddSubsemigroup.prod s t) = ↑s ×ˢ ↑t
source
theorem Subsemigroup.coe_prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup M) (t : Subsemigroup N) :
↑(Subsemigroup.prod s t) = ↑s ×ˢ ↑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 ∈ AddSubsemigroup.prod s t ↔ p.1 ∈ s ∧ p.2 ∈ 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 ∈ Subsemigroup.prod s t ↔ p.1 ∈ s ∧ p.2 ∈ t
source
theorem AddSubsemigroup.prod_mono {M : Type u_1} {N : Type u_2} [Add M] [Add N] {s₁ : AddSubsemigroup M} {s₂ : AddSubsemigroup M} {t₁ : AddSubsemigroup N} {t₂ : AddSubsemigroup N} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :
AddSubsemigroup.prod s₁ t₁ ≤ AddSubsemigroup.prod s₂ t₂
source
theorem Subsemigroup.prod_mono {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {s₁ : Subsemigroup M} {s₂ : Subsemigroup M} {t₁ : Subsemigroup N} {t₂ : Subsemigroup N} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :
Subsemigroup.prod s₁ t₁ ≤ Subsemigroup.prod s₂ t₂
source
theorem AddSubsemigroup.prod_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) :
AddSubsemigroup.prod s ⊤ = AddSubsemigroup.comap (AddHom.fst M N) s
source
theorem Subsemigroup.prod_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup M) :
Subsemigroup.prod s ⊤ = Subsemigroup.comap (MulHom.fst M N) s
source
theorem AddSubsemigroup.top_prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup N) :
AddSubsemigroup.prod ⊤ s = AddSubsemigroup.comap (AddHom.snd M N) s
source
theorem Subsemigroup.top_prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup N) :
Subsemigroup.prod ⊤ s = Subsemigroup.comap (MulHom.snd M N) s
source
@[simp]
theorem AddSubsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [Add M] [Add N] :
AddSubsemigroup.prod ⊤ ⊤ = ⊤
source
@[simp]
theorem Subsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] :
Subsemigroup.prod ⊤ ⊤ = ⊤
source
theorem AddSubsemigroup.bot_prod_bot {M : Type u_1} {N : Type u_2} [Add M] [Add N] :
AddSubsemigroup.prod ⊥ ⊥ = ⊥
source
theorem Subsemigroup.bot_prod_bot {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] :
Subsemigroup.prod ⊥ ⊥ = ⊥
source
def AddSubsemigroup.prodEquiv {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
↥(AddSubsemigroup.prod s t) ≃+ ↥s × ↥t

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

Equations
source
theorem AddSubsemigroup.prodEquiv.proof_2 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (s : AddSubsemigroup M) (t : AddSubsemigroup N) :
∀ (x x_1 : ↥(AddSubsemigroup.prod s t)), (Equiv.Set.prod ↑s ↑t).toFun (x + x_1) = (Equiv.Set.prod ↑s ↑t).toFun (x + x_1)
source
theorem AddSubsemigroup.prodEquiv.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] :
AddMemClass (AddSubsemigroup (M × N)) (M × N)
source
def Subsemigroup.prodEquiv {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (s : Subsemigroup M) (t : Subsemigroup N) :
↥(Subsemigroup.prod s t) ≃* ↥s × ↥t

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

Equations
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 ↔ (AddEquiv.symm f) x ∈ K
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 ↔ (MulEquiv.symm f) x ∈ 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 (↑(AddEquiv.symm f)) 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 (↑(MulEquiv.symm f)) 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 (↑(AddEquiv.symm f)) 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 (↑(MulEquiv.symm f)) K
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
@[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
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 ≤ AddSubsemigroup.prod s t ↔ AddSubsemigroup.map (AddHom.fst M N) u ≤ s ∧ AddSubsemigroup.map (AddHom.snd M N) u ≤ t
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 ≤ Subsemigroup.prod s t ↔ Subsemigroup.map (MulHom.fst M N) u ≤ s ∧ Subsemigroup.map (MulHom.snd M N) u ≤ t
source
theorem AddHom.srange.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) :
Set.range ⇑f = ⇑f '' Set.univ
source
def AddHom.srange {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
AddSubsemigroup N

The range of an AddHom is an AddSubsemigroup.

Equations
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
source
@[simp]
theorem AddHom.coe_srange {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
↑(AddHom.srange f) = Set.range ⇑f
source
@[simp]
theorem MulHom.coe_srange {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
↑(MulHom.srange f) = Set.range ⇑f
source
@[simp]
theorem AddHom.mem_srange {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {y : N} :
y ∈ AddHom.srange f ↔ ∃ (x : M), f x = y
source
@[simp]
theorem MulHom.mem_srange {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {y : N} :
y ∈ MulHom.srange f ↔ ∃ (x : M), f x = y
source
theorem AddHom.srange_eq_map {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
AddHom.srange f = AddSubsemigroup.map f ⊤
source
theorem MulHom.srange_eq_map {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
MulHom.srange f = Subsemigroup.map f ⊤
source
theorem AddHom.map_srange {M : Type u_1} {N : Type u_2} {P : Type u_3} [Add M] [Add N] [Add P] (g : AddHom N P) (f : AddHom M N) :
AddSubsemigroup.map g (AddHom.srange f) = AddHom.srange (AddHom.comp g 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 (MulHom.srange f) = MulHom.srange (MulHom.comp g f)
source
theorem AddHom.srange_top_iff_surjective {M : Type u_1} [Add M] {N : Type u_5} [Add N] {f : AddHom M N} :
AddHom.srange f = ⊤ ↔ Function.Surjective ⇑f
source
theorem MulHom.srange_top_iff_surjective {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] {f : M →ₙ* N} :
MulHom.srange f = ⊤ ↔ Function.Surjective ⇑f
source
@[simp]
theorem AddHom.srange_top_of_surjective {M : Type u_1} [Add M] {N : Type u_5} [Add N] (f : AddHom M N) (hf : Function.Surjective ⇑f) :
AddHom.srange f = ⊤

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

source
@[simp]
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) :
MulHom.srange f = ⊤

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

source
theorem AddHom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (s : Set N) :
AddSubsemigroup.closure (⇑f ⁻¹' s) ≤ AddSubsemigroup.comap f (AddSubsemigroup.closure s)
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.map_mclosure {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom 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
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
def AddHom.restrict {M : Type u_1} {σ : Type u_4} [Add M] {N : Type u_5} [Add N] [SetLike σ M] [AddMemClass σ M] (f : AddHom M N) (S : σ) :
AddHom (↥S) N

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

Equations
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
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 : AddHom M N) {S : σ} (x : ↥S) :
(AddHom.restrict f S) x = f ↑x
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) :
(MulHom.restrict f S) x = f ↑x
source
theorem AddHom.codRestrict.proof_1 {M : Type u_3} {N : Type u_1} {σ : Type u_2} [Add M] [Add N] [SetLike σ N] [AddMemClass σ N] (f : AddHom M N) (S : σ) (h : ∀ (x : M), f x ∈ S) (x : M) (y : M) :
(fun (n : M) => { val := f n, property := ⋯ }) (x + y) = (fun (n : M) => { val := f n, property := ⋯ }) x + (fun (n : M) => { val := f n, property := ⋯ }) y
source
def AddHom.codRestrict {M : Type u_1} {N : Type u_2} {σ : Type u_4} [Add M] [Add N] [SetLike σ N] [AddMemClass σ N] (f : AddHom M N) (S : σ) (h : ∀ (x : M), f x ∈ S) :
AddHom M ↥S

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

Equations
  • AddHom.codRestrict f S h = { toFun := fun (n : M) => { val := f n, property := ⋯ }, map_add' := ⋯ }
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) :
↑((MulHom.codRestrict f 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 : AddHom M N) (S : σ) (h : ∀ (x : M), f x ∈ S) (n : M) :
↑((AddHom.codRestrict f S h) n) = f n
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
  • MulHom.codRestrict f S h = { toFun := fun (n : M) => { val := f n, property := ⋯ }, map_mul' := ⋯ }
source
def AddHom.srangeRestrict {M : Type u_1} [Add M] {N : Type u_5} [Add N] (f : AddHom M N) :
AddHom M ↥(AddHom.srange f)

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

Equations
source
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
source
def MulHom.srangeRestrict {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] (f : M →ₙ* N) :
M →ₙ* ↥(MulHom.srange f)

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

Equations
source
@[simp]
theorem AddHom.coe_srangeRestrict {M : Type u_1} [Add M] {N : Type u_5} [Add N] (f : AddHom M N) (x : M) :
↑((AddHom.srangeRestrict f) x) = f x
source
@[simp]
theorem MulHom.coe_srangeRestrict {M : Type u_1} [Mul M] {N : Type u_5} [Mul N] (f : M →ₙ* N) (x : M) :
↑((MulHom.srangeRestrict f) x) = f x
source
abbrev AddHom.srangeRestrict_surjective.match_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (motive : ↥(AddHom.srange f) → Prop) :
∀ (x : ↥(AddHom.srange f)), (∀ (x : M), motive { val := f x, property := ⋯ }) → motive x
Equations
  • ⋯ = ⋯
source
theorem AddHom.srangeRestrict_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) :
Function.Surjective ⇑(AddHom.srangeRestrict f)
source
theorem MulHom.srangeRestrict_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) :
Function.Surjective ⇑(MulHom.srangeRestrict f)
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 : AddHom M N) (g : AddHom M' N') (S : AddSubsemigroup N) (S' : AddSubsemigroup N') :
AddSubsemigroup.comap (AddHom.prodMap f g) (AddSubsemigroup.prod S S') = AddSubsemigroup.prod (AddSubsemigroup.comap f S) (AddSubsemigroup.comap g S')
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 (MulHom.prodMap f g) (Subsemigroup.prod S S') = Subsemigroup.prod (Subsemigroup.comap f S) (Subsemigroup.comap g S')
source
theorem AddHom.subsemigroupComap.proof_2 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (N' : AddSubsemigroup N) (x : ↥(AddSubsemigroup.comap f N')) (y : ↥(AddSubsemigroup.comap f N')) :
(fun (x : ↥(AddSubsemigroup.comap f N')) => { val := f ↑x, property := ⋯ }) (x + y) = (fun (x : ↥(AddSubsemigroup.comap f N')) => { val := f ↑x, property := ⋯ }) x + (fun (x : ↥(AddSubsemigroup.comap f N')) => { val := f ↑x, property := ⋯ }) y
source
def AddHom.subsemigroupComap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (N' : AddSubsemigroup N) :
AddHom ↥(AddSubsemigroup.comap f N') ↥N'

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

Equations
source
theorem AddHom.subsemigroupComap.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (N' : AddSubsemigroup N) (x : ↥(AddSubsemigroup.comap f N')) :
↑x ∈ AddSubsemigroup.comap f N'
source
@[simp]
theorem AddHom.subsemigroupComap_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (N' : AddSubsemigroup N) (x : ↥(AddSubsemigroup.comap f N')) :
↑((AddHom.subsemigroupComap f 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')) :
↑((MulHom.subsemigroupComap f N') x) = f ↑x
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
source
theorem AddHom.subsemigroupMap.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : AddSubsemigroup M) (x : ↥M') :
∃ a ∈ ↑M', f a = f ↑x
source
theorem AddHom.subsemigroupMap.proof_2 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : AddSubsemigroup M) (x : ↥M') (y : ↥M') :
(fun (x : ↥M') => { val := f ↑x, property := ⋯ }) (x + y) = (fun (x : ↥M') => { val := f ↑x, property := ⋯ }) x + (fun (x : ↥M') => { val := f ↑x, property := ⋯ }) y
source
def AddHom.subsemigroupMap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : AddSubsemigroup M) :
AddHom ↥M' ↥(AddSubsemigroup.map f M')

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

Equations
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') :
↑((MulHom.subsemigroupMap f M') x) = f ↑x
source
@[simp]
theorem AddHom.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : AddSubsemigroup M) (x : ↥M') :
↑((AddHom.subsemigroupMap f M') 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
source
theorem AddHom.subsemigroupMap_surjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (M' : AddSubsemigroup M) :
Function.Surjective ⇑(AddHom.subsemigroupMap f M')
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 ⇑(MulHom.subsemigroupMap f M')
source
@[simp]
theorem AddSubsemigroup.srange_fst {M : Type u_1} {N : Type u_2} [Add M] [Add N] [Nonempty N] :
AddHom.srange (AddHom.fst M N) = ⊤
source
@[simp]
theorem Subsemigroup.srange_fst {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] [Nonempty N] :
MulHom.srange (MulHom.fst M N) = ⊤
source
@[simp]
theorem AddSubsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [Add M] [Add N] [Nonempty M] :
AddHom.srange (AddHom.snd M N) = ⊤
source
@[simp]
theorem Subsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] [Nonempty M] :
MulHom.srange (MulHom.snd M N) = ⊤
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} :
AddSubsemigroup.prod s t = ⊤ ↔ s = ⊤ ∧ t = ⊤
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} :
Subsemigroup.prod s t = ⊤ ↔ s = ⊤ ∧ t = ⊤
source
def AddSubsemigroup.inclusion {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S ≤ T) :
AddHom ↥S ↥T

The AddSemigroup hom associated to an inclusion of subsemigroups.

Equations
source
theorem AddSubsemigroup.inclusion.proof_1 {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S ≤ T) (x : ↥S) :
(AddMemClass.subtype S) x ∈ T
source
def Subsemigroup.inclusion {M : Type u_1} [Mul M] {S : Subsemigroup M} {T : Subsemigroup M} (h : S ≤ T) :
↥S →ₙ* ↥T

The semigroup hom associated to an inclusion of subsemigroups.

Equations
source
@[simp]
theorem AddSubsemigroup.range_subtype {M : Type u_1} [Add M] (s : AddSubsemigroup M) :
AddHom.srange (AddMemClass.subtype s) = s
source
@[simp]
theorem Subsemigroup.range_subtype {M : Type u_1} [Mul M] (s : Subsemigroup M) :
MulHom.srange (MulMemClass.subtype s) = s
source
theorem AddSubsemigroup.eq_top_iff' {M : Type u_1} [Add M] (S : AddSubsemigroup M) :
S = ⊤ ↔ ∀ (x : M), x ∈ S
source
theorem Subsemigroup.eq_top_iff' {M : Type u_1} [Mul M] (S : Subsemigroup M) :
S = ⊤ ↔ ∀ (x : M), x ∈ S
source
def AddEquiv.subsemigroupCongr {M : Type u_1} [Add M] {S : AddSubsemigroup M} {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
source
theorem AddEquiv.subsemigroupCongr.proof_2 {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
∀ (x x_1 : ↥S), (Equiv.setCongr ⋯).toFun (x + x_1) = (Equiv.setCongr ⋯).toFun (x + x_1)
source
theorem AddEquiv.subsemigroupCongr.proof_1 {M : Type u_1} [Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S = T) :
↑S = ↑T
source
def MulEquiv.subsemigroupCongr {M : Type u_1} [Mul M] {S : Subsemigroup M} {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
source
abbrev AddEquiv.ofLeftInverse.match_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (x : ↥(AddHom.srange f)) (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
  • ⋯ = ⋯
source
def AddEquiv.ofLeftInverse {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) {g : N → M} (h : Function.LeftInverse g ⇑f) :
M ≃+ ↥(AddHom.srange f)

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
  • One or more equations did not get rendered due to their size.
source
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) :
(AddHom.srangeRestrict f).toFun (x + y) = (AddHom.srangeRestrict f).toFun x + (AddHom.srangeRestrict f).toFun y
source
theorem AddEquiv.ofLeftInverse.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) {g : N → M} (h : Function.LeftInverse g ⇑f) (x : ↥(AddHom.srange f)) :
(AddHom.srangeRestrict f) ((g ∘ ⇑(AddMemClass.subtype (AddHom.srange f))) x) = x
source
@[simp]
theorem AddEquiv.ofLeftInverse_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) {g : N → M} (h : Function.LeftInverse g ⇑f) (a : M) :
(AddEquiv.ofLeftInverse f h) a = (AddHom.srangeRestrict f) 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 : ↥(MulHom.srange f)), (MulEquiv.symm (MulEquiv.ofLeftInverse f h)) a = g ↑a
source
@[simp]
theorem AddEquiv.ofLeftInverse_symm_apply {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) {g : N → M} (h : Function.LeftInverse g ⇑f) :
∀ (a : ↥(AddHom.srange f)), (AddEquiv.symm (AddEquiv.ofLeftInverse f h)) 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 = (MulHom.srangeRestrict f) a
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 ≃* ↥(MulHom.srange f)

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
  • One or more equations did not get rendered due to their size.
source
theorem AddEquiv.subsemigroupMap.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] :
AddHomClass (M ≃+ N) M N
source
theorem AddEquiv.subsemigroupMap.proof_4 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) :
Function.LeftInverse (Equiv.image ↑e ↑S).invFun (Equiv.image ↑e ↑S).toFun
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
  • One or more equations did not get rendered due to their size.
source
theorem AddEquiv.subsemigroupMap.proof_5 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) :
Function.RightInverse (Equiv.image ↑e ↑S).invFun (Equiv.image ↑e ↑S).toFun
source
theorem AddEquiv.subsemigroupMap.proof_2 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : ↥S) :
↑e ↑x ∈ ⇑↑e '' ↑S
source
theorem AddEquiv.subsemigroupMap.proof_3 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : ↥(AddSubsemigroup.map (↑e) S)) :
(↑e).symm ↑x ∈ ↑S
source
theorem AddEquiv.subsemigroupMap.proof_6 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : ↥S) (y : ↥S) :
(AddHom.subsemigroupMap (↑e) S).toFun (x + y) = (AddHom.subsemigroupMap (↑e) S).toFun x + (AddHom.subsemigroupMap (↑e) S).toFun y
source
@[simp]
theorem MulEquiv.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (e : M ≃* N) (S : Subsemigroup M) (x : ↥S) :
↑((MulEquiv.subsemigroupMap e S) x) = e ↑x
source
@[simp]
theorem MulEquiv.subsemigroupMap_symm_apply_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (e : M ≃* N) (S : Subsemigroup M) (x : ↥(Subsemigroup.map (↑e) S)) :
↑((MulEquiv.symm (MulEquiv.subsemigroupMap e S)) x) = (MulEquiv.symm e) ↑x
source
@[simp]
theorem AddEquiv.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : ↥S) :
↑((AddEquiv.subsemigroupMap e S) x) = e ↑x
source
@[simp]
theorem AddEquiv.subsemigroupMap_symm_apply_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : ↥(AddSubsemigroup.map (↑e) S)) :
↑((AddEquiv.symm (AddEquiv.subsemigroupMap e S)) x) = (AddEquiv.symm e) ↑x
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
  • One or more equations did not get rendered due to their size.