cast_subgroup_of_units_card_ne_zero for infinite fields

Stream: maths

[Bolton Bailey]

I have this theorem in recent PR for finite fields K

theorem cast_subgroup_of_units_card_ne_zero [DecidableEq K]
    (G : Subgroup (Units (K))) [Fintype G] : (Fintype.card G : K) ≠ 0 := by

Does anyone know if it's also true of infinite fields as well?

[Damiano Testa]

Isn't the additive span of G also closed under multiplication? If so, then it is a finite subfield and your previous result should apply.

[Kevin Buzzard]

This is true for infinite fields. If G is a finite subgroup of K^* and |G|=0 in K then K must have char p for some prime and G must have an element of order p, but x^p=1 implies (x-1)^p=0 and hence x=1, meaning x didn't have order p after all, contradiction.

[Richard Copley]

This was a good exercise.

import Mathlib.GroupTheory.Perm.Cycle.Type
import Mathlib.Algebra.CharP.Algebra

theorem cast_subgroup_of_units_card_ne_zero' {F : Type u} [Field F]
  (G : Subgroup (Units (F))) (h : Fintype G)
: (Fintype.card G : F) ≠ 0 := by
  let n := Fintype.card G
  have npos : 0 < n := Fintype.card_pos
  intro nzero
  have ⟨p, char_p⟩ := CharP.exists F
  have hd : p ∣ n := (CharP.cast_eq_zero_iff F p n).mp nzero
  cases CharP.char_is_prime_or_zero F p with
  | inr pzero =>
    apply ne_zero_of_lt npos
    apply Nat.eq_zero_of_zero_dvd
    exact pzero ▸ hd
  | inl pprime =>
    have fact_pprime := Fact.mk pprime
    -- G has an element x of order p by Cauchy's theorem
    have ⟨x, hx⟩ := exists_prime_orderOf_dvd_card p hd
    -- F has an element u (= ↑↑x) of order p
    let u := ((x : Fˣ) : F)
    have hu : orderOf u = p := by rwa [orderOf_units, orderOf_subgroup]
    -- u ^ p = 1 implies (u - 1) ^ p = 0
    have h₁ : (u - 1) ^ p = 0 := by
      rewrite [sub_pow_char (R := F) (p := p) u 1]
      rewrite [one_pow]
      rewrite [← hu, pow_orderOf_eq_one]
      exact sub_self 1
    -- ... and hence u = 1 ...
    have h₂ : u = 1 := by
      rewrite [← sub_left_inj, sub_self 1]
      apply pow_eq_zero (n := p)
      exact h₁
    -- ... meaning x didn't have order p after all, contradiction
    apply ne_of_lt (Nat.Prime.one_lt pprime)
    rw [← hu, h₂, orderOf_one]

[Bolton Bailey]

Cool! Do you mind if I add this to #6500 @Buster? (Or you can add it yourself)

[Richard Copley]

I don't mind at all! Probably easier if you do it, if that's ok.

[Richard Copley]

I assume lots of improvements to the style and substance are possible. In particular, is that finiteness assumption (h : Fintype G) a bit weird?

(And Type u is a typo.)