Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-19 03:29 45140211

View on Github →

feat(algebra/category_theory/Group/epi_mono): about monomorphism and epimorphism in category of group (#14720) This pr proves that monomorphism and injective homomorphism are the same and epimorphism and surjective homomorphism are the same in Group. For CommGroup, AddGroup and AddCommGroup, the same is proved in #15496

Estimated changes

Created src/algebra/category/Group/epi_mono.lean

added theorem Group.epi_iff_range_eq_top

added theorem Group.epi_iff_surjective

added theorem Group.ker_eq_bot_of_mono

added theorem Group.mono_iff_injective

added theorem Group.mono_iff_ker_eq_bot

added theorem Group.surjective_of_epi

added def Group.surjective_of_epi_auxs.G

added def Group.surjective_of_epi_auxs.H

added inductive Group.surjective_of_epi_auxs.X_with_infinity

added theorem Group.surjective_of_epi_auxs.agree

added theorem Group.surjective_of_epi_auxs.comp_eq

added theorem Group.surjective_of_epi_auxs.from_coset_eq_of_mem_range

added theorem Group.surjective_of_epi_auxs.from_coset_ne_of_nin_range

added theorem Group.surjective_of_epi_auxs.g_apply_from_coset

added theorem Group.surjective_of_epi_auxs.g_apply_infinity

added theorem Group.surjective_of_epi_auxs.g_ne_h

added theorem Group.surjective_of_epi_auxs.h_apply_from_coset'

added theorem Group.surjective_of_epi_auxs.h_apply_from_coset

added theorem Group.surjective_of_epi_auxs.h_apply_from_coset_nin_range

added theorem Group.surjective_of_epi_auxs.h_apply_infinity

added theorem Group.surjective_of_epi_auxs.mul_smul

added theorem Group.surjective_of_epi_auxs.one_smul

added theorem Group.surjective_of_epi_auxs.τ_apply_from_coset'

added theorem Group.surjective_of_epi_auxs.τ_apply_from_coset

added theorem Group.surjective_of_epi_auxs.τ_apply_infinity

added theorem Group.surjective_of_epi_auxs.τ_symm_apply_from_coset

added theorem Group.surjective_of_epi_auxs.τ_symm_apply_infinity

added theorem monoid_hom.ker_eq_bot_of_cancel

Modified src/group_theory/subgroup/basic.lean

added theorem monoid_hom.range_one