nilpotencyClass_quotient_center — Mathlib

English

Quotienting G by its center decreases the nilpotency class by 1 (unless the class is 0, in which case both sides are 0).

Русский

Свёртка группы по её центру уменьшает класс нильпотентности на 1 (если класс 0, то оба равны 0).

LaTeX

$$$\\operatorname{nilpotencyClass}(G/Z(G)) = \\operatorname{nilpotencyClass}(G) - 1$$$

Lean4

/-- Quotienting the `center G` reduces the nilpotency class by 1 -/
theorem nilpotencyClass_quotient_center [hH : IsNilpotent G] :
    Group.nilpotencyClass (G ⧸ center G) = Group.nilpotencyClass G - 1 :=
  by
  generalize hn : Group.nilpotencyClass G = n
  rcases n with (rfl | n)
  · simp only [nilpotencyClass_zero_iff_subsingleton, zero_tsub] at *
    exact Quotient.instSubsingletonQuotient (leftRel (center G))
  · suffices Group.nilpotencyClass (G ⧸ center G) = n by simpa
    apply le_antisymm
    · apply upperCentralSeries_eq_top_iff_nilpotencyClass_le.mp
      apply comap_injective (f := (mk' (center G))) Quot.mk_surjective
      rw [comap_upperCentralSeries_quotient_center, comap_top, Nat.succ_eq_add_one, ← hn]
      exact upperCentralSeries_nilpotencyClass
    · apply le_of_add_le_add_right
      calc
        n + 1 = Group.nilpotencyClass G := hn.symm
        _ ≤ Group.nilpotencyClass (G ⧸ center G) + 1 := nilpotencyClass_le_of_ker_le_center _ (le_of_eq (ker_mk' _)) _

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