English
If p is the smallest prime dividing the order of G and P is a cyclic Sylow p-subgroup, then N_G(P) ≤ C_G(P).
Русский
Пусть p — наименьшая простая, делящая порядок G, и P — циклическая Sylow-p-подгруппа. Тогда N_G(P) ≤ C_G(P).
LaTeX
$$P.normalizer \le P.centralizer$$
Lean4
theorem normalizer_le_centralizer (hP : IsCyclic P) : P.normalizer ≤ centralizer (P : Set G) :=
by
subst hp
by_cases hn : Nat.card G = 1
· have := (Nat.card_eq_one_iff_unique.mp hn).1
rw [Subsingleton.elim P.normalizer (centralizer P)]
have := Fact.mk (Nat.minFac_prime hn)
have key := card_dvd_of_injective _ (QuotientGroup.kerLift_injective P.normalizerMonoidHom)
rw [normalizerMonoidHom_ker, ← index, ← relIndex] at key
refine relIndex_eq_one.mp (Nat.eq_one_of_dvd_coprimes ?_ dvd_rfl key)
obtain ⟨k, hk⟩ := P.2.exists_card_eq
rcases eq_zero_or_pos k with h0 | h0
· rw [hP.card_mulAut, hk, h0, pow_zero, Nat.totient_one]
apply Nat.coprime_one_right
rw [hP.card_mulAut, hk, Nat.totient_prime_pow Fact.out h0]
refine (Nat.Coprime.pow_right _ ?_).mul_right ?_
· apply Nat.Coprime.coprime_dvd_left (relIndex_dvd_of_le_left P.normalizer P.le_centralizer)
apply Nat.Coprime.coprime_dvd_left (relIndex_dvd_index_of_le P.le_normalizer)
rw [Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd Fact.out]
exact P.not_dvd_index
· apply Nat.Coprime.coprime_dvd_left (relIndex_dvd_card (centralizer P) P.normalizer)
apply Nat.Coprime.coprime_dvd_left (card_subgroup_dvd_card P.normalizer)
have h1 := Nat.gcd_dvd_left (Nat.card G) ((Nat.card G).minFac - 1)
have h2 :=
Nat.gcd_le_right (n := (Nat.card G).minFac - 1) (Nat.card G) (tsub_pos_iff_lt.mpr (Nat.minFac_prime hn).one_lt)
contrapose! h2
refine Nat.sub_one_lt_of_le (Nat.card G).minFac_pos (Nat.minFac_le_of_dvd ?_ h1)
exact (Nat.two_le_iff _).mpr ⟨ne_zero_of_dvd_ne_zero Nat.card_pos.ne' h1, h2⟩
