group_theory.subsemigroup.operations

@[simp]

theorem subsemigroup.to_add_subsemigroup_symm_apply_coe {M : Type u_1} [has_mul M] (S : add_subsemigroup (additive M)) :

↑(⇑(rel_iso.symm subsemigroup.to_add_subsemigroup) S) = ⇑additive.of_mul ⁻¹' ↑S

source

def subsemigroup.to_add_subsemigroup {M : Type u_1} [has_mul M] :

subsemigroup M ≃o add_subsemigroup (additive M)

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

Equations

subsemigroup.to_add_subsemigroup = {to_equiv := {to_fun := λ (S : subsemigroup M), {carrier := ⇑additive.to_mul ⁻¹' ↑S, add_mem' := _}, inv_fun := λ (S : add_subsemigroup (additive M)), {carrier := ⇑additive.of_mul ⁻¹' ↑S, mul_mem' := _}, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem subsemigroup.to_add_subsemigroup_apply_coe {M : Type u_1} [has_mul M] (S : subsemigroup M) :

↑(⇑subsemigroup.to_add_subsemigroup S) = ⇑additive.to_mul ⁻¹' ↑S

source

@[reducible]

def add_subsemigroup.to_subsemigroup' {M : Type u_1} [has_mul M] :

add_subsemigroup (additive M) ≃o subsemigroup M

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

source

theorem subsemigroup.to_add_subsemigroup_closure {M : Type u_1} [has_mul M] (S : set M) :

⇑subsemigroup.to_add_subsemigroup (subsemigroup.closure S) = add_subsemigroup.closure (⇑additive.to_mul ⁻¹' S)

source

theorem add_subsemigroup.to_subsemigroup'_closure {M : Type u_1} [has_mul M] (S : set (additive M)) :

⇑add_subsemigroup.to_subsemigroup' (add_subsemigroup.closure S) = subsemigroup.closure (⇑multiplicative.of_add ⁻¹' S)

source

@[simp]

theorem add_subsemigroup.to_subsemigroup_symm_apply_coe {A : Type u_5} [has_add A] (S : subsemigroup (multiplicative A)) :

↑(⇑(rel_iso.symm add_subsemigroup.to_subsemigroup) S) = ⇑multiplicative.of_add ⁻¹' ↑S

source

@[simp]

theorem add_subsemigroup.to_subsemigroup_apply_coe {A : Type u_5} [has_add A] (S : add_subsemigroup A) :

↑(⇑add_subsemigroup.to_subsemigroup S) = ⇑multiplicative.to_add ⁻¹' ↑S

source

def add_subsemigroup.to_subsemigroup {A : Type u_5} [has_add A] :

add_subsemigroup A ≃o subsemigroup (multiplicative A)

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

Equations

add_subsemigroup.to_subsemigroup = {to_equiv := {to_fun := λ (S : add_subsemigroup A), {carrier := ⇑multiplicative.to_add ⁻¹' ↑S, mul_mem' := _}, inv_fun := λ (S : subsemigroup (multiplicative A)), {carrier := ⇑multiplicative.of_add ⁻¹' ↑S, add_mem' := _}, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[reducible]

def subsemigroup.to_add_subsemigroup' {A : Type u_5} [has_add A] :

subsemigroup (multiplicative A) ≃o add_subsemigroup A

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

source

theorem add_subsemigroup.to_subsemigroup_closure {A : Type u_5} [has_add A] (S : set A) :

⇑add_subsemigroup.to_subsemigroup (add_subsemigroup.closure S) = subsemigroup.closure (⇑multiplicative.to_add ⁻¹' S)

source

theorem subsemigroup.to_add_subsemigroup'_closure {A : Type u_5} [has_add A] (S : set (multiplicative A)) :

⇑subsemigroup.to_add_subsemigroup' (subsemigroup.closure S) = add_subsemigroup.closure (⇑additive.of_mul ⁻¹' S)

source

def subsemigroup.comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_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' := _}

source

def add_subsemigroup.comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (S : add_subsemigroup N) :

add_subsemigroup M

The preimage of an add_subsemigroup along an add_semigroup homomorphism is an add_subsemigroup.

Equations

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

source

@[simp]

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

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

source

@[simp]

theorem add_subsemigroup.coe_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S : add_subsemigroup N) (f : add_hom M N) :

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

source

@[simp]

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

x ∈ subsemigroup.comap f S ↔ ⇑f x ∈ S

source

@[simp]

theorem add_subsemigroup.mem_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {S : add_subsemigroup N} {f : add_hom M N} {x : M} :

x ∈ add_subsemigroup.comap f S ↔ ⇑f x ∈ S

source

theorem add_subsemigroup.comap_comap {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] (S : add_subsemigroup P) (g : add_hom N P) (f : add_hom M N) :

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

source

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

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

source

@[simp]

theorem add_subsemigroup.comap_id {P : Type u_3} [has_add P] (S : add_subsemigroup P) :

add_subsemigroup.comap (add_hom.id P) S = S

source

@[simp]

theorem subsemigroup.comap_id {P : Type u_3} [has_mul P] (S : subsemigroup P) :

subsemigroup.comap (mul_hom.id P) S = S

source

def subsemigroup.map {M : Type u_1} {N : Type u_2} [has_mul M] [has_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' := _}

source

def add_subsemigroup.map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (S : add_subsemigroup M) :

add_subsemigroup N

The image of an add_subsemigroup along an add_semigroup homomorphism is an add_subsemigroup.

Equations

add_subsemigroup.map f S = {carrier := ⇑f '' ↑S, add_mem' := _}

source

@[simp]

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

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

source

@[simp]

theorem add_subsemigroup.coe_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (S : add_subsemigroup M) :

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

source

@[simp]

theorem add_subsemigroup.mem_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} {S : add_subsemigroup M} {y : N} :

y ∈ add_subsemigroup.map f S ↔ ∃ (x : M) (H : x ∈ S), ⇑f x = y

source

@[simp]

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

y ∈ subsemigroup.map f S ↔ ∃ (x : M) (H : x ∈ S), ⇑f x = y

source

theorem add_subsemigroup.mem_map_of_mem {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) {S : add_subsemigroup M} {x : M} (hx : x ∈ S) :

⇑f x ∈ add_subsemigroup.map f S

source

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

⇑f x ∈ subsemigroup.map f S

source

theorem add_subsemigroup.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (S : add_subsemigroup M) (x : ↥S) :

⇑f ↑x ∈ add_subsemigroup.map f S

source

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

⇑f ↑x ∈ subsemigroup.map f S

source

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

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

source

theorem add_subsemigroup.map_map {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] (S : add_subsemigroup M) (g : add_hom N P) (f : add_hom M N) :

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

source

theorem add_subsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.injective ⇑f) {S : add_subsemigroup M} {x : M} :

⇑f x ∈ add_subsemigroup.map f S ↔ x ∈ S

source

theorem subsemigroup.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective ⇑f) {S : subsemigroup M} {x : M} :

⇑f x ∈ subsemigroup.map f S ↔ x ∈ S

source

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

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

source

theorem add_subsemigroup.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} {S : add_subsemigroup M} {T : add_subsemigroup N} :

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

source

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

galois_connection (subsemigroup.map f) (subsemigroup.comap f)

source

theorem add_subsemigroup.gc_map_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :

galois_connection (add_subsemigroup.map f) (add_subsemigroup.comap f)

source

theorem add_subsemigroup.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S : add_subsemigroup M) {T : add_subsemigroup N} {f : add_hom M N} :

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

