Mathlib.GroupTheory.Rank

Group.rank definition

[h : FG G] : ℕ

Full source

/-- The minimum number of generators of a group. -/
@[to_additive "The minimum number of generators of an additive group."]
noncomputable def rank [h : FG G] : ℕ := @Nat.find _ (Classical.decPred _) (fg_iff'.mp h)

Rank of a finitely generated group

Informal description

For a finitely generated group $ G $, the rank of $ G $ is the minimal cardinality of a generating set $ S $ of $ G $, i.e., the smallest natural number $ n $ such that there exists a subset $ S \subseteq G $ with $ |S| = n $ and the subgroup generated by $ S $ is $ G $ itself.

Group.rank_spec theorem

[h : FG G] : ∃ S : Finset G, S.card = rank G ∧ .closure S = (⊤ : Subgroup G)

Full source

@[to_additive]
lemma rank_spec [h : FG G] : ∃ S : Finset G, S.card = rank G ∧ .closure S = (⊤ : Subgroup G) :=
  @Nat.find_spec _ (Classical.decPred _) (fg_iff'.mp h)

Existence of Minimal Generating Set for Finitely Generated Groups

Informal description

For any finitely generated group $G$, there exists a finite subset $S \subseteq G$ such that the cardinality of $S$ equals the rank of $G$ and the subgroup generated by $S$ is $G$ itself.

Group.rank_le theorem

[h : FG G] {S : Finset G} (hS : .closure S = (⊤ : Subgroup G)) : rank G ≤ S.card

Full source

@[to_additive]
lemma rank_le [h : FG G] {S : Finset G} (hS : .closure S = (⊤ : Subgroup G)) : rank G ≤ S.card :=
  @Nat.find_le _ _ (Classical.decPred _) (fg_iff'.mp h) ⟨S, rfl, hS⟩

Rank Bound by Generating Set Cardinality in Finitely Generated Groups

Informal description

For any finitely generated group $G$ and any finite subset $S \subseteq G$ that generates $G$ (i.e., $\langle S \rangle = G$), the rank of $G$ is less than or equal to the cardinality of $S$.

Group.rank_le_of_surjective theorem

[FG G] [FG H] (f : G →* H) (hf : Surjective f) : rank H ≤ rank G

Full source

@[to_additive]
lemma rank_le_of_surjective [FG G] [FG H] (f : G →* H) (hf : Surjective f) : rank H ≤ rank G := by
  classical
  obtain ⟨S, hS1, hS2⟩ := rank_spec G
  trans (S.image f).card
  · apply rank_le
    rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
  · exact Finset.card_image_le.trans_eq hS1

Rank Inequality for Surjective Group Homomorphisms

Informal description

Let $G$ and $H$ be finitely generated groups, and let $f: G \to H$ be a surjective group homomorphism. Then the rank of $H$ is less than or equal to the rank of $G$.

Group.rank_range_le theorem

[FG G] {f : G →* H} : rank f.range ≤ rank G

Full source

@[to_additive]
lemma rank_range_le [FG G] {f : G →* H} : rank f.range ≤ rank G :=
  rank_le_of_surjective f.rangeRestrict f.rangeRestrict_surjective

Rank Inequality for Group Homomorphism Range: $\text{rank}(f(G)) \leq \text{rank}(G)$

Informal description

For any finitely generated group $G$ and group homomorphism $f \colon G \to H$, the rank of the range of $f$ is less than or equal to the rank of $G$, i.e., $\text{rank}(f(G)) \leq \text{rank}(G)$.

Group.rank_congr theorem

[FG G] [FG H] (e : G ≃* H) : rank G = rank H

Full source

@[to_additive]
lemma rank_congr [FG G] [FG H] (e : G ≃* H) : rank G = rank H :=
  le_antisymm (rank_le_of_surjective e.symm e.symm.surjective)
    (rank_le_of_surjective e e.surjective)

Rank Preservation under Group Isomorphism: $\text{rank}(G) = \text{rank}(H)$ for $G \cong H$

Informal description

For any finitely generated groups $G$ and $H$, if there exists a group isomorphism $e: G \cong H$, then the ranks of $G$ and $H$ are equal, i.e., $\text{rank}(G) = \text{rank}(H)$.

Subgroup.rank_congr theorem

{H K : Subgroup G} [Group.FG H] [Group.FG K] (h : H = K) : rank H = rank K

Full source

@[to_additive]
lemma rank_congr {H K : Subgroup G} [Group.FG H] [Group.FG K] (h : H = K) : rank H = rank K := by
  subst h; rfl

Rank Equality for Equal Finitely Generated Subgroups

Informal description

Let $G$ be a group with finitely generated subgroups $H$ and $K$. If $H = K$, then the ranks of $H$ and $K$ are equal, i.e., $\text{rank}(H) = \text{rank}(K)$.

Subgroup.rank_closure_finset_le_card theorem

(s : Finset G) : rank (closure (s : Set G)) ≤ s.card

Full source

@[to_additive]
lemma rank_closure_finset_le_card (s : Finset G) : rank (closure (s : Set G)) ≤ s.card := by
  classical
  let t : Finset (closure (s : Set G)) := s.preimage Subtype.val Subtype.coe_injective.injOn
  have ht : closure (t : Set (closure (s : Set G))) = ⊤ := by
    rw [Finset.coe_preimage]
    exact closure_preimage_eq_top (s : Set G)
  apply (rank_le ht).trans
  suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G))) by
    rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
    apply Finset.card_filter_le
  apply Subtype.coe_injective.injOn

Rank Bound for Subgroup Generated by Finite Set: $\text{rank}(\langle s \rangle) \leq |s|$

Informal description

For any finite subset $s$ of a group $G$, the rank of the subgroup generated by $s$ is less than or equal to the cardinality of $s$, i.e., $\text{rank}(\langle s \rangle) \leq |s|$.

Subgroup.rank_closure_finite_le_nat_card theorem

(s : Set G) [Finite s] : rank (closure s) ≤ Nat.card s

Full source

@[to_additive]
lemma rank_closure_finite_le_nat_card (s : Set G) [Finite s] : rank (closure s) ≤ Nat.card s := by
  haveI := Fintype.ofFinite s
  rw [Nat.card_eq_fintype_card, ← s.toFinset_card, ← rank_congr (congr_arg _ s.coe_toFinset)]
  exact rank_closure_finset_le_card s.toFinset

Rank Bound for Subgroup Generated by Finite Set: $\text{rank}(\langle s \rangle) \leq |s|$

Informal description

For any finite subset $s$ of a group $G$, the rank of the subgroup generated by $s$ is less than or equal to the cardinality of $s$, i.e., $\text{rank}(\langle s \rangle) \leq |s|$.

Subgroup.nat_card_centralizer_nat_card_stabilizer theorem

(g : G) : Nat.card (centralizer { g }) = Nat.card (MulAction.stabilizer (ConjAct G) g)

Full source

lemma nat_card_centralizer_nat_card_stabilizer (g : G) :
    Nat.card (centralizer {g}) = Nat.card (MulAction.stabilizer (ConjAct G) g) := by
  rw [centralizer_eq_comap_stabilizer];   rfl

Cardinality Equality between Centralizer and Stabilizer under Conjugation Action

Informal description

For any element $g$ in a group $G$, the cardinality of the centralizer of $\{g\}$ in $G$ is equal to the cardinality of the stabilizer subgroup of $g$ under the conjugation action of $G$ on itself. That is, \[ \text{card}(\text{centralizer}(\{g\})) = \text{card}(\text{stabilizer}(\text{ConjAct}\, G, g)). \]

TODO