English
If f: G' →* G is surjective, then the index of the comapped subgroup equals the index of the original subgroup.
Русский
Пусть f: G' →* G сюръективно; тогда индекс подгруппы, взятой по образу, равен индексу исходной подгруппы.
LaTeX
$$$ (H \\!\\! \\text{comap } f).\\!\\index = H.\\!\\index $.$$
Lean4
@[to_additive]
theorem index_comap_of_surjective {f : G' →* G} (hf : Function.Surjective f) : (H.comap f).index = H.index :=
by
have key : ∀ x y : G', QuotientGroup.leftRel (H.comap f) x y ↔ QuotientGroup.leftRel H (f x) (f y) :=
by
simp only [QuotientGroup.leftRel_apply]
exact fun x y => iff_of_eq (congr_arg (· ∈ H) (by rw [f.map_mul, f.map_inv]))
refine Cardinal.toNat_congr (Equiv.ofBijective (Quotient.map' f fun x y => (key x y).mp) ⟨?_, ?_⟩)
· simp_rw [← Quotient.eq''] at key
refine Quotient.ind' fun x => ?_
refine Quotient.ind' fun y => ?_
exact (key x y).mpr
· refine Quotient.ind' fun x => ?_
obtain ⟨y, hy⟩ := hf x
exact ⟨y, (Quotient.map'_mk'' f _ y).trans (congr_arg Quotient.mk'' hy)⟩
