Theorems · Theorem · group theory

Subgroup.IsFinitelyNormallyGenerated.comap

∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {N : Subgroup H},
  N.IsFinitelyNormallyGenerated →
    ∀ {f : G →* H},
      Function.Surjective ⇑f → f.ker.IsFinitelyNormallyGenerated → (Subgroup.comap f N).IsFinitelyNormallyGenerated

The preimage of a finitely generated normal subgroup by a surjective homomorphism with a finitely generated kernel is finitely generated.

Defined in

Mathlib.GroupTheory.FinitelyPresentedGroup

Cited by

1 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupGroup