Subgroup.map_eq_ker_of_comp_ker_eq_sup_of_left_le_ker
Suppose φ is surjective, the kernel of ψ.comp φ is Z ⊔ U, and Z is already killed by φ. Then the image of U is exactly the kernel of ψ.
Source context 1 command
Surrounding namespaces, section variables, and local commands at this declaration.
namespace SubgroupLean source · statement
theorem map_eq_ker_of_comp_ker_eq_sup_of_left_le_ker
{A G H : Type*} [Group A] [Group G] [Group H]
(φ : A →* G) (ψ : G →* H) (Z U : Subgroup A)
(hφ : Function.Surjective φ)
(hker : (ψ.comp φ).ker = Z ⊔ U)
(hZ : Z ≤ φ.ker) :
U.map φ = ψ.ker