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× 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≤ 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× t;

Operations on `mul_hom`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

ink

@[simp]

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

↑(↑(RelIso.toRelEmbedding Subsemigroup.toAddSubsemigroup).toEmbedding S) = ↑Additive.toMul ⁻¹' ↑S

source

ink

@[simp]

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

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

source

ink

def Subsemigroup.toAddSubsemigroup {M : Type u_1} [inst : 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

ink

@[inline]

abbrev AddSubsemigroup.toSubsemigroup' {M : Type u_1} [inst : 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

ink

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

↑(RelIso.toRelEmbedding Subsemigroup.toAddSubsemigroup).toEmbedding (Subsemigroup.closure S) = AddSubsemigroup.closure (↑Additive.toMul ⁻¹' S)

source

ink

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

↑(RelIso.toRelEmbedding AddSubsemigroup.toSubsemigroup').toEmbedding (AddSubsemigroup.closure S) = Subsemigroup.closure (↑Multiplicative.ofAdd ⁻¹' S)

source

ink

@[simp]

theorem AddSubsemigroup.toSubsemigroup_symm_apply_coe {A : Type u_1} [inst : Add A] (S : Subsemigroup (Multiplicative A)) :

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

source

ink

@[simp]

theorem AddSubsemigroup.toSubsemigroup_apply_coe {A : Type u_1} [inst : Add A] (S : AddSubsemigroup A) :

↑(↑(RelIso.toRelEmbedding AddSubsemigroup.toSubsemigroup).toEmbedding S) = ↑Multiplicative.toAdd ⁻¹' ↑S

source

ink

def AddSubsemigroup.toSubsemigroup {A : Type u_1} [inst : 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

ink

@[inline]

abbrev Subsemigroup.toAddSubsemigroup' {A : Type u_1} [inst : 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

ink

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

↑(RelIso.toRelEmbedding AddSubsemigroup.toSubsemigroup).toEmbedding (AddSubsemigroup.closure S) = Subsemigroup.closure (↑Multiplicative.toAdd ⁻¹' S)

source

ink

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

↑(RelIso.toRelEmbedding Subsemigroup.toAddSubsemigroup').toEmbedding (Subsemigroup.closure S) = AddSubsemigroup.closure (↑Additive.ofMul ⁻¹' S)

`comap` and `map` #

source

ink

def AddSubsemigroup.comap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom 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' := (_ : ∀ {a b : M}, a ∈ ↑f ⁻¹' ↑S → b ∈ ↑f ⁻¹' ↑S → ↑f (a + b) ∈ S) }

source

ink

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

∀ {a b : M}, a ∈ ↑f ⁻¹' ↑S → b ∈ ↑f ⁻¹' ↑S → ↑f (a + b) ∈ S

Equations

(_ : ↑f (a + b) ∈ S) = (_ : ↑f (a + b) ∈ S)

source

ink

def Subsemigroup.comap {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : 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' := (_ : ∀ {a b : M}, a ∈ ↑f ⁻¹' ↑S → b ∈ ↑f ⁻¹' ↑S → ↑f (a * b) ∈ S) }

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

theorem AddSubsemigroup.mem_comap {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {S : AddSubsemigroup N} {f : AddHom M N} {x : M} :

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

source

ink

@[simp]

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

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

source

ink

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

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

source

ink

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

def AddSubsemigroup.map {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom 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' := (_ : ∀ {a b : N}, a ∈ ↑f '' ↑S → b ∈ ↑f '' ↑S → a + b ∈ ↑f '' ↑S) }

source

ink

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

∀ {a b : N}, a ∈ ↑f '' ↑S → b ∈ ↑f '' ↑S → a + b ∈ ↑f '' ↑S

Equations

(_ : b ∈ ↑f '' ↑S → a + b ∈ ↑f '' ↑S) = (_ : b ∈ ↑f '' ↑S → a + b ∈ ↑f '' ↑S)

source

ink

def Subsemigroup.map {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : 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' := (_ : ∀ {a b : N}, a ∈ ↑f '' ↑S → b ∈ ↑f '' ↑S → a * b ∈ ↑f '' ↑S) }

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

theorem AddSubsemigroup.mem_map {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} {S : AddSubsemigroup M} {y : N} :

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

source

ink

@[simp]

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

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

source

ink

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

↑f x ∈ AddSubsemigroup.map f S

source

ink

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

↑f x ∈ Subsemigroup.map f S

source

ink

theorem AddSubsemigroup.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (S : AddSubsemigroup M) (x : { x // x ∈ S }) :

↑f ↑x ∈ AddSubsemigroup.map f S

source

ink

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

↑f ↑x ∈ Subsemigroup.map f S

source

ink

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

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective ↑f) {S : AddSubsemigroup M} {x : M} :

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} {S : AddSubsemigroup M} {T : AddSubsemigroup N} :

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.gc_map_comap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.map_comap_le {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {S : AddSubsemigroup N} {f : AddHom M N} :

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.monotone_map {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} :

Monotone (AddSubsemigroup.map f)

source

ink

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

Monotone (Subsemigroup.map f)

source

ink

theorem AddSubsemigroup.monotone_comap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} :

Monotone (AddSubsemigroup.comap f)

source

ink

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

Monotone (Subsemigroup.comap f)

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

theorem AddSubsemigroup.comap_map_comap {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {S : AddSubsemigroup N} {f : AddHom M N} :

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

source

ink

@[simp]

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

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

source

ink

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

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.map_supᵢ {M : Type u_2} {N : Type u_3} [inst : Add M] [inst : Add N] {ι : Sort u_1} (f : AddHom M N) (s : ι → AddSubsemigroup M) :

AddSubsemigroup.map f (supᵢ s) = ⨆ i, AddSubsemigroup.map f (s i)

source

ink

theorem Subsemigroup.map_supᵢ {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst : Mul N] {ι : Sort u_1} (f : M →ₙ* N) (s : ι → Subsemigroup M) :

Subsemigroup.map f (supᵢ s) = ⨆ i, Subsemigroup.map f (s i)

source

ink

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

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.comap_infᵢ {M : Type u_2} {N : Type u_3} [inst : Add M] [inst : Add N] {ι : Sort u_1} (f : AddHom M N) (s : ι → AddSubsemigroup N) :

AddSubsemigroup.comap f (infᵢ s) = ⨅ i, AddSubsemigroup.comap f (s i)

source

ink

theorem Subsemigroup.comap_infᵢ {M : Type u_2} {N : Type u_3} [inst : Mul M] [inst : Mul N] {ι : Sort u_1} (f : M →ₙ* N) (s : ι → Subsemigroup N) :

Subsemigroup.comap f (infᵢ s) = ⨅ i, Subsemigroup.comap f (s i)

source

ink

@[simp]

theorem AddSubsemigroup.map_bot {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :

AddSubsemigroup.map f ⊥ = ⊥

source

ink

@[simp]

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

Subsemigroup.map f ⊥ = ⊥

source

ink

@[simp]

theorem AddSubsemigroup.comap_top {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) :

AddSubsemigroup.comap f ⊤ = ⊤

source

ink

@[simp]

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

Subsemigroup.comap f ⊤ = ⊤

source

ink

abbrev AddSubsemigroup.map_id.match_1 {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M) :

(x : M) → ∀ (motive : x ∈ AddSubsemigroup.map (AddHom.id M) S → Prop) (x_1 : x ∈ AddSubsemigroup.map (AddHom.id M) S), (∀ (h : x ∈ ↑S), motive (_ : ∃ a, a ∈ ↑S ∧ ↑(AddHom.id M) a = x)) → motive x_1

Equations

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

def AddSubsemigroup.gciMapComap.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective ↑f) (S : AddSubsemigroup M) (x : M) :

x ∈ AddSubsemigroup.comap f (AddSubsemigroup.map f S) → x ∈ S

Equations

(_ : x ∈ AddSubsemigroup.comap f (AddSubsemigroup.map f S) → x ∈ S) = (_ : x ∈ AddSubsemigroup.comap f (AddSubsemigroup.map f S) → x ∈ S)

source

ink

def AddSubsemigroup.gciMapComap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective ↑f) :

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

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

Equations

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

source

ink

def Subsemigroup.gciMapComap {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : 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

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

source

ink

theorem AddSubsemigroup.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective ↑f) (S : AddSubsemigroup M) :

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.comap_surjective_of_injective {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective ↑f) :

Function.Surjective (AddSubsemigroup.comap f)

source

ink

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

Function.Surjective (Subsemigroup.comap f)

source

ink

theorem AddSubsemigroup.map_injective_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective ↑f) :

Function.Injective (AddSubsemigroup.map f)

source

ink

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

Function.Injective (Subsemigroup.map f)

source

ink

theorem AddSubsemigroup.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective ↑f) (S : AddSubsemigroup M) (T : AddSubsemigroup M) :

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.comap_infᵢ_map_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {ι : Type u_3} {f : AddHom M N} (hf : Function.Injective ↑f) (S : ι → AddSubsemigroup M) :

AddSubsemigroup.comap f (⨅ i, AddSubsemigroup.map f (S i)) = infᵢ S

source

ink

theorem Subsemigroup.comap_infᵢ_map_of_injective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {ι : Type u_3} {f : M →ₙ* N} (hf : Function.Injective ↑f) (S : ι → Subsemigroup M) :

Subsemigroup.comap f (⨅ i, Subsemigroup.map f (S i)) = infᵢ S

source

ink

theorem AddSubsemigroup.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective ↑f) (S : AddSubsemigroup M) (T : AddSubsemigroup M) :

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.comap_supᵢ_map_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {ι : Type u_3} {f : AddHom M N} (hf : Function.Injective ↑f) (S : ι → AddSubsemigroup M) :

AddSubsemigroup.comap f (⨆ i, AddSubsemigroup.map f (S i)) = supᵢ S

source

ink

theorem Subsemigroup.comap_supᵢ_map_of_injective {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {ι : Type u_3} {f : M →ₙ* N} (hf : Function.Injective ↑f) (S : ι → Subsemigroup M) :

Subsemigroup.comap f (⨆ i, Subsemigroup.map f (S i)) = supᵢ S

source

ink

theorem AddSubsemigroup.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective ↑f) {S : AddSubsemigroup M} {T : AddSubsemigroup M} :

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Injective ↑f) :

StrictMono (AddSubsemigroup.map f)

source

ink

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

StrictMono (Subsemigroup.map f)

source

ink

abbrev AddSubsemigroup.giMapComap.match_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (x : N) (motive : (∃ a, ↑f a = x) → Prop) :

(x : ∃ a, ↑f a = x) → ((y : M) → (hy : ↑f y = x) → motive (_ : ∃ a, ↑f a = x)) → motive x

Equations

AddSubsemigroup.giMapComap.match_1 x motive x h_1 = Exists.casesOn x fun w h => h_1 w h

source

ink

def AddSubsemigroup.giMapComap.proof_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Surjective ↑f) (S : AddSubsemigroup N) (x : N) (h : x ∈ S) :

x ∈ AddSubsemigroup.map f (AddSubsemigroup.comap f S)

Equations

(_ : x ∈ AddSubsemigroup.map f (AddSubsemigroup.comap f S)) = (_ : x ∈ AddSubsemigroup.map f (AddSubsemigroup.comap f S))

source

ink

def AddSubsemigroup.giMapComap {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Surjective ↑f) :

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

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

Equations

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

source

ink

def Subsemigroup.giMapComap {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : 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

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

source

ink

theorem AddSubsemigroup.map_comap_eq_of_surjective {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Surjective ↑f) (S : AddSubsemigroup N) :

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Surjective ↑f) :

Function.Surjective (AddSubsemigroup.map f)

source

ink

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

Function.Surjective (Subsemigroup.map f)

source

ink

theorem AddSubsemigroup.comap_injective_of_surjective {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Surjective ↑f) :

Function.Injective (AddSubsemigroup.comap f)

source

ink

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

Function.Injective (Subsemigroup.comap f)

source

ink

theorem AddSubsemigroup.map_inf_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Surjective ↑f) (S : AddSubsemigroup N) (T : AddSubsemigroup N) :

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.map_infᵢ_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {ι : Type u_3} {f : AddHom M N} (hf : Function.Surjective ↑f) (S : ι → AddSubsemigroup N) :

AddSubsemigroup.map f (⨅ i, AddSubsemigroup.comap f (S i)) = infᵢ S

source

ink

theorem Subsemigroup.map_infᵢ_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {ι : Type u_3} {f : M →ₙ* N} (hf : Function.Surjective ↑f) (S : ι → Subsemigroup N) :

Subsemigroup.map f (⨅ i, Subsemigroup.comap f (S i)) = infᵢ S

source

ink

theorem AddSubsemigroup.map_sup_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Surjective ↑f) (S : AddSubsemigroup N) (T : AddSubsemigroup N) :

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.map_supᵢ_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {ι : Type u_3} {f : AddHom M N} (hf : Function.Surjective ↑f) (S : ι → AddSubsemigroup N) :

AddSubsemigroup.map f (⨆ i, AddSubsemigroup.comap f (S i)) = supᵢ S

source

ink

theorem Subsemigroup.map_supᵢ_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst : Mul N] {ι : Type u_3} {f : M →ₙ* N} (hf : Function.Surjective ↑f) (S : ι → Subsemigroup N) :

