mathlib3 documentation

algebra.category.Group.epi_mono

Monomorphisms and epimorphisms in Group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. In this file, we prove monomorphisms in category of group are injective homomorphisms and epimorphisms are surjective homomorphisms.

source
theorem monoid_hom.ker_eq_bot_of_cancel {A : Type u} {B : Type v} [group A] [group B] {f : A →* B} (h : ∀ (u v : ↥(f.ker) →* A), f.comp u = f.comp v → u = v) :
f.ker = ⊥
source
theorem add_monoid_hom.ker_eq_bot_of_cancel {A : Type u} {B : Type v} [add_group A] [add_group B] {f : A →+ B} (h : ∀ (u v : ↥(f.ker) →+ A), f.comp u = f.comp v → u = v) :
f.ker = ⊥
source
theorem monoid_hom.range_eq_top_of_cancel {A : Type u} {B : Type v} [comm_group A] [comm_group B] {f : A →* B} (h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v) :
f.range = ⊤
source
theorem add_monoid_hom.range_eq_top_of_cancel {A : Type u} {B : Type v} [add_comm_group A] [add_comm_group B] {f : A →+ B} (h : ∀ (u v : B →+ B ⧸ f.range), u.comp f = v.comp f → u = v) :
f.range = ⊤
source
theorem AddGroup.ker_eq_bot_of_mono {A B : AddGroup} (f : A ⟶ B) [category_theory.mono f] :
add_monoid_hom.ker f = ⊥
source
theorem Group.ker_eq_bot_of_mono {A B : Group} (f : A ⟶ B) [category_theory.mono f] :
monoid_hom.ker f = ⊥
source
theorem AddGroup.mono_iff_ker_eq_bot {A B : AddGroup} (f : A ⟶ B) :
category_theory.mono f ↔ add_monoid_hom.ker f = ⊥
source
theorem Group.mono_iff_ker_eq_bot {A B : Group} (f : A ⟶ B) :
category_theory.mono f ↔ monoid_hom.ker f = ⊥
source
theorem AddGroup.mono_iff_injective {A B : AddGroup} (f : A ⟶ B) :
category_theory.mono f ↔ function.injective ⇑f
source
theorem Group.mono_iff_injective {A B : Group} (f : A ⟶ B) :
category_theory.mono f ↔ function.injective ⇑f
source
@[nolint]
inductive Group.surjective_of_epi_auxs.X_with_infinity {A B : Group} (f : A ⟶ B) :
Type u

Define X' to be the set of all left cosets with an extra point at "infinity".

