[Merged by Bors] - feat(field_theory/cardinality): cardinality of fields & localizations

src/field_theory/cardinality.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2022 Eric Rodriguez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Rodriguez
+-/
+import ring_theory.localization.cardinality
+import algebra.is_prime_pow
+import field_theory.finite.galois_field
+import data.equiv.transfer_instance
+import algebra.ring.ulift
+import data.mv_polynomial.cardinal
+import data.rat.denumerable
+
+/-!
+# Cardinality of Fields
+
+In this file we show all the possible cardinalities of fields. All infinite cardinals can harbour
+a field structure, and so can all types with prime power cardinalities, and this is sharp.
+
+## Main statements
+
+* `fintype.nonempty_field_iff`: A `fintype` can be given a field structure iff its cardinality is a
+  prime power.
+* `infinite.nonempty_field` : Any infinite type can be endowed a field structure.
+
+-/
+
+local notation `‖` x `‖` := fintype.card x
+
+open_locale cardinal non_zero_divisors
+
+universe u
+
+/-- A `fintype` can be given a field structure iff its cardinality is a prime power. -/
+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
+
+/-- Any infinite type can be endowed a field structure. -/
+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

src/ring_theory/localization/cardinality.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2022 Eric Rodriguez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Rodriguez
+-/
+import ring_theory.localization.basic
+import set_theory.cardinal_ordinal
+import ring_theory.integral_domain
+
+/-!
+# Cardinality of localizations
+
+In this file, we establish the cardinality of localizations. In most cases, a localization has
+cardinality equal to the base ring (even in the finite case!); however, this can be muddled by
+zero-divisors.
+
+## Main statements
+
+* `is_localization.cardinal_mk`: All infinite localizations of rings at submonoids smaller than the
+  non-zero divisors have the same cardinality as the base ring.
+* `is_localization.card`: All localizations of finite integral domains at submonoids not containing
+  zero have the same cardinality as the base domain.
+
+## Implementation details
+
+Note that in `is_localization.card`, the second `fintype` is not an instance, and is instead
+provided by `is_localization.fintype' S L`.
+
+-/
+
+
+open_locale cardinal non_zero_divisors
+
+universes u v
+
+namespace is_localization
+
+/-- All infinite localizations of rings at submonoids smaller than the non-zero divisors have the
+same cardinality as the base ring. -/
+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,
+  erw [←cardinal.mul_eq_self $ cardinal.omega_le_mk R],
+  let f : R × R → L := λ aa, is_localization.mk' _ aa.1 (if h : aa.2 ∈ S then ⟨aa.2, h⟩ else 1),
+  refine @cardinal.mk_le_of_surjective _ _ f (λ 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]
+end
+
+/-- All finite localizations of integral domains at submonoids not containing zero have the same
+cardinality as the base domain. -/
+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