source

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

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

source

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

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

source

theorem add_subsemigroup.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S : add_subsemigroup M) {T : add_subsemigroup N} {f : add_hom M N} :

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

source

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

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

source

theorem add_subsemigroup.le_comap_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S : add_subsemigroup M) {f : add_hom M N} :

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

source

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

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

source

theorem add_subsemigroup.map_comap_le {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {S : add_subsemigroup N} {f : add_hom M N} :

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

source

theorem add_subsemigroup.monotone_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} :

monotone (add_subsemigroup.map f)

source

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

monotone (subsemigroup.map f)

source

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

monotone (subsemigroup.comap f)

source

theorem add_subsemigroup.monotone_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} :

monotone (add_subsemigroup.comap f)

source

@[simp]

theorem add_subsemigroup.map_comap_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S : add_subsemigroup M) {f : add_hom M N} :

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

source

@[simp]

theorem subsemigroup.map_comap_map {M : Type u_1} {N : Type u_2} [has_mul M] [has_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 add_subsemigroup.comap_map_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {S : add_subsemigroup N} {f : add_hom M N} :

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

source

@[simp]

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

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

source

theorem add_subsemigroup.map_sup {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S T : add_subsemigroup M) (f : add_hom M N) :

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

source

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

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

source

theorem add_subsemigroup.map_supr {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {ι : Sort u_3} (f : add_hom M N) (s : ι → add_subsemigroup M) :

add_subsemigroup.map f (supr s) = ⨆ (i : ι), add_subsemigroup.map f (s i)

source

theorem subsemigroup.map_supr {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {ι : Sort u_3} (f : M →ₙ* N) (s : ι → subsemigroup M) :

subsemigroup.map f (supr s) = ⨆ (i : ι), subsemigroup.map f (s i)

source

theorem add_subsemigroup.comap_inf {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S T : add_subsemigroup N) (f : add_hom M N) :

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

source

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

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

source

theorem subsemigroup.comap_infi {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {ι : Sort u_3} (f : M →ₙ* N) (s : ι → subsemigroup N) :

subsemigroup.comap f (infi s) = ⨅ (i : ι), subsemigroup.comap f (s i)

source

theorem add_subsemigroup.comap_infi {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {ι : Sort u_3} (f : add_hom M N) (s : ι → add_subsemigroup N) :

add_subsemigroup.comap f (infi s) = ⨅ (i : ι), add_subsemigroup.comap f (s i)

source

@[simp]

theorem add_subsemigroup.map_bot {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :

add_subsemigroup.map f ⊥ = ⊥

source

@[simp]

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

subsemigroup.map f ⊥ = ⊥

source

@[simp]

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

subsemigroup.comap f ⊤ = ⊤

source

@[simp]

theorem add_subsemigroup.comap_top {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :

add_subsemigroup.comap f ⊤ = ⊤

source

@[simp]

theorem add_subsemigroup.map_id {M : Type u_1} [has_add M] (S : add_subsemigroup M) :

add_subsemigroup.map (add_hom.id M) S = S

source

@[simp]

theorem subsemigroup.map_id {M : Type u_1} [has_mul M] (S : subsemigroup M) :

subsemigroup.map (mul_hom.id M) S = S

source

def add_subsemigroup.gci_map_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.injective ⇑f) :

galois_coinsertion (add_subsemigroup.map f) (add_subsemigroup.comap f)

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

Equations

add_subsemigroup.gci_map_comap hf = _.to_galois_coinsertion _

source

def subsemigroup.gci_map_comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective ⇑f) :

galois_coinsertion (subsemigroup.map f) (subsemigroup.comap f)

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

Equations

subsemigroup.gci_map_comap hf = _.to_galois_coinsertion _

source

theorem subsemigroup.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective ⇑f) (S : subsemigroup M) :

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

source

theorem add_subsemigroup.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.injective ⇑f) (S : add_subsemigroup M) :

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

source

theorem subsemigroup.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective ⇑f) :

function.surjective (subsemigroup.comap f)

source

theorem add_subsemigroup.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.injective ⇑f) :

function.surjective (add_subsemigroup.comap f)

source

theorem subsemigroup.map_injective_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective ⇑f) :

