Index of a Subgroup #
In this file we define the index of a subgroup, and prove several divisibility properties. Several theorems proved in this file are known as Lagrange's theorem.
Main definitions #
H.index
: the index ofH : subgroup G
as a natural number, and returns 0 if the index is infinite.H.relindex K
: the relative index ofH : subgroup G
inK : subgroup G
as a natural number, and returns 0 if the relative index is infinite.
Main results #
card_mul_index
:nat.card H * H.index = nat.card G
index_mul_card
:H.index * fintype.card H = fintype.card G
index_dvd_card
:H.index ∣ fintype.card G
index_eq_mul_of_le
: IfH ≤ K
, thenH.index = K.index * (H.subgroup_of K).index
index_dvd_of_le
: IfH ≤ K
, thenK.index ∣ H.index
relindex_mul_relindex
:relindex
is multiplicative in towers
The index of a subgroup as a natural number, and returns 0 if the index is infinite.
The relative index of a subgroup as a natural number, and returns 0 if the relative index is infinite.
Equations
- H.relindex K = (H.subgroup_of K).index
The relative index of a subgroup as a natural number, and returns 0 if the relative index is infinite.
Equations
- H.relindex K = (H.add_subgroup_of K).index
theorem
subgroup.index_comap_of_surjective
{G : Type u_1}
[group G]
(H : subgroup G)
{G' : Type u_2}
[group G']
{f : G' →* G}
(hf : function.surjective ⇑f) :
(subgroup.comap f H).index = H.index
theorem
add_subgroup.index_comap_of_surjective
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{G' : Type u_2}
[add_group G']
{f : G' →+ G}
(hf : function.surjective ⇑f) :
(add_subgroup.comap f H).index = H.index
theorem
add_subgroup.index_comap
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{G' : Type u_2}
[add_group G']
(f : G' →+ G) :
(add_subgroup.comap f H).index = H.relindex f.range
theorem
add_subgroup.relindex_comap
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{G' : Type u_2}
[add_group G']
(f : G' →+ G)
(K : add_subgroup G') :
(add_subgroup.comap f H).relindex K = H.relindex (add_subgroup.map f K)
theorem
subgroup.relindex_comap
{G : Type u_1}
[group G]
(H : subgroup G)
{G' : Type u_2}
[group G']
(f : G' →* G)
(K : subgroup G') :
(subgroup.comap f H).relindex K = H.relindex (subgroup.map f K)
theorem
add_subgroup.index_dvd_of_le
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h : H ≤ K) :
theorem
add_subgroup.relindex_dvd_index_of_le
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h : H ≤ K) :
theorem
add_subgroup.relindex_add_subgroup_of
{G : Type u_1}
[add_group G]
{H K L : add_subgroup G}
(hKL : K ≤ L) :
(H.add_subgroup_of L).relindex (K.add_subgroup_of L) = H.relindex K
theorem
subgroup.relindex_subgroup_of
{G : Type u_1}
[group G]
{H K L : subgroup G}
(hKL : K ≤ L) :
(H.subgroup_of L).relindex (K.subgroup_of L) = H.relindex K
@[simp]
theorem
add_subgroup.relindex_sup_right
{G : Type u_1}
[add_group G]
(H K : add_subgroup G)
[K.normal] :
@[simp]
theorem
add_subgroup.relindex_sup_left
{G : Type u_1}
[add_group G]
(H K : add_subgroup G)
[K.normal] :
theorem
add_subgroup.relindex_dvd_index_of_normal
{G : Type u_1}
[add_group G]
(H K : add_subgroup G)
[H.normal] :
theorem
add_subgroup.relindex_dvd_of_le_left
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(L : add_subgroup G)
(hHK : H ≤ K) :
theorem
add_subgroup.add_self_mem_of_index_two
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
(h : H.index = 2)
(a : G) :
theorem
add_subgroup.two_smul_mem_of_index_two
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
(h : H.index = 2)
(a : G) :
theorem
add_subgroup.index_bot_eq_card
{G : Type u_1}
[add_group G]
[fintype G] :
⊥.index = fintype.card G
@[simp]
@[simp]
@[simp]
theorem
add_subgroup.relindex_bot_left_eq_card
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[fintype ↥H] :
⊥.relindex H = fintype.card ↥H
@[simp]
@[simp]
theorem
add_subgroup.card_dvd_of_surjective
{G : Type u_1}
{H : Type u_2}
[add_group G]
[add_group H]
[fintype G]
[fintype H]
(f : G →+ H)
(hf : function.surjective ⇑f) :
theorem
subgroup.card_dvd_of_surjective
{G : Type u_1}
{H : Type u_2}
[group G]
[group H]
[fintype G]
[fintype H]
(f : G →* H)
(hf : function.surjective ⇑f) :
theorem
add_subgroup.index_map_dvd
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{G' : Type u_2}
[add_group G']
{f : G →+ G'}
(hf : function.surjective ⇑f) :
(add_subgroup.map f H).index ∣ H.index
theorem
subgroup.index_map_dvd
{G : Type u_1}
[group G]
(H : subgroup G)
{G' : Type u_2}
[group G']
{f : G →* G'}
(hf : function.surjective ⇑f) :
(subgroup.map f H).index ∣ H.index
theorem
add_subgroup.dvd_index_map
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{G' : Type u_2}
[add_group G']
{f : G →+ G'}
(hf : f.ker ≤ H) :
H.index ∣ (add_subgroup.map f H).index
theorem
add_subgroup.index_map_eq
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{G' : Type u_2}
[add_group G']
{f : G →+ G'}
(hf1 : function.surjective ⇑f)
(hf2 : f.ker ≤ H) :
(add_subgroup.map f H).index = H.index
theorem
add_subgroup.index_eq_card
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[fintype (G ⧸ H)] :
H.index = fintype.card (G ⧸ H)
theorem
subgroup.index_mul_card
{G : Type u_1}
[group G]
(H : subgroup G)
[fintype G]
[hH : fintype ↥H] :
H.index * fintype.card ↥H = fintype.card G
theorem
add_subgroup.index_mul_card
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[fintype G]
[hH : fintype ↥H] :
H.index * fintype.card ↥H = fintype.card G
theorem
subgroup.index_dvd_card
{G : Type u_1}
[group G]
(H : subgroup G)
[fintype G] :
H.index ∣ fintype.card G
theorem
add_subgroup.index_dvd_card
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[fintype G] :
H.index ∣ fintype.card G
theorem
add_subgroup.relindex_eq_zero_of_le_left
{G : Type u_1}
[add_group G]
{H K L : add_subgroup G}
(hHK : H ≤ K)
(hKL : K.relindex L = 0) :
theorem
add_subgroup.relindex_eq_zero_of_le_right
{G : Type u_1}
[add_group G]
{H K L : add_subgroup G}
(hKL : K ≤ L)
(hHK : H.relindex K = 0) :
theorem
add_subgroup.index_eq_zero_of_relindex_eq_zero
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h : H.relindex K = 0) :
theorem
add_subgroup.relindex_infi_le
{G : Type u_1}
[add_group G]
{L : add_subgroup G}
{ι : Type u_2}
[fintype ι]
(f : ι → add_subgroup G) :
theorem
add_subgroup.index_infi_le
{G : Type u_1}
[add_group G]
{ι : Type u_2}
[fintype ι]
(f : ι → add_subgroup G) :
@[simp]
@[simp]
theorem
add_subgroup.index_ne_zero_of_finite
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
[hH : finite (G ⧸ H)] :
noncomputable
def
add_subgroup.fintype_of_index_ne_zero
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
(hH : H.index ≠ 0) :
Finite index implies finite quotient.
Equations
@[class]
Typeclass for finite index subgroups.
@[class]
Typeclass for finite index subgroups.
noncomputable
def
subgroup.fintype_quotient_of_finite_index
{G : Type u_1}
[group G]
(H : subgroup G)
[H.finite_index] :
A finite index subgroup has finite quotient.
noncomputable
def
add_subgroup.fintype_quotient_of_finite_index
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[H.finite_index] :
A finite index subgroup has finite quotient
@[protected, instance]
def
add_subgroup.finite_quotient_of_finite_index
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[H.finite_index] :
@[protected, instance]
def
subgroup.finite_quotient_of_finite_index
{G : Type u_1}
[group G]
(H : subgroup G)
[H.finite_index] :
theorem
add_subgroup.finite_index_of_finite_quotient
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[finite (G ⧸ H)] :
@[protected, instance]
def
add_subgroup.finite_index_of_finite
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[finite G] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
add_subgroup.has_inf.inf.finite_index
{G : Type u_1}
[add_group G]
(H K : add_subgroup G)
[H.finite_index]
[K.finite_index] :
(H ⊓ K).finite_index
@[protected, instance]
def
subgroup.has_inf.inf.finite_index
{G : Type u_1}
[group G]
(H K : subgroup G)
[H.finite_index]
[K.finite_index] :
(H ⊓ K).finite_index
theorem
subgroup.finite_index_of_le
{G : Type u_1}
[group G]
{H K : subgroup G}
[H.finite_index]
(h : H ≤ K) :
theorem
add_subgroup.finite_index_of_le
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
[H.finite_index]
(h : H ≤ K) :
@[protected, instance]
@[protected, instance]
def
subgroup.finite_index_center
(G : Type u_1)
[group G]
[finite ↥(commutator_set G)]
[group.fg G] :
theorem
subgroup.index_center_le_pow
(G : Type u_1)
[group G]
[finite ↥(commutator_set G)]
[group.fg G] :
(subgroup.center G).index ≤ nat.card ↥(commutator_set G) ^ group.rank G