cardinality of a field

Stream: general

[Eric Rodriguez]

I've now finished the result in full generality! (I'm moving this away from the thread that I hijacked, sorry Jireh)

Field is p^k or any possible cardinality

import field_theory.finite.galois_field
import algebra.is_prime_pow
import data.equiv.transfer_instance
import data.mv_polynomial.cardinal
import data.rat.denumerable

local notation `‖` x `‖` := fintype.card x
open_locale cardinal non_zero_divisors

lemma nat.prime.is_prime_pow {p : ℕ} (hp : p.prime) : is_prime_pow p :=
(is_prime_pow_nat_iff p).mpr ⟨p, 1, hp, one_pos, pow_one p⟩

example {α} [fintype α] : nonempty (field α) ↔ is_prime_pow (fintype.card α) :=
begin
  split,
  swap,
  { rintros ⟨p, n, hp, hn, hα⟩,
    haveI := fact.mk (nat.prime_iff.mpr hp),
    exact ⟨(fintype.equiv_of_card_eq ((galois_field.card p n hn.ne').trans hα)).symm.field⟩ },
  rintro ⟨h⟩,
  casesI char_p.exists α with p _,
  haveI hp := fact.mk (char_p.char_is_prime α p),
  let b := is_noetherian.finset_basis (zmod p) α,
  rw [module.card_fintype b, zmod.card, is_prime_pow_pow_iff],
  exact hp.1.is_prime_pow,
  rw ←finite_dimensional.finrank_eq_card_basis b,
  exact finite_dimensional.finrank_pos.ne'
end

lemma monomial_ext_iff {α} {R} [comm_semiring R] {a b : α →₀ ℕ} {c d : R} (hc : c ≠ 0) :
  mv_polynomial.monomial a c = mv_polynomial.monomial b d ↔ a = b ∧ c = d :=
begin
  refine ⟨λ h, _, by {rintro ⟨rfl, rfl⟩, refl}⟩,
  replace h := (mv_polynomial.ext_iff _ _).mp h a,
  classical,
  simp only [mv_polynomial.coeff_monomial, eq_self_iff_true, if_true] at h,
  split_ifs at h; tauto
end

example {α} [infinite α] : nonempty (field α) :=
begin
  letI K := fraction_ring (mv_polynomial α ℚ),
  suffices : #K ≤ #α,
  { let f := λ a : α, algebra_map _ K (mv_polynomial.monomial (finsupp.single a 1) (1 : ℚ)),
    have hf : function.injective f,
    { intros a b h,
      dsimp only [f] at h,
      replace h := is_fraction_ring.injective _ K h,
      rw monomial_ext_iff (@one_ne_zero ℚ _ _) at h,
      exact finsupp.single_left_injective one_ne_zero h.1 },
    obtain ⟨e⟩ := cardinal.eq.mp (le_antisymm this $ cardinal.mk_le_of_injective hf),
    exact ⟨e.symm.field⟩ },
  classical,
  let f : (mv_polynomial α ℚ) × (mv_polynomial α ℚ) → K :=
    λ aa, is_localization.mk' _ aa.1 (if h : aa.2 ∈ (mv_polynomial α ℚ)⁰ then ⟨aa.2, h⟩ else 1),
  have hf : function.surjective f,
  { intro a,
    obtain ⟨x, y, h⟩ := is_localization.mk'_surjective (mv_polynomial α ℚ)⁰ a,
    use ⟨x, y⟩,
    dsimp [f],
    have := y.2, -- can I avoid this?
    simp only [subtype.val_eq_coe] at this,
    rwa [dif_pos this, set_like.eta] },
  apply (cardinal.mk_le_of_surjective hf).trans,
  rw [←cardinal.mul_def, cardinal.mul_eq_self $ cardinal.omega_le_mk $ mv_polynomial α ℚ],
  have := @mv_polynomial.cardinal_mk_le_max α ℚ _,
  rw cardinal.mk_rat at this,
  cases (cardinal.omega_le_mk α).eq_or_lt with h h,
  { simpa [h] using this },
  { rwa [max_eq_right_of_lt h, max_eq_left_of_lt h] at this }
  --why is there no `max_eq_right_of_le?!`
end

this needs cleaning up, but I have to run - I'm happy for anyone to fix things up! I left a couple comments about my frustrations...

cc: @Mario Carneiro @Alex J. Best who seemed interested

[Alex J. Best]

Nice, the last 3 lines can just be simpa I think

[Alex J. Best]

And docs#finsupp.single_eq_single_iff exists so you can do

lemma monomial_ext_iff {α} {R} [comm_semiring R] {a b : α →₀ ℕ} {c d : R} (hc : c ≠ 0) :
  mv_polynomial.monomial a c = mv_polynomial.monomial b d ↔ a = b ∧ c = d :=
begin
  convert finsupp.single_eq_single_iff _ _ _ _,
  simp [hc],
end

[Eric Rodriguez]

Also, i just realised the general result can just be is_prime_power #a - as all infinite cardinals are prime :) (probably too cute though)

[Kevin Buzzard]

wait, if $\kappa$ is an infinite cardinal then $\kappa=\kappa\times\kappa$ right?

[Eric Rodriguez]

the result (modulo cute cardinal stuff) is finally pr'd! #12285 (I need #12197 for the cute cardinal stuff)

[Eric Rodriguez]

(and we have cute cardinal stuff on #12442)