group_theory.submonoid.operations

source

@[simp]

theorem submonoid.to_add_submonoid_apply_coe {M : Type u_1} [mul_one_class M] (S : submonoid M) :

↑(⇑submonoid.to_add_submonoid S) = ⇑additive.to_mul ⁻¹' ↑S

source

@[simp]

theorem submonoid.to_add_submonoid_symm_apply_coe {M : Type u_1} [mul_one_class M] (S : add_submonoid (additive M)) :

↑(⇑(rel_iso.symm submonoid.to_add_submonoid) S) = ⇑additive.of_mul ⁻¹' ↑S

source

def submonoid.to_add_submonoid {M : Type u_1} [mul_one_class M] :

submonoid M ≃o add_submonoid (additive M)

Submonoids of monoid M are isomorphic to additive submonoids of additive M.

Equations

submonoid.to_add_submonoid = {to_equiv := {to_fun := λ (S : submonoid M), {carrier := ⇑additive.to_mul ⁻¹' ↑S, add_mem' := _, zero_mem' := _}, inv_fun := λ (S : add_submonoid (additive M)), {carrier := ⇑additive.of_mul ⁻¹' ↑S, mul_mem' := _, one_mem' := _}, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[reducible]

def add_submonoid.to_submonoid' {M : Type u_1} [mul_one_class M] :

add_submonoid (additive M) ≃o submonoid M

Additive submonoids of an additive monoid additive M are isomorphic to submonoids of M.

source

theorem submonoid.to_add_submonoid_closure {M : Type u_1} [mul_one_class M] (S : set M) :

⇑submonoid.to_add_submonoid (submonoid.closure S) = add_submonoid.closure (⇑additive.to_mul ⁻¹' S)

source

theorem add_submonoid.to_submonoid'_closure {M : Type u_1} [mul_one_class M] (S : set (additive M)) :

⇑add_submonoid.to_submonoid' (add_submonoid.closure S) = submonoid.closure (⇑multiplicative.of_add ⁻¹' S)

source

@[simp]

theorem add_submonoid.to_submonoid_symm_apply_coe {A : Type u_4} [add_zero_class A] (S : submonoid (multiplicative A)) :

↑(⇑(rel_iso.symm add_submonoid.to_submonoid) S) = ⇑multiplicative.of_add ⁻¹' ↑S

source

@[simp]

theorem add_submonoid.to_submonoid_apply_coe {A : Type u_4} [add_zero_class A] (S : add_submonoid A) :

↑(⇑add_submonoid.to_submonoid S) = ⇑multiplicative.to_add ⁻¹' ↑S

source

def add_submonoid.to_submonoid {A : Type u_4} [add_zero_class A] :

add_submonoid A ≃o submonoid (multiplicative A)

Additive submonoids of an additive monoid A are isomorphic to multiplicative submonoids of multiplicative A.

Equations

add_submonoid.to_submonoid = {to_equiv := {to_fun := λ (S : add_submonoid A), {carrier := ⇑multiplicative.to_add ⁻¹' ↑S, mul_mem' := _, one_mem' := _}, inv_fun := λ (S : submonoid (multiplicative A)), {carrier := ⇑multiplicative.of_add ⁻¹' ↑S, add_mem' := _, zero_mem' := _}, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[reducible]

def submonoid.to_add_submonoid' {A : Type u_4} [add_zero_class A] :

submonoid (multiplicative A) ≃o add_submonoid A

Submonoids of a monoid multiplicative A are isomorphic to additive submonoids of A.

source

theorem add_submonoid.to_submonoid_closure {A : Type u_4} [add_zero_class A] (S : set A) :

⇑add_submonoid.to_submonoid (add_submonoid.closure S) = submonoid.closure (⇑multiplicative.to_add ⁻¹' S)

source

theorem submonoid.to_add_submonoid'_closure {A : Type u_4} [add_zero_class A] (S : set (multiplicative A)) :

⇑submonoid.to_add_submonoid' (submonoid.closure S) = add_submonoid.closure (⇑additive.of_mul ⁻¹' S)

source

def submonoid.comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) (S : submonoid N) :

submonoid M

The preimage of a submonoid along a monoid homomorphism is a submonoid.

Equations

submonoid.comap f S = {carrier := ⇑f ⁻¹' ↑S, mul_mem' := _, one_mem' := _}

source

def add_submonoid.comap {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) (S : add_submonoid N) :

add_submonoid M

The preimage of an add_submonoid along an add_monoid homomorphism is an add_submonoid.

Equations

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

source

@[simp]

theorem submonoid.coe_comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (S : submonoid N) (f : F) :

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

source

@[simp]

theorem add_submonoid.coe_comap {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (S : add_submonoid N) (f : F) :

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

source

@[simp]

theorem submonoid.mem_comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {S : submonoid N} {f : F} {x : M} :

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

source

@[simp]

theorem add_submonoid.mem_comap {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {S : add_submonoid N} {f : F} {x : M} :

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

source

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

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

source

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

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

source

@[simp]

theorem submonoid.comap_id {P : Type u_3} [mul_one_class P] (S : submonoid P) :

submonoid.comap (monoid_hom.id P) S = S

source

@[simp]

theorem add_submonoid.comap_id {P : Type u_3} [add_zero_class P] (S : add_submonoid P) :

add_submonoid.comap (add_monoid_hom.id P) S = S

source

def submonoid.map {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) (S : submonoid M) :

submonoid N

The image of a submonoid along a monoid homomorphism is a submonoid.

Equations

submonoid.map f S = {carrier := ⇑f '' ↑S, mul_mem' := _, one_mem' := _}

source

def add_submonoid.map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) (S : add_submonoid M) :

add_submonoid N

The image of an add_submonoid along an add_monoid homomorphism is an add_submonoid.

Equations

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

source

@[simp]

theorem submonoid.coe_map {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) (S : submonoid M) :

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

source

@[simp]

theorem add_submonoid.coe_map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) (S : add_submonoid M) :

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

source

@[simp]

theorem add_submonoid.mem_map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} {S : add_submonoid M} {y : N} :

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

source

@[simp]

theorem submonoid.mem_map {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} {S : submonoid M} {y : N} :

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

source

theorem submonoid.mem_map_of_mem {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) {S : submonoid M} {x : M} (hx : x ∈ S) :

⇑f x ∈ submonoid.map f S

source

theorem add_submonoid.mem_map_of_mem {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) {S : add_submonoid M} {x : M} (hx : x ∈ S) :

⇑f x ∈ add_submonoid.map f S

source

theorem add_submonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) (S : add_submonoid M) (x : ↥S) :

⇑f ↑x ∈ add_submonoid.map f S

source

theorem submonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) (S : submonoid M) (x : ↥S) :

⇑f ↑x ∈ submonoid.map f S

source

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

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

source

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

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

source

theorem add_submonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) {S : add_submonoid M} {x : M} :

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

source

theorem submonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) {S : submonoid M} {x : M} :

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

source

theorem add_submonoid.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} {S : add_submonoid M} {T : add_submonoid N} :

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

source

theorem submonoid.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} {S : submonoid M} {T : submonoid N} :

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

source

theorem submonoid.gc_map_comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) :

galois_connection (submonoid.map f) (submonoid.comap f)

source

theorem add_submonoid.gc_map_comap {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) :

galois_connection (add_submonoid.map f) (add_submonoid.comap f)

source

theorem submonoid.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (S : submonoid M) {F : Type u_4} [mc : monoid_hom_class F M N] {T : submonoid N} {f : F} :

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

source

theorem add_submonoid.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (S : add_submonoid M) {F : Type u_4} [mc : add_monoid_hom_class F M N] {T : add_submonoid N} {f : F} :

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

source

theorem submonoid.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (S : submonoid M) {F : Type u_4} [mc : monoid_hom_class F M N] {T : submonoid N} {f : F} :

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

source

