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_mul_index
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h : H ≤ 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
theorem
add_subgroup.inf_relindex_eq_relindex_sup
{G : Type u_1}
[add_group G]
(H K : add_subgroup G)
[K.normal] :
theorem
add_subgroup.relindex_eq_relindex_sup
{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.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]
@[simp]
theorem
subgroup.nat_card_dvd_of_injective
{G : Type u_1}
{H : Type u_2}
[group G]
[group H]
(f : G →* H)
(hf : function.injective ⇑f) :
theorem
add_subgroup.nat_card_dvd_of_injective
{G : Type u_1}
{H : Type u_2}
[add_group G]
[add_group H]
(f : G →+ H)
(hf : function.injective ⇑f) :
theorem
subgroup.nat_card_dvd_of_surjective
{G : Type u_1}
{H : Type u_2}
[group G]
[group H]
(f : G →* H)
(hf : function.surjective ⇑f) :
theorem
add_subgroup.nat_card_dvd_of_surjective
{G : Type u_1}
{H : Type u_2}
[add_group G]
[add_group H]
(f : G →+ H)
(hf : function.surjective ⇑f) :
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
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{G' : Type u_2}
[add_group G']
(f : G →+ G') :
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
subgroup.index_map_eq
{G : Type u_1}
[group G]
(H : subgroup G)
{G' : Type u_2}
[group G']
{f : G →* G'}
(hf1 : function.surjective ⇑f)
(hf2 : f.ker ≤ H) :
(subgroup.map f H).index = H.index
theorem
subgroup.index_eq_card
{G : Type u_1}
[group G]
(H : subgroup G)
[fintype (G ⧸ H)] :
H.index = fintype.card (G ⧸ H)
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.relindex_le_of_le_left
{G : Type u_1}
[add_group G]
{H K L : add_subgroup G}
(hHK : H ≤ K)
(hHL : H.relindex L ≠ 0) :
theorem
add_subgroup.relindex_le_of_le_right
{G : Type u_1}
[add_group G]
{H K L : add_subgroup G}
(hKL : K ≤ L)
(hHL : H.relindex L ≠ 0) :
theorem
add_subgroup.relindex_ne_zero_trans
{G : Type u_1}
[add_group G]
{H K L : add_subgroup G}
(hHK : H.relindex K ≠ 0)
(hKL : K.relindex L ≠ 0) :
@[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
theorem
add_subgroup.one_lt_index_of_ne_top
{G : Type u_1}
[add_group G]
{H : add_subgroup G}
[finite (G ⧸ H)]
(hH : H ≠ ⊤) :