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
relindex_mul_index
: IfH ≤ K
, thenH.relindex K * K.index = H.index
index_dvd_of_le
: IfH ≤ K
, thenK.index ∣ H.index
relindex_mul_relindex
:relindex
is multiplicative in towersMulAction.index_stabilizer
: the index of the stabilizer is the cardinality of the orbit
The index of an additive subgroup as a natural number. Returns 0 if the index is infinite.
Instances For
theorem
Subgroup.index_comap_of_surjective
{G : Type u_1}
{G' : Type u_2}
[Group G]
[Group G']
(H : Subgroup G)
{f : G' →* G}
(hf : Function.Surjective ⇑f)
:
(Subgroup.comap f H).index = H.index
theorem
AddSubgroup.index_comap_of_surjective
{G : Type u_1}
{G' : Type u_2}
[AddGroup G]
[AddGroup G']
(H : AddSubgroup G)
{f : G' →+ G}
(hf : Function.Surjective ⇑f)
:
(AddSubgroup.comap f H).index = H.index
theorem
Subgroup.index_comap
{G : Type u_1}
{G' : Type u_2}
[Group G]
[Group G']
(H : Subgroup G)
(f : G' →* G)
:
(Subgroup.comap f H).index = H.relindex f.range
theorem
AddSubgroup.index_comap
{G : Type u_1}
{G' : Type u_2}
[AddGroup G]
[AddGroup G']
(H : AddSubgroup G)
(f : G' →+ G)
:
(AddSubgroup.comap f H).index = H.relindex f.range
theorem
Subgroup.relindex_comap
{G : Type u_1}
{G' : Type u_2}
[Group G]
[Group G']
(H : Subgroup G)
(f : G' →* G)
(K : Subgroup G')
:
(Subgroup.comap f H).relindex K = H.relindex (Subgroup.map f K)
theorem
AddSubgroup.relindex_comap
{G : Type u_1}
{G' : Type u_2}
[AddGroup G]
[AddGroup G']
(H : AddSubgroup G)
(f : G' →+ G)
(K : AddSubgroup G')
:
(AddSubgroup.comap f H).relindex K = H.relindex (AddSubgroup.map f K)
theorem
AddSubgroup.relindex_mul_index
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(h : H ≤ K)
:
theorem
AddSubgroup.index_dvd_of_le
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(h : H ≤ K)
:
K.index ∣ H.index
theorem
AddSubgroup.relindex_dvd_index_of_le
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(h : H ≤ K)
:
H.relindex K ∣ H.index
theorem
AddSubgroup.relindex_addSubgroupOf
{G : Type u_1}
[AddGroup G]
{H K L : AddSubgroup G}
(hKL : K ≤ L)
:
(H.addSubgroupOf L).relindex (K.addSubgroupOf L) = H.relindex K
theorem
AddSubgroup.relindex_mul_relindex
{G : Type u_1}
[AddGroup G]
(H K L : AddSubgroup G)
(hHK : H ≤ K)
(hKL : K ≤ L)
:
@[simp]
theorem
AddSubgroup.relindex_sup_right
{G : Type u_1}
[AddGroup G]
(H K : AddSubgroup G)
[K.Normal]
:
@[simp]
theorem
AddSubgroup.relindex_sup_left
{G : Type u_1}
[AddGroup G]
(H K : AddSubgroup G)
[K.Normal]
:
theorem
AddSubgroup.relindex_dvd_index_of_normal
{G : Type u_1}
[AddGroup G]
(H K : AddSubgroup G)
[H.Normal]
:
H.relindex K ∣ H.index
theorem
AddSubgroup.relindex_dvd_of_le_left
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(L : AddSubgroup G)
(hHK : H ≤ K)
:
K.relindex L ∣ H.relindex L
theorem
AddSubgroup.add_self_mem_of_index_two
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
(h : H.index = 2)
(a : G)
:
theorem
AddSubgroup.two_smul_mem_of_index_two
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
(h : H.index = 2)
(a : G)
:
@[deprecated Subgroup.index_bot]
Alias of Subgroup.index_bot
.
@[simp]
@[simp]
@[simp]
@[deprecated Subgroup.relindex_bot_left]
Alias of Subgroup.relindex_bot_left
.
@[simp]
@[simp]
theorem
AddSubgroup.relindex_ker
{G : Type u_1}
{G' : Type u_2}
[AddGroup G]
[AddGroup G']
(K : AddSubgroup G)
(f : G →+ G')
:
f.ker.relindex K = Nat.card ↥(AddSubgroup.map f K)
@[simp]
@[deprecated Subgroup.card_dvd_of_injective]
theorem
Subgroup.nat_card_dvd_of_injective
{α : Type u_1}
[Group α]
{H : Type u_2}
[Group H]
(f : α →* H)
(hf : Function.Injective ⇑f)
:
Alias of Subgroup.card_dvd_of_injective
.
@[deprecated Subgroup.card_dvd_of_le]
Alias of Subgroup.card_dvd_of_le
.
@[deprecated Subgroup.card_dvd_of_surjective]
theorem
Subgroup.nat_card_dvd_of_surjective
{G : Type u_1}
{G' : Type u_2}
[Group G]
[Group G']
(f : G →* G')
(hf : Function.Surjective ⇑f)
:
Alias of Subgroup.card_dvd_of_surjective
.
theorem
AddSubgroup.card_map_dvd
{G : Type u_1}
{G' : Type u_2}
[AddGroup G]
[AddGroup G']
(H : AddSubgroup G)
(f : G →+ G')
:
Nat.card ↥(AddSubgroup.map f H) ∣ Nat.card ↥H
theorem
AddSubgroup.index_map
{G : Type u_1}
{G' : Type u_2}
[AddGroup G]
[AddGroup G']
(H : AddSubgroup G)
(f : G →+ G')
:
(AddSubgroup.map f H).index = (H ⊔ f.ker).index * f.range.index
theorem
Subgroup.index_map_dvd
{G : Type u_1}
{G' : Type u_2}
[Group G]
[Group G']
(H : Subgroup G)
{f : G →* G'}
(hf : Function.Surjective ⇑f)
:
(Subgroup.map f H).index ∣ H.index
theorem
AddSubgroup.index_map_dvd
{G : Type u_1}
{G' : Type u_2}
[AddGroup G]
[AddGroup G']
(H : AddSubgroup G)
{f : G →+ G'}
(hf : Function.Surjective ⇑f)
:
(AddSubgroup.map f H).index ∣ H.index
theorem
AddSubgroup.dvd_index_map
{G : Type u_1}
{G' : Type u_2}
[AddGroup G]
[AddGroup G']
(H : AddSubgroup G)
{f : G →+ G'}
(hf : f.ker ≤ H)
:
H.index ∣ (AddSubgroup.map f H).index
theorem
Subgroup.index_map_eq
{G : Type u_1}
{G' : Type u_2}
[Group G]
[Group G']
(H : Subgroup G)
{f : G →* G'}
(hf1 : Function.Surjective ⇑f)
(hf2 : f.ker ≤ H)
:
(Subgroup.map f H).index = H.index
theorem
AddSubgroup.index_map_eq
{G : Type u_1}
{G' : Type u_2}
[AddGroup G]
[AddGroup G']
(H : AddSubgroup G)
{f : G →+ G'}
(hf1 : Function.Surjective ⇑f)
(hf2 : f.ker ≤ H)
:
(AddSubgroup.map f H).index = H.index
theorem
Subgroup.index_map_of_injective
{G : Type u_1}
{G' : Type u_2}
[Group G]
[Group G']
(H : Subgroup G)
{f : G →* G'}
(hf : Function.Injective ⇑f)
:
(Subgroup.map f H).index = H.index * f.range.index
theorem
AddSubgroup.index_map_of_injective
{G : Type u_1}
{G' : Type u_2}
[AddGroup G]
[AddGroup G']
(H : AddSubgroup G)
{f : G →+ G'}
(hf : Function.Injective ⇑f)
:
(AddSubgroup.map f H).index = H.index * f.range.index
theorem
Subgroup.index_map_subtype
{G : Type u_1}
[Group G]
{H : Subgroup G}
(K : Subgroup ↥H)
:
(Subgroup.map H.subtype K).index = K.index * H.index
theorem
AddSubgroup.index_map_subtype
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
(K : AddSubgroup ↥H)
:
(AddSubgroup.map H.subtype K).index = K.index * H.index
theorem
AddSubgroup.relindex_eq_zero_of_le_left
{G : Type u_1}
[AddGroup G]
{H K L : AddSubgroup G}
(hHK : H ≤ K)
(hKL : K.relindex L = 0)
:
H.relindex L = 0
theorem
AddSubgroup.relindex_eq_zero_of_le_right
{G : Type u_1}
[AddGroup G]
{H K L : AddSubgroup G}
(hKL : K ≤ L)
(hHK : H.relindex K = 0)
:
H.relindex L = 0
theorem
AddSubgroup.index_eq_zero_of_relindex_eq_zero
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(h : H.relindex K = 0)
:
H.index = 0
theorem
AddSubgroup.relindex_le_of_le_left
{G : Type u_1}
[AddGroup G]
{H K L : AddSubgroup G}
(hHK : H ≤ K)
(hHL : H.relindex L ≠ 0)
:
K.relindex L ≤ H.relindex L
theorem
AddSubgroup.relindex_le_of_le_right
{G : Type u_1}
[AddGroup G]
{H K L : AddSubgroup G}
(hKL : K ≤ L)
(hHL : H.relindex L ≠ 0)
:
H.relindex K ≤ H.relindex L
theorem
AddSubgroup.relindex_ne_zero_trans
{G : Type u_1}
[AddGroup G]
{H K L : AddSubgroup G}
(hHK : H.relindex K ≠ 0)
(hKL : K.relindex L ≠ 0)
:
H.relindex L ≠ 0
theorem
AddSubgroup.relindex_inf_ne_zero
{G : Type u_1}
[AddGroup G]
{H K L : AddSubgroup G}
(hH : H.relindex L ≠ 0)
(hK : K.relindex L ≠ 0)
:
theorem
AddSubgroup.index_inf_ne_zero
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(hH : H.index ≠ 0)
(hK : K.index ≠ 0)
:
theorem
AddSubgroup.relindex_iInf_ne_zero
{G : Type u_1}
[AddGroup G]
{L : AddSubgroup G}
{ι : Type u_3}
[_hι : Finite ι]
{f : ι → AddSubgroup G}
(hf : ∀ (i : ι), (f i).relindex L ≠ 0)
:
(⨅ (i : ι), f i).relindex L ≠ 0
theorem
AddSubgroup.relindex_iInf_le
{G : Type u_1}
[AddGroup G]
{L : AddSubgroup G}
{ι : Type u_3}
[Fintype ι]
(f : ι → AddSubgroup G)
:
(⨅ (i : ι), f i).relindex L ≤ ∏ i : ι, (f i).relindex L
theorem
AddSubgroup.index_iInf_ne_zero
{G : Type u_1}
[AddGroup G]
{ι : Type u_3}
[Finite ι]
{f : ι → AddSubgroup G}
(hf : ∀ (i : ι), (f i).index ≠ 0)
:
(⨅ (i : ι), f i).index ≠ 0
theorem
AddSubgroup.index_iInf_le
{G : Type u_1}
[AddGroup G]
{ι : Type u_3}
[Fintype ι]
(f : ι → AddSubgroup G)
:
(⨅ (i : ι), f i).index ≤ ∏ i : ι, (f i).index
@[simp]
@[simp]
@[simp]
theorem
AddSubgroup.inf_eq_bot_of_coprime
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(h : (Nat.card ↥H).Coprime (Nat.card ↥K))
:
@[deprecated AddSubgroup.inf_eq_bot_of_coprime]
theorem
add_inf_eq_bot_of_coprime
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(h : (Nat.card ↥H).Coprime (Nat.card ↥K))
:
Alias of AddSubgroup.inf_eq_bot_of_coprime
.
theorem
AddSubgroup.index_ne_zero_of_finite
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
[hH : Finite (G ⧸ H)]
:
H.index ≠ 0
noncomputable def
Subgroup.fintypeOfIndexNeZero
{G : Type u_1}
[Group G]
{H : Subgroup G}
(hH : H.index ≠ 0)
:
Finite index implies finite quotient.
Equations
- Subgroup.fintypeOfIndexNeZero hH = Fintype.ofFinite (G ⧸ H)
Instances For
noncomputable def
AddSubgroup.fintypeOfIndexNeZero
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
(hH : H.index ≠ 0)
:
Finite index implies finite quotient.
Equations
Instances For
theorem
AddSubgroup.one_lt_index_of_ne_top
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
[Finite (G ⧸ H)]
(hH : H ≠ ⊤)
:
1 < H.index
theorem
Subgroup.finite_quotient_of_finite_quotient_of_index_ne_zero
{G : Type u_1}
[Group G]
{H : Subgroup G}
{X : Type u_3}
[MulAction G X]
[Finite (MulAction.orbitRel.Quotient G X)]
(hi : H.index ≠ 0)
:
Finite (MulAction.orbitRel.Quotient (↥H) X)
theorem
AddSubgroup.finite_quotient_of_finite_quotient_of_index_ne_zero
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
{X : Type u_3}
[AddAction G X]
[Finite (AddAction.orbitRel.Quotient G X)]
(hi : H.index ≠ 0)
:
Finite (AddAction.orbitRel.Quotient (↥H) X)
theorem
Subgroup.finite_quotient_of_pretransitive_of_index_ne_zero
{G : Type u_1}
[Group G]
{H : Subgroup G}
{X : Type u_3}
[MulAction G X]
[MulAction.IsPretransitive G X]
(hi : H.index ≠ 0)
:
Finite (MulAction.orbitRel.Quotient (↥H) X)
theorem
AddSubgroup.finite_quotient_of_pretransitive_of_index_ne_zero
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
{X : Type u_3}
[AddAction G X]
[AddAction.IsPretransitive G X]
(hi : H.index ≠ 0)
:
Finite (AddAction.orbitRel.Quotient (↥H) X)
@[simp]
theorem
AddSubgroup.index_sum
{G : Type u_1}
{G' : Type u_2}
[AddGroup G]
[AddGroup G']
(H : AddSubgroup G)
(K : AddSubgroup G')
:
@[simp]
theorem
Subgroup.index_pi
{G : Type u_1}
[Group G]
{ι : Type u_3}
[Fintype ι]
(H : ι → Subgroup G)
:
(Subgroup.pi Set.univ H).index = ∏ i : ι, (H i).index
@[simp]
theorem
AddSubgroup.index_pi
{G : Type u_1}
[AddGroup G]
{ι : Type u_3}
[Fintype ι]
(H : ι → AddSubgroup G)
:
(AddSubgroup.pi Set.univ H).index = ∏ i : ι, (H i).index
@[simp]
theorem
AddSubgroup.index_toSubgroup
{G : Type u_3}
[AddGroup G]
(H : AddSubgroup G)
:
(AddSubgroup.toSubgroup H).index = H.index
@[simp]
theorem
AddSubgroup.relindex_toSubgroup
{G : Type u_3}
[AddGroup G]
(H K : AddSubgroup G)
:
(AddSubgroup.toSubgroup H).relindex (AddSubgroup.toSubgroup K) = H.relindex K
Typeclass for finite index subgroups.
- finiteIndex : H.index ≠ 0
The additive subgroup has finite index
Instances
noncomputable def
Subgroup.fintypeQuotientOfFiniteIndex
{G : Type u_1}
[Group G]
(H : Subgroup G)
[H.FiniteIndex]
:
A finite index subgroup has finite quotient.
Equations
- H.fintypeQuotientOfFiniteIndex = Subgroup.fintypeOfIndexNeZero ⋯
Instances For
noncomputable def
AddSubgroup.fintypeQuotientOfFiniteIndex
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[H.FiniteIndex]
:
A finite index subgroup has finite quotient
Equations
- H.fintypeQuotientOfFiniteIndex = AddSubgroup.fintypeOfIndexNeZero ⋯
Instances For
instance
AddSubgroup.finite_quotient_of_finiteIndex
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[H.FiniteIndex]
:
theorem
AddSubgroup.finiteIndex_of_finite_quotient
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Finite (G ⧸ H)]
:
H.FiniteIndex
@[instance 100]
instance
AddSubgroup.finiteIndex_of_finite
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Finite G]
:
H.FiniteIndex
instance
AddSubgroup.instFiniteIndexMin
{G : Type u_1}
[AddGroup G]
(H K : AddSubgroup G)
[H.FiniteIndex]
[K.FiniteIndex]
:
(H ⊓ K).FiniteIndex
theorem
AddSubgroup.finiteIndex_iInf
{G : Type u_1}
[AddGroup G]
{ι : Type u_3}
[Finite ι]
{f : ι → AddSubgroup G}
(hf : ∀ (i : ι), (f i).FiniteIndex)
:
(⨅ (i : ι), f i).FiniteIndex
theorem
AddSubgroup.finiteIndex_iInf'
{G : Type u_1}
[AddGroup G]
{ι : Type u_3}
{s : Finset ι}
(f : ι → AddSubgroup G)
(hs : ∀ i ∈ s, (f i).FiniteIndex)
:
(⨅ i ∈ s, f i).FiniteIndex
instance
Subgroup.instFiniteIndex_subgroupOf
{G : Type u_1}
[Group G]
(H K : Subgroup G)
[H.FiniteIndex]
:
(H.subgroupOf K).FiniteIndex
instance
AddSubgroup.instFiniteIndex_addSubgroupOf
{G : Type u_1}
[AddGroup G]
(H K : AddSubgroup G)
[H.FiniteIndex]
:
(H.addSubgroupOf K).FiniteIndex
theorem
AddSubgroup.finiteIndex_of_le
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
[H.FiniteIndex]
(h : H ≤ K)
:
K.FiniteIndex
theorem
AddSubgroup.index_antitone
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(h : H ≤ K)
[H.FiniteIndex]
:
K.index ≤ H.index
theorem
AddSubgroup.index_strictAnti
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(h : H < K)
[H.FiniteIndex]
:
K.index < H.index
instance
Subgroup.finiteIndex_normalCore
{G : Type u_1}
[Group G]
(H : Subgroup G)
[H.FiniteIndex]
:
H.normalCore.FiniteIndex
instance
Subgroup.finiteIndex_center
(G : Type u_1)
[Group G]
[Finite ↑(commutatorSet G)]
[Group.FG G]
:
(Subgroup.center G).FiniteIndex
theorem
Subgroup.index_center_le_pow
(G : Type u_1)
[Group G]
[Finite ↑(commutatorSet G)]
[Group.FG G]
:
(Subgroup.center G).index ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G
theorem
MulAction.index_stabilizer
(G : Type u_1)
{X : Type u_2}
[Group G]
[MulAction G X]
(x : X)
:
(MulAction.stabilizer G x).index = (MulAction.orbit G x).ncard
theorem
MulAction.index_stabilizer_of_transitive
(G : Type u_1)
{X : Type u_2}
[Group G]
[MulAction G X]
(x : X)
[MulAction.IsPretransitive G X]
:
(MulAction.stabilizer G x).index = Nat.card X
theorem
MonoidHom.card_fiber_eq_of_mem_range
{G : Type u_1}
{M : Type u_2}
{F : Type u_3}
[Group G]
[Fintype G]
[Monoid M]
[DecidableEq M]
[FunLike F G M]
[MonoidHomClass F G M]
(f : F)
{x y : M}
(hx : x ∈ Set.range ⇑f)
(hy : y ∈ Set.range ⇑f)
:
(Finset.filter (fun (g : G) => f g = x) Finset.univ).card = (Finset.filter (fun (g : G) => f g = y) Finset.univ).card
theorem
AddMonoidHom.card_fiber_eq_of_mem_range
{G : Type u_1}
{M : Type u_2}
{F : Type u_3}
[AddGroup G]
[Fintype G]
[AddMonoid M]
[DecidableEq M]
[FunLike F G M]
[AddMonoidHomClass F G M]
(f : F)
{x y : M}
(hx : x ∈ Set.range ⇑f)
(hy : y ∈ Set.range ⇑f)
:
(Finset.filter (fun (g : G) => f g = x) Finset.univ).card = (Finset.filter (fun (g : G) => f g = y) Finset.univ).card