mathlib documentation

group_theory.index

Index of a Subgroup #

In this file we define the index of a subgroup, and prove several divisibility properties.

Main definitions #

Main results #

source
def subgroup.index {G : Type u_1} [group G] (H : subgroup G) :
ℕ

The index of a subgroup as a natural number, and returns 0 if the index is infinite.

Equations
source
def add_subgroup.index {G : Type u_1} [add_group G] (H : add_subgroup G) :
ℕ

The index of a subgroup as a natural number, and returns 0 if the index is infinite.

Equations
source
def subgroup.relindex {G : Type u_1} [group G] (H K : subgroup G) :
ℕ

The relative index of a subgroup as a natural number, and returns 0 if the relative index is infinite.

Equations
source
def add_subgroup.relindex {G : Type u_1} [add_group G] (H K : add_subgroup G) :
ℕ

The relative index of a subgroup as a natural number, and returns 0 if the relative index is infinite.

Equations
source
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
source
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
source
theorem subgroup.index_comap {G : Type u_1} [group G] (H : subgroup G) {G' : Type u_2} [group G'] (f : G' →* G) :
(subgroup.comap f H).index = H.relindex f.range
source
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
source
theorem add_subgroup.relindex_add_index {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H ≤ K) :
(H.relindex K) * K.index = H.index
source
theorem subgroup.relindex_mul_index {G : Type u_1} [group G] {H K : subgroup G} (h : H ≤ K) :
(H.relindex K) * K.index = H.index
source
theorem subgroup.index_dvd_of_le {G : Type u_1} [group G] {H K : subgroup G} (h : H ≤ K) :
K.index ∣ H.index
source
theorem add_subgroup.index_dvd_of_le {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H ≤ K) :
K.index ∣ H.index
source
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
source
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
source
theorem subgroup.relindex_mul_relindex {G : Type u_1} [group G] {H K L : subgroup G} (hHK : H ≤ K) (hKL : K ≤ L) :
(H.relindex K) * K.relindex L = H.relindex L
source
theorem add_subgroup.relindex_add_relindex {G : Type u_1} [add_group G] {H K L : add_subgroup G} (hHK : H ≤ K) (hKL : K ≤ L) :
(H.relindex K) * K.relindex L = H.relindex L
source
@[simp]
theorem add_subgroup.index_top {G : Type u_1} [add_group G] :
⊤.index = 1
source
@[simp]
theorem subgroup.index_top {G : Type u_1} [group G] :
⊤.index = 1
source
@[simp]
theorem subgroup.index_bot {G : Type u_1} [group G] :
⊥.index = nat.card G
source
@[simp]
theorem add_subgroup.index_bot {G : Type u_1} [add_group G] :
⊥.index = nat.card G
source
theorem add_subgroup.index_bot_eq_card {G : Type u_1} [add_group G] [fintype G] :
⊥.index = fintype.card G
source
theorem subgroup.index_bot_eq_card {G : Type u_1} [group G] [fintype G] :
⊥.index = fintype.card G
source
@[simp]
theorem add_subgroup.relindex_top_left {G : Type u_1} [add_group G] (H : add_subgroup G) :
⊤.relindex H = 1
source
@[simp]
theorem subgroup.relindex_top_left {G : Type u_1} [group G] (H : subgroup G) :
⊤.relindex H = 1
source
@[simp]
theorem subgroup.relindex_top_right {G : Type u_1} [group G] (H : subgroup G) :
H.relindex ⊤ = H.index
source
@[simp]
theorem add_subgroup.relindex_top_right {G : Type u_1} [add_group G] (H : add_subgroup G) :
H.relindex ⊤ = H.index
source
@[simp]
theorem add_subgroup.relindex_bot_left {G : Type u_1} [add_group G] (H : add_subgroup G) :
⊥.relindex H = nat.card ↥H
source
@[simp]
theorem subgroup.relindex_bot_left {G : Type u_1} [group G] (H : subgroup G) :
⊥.relindex H = nat.card ↥H
source
theorem subgroup.relindex_bot_left_eq_card {G : Type u_1} [group G] (H : subgroup G) [fintype ↥H] :
⊥.relindex H = fintype.card ↥H
source
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
source
@[simp]
theorem subgroup.relindex_bot_right {G : Type u_1} [group G] (H : subgroup G) :
H.relindex ⊥ = 1
source
@[simp]
theorem add_subgroup.relindex_bot_right {G : Type u_1} [add_group G] (H : add_subgroup G) :
H.relindex ⊥ = 1
source
@[simp]
theorem add_subgroup.relindex_self {G : Type u_1} [add_group G] (H : add_subgroup G) :
H.relindex H = 1
source
@[simp]
theorem subgroup.relindex_self {G : Type u_1} [group G] (H : subgroup G) :
H.relindex H = 1
source
theorem subgroup.index_eq_card {G : Type u_1} [group G] (H : subgroup G) [fintype (quotient_group.quotient H)] :
H.index = fintype.card (quotient_group.quotient H)
source
theorem add_subgroup.index_eq_card {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype (quotient_add_group.quotient H)] :
H.index = fintype.card (quotient_add_group.quotient H)
source
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
source
theorem add_subgroup.index_add_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
source
theorem subgroup.index_dvd_card {G : Type u_1} [group G] (H : subgroup G) [fintype G] :
H.index ∣ fintype.card G
source
theorem add_subgroup.index_dvd_card {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype G] :
H.index ∣ fintype.card G