theorem add_submonoid.le_comap_of_map_le {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (S : add_submonoid M) {F : Type u_4} [mc : add_monoid_hom_class F M N] {T : add_submonoid N} {f : F} :

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

source

theorem submonoid.le_comap_map {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (S : submonoid M) {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} :

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

source

theorem add_submonoid.le_comap_map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (S : add_submonoid M) {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} :

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

source

theorem add_submonoid.map_comap_le {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {S : add_submonoid N} {f : F} :

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

source

theorem submonoid.map_comap_le {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {S : submonoid N} {f : F} :

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

source

theorem add_submonoid.monotone_map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} :

monotone (add_submonoid.map f)

source

theorem submonoid.monotone_map {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} :

monotone (submonoid.map f)

source

theorem add_submonoid.monotone_comap {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} :

monotone (add_submonoid.comap f)

source

theorem submonoid.monotone_comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} :

monotone (submonoid.comap f)

source

@[simp]

theorem submonoid.map_comap_map {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (S : submonoid M) {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} :

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

source

@[simp]

theorem add_submonoid.map_comap_map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (S : add_submonoid M) {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} :

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

source

@[simp]

theorem add_submonoid.comap_map_comap {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {S : add_submonoid N} {f : F} :

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

source

@[simp]

theorem submonoid.comap_map_comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {S : submonoid N} {f : F} :

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

source

theorem submonoid.map_sup {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (S T : submonoid M) (f : F) :

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

source

theorem add_submonoid.map_sup {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (S T : add_submonoid M) (f : F) :

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

source

theorem submonoid.map_supr {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {ι : Sort u_3} (f : F) (s : ι → submonoid M) :

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

source

theorem add_submonoid.map_supr {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {ι : Sort u_3} (f : F) (s : ι → add_submonoid M) :

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

source

theorem submonoid.comap_inf {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (S T : submonoid N) (f : F) :

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

source

theorem add_submonoid.comap_inf {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (S T : add_submonoid N) (f : F) :

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

source

theorem submonoid.comap_infi {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {ι : Sort u_3} (f : F) (s : ι → submonoid N) :

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

source

theorem add_submonoid.comap_infi {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {ι : Sort u_3} (f : F) (s : ι → add_submonoid N) :

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

source

@[simp]

theorem submonoid.map_bot {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) :

submonoid.map f ⊥ = ⊥

source

@[simp]

theorem add_submonoid.map_bot {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) :

add_submonoid.map f ⊥ = ⊥

source

@[simp]

theorem add_submonoid.comap_top {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) :

add_submonoid.comap f ⊤ = ⊤

source

@[simp]

theorem submonoid.comap_top {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) :

submonoid.comap f ⊤ = ⊤

source

@[simp]

theorem add_submonoid.map_id {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

add_submonoid.map (add_monoid_hom.id M) S = S

source

@[simp]

theorem submonoid.map_id {M : Type u_1} [mul_one_class M] (S : submonoid M) :

submonoid.map (monoid_hom.id M) S = S

source

def add_submonoid.gci_map_comap {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) :

galois_coinsertion (add_submonoid.map f) (add_submonoid.comap f)

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

Equations

add_submonoid.gci_map_comap hf = _.to_galois_coinsertion _

source

def submonoid.gci_map_comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) :

galois_coinsertion (submonoid.map f) (submonoid.comap f)

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

Equations

submonoid.gci_map_comap hf = _.to_galois_coinsertion _

source

theorem add_submonoid.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) (S : add_submonoid M) :

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

source

theorem submonoid.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) (S : submonoid M) :

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

source

theorem add_submonoid.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) :

function.surjective (add_submonoid.comap f)

source

theorem submonoid.comap_surjective_of_injective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) :

function.surjective (submonoid.comap f)

source

theorem submonoid.map_injective_of_injective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) :

function.injective (submonoid.map f)

source

theorem add_submonoid.map_injective_of_injective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) :

function.injective (add_submonoid.map f)

source

theorem add_submonoid.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) (S T : add_submonoid M) :

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

source

theorem submonoid.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) (S T : submonoid M) :

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

source

theorem submonoid.comap_infi_map_of_injective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {ι : Type u_5} {f : F} (hf : function.injective ⇑f) (S : ι → submonoid M) :

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

source

theorem add_submonoid.comap_infi_map_of_injective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {ι : Type u_5} {f : F} (hf : function.injective ⇑f) (S : ι → add_submonoid M) :

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

source

theorem add_submonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) (S T : add_submonoid M) :

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

source

theorem submonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) (S T : submonoid M) :

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

source

theorem submonoid.comap_supr_map_of_injective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {ι : Type u_5} {f : F} (hf : function.injective ⇑f) (S : ι → submonoid M) :

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

source

theorem add_submonoid.comap_supr_map_of_injective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {ι : Type u_5} {f : F} (hf : function.injective ⇑f) (S : ι → add_submonoid M) :

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

source

theorem submonoid.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) {S T : submonoid M} :

submonoid.map f S ≤ submonoid.map f T ↔ S ≤ T

source

theorem add_submonoid.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) {S T : add_submonoid M} :

add_submonoid.map f S ≤ add_submonoid.map f T ↔ S ≤ T

source

theorem add_submonoid.map_strict_mono_of_injective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) :

strict_mono (add_submonoid.map f)

source

theorem submonoid.map_strict_mono_of_injective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.injective ⇑f) :

strict_mono (submonoid.map f)

source

def submonoid.gi_map_comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) :

galois_insertion (submonoid.map f) (submonoid.comap f)

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

Equations

submonoid.gi_map_comap hf = _.to_galois_insertion _

source

def add_submonoid.gi_map_comap {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) :

galois_insertion (add_submonoid.map f) (add_submonoid.comap f)

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

Equations

add_submonoid.gi_map_comap hf = _.to_galois_insertion _

source

theorem add_submonoid.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) (S : add_submonoid N) :

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

source

theorem submonoid.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) (S : submonoid N) :

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

source

theorem submonoid.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) :

function.surjective (submonoid.map f)

source

theorem add_submonoid.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) :

function.surjective (add_submonoid.map f)

source

theorem add_submonoid.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) :

function.injective (add_submonoid.comap f)

source

theorem submonoid.comap_injective_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) :

function.injective (submonoid.comap f)

source

theorem add_submonoid.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) (S T : add_submonoid N) :

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

source

theorem submonoid.map_inf_comap_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) (S T : submonoid N) :

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

source

theorem add_submonoid.map_infi_comap_of_surjective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {ι : Type u_5} {f : F} (hf : function.surjective ⇑f) (S : ι → add_submonoid N) :

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

source

theorem submonoid.map_infi_comap_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {ι : Type u_5} {f : F} (hf : function.surjective ⇑f) (S : ι → submonoid N) :

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

source

theorem submonoid.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) (S T : submonoid N) :

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

source

theorem add_submonoid.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) (S T : add_submonoid N) :

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

source

theorem submonoid.map_supr_comap_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {ι : Type u_5} {f : F} (hf : function.surjective ⇑f) (S : ι → submonoid N) :

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

source

theorem add_submonoid.map_supr_comap_of_surjective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {ι : Type u_5} {f : F} (hf : function.surjective ⇑f) (S : ι → add_submonoid N) :

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

source

theorem add_submonoid.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) {S T : add_submonoid N} :

add_submonoid.comap f S ≤ add_submonoid.comap f T ↔ S ≤ T

source

theorem submonoid.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) {S T : submonoid N} :

submonoid.comap f S ≤ submonoid.comap f T ↔ S ≤ T

source

theorem add_submonoid.comap_strict_mono_of_surjective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) :

strict_mono (add_submonoid.comap f)

source

theorem submonoid.comap_strict_mono_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} (hf : function.surjective ⇑f) :

strict_mono (submonoid.comap f)

source

@[protected, instance]