Subsemigroup.map f (⨆ i, Subsemigroup.comap f (S i)) = supᵢ S

source

ink

theorem AddSubsemigroup.comap_le_comap_iff_of_surjective {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Surjective ↑f) {S : AddSubsemigroup N} {T : AddSubsemigroup N} :

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

source

ink

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

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

source

ink

theorem AddSubsemigroup.comap_strictMono_of_surjective {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] {f : AddHom M N} (hf : Function.Surjective ↑f) :

StrictMono (AddSubsemigroup.comap f)

source

ink

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

StrictMono (Subsemigroup.comap f)

source

ink

instance AddMemClass.add {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) :

Add { x // x ∈ S' }

An additive submagma of an additive magma inherits an addition.

Equations

AddMemClass.add S' = { add := fun a b => { val := ↑a + ↑b, property := (_ : ↑a + ↑b ∈ S') } }

source

ink

def AddMemClass.add.proof_1 {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) (a : { x // x ∈ S' }) (b : { x // x ∈ S' }) :

↑a + ↑b ∈ S'

Equations

(_ : ↑a + ↑b ∈ S') = (_ : ↑a + ↑b ∈ S')

source

ink

instance MulMemClass.mul {M : Type u_1} {A : Type u_2} [inst : Mul M] [inst : SetLike A M] [hA : MulMemClass A M] (S' : A) :

Mul { x // x ∈ S' }

A submagma of a magma inherits a multiplication.

Equations

MulMemClass.mul S' = { mul := fun a b => { val := ↑a * ↑b, property := (_ : ↑a * ↑b ∈ S') } }

source

ink

@[simp]

theorem AddMemClass.coe_add {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) (x : { x // x ∈ S' }) (y : { x // x ∈ S' }) :

↑(x + y) = ↑x + ↑y

source

ink

@[simp]

theorem MulMemClass.coe_mul {M : Type u_1} {A : Type u_2} [inst : Mul M] [inst : SetLike A M] [hA : MulMemClass A M] (S' : A) (x : { x // x ∈ S' }) (y : { x // x ∈ S' }) :

↑(x * y) = ↑x * ↑y

source

ink

@[simp]

theorem AddMemClass.mk_add_mk {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) (x : M) (y : M) (hx : x ∈ S') (hy : y ∈ S') :

{ val := x, property := hx } + { val := y, property := hy } = { val := x + y, property := (_ : x + y ∈ S') }

source

ink

@[simp]

theorem MulMemClass.mk_mul_mk {M : Type u_1} {A : Type u_2} [inst : Mul M] [inst : SetLike A M] [hA : MulMemClass A M] (S' : A) (x : M) (y : M) (hx : x ∈ S') (hy : y ∈ S') :

{ val := x, property := hx } * { val := y, property := hy } = { val := x * y, property := (_ : x * y ∈ S') }

source

ink

theorem AddMemClass.add_def {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) (x : { x // x ∈ S' }) (y : { x // x ∈ S' }) :

x + y = { val := ↑x + ↑y, property := (_ : ↑x + ↑y ∈ S') }

source

ink

theorem MulMemClass.mul_def {M : Type u_1} {A : Type u_2} [inst : Mul M] [inst : SetLike A M] [hA : MulMemClass A M] (S' : A) (x : { x // x ∈ S' }) (y : { x // x ∈ S' }) :

x * y = { val := ↑x * ↑y, property := (_ : ↑x * ↑y ∈ S') }

source

ink

def AddMemClass.toAddSemigroup.proof_2 {M : Type u_1} [inst : AddSemigroup M] {A : Type u_2} [inst : SetLike A M] [inst : AddMemClass A M] (S : A) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

source

ink

def AddMemClass.toAddSemigroup.proof_1 {M : Type u_1} {A : Type u_2} [inst : SetLike A M] (S : A) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

source

ink

instance AddMemClass.toAddSemigroup {M : Type u_1} [inst : AddSemigroup M] {A : Type u_2} [inst : SetLike A M] [inst : AddMemClass A M] (S : A) :

AddSemigroup { x // x ∈ S }

An AddSubsemigroup of an AddSemigroup inherits an AddSemigroup structure.

Equations

AddMemClass.toAddSemigroup S = Function.Injective.addSemigroup Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1))

source

ink

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

Semigroup { x // x ∈ S }

A subsemigroup of a semigroup inherits a semigroup structure.

Equations

MulMemClass.toSemigroup S = Function.Injective.semigroup Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ∀ (x x_1 : { x // x ∈ S }), ↑(x * x_1) = ↑(x * x_1))

source

ink

def AddMemClass.toAddCommSemigroup.proof_1 {M : Type u_1} {A : Type u_2} [inst : SetLike A M] (S : A) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

source

ink

instance AddMemClass.toAddCommSemigroup {M : Type u_1} [inst : AddCommSemigroup M] {A : Type u_2} [inst : SetLike A M] [inst : AddMemClass A M] (S : A) :

AddCommSemigroup { x // x ∈ S }

An AddSubsemigroup of an AddCommSemigroup is an AddCommSemigroup.

Equations

AddMemClass.toAddCommSemigroup S = Function.Injective.addCommSemigroup Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1))

source

ink

def AddMemClass.toAddCommSemigroup.proof_2 {M : Type u_1} [inst : AddCommSemigroup M] {A : Type u_2} [inst : SetLike A M] [inst : AddMemClass A M] (S : A) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

source

ink

instance MulMemClass.toCommSemigroup {M : Type u_1} [inst : CommSemigroup M] {A : Type u_2} [inst : SetLike A M] [inst : MulMemClass A M] (S : A) :

CommSemigroup { x // x ∈ S }

A subsemigroup of a CommSemigroup is a CommSemigroup.

Equations

MulMemClass.toCommSemigroup S = Function.Injective.commSemigroup Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ∀ (x x_1 : { x // x ∈ S }), ↑(x * x_1) = ↑(x * x_1))

source

ink

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

∀ (x x_1 : { x // x ∈ S' }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

source

ink

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

AddHom { x // x ∈ S' } M

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

Equations

AddMemClass.subtype S' = { toFun := Subtype.val, map_add' := (_ : ∀ (x x_1 : { x // x ∈ S' }), ↑(x + x_1) = ↑(x + x_1)) }

source

ink

def MulMemClass.subtype {M : Type u_1} {A : Type u_2} [inst : Mul M] [inst : SetLike A M] [hA : MulMemClass A M] (S' : A) :

{ x // x ∈ S' } →ₙ* M

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

Equations

MulMemClass.subtype S' = { toFun := Subtype.val, map_mul' := (_ : ∀ (x x_1 : { x // x ∈ S' }), ↑(x * x_1) = ↑(x * x_1)) }

source

ink

@[simp]

theorem AddMemClass.coe_subtype {M : Type u_1} {A : Type u_2} [inst : Add M] [inst : SetLike A M] [hA : AddMemClass A M] (S' : A) :

↑(AddMemClass.subtype S') = Subtype.val

source

ink

@[simp]

theorem MulMemClass.coe_subtype {M : Type u_1} {A : Type u_2} [inst : Mul M] [inst : SetLike A M] [hA : MulMemClass A M] (S' : A) :

↑(MulMemClass.subtype S') = Subtype.val

source

ink

def AddSubsemigroup.topEquiv.proof_1 {M : Type u_1} [inst : Add M] (x : { x // x ∈ ⊤ }) :

{ val := ↑x, property := (_ : (fun x => ↑x) x ∈ ⊤) } = x

Equations

(_ : { val := ↑x, property := (_ : (fun x => ↑x) x ∈ ⊤) } = x) = (_ : { val := ↑x, property := (_ : (fun x => ↑x) x ∈ ⊤) } = x)

source

ink

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

∀ (x x_1 : { x // x ∈ ⊤ }), Equiv.toFun { toFun := fun x => ↑x, invFun := fun x => { val := x, property := (_ : x ∈ ⊤) }, left_inv := (_ : ∀ (x : { x // x ∈ ⊤ }), { val := ↑x, property := (_ : (fun x => ↑x) x ∈ ⊤) } = x), right_inv := (_ : ∀ (x : M), (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x) = (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x)) } (x + x_1) = Equiv.toFun { toFun := fun x => ↑x, invFun := fun x => { val := x, property := (_ : x ∈ ⊤) }, left_inv := (_ : ∀ (x : { x // x ∈ ⊤ }), { val := ↑x, property := (_ : (fun x => ↑x) x ∈ ⊤) } = x), right_inv := (_ : ∀ (x : M), (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x) = (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x)) } (x + x_1)

Equations

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

source

ink

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

∀ (x : M), (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x) = (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x)

Equations

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

source

ink

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

{ x // x ∈ ⊤ } ≃+ M

The top additive subsemigroup is isomorphic to the additive semigroup.

Equations

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

source

ink

@[simp]

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

↑AddSubsemigroup.topEquiv x = ↑x

source

ink

@[simp]

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

↑Subsemigroup.topEquiv x = ↑x

source

ink

@[simp]

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

↑(↑(AddEquiv.symm AddSubsemigroup.topEquiv) x) = x

source

ink

@[simp]

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

↑(↑(MulEquiv.symm Subsemigroup.topEquiv) x) = x

source

ink

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

{ x // x ∈ ⊤ } ≃* M

The top subsemigroup is isomorphic to the semigroup.

Equations

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

source

ink

@[simp]

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

AddEquiv.toAddHom AddSubsemigroup.topEquiv = AddMemClass.subtype ⊤

source

ink

@[simp]

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

MulEquiv.toMulHom Subsemigroup.topEquiv = MulMemClass.subtype ⊤

source

ink

def AddSubsemigroup.equivMapOfInjective.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective ↑f) :

Function.LeftInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun

Equations

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

source

ink

def AddSubsemigroup.equivMapOfInjective.proof_3 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective ↑f) :

∀ (x x_1 : { x // x ∈ S }), Equiv.toFun { toFun := (Equiv.Set.image (↑f) (↑S) hf).toFun, invFun := (Equiv.Set.image (↑f) (↑S) hf).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.Set.image (↑f) (↑S) hf).toFun, invFun := (Equiv.Set.image (↑f) (↑S) hf).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun) } x + Equiv.toFun { toFun := (Equiv.Set.image (↑f) (↑S) hf).toFun, invFun := (Equiv.Set.image (↑f) (↑S) hf).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun) } x_1

Equations

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

source

ink

noncomputable def AddSubsemigroup.equivMapOfInjective {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective ↑f) :

{ x // x ∈ S } ≃+ { x // x ∈ AddSubsemigroup.map f S }

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

Equations

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

source

ink

def AddSubsemigroup.equivMapOfInjective.proof_2 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective ↑f) :

Function.RightInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun

Equations

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

source

ink

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

{ x // x ∈ S } ≃* { x // x ∈ Subsemigroup.map f S }

A subsemigroup is isomorphic to its image under an injective function

Equations

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

source

ink

@[simp]

theorem AddSubsemigroup.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (S : AddSubsemigroup M) (f : AddHom M N) (hf : Function.Injective ↑f) (x : { x // x ∈ S }) :

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

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

AddSubsemigroup (M × N)

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

Equations

AddSubsemigroup.prod s t = { carrier := ↑s ×ˢ ↑t, add_mem' := (_ : ∀ {a b : M × N}, a ∈ ↑s ×ˢ ↑t → b ∈ ↑s ×ˢ ↑t → (a + b).fst ∈ ↑s ∧ (a + b).snd ∈ ↑t) }

source

ink

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

∀ {a b : M × N}, a ∈ ↑s ×ˢ ↑t → b ∈ ↑s ×ˢ ↑t → (a + b).fst ∈ ↑s ∧ (a + b).snd ∈ ↑t

Equations

(_ : (a + b).fst ∈ ↑s ∧ (a + b).snd ∈ ↑t) = (_ : (a + b).fst ∈ ↑s ∧ (a + b).snd ∈ ↑t)

source

ink

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

Subsemigroup (M × N)

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

Equations

Subsemigroup.prod s t = { carrier := ↑s ×ˢ ↑t, mul_mem' := (_ : ∀ {a b : M × N}, a ∈ ↑s ×ˢ ↑t → b ∈ ↑s ×ˢ ↑t → (a * b).fst ∈ ↑s ∧ (a * b).snd ∈ ↑t) }

source

ink

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

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

source

ink

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

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

source

ink

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

p ∈ AddSubsemigroup.prod s t ↔ p.fst ∈ s ∧ p.snd ∈ t

source

ink

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

p ∈ Subsemigroup.prod s t ↔ p.fst ∈ s ∧ p.snd ∈ t

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

source

ink

@[simp]

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

AddSubsemigroup.prod ⊤ ⊤ = ⊤

source

ink

@[simp]

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

Subsemigroup.prod ⊤ ⊤ = ⊤

source

ink

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

AddSubsemigroup.prod ⊥ ⊥ = ⊥

source

ink

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

Subsemigroup.prod ⊥ ⊥ = ⊥

source

ink

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

Function.RightInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun

Equations

(_ : Function.RightInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun) = (_ : Function.RightInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun)

source

ink

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

Function.LeftInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun

Equations

(_ : Function.LeftInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun) = (_ : Function.LeftInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun)

source

ink

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

∀ (x x_1 : { x // x ∈ AddSubsemigroup.prod s t }), Equiv.toFun { toFun := (Equiv.Set.prod ↑s ↑t).toFun, invFun := (Equiv.Set.prod ↑s ↑t).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.Set.prod ↑s ↑t).toFun, invFun := (Equiv.Set.prod ↑s ↑t).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun) } (x + x_1)

Equations

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

source

ink

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

{ x // x ∈ AddSubsemigroup.prod s t } ≃+ { x // x ∈ s } × { x // x ∈ t }

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

Equations

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

source

ink

def AddSubsemigroup.prodEquiv.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] :

AddMemClass (AddSubsemigroup (M × N)) (M × N)

Equations

(_ : AddMemClass (AddSubsemigroup (M × N)) (M × N)) = (_ : AddMemClass (AddSubsemigroup (M × N)) (M × N))

source

ink

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

{ x // x ∈ Subsemigroup.prod s t } ≃* { x // x ∈ s } × { x // x ∈ t }

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

Equations

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

source

ink

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

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

source

ink

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

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

source

ink

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

AddSubsemigroup.map (AddEquiv.toAddHom f) K = AddSubsemigroup.comap (AddEquiv.toAddHom (AddEquiv.symm f)) K

source

ink

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

Subsemigroup.map (MulEquiv.toMulHom f) K = Subsemigroup.comap (MulEquiv.toMulHom (MulEquiv.symm f)) K

source

ink

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

AddSubsemigroup.comap (AddEquiv.toAddHom f) K = AddSubsemigroup.map (AddEquiv.toAddHom (AddEquiv.symm f)) K

source

ink

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

Subsemigroup.comap (MulEquiv.toMulHom f) K = Subsemigroup.map (MulEquiv.toMulHom (MulEquiv.symm f)) K

source

ink

@[simp]

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

AddSubsemigroup.map (AddEquiv.toAddHom f) ⊤ = ⊤

source

ink

@[simp]

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

Subsemigroup.map (MulEquiv.toMulHom f) ⊤ = ⊤

source

ink

theorem AddSubsemigroup.le_prod_iff {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : 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

ink

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

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

source

ink

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

AddSubsemigroup N

The range of an AddHom is an AddSubsemigroup.

Equations

AddHom.srange f = AddSubsemigroup.copy (AddSubsemigroup.map f ⊤) (Set.range ↑f) (_ : Set.range ↑f = ↑f '' Set.univ)

source

ink

def AddHom.srange.proof_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (f : AddHom M N) :

Set.range ↑f = ↑f '' Set.univ

Equations

(_ : Set.range ↑f = ↑f '' Set.univ) = (_ : Set.range ↑f = ↑f '' Set.univ)

source

ink

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

Subsemigroup N

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

Equations

MulHom.srange f = Subsemigroup.copy (Subsemigroup.map f ⊤) (Set.range ↑f) (_ : Set.range ↑f = ↑f '' Set.univ)

source

ink

@[simp]

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

↑(AddHom.srange f) = Set.range ↑f

source

ink

@[simp]

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

↑(MulHom.srange f) = Set.range ↑f

source

ink

@[simp]

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

y ∈ AddHom.srange f ↔ ∃ x, ↑f x = y

source

ink

@[simp]

theorem MulHom.mem_srange {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] {f : M →ₙ* N} {y : N} :

y ∈ MulHom.srange f ↔ ∃ x, ↑f x = y

source

ink

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

AddHom.srange f = AddSubsemigroup.map f ⊤

source

ink

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

MulHom.srange f = Subsemigroup.map f ⊤

source

ink

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

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

source

ink

theorem MulHom.map_srange {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : Mul M] [inst : Mul N] [inst : Mul P] (g : N →ₙ* P) (f : M →ₙ* N) :

Subsemigroup.map g (MulHom.srange f) = MulHom.srange (MulHom.comp g f)

source

ink

theorem AddHom.srange_top_iff_surjective {M : Type u_2} [inst : Add M] {N : Type u_1} [inst : Add N] {f : AddHom M N} :

AddHom.srange f = ⊤ ↔ Function.Surjective ↑f

source

ink

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

MulHom.srange f = ⊤ ↔ Function.Surjective ↑f

source

ink

theorem AddHom.srange_top_of_surjective {M : Type u_2} [inst : Add M] {N : Type u_1} [inst : Add N] (f : AddHom M N) (hf : Function.Surjective ↑f) :

AddHom.srange f = ⊤

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

source

ink

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

MulHom.srange f = ⊤

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

source

ink

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

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

source

ink

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

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

source

ink

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

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

ink

theorem MulHom.map_mclosure {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : 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

ink

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

AddHom { x // x ∈ S } N

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

Equations

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

source

ink

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

{ x // x ∈ S } →ₙ* N

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

Equations

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

source

ink

@[simp]

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

↑(AddHom.restrict f S) x = ↑f ↑x

source

ink

@[simp]

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

↑(MulHom.restrict f S) x = ↑f ↑x

source

ink

def AddHom.codRestrict {M : Type u_1} {N : Type u_2} {σ : Type u_3} [inst : Add M] [inst : Add N] [inst : SetLike σ N] [inst : AddMemClass σ N] (f : AddHom M N) (S : σ) (h : ∀ (x : M), ↑f x ∈ S) :

AddHom M { x // x ∈ S }

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

Equations

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

source

ink

def AddHom.codRestrict.proof_1 {M : Type u_3} {N : Type u_1} {σ : Type u_2} [inst : Add M] [inst : Add N] [inst : SetLike σ N] [inst : AddMemClass σ N] (f : AddHom M N) (S : σ) (h : ∀ (x : M), ↑f x ∈ S) (x : M) (y : M) :

(fun n => { val := ↑f n, property := h n }) (x + y) = (fun n => { val := ↑f n, property := h n }) x + (fun n => { val := ↑f n, property := h n }) y

Equations

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

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

def MulHom.codRestrict {M : Type u_1} {N : Type u_2} {σ : Type u_3} [inst : Mul M] [inst : Mul N] [inst : SetLike σ N] [inst : MulMemClass σ N] (f : M →ₙ* N) (S : σ) (h : ∀ (x : M), ↑f x ∈ S) :

M →ₙ* { x // x ∈ S }

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

Equations

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

source

ink

def AddHom.srangeRestrict.proof_1 {M : Type u_1} [inst : Add M] {N : Type u_2} [inst : Add N] (f : AddHom M N) (x : M) :

∃ y, ↑f y = ↑f x

Equations

(_ : ∃ y, ↑f y = ↑f x) = (_ : ∃ y, ↑f y = ↑f x)

source

ink

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

AddHom M { x // x ∈ AddHom.srange f }

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

Equations

AddHom.srangeRestrict f = AddHom.codRestrict f (AddHom.srange f) (_ : ∀ (x : M), ∃ y, ↑f y = ↑f x)

source

ink

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

M →ₙ* { x // x ∈ MulHom.srange f }

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

Equations

MulHom.srangeRestrict f = MulHom.codRestrict f (MulHom.srange f) (_ : ∀ (x : M), ∃ y, ↑f y = ↑f x)

source

ink

@[simp]

theorem AddHom.coe_srangeRestrict {M : Type u_2} [inst : Add M] {N : Type u_1} [inst : Add N] (f : AddHom M N) (x : M) :

↑(↑(AddHom.srangeRestrict f) x) = ↑f x

source

ink

@[simp]

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

↑(↑(MulHom.srangeRestrict f) x) = ↑f x

source

ink

abbrev AddHom.srangeRestrict_surjective.match_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (f : AddHom M N) (motive : { x // x ∈ AddHom.srange f } → Prop) :

(x : { x // x ∈ AddHom.srange f }) → ((x : M) → motive { val := ↑f x, property := (_ : ∃ y, ↑f y = ↑f x) }) → motive x

Equations

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

source

ink

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

Function.Surjective ↑(AddHom.srangeRestrict f)

source

ink

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

Function.Surjective ↑(MulHom.srangeRestrict f)

source

ink

theorem AddHom.prod_map_comap_prod' {M : Type u_3} {N : Type u_4} [inst : Add M] [inst : Add N] {M' : Type u_1} {N' : Type u_2} [inst : Add M'] [inst : Add N'] (f : AddHom M N) (g : AddHom M' N') (S : AddSubsemigroup N) (S' : AddSubsemigroup N') :

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

source

ink

theorem MulHom.prod_map_comap_prod' {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst : Mul N] {M' : Type u_1} {N' : Type u_2} [inst : Mul M'] [inst : Mul N'] (f : M →ₙ* N) (g : M' →ₙ* N') (S : Subsemigroup N) (S' : Subsemigroup N') :

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

source

ink

def AddHom.subsemigroupComap.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (N' : AddSubsemigroup N) (x : { x // x ∈ AddSubsemigroup.comap f N' }) :

↑x ∈ AddSubsemigroup.comap f N'

Equations

(_ : ↑x ∈ AddSubsemigroup.comap f N') = (_ : ↑x ∈ AddSubsemigroup.comap f N')

source

ink

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

AddHom { x // x ∈ AddSubsemigroup.comap f N' } { x // x ∈ N' }

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

Equations

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

source

ink

def AddHom.subsemigroupComap.proof_2 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (N' : AddSubsemigroup N) (x : { x // x ∈ AddSubsemigroup.comap f N' }) (y : { x // x ∈ AddSubsemigroup.comap f N' }) :

(fun x => { val := ↑f ↑x, property := (_ : ↑x ∈ AddSubsemigroup.comap f N') }) (x + y) = (fun x => { val := ↑f ↑x, property := (_ : ↑x ∈ AddSubsemigroup.comap f N') }) x + (fun x => { val := ↑f ↑x, property := (_ : ↑x ∈ AddSubsemigroup.comap f N') }) y

Equations

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

source

ink

@[simp]

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

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

source

ink

@[simp]

theorem AddHom.subsemigroupComap_apply_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (N' : AddSubsemigroup N) (x : { x // x ∈ AddSubsemigroup.comap f N' }) :

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

source

ink

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

{ x // x ∈ Subsemigroup.comap f N' } →ₙ* { x // x ∈ N' }

The MulHom from the preimage of a subsemigroup to itself.

Equations

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

source

ink

def AddHom.subsemigroupMap.proof_2 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (M' : AddSubsemigroup M) (x : { x // x ∈ M' }) (y : { x // x ∈ M' }) :

(fun x => { val := ↑f ↑x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x) }) (x + y) = (fun x => { val := ↑f ↑x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x) }) x + (fun x => { val := ↑f ↑x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x) }) y

Equations

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

source

ink

def AddHom.subsemigroupMap.proof_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (M' : AddSubsemigroup M) (x : { x // x ∈ M' }) :

∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x

Equations

(_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x) = (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x)

source

ink

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

AddHom { x // x ∈ M' } { x // x ∈ AddSubsemigroup.map f M' }

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

Equations

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

source

ink

@[simp]

theorem AddHom.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (M' : AddSubsemigroup M) (x : { x // x ∈ M' }) :

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

source

ink

@[simp]

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

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

source

ink

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

{ x // x ∈ M' } →ₙ* { x // x ∈ Subsemigroup.map f M' }

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

Equations

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

source

ink

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

Function.Surjective ↑(AddHom.subsemigroupMap f M')

source

ink

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

Function.Surjective ↑(MulHom.subsemigroupMap f M')

source

ink

@[simp]

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

AddHom.srange (AddHom.fst M N) = ⊤

source

ink

@[simp]

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

MulHom.srange (MulHom.fst M N) = ⊤

source

ink

@[simp]

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

AddHom.srange (AddHom.snd M N) = ⊤

source

ink

@[simp]

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

MulHom.srange (MulHom.snd M N) = ⊤

source

ink

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

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

source

ink

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

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

source

ink

def AddSubsemigroup.inclusion.proof_1 {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {T : AddSubsemigroup M} (h : S ≤ T) (x : { x // x ∈ S }) :

↑(AddMemClass.subtype S) x ∈ T

Equations

(_ : ↑(AddMemClass.subtype S) x ∈ T) = h (↑(AddMemClass.subtype S) x) (_ : ↑x ∈ S)

source

ink

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

AddHom { x // x ∈ S } { x // x ∈ T }

The AddSemigroup hom associated to an inclusion of subsemigroups.

Equations

AddSubsemigroup.inclusion h = AddHom.codRestrict (AddMemClass.subtype S) T (_ : ∀ (x : { x // x ∈ S }), ↑(AddMemClass.subtype S) x ∈ T)

source

ink

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

{ x // x ∈ S } →ₙ* { x // x ∈ T }

The semigroup hom associated to an inclusion of subsemigroups.

Equations

Subsemigroup.inclusion h = MulHom.codRestrict (MulMemClass.subtype S) T (_ : ∀ (x : { x // x ∈ S }), ↑(MulMemClass.subtype S) x ∈ T)

source

ink

@[simp]

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

AddHom.srange (AddMemClass.subtype s) = s

source

ink

@[simp]

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

MulHom.srange (MulMemClass.subtype s) = s

source

ink

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

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

source

ink

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

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

source

ink

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

Function.RightInverse (Equiv.setCongr (_ : ↑S = ↑T)).invFun (Equiv.setCongr (_ : ↑S = ↑T)).toFun

Equations

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

source

ink

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

↑S = ↑T

Equations

(_ : ↑S = ↑T) = (_ : ↑S = ↑T)

source

ink

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

{ x // x ∈ S } ≃+ { x // x ∈ T }

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

Equations

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

source

ink

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

Function.LeftInverse (Equiv.setCongr (_ : ↑S = ↑T)).invFun (Equiv.setCongr (_ : ↑S = ↑T)).toFun

Equations

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

source

ink

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

∀ (x x_1 : { x // x ∈ S }), Equiv.toFun { toFun := (Equiv.setCongr (_ : ↑S = ↑T)).toFun, invFun := (Equiv.setCongr (_ : ↑S = ↑T)).invFun, left_inv := (_ : Function.LeftInverse (Equiv.setCongr (_ : ↑S = ↑T)).invFun (Equiv.setCongr (_ : ↑S = ↑T)).toFun), right_inv := (_ : Function.RightInverse (Equiv.setCongr (_ : ↑S = ↑T)).invFun (Equiv.setCongr (_ : ↑S = ↑T)).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.setCongr (_ : ↑S = ↑T)).toFun, invFun := (Equiv.setCongr (_ : ↑S = ↑T)).invFun, left_inv := (_ : Function.LeftInverse (Equiv.setCongr (_ : ↑S = ↑T)).invFun (Equiv.setCongr (_ : ↑S = ↑T)).toFun), right_inv := (_ : Function.RightInverse (Equiv.setCongr (_ : ↑S = ↑T)).invFun (Equiv.setCongr (_ : ↑S = ↑T)).toFun) } (x + x_1)

Equations

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

source

ink

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

{ x // x ∈ S } ≃* { x // x ∈ T }

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

Equations

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

source

ink

def AddEquiv.ofLeftInverse.proof_1 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (f : AddHom M N) {g : N → M} (h : Function.LeftInverse g ↑f) (x : { x // x ∈ AddHom.srange f }) :

↑(AddHom.srangeRestrict f) ((g ∘ ↑(AddMemClass.subtype (AddHom.srange f))) x) = x

Equations

(_ : ↑(AddHom.srangeRestrict f) ((g ∘ ↑(AddMemClass.subtype (AddHom.srange f))) x) = x) = (_ : ↑(AddHom.srangeRestrict f) ((g ∘ ↑(AddMemClass.subtype (AddHom.srange f))) x) = x)

source

ink

abbrev AddEquiv.ofLeftInverse.match_1 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) (x : { x // x ∈ AddHom.srange f }) (motive : (∃ x, ↑f x = ↑x) → Prop) :

(x : ∃ x, ↑f x = ↑x) → ((x' : M) → (hx' : ↑f x' = ↑x) → motive (_ : ∃ x, ↑f x = ↑x)) → motive x

Equations

AddEquiv.ofLeftInverse.match_1 f x motive x h_1 = Exists.casesOn x fun w h => h_1 w h

source

ink

def AddEquiv.ofLeftInverse.proof_2 {M : Type u_2} {N : Type u_1} [inst : Add M] [inst : Add N] (f : AddHom M N) (x : M) (y : M) :

AddHom.toFun (AddHom.srangeRestrict f) (x + y) = AddHom.toFun (AddHom.srangeRestrict f) x + AddHom.toFun (AddHom.srangeRestrict f) y

Equations

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

source

ink

def AddEquiv.ofLeftInverse {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) {g : N → M} (h : Function.LeftInverse g ↑f) :

M ≃+ { x // x ∈ AddHom.srange f }

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

Equations

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

source

ink

@[simp]

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

∀ (a : { x // x ∈ MulHom.srange f }), ↑(MulEquiv.symm (MulEquiv.ofLeftInverse f h)) a = g ↑a

source

ink

@[simp]

theorem AddEquiv.ofLeftInverse_symm_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (f : AddHom M N) {g : N → M} (h : Function.LeftInverse g ↑f) :

∀ (a : { x // x ∈ AddHom.srange f }), ↑(AddEquiv.symm (AddEquiv.ofLeftInverse f h)) a = g ↑a

source

ink

@[simp]

theorem MulEquiv.ofLeftInverse_apply {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : 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

ink

@[simp]

theorem AddEquiv.ofLeftInverse_apply {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : 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

ink

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

M ≃* { x // x ∈ MulHom.srange f }

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

This is a bidirectional version of MulHom.srangeRestrict.

Equations

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

source

ink

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

Function.RightInverse (Equiv.image e.toEquiv ↑S).invFun (Equiv.image e.toEquiv ↑S).toFun

Equations

(_ : Function.RightInverse (Equiv.image e.toEquiv ↑S).invFun (Equiv.image e.toEquiv ↑S).toFun) = (_ : Function.RightInverse (Equiv.image e.toEquiv ↑S).invFun (Equiv.image e.toEquiv ↑S).toFun)

source

ink

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

{ x // x ∈ S } ≃+ { x // x ∈ AddSubsemigroup.map (AddEquiv.toAddHom e) S }

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

Equations

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

source

ink

def AddEquiv.subsemigroupMap.proof_5 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : { x // x ∈ S }) (y : { x // x ∈ S }) :

AddHom.toFun (AddHom.subsemigroupMap (AddEquiv.toAddHom e) S) (x + y) = AddHom.toFun (AddHom.subsemigroupMap (AddEquiv.toAddHom e) S) x + AddHom.toFun (AddHom.subsemigroupMap (AddEquiv.toAddHom e) S) y

Equations

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

source

ink

def AddEquiv.subsemigroupMap.proof_2 {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : { x // x ∈ AddSubsemigroup.map (AddEquiv.toAddHom e) S }) :

↑(Equiv.invFun (Equiv.image e.toEquiv ↑S) x) ∈ S

Equations

(_ : ↑(Equiv.invFun (Equiv.image e.toEquiv ↑S) x) ∈ S) = (_ : ↑(Equiv.invFun (Equiv.image e.toEquiv ↑S) x) ∈ S)

source

ink

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

↑(Equiv.toFun (Equiv.image e.toEquiv ↑S) x) ∈ AddSubsemigroup.map (AddEquiv.toAddHom e) S

Equations

(_ : ↑(Equiv.toFun (Equiv.image e.toEquiv ↑S) x) ∈ AddSubsemigroup.map (AddEquiv.toAddHom e) S) = (_ : ↑(Equiv.toFun (Equiv.image e.toEquiv ↑S) x) ∈ AddSubsemigroup.map (AddEquiv.toAddHom e) S)

source

ink

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

Function.LeftInverse (Equiv.image e.toEquiv ↑S).invFun (Equiv.image e.toEquiv ↑S).toFun

Equations

(_ : Function.LeftInverse (Equiv.image e.toEquiv ↑S).invFun (Equiv.image e.toEquiv ↑S).toFun) = (_ : Function.LeftInverse (Equiv.image e.toEquiv ↑S).invFun (Equiv.image e.toEquiv ↑S).toFun)

source

ink

@[simp]

theorem AddEquiv.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : { x // x ∈ S }) :

↑(↑(AddEquiv.subsemigroupMap e S) x) = ↑e ↑x

source

ink

@[simp]

theorem MulEquiv.subsemigroupMap_apply_coe {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) (S : Subsemigroup M) (x : { x // x ∈ S }) :

↑(↑(MulEquiv.subsemigroupMap e S) x) = ↑e ↑x

source

ink

@[simp]

theorem MulEquiv.subsemigroupMap_symm_apply_coe {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (e : M ≃* N) (S : Subsemigroup M) (x : { x // x ∈ Subsemigroup.map (MulEquiv.toMulHom e) S }) :

↑(↑(MulEquiv.symm (MulEquiv.subsemigroupMap e S)) x) = ↑(MulEquiv.symm e) ↑x

source

ink

@[simp]

theorem AddEquiv.subsemigroupMap_symm_apply_coe {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (e : M ≃+ N) (S : AddSubsemigroup M) (x : { x // x ∈ AddSubsemigroup.map (AddEquiv.toAddHom e) S }) :

↑(↑(AddEquiv.symm (AddEquiv.subsemigroupMap e S)) x) = ↑(AddEquiv.symm e) ↑x

source

ink

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

{ x // x ∈ S } ≃* { x // x ∈ Subsemigroup.map (MulEquiv.toMulHom e) S }

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

Equations

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

Operations on Subsemigroups #

Main definitions #

Conversion between multiplicative and additive definitions #

(Commutative) semigroup structure on a subsemigroup #

Operations on subsemigroups #

Semigroup homomorphisms between subsemigroups #

Operations on mul_homs #

Implementation notes #

Tags #

Conversion to/from Additive/Multiplicative #

comap and map #

Operations on `Subsemigroup`s #

Operations on `mul_hom`s #

Conversion to/from `Additive`/`Multiplicative` #

`comap` and `map` #