The cardinality of a field!

field_cardinality.lean

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
import algebra.ring.ulift

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

universes u v

lemma fintype.nonempty_field_iff {α} [fintype α] :
  nonempty (field α) ↔ is_prime_pow (‖α‖) :=
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

namespace is_localization

lemma cardinal_mk {R : Type u} [comm_ring R] {S : submonoid R} (L : Type u) [comm_ring L]
  [algebra R L] [infinite R] [is_localization S L] (hS : S ≤ R⁰) : #R = #L :=
begin
  classical,
  apply (cardinal.mk_le_of_injective (is_localization.injective L hS)).antisymm,
  let f : R × R → L := λ aa, is_localization.mk' _ aa.1 (if h : aa.2 ∈ S then ⟨aa.2, h⟩ else 1),
  have hf : function.surjective f,
  { intro a,
    obtain ⟨x, y, h⟩ := is_localization.mk'_surjective S a,
    use (x, y),
    dsimp [f],
    rwa [dif_pos $ show ↑y ∈ S, from y.2, set_like.eta] },
  have := cardinal.mk_le_of_surjective hf,
  rwa [←cardinal.mul_def, cardinal.mul_eq_self $ cardinal.omega_le_mk $ R] at this
end

lemma card {R : Type u} [comm_ring R] {S : submonoid R} {L : Type v} [comm_ring L] [algebra R L]
  [fintype R] [is_domain R] [is_localization S L] (hS : ↑0 ∉ S) :
  fintype.card R = @fintype.card L (fintype' S L) :=
begin
  casesI subsingleton_or_nontrivial R,
  { haveI := unique R L S,
    haveI := unique_of_subsingleton (0 : R),
    simp },
  letI := fintype' S L,
  refine fintype.card_of_bijective
         (localization_map_bijective_of_field hS ⟨nontrivial.exists_pair_ne, mul_comm, λ a ha, _⟩),
  classical,
  letI hG := group_with_zero_of_fintype R,
  exact ⟨a⁻¹, mul_inv_cancel ha⟩
end

end is_localization

lemma infinite.nonempty_field {α : Type u} [infinite α] : nonempty (field α) :=
begin
  letI K := fraction_ring (mv_polynomial α $ ulift.{u} ℚ),
  suffices : #α = #K,
  { obtain ⟨e⟩ := cardinal.eq.1 this,
    exact ⟨e.field⟩ },
  rw ←is_localization.cardinal_mk K (le_refl (mv_polynomial α $ ulift.{u} ℚ)⁰),
  apply le_antisymm,
  { refine ⟨⟨λ a, mv_polynomial.monomial (finsupp.single a 1) (1 : ulift.{u} ℚ), λ x y h, _⟩⟩,
    simpa [mv_polynomial.monomial_eq_monomial_iff, finsupp.single_eq_single_iff] using h },
  { simpa using @mv_polynomial.cardinal_mk_le_max α (ulift.{u} ℚ) _ }
end

namespace cardinal

variables {a b : cardinal.{u}} {n m : ℕ}

@[simp] lemma is_unit_iff : is_unit a ↔ a = 1 :=
begin
  refine ⟨λ h, _, by { rintro rfl, exact is_unit_one }⟩,
  rcases eq_or_ne a 0 with rfl | ha,
  { exact (not_is_unit_zero h).elim },
  rw is_unit_iff_forall_dvd at h,
  contrapose! h,
  use 1,
  rintro ⟨t, ht⟩,
  rw [eq_comm, mul_eq_one_iff'] at ht,
  { exact h ht.1 },
  { rwa one_le_iff_ne_zero },
  { rw one_le_iff_ne_zero,
    rintro rfl,
    rw mul_zero at ht,
    exact zero_ne_one ht }
end

theorem le_of_dvd : ∀ {a b : cardinal}, b ≠ 0 → a ∣ b → a ≤ b
| a _ b0 ⟨b, rfl⟩ := by simpa only [mul_one] using mul_le_mul_left'
  (one_le_iff_ne_zero.2 (λ h : b = 0, by simpa only [h, mul_zero] using b0)) a

lemma omega_le_mul_iff : ω ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ω ≤ a ∨ ω ≤ b) :=
begin
  have := (@mul_lt_omega_iff a b).not,
  rwa [not_lt, not_or_distrib, not_or_distrib, not_and_distrib, not_lt, not_lt] at this
end

lemma dvd_of_le_of_omega_le (ha : a ≠ 0) (hb : ω ≤ b) (h : a ≤ b) : a ∣ b :=
⟨b, (mul_eq_right hb h ha).symm⟩

lemma mul_eq_max' (h : ω ≤ a * b) : a * b = max a b :=
by begin
  rcases omega_le_mul_iff.mp h with ⟨ha, hb, h⟩,
  wlog h : ω ≤ a := h using [a b],
  exact cardinal.mul_eq_max_of_omega_le_left h hb
end

@[simp] lemma prime_of_omega_le (ha : ω ≤ a) : prime a :=
by begin
  refine ⟨(omega_pos.trans_le ha).ne', _, _⟩,
  { rw is_unit_iff,
    exact (one_lt_omega.trans_le ha).ne' },
  rintro b c hbc,
  rcases eq_or_ne (b * c) 0 with hz | hz,
  { rcases mul_eq_zero.mp hz with rfl | rfl; simp },
  wlog h : c ≤ b,
  left,
  have habc := le_of_dvd hz hbc,
  rwa [mul_eq_max' $ ha.trans $ habc, max_def, if_pos h] at hbc
end

@[simp, norm_cast] lemma nat_coe_dvd_iff : (n : cardinal) ∣ m ↔ n ∣ m :=
begin
  refine ⟨_, λ ⟨h, ht⟩, ⟨h, by exact_mod_cast ht⟩⟩,
  rintro ⟨k, hk⟩,
  have : ↑m < ω := nat_lt_omega m,
  rw [hk, mul_lt_omega_iff] at this,
  rcases this with h | h | ⟨-, hk'⟩,
  { rw [h, zero_mul, nat.cast_eq_zero] at hk, simp [hk] },
  { rw [h, mul_zero, nat.cast_eq_zero] at hk, simp [hk] },
  lift k to ℕ using hk',
  exact ⟨k, by exact_mod_cast hk⟩
end

@[simp] lemma nat_is_prime_iff : prime (n : cardinal) ↔ n.prime :=
by begin
  simp only [prime, nat.prime_iff],
  apply and_congr _ (and_congr _ ⟨_, _⟩),
  { simp },
  { simp only [is_unit_iff, nat.is_unit_iff],
    refine ⟨λ h, _, λ h, _⟩; exact_mod_cast h },
  { intros h b c hbc,
    exact_mod_cast h b c (by exact_mod_cast hbc) },
  rintros h b c hbc,
  cases lt_or_le (b * c) ω with h' h',
  { rcases mul_lt_omega_iff.mp h' with rfl | rfl | ⟨hb, hc⟩,
    { simp },
    { simp },
    lift b to ℕ using hb,
    lift c to ℕ using hc,
    exact_mod_cast h b c (by exact_mod_cast hbc) },
  rcases omega_le_mul_iff.mp h' with ⟨hb, hc, hω⟩,
  have hn : (n : cardinal) ≠ 0,
  { intro h,
    rw [h, zero_dvd_iff, mul_eq_zero] at hbc,
    cases hbc; contradiction },
  wlog hω : ω ≤ b := hω using [b c],
  exact or.inl (dvd_of_le_of_omega_le hn hω ((nat_lt_omega n).le.trans hω)),
end

lemma is_prime_iff {a : cardinal} : prime a ↔ ω ≤ a ∨ ∃ p : ℕ, a = p ∧ p.prime :=
begin
  cases le_or_lt ω a with h h,
  { simp [h] },
  lift a to ℕ using id h,
  simp [not_le.mpr h]
end

lemma is_prime_pow_iff {a : cardinal} : is_prime_pow a ↔ ω ≤ a ∨ ∃ n : ℕ, a = n ∧ is_prime_pow n :=
begin
  by_cases h : ω ≤ a,
  { simp [h, (prime_of_omega_le h).is_prime_pow] },
  lift a to ℕ using not_le.mp h,
  simp only [h, nat.cast_inj, exists_eq_left', false_or, is_prime_pow_nat_iff],
  rw is_prime_pow_def,
  split,
  swap,
  { rintro ⟨p, k, hp, hk, rfl⟩,
    exact ⟨p, k, nat_is_prime_iff.mpr hp, by exact_mod_cast hk, by norm_cast⟩ },
  rintro ⟨p, k, hp, hk, hpk⟩,
  have key : _ ≤ p ^ k :=
    power_le_power_left hp.ne_zero (show (1 : cardinal) ≤ k, by exact_mod_cast hk),
  rw [power_one, hpk] at key,
  lift p to ℕ using key.trans_lt (nat_lt_omega a),
  refine ⟨p, k, nat_is_prime_iff.mp hp, hk, by exact_mod_cast hpk⟩
end

end cardinal

lemma field.nonempty_iff {α : Type u} : nonempty (field α) ↔ is_prime_pow (#α) :=
begin
  rw cardinal.is_prime_pow_iff,
  by_cases ω ≤ (#α),
  { simp only [h, true_or, iff_true],
    haveI := cardinal.infinite_iff.mpr h,
    exact infinite.nonempty_field },
  casesI cardinal.lt_omega_iff_fintype.mp (not_le.mp h),
  simp_rw [h, false_or, cardinal.mk_fintype, nat.cast_inj, exists_eq_left'],
  exact fintype.nonempty_field_iff
end