The index of a preimage

The preimage of a subgroup H ≤ G under a homomorphism f : G' →* G has index the relative index of H in the range of f (Mathlib's Subgroup.index_comap). So it never exceeds the index of H when that is finite (Subgroup.index_comap_le), and it is strictly smaller when the range of f lies in a proper subgroup containing H, being then at most the relative index of H in that subgroup (Subgroup.index_comap_lt_of_range_le).

Main results

• Subgroup.index_comap_le: a preimage of a subgroup of finite index has at most its index.
• Subgroup.index_comap_lt_of_range_le: if the range lies in a proper subgroup containing H, the preimage of H has smaller index.

theorem Subgroup.index_comap_le {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G' →* G) [H.FiniteIndex] : (comap f H).index ≤ H.index

The preimage of a subgroup of finite index under a homomorphism has at most its index.

theorem AddSubgroup.index_comap_le {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G' →+ G) [H.FiniteIndex] : (comap f H).index ≤ H.index

The preimage of a subgroup of finite index under a homomorphism has at most its index.

theorem Subgroup.index_comap_lt_of_range_le {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) {K : Subgroup G} (f : G' →* G) [H.FiniteIndex] (hHK : H ≤ K) (hK : K ≠ ⊤) (hf : f.range ≤ K) : (comap f H).index < H.index

If the range of f lies in a proper subgroup K containing a subgroup H of finite index, then the preimage of H has smaller index than H: its index is at most [K : H].

theorem AddSubgroup.index_comap_lt_of_range_le {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {K : AddSubgroup G} (f : G' →+ G) [H.FiniteIndex] (hHK : H ≤ K) (hK : K ≠ ⊤) (hf : f.range ≤ K) : (comap f H).index < H.index

If the range of f lies in a proper subgroup K containing a subgroup H of finite index, then the preimage of H has smaller index than H: its index is at most [K : H].