Instances for Group.surjective_of_epi_auxs.X_with_infinity
source
@[protected, instance]
def Group.surjective_of_epi_auxs.X_with_infinity.has_smul {A B : Group} (f : A ⟶ B) :
has_smul ↥B (Group.surjective_of_epi_auxs.X_with_infinity f)
Equations
source
theorem Group.surjective_of_epi_auxs.mul_smul {A B : Group} (f : A ⟶ B) (b b' : ↥B) (x : Group.surjective_of_epi_auxs.X_with_infinity f) :
(b * b') • x = b • b' • x
source
theorem Group.surjective_of_epi_auxs.one_smul {A B : Group} (f : A ⟶ B) (x : Group.surjective_of_epi_auxs.X_with_infinity f) :
1 • x = x
source
theorem Group.surjective_of_epi_auxs.from_coset_eq_of_mem_range {A B : Group} (f : A ⟶ B) {b : ↥B} (hb : b ∈ monoid_hom.range f) :
Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨left_coset b (monoid_hom.range f).carrier, _⟩ = Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨(monoid_hom.range f).carrier, _⟩
source
theorem Group.surjective_of_epi_auxs.from_coset_ne_of_nin_range {A B : Group} (f : A ⟶ B) {b : ↥B} (hb : b ∉ monoid_hom.range f) :
Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨left_coset b (monoid_hom.range f).carrier, _⟩ ≠ Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨(monoid_hom.range f).carrier, _⟩
source
@[protected, instance]
noncomputable def Group.surjective_of_epi_auxs.X_with_infinity.decidable_eq {A B : Group} (f : A ⟶ B) :
decidable_eq (Group.surjective_of_epi_auxs.X_with_infinity f)
Equations
source
noncomputable def Group.surjective_of_epi_auxs.tau {A B : Group} (f : A ⟶ B) :
equiv.perm (Group.surjective_of_epi_auxs.X_with_infinity f)

Let τ be the permutation on X' exchanging f.range and the point at infinity.

Equations
source
theorem Group.surjective_of_epi_auxs.τ_apply_infinity {A B : Group} (f : A ⟶ B) :
⇑(Group.surjective_of_epi_auxs.tau f) Group.surjective_of_epi_auxs.X_with_infinity.infinity = Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨(monoid_hom.range f).carrier, _⟩
source
theorem Group.surjective_of_epi_auxs.τ_apply_from_coset {A B : Group} (f : A ⟶ B) :
⇑(Group.surjective_of_epi_auxs.tau f) (Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨(monoid_hom.range f).carrier, _⟩) = Group.surjective_of_epi_auxs.X_with_infinity.infinity
source
theorem Group.surjective_of_epi_auxs.τ_apply_from_coset' {A B : Group} (f : A ⟶ B) (x : ↥B) (hx : x ∈ monoid_hom.range f) :
⇑(Group.surjective_of_epi_auxs.tau f) (Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨left_coset x (monoid_hom.range f).carrier, _⟩) = Group.surjective_of_epi_auxs.X_with_infinity.infinity
source
theorem Group.surjective_of_epi_auxs.τ_symm_apply_from_coset {A B : Group} (f : A ⟶ B) :
⇑(equiv.symm (Group.surjective_of_epi_auxs.tau f)) (Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨(monoid_hom.range f).carrier, _⟩) = Group.surjective_of_epi_auxs.X_with_infinity.infinity
source
theorem Group.surjective_of_epi_auxs.τ_symm_apply_infinity {A B : Group} (f : A ⟶ B) :
⇑(equiv.symm (Group.surjective_of_epi_auxs.tau f)) Group.surjective_of_epi_auxs.X_with_infinity.infinity = Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨(monoid_hom.range f).carrier, _⟩
source
def Group.surjective_of_epi_auxs.G {A B : Group} (f : A ⟶ B) :
↥B →* equiv.perm (Group.surjective_of_epi_auxs.X_with_infinity f)

Let g : B ⟶ S(X') be defined as such that, for any β : B, g(β) is the function sending point at infinity to point at infinity and sending coset y to β *l y.

Equations
source
noncomputable def Group.surjective_of_epi_auxs.H {A B : Group} (f : A ⟶ B) :
↥B →* equiv.perm (Group.surjective_of_epi_auxs.X_with_infinity f)

Define h : B ⟶ S(X') to be τ g τ⁻¹

Equations

The strategy is the following: assuming epi f

source
theorem Group.surjective_of_epi_auxs.g_apply_from_coset {A B : Group} (f : A ⟶ B) (x : ↥B) (y : ↥(set.range (function.swap left_coset (monoid_hom.range f).carrier))) :
⇑(⇑(Group.surjective_of_epi_auxs.G f) x) (Group.surjective_of_epi_auxs.X_with_infinity.from_coset y) = Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨left_coset x ↑y, _⟩
source
theorem Group.surjective_of_epi_auxs.g_apply_infinity {A B : Group} (f : A ⟶ B) (x : ↥B) :
⇑(⇑(Group.surjective_of_epi_auxs.G f) x) Group.surjective_of_epi_auxs.X_with_infinity.infinity = Group.surjective_of_epi_auxs.X_with_infinity.infinity
source
theorem Group.surjective_of_epi_auxs.h_apply_infinity {A B : Group} (f : A ⟶ B) (x : ↥B) (hx : x ∈ monoid_hom.range f) :
⇑(⇑(Group.surjective_of_epi_auxs.H f) x) Group.surjective_of_epi_auxs.X_with_infinity.infinity = Group.surjective_of_epi_auxs.X_with_infinity.infinity
source
theorem Group.surjective_of_epi_auxs.h_apply_from_coset {A B : Group} (f : A ⟶ B) (x : ↥B) :
⇑(⇑(Group.surjective_of_epi_auxs.H f) x) (Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨(monoid_hom.range f).carrier, _⟩) = Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨(monoid_hom.range f).carrier, _⟩
source
theorem Group.surjective_of_epi_auxs.h_apply_from_coset' {A B : Group} (f : A ⟶ B) (x b : ↥B) (hb : b ∈ monoid_hom.range f) :
⇑(⇑(Group.surjective_of_epi_auxs.H f) x) (Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨left_coset b (monoid_hom.range f).carrier, _⟩) = Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨left_coset b (monoid_hom.range f).carrier, _⟩
source
theorem Group.surjective_of_epi_auxs.h_apply_from_coset_nin_range {A B : Group} (f : A ⟶ B) (x : ↥B) (hx : x ∈ monoid_hom.range f) (b : ↥B) (hb : b ∉ monoid_hom.range f) :
⇑(⇑(Group.surjective_of_epi_auxs.H f) x) (Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨left_coset b (monoid_hom.range f).carrier, _⟩) = Group.surjective_of_epi_auxs.X_with_infinity.from_coset ⟨left_coset (x * b) (monoid_hom.range f).carrier, _⟩
source
theorem Group.surjective_of_epi_auxs.agree {A B : Group} (f : A ⟶ B) :
(monoid_hom.range f).carrier = {x : ↥B | ⇑(Group.surjective_of_epi_auxs.H f) x = ⇑(Group.surjective_of_epi_auxs.G f) x}
source
theorem Group.surjective_of_epi_auxs.comp_eq {A B : Group} (f : A ⟶ B) :
(f ≫ show B ⟶ Group.of (equiv.perm (Group.surjective_of_epi_auxs.X_with_infinity f)), from Group.surjective_of_epi_auxs.G f) = f ≫ Group.surjective_of_epi_auxs.H f
source
theorem Group.surjective_of_epi_auxs.g_ne_h {A B : Group} (f : A ⟶ B) (x : ↥B) (hx : x ∉ monoid_hom.range f) :
Group.surjective_of_epi_auxs.G f ≠ Group.surjective_of_epi_auxs.H f
source
theorem Group.surjective_of_epi {A B : Group} (f : A ⟶ B) [category_theory.epi f] :
function.surjective ⇑f
source
theorem Group.epi_iff_surjective {A B : Group} (f : A ⟶ B) :
category_theory.epi f ↔ function.surjective ⇑f
source
theorem Group.epi_iff_range_eq_top {A B : Group} (f : A ⟶ B) :
category_theory.epi f ↔ monoid_hom.range f = ⊤
source
theorem AddGroup.epi_iff_surjective {A B : AddGroup} (f : A ⟶ B) :
category_theory.epi f ↔ function.surjective ⇑f
source
theorem AddGroup.epi_iff_range_eq_top {A B : AddGroup} (f : A ⟶ B) :
category_theory.epi f ↔ add_monoid_hom.range f = ⊤
source
@[protected, instance]
def Group.forget_Group_preserves_mono  :
(category_theory.forget Group).preserves_monomorphisms
source
@[protected, instance]
def AddGroup.forget_Group_preserves_mono  :
(category_theory.forget AddGroup).preserves_monomorphisms
source
@[protected, instance]
def Group.forget_Group_preserves_epi  :
(category_theory.forget Group).preserves_epimorphisms
source
@[protected, instance]
def AddGroup.forget_Group_preserves_epi  :
(category_theory.forget AddGroup).preserves_epimorphisms
source
theorem CommGroup.ker_eq_bot_of_mono {A B : CommGroup} (f : A ⟶ B) [category_theory.mono f] :
monoid_hom.ker f = ⊥
source
theorem AddCommGroup.ker_eq_bot_of_mono {A B : AddCommGroup} (f : A ⟶ B) [category_theory.mono f] :
add_monoid_hom.ker f = ⊥
source
theorem CommGroup.mono_iff_ker_eq_bot {A B : CommGroup} (f : A ⟶ B) :
category_theory.mono f ↔ monoid_hom.ker f = ⊥
source
theorem AddCommGroup.mono_iff_ker_eq_bot {A B : AddCommGroup} (f : A ⟶ B) :
category_theory.mono f ↔ add_monoid_hom.ker f = ⊥
source
theorem AddCommGroup.mono_iff_injective {A B : AddCommGroup} (f : A ⟶ B) :
category_theory.mono f ↔ function.injective ⇑f
source
theorem CommGroup.mono_iff_injective {A B : CommGroup} (f : A ⟶ B) :
category_theory.mono f ↔ function.injective ⇑f
source
theorem CommGroup.range_eq_top_of_epi {A B : CommGroup} (f : A ⟶ B) [category_theory.epi f] :
monoid_hom.range f = ⊤
source
theorem AddCommGroup.range_eq_top_of_epi {A B : AddCommGroup} (f : A ⟶ B) [category_theory.epi f] :
add_monoid_hom.range f = ⊤
source
theorem AddCommGroup.epi_iff_range_eq_top {A B : AddCommGroup} (f : A ⟶ B) :
category_theory.epi f ↔ add_monoid_hom.range f = ⊤
source
theorem CommGroup.epi_iff_range_eq_top {A B : CommGroup} (f : A ⟶ B) :
category_theory.epi f ↔ monoid_hom.range f = ⊤
source
theorem AddCommGroup.epi_iff_surjective {A B : AddCommGroup} (f : A ⟶ B) :
category_theory.epi f ↔ function.surjective ⇑f
source
theorem CommGroup.epi_iff_surjective {A B : CommGroup} (f : A ⟶ B) :
category_theory.epi f ↔ function.surjective ⇑f
source
@[protected, instance]
def AddCommGroup.forget_CommGroup_preserves_mono  :
(category_theory.forget AddCommGroup).preserves_monomorphisms
source
@[protected, instance]
def CommGroup.forget_CommGroup_preserves_mono  :
(category_theory.forget CommGroup).preserves_monomorphisms
source
@[protected, instance]
def CommGroup.forget_CommGroup_preserves_epi  :
(category_theory.forget CommGroup).preserves_epimorphisms
source
@[protected, instance]
def AddCommGroup.forget_CommGroup_preserves_epi  :
(category_theory.forget AddCommGroup).preserves_epimorphisms