Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(field_theory/cardinality): a cardinal can have a field structure iff it is a prime power #12442

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat(field_theory/cardinality): a cardinal can have a field structure iff it is a prime power #12442

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
4b2e3a4
feat(field_theory/cardinality): a cardinal can have a field structure…
ericrbg Mar 4, 2022
20555d4
docs
ericrbg Mar 4, 2022
1577dda
iff
ericrbg Mar 4, 2022
c997d65
less clunky proof
ericrbg Mar 4, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 14 additions & 1 deletion src/field_theory/cardinality.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ 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 set_theory.cardinal_divisibility
import field_theory.finite.galois_field
import data.equiv.transfer_instance
import algebra.ring.ulift
Expand All @@ -22,6 +22,7 @@ a field structure, and so can all types with prime power cardinalities, and this
* `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.
* `field.nonempty_iff` : There is a field structure on type iff its cardinality is a prime power.

-/

Expand Down Expand Up @@ -69,3 +70,15 @@ begin
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

/-- There is a field structure on type if and only if its cardinality is a prime power. -/
lemma field.nonempty_iff {α : Type u} : nonempty (field α) ↔ is_prime_pow (#α) :=
begin
rw cardinal.is_prime_pow_iff,
casesI fintype_or_infinite α with h h,
{ simpa only [cardinal.mk_fintype, nat.cast_inj, exists_eq_left',
(cardinal.nat_lt_omega _).not_le, false_or]
using fintype.nonempty_field_iff },
{ simpa only [← cardinal.infinite_iff, h, true_or, iff_true]
using infinite.nonempty_field },
end