Skip to content

Commit 7c2ef33

Browse files
ChrisHughes24ChrisHughes24
committed
chore(IsAlgClosed/Classification): make theorems more universe polymorphic (#18434)
1 parent a7ed2d0 commit 7c2ef33

File tree

2 files changed

+92
-45
lines changed

2 files changed

+92
-45
lines changed

‎Mathlib/FieldTheory/IsAlgClosed/Classification.lean‎

Lines changed: 88 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ This file contains results related to classifying algebraically closed fields.
2424
-/
2525

2626

27-
universe u
27+
universe u v w
2828

2929
open scoped Cardinal Polynomial
3030

@@ -73,82 +73,131 @@ end Classification
7373

7474
section Cardinal
7575

76-
variable {R K : Type u} [CommRing R] [Field K] [Algebra R K] [IsAlgClosed K]
77-
variable {ι : Type u} (v : ι → K)
76+
variable {R : Type u} {K : Type v} [CommRing R] [Field K] [Algebra R K] [IsAlgClosed K]
77+
variable {ι : Type w} (v : ι → K)
7878

79+
variable {K' : Type u} [Field K'] [Algebra R K'] [IsAlgClosed K']
80+
variable {ι' : Type u} (v' : ι' → K')
81+
82+
/-- The cardinality of an algebraically closed `R`-algebra is less than or equal to
83+
the maximum of of the cardinality of `R`, the cardinality of a transcendence basis and
84+
`ℵ₀`
85+
86+
For a simpler, but less universe-polymorphic statement, see
87+
`IsAlgCLosed.cardinal_le_max_transcendence_basis'` -/
7988
theorem cardinal_le_max_transcendence_basis (hv : IsTranscendenceBasis R v) :
80-
#K ≤ max (max #R #ι) ℵ₀ :=
89+
Cardinal.lift.{max u w} #K ≤ max (max (Cardinal.lift.{max v w} #R)
90+
(Cardinal.lift.{max u v} #ι)) ℵ₀ :=
8191
calc
82-
#K ≤ max #(Algebra.adjoin R (Set.range v)) ℵ₀ :=
92+
Cardinal.lift.{max u w} #K ≤ Cardinal.lift.{max u w}
93+
(max #(Algebra.adjoin R (Set.range v)) ℵ₀) := by
8394
letI := isAlgClosure_of_transcendence_basis v hv
84-
Algebra.IsAlgebraic.cardinalMk_le_max _ _
85-
_ = max #(MvPolynomial ι R) ℵ₀ := by rw [Cardinal.eq.2 ⟨hv.1.aevalEquiv.toEquiv⟩]
86-
_ ≤ max (max (max #R #ι) ℵ₀) ℵ₀ := max_le_max MvPolynomial.cardinalMk_le_max le_rfl
87-
_ = _ := by simp [max_assoc]
95+
simpa using Algebra.IsAlgebraic.cardinalMk_le_max (Algebra.adjoin R (Set.range v)) K
96+
_ = Cardinal.lift.{v} (max #(MvPolynomial ι R) ℵ₀) := by
97+
rw [lift_max, ← Cardinal.lift_mk_eq.2 ⟨hv.1.aevalEquiv.toEquiv⟩, lift_aleph0,
98+
← lift_aleph0.{max u v w, max u w}, ← lift_max, lift_umax.{max u w, v}]
99+
_ ≤ Cardinal.lift.{v} (max (max (max (Cardinal.lift #R) (Cardinal.lift #ι)) ℵ₀) ℵ₀) :=
100+
lift_le.2 (max_le_max MvPolynomial.cardinalMk_le_max_lift le_rfl)
101+
_ = _ := by simp
102+
103+
/-- The cardinality of an algebraically closed `R`-algebra is less than or equal to
104+
the maximum of of the cardinality of `R`, the cardinality of a transcendence basis and
105+
`ℵ₀`
106+
107+
A less-universe polymorphic, but simpler statement of
108+
`IsAlgCLosed.cardinal_le_max_transcendence_basis` -/
109+
theorem cardinal_le_max_transcendence_basis' (hv : IsTranscendenceBasis R v') :
110+
#K' ≤ max (max #R #ι') ℵ₀ := by
111+
simpa using cardinal_le_max_transcendence_basis v' hv
88112

89113
/-- If `K` is an uncountable algebraically closed field, then its
90-
cardinality is the same as that of a transcendence basis. -/
114+
cardinality is the same as that of a transcendence basis.
115+
116+
For a simpler, but less universe-polymorphic statement, see
117+
`IsAlgCLosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt'` -/
91118
theorem cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt [Nontrivial R]
92-
(hv : IsTranscendenceBasis R v) (hR : #R ≤ ℵ₀) (hK : ℵ₀ < #K) : #K = #ι :=
93-
have : ℵ₀ ≤ #ι := le_of_not_lt fun h => not_le_of_gt hK <|
119+
(hv : IsTranscendenceBasis R v) (hR : #R ≤ ℵ₀) (hK : ℵ₀ < #K) :
120+
Cardinal.lift.{w} #K = Cardinal.lift.{v} #ι :=
121+
have : ℵ₀ ≤ Cardinal.lift.{max u v} #ι := le_of_not_lt fun h => not_le_of_gt
122+
(show ℵ₀ < Cardinal.lift.{max u w} #K by simpa) <|
94123
calc
95-
#K ≤ max (max #R #ι) ℵ₀ := cardinal_le_max_transcendence_basis v hv
96-
_ ≤ _ := max_le (max_le hR (le_of_lt h)) le_rfl
124+
Cardinal.lift.{max u w, v} #K ≤ max (max (Cardinal.lift.{max v w, u} #R)
125+
(Cardinal.lift.{max u v, w} #ι)) ℵ₀ := cardinal_le_max_transcendence_basis v hv
126+
_ ≤ _ := max_le (max_le (by simpa) (by simpa using le_of_lt h)) le_rfl
127+
suffices Cardinal.lift.{max u w} #K = Cardinal.lift.{max u v} #ι
128+
from Cardinal.lift_injective.{u, max v w} (by simpa)
97129
le_antisymm
98130
(calc
99-
#K ≤ max (max #R #ι) ℵ₀ := cardinal_le_max_transcendence_basis v hv
100-
_ = #ι := by
131+
Cardinal.lift.{max u w} #K ≤ max (max
132+
(Cardinal.lift.{max v w} #R) (Cardinal.lift.{max u v} #ι)) ℵ₀ :=
133+
cardinal_le_max_transcendence_basis v hv
134+
_ = Cardinal.lift #ι := by
101135
rw [max_eq_left, max_eq_right]
102-
· exact le_trans hR this
136+
· exact le_trans (by simpa using hR) this
103137
· exact le_max_of_le_right this)
104-
(mk_le_of_injective (show Function.Injective v from hv.1.injective))
138+
(lift_mk_le.2 ⟨⟨v, hv.1.injective⟩⟩)
139+
140+
/-- If `K` is an uncountable algebraically closed field, then its
141+
cardinality is the same as that of a transcendence basis.
142+
143+
This is a simpler, but less general statement of
144+
`cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt`. -/
145+
theorem cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt' [Nontrivial R]
146+
(hv : IsTranscendenceBasis R v') (hR : #R ≤ ℵ₀) (hK : ℵ₀ < #K') : #K' = #ι' := by
147+
simpa using cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt v' hv hR hK
105148

106149
end Cardinal
107150

108-
variable {K L : Type} [Field K] [Field L] [IsAlgClosed K] [IsAlgClosed L]
151+
variable {K : Type u} {L : Type v} [Field K] [Field L] [IsAlgClosed K] [IsAlgClosed L]
109152

110153
/-- Two uncountable algebraically closed fields of characteristic zero are isomorphic
111154
if they have the same cardinality. -/
112-
theorem ringEquivOfCardinalEqOfCharZero [CharZero K] [CharZero L] (hK : ℵ₀ < #K)
113-
(hKL : #K = #L) : Nonempty (K ≃+* L) := by
155+
theorem ringEquiv_of_equiv_of_charZero [CharZero K] [CharZero L] (hK : ℵ₀ < #K)
156+
(hKL : Nonempty (K ≃ L)) : Nonempty (K ≃+* L) := by
114157
cases' exists_isTranscendenceBasis ℤ
115158
(show Function.Injective (algebraMap ℤ K) from Int.cast_injective) with s hs
116159
cases' exists_isTranscendenceBasis ℤ
117160
(show Function.Injective (algebraMap ℤ L) from Int.cast_injective) with t ht
118-
have : #s = #t := by
119-
rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs (le_of_eq mk_int) hK, ←
120-
cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht (le_of_eq mk_int), hKL]
121-
rwa [← hKL]
122-
cases' Cardinal.eq.1 this with e
161+
have hL : ℵ₀ < #L := by
162+
rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]
163+
have : Cardinal.lift.{v} #s = Cardinal.lift.{u} #t := by
164+
rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
165+
hs (le_of_eq mk_int) hK),
166+
← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
167+
ht (le_of_eq mk_int) hL)]
168+
exact Cardinal.lift_mk_eq'.2 hKL
169+
cases' Cardinal.lift_mk_eq'.1 this with e
123170
exact ⟨equivOfTranscendenceBasis _ _ e hs ht⟩
124171

125-
private theorem ringEquivOfCardinalEqOfCharP (p : ℕ) [Fact p.Prime] [CharP K p] [CharP L p]
126-
(hK : ℵ₀ < #K) (hKL : #K = #L) : Nonempty (K ≃+* L) := by
172+
private theorem ringEquiv_of_Cardinal_eq_of_charP (p : ℕ) [Fact p.Prime] [CharP K p] [CharP L p]
173+
(hK : ℵ₀ < #K) (hKL : Nonempty (K ≃ L)) : Nonempty (K ≃+* L) := by
127174
letI : Algebra (ZMod p) K := ZMod.algebra _ _
128175
letI : Algebra (ZMod p) L := ZMod.algebra _ _
129176
cases' exists_isTranscendenceBasis (ZMod p)
130177
(show Function.Injective (algebraMap (ZMod p) K) from RingHom.injective _) with s hs
131178
cases' exists_isTranscendenceBasis (ZMod p)
132179
(show Function.Injective (algebraMap (ZMod p) L) from RingHom.injective _) with t ht
133-
have : #s = #t := by
134-
rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs
135-
(lt_aleph0_of_finite (ZMod p)).le hK,
136-
← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht
137-
(lt_aleph0_of_finite (ZMod p)).le, hKL]
138-
rwa [← hKL]
139-
cases' Cardinal.eq.1 this with e
180+
have hL : ℵ₀ < #L := by
181+
rwa [← aleph0_lt_lift.{v, u}, ← lift_mk_eq'.2 hKL, aleph0_lt_lift]
182+
have : Cardinal.lift.{v} #s = Cardinal.lift.{u} #t := by
183+
rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
184+
hs (le_of_lt (lt_aleph0_of_finite _)) hK),
185+
← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
186+
ht (le_of_lt (lt_aleph0_of_finite _)) hL)]
187+
exact Cardinal.lift_mk_eq'.2 hKL
188+
cases' Cardinal.lift_mk_eq'.1 this with e
140189
exact ⟨equivOfTranscendenceBasis _ _ e hs ht⟩
141190

142191
/-- Two uncountable algebraically closed fields are isomorphic
143192
if they have the same cardinality and the same characteristic. -/
144-
theorem ringEquivOfCardinalEqOfCharEq (p : ℕ) [CharP K p] [CharP L p] (hK : ℵ₀ < #K)
145-
(hKL : #K = #L) : Nonempty (K ≃+* L) := by
193+
theorem ringEquiv_of_equiv_of_char_eq (p : ℕ) [CharP K p] [CharP L p] (hK : ℵ₀ < #K)
194+
(hKL : Nonempty (K ≃ L)) : Nonempty (K ≃+* L) := by
146195
rcases CharP.char_is_prime_or_zero K p with (hp | hp)
147196
· haveI : Fact p.Prime := ⟨hp⟩
148-
exact ringEquivOfCardinalEqOfCharP p hK hKL
197+
exact ringEquiv_of_Cardinal_eq_of_charP p hK hKL
149198
· simp only [hp] at *
150199
letI : CharZero K := CharP.charP_to_charZero K
151200
letI : CharZero L := CharP.charP_to_charZero L
152-
exact ringEquivOfCardinalEqOfCharZero hK hKL
201+
exact ringEquiv_of_equiv_of_charZero hK hKL
153202

154203
end IsAlgClosed

‎Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean‎

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -146,10 +146,8 @@ theorem ACF_isSatisfiable {p : ℕ} (hp : p.Prime ∨ p = 0) :
146146

147147
open Cardinal
148148

149-
/-- The Theory `Theory.ACF p` is `κ`-categorical whenever `κ` is an uncountable cardinal.
150-
At the moment this is not as universe polymorphic as it could be,
151-
it currently requires `κ : Cardinal.{0}`, but it is true for any universe. -/
152-
theorem ACF_categorical {p : ℕ} (κ : Cardinal.{0}) (hκ : ℵ₀ < κ) :
149+
/-- The Theory `Theory.ACF p` is `κ`-categorical whenever `κ` is an uncountable cardinal. -/
150+
theorem ACF_categorical {p : ℕ} (κ : Cardinal) (hκ : ℵ₀ < κ) :
153151
Categorical κ (Theory.ACF p) := by
154152
rintro ⟨M⟩ ⟨N⟩ hM hN
155153
let _ := fieldOfModelACF p M
@@ -165,9 +163,9 @@ theorem ACF_categorical {p : ℕ} (κ : Cardinal.{0}) (hκ : ℵ₀ < κ) :
165163
constructor
166164
refine languageEquivEquivRingEquiv.symm ?_
167165
apply Classical.choice
168-
refine IsAlgClosed.ringEquivOfCardinalEqOfCharEq p ?_ ?_
166+
refine IsAlgClosed.ringEquiv_of_equiv_of_char_eq p ?_ ?_
169167
· rw [hM]; exact hκ
170-
· rw [hM, hN]
168+
· rw [← Cardinal.eq, hM, hN]
171169

172170
theorem ACF_isComplete {p : ℕ} (hp : p.Prime ∨ p = 0) :
173171
(Theory.ACF p).IsComplete := by

0 commit comments

Comments
 (0)