finite subgroup of group iso to Fˣ lies within finite field

Stream: maths

[Alex Brodbelt]

Hi!

Potentially #xy, so overall result I need to prove that a finite subgroup of a group isomorphic to the units of a field has cardinality dividing $p^n - 1$ and hence coprime to $p$ (where $p$ is the characteristic of the field, so prime).

Maths question/would like to know if this is sensible or if there is an easier proof:
My reasoning so far is that, if $A_0 < D$ and $D \cong F^\times$. I know every element of $A_0$ is algebraic as every element satisfies $x^{|A_0|} - 1 = 0$. And taking $\mathbb{F}_p = \langle 1 \rangle_+$ and the extending the field by every element is finite as it is algebraic(? I believe this is true, but my basic galois theory knowledge is not too deep yet)*so $\mathbb{F}_p (x_1, \ldots , x_{A_0})$ is finite (by induction) and hence of order $p^n$ and given it the group lies within the gorup of units of this field, $A_0$ has order dividing $p^n -1$.

Have not used it in the proof but could be useful, I have formalized $A_0$ is cyclic.

*I believe this is true as the elements in $\mathbb{F}_p (x_1)$ are of the form $a_0 + a_1 x_1 + ... + a_{|A_0| -1} x_1 ^{|A_0| - 1}$ and so is finite as has order at most $p^{A_0}$.

Lean question:
How do I relate a finite subgroup which is initially not related to a field (it is related to field after an isomorphism MulEquiv between the group it is contained in and the units of the field) to a finite field.
These are the current relationships between subgroups and groups: $A \leq c \cdot D \sqcap G$ (acting by conjugation) $c \cdot D \cong F^\times$ in a chain of homomorphisms:
$A_0 \hookrightarrow c \cdot D \xrightarrow{\sim} D \xrightarrow{\sim} F^\times$

If more context is useful:

• $D$ is the group of diagonal matrices of $SL(2,F)$.
• $F$ is alg closed field (so infinite).
• $G$ finite subgroup of $SL(2,F)$ which will be eventually classified through the so called maximal abelian class equation.
• $A_0$ finite maximal abelian group which is isomorphic to a finite subgroup of $F^\times$.

Assuming the argument above is correct, how can I translate it to lean in a way which is idiomatic?

Thanks in advance

[Mitchell Lee]

A finite group has order coprime to $p$ (and thus, its order divides a number of the form $p^n - 1$ with $n > 0$) if and only if it has no element of order $p$. This is Cauchy's theorem: https://en.m.wikipedia.org/wiki/Cauchy%27s_theorem_(group_theory)

[Alex Brodbelt]

Hmm so I show there is no element of order $p$, seems plausible. I don't follow why the order has to divide $p^n - 1$ though (I suppose this part of the result is not strictly necessary, but I am curious to know why it follows without using the argument I use).

[Edward van de Meent]

overall result I need to prove that a finite subgroup of a group isomorphic to the units of a field has cardinality dividing $p^n−1$ and hence coprime to p (where p is the characteristic of the field, so prime).

surely this is just "since $F$ is a finite field, it has cardinality $p ^ n$ for some prime $p$ and natural $n$. Then, $F^\times$ has size $p ^ n - 1$ by definition. finally, the size of a subgroup divides the size of the ambient group"?

[Alex Brodbelt]

$F$ is not a finite field, it is infinite as it is algebraically closed.

[Edward van de Meent]

ah, i missed that bit

[Johan Commelin]

Alex Brodbelt said:

Have not used it in the proof but could be useful, I have formalized $A_0$ is cyclic.

This is already in mathlib, I'm quite sure.

[Alex Brodbelt]

Indeed, I used the mathlib to formalize this result. I contructed the monoid homomorphism and then used docs#isCyclic_of_subgroup_isDomain (lol don't know how to link to mathlib theorem)
:lol:

[Michael Stoll]

docs#isCyclic_of_subgroup_isDomain

[Alex Brodbelt]

Aha yes, thank you

[Mitchell Lee]