function.injective (subsemigroup.map f)

source

theorem add_subsemigroup.map_injective_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.injective ⇑f) :

function.injective (add_subsemigroup.map f)

source

theorem add_subsemigroup.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.injective ⇑f) (S T : add_subsemigroup M) :

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

source

theorem subsemigroup.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective ⇑f) (S T : subsemigroup M) :

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

source

theorem add_subsemigroup.comap_infi_map_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {ι : Type u_5} {f : add_hom M N} (hf : function.injective ⇑f) (S : ι → add_subsemigroup M) :

add_subsemigroup.comap f (⨅ (i : ι), add_subsemigroup.map f (S i)) = infi S

source

theorem subsemigroup.comap_infi_map_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : function.injective ⇑f) (S : ι → subsemigroup M) :

subsemigroup.comap f (⨅ (i : ι), subsemigroup.map f (S i)) = infi S

source

theorem add_subsemigroup.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.injective ⇑f) (S T : add_subsemigroup M) :

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

source

theorem subsemigroup.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective ⇑f) (S T : subsemigroup M) :

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

source

theorem add_subsemigroup.comap_supr_map_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {ι : Type u_5} {f : add_hom M N} (hf : function.injective ⇑f) (S : ι → add_subsemigroup M) :

add_subsemigroup.comap f (⨆ (i : ι), add_subsemigroup.map f (S i)) = supr S

source

theorem subsemigroup.comap_supr_map_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : function.injective ⇑f) (S : ι → subsemigroup M) :

subsemigroup.comap f (⨆ (i : ι), subsemigroup.map f (S i)) = supr S

source

theorem subsemigroup.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective ⇑f) {S T : subsemigroup M} :

subsemigroup.map f S ≤ subsemigroup.map f T ↔ S ≤ T

source

theorem add_subsemigroup.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.injective ⇑f) {S T : add_subsemigroup M} :

add_subsemigroup.map f S ≤ add_subsemigroup.map f T ↔ S ≤ T

source

theorem subsemigroup.map_strict_mono_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.injective ⇑f) :

strict_mono (subsemigroup.map f)

source

theorem add_subsemigroup.map_strict_mono_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.injective ⇑f) :

strict_mono (add_subsemigroup.map f)

source

def subsemigroup.gi_map_comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective ⇑f) :

galois_insertion (subsemigroup.map f) (subsemigroup.comap f)

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

Equations

subsemigroup.gi_map_comap hf = _.to_galois_insertion _

source

def add_subsemigroup.gi_map_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.surjective ⇑f) :

galois_insertion (add_subsemigroup.map f) (add_subsemigroup.comap f)

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

Equations

add_subsemigroup.gi_map_comap hf = _.to_galois_insertion _

source

theorem add_subsemigroup.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.surjective ⇑f) (S : add_subsemigroup N) :

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

source

theorem subsemigroup.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective ⇑f) (S : subsemigroup N) :

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

source

theorem add_subsemigroup.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.surjective ⇑f) :

function.surjective (add_subsemigroup.map f)

source

theorem subsemigroup.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective ⇑f) :

function.surjective (subsemigroup.map f)

source

theorem add_subsemigroup.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.surjective ⇑f) :

function.injective (add_subsemigroup.comap f)

source

theorem subsemigroup.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective ⇑f) :

function.injective (subsemigroup.comap f)

source

theorem add_subsemigroup.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.surjective ⇑f) (S T : add_subsemigroup N) :

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

source

theorem subsemigroup.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective ⇑f) (S T : subsemigroup N) :

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

source

theorem add_subsemigroup.map_infi_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {ι : Type u_5} {f : add_hom M N} (hf : function.surjective ⇑f) (S : ι → add_subsemigroup N) :

add_subsemigroup.map f (⨅ (i : ι), add_subsemigroup.comap f (S i)) = infi S

source

theorem subsemigroup.map_infi_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : function.surjective ⇑f) (S : ι → subsemigroup N) :

subsemigroup.map f (⨅ (i : ι), subsemigroup.comap f (S i)) = infi S

source

theorem add_subsemigroup.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.surjective ⇑f) (S T : add_subsemigroup N) :

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

source

theorem subsemigroup.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective ⇑f) (S T : subsemigroup N) :

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

source

theorem subsemigroup.map_supr_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {ι : Type u_5} {f : M →ₙ* N} (hf : function.surjective ⇑f) (S : ι → subsemigroup N) :

subsemigroup.map f (⨆ (i : ι), subsemigroup.comap f (S i)) = supr S

source

theorem add_subsemigroup.map_supr_comap_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {ι : Type u_5} {f : add_hom M N} (hf : function.surjective ⇑f) (S : ι → add_subsemigroup N) :

add_subsemigroup.map f (⨆ (i : ι), add_subsemigroup.comap f (S i)) = supr S

source

theorem add_subsemigroup.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.surjective ⇑f) {S T : add_subsemigroup N} :

add_subsemigroup.comap f S ≤ add_subsemigroup.comap f T ↔ S ≤ T

source

theorem subsemigroup.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective ⇑f) {S T : subsemigroup N} :

subsemigroup.comap f S ≤ subsemigroup.comap f T ↔ S ≤ T

source

theorem subsemigroup.comap_strict_mono_of_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} (hf : function.surjective ⇑f) :

strict_mono (subsemigroup.comap f)

source

theorem add_subsemigroup.comap_strict_mono_of_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} (hf : function.surjective ⇑f) :

strict_mono (add_subsemigroup.comap f)

source

@[protected, instance]

def add_mem_class.has_add {M : Type u_1} {A : Type u_5} [has_add M] [set_like A M] [hA : add_mem_class A M] (S' : A) :

has_add ↥S'

An additive submagma of an additive magma inherits an addition.

Equations

add_mem_class.has_add S' = {add := λ (a b : ↥S'), ⟨a.val + b.val, _⟩}

