card_commutator_dvd_index_center_pow

English

If the commutator set is finite, then the commutator subgroup has size dividing an explicit bound depending on the center and the commutator set.

Русский

Если множество коммутаторов конечное, то покрывающая граница для размера коммутаторной подгруппы зависит от центра и множества коммутаторов.

LaTeX

$$Nat.card(commutator G) ∣ (center G).index ^ ((center G).index · Nat.card(commutatorSet G) + 1)$$

Lean4

/-- If `G` has `n` commutators `[g₁, g₂]`, then `|G'| ∣ [G : Z(G)] ^ ([G : Z(G)] * n + 1)`,
where `G'` denotes the commutator of `G`. -/
theorem card_commutator_dvd_index_center_pow [Finite (commutatorSet G)] :
    Nat.card (_root_.commutator G) ∣ (center G).index ^ ((center G).index * Nat.card (commutatorSet G) + 1) := by
  -- First handle the case when `Z(G)` has infinite index and `[G : Z(G)]` is defined to be `0`

  by_cases hG : (center G).index = 0
  · simp_rw [hG, zero_mul, zero_add, pow_one, dvd_zero]
  haveI : FiniteIndex (center G) :=
    ⟨hG⟩
      -- Rewrite as `|Z(G) ∩ G'| * [G' : Z(G) ∩ G'] ∣ [G : Z(G)] ^ ([G : Z(G)] * n) * [G : Z(G)]`

  rw [← ((center G).subgroupOf (_root_.commutator G)).card_mul_index, pow_succ]
    -- We have `h1 : [G' : Z(G) ∩ G'] ∣ [G : Z(G)]`

  have h1 :=
    relIndex_dvd_index_of_normal (center G)
      (_root_.commutator G)
        -- So we can reduce to proving `|Z(G) ∩ G'| ∣ [G : Z(G)] ^ ([G : Z(G)] * n)`

  refine mul_dvd_mul ?_ h1
  haveI : FiniteIndex ((center G).subgroupOf (_root_.commutator G)) :=
    ⟨ne_zero_of_dvd_ne_zero hG h1⟩
      -- We have `h2 : rank (Z(G) ∩ G') ≤ [G' : Z(G) ∩ G'] * rank G'` by Schreier's lemma

  have h2 :=
    rank_le_index_mul_rank
      ((center G).subgroupOf (_root_.commutator G))
        -- We have `h3 : [G' : Z(G) ∩ G'] * rank G' ≤ [G : Z(G)] * n` by `h1` and `rank G' ≤ n`

  have h3 :=
    Nat.mul_le_mul (Nat.le_of_dvd (Nat.pos_of_ne_zero hG) h1)
      (rank_commutator_le_card G)
        -- So we can reduce to proving `|Z(G) ∩ G'| ∣ [G : Z(G)] ^ rank (Z(G) ∩ G')`

  refine
    dvd_trans ?_
      (pow_dvd_pow (center G).index (h2.trans h3))
        -- `Z(G) ∩ G'` is abelian, so it enough to prove that `g ^ [G : Z(G)] = 1` for `g ∈ Z(G) ∩ G'`

  apply card_dvd_exponent_pow_rank'
  intro g
  have :=
    Abelianization.commutator_subset_ker (MonoidHom.transferCenterPow G)
      g.1.2
        -- `transfer g` is defeq to `g ^ [G : Z(G)]`, so we are done

  simpa only [MonoidHom.mem_ker, Subtype.ext_iff] using this

Похожие утверждения