EtaleFundamentalGroups.Inertia.map_eq_of_isPGroup_of_index_not_dvd
A surjective homomorphism of finite groups maps a p-subgroup of prime-to-p index onto the normal p-subgroup of prime-to-p index in the target. Both preservation and element lifting follow from this literal image equality.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
universe u vLean source · statement
theorem map_eq_of_isPGroup_of_index_not_dvd
(p : ℕ) [Fact p.Prime]
{G : Type u} {H : Type v} [Group G] [Group H] [Finite G]
(f : G →* H) (hf : Function.Surjective f)
(P : Subgroup G) (Q : Subgroup H) [Q.Normal]
(hP : IsPGroup p P) (hQ : IsPGroup p Q)
(hPindex : ¬ p ∣ P.index) (hQindex : ¬ p ∣ Q.index) :
P.map f = Q