1. A field of characteristic $p$ cannot have any element of multiplicative order $p$. Assume for the sake of contradiction that $x$ is such an element. Then $(x - 1)^p = x^p - 1 = 0$ (see https://en.m.wikipedia.org/wiki/Frobenius_endomorphism), so $x = 1$, which is a contradiction.
2. If an integer $m$ is coprime to $p$, then $m$ divides $p^n - 1$ for some $n$. This follows fron Euler's totient theorem: https://en.m.wikipedia.org/wiki/Euler%27s_theorem

[Alex Brodbelt]

Mitchell Lee said:

A finite group has order coprime to $p$ (and thus, its order divides a number of the form $p^n - 1$ with $n > 0$) if and only if it has no element of order $p$. This is Cauchy's theorem: https://en.m.wikipedia.org/wiki/Cauchy%27s_theorem_(group_theory)

1. Makes sense!
2. Ah yes, of course! silly me.

Thank you @Mitchell Lee ! Much simpler than my approach, I will try formalize this.

[Alex Brodbelt]

1.

import Mathlib

lemma order_ne_char (F : Type*) [Field F] {p : ℕ} [hp' : Fact (Nat.Prime p)] [hC : CharP F p]
  (x : Fˣ) :
  orderOf x ≠ p := by
  intro order_eq_p
  have x_pow_p_eq_one : x^p = 1 := by rw [← order_eq_p, pow_orderOf_eq_one x]
  have x_pow_p_eq_one' : (x : F)^p = 1 := by
    simp [Units.ext_iff] at x_pow_p_eq_one
    exact x_pow_p_eq_one
  suffices frobenius F p (x - 1) = 0 by
    rw [← frobenius_zero F p] at this
    apply frobenius_inj at this
    rw [sub_eq_zero] at this
    simp at this
    rw [← orderOf_eq_one_iff] at this
    rw [this] at order_eq_p
    have hp : Nat.Prime p := hp'.out
    have p_ne_one : 1 ≠ p := (Nat.Prime.ne_one hp).symm
    contradiction
  dsimp [frobenius]
  rw [sub_eq_add_neg, add_pow_char_of_commute (h := Commute.neg_one_right _),
    x_pow_p_eq_one', ExpChar.neg_one_pow_expChar, add_neg_cancel]

[Riccardo Brasca]

You can golf it a little.

import Mathlib

lemma order_ne_char (F : Type*) [Field F] {p : ℕ} [hp' : Fact (Nat.Prime p)] [hC : CharP F p]
  (x : Fˣ) : orderOf x ≠ p := by
  intro h
  suffices (x : F) ≠ 1 by
    apply Function.Injective.ne (frobenius_inj F p) this
    simp only [frobenius, RingHom.coe_mk, powMonoidHom_apply, one_pow, ← Units.val_pow_eq_pow_val]
    have := pow_orderOf_eq_one x
    rw [h] at this
    rw [this, Units.val_one]
  intro H
  rw [Units.val_eq_one] at H
  rw [H, orderOf_one] at h
  exact hp'.out.ne_one h.symm

[Riccardo Brasca]

(It can surely be golfed even more, but who cares)

[Filippo A. E. Nuccio]

For example like this

import Mathlib

lemma order_ne_char (F : Type*) [Field F] {p : ℕ} [hp' : Fact (Nat.Prime p)] [hC : CharP F p]
  (x : Fˣ) : orderOf x ≠ p := by
  by_contra H
  have := ExpChar.pow_prime_pow_mul_eq_one_iff p 1 1 (x : F)
  simp only [← H, pow_one, mul_one, ← Units.val_pow_eq_pow_val, pow_orderOf_eq_one x, Units.val_one,
    Units.val_eq_one, true_iff] at this
  exact hp'.out.ne_one (@orderOf_one Fˣ _ ▸ (this ▸ H)).symm

(not that I care, but had to kill some time :golf: )

[Alex Brodbelt]

always love a :golf:

[Antoine Chambert-Loir]

Why not prove that orderOf x is not divisible by p?

[Antoine Chambert-Loir]

(OK, if x has infinite order, then orderOf x is zero…)

[Alex Brodbelt]

2. this one could be simpler but given its over MOD rather than ZMOD I don't have access to docs#sub_eq_zero

import Mathlib

lemma dvd_pow_totient_sub_one_of_coprime {m p : ℕ} (hp : Nat.Prime p) (h : Nat.Coprime m p) :
  m ∣ p^Nat.totient m - 1 := by
  rw [← Nat.modEq_zero_iff_dvd]
  suffices p ^ m.totient ≡ 1 [MOD m] by
    rw [← add_zero (p ^ Nat.totient m), ← Nat.sub_self 1] at this
    nth_rewrite 3 [← zero_add 1] at this
    rw [← Nat.add_sub_assoc (le_refl _), Nat.sub_add_comm (one_le_pow₀ hp.one_le)] at this
    apply Nat.ModEq.add_right_cancel' 1 this
  exact Nat.ModEq.pow_totient h.symm

[Alex Brodbelt]

Overall

import Mathlib

lemma coprime_card_fin_subgroup_of_inj_hom_group_iso_units {F G : Type*} [Field F] {p : ℕ} [hp' : Fact (Nat.Prime p)]
  [hC : CharP F p] [Group G] (H : Subgroup G) [Finite H] (f : G →* Fˣ) (hf : Injective f) :
    Nat.Coprime (Nat.card H) p := by
  rw [Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd hp'.out]
  have order_ne_p := @order_ne_char F _ p _ _
  contrapose! order_ne_p
  let H_fintype : Fintype H := Fintype.ofFinite ↥H
  simp only [Nat.card_eq_fintype_card] at order_ne_p
  obtain ⟨h, hh⟩ := @exists_prime_orderOf_dvd_card H _ _ p _ order_ne_p
  use f h
  rw [orderOf_injective f hf ↑h, ← hh, orderOf_submonoid]

Thank you Mitchell for the nice argument and everyone else for helping out :)