index_comap — Mathlib

English

For subgroups H, K ⊆ G and a homomorphism f: G' →* G, the relative index relIndex(comap f H, K) equals relIndex(H, map f K).

Русский

Для подгрупп H, K ⊆ G и гомоморфизма f: G' →* G верно relIndex(comap f H, K) = relIndex(H, map f K).

LaTeX

$$$\\mathrm{relIndex}(\\mathrm{comap}\\ f\, H, K) = \\mathrm{relIndex}(H, \\mathrm{map}\ f\ K).$$$

Lean4

@[to_additive]
theorem index_comap (f : G' →* G) : (H.comap f).index = H.relIndex f.range :=
  Eq.trans (congr_arg index (by rfl)) ((H.subgroupOf f.range).index_comap_of_surjective f.rangeRestrict_surjective)

Похожие утверждения