English
Let f: G →* G' and J, K be subgroups of G'. If J.relIndex K ≠ 0, then (preimage under f) J.comap f has relative index in (K.comap f) which is not zero.
Русский
Пусть f: G →* G' и J, K подгруппы G'. Если J.relIndex K ≠ 0, то их прообраз через f имеет ненулевой относительный индекс в прообразе K.
LaTeX
$$$(J \relIndex K \neq 0) \rightarrow (J.\comap f).\relIndex (K.\comap f) \neq 0$$$
Lean4
/-- If `J` has finite index in `K`, then the same holds for their comaps under any group hom. -/
@[to_additive /-- If `J` has finite index in `K`, then the same holds for their comaps under any
additive group hom. -/
]
theorem relIndex_comap_ne_zero (f : G →* G') {J K : Subgroup G'} (hJK : J.relIndex K ≠ 0) :
(J.comap f).relIndex (K.comap f) ≠ 0 := by
rw [relIndex_comap]
exact fun h ↦ hJK <| relIndex_eq_zero_of_le_right (map_comap_le _ _) h