def one_mem_class.has_one {A : Type u_4} {M₁ : Type u_5} [set_like A M₁] [has_one M₁] [hA : one_mem_class A M₁] (S' : A) :

has_one ↥S'

A submonoid of a monoid inherits a 1.

Equations

one_mem_class.has_one S' = {one := ⟨1, _⟩}

source

@[protected, instance]

def zero_mem_class.has_zero {A : Type u_4} {M₁ : Type u_5} [set_like A M₁] [has_zero M₁] [hA : zero_mem_class A M₁] (S' : A) :

has_zero ↥S'

An add_submonoid of an add_monoid inherits a zero.

Equations

zero_mem_class.has_zero S' = {zero := ⟨0, _⟩}

source

@[simp, norm_cast]

theorem zero_mem_class.coe_zero {A : Type u_4} {M₁ : Type u_5} [set_like A M₁] [has_zero M₁] [hA : zero_mem_class A M₁] (S' : A) :

↑0 = 0

source

@[simp, norm_cast]

theorem one_mem_class.coe_one {A : Type u_4} {M₁ : Type u_5} [set_like A M₁] [has_one M₁] [hA : one_mem_class A M₁] (S' : A) :

↑1 = 1

source

@[simp, norm_cast]

theorem zero_mem_class.coe_eq_zero {A : Type u_4} {M₁ : Type u_5} [set_like A M₁] [has_zero M₁] [hA : zero_mem_class A M₁] {S' : A} {x : ↥S'} :

↑x = 0 ↔ x = 0

source

@[simp, norm_cast]

theorem one_mem_class.coe_eq_one {A : Type u_4} {M₁ : Type u_5} [set_like A M₁] [has_one M₁] [hA : one_mem_class A M₁] {S' : A} {x : ↥S'} :

↑x = 1 ↔ x = 1

source

theorem zero_mem_class.zero_def {A : Type u_4} {M₁ : Type u_5} [set_like A M₁] [has_zero M₁] [hA : zero_mem_class A M₁] (S' : A) :

0 = ⟨0, _⟩

source

theorem one_mem_class.one_def {A : Type u_4} {M₁ : Type u_5} [set_like A M₁] [has_one M₁] [hA : one_mem_class A M₁] (S' : A) :

1 = ⟨1, _⟩

source

@[protected, instance]

def add_submonoid_class.has_nsmul {M : Type u_1} [add_monoid M] {A : Type u_2} [set_like A M] [add_submonoid_class A M] (S : A) :

has_smul ℕ ↥S

An add_submonoid of an add_monoid inherits a scalar multiplication.

Equations

add_submonoid_class.has_nsmul S = {smul := λ (n : ℕ) (a : ↥S), ⟨n • a.val, _⟩}

source

@[protected, instance]

def submonoid_class.has_pow {M : Type u_1} [monoid M] {A : Type u_2} [set_like A M] [submonoid_class A M] (S : A) :

has_pow ↥S ℕ

A submonoid of a monoid inherits a power operator.

Equations

submonoid_class.has_pow S = {pow := λ (a : ↥S) (n : ℕ), ⟨a.val ^ n, _⟩}

source

@[simp, norm_cast]

theorem add_submonoid_class.coe_nsmul {M : Type u_1} [add_monoid M] {A : Type u_2} [set_like A M] [add_submonoid_class A M] {S : A} (x : ↥S) (n : ℕ) :

↑(n • x) = n • ↑x

source

@[simp, norm_cast]

theorem submonoid_class.coe_pow {M : Type u_1} [monoid M] {A : Type u_2} [set_like A M] [submonoid_class A M] {S : A} (x : ↥S) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

source

@[simp]

theorem add_submonoid_class.mk_nsmul {M : Type u_1} [add_monoid M] {A : Type u_2} [set_like A M] [add_submonoid_class A M] {S : A} (x : M) (hx : x ∈ S) (n : ℕ) :

n • ⟨x, hx⟩ = ⟨n • x, _⟩

source

@[simp]

theorem submonoid_class.mk_pow {M : Type u_1} [monoid M] {A : Type u_2} [set_like A M] [submonoid_class A M] {S : A} (x : M) (hx : x ∈ S) (n : ℕ) :

⟨x, hx⟩ ^ n = ⟨x ^ n, _⟩

source

@[protected, instance]

def add_submonoid_class.to_add_zero_class {M : Type u_1} [add_zero_class M] {A : Type u_2} [set_like A M] [add_submonoid_class A M] (S : A) :

add_zero_class ↥S

An add_submonoid of an unital additive magma inherits an unital additive magma structure.

Equations

add_submonoid_class.to_add_zero_class S = function.injective.add_zero_class coe _ _ _

source

@[protected, instance]

def submonoid_class.to_mul_one_class {M : Type u_1} [mul_one_class M] {A : Type u_2} [set_like A M] [submonoid_class A M] (S : A) :

mul_one_class ↥S

A submonoid of a unital magma inherits a unital magma structure.

Equations

submonoid_class.to_mul_one_class S = function.injective.mul_one_class coe _ _ _

source

@[protected, instance]

def submonoid_class.to_monoid {M : Type u_1} [monoid M] {A : Type u_2} [set_like A M] [submonoid_class A M] (S : A) :

monoid ↥S

A submonoid of a monoid inherits a monoid structure.

Equations

submonoid_class.to_monoid S = function.injective.monoid coe _ _ _ _

source

@[protected, instance]

def add_submonoid_class.to_add_monoid {M : Type u_1} [add_monoid M] {A : Type u_2} [set_like A M] [add_submonoid_class A M] (S : A) :

add_monoid ↥S

An add_submonoid of an add_monoid inherits an add_monoid structure.

Equations

add_submonoid_class.to_add_monoid S = function.injective.add_monoid coe _ _ _ _

source

@[protected, instance]

def submonoid_class.to_comm_monoid {M : Type u_1} [comm_monoid M] {A : Type u_2} [set_like A M] [submonoid_class A M] (S : A) :

comm_monoid ↥S

A submonoid of a comm_monoid is a comm_monoid.

Equations

submonoid_class.to_comm_monoid S = function.injective.comm_monoid coe _ _ _ _

source

@[protected, instance]

def add_submonoid_class.to_add_comm_monoid {M : Type u_1} [add_comm_monoid M] {A : Type u_2} [set_like A M] [add_submonoid_class A M] (S : A) :

add_comm_monoid ↥S

An add_submonoid of an add_comm_monoid is an add_comm_monoid.

Equations

add_submonoid_class.to_add_comm_monoid S = function.injective.add_comm_monoid coe _ _ _ _

source

@[protected, instance]

def add_submonoid_class.to_ordered_add_comm_monoid {M : Type u_1} [ordered_add_comm_monoid M] {A : Type u_2} [set_like A M] [add_submonoid_class A M] (S : A) :

ordered_add_comm_monoid ↥S

An add_submonoid of an ordered_add_comm_monoid is an ordered_add_comm_monoid.

Equations

add_submonoid_class.to_ordered_add_comm_monoid S = function.injective.ordered_add_comm_monoid coe _ _ _ _

source

@[protected, instance]

def submonoid_class.to_ordered_comm_monoid {M : Type u_1} [ordered_comm_monoid M] {A : Type u_2} [set_like A M] [submonoid_class A M] (S : A) :

ordered_comm_monoid ↥S

A submonoid of an ordered_comm_monoid is an ordered_comm_monoid.

Equations

submonoid_class.to_ordered_comm_monoid S = function.injective.ordered_comm_monoid coe _ _ _ _

source

@[protected, instance]

def add_submonoid_class.to_linear_ordered_add_comm_monoid {M : Type u_1} [linear_ordered_add_comm_monoid M] {A : Type u_2} [set_like A M] [add_submonoid_class A M] (S : A) :

linear_ordered_add_comm_monoid ↥S

An add_submonoid of a linear_ordered_add_comm_monoid is a linear_ordered_add_comm_monoid.

Equations

add_submonoid_class.to_linear_ordered_add_comm_monoid S = function.injective.linear_ordered_add_comm_monoid coe _ _ _ _ _ _

source

@[protected, instance]

def submonoid_class.to_linear_ordered_comm_monoid {M : Type u_1} [linear_ordered_comm_monoid M] {A : Type u_2} [set_like A M] [submonoid_class A M] (S : A) :

linear_ordered_comm_monoid ↥S

A submonoid of a linear_ordered_comm_monoid is a linear_ordered_comm_monoid.

Equations

submonoid_class.to_linear_ordered_comm_monoid S = function.injective.linear_ordered_comm_monoid coe _ _ _ _ _ _

source

@[protected, instance]

def add_submonoid_class.to_ordered_cancel_add_comm_monoid {M : Type u_1} [ordered_cancel_add_comm_monoid M] {A : Type u_2} [set_like A M] [add_submonoid_class A M] (S : A) :

ordered_cancel_add_comm_monoid ↥S

An add_submonoid of an ordered_cancel_add_comm_monoid is an ordered_cancel_add_comm_monoid.

Equations

add_submonoid_class.to_ordered_cancel_add_comm_monoid S = function.injective.ordered_cancel_add_comm_monoid coe _ _ _ _

source

@[protected, instance]

def submonoid_class.to_ordered_cancel_comm_monoid {M : Type u_1} [ordered_cancel_comm_monoid M] {A : Type u_2} [set_like A M] [submonoid_class A M] (S : A) :

ordered_cancel_comm_monoid ↥S

A submonoid of an ordered_cancel_comm_monoid is an ordered_cancel_comm_monoid.

Equations

submonoid_class.to_ordered_cancel_comm_monoid S = function.injective.ordered_cancel_comm_monoid coe _ _ _ _

source

@[protected, instance]

def submonoid_class.to_linear_ordered_cancel_comm_monoid {M : Type u_1} [linear_ordered_cancel_comm_monoid M] {A : Type u_2} [set_like A M] [submonoid_class A M] (S : A) :

linear_ordered_cancel_comm_monoid ↥S

A submonoid of a linear_ordered_cancel_comm_monoid is a linear_ordered_cancel_comm_monoid.

Equations

submonoid_class.to_linear_ordered_cancel_comm_monoid S = function.injective.linear_ordered_cancel_comm_monoid coe _ _ _ _ _ _

source

@[protected, instance]

def add_submonoid_class.to_linear_ordered_cancel_add_comm_monoid {M : Type u_1} [linear_ordered_cancel_add_comm_monoid M] {A : Type u_2} [set_like A M] [add_submonoid_class A M] (S : A) :

linear_ordered_cancel_add_comm_monoid ↥S

An add_submonoid of a linear_ordered_cancel_add_comm_monoid is a linear_ordered_cancel_add_comm_monoid.

Equations

add_submonoid_class.to_linear_ordered_cancel_add_comm_monoid S = function.injective.linear_ordered_cancel_add_comm_monoid coe _ _ _ _ _ _

source

def submonoid_class.subtype {M : Type u_1} [mul_one_class M] {A : Type u_4} [set_like A M] [hA : submonoid_class A M] (S' : A) :

↥S' →* M

The natural monoid hom from a submonoid of monoid M to M.

Equations

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

source

def add_submonoid_class.subtype {M : Type u_1} [add_zero_class M] {A : Type u_4} [set_like A M] [hA : add_submonoid_class A M] (S' : A) :

↥S' →+ M

The natural monoid hom from an add_submonoid of add_monoid M to M.

Equations

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

source

@[simp]

theorem add_submonoid_class.coe_subtype {M : Type u_1} [add_zero_class M] {A : Type u_4} [set_like A M] [hA : add_submonoid_class A M] (S' : A) :

⇑(add_submonoid_class.subtype S') = coe

source

@[simp]

theorem submonoid_class.coe_subtype {M : Type u_1} [mul_one_class M] {A : Type u_4} [set_like A M] [hA : submonoid_class A M] (S' : A) :

⇑(submonoid_class.subtype S') = coe

source

@[protected, instance]

def submonoid.has_mul {M : Type u_1} [mul_one_class M] (S : submonoid M) :

has_mul ↥S

A submonoid of a monoid inherits a multiplication.

Equations

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

source

@[protected, instance]

def add_submonoid.has_add {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

has_add ↥S

An add_submonoid of an add_monoid inherits an addition.

Equations

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

source

@[protected, instance]

def submonoid.has_one {M : Type u_1} [mul_one_class M] (S : submonoid M) :

has_one ↥S

A submonoid of a monoid inherits a 1.

Equations

S.has_one = {one := ⟨1, _⟩}

source

@[protected, instance]

def add_submonoid.has_zero {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

has_zero ↥S

An add_submonoid of an add_monoid inherits a zero.

Equations

S.has_zero = {zero := ⟨0, _⟩}

source

@[simp, norm_cast]

theorem submonoid.coe_mul {M : Type u_1} [mul_one_class M] (S : submonoid M) (x y : ↥S) :

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

source

@[simp, norm_cast]

theorem add_submonoid.coe_add {M : Type u_1} [add_zero_class M] (S : add_submonoid M) (x y : ↥S) :

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

source

@[simp, norm_cast]

theorem add_submonoid.coe_zero {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

↑0 = 0

source

@[simp, norm_cast]

theorem submonoid.coe_one {M : Type u_1} [mul_one_class M] (S : submonoid M) :

↑1 = 1

source

@[simp]

theorem submonoid.mk_mul_mk {M : Type u_1} [mul_one_class M] (S : submonoid M) (x y : M) (hx : x ∈ S) (hy : y ∈ S) :

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

source

@[simp]

theorem add_submonoid.mk_add_mk {M : Type u_1} [add_zero_class M] (S : add_submonoid M) (x y : M) (hx : x ∈ S) (hy : y ∈ S) :

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

source

theorem submonoid.mul_def {M : Type u_1} [mul_one_class M] (S : submonoid M) (x y : ↥S) :

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

source

theorem add_submonoid.add_def {M : Type u_1} [add_zero_class M] (S : add_submonoid M) (x y : ↥S) :

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

source

theorem submonoid.one_def {M : Type u_1} [mul_one_class M] (S : submonoid M) :

1 = ⟨1, _⟩

source

theorem add_submonoid.zero_def {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

0 = ⟨0, _⟩

source

@[protected, instance]

def add_submonoid.to_add_zero_class {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

add_zero_class ↥S

An add_submonoid of an unital additive magma inherits an unital additive magma structure.

Equations

S.to_add_zero_class = function.injective.add_zero_class coe _ _ _

source

@[protected, instance]

def submonoid.to_mul_one_class {M : Type u_1} [mul_one_class M] (S : submonoid M) :

mul_one_class ↥S

A submonoid of a unital magma inherits a unital magma structure.

Equations

S.to_mul_one_class = function.injective.mul_one_class coe _ _ _

source

@[protected]

theorem submonoid.pow_mem {M : Type u_1} [monoid M] (S : submonoid M) {x : M} (hx : x ∈ S) (n : ℕ) :

x ^ n ∈ S

source

@[protected]

theorem add_submonoid.nsmul_mem {M : Type u_1} [add_monoid M] (S : add_submonoid M) {x : M} (hx : x ∈ S) (n : ℕ) :

n • x ∈ S

source

@[simp, norm_cast]

theorem add_submonoid.coe_nsmul {M : Type u_1} [add_monoid M] {S : add_submonoid M} (x : ↥S) (n : ℕ) :

↑(n • x) = n • ↑x

source

@[simp, norm_cast]

theorem submonoid.coe_pow {M : Type u_1} [monoid M] {S : submonoid M} (x : ↥S) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

source

@[protected, instance]

def submonoid.to_monoid {M : Type u_1} [monoid M] (S : submonoid M) :

monoid ↥S

A submonoid of a monoid inherits a monoid structure.

Equations

S.to_monoid = function.injective.monoid coe _ _ _ _

source

@[protected, instance]

def add_submonoid.to_add_monoid {M : Type u_1} [add_monoid M] (S : add_submonoid M) :

add_monoid ↥S

An add_submonoid of an add_monoid inherits an add_monoid structure.

Equations

S.to_add_monoid = function.injective.add_monoid coe _ _ _ _

source

@[protected, instance]

def add_submonoid.to_add_comm_monoid {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

add_comm_monoid ↥S

An add_submonoid of an add_comm_monoid is an add_comm_monoid.

Equations

S.to_add_comm_monoid = function.injective.add_comm_monoid coe _ _ _ _

source

@[protected, instance]

def submonoid.to_comm_monoid {M : Type u_1} [comm_monoid M] (S : submonoid M) :

comm_monoid ↥S

A submonoid of a comm_monoid is a comm_monoid.

Equations

S.to_comm_monoid = function.injective.comm_monoid coe _ _ _ _

source

@[protected, instance]

def add_submonoid.to_ordered_add_comm_monoid {M : Type u_1} [ordered_add_comm_monoid M] (S : add_submonoid M) :

ordered_add_comm_monoid ↥S

An add_submonoid of an ordered_add_comm_monoid is an ordered_add_comm_monoid.

Equations

S.to_ordered_add_comm_monoid = function.injective.ordered_add_comm_monoid coe _ _ _ _

source

@[protected, instance]

def submonoid.to_ordered_comm_monoid {M : Type u_1} [ordered_comm_monoid M] (S : submonoid M) :

ordered_comm_monoid ↥S

A submonoid of an ordered_comm_monoid is an ordered_comm_monoid.

Equations

S.to_ordered_comm_monoid = function.injective.ordered_comm_monoid coe _ _ _ _

source

@[protected, instance]

def add_submonoid.to_linear_ordered_add_comm_monoid {M : Type u_1} [linear_ordered_add_comm_monoid M] (S : add_submonoid M) :

linear_ordered_add_comm_monoid ↥S

An add_submonoid of a linear_ordered_add_comm_monoid is a linear_ordered_add_comm_monoid.

Equations

S.to_linear_ordered_add_comm_monoid = function.injective.linear_ordered_add_comm_monoid coe _ _ _ _ _ _

source

@[protected, instance]

def submonoid.to_linear_ordered_comm_monoid {M : Type u_1} [linear_ordered_comm_monoid M] (S : submonoid M) :

linear_ordered_comm_monoid ↥S

A submonoid of a linear_ordered_comm_monoid is a linear_ordered_comm_monoid.

Equations

S.to_linear_ordered_comm_monoid = function.injective.linear_ordered_comm_monoid coe _ _ _ _ _ _

source

@[protected, instance]

def add_submonoid.to_ordered_cancel_add_comm_monoid {M : Type u_1} [ordered_cancel_add_comm_monoid M] (S : add_submonoid M) :

ordered_cancel_add_comm_monoid ↥S

An add_submonoid of an ordered_cancel_add_comm_monoid is an ordered_cancel_add_comm_monoid.

Equations

S.to_ordered_cancel_add_comm_monoid = function.injective.ordered_cancel_add_comm_monoid coe _ _ _ _

source

@[protected, instance]

def submonoid.to_ordered_cancel_comm_monoid {M : Type u_1} [ordered_cancel_comm_monoid M] (S : submonoid M) :

ordered_cancel_comm_monoid ↥S

A submonoid of an ordered_cancel_comm_monoid is an ordered_cancel_comm_monoid.

Equations

S.to_ordered_cancel_comm_monoid = function.injective.ordered_cancel_comm_monoid coe _ _ _ _

source

@[protected, instance]

def add_submonoid.to_linear_ordered_cancel_add_comm_monoid {M : Type u_1} [linear_ordered_cancel_add_comm_monoid M] (S : add_submonoid M) :

linear_ordered_cancel_add_comm_monoid ↥S

An add_submonoid of a linear_ordered_cancel_add_comm_monoid is a linear_ordered_cancel_add_comm_monoid.

Equations

S.to_linear_ordered_cancel_add_comm_monoid = function.injective.linear_ordered_cancel_add_comm_monoid coe _ _ _ _ _ _

source

@[protected, instance]

def submonoid.to_linear_ordered_cancel_comm_monoid {M : Type u_1} [linear_ordered_cancel_comm_monoid M] (S : submonoid M) :

linear_ordered_cancel_comm_monoid ↥S

A submonoid of a linear_ordered_cancel_comm_monoid is a linear_ordered_cancel_comm_monoid.

Equations

S.to_linear_ordered_cancel_comm_monoid = function.injective.linear_ordered_cancel_comm_monoid coe _ _ _ _ _ _

source

def add_submonoid.subtype {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

↥S →+ M

The natural monoid hom from an add_submonoid of add_monoid M to M.

Equations

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

source

def submonoid.subtype {M : Type u_1} [mul_one_class M] (S : submonoid M) :

↥S →* M

The natural monoid hom from a submonoid of monoid M to M.

Equations

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

source

@[simp]

theorem add_submonoid.coe_subtype {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

⇑(S.subtype) = coe

source

@[simp]

theorem submonoid.coe_subtype {M : Type u_1} [mul_one_class M] (S : submonoid M) :

⇑(S.subtype) = coe

source

@[simp]

theorem add_submonoid.top_equiv_symm_apply_coe {M : Type u_1} [add_zero_class M] (x : M) :

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

source

def submonoid.top_equiv {M : Type u_1} [mul_one_class M] :

↥⊤ ≃* M

The top submonoid is isomorphic to the monoid.

Equations

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

source

@[simp]

theorem submonoid.top_equiv_symm_apply_coe {M : Type u_1} [mul_one_class M] (x : M) :

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

source

@[simp]

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

⇑add_submonoid.top_equiv x = ↑x

source

@[simp]

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

⇑submonoid.top_equiv x = ↑x

source

def add_submonoid.top_equiv {M : Type u_1} [add_zero_class M] :

↥⊤ ≃+ M

The top additive submonoid is isomorphic to the additive monoid.

Equations

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

source

@[simp]

theorem submonoid.top_equiv_to_monoid_hom {M : Type u_1} [mul_one_class M] :

submonoid.top_equiv.to_monoid_hom = ⊤.subtype

source

@[simp]

theorem add_submonoid.top_equiv_to_add_monoid_hom {M : Type u_1} [add_zero_class M] :

add_submonoid.top_equiv.to_add_monoid_hom = ⊤.subtype

source

noncomputable def add_submonoid.equiv_map_of_injective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (S : add_submonoid M) (f : M →+ N) (hf : function.injective ⇑f) :

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

An additive subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use add_equiv.add_submonoid_map for better definitional equalities.

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 submonoid.equiv_map_of_injective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (S : submonoid M) (f : M →* N) (hf : function.injective ⇑f) :

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

A subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use mul_equiv.submonoid_map for better definitional equalities.

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 add_submonoid.coe_equiv_map_of_injective_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (S : add_submonoid M) (f : M →+ N) (hf : function.injective ⇑f) (x : ↥S) :

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

source

@[simp]

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

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

source

@[simp]

theorem submonoid.closure_closure_coe_preimage {M : Type u_1} [mul_one_class M] {s : set M} :

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

source

@[simp]

theorem add_submonoid.closure_closure_coe_preimage {M : Type u_1} [add_zero_class M] {s : set M} :

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

source

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

submonoid (M × N)

Given submonoids s, t of monoids M, N respectively, s × t as a submonoid of M × N.

Equations

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

source

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

add_submonoid (M × N)

Given add_submonoids s, t of add_monoids A, B respectively, s × t as an add_submonoid of A × B.

Equations

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

s.prod ⊤ = add_submonoid.comap (add_monoid_hom.fst M N) s

source

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

s.prod ⊤ = submonoid.comap (monoid_hom.fst M N) s

source

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

⊤.prod s = submonoid.comap (monoid_hom.snd M N) s

source

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

⊤.prod s = add_submonoid.comap (add_monoid_hom.snd M N) s

source

@[simp]

theorem add_submonoid.top_prod_top {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

⊤.prod ⊤ = ⊤

source

@[simp]

theorem submonoid.top_prod_top {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

⊤.prod ⊤ = ⊤

source

theorem add_submonoid.bot_sum_bot {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

⊥.prod ⊥ = ⊥

source

theorem submonoid.bot_prod_bot {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

⊥.prod ⊥ = ⊥

source

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

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

The product of submonoids is isomorphic to their product as monoids.

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_submonoid.prod_equiv {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (s : add_submonoid M) (t : add_submonoid N) :

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

The product of additive submonoids is isomorphic to their product as additive monoids

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_submonoid.map_inl {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (s : add_submonoid M) :

add_submonoid.map (add_monoid_hom.inl M N) s = s.prod ⊥

source

theorem submonoid.map_inl {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (s : submonoid M) :

submonoid.map (monoid_hom.inl M N) s = s.prod ⊥

source

theorem submonoid.map_inr {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (s : submonoid N) :

submonoid.map (monoid_hom.inr M N) s = ⊥.prod s

source

theorem add_submonoid.map_inr {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (s : add_submonoid N) :

add_submonoid.map (add_monoid_hom.inr M N) s = ⊥.prod s

source

@[simp]

theorem submonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (s : submonoid M) (t : submonoid N) :

s.prod ⊥ ⊔ ⊥.prod t = s.prod t

source

@[simp]

theorem add_submonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (s : add_submonoid M) (t : add_submonoid N) :

s.prod ⊥ ⊔ ⊥.prod t = s.prod t

source

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

x ∈ add_submonoid.map f.to_add_monoid_hom K ↔ ⇑(f.symm) x ∈ K

source

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

x ∈ submonoid.map f.to_monoid_hom K ↔ ⇑(f.symm) x ∈ K

source

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

add_submonoid.map f.to_add_monoid_hom K = add_submonoid.comap f.symm.to_add_monoid_hom K

source

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

submonoid.map f.to_monoid_hom K = submonoid.comap f.symm.to_monoid_hom K

source

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

submonoid.comap f.to_monoid_hom K = submonoid.map f.symm.to_monoid_hom K

source

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

add_submonoid.comap f.to_add_monoid_hom K = add_submonoid.map f.symm.to_add_monoid_hom K

source

@[simp]

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

submonoid.map f.to_monoid_hom ⊤ = ⊤

source

@[simp]

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

add_submonoid.map f.to_add_monoid_hom ⊤ = ⊤

source

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

u ≤ s.prod t ↔ add_submonoid.map (add_monoid_hom.fst M N) u ≤ s ∧ add_submonoid.map (add_monoid_hom.snd M N) u ≤ t

source

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

u ≤ s.prod t ↔ submonoid.map (monoid_hom.fst M N) u ≤ s ∧ submonoid.map (monoid_hom.snd M N) u ≤ t

source

theorem submonoid.prod_le_iff {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {s : submonoid M} {t : submonoid N} {u : submonoid (M × N)} :

s.prod t ≤ u ↔ submonoid.map (monoid_hom.inl M N) s ≤ u ∧ submonoid.map (monoid_hom.inr M N) t ≤ u

source

theorem add_submonoid.prod_le_iff {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {s : add_submonoid M} {t : add_submonoid N} {u : add_submonoid (M × N)} :

s.prod t ≤ u ↔ add_submonoid.map (add_monoid_hom.inl M N) s ≤ u ∧ add_submonoid.map (add_monoid_hom.inr M N) t ≤ u

source

def library_note.range copy pattern :

unit

For many categories (monoids, modules, rings, ...) the set-theoretic image of a morphism f is a subobject of the codomain. When this is the case, it is useful to define the range of a morphism in such a way that the underlying carrier set of the range subobject is definitionally set.range f. In particular this means that the types ↥(set.range f) and ↥f.range are interchangeable without proof obligations.

A convenient candidate definition for range which is mathematically correct is map ⊤ f, just as set.range could have been defined as f '' set.univ. However, this lacks the desired definitional convenience, in that it both does not match set.range, and that it introduces a redudant x ∈ ⊤ term which clutters proofs. In such a case one may resort to the copy pattern. A copy function converts the definitional problem for the carrier set of a subobject into a one-off propositional proof obligation which one discharges while writing the definition of the definitionally convenient range (the parameter hs in the example below).

A good example is the case of a morphism of monoids. A convenient definition for monoid_hom.mrange would be (⊤ : submonoid M).map f. However since this lacks the required definitional convenience, we first define submonoid.copy as follows:

protected def copy (S : submonoid M) (s : set M) (hs : s = S) : submonoid M :=
{ carrier  := s,
  one_mem' := hs.symm ▸ S.one_mem',
  mul_mem' := hs.symm ▸ S.mul_mem' }

and then finally define:

def mrange (f : M →* N) : submonoid N :=
((⊤ : submonoid M).map f).copy (set.range f) set.image_univ.symm

source

def monoid_hom.mrange {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) :

submonoid N

The range of a monoid homomorphism is a submonoid. See Note [range copy pattern].

Equations

monoid_hom.mrange f = (submonoid.map f ⊤).copy (set.range ⇑f) _

Instances for ↥monoid_hom.mrange

source

def add_monoid_hom.mrange {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) :

add_submonoid N

The range of an add_monoid_hom is an add_submonoid.

Equations

add_monoid_hom.mrange f = (add_submonoid.map f ⊤).copy (set.range ⇑f) _

Instances for ↥add_monoid_hom.mrange

source

@[simp]

theorem monoid_hom.coe_mrange {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) :

↑(monoid_hom.mrange f) = set.range ⇑f

source

@[simp]

theorem add_monoid_hom.coe_mrange {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) :

↑(add_monoid_hom.mrange f) = set.range ⇑f

source

@[simp]

theorem add_monoid_hom.mem_mrange {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} {y : N} :

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

source

@[simp]

theorem monoid_hom.mem_mrange {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} {y : N} :

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

source

theorem monoid_hom.mrange_eq_map {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) :

monoid_hom.mrange f = submonoid.map f ⊤

source

theorem add_monoid_hom.mrange_eq_map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) :

add_monoid_hom.mrange f = add_submonoid.map f ⊤

source

theorem add_monoid_hom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_zero_class M] [add_zero_class N] [add_zero_class P] (g : N →+ P) (f : M →+ N) :

add_submonoid.map g (add_monoid_hom.mrange f) = add_monoid_hom.mrange (g.comp f)

source

theorem monoid_hom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_one_class M] [mul_one_class N] [mul_one_class P] (g : N →* P) (f : M →* N) :

submonoid.map g (monoid_hom.mrange f) = monoid_hom.mrange (g.comp f)

source

theorem add_monoid_hom.mrange_top_iff_surjective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] {f : F} :

add_monoid_hom.mrange f = ⊤ ↔ function.surjective ⇑f

source

theorem monoid_hom.mrange_top_iff_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] {f : F} :

monoid_hom.mrange f = ⊤ ↔ function.surjective ⇑f

source

theorem add_monoid_hom.mrange_top_of_surjective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) (hf : function.surjective ⇑f) :

add_monoid_hom.mrange f = ⊤

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

source

theorem monoid_hom.mrange_top_of_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) (hf : function.surjective ⇑f) :

monoid_hom.mrange f = ⊤

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

source

theorem monoid_hom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) (s : set N) :

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

source

theorem add_monoid_hom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) (s : set N) :

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

source

theorem add_monoid_hom.map_mclosure {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) (s : set M) :

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

The image under an add_monoid hom of the add_submonoid generated by a set equals the add_submonoid generated by the image of the set.

source

theorem monoid_hom.map_mclosure {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) (s : set M) :

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

The image under a monoid hom of the submonoid generated by a set equals the submonoid generated by the image of the set.

source

def add_monoid_hom.restrict {M : Type u_1} [add_zero_class M] {N : Type u_2} {S : Type u_3} [add_zero_class N] [set_like S M] [add_submonoid_class S M] (f : M →+ N) (s : S) :

↥s →+ N

Restriction of an add_monoid hom to an add_submonoid of the domain.

Equations

f.restrict s = f.comp (add_submonoid_class.subtype s)

source

def monoid_hom.restrict {M : Type u_1} [mul_one_class M] {N : Type u_2} {S : Type u_3} [mul_one_class N] [set_like S M] [submonoid_class S M] (f : M →* N) (s : S) :

↥s →* N

Restriction of a monoid hom to a submonoid of the domain.

Equations

f.restrict s = f.comp (submonoid_class.subtype s)

source

@[simp]

theorem add_monoid_hom.restrict_apply {M : Type u_1} [add_zero_class M] {N : Type u_2} {S : Type u_3} [add_zero_class N] [set_like S M] [add_submonoid_class S M] (f : M →+ N) (s : S) (x : ↥s) :

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

source

@[simp]

theorem monoid_hom.restrict_apply {M : Type u_1} [mul_one_class M] {N : Type u_2} {S : Type u_3} [mul_one_class N] [set_like S M] [submonoid_class S M] (f : M →* N) (s : S) (x : ↥s) :

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

source

@[simp]

theorem monoid_hom.restrict_mrange {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (S : submonoid M) (f : M →* N) :

monoid_hom.mrange (f.restrict S) = submonoid.map f S

source

@[simp]

theorem add_monoid_hom.restrict_mrange {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (S : add_submonoid M) (f : M →+ N) :

add_monoid_hom.mrange (f.restrict S) = add_submonoid.map f S

source

@[simp]

theorem monoid_hom.cod_restrict_apply {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {S : Type u_3} [set_like S N] [submonoid_class S N] (f : M →* N) (s : S) (h : ∀ (x : M), ⇑f x ∈ s) (n : M) :

⇑(f.cod_restrict s h) n = ⟨⇑f n, _⟩

source

def add_monoid_hom.cod_restrict {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {S : Type u_3} [set_like S N] [add_submonoid_class S N] (f : M →+ N) (s : S) (h : ∀ (x : M), ⇑f x ∈ s) :

M →+ ↥s

Restriction of an add_monoid hom to an add_submonoid of the codomain.

Equations

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

source

def monoid_hom.cod_restrict {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {S : Type u_3} [set_like S N] [submonoid_class S N] (f : M →* N) (s : S) (h : ∀ (x : M), ⇑f x ∈ s) :

M →* ↥s

Restriction of a monoid hom to a submonoid of the codomain.

Equations

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

source

@[simp]

theorem add_monoid_hom.cod_restrict_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {S : Type u_3} [set_like S N] [add_submonoid_class S N] (f : M →+ N) (s : S) (h : ∀ (x : M), ⇑f x ∈ s) (n : M) :

⇑(f.cod_restrict s h) n = ⟨⇑f n, _⟩

source

def add_monoid_hom.mrange_restrict {M : Type u_1} [add_zero_class M] {N : Type u_2} [add_zero_class N] (f : M →+ N) :

M →+ ↥(add_monoid_hom.mrange f)

Restriction of an add_monoid hom to its range interpreted as a submonoid.

Equations

f.mrange_restrict = f.cod_restrict (add_monoid_hom.mrange f) _

source

def monoid_hom.mrange_restrict {M : Type u_1} [mul_one_class M] {N : Type u_2} [mul_one_class N] (f : M →* N) :

M →* ↥(monoid_hom.mrange f)

Restriction of a monoid hom to its range interpreted as a submonoid.

Equations

f.mrange_restrict = f.cod_restrict (monoid_hom.mrange f) _

source

@[simp]

theorem add_monoid_hom.coe_mrange_restrict {M : Type u_1} [add_zero_class M] {N : Type u_2} [add_zero_class N] (f : M →+ N) (x : M) :

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

source

@[simp]

theorem monoid_hom.coe_mrange_restrict {M : Type u_1} [mul_one_class M] {N : Type u_2} [mul_one_class N] (f : M →* N) (x : M) :

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

source

theorem add_monoid_hom.mrange_restrict_surjective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) :

function.surjective ⇑(f.mrange_restrict)

source

theorem monoid_hom.mrange_restrict_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) :

function.surjective ⇑(f.mrange_restrict)

source

def monoid_hom.mker {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) :

submonoid M

The multiplicative kernel of a monoid homomorphism is the submonoid of elements x : G such that f x = 1

Equations

monoid_hom.mker f = submonoid.comap f ⊥

source

def add_monoid_hom.mker {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) :

add_submonoid M

The additive kernel of an add_monoid homomorphism is the add_submonoid of elements such that f x = 0

Equations

add_monoid_hom.mker f = add_submonoid.comap f ⊥

source

theorem monoid_hom.mem_mker {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) {x : M} :

x ∈ monoid_hom.mker f ↔ ⇑f x = 1

source

theorem add_monoid_hom.mem_mker {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) {x : M} :

x ∈ add_monoid_hom.mker f ↔ ⇑f x = 0

source

theorem monoid_hom.coe_mker {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) :

↑(monoid_hom.mker f) = ⇑f ⁻¹' {1}

source

theorem add_monoid_hom.coe_mker {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) :

↑(add_monoid_hom.mker f) = ⇑f ⁻¹' {0}

source

@[protected, instance]

def add_monoid_hom.decidable_mem_mker {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] [decidable_eq N] (f : F) :

decidable_pred (λ (_x : M), _x ∈ add_monoid_hom.mker f)

Equations

add_monoid_hom.decidable_mem_mker f = λ (x : M), decidable_of_iff (⇑f x = 0) _

source

@[protected, instance]

def monoid_hom.decidable_mem_mker {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] [decidable_eq N] (f : F) :

decidable_pred (λ (_x : M), _x ∈ monoid_hom.mker f)

Equations

monoid_hom.decidable_mem_mker f = λ (x : M), decidable_of_iff (⇑f x = 1) _

source

theorem add_monoid_hom.comap_mker {M : Type u_1} {N : Type u_2} {P : Type u_3} [add_zero_class M] [add_zero_class N] [add_zero_class P] (g : N →+ P) (f : M →+ N) :

add_submonoid.comap f (add_monoid_hom.mker g) = add_monoid_hom.mker (g.comp f)

source

theorem monoid_hom.comap_mker {M : Type u_1} {N : Type u_2} {P : Type u_3} [mul_one_class M] [mul_one_class N] [mul_one_class P] (g : N →* P) (f : M →* N) :

submonoid.comap f (monoid_hom.mker g) = monoid_hom.mker (g.comp f)

source

@[simp]

theorem add_monoid_hom.comap_bot' {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {F : Type u_4} [mc : add_monoid_hom_class F M N] (f : F) :

add_submonoid.comap f ⊥ = add_monoid_hom.mker f

source

@[simp]

theorem monoid_hom.comap_bot' {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {F : Type u_4} [mc : monoid_hom_class F M N] (f : F) :

submonoid.comap f ⊥ = monoid_hom.mker f

source

@[simp]

theorem add_monoid_hom.restrict_mker {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (S : add_submonoid M) (f : M →+ N) :

add_monoid_hom.mker (f.restrict S) = add_submonoid.comap S.subtype (add_monoid_hom.mker f)

source

@[simp]

theorem monoid_hom.restrict_mker {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (S : submonoid M) (f : M →* N) :

monoid_hom.mker (f.restrict S) = submonoid.comap S.subtype (monoid_hom.mker f)

source

theorem monoid_hom.range_restrict_mker {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) :

monoid_hom.mker f.mrange_restrict = monoid_hom.mker f

source

theorem add_monoid_hom.range_restrict_mker {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) :

add_monoid_hom.mker f.mrange_restrict = add_monoid_hom.mker f

source

@[simp]

theorem add_monoid_hom.mker_zero {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

add_monoid_hom.mker 0 = ⊤

source

@[simp]

theorem monoid_hom.mker_one {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

monoid_hom.mker 1 = ⊤

source

theorem monoid_hom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {M' : Type u_3} {N' : Type u_4} [mul_one_class M'] [mul_one_class N'] (f : M →* N) (g : M' →* N') (S : submonoid N) (S' : submonoid N') :

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

source

theorem add_monoid_hom.sum_map_comap_sum' {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {M' : Type u_3} {N' : Type u_4} [add_zero_class M'] [add_zero_class N'] (f : M →+ N) (g : M' →+ N') (S : add_submonoid N) (S' : add_submonoid N') :

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

source

theorem add_monoid_hom.mker_sum_map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {M' : Type u_3} {N' : Type u_4} [add_zero_class M'] [add_zero_class N'] (f : M →+ N) (g : M' →+ N') :

add_monoid_hom.mker (f.prod_map g) = (add_monoid_hom.mker f).prod (add_monoid_hom.mker g)

source

theorem monoid_hom.mker_prod_map {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {M' : Type u_3} {N' : Type u_4} [mul_one_class M'] [mul_one_class N'] (f : M →* N) (g : M' →* N') :

monoid_hom.mker (f.prod_map g) = (monoid_hom.mker f).prod (monoid_hom.mker g)

source

@[simp]

theorem monoid_hom.mker_inl {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

monoid_hom.mker (monoid_hom.inl M N) = ⊥

source

@[simp]

theorem add_monoid_hom.mker_inl {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

add_monoid_hom.mker (add_monoid_hom.inl M N) = ⊥

source

@[simp]

theorem add_monoid_hom.mker_inr {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

add_monoid_hom.mker (add_monoid_hom.inr M N) = ⊥

source

@[simp]

theorem monoid_hom.mker_inr {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

monoid_hom.mker (monoid_hom.inr M N) = ⊥

source

@[simp]

theorem monoid_hom.submonoid_comap_apply_coe {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (N' : submonoid N) (x : ↥(submonoid.comap f N')) :

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

source

def add_monoid_hom.add_submonoid_comap {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (N' : add_submonoid N) :

↥(add_submonoid.comap f N') →+ ↥N'

the add_monoid_hom from the preimage of an additive submonoid to itself.

Equations

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

source

def monoid_hom.submonoid_comap {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (N' : submonoid N) :

↥(submonoid.comap f N') →* ↥N'

The monoid_hom from the preimage of a submonoid to itself.

Equations

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

source

@[simp]

theorem add_monoid_hom.add_submonoid_comap_apply_coe {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (N' : add_submonoid N) (x : ↥(add_submonoid.comap f N')) :

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

source

def add_monoid_hom.add_submonoid_map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (M' : add_submonoid M) :

↥M' →+ ↥(add_submonoid.map f M')

the add_monoid_hom from an additive submonoid to its image. See add_equiv.add_submonoid_map for a variant for add_equivs.

Equations

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

source

def monoid_hom.submonoid_map {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (M' : submonoid M) :

↥M' →* ↥(submonoid.map f M')

The monoid_hom from a submonoid to its image. See mul_equiv.submonoid_map for a variant for mul_equivs.

Equations

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

source

@[simp]

theorem monoid_hom.submonoid_map_apply_coe {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (M' : submonoid M) (x : ↥M') :

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

source

@[simp]

theorem add_monoid_hom.add_submonoid_map_apply_coe {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (M' : add_submonoid M) (x : ↥M') :

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

source

theorem add_monoid_hom.add_submonoid_map_surjective {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (M' : add_submonoid M) :

function.surjective ⇑(f.add_submonoid_map M')

source

theorem monoid_hom.submonoid_map_surjective {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (M' : submonoid M) :

function.surjective ⇑(f.submonoid_map M')

source

theorem submonoid.mrange_inl {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

monoid_hom.mrange (monoid_hom.inl M N) = ⊤.prod ⊥

source

theorem add_submonoid.mrange_inl {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

add_monoid_hom.mrange (add_monoid_hom.inl M N) = ⊤.prod ⊥

source

theorem submonoid.mrange_inr {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

monoid_hom.mrange (monoid_hom.inr M N) = ⊥.prod ⊤

source

theorem add_submonoid.mrange_inr {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

add_monoid_hom.mrange (add_monoid_hom.inr M N) = ⊥.prod ⊤

source

theorem add_submonoid.mrange_inl' {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

add_monoid_hom.mrange (add_monoid_hom.inl M N) = add_submonoid.comap (add_monoid_hom.snd M N) ⊥

source

theorem submonoid.mrange_inl' {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

monoid_hom.mrange (monoid_hom.inl M N) = submonoid.comap (monoid_hom.snd M N) ⊥

source

theorem submonoid.mrange_inr' {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

monoid_hom.mrange (monoid_hom.inr M N) = submonoid.comap (monoid_hom.fst M N) ⊥

source

theorem add_submonoid.mrange_inr' {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

add_monoid_hom.mrange (add_monoid_hom.inr M N) = add_submonoid.comap (add_monoid_hom.fst M N) ⊥

source

@[simp]

theorem submonoid.mrange_fst {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

monoid_hom.mrange (monoid_hom.fst M N) = ⊤

source

@[simp]

theorem add_submonoid.mrange_fst {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

add_monoid_hom.mrange (add_monoid_hom.fst M N) = ⊤

source

@[simp]

theorem submonoid.mrange_snd {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

monoid_hom.mrange (monoid_hom.snd M N) = ⊤

source

@[simp]

theorem add_submonoid.mrange_snd {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

add_monoid_hom.mrange (add_monoid_hom.snd M N) = ⊤

source

theorem submonoid.prod_eq_bot_iff {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {s : submonoid M} {t : submonoid N} :

s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥

source

theorem add_submonoid.sum_eq_bot_iff {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {s : add_submonoid M} {t : add_submonoid N} :

s.prod t = ⊥ ↔ s = ⊥ ∧ t = ⊥

source

theorem submonoid.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {s : submonoid M} {t : submonoid N} :

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

source

theorem add_submonoid.sum_eq_top_iff {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {s : add_submonoid M} {t : add_submonoid N} :

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

source

@[simp]

theorem submonoid.mrange_inl_sup_mrange_inr {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

monoid_hom.mrange (monoid_hom.inl M N) ⊔ monoid_hom.mrange (monoid_hom.inr M N) = ⊤

source

@[simp]

theorem add_submonoid.mrange_inl_sup_mrange_inr {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

add_monoid_hom.mrange (add_monoid_hom.inl M N) ⊔ add_monoid_hom.mrange (add_monoid_hom.inr M N) = ⊤

source

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

↥S →* ↥T

The monoid hom associated to an inclusion of submonoids.

Equations

submonoid.inclusion h = S.subtype.cod_restrict T _

source

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

↥S →+ ↥T

The add_monoid hom associated to an inclusion of submonoids.

Equations

add_submonoid.inclusion h = S.subtype.cod_restrict T _

source

@[simp]

theorem add_submonoid.range_subtype {M : Type u_1} [add_zero_class M] (s : add_submonoid M) :

add_monoid_hom.mrange s.subtype = s

source

@[simp]

theorem submonoid.range_subtype {M : Type u_1} [mul_one_class M] (s : submonoid M) :

monoid_hom.mrange s.subtype = s

source

theorem add_submonoid.eq_top_iff' {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

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

source

theorem submonoid.eq_top_iff' {M : Type u_1} [mul_one_class M] (S : submonoid M) :

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

source

theorem submonoid.eq_bot_iff_forall {M : Type u_1} [mul_one_class M] (S : submonoid M) :

S = ⊥ ↔ ∀ (x : M), x ∈ S → x = 1

source

theorem add_submonoid.eq_bot_iff_forall {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

S = ⊥ ↔ ∀ (x : M), x ∈ S → x = 0

source

theorem submonoid.nontrivial_iff_exists_ne_one {M : Type u_1} [mul_one_class M] (S : submonoid M) :

nontrivial ↥S ↔ ∃ (x : M) (H : x ∈ S), x ≠ 1

source

theorem add_submonoid.nontrivial_iff_exists_ne_zero {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

nontrivial ↥S ↔ ∃ (x : M) (H : x ∈ S), x ≠ 0

source

theorem submonoid.bot_or_nontrivial {M : Type u_1} [mul_one_class M] (S : submonoid M) :

S = ⊥ ∨ nontrivial ↥S

A submonoid is either the trivial submonoid or nontrivial.

source

theorem add_submonoid.bot_or_nontrivial {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

S = ⊥ ∨ nontrivial ↥S

An additive submonoid is either the trivial additive submonoid or nontrivial.

source

theorem submonoid.bot_or_exists_ne_one {M : Type u_1} [mul_one_class M] (S : submonoid M) :

S = ⊥ ∨ ∃ (x : M) (H : x ∈ S), x ≠ 1

A submonoid is either the trivial submonoid or contains a nonzero element.

source

theorem add_submonoid.bot_or_exists_ne_zero {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

S = ⊥ ∨ ∃ (x : M) (H : x ∈ S), x ≠ 0

An additive submonoid is either the trivial additive submonoid or contains a nonzero element.

source

def mul_equiv.submonoid_congr {M : Type u_1} [mul_one_class M] {S T : submonoid M} (h : S = T) :

↥S ≃* ↥T

Makes the identity isomorphism from a proof that two submonoids of a multiplicative monoid are equal.

Equations

mul_equiv.submonoid_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.add_submonoid_congr {M : Type u_1} [add_zero_class M] {S T : add_submonoid M} (h : S = T) :

↥S ≃+ ↥T

Makes the identity additive isomorphism from a proof two submonoids of an additive monoid are equal.

Equations

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

source

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

M ≃* ↥(monoid_hom.mrange f)

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

This is a bidirectional version of monoid_hom.mrange_restrict.

Equations

mul_equiv.of_left_inverse' f h = {to_fun := ⇑(f.mrange_restrict), inv_fun := g ∘ ⇑((monoid_hom.mrange f).subtype), left_inv := h, right_inv := _, map_mul' := _}

source

@[simp]

theorem add_equiv.of_left_inverse'_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) {g : N → M} (h : function.left_inverse g ⇑f) (ᾰ : M) :

⇑(add_equiv.of_left_inverse' f h) ᾰ = ⇑(f.mrange_restrict) ᾰ

source

@[simp]

theorem mul_equiv.of_left_inverse'_apply {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) {g : N → M} (h : function.left_inverse g ⇑f) (ᾰ : M) :

⇑(mul_equiv.of_left_inverse' f h) ᾰ = ⇑(f.mrange_restrict) ᾰ

source

@[simp]

theorem mul_equiv.of_left_inverse'_symm_apply {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) {g : N → M} (h : function.left_inverse g ⇑f) (ᾰ : ↥(monoid_hom.mrange f)) :

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

source

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

M ≃+ ↥(add_monoid_hom.mrange f)

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

This is a bidirectional version of add_monoid_hom.mrange_restrict.

Equations

add_equiv.of_left_inverse' f h = {to_fun := ⇑(f.mrange_restrict), inv_fun := g ∘ ⇑((add_monoid_hom.mrange f).subtype), left_inv := h, right_inv := _, map_add' := _}

source

@[simp]

theorem add_equiv.of_left_inverse'_symm_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) {g : N → M} (h : function.left_inverse g ⇑f) (ᾰ : ↥(add_monoid_hom.mrange f)) :

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

source

def add_equiv.add_submonoid_map {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (e : M ≃+ N) (S : add_submonoid M) :

↥S ≃+ ↥(add_submonoid.map e.to_add_monoid_hom S)

An add_equiv φ between two additive monoids M and N induces an add_equiv between a submonoid S ≤ M and the submonoid φ(S) ≤ N. See add_monoid_hom.add_submonoid_map for a variant for add_monoid_homs.

Equations

e.add_submonoid_map S = {to_fun := (↑e.image ↑S).to_fun, inv_fun := (↑e.image ↑S).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

def mul_equiv.submonoid_map {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (e : M ≃* N) (S : submonoid M) :

↥S ≃* ↥(submonoid.map e.to_monoid_hom S)

A mul_equiv φ between two monoids M and N induces a mul_equiv between a submonoid S ≤ M and the submonoid φ(S) ≤ N. See monoid_hom.submonoid_map for a variant for monoid_homs.

Equations

e.submonoid_map S = {to_fun := (↑e.image ↑S).to_fun, inv_fun := (↑e.image ↑S).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem mul_equiv.coe_submonoid_map_apply {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (e : M ≃* N) (S : submonoid M) (g : ↥S) :

↑(⇑(e.submonoid_map S) g) = ⇑e ↑g

source

@[simp]

theorem add_equiv.coe_add_submonoid_map_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (e : M ≃+ N) (S : add_submonoid M) (g : ↥S) :

↑(⇑(e.add_submonoid_map S) g) = ⇑e ↑g

source

@[simp]

theorem mul_equiv.submonoid_map_symm_apply {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (e : M ≃* N) (S : submonoid M) (g : ↥(submonoid.map ↑e S)) :

⇑((e.submonoid_map S).symm) g = ⟨⇑(e.symm) ↑g, _⟩

source

@[simp]

theorem add_equiv.add_submonoid_map_symm_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (e : M ≃+ N) (S : add_submonoid M) (g : ↥(add_submonoid.map ↑e S)) :

⇑((e.add_submonoid_map S).symm) g = ⟨⇑(e.symm) ↑g, _⟩

source

@[simp]

theorem add_submonoid.equiv_map_of_injective_coe_add_equiv {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (S : add_submonoid M) (e : M ≃+ N) :

S.equiv_map_of_injective ↑e _ = e.add_submonoid_map S

source

@[simp]

theorem submonoid.equiv_map_of_injective_coe_mul_equiv {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (S : submonoid M) (e : M ≃* N) :

S.equiv_map_of_injective ↑e _ = e.submonoid_map S

source

@[protected, instance]

def add_submonoid.has_vadd {M' : Type u_4} {α : Type u_5} [add_zero_class M'] [has_vadd M' α] (S : add_submonoid M') :

has_vadd ↥S α

Equations

S.has_vadd = has_vadd.comp α ⇑(S.subtype)

source

@[protected, instance]

def submonoid.has_smul {M' : Type u_4} {α : Type u_5} [mul_one_class M'] [has_smul M' α] (S : submonoid M') :

has_smul ↥S α

Equations

S.has_smul = has_smul.comp α ⇑(S.subtype)

source

@[protected, instance]

def add_submonoid.vadd_comm_class_left {M' : Type u_4} {α : Type u_5} {β : Type u_6} [add_zero_class M'] [has_vadd M' β] [has_vadd α β] [vadd_comm_class M' α β] (S : add_submonoid M') :

vadd_comm_class ↥S α β

source

@[protected, instance]

def submonoid.smul_comm_class_left {M' : Type u_4} {α : Type u_5} {β : Type u_6} [mul_one_class M'] [has_smul M' β] [has_smul α β] [smul_comm_class M' α β] (S : submonoid M') :

smul_comm_class ↥S α β

source

@[protected, instance]

def add_submonoid.vadd_comm_class_right {M' : Type u_4} {α : Type u_5} {β : Type u_6} [add_zero_class M'] [has_vadd α β] [has_vadd M' β] [vadd_comm_class α M' β] (S : add_submonoid M') :

vadd_comm_class α ↥S β

source

@[protected, instance]

def submonoid.smul_comm_class_right {M' : Type u_4} {α : Type u_5} {β : Type u_6} [mul_one_class M'] [has_smul α β] [has_smul M' β] [smul_comm_class α M' β] (S : submonoid M') :

smul_comm_class α ↥S β

source

@[protected, instance]

def submonoid.is_scalar_tower {M' : Type u_4} {α : Type u_5} {β : Type u_6} [mul_one_class M'] [has_smul α β] [has_smul M' α] [has_smul M' β] [is_scalar_tower M' α β] (S : submonoid M') :

is_scalar_tower ↥S α β

Note that this provides is_scalar_tower S M' M' which is needed by smul_mul_assoc.

source

theorem submonoid.smul_def {M' : Type u_4} {α : Type u_5} [mul_one_class M'] [has_smul M' α] {S : submonoid M'} (g : ↥S) (m : α) :

g • m = ↑g • m

source

theorem add_submonoid.vadd_def {M' : Type u_4} {α : Type u_5} [add_zero_class M'] [has_vadd M' α] {S : add_submonoid M'} (g : ↥S) (m : α) :

g +ᵥ m = ↑g +ᵥ m

source

@[protected, instance]

def submonoid.has_faithful_smul {M' : Type u_4} {α : Type u_5} [mul_one_class M'] [has_smul M' α] [has_faithful_smul M' α] (S : submonoid M') :

has_faithful_smul ↥S α

source

@[protected, instance]

def submonoid.mul_action {M' : Type u_4} {α : Type u_5} [monoid M'] [mul_action M' α] (S : submonoid M') :

mul_action ↥S α

The action by a submonoid is the action by the underlying monoid.

Equations

S.mul_action = mul_action.comp_hom α S.subtype

source

@[protected, instance]

def add_submonoid.add_action {M' : Type u_4} {α : Type u_5} [add_monoid M'] [add_action M' α] (S : add_submonoid M') :

add_action ↥S α

The additive action by an add_submonoid is the action by the underlying add_monoid.

Equations

S.add_action = add_action.comp_hom α S.subtype

source

@[protected, instance]

def submonoid.distrib_mul_action {M' : Type u_4} {α : Type u_5} [monoid M'] [add_monoid α] [distrib_mul_action M' α] (S : submonoid M') :

distrib_mul_action ↥S α

The action by a submonoid is the action by the underlying monoid.

Equations

S.distrib_mul_action = distrib_mul_action.comp_hom α S.subtype

source

@[protected, instance]

def submonoid.mul_distrib_mul_action {M' : Type u_4} {α : Type u_5} [monoid M'] [monoid α] [mul_distrib_mul_action M' α] (S : submonoid M') :

mul_distrib_mul_action ↥S α

The action by a submonoid is the action by the underlying monoid.

Equations

S.mul_distrib_mul_action = mul_distrib_mul_action.comp_hom α S.subtype

mathlib3 documentation

Operations on `submonoid`s #

Main definitions #

Conversion between multiplicative and additive definitions #

(Commutative) monoid structure on a submonoid #

Group actions by submonoids #

Operations on submonoids #

Monoid homomorphisms between submonoid #

Operations on `monoid_hom`s #

Tags #

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

`comap` and `map` #

Actions by `submonoid`s #

Operations on submonoids #

Main definitions #

Conversion between multiplicative and additive definitions #

(Commutative) monoid structure on a submonoid #

Group actions by submonoids #

Operations on submonoids #

Monoid homomorphisms between submonoid #

Operations on monoid_homs #

Tags #

Conversion to/from additive/multiplicative #

comap and map #

Actions by submonoids #

Operations on `submonoid`s #

Operations on `monoid_hom`s #

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

`comap` and `map` #

Actions by `submonoid`s #