Documentation

Mathlib.GroupTheory.Rank

Rank of a group #

This file defines the rank of a group, namely the minimum size of a generating set.

TODO #

Should we define erank G : ℕ∞ the rank of a not necessarily finitely generated group G, then redefine rank G as (erank G).toNat? Maybe a Cardinal-valued version too?

source
noncomputable def Group.rank (G : Type u_1) [Group G] [h : FG G] :
ℕ

The minimum number of generators of a group.

Instances For
    source
    noncomputable def AddGroup.rank (G : Type u_1) [AddGroup G] [h : FG G] :
    ℕ

    The minimum number of generators of an additive group.

    Instances For
      source
      theorem Group.rank_spec (G : Type u_1) [Group G] [h : FG G] :
      ∃ (S : Finset G), S.card = rank G ∧ Subgroup.closure ↑S = ⊤
      source
      theorem AddGroup.rank_spec (G : Type u_1) [AddGroup G] [h : FG G] :
      ∃ (S : Finset G), S.card = rank G ∧ AddSubgroup.closure ↑S = ⊤
      source
      theorem Group.rank_le {G : Type u_1} [Group G] [h : FG G] {S : Finset G} (hS : Subgroup.closure ↑S = ⊤) :
      rank G ≤ S.card
      source
      theorem AddGroup.rank_le {G : Type u_1} [AddGroup G] [h : FG G] {S : Finset G} (hS : AddSubgroup.closure ↑S = ⊤) :
      rank G ≤ S.card
      source
      theorem Group.rank_eq_zero (G : Type u_1) [Group G] [Subsingleton G] :
      rank G = 0
      source
      theorem AddGroup.rank_eq_zero (G : Type u_1) [AddGroup G] [Subsingleton G] :
      rank G = 0
      source
      theorem Group.rank_eq_zero_iff {G : Type u_1} [Group G] [FG G] :
      rank G = 0 ↔ Subsingleton G
      source
      theorem AddGroup.rank_eq_zero_iff {G : Type u_1} [AddGroup G] [FG G] :
      rank G = 0 ↔ Subsingleton G
      source
      theorem Group.rank_pos (G : Type u_1) [Group G] [Nontrivial G] [FG G] :
      0 < rank G
      source
      theorem AddGroup.rank_pos (G : Type u_1) [AddGroup G] [Nontrivial G] [FG G] :
      0 < rank G
      source
      theorem Group.rank_le_of_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] [FG G] [FG H] (f : G →* H) (hf : Function.Surjective ⇑f) :
      rank H ≤ rank G
      source
      theorem AddGroup.rank_le_of_surjective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [FG G] [FG H] (f : G →+ H) (hf : Function.Surjective ⇑f) :
      rank H ≤ rank G
      source
      theorem Group.rank_range_le {G : Type u_1} {H : Type u_2} [Group G] [Group H] [FG G] {f : G →* H} :
      rank ↥f.range ≤ rank G
      source
      theorem AddGroup.rank_range_le {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [FG G] {f : G →+ H} :
      rank ↥f.range ≤ rank G
      source
      theorem Group.rank_congr {G : Type u_1} {H : Type u_2} [Group G] [Group H] [FG G] [FG H] (e : G ≃* H) :
      rank G = rank H
      source
      theorem AddGroup.rank_congr {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [FG G] [FG H] (e : G ≃+ H) :
      rank G = rank H
      source
      theorem Subgroup.rank_congr {G : Type u_1} [Group G] {H K : Subgroup G} [Group.FG ↥H] [Group.FG ↥K] (h : H = K) :
      Group.rank ↥H = Group.rank ↥K
      source
      theorem AddSubgroup.rank_congr {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [AddGroup.FG ↥H] [AddGroup.FG ↥K] (h : H = K) :
      AddGroup.rank ↥H = AddGroup.rank ↥K
      source
      theorem Subgroup.rank_closure_finset_le_card {G : Type u_1} [Group G] (s : Finset G) :
      Group.rank ↥(closure ↑s) ≤ s.card
      source
      theorem AddSubgroup.rank_closure_finset_le_card {G : Type u_1} [AddGroup G] (s : Finset G) :
      AddGroup.rank ↥(closure ↑s) ≤ s.card
      source
      theorem Subgroup.rank_closure_finite_le_nat_card {G : Type u_1} [Group G] (s : Set G) [Finite ↑s] :
      Group.rank ↥(closure s) ≤ Nat.card ↑s
      source
      theorem AddSubgroup.rank_closure_finite_le_nat_card {G : Type u_1} [AddGroup G] (s : Set G) [Finite ↑s] :
      AddGroup.rank ↥(closure s) ≤ Nat.card ↑s
      source
      theorem Subgroup.nat_card_centralizer_nat_card_stabilizer {G : Type u_1} [Group G] (g : G) :
      Nat.card ↥(centralizer {g}) = Nat.card ↥(MulAction.stabilizer (ConjAct G) g)