source

@[protected, instance]

def mul_mem_class.has_mul {M : Type u_1} {A : Type u_5} [has_mul M] [set_like A M] [hA : mul_mem_class A M] (S' : A) :

has_mul ↥S'

A submagma of a magma inherits a multiplication.

Equations

mul_mem_class.has_mul S' = {mul := λ (a b : ↥S'), ⟨a.val * b.val, _⟩}

source

@[simp, norm_cast]

theorem add_mem_class.coe_add {M : Type u_1} {A : Type u_5} [has_add M] [set_like A M] [hA : add_mem_class A M] (S' : A) (x y : ↥S') :

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

source

@[simp, norm_cast]

theorem mul_mem_class.coe_mul {M : Type u_1} {A : Type u_5} [has_mul M] [set_like A M] [hA : mul_mem_class A M] (S' : A) (x y : ↥S') :

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

source

@[simp]

theorem add_mem_class.mk_add_mk {M : Type u_1} {A : Type u_5} [has_add M] [set_like A M] [hA : add_mem_class A M] (S' : A) (x y : M) (hx : x ∈ S') (hy : y ∈ S') :

⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, _⟩

source

@[simp]

theorem mul_mem_class.mk_mul_mk {M : Type u_1} {A : Type u_5} [has_mul M] [set_like A M] [hA : mul_mem_class A M] (S' : A) (x y : M) (hx : x ∈ S') (hy : y ∈ S') :

⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, _⟩

source

theorem add_mem_class.add_def {M : Type u_1} {A : Type u_5} [has_add M] [set_like A M] [hA : add_mem_class A M] (S' : A) (x y : ↥S') :

x + y = ⟨↑x + ↑y, _⟩

source

theorem mul_mem_class.mul_def {M : Type u_1} {A : Type u_5} [has_mul M] [set_like A M] [hA : mul_mem_class A M] (S' : A) (x y : ↥S') :

x * y = ⟨↑x * ↑y, _⟩

source

@[protected, instance]

def add_mem_class.to_add_semigroup {M : Type u_1} [add_semigroup M] {A : Type u_2} [set_like A M] [add_mem_class A M] (S : A) :

add_semigroup ↥S

An add_subsemigroup of an add_semigroup inherits an add_semigroup structure.

Equations

add_mem_class.to_add_semigroup S = function.injective.add_semigroup coe _ _

source

@[protected, instance]

def mul_mem_class.to_semigroup {M : Type u_1} [semigroup M] {A : Type u_2} [set_like A M] [mul_mem_class A M] (S : A) :

semigroup ↥S

A subsemigroup of a semigroup inherits a semigroup structure.

Equations

mul_mem_class.to_semigroup S = function.injective.semigroup coe _ _

source

@[protected, instance]

def mul_mem_class.to_comm_semigroup {M : Type u_1} [comm_semigroup M] {A : Type u_2} [set_like A M] [mul_mem_class A M] (S : A) :

comm_semigroup ↥S

A subsemigroup of a comm_semigroup is a comm_semigroup.

Equations

mul_mem_class.to_comm_semigroup S = function.injective.comm_semigroup coe _ _

source

@[protected, instance]

def add_mem_class.to_add_comm_semigroup {M : Type u_1} [add_comm_semigroup M] {A : Type u_2} [set_like A M] [add_mem_class A M] (S : A) :

add_comm_semigroup ↥S

An add_subsemigroup of an add_comm_semigroup is an add_comm_semigroup.

Equations

add_mem_class.to_add_comm_semigroup S = function.injective.add_comm_semigroup coe _ _

source

def mul_mem_class.subtype {M : Type u_1} {A : Type u_5} [has_mul M] [set_like A M] [hA : mul_mem_class A M] (S' : A) :

↥S' →ₙ* M

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

Equations

mul_mem_class.subtype S' = {to_fun := coe coe_to_lift, map_mul' := _}

source

def add_mem_class.subtype {M : Type u_1} {A : Type u_5} [has_add M] [set_like A M] [hA : add_mem_class A M] (S' : A) :

add_hom ↥S' M

The natural semigroup hom from an add_subsemigroup of add_semigroup M to M.

Equations

add_mem_class.subtype S' = {to_fun := coe coe_to_lift, map_add' := _}

source

@[simp]

theorem add_mem_class.coe_subtype {M : Type u_1} {A : Type u_5} [has_add M] [set_like A M] [hA : add_mem_class A M] (S' : A) :

⇑(add_mem_class.subtype S') = coe

source

@[simp]

theorem mul_mem_class.coe_subtype {M : Type u_1} {A : Type u_5} [has_mul M] [set_like A M] [hA : mul_mem_class A M] (S' : A) :

⇑(mul_mem_class.subtype S') = coe

source

@[simp]

theorem add_subsemigroup.top_equiv_apply {M : Type u_1} [has_add M] (x : ↥⊤) :

⇑add_subsemigroup.top_equiv x = ↑x

source

@[simp]

theorem subsemigroup.top_equiv_symm_apply_coe {M : Type u_1} [has_mul M] (x : M) :

↑(⇑(subsemigroup.top_equiv.symm) x) = x

source

@[simp]

theorem add_subsemigroup.top_equiv_symm_apply_coe {M : Type u_1} [has_add M] (x : M) :

↑(⇑(add_subsemigroup.top_equiv.symm) x) = x

source

def add_subsemigroup.top_equiv {M : Type u_1} [has_add M] :

↥⊤ ≃+ M

The top additive subsemigroup is isomorphic to the additive semigroup.

Equations

add_subsemigroup.top_equiv = {to_fun := λ (x : ↥⊤), ↑x, inv_fun := λ (x : M), ⟨x, _⟩, left_inv := _, right_inv := _, map_add' := _}

source

def subsemigroup.top_equiv {M : Type u_1} [has_mul M] :

↥⊤ ≃* M

The top subsemigroup is isomorphic to the semigroup.

Equations

subsemigroup.top_equiv = {to_fun := λ (x : ↥⊤), ↑x, inv_fun := λ (x : M), ⟨x, _⟩, left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem subsemigroup.top_equiv_apply {M : Type u_1} [has_mul M] (x : ↥⊤) :

⇑subsemigroup.top_equiv x = ↑x

source

@[simp]

theorem add_subsemigroup.top_equiv_to_add_hom {M : Type u_1} [has_add M] :

add_subsemigroup.top_equiv.to_add_hom = add_mem_class.subtype ⊤

source

@[simp]

theorem subsemigroup.top_equiv_to_mul_hom {M : Type u_1} [has_mul M] :

subsemigroup.top_equiv.to_mul_hom = mul_mem_class.subtype ⊤

source

noncomputable def add_subsemigroup.equiv_map_of_injective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S : add_subsemigroup M) (f : add_hom M N) (hf : function.injective ⇑f) :

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

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

Equations

S.equiv_map_of_injective f hf = {to_fun := (equiv.set.image ⇑f ↑S hf).to_fun, inv_fun := (equiv.set.image ⇑f ↑S hf).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

noncomputable def subsemigroup.equiv_map_of_injective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (S : subsemigroup M) (f : M →ₙ* N) (hf : function.injective ⇑f) :

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

A subsemigroup is isomorphic to its image under an injective function

Equations

S.equiv_map_of_injective f hf = {to_fun := (equiv.set.image ⇑f ↑S hf).to_fun, inv_fun := (equiv.set.image ⇑f ↑S hf).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem subsemigroup.coe_equiv_map_of_injective_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (S : subsemigroup M) (f : M →ₙ* N) (hf : function.injective ⇑f) (x : ↥S) :

↑(⇑(S.equiv_map_of_injective f hf) x) = ⇑f ↑x

source

@[simp]

theorem add_subsemigroup.coe_equiv_map_of_injective_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (S : add_subsemigroup M) (f : add_hom M N) (hf : function.injective ⇑f) (x : ↥S) :

↑(⇑(S.equiv_map_of_injective f hf) x) = ⇑f ↑x

source

@[simp]

theorem subsemigroup.closure_closure_coe_preimage {M : Type u_1} [has_mul M] {s : set M} :

subsemigroup.closure (coe ⁻¹' s) = ⊤

source

@[simp]

theorem add_subsemigroup.closure_closure_coe_preimage {M : Type u_1} [has_add M] {s : set M} :

add_subsemigroup.closure (coe ⁻¹' s) = ⊤

source

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

subsemigroup (M × N)

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

Equations

s.prod t = {carrier := ↑s ×ˢ ↑t, mul_mem' := _}

source

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

add_subsemigroup (M × N)

Given add_subsemigroups s, t of add_semigroups A, B respectively, s × t as an add_subsemigroup of A × B.

Equations

s.prod t = {carrier := ↑s ×ˢ ↑t, add_mem' := _}

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

s.prod ⊤ = add_subsemigroup.comap (add_hom.fst M N) s

source

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

s.prod ⊤ = subsemigroup.comap (mul_hom.fst M N) s

source

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

⊤.prod s = subsemigroup.comap (mul_hom.snd M N) s

source

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

⊤.prod s = add_subsemigroup.comap (add_hom.snd M N) s

source

@[simp]

theorem subsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :

⊤.prod ⊤ = ⊤

source

@[simp]

theorem add_subsemigroup.top_prod_top {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] :

⊤.prod ⊤ = ⊤

source

theorem subsemigroup.bot_prod_bot {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :

⊥.prod ⊥ = ⊥

source

theorem add_subsemigroup.bot_sum_bot {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] :

⊥.prod ⊥ = ⊥

source

def subsemigroup.prod_equiv {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (s : subsemigroup M) (t : subsemigroup N) :

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

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

Equations

s.prod_equiv t = {to_fun := (equiv.set.prod ↑s ↑t).to_fun, inv_fun := (equiv.set.prod ↑s ↑t).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

def add_subsemigroup.prod_equiv {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (s : add_subsemigroup M) (t : add_subsemigroup N) :

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

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

Equations

s.prod_equiv t = {to_fun := (equiv.set.prod ↑s ↑t).to_fun, inv_fun := (equiv.set.prod ↑s ↑t).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

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

x ∈ add_subsemigroup.map f.to_add_hom K ↔ ⇑(f.symm) x ∈ K

source

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

x ∈ subsemigroup.map f.to_mul_hom K ↔ ⇑(f.symm) x ∈ K

source

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

subsemigroup.map f.to_mul_hom K = subsemigroup.comap f.symm.to_mul_hom K

source

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

add_subsemigroup.map f.to_add_hom K = add_subsemigroup.comap f.symm.to_add_hom K

source

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

subsemigroup.comap f.to_mul_hom K = subsemigroup.map f.symm.to_mul_hom K

source

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

add_subsemigroup.comap f.to_add_hom K = add_subsemigroup.map f.symm.to_add_hom K

source

@[simp]

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

subsemigroup.map f.to_mul_hom ⊤ = ⊤

source

@[simp]

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

add_subsemigroup.map f.to_add_hom ⊤ = ⊤

source

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

u ≤ s.prod t ↔ subsemigroup.map (mul_hom.fst M N) u ≤ s ∧ subsemigroup.map (mul_hom.snd M N) u ≤ t

source

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

u ≤ s.prod t ↔ add_subsemigroup.map (add_hom.fst M N) u ≤ s ∧ add_subsemigroup.map (add_hom.snd M N) u ≤ t

source

def add_hom.srange {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :

add_subsemigroup N

The range of an add_hom is an add_subsemigroup.

Equations

f.srange = (add_subsemigroup.map f ⊤).copy (set.range ⇑f) _

source

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

subsemigroup N

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

Equations

f.srange = (subsemigroup.map f ⊤).copy (set.range ⇑f) _

source

@[simp]

theorem add_hom.coe_srange {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :

↑(f.srange) = set.range ⇑f

source

@[simp]

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

↑(f.srange) = set.range ⇑f

source

@[simp]

theorem mul_hom.mem_srange {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f : M →ₙ* N} {y : N} :

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

source

@[simp]

theorem add_hom.mem_srange {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f : add_hom M N} {y : N} :

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

source

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

f.srange = subsemigroup.map f ⊤

source

theorem add_hom.srange_eq_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :

f.srange = add_subsemigroup.map f ⊤

source

theorem add_hom.map_srange {M : Type u_1} {N : Type u_2} {P : Type u_3} [has_add M] [has_add N] [has_add P] (g : add_hom N P) (f : add_hom M N) :

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

source

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

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

source

theorem mul_hom.srange_top_iff_surjective {M : Type u_1} [has_mul M] {N : Type u_2} [has_mul N] {f : M →ₙ* N} :

f.srange = ⊤ ↔ function.surjective ⇑f

source

theorem add_hom.srange_top_iff_surjective {M : Type u_1} [has_add M] {N : Type u_2} [has_add N] {f : add_hom M N} :

f.srange = ⊤ ↔ function.surjective ⇑f

source

theorem mul_hom.srange_top_of_surjective {M : Type u_1} [has_mul M] {N : Type u_2} [has_mul N] (f : M →ₙ* N) (hf : function.surjective ⇑f) :

f.srange = ⊤

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

source

theorem add_hom.srange_top_of_surjective {M : Type u_1} [has_add M] {N : Type u_2} [has_add N] (f : add_hom M N) (hf : function.surjective ⇑f) :

f.srange = ⊤

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

source

theorem mul_hom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (s : set N) :

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

source

theorem add_hom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (s : set N) :

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

source

theorem mul_hom.map_mclosure {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (s : set M) :

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

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

source

theorem add_hom.map_mclosure {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (s : set M) :

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

The image under an add_semigroup hom of the add_subsemigroup generated by a set equals the add_subsemigroup generated by the image of the set.

source

def mul_hom.restrict {M : Type u_1} {σ : Type u_4} [has_mul M] {N : Type u_2} [has_mul N] [set_like σ M] [mul_mem_class σ M] (f : M →ₙ* N) (S : σ) :

↥S →ₙ* N

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

Equations

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

source

def add_hom.restrict {M : Type u_1} {σ : Type u_4} [has_add M] {N : Type u_2} [has_add N] [set_like σ M] [add_mem_class σ M] (f : add_hom M N) (S : σ) :

add_hom ↥S N

Restriction of an add_semigroup hom to an add_subsemigroup of the domain.

Equations

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

source

@[simp]

theorem add_hom.restrict_apply {M : Type u_1} {σ : Type u_4} [has_add M] {N : Type u_2} [has_add N] [set_like σ M] [add_mem_class σ M] (f : add_hom M N) {S : σ} (x : ↥S) :

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

source

@[simp]

theorem mul_hom.restrict_apply {M : Type u_1} {σ : Type u_4} [has_mul M] {N : Type u_2} [has_mul N] [set_like σ M] [mul_mem_class σ M] (f : M →ₙ* N) {S : σ} (x : ↥S) :

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

source

def add_hom.cod_restrict {M : Type u_1} {N : Type u_2} {σ : Type u_4} [has_add M] [has_add N] [set_like σ N] [add_mem_class σ N] (f : add_hom M N) (S : σ) (h : ∀ (x : M), ⇑f x ∈ S) :

add_hom M ↥S

Restriction of an add_semigroup hom to an add_subsemigroup of the codomain.

Equations

f.cod_restrict S h = {to_fun := λ (n : M), ⟨⇑f n, _⟩, map_add' := _}

source

def mul_hom.cod_restrict {M : Type u_1} {N : Type u_2} {σ : Type u_4} [has_mul M] [has_mul N] [set_like σ N] [mul_mem_class σ N] (f : M →ₙ* N) (S : σ) (h : ∀ (x : M), ⇑f x ∈ S) :

M →ₙ* ↥S

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

Equations

f.cod_restrict S h = {to_fun := λ (n : M), ⟨⇑f n, _⟩, map_mul' := _}

source

@[simp]

theorem add_hom.cod_restrict_apply_coe {M : Type u_1} {N : Type u_2} {σ : Type u_4} [has_add M] [has_add N] [set_like σ N] [add_mem_class σ N] (f : add_hom M N) (S : σ) (h : ∀ (x : M), ⇑f x ∈ S) (n : M) :

↑(⇑(f.cod_restrict S h) n) = ⇑f n

source

@[simp]

theorem mul_hom.cod_restrict_apply_coe {M : Type u_1} {N : Type u_2} {σ : Type u_4} [has_mul M] [has_mul N] [set_like σ N] [mul_mem_class σ N] (f : M →ₙ* N) (S : σ) (h : ∀ (x : M), ⇑f x ∈ S) (n : M) :

↑(⇑(f.cod_restrict S h) n) = ⇑f n

source

def mul_hom.srange_restrict {M : Type u_1} [has_mul M] {N : Type u_2} [has_mul N] (f : M →ₙ* N) :

M →ₙ* ↥(f.srange)

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

Equations

f.srange_restrict = f.cod_restrict f.srange _

source

def add_hom.srange_restrict {M : Type u_1} [has_add M] {N : Type u_2} [has_add N] (f : add_hom M N) :

add_hom M ↥(f.srange)

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

Equations

f.srange_restrict = f.cod_restrict f.srange _

source

@[simp]

theorem add_hom.coe_srange_restrict {M : Type u_1} [has_add M] {N : Type u_2} [has_add N] (f : add_hom M N) (x : M) :

↑(⇑(f.srange_restrict) x) = ⇑f x

source

@[simp]

theorem mul_hom.coe_srange_restrict {M : Type u_1} [has_mul M] {N : Type u_2} [has_mul N] (f : M →ₙ* N) (x : M) :

↑(⇑(f.srange_restrict) x) = ⇑f x

source

theorem add_hom.srange_restrict_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) :

function.surjective ⇑(f.srange_restrict)

source

theorem mul_hom.srange_restrict_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) :

function.surjective ⇑(f.srange_restrict)

source

theorem add_hom.sum_map_comap_sum' {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {M' : Type u_3} {N' : Type u_4} [has_add M'] [has_add N'] (f : add_hom M N) (g : add_hom M' N') (S : add_subsemigroup N) (S' : add_subsemigroup N') :

add_subsemigroup.comap (f.prod_map g) (S.prod S') = (add_subsemigroup.comap f S).prod (add_subsemigroup.comap g S')

source

theorem mul_hom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {M' : Type u_3} {N' : Type u_4} [has_mul M'] [has_mul N'] (f : M →ₙ* N) (g : M' →ₙ* N') (S : subsemigroup N) (S' : subsemigroup N') :

subsemigroup.comap (f.prod_map g) (S.prod S') = (subsemigroup.comap f S).prod (subsemigroup.comap g S')

source

@[simp]

theorem add_hom.subsemigroup_comap_apply_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (N' : add_subsemigroup N) (x : ↥(add_subsemigroup.comap f N')) :

↑(⇑(f.subsemigroup_comap N') x) = ⇑f ↑x

source

def add_hom.subsemigroup_comap {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (N' : add_subsemigroup N) :

add_hom ↥(add_subsemigroup.comap f N') ↥N'

the add_hom from the preimage of an additive subsemigroup to itself.

Equations

f.subsemigroup_comap N' = {to_fun := λ (x : ↥(add_subsemigroup.comap f N')), ⟨⇑f ↑x, _⟩, map_add' := _}

source

@[simp]

theorem mul_hom.subsemigroup_comap_apply_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (N' : subsemigroup N) (x : ↥(subsemigroup.comap f N')) :

↑(⇑(f.subsemigroup_comap N') x) = ⇑f ↑x

source

def mul_hom.subsemigroup_comap {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (N' : subsemigroup N) :

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

The mul_hom from the preimage of a subsemigroup to itself.

Equations

f.subsemigroup_comap N' = {to_fun := λ (x : ↥(subsemigroup.comap f N')), ⟨⇑f ↑x, _⟩, map_mul' := _}

source

def mul_hom.subsemigroup_map {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (M' : subsemigroup M) :

↥M' →ₙ* ↥(subsemigroup.map f M')

The mul_hom from a subsemigroup to its image. See mul_equiv.subsemigroup_map for a variant for mul_equivs.

Equations

f.subsemigroup_map M' = {to_fun := λ (x : ↥M'), ⟨⇑f ↑x, _⟩, map_mul' := _}

source

def add_hom.subsemigroup_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (M' : add_subsemigroup M) :

add_hom ↥M' ↥(add_subsemigroup.map f M')

the add_hom from an additive subsemigroup to its image. See add_equiv.add_subsemigroup_map for a variant for add_equivs.

Equations

f.subsemigroup_map M' = {to_fun := λ (x : ↥M'), ⟨⇑f ↑x, _⟩, map_add' := _}

source

@[simp]

theorem add_hom.subsemigroup_map_apply_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (M' : add_subsemigroup M) (x : ↥M') :

↑(⇑(f.subsemigroup_map M') x) = ⇑f ↑x

source

@[simp]

theorem mul_hom.subsemigroup_map_apply_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (M' : subsemigroup M) (x : ↥M') :

↑(⇑(f.subsemigroup_map M') x) = ⇑f ↑x

source

theorem mul_hom.subsemigroup_map_surjective {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (M' : subsemigroup M) :

function.surjective ⇑(f.subsemigroup_map M')

source

theorem add_hom.subsemigroup_map_surjective {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (M' : add_subsemigroup M) :

function.surjective ⇑(f.subsemigroup_map M')

source

@[simp]

theorem subsemigroup.srange_fst {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] [nonempty N] :

(mul_hom.fst M N).srange = ⊤

source

@[simp]

theorem add_subsemigroup.srange_fst {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] [nonempty N] :

(add_hom.fst M N).srange = ⊤

source

@[simp]

theorem add_subsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] [nonempty M] :

(add_hom.snd M N).srange = ⊤

source

@[simp]

theorem subsemigroup.srange_snd {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] [nonempty M] :

(mul_hom.snd M N).srange = ⊤

source

theorem subsemigroup.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] [nonempty M] [nonempty N] {s : subsemigroup M} {t : subsemigroup N} :

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

source

theorem add_subsemigroup.sum_eq_top_iff {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] [nonempty M] [nonempty N] {s : add_subsemigroup M} {t : add_subsemigroup N} :

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

source

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

add_hom ↥S ↥T

The add_semigroup hom associated to an inclusion of subsemigroups.

Equations

add_subsemigroup.inclusion h = (add_mem_class.subtype S).cod_restrict T _

source

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

↥S →ₙ* ↥T

The semigroup hom associated to an inclusion of subsemigroups.

Equations

subsemigroup.inclusion h = (mul_mem_class.subtype S).cod_restrict T _

source

@[simp]

theorem add_subsemigroup.range_subtype {M : Type u_1} [has_add M] (s : add_subsemigroup M) :

(add_mem_class.subtype s).srange = s

source

@[simp]

theorem subsemigroup.range_subtype {M : Type u_1} [has_mul M] (s : subsemigroup M) :

(mul_mem_class.subtype s).srange = s

source

theorem subsemigroup.eq_top_iff' {M : Type u_1} [has_mul M] (S : subsemigroup M) :

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

source

theorem add_subsemigroup.eq_top_iff' {M : Type u_1} [has_add M] (S : add_subsemigroup M) :

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

source

def mul_equiv.subsemigroup_congr {M : Type u_1} [has_mul M] {S T : subsemigroup M} (h : S = T) :

↥S ≃* ↥T

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

Equations

mul_equiv.subsemigroup_congr h = {to_fun := (equiv.set_congr _).to_fun, inv_fun := (equiv.set_congr _).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

def add_equiv.subsemigroup_congr {M : Type u_1} [has_add M] {S T : add_subsemigroup M} (h : S = T) :

↥S ≃+ ↥T

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

Equations

add_equiv.subsemigroup_congr h = {to_fun := (equiv.set_congr _).to_fun, inv_fun := (equiv.set_congr _).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

@[simp]

theorem add_equiv.of_left_inverse_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) {g : N → M} (h : function.left_inverse g ⇑f) (ᾰ : M) :

⇑(add_equiv.of_left_inverse f h) ᾰ = ⇑(f.srange_restrict) ᾰ

source

def add_equiv.of_left_inverse {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) {g : N → M} (h : function.left_inverse g ⇑f) :

M ≃+ ↥(f.srange)

An additive semigroup homomorphism f : M →+ N with a left-inverse g : N → M defines an additive equivalence between M and f.srange.

This is a bidirectional version of add_hom.srange_restrict.

Equations

add_equiv.of_left_inverse f h = {to_fun := ⇑(f.srange_restrict), inv_fun := g ∘ ⇑(add_mem_class.subtype f.srange), left_inv := h, right_inv := _, map_add' := _}

source

def mul_equiv.of_left_inverse {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) {g : N → M} (h : function.left_inverse g ⇑f) :

M ≃* ↥(f.srange)

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

This is a bidirectional version of mul_hom.srange_restrict.

Equations

mul_equiv.of_left_inverse f h = {to_fun := ⇑(f.srange_restrict), inv_fun := g ∘ ⇑(mul_mem_class.subtype f.srange), left_inv := h, right_inv := _, map_mul' := _}

source

@[simp]

theorem mul_equiv.of_left_inverse_symm_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) {g : N → M} (h : function.left_inverse g ⇑f) (ᾰ : ↥(f.srange)) :

⇑((mul_equiv.of_left_inverse f h).symm) ᾰ = g ↑ᾰ

source

@[simp]

theorem add_equiv.of_left_inverse_symm_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) {g : N → M} (h : function.left_inverse g ⇑f) (ᾰ : ↥(f.srange)) :

⇑((add_equiv.of_left_inverse f h).symm) ᾰ = g ↑ᾰ

source

@[simp]

theorem mul_equiv.of_left_inverse_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) {g : N → M} (h : function.left_inverse g ⇑f) (ᾰ : M) :

⇑(mul_equiv.of_left_inverse f h) ᾰ = ⇑(f.srange_restrict) ᾰ

source

@[simp]

theorem mul_equiv.subsemigroup_map_apply_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (e : M ≃* N) (S : subsemigroup M) (x : ↥S) :

↑(⇑(e.subsemigroup_map S) x) = ⇑e ↑x

source

def add_equiv.subsemigroup_map {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (e : M ≃+ N) (S : add_subsemigroup M) :

↥S ≃+ ↥(add_subsemigroup.map e.to_add_hom S)

An add_equiv φ between two additive semigroups M and N induces an add_equiv between a subsemigroup S ≤ M and the subsemigroup φ(S) ≤ N. See add_hom.add_subsemigroup_map for a variant for add_homs.

Equations

e.subsemigroup_map S = {to_fun := λ (x : ↥S), ⟨⇑e ↑x, _⟩, inv_fun := λ (x : ↥(add_subsemigroup.map e.to_add_hom S)), ⟨⇑(e.symm) ↑x, _⟩, left_inv := _, right_inv := _, map_add' := _}

source

@[simp]

theorem add_equiv.subsemigroup_map_symm_apply_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (e : M ≃+ N) (S : add_subsemigroup M) (x : ↥(add_subsemigroup.map e.to_add_hom S)) :

↑(⇑((e.subsemigroup_map S).symm) x) = ⇑(e.symm) ↑x

source

@[simp]

theorem mul_equiv.subsemigroup_map_symm_apply_coe {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (e : M ≃* N) (S : subsemigroup M) (x : ↥(subsemigroup.map e.to_mul_hom S)) :

↑(⇑((e.subsemigroup_map S).symm) x) = ⇑(e.symm) ↑x

source

def mul_equiv.subsemigroup_map {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (e : M ≃* N) (S : subsemigroup M) :

↥S ≃* ↥(subsemigroup.map e.to_mul_hom S)

A mul_equiv φ between two semigroups M and N induces a mul_equiv between a subsemigroup S ≤ M and the subsemigroup φ(S) ≤ N. See mul_hom.subsemigroup_map for a variant for mul_homs.

Equations

e.subsemigroup_map S = {to_fun := λ (x : ↥S), ⟨⇑e ↑x, _⟩, inv_fun := λ (x : ↥(subsemigroup.map e.to_mul_hom S)), ⟨⇑(e.symm) ↑x, _⟩, left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem add_equiv.subsemigroup_map_apply_coe {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (e : M ≃+ N) (S : add_subsemigroup M) (x : ↥S) :

↑(⇑(e.subsemigroup_map S) x) = ⇑e ↑x

mathlib3 documentation

Operations on `subsemigroup`s #

Main definitions #

Conversion between multiplicative and additive definitions #

(Commutative) semigroup structure on a subsemigroup #

Operations on subsemigroups #

Semigroup homomorphisms between subsemigroups #

Operations on `mul_hom`s #

Implementation notes #

Tags #

Conversion to/from `additive`/`multiplicative` #

`comap` and `map` #

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