Skip to content

Commit 1109970

Browse files
acmepjzacmepjz
committed
feat: IntermediateField.rank_sup_le (#19527)
New results: In `Mathlib/RingTheory/AlgebraicIndependent.lean`: - `IsTranscendenceBasis.lift_(cardinalMk|rank)_eq_max_lift`: if `x` is a transcendence basis of `E/F` and is not empty, then `[E:F] = #E = max(#F, #x, ℵ₀)` - `Algebra.Transcendental.rank_eq_cardinalMk`: if `E/F` is transcendental, then `[E:F] = #E`. (a corollary of above result) - `IntermediateField.rank_sup_le`: if `A` and `B` are intermediate fields of `E/F`, then `[AB:F] ≤ [A:F] * [B:F]` (an application of above result) In `Mathlib/RingTheory/Algebraic.lean`: - `[Algebra.]Transcendental.infinite`: a ring has infinitely many elements if it has a transcendental element. In `Mathlib/FieldTheory/MvRatFunc/Rank.lean` (new file): - `MvRatFunc.rank_eq_max_lift`: rank of multivariate rational function field. Note that we don't have `MvRatFunc` yet, so the statement uses `FractionRing (MvPolynomial ...)`. Eventually the theory of `MvRatFunc` should go this directory. Also move the results `Algebra.IsAlgebraic.[lift_]cardinalMk_le_XXX` from `Mathlib/FieldTheory/IsAlgClosed/Classification.lean` to a new file `Mathlib/RingTheory/Algebraic/Cardinality.lean` which has fewer imports.
1 parent 8d63494 commit 1109970

File tree

6 files changed

+188
-54
lines changed

6 files changed

+188
-54
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2985,6 +2985,7 @@ import Mathlib.FieldTheory.Minpoly.Field
29852985
import Mathlib.FieldTheory.Minpoly.IsConjRoot
29862986
import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
29872987
import Mathlib.FieldTheory.Minpoly.MinpolyDiv
2988+
import Mathlib.FieldTheory.MvRatFunc.Rank
29882989
import Mathlib.FieldTheory.Normal
29892990
import Mathlib.FieldTheory.NormalClosure
29902991
import Mathlib.FieldTheory.Perfect
@@ -4198,6 +4199,7 @@ import Mathlib.RingTheory.Adjoin.Tower
41984199
import Mathlib.RingTheory.AdjoinRoot
41994200
import Mathlib.RingTheory.AlgebraTower
42004201
import Mathlib.RingTheory.Algebraic
4202+
import Mathlib.RingTheory.Algebraic.Cardinality
42014203
import Mathlib.RingTheory.AlgebraicIndependent
42024204
import Mathlib.RingTheory.Artinian
42034205
import Mathlib.RingTheory.Bezout

‎Mathlib/FieldTheory/IsAlgClosed/Classification.lean‎

Lines changed: 1 addition & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Algebra.ZMod
77
import Mathlib.Algebra.MvPolynomial.Cardinal
88
import Mathlib.Algebra.Polynomial.Cardinal
99
import Mathlib.FieldTheory.IsAlgClosed.Basic
10+
import Mathlib.RingTheory.Algebraic.Cardinality
1011
import Mathlib.RingTheory.AlgebraicIndependent
1112

1213
/-!
@@ -29,59 +30,6 @@ open scoped Cardinal Polynomial
2930

3031
open Cardinal
3132

32-
section AlgebraicClosure
33-
34-
namespace Algebra.IsAlgebraic
35-
36-
variable (R L : Type u) [CommRing R] [CommRing L] [IsDomain L] [Algebra R L]
37-
variable [NoZeroSMulDivisors R L] [Algebra.IsAlgebraic R L]
38-
39-
theorem cardinalMk_le_sigma_polynomial :
40-
#L ≤ #(Σ p : R[X], { x : L // x ∈ p.aroots L }) :=
41-
@mk_le_of_injective L (Σ p : R[X], {x : L | x ∈ p.aroots L})
42-
(fun x : L =>
43-
let p := Classical.indefiniteDescription _ (Algebra.IsAlgebraic.isAlgebraic x)
44-
⟨p.1, x, by
45-
dsimp
46-
have h : p.1.map (algebraMap R L) ≠ 0 := by
47-
rw [Ne, ← Polynomial.degree_eq_bot,
48-
Polynomial.degree_map_eq_of_injective (NoZeroSMulDivisors.algebraMap_injective R L),
49-
Polynomial.degree_eq_bot]
50-
exact p.2.1
51-
rw [Polynomial.mem_roots h, Polynomial.IsRoot, Polynomial.eval_map, ← Polynomial.aeval_def,
52-
p.2.2]⟩)
53-
fun x y => by
54-
intro h
55-
simp? at h says simp only [Set.coe_setOf, ne_eq, Set.mem_setOf_eq, Sigma.mk.inj_iff] at h
56-
refine (Subtype.heq_iff_coe_eq ?_).1 h.2
57-
simp only [h.1, forall_true_iff]
58-
59-
@[deprecated (since := "2024-11-10")]
60-
alias cardinal_mk_le_sigma_polynomial := cardinalMk_le_sigma_polynomial
61-
62-
/-- The cardinality of an algebraic extension is at most the maximum of the cardinality
63-
of the base ring or `ℵ₀`. -/
64-
@[stacks 09GK]
65-
theorem cardinalMk_le_max : #L ≤ max #R ℵ₀ :=
66-
calc
67-
#L ≤ #(Σ p : R[X], { x : L // x ∈ p.aroots L }) :=
68-
cardinalMk_le_sigma_polynomial R L
69-
_ = Cardinal.sum fun p : R[X] => #{x : L | x ∈ p.aroots L} := by
70-
rw [← mk_sigma]; rfl
71-
_ ≤ Cardinal.sum.{u, u} fun _ : R[X] => ℵ₀ :=
72-
(sum_le_sum _ _ fun _ => (Multiset.finite_toSet _).lt_aleph0.le)
73-
_ = #(R[X]) * ℵ₀ := sum_const' _ _
74-
_ ≤ max (max #(R[X]) ℵ₀) ℵ₀ := mul_le_max _ _
75-
_ ≤ max (max (max #R ℵ₀) ℵ₀) ℵ₀ :=
76-
(max_le_max (max_le_max Polynomial.cardinalMk_le_max le_rfl) le_rfl)
77-
_ = max #R ℵ₀ := by simp only [max_assoc, max_comm ℵ₀, max_left_comm ℵ₀, max_self]
78-
79-
@[deprecated (since := "2024-11-10")] alias cardinal_mk_le_max := cardinalMk_le_max
80-
81-
end Algebra.IsAlgebraic
82-
83-
end AlgebraicClosure
84-
8533
namespace IsAlgClosed
8634

8735
section Classification

‎Mathlib/FieldTheory/MvRatFunc/Rank.lean‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
/-
2+
Copyright (c) 2024 Jz Pan. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jz Pan
5+
-/
6+
import Mathlib.Algebra.MvPolynomial.Cardinal
7+
import Mathlib.RingTheory.Algebraic
8+
import Mathlib.RingTheory.Localization.Cardinality
9+
import Mathlib.RingTheory.MvPolynomial
10+
11+
/-!
12+
# Rank of multivariate rational function field
13+
-/
14+
15+
noncomputable section
16+
17+
universe u v
18+
19+
open Cardinal in
20+
theorem MvRatFunc.rank_eq_max_lift
21+
{σ : Type u} {F : Type v} [Field F] [Nonempty σ] :
22+
Module.rank F (FractionRing (MvPolynomial σ F)) = lift.{u} #F ⊔ lift.{v} #σ ⊔ ℵ₀ := by
23+
let R := MvPolynomial σ F
24+
let K := FractionRing R
25+
refine ((rank_le_card _ _).trans ?_).antisymm ?_
26+
· rw [FractionRing.cardinalMk, MvPolynomial.cardinalMk_eq_max_lift]
27+
have hinj := IsFractionRing.injective R K
28+
have h1 := (IsScalarTower.toAlgHom F R K).toLinearMap.rank_le_of_injective hinj
29+
rw [MvPolynomial.rank_eq_lift, mk_finsupp_nat, lift_max, lift_aleph0, max_le_iff] at h1
30+
obtain ⟨i⟩ := ‹Nonempty σ›
31+
have hx : Transcendental F (algebraMap R K (MvPolynomial.X i)) :=
32+
(transcendental_algebraMap_iff hinj).2 (MvPolynomial.transcendental_X F i)
33+
have h2 := hx.linearIndependent_sub_inv.cardinal_lift_le_rank
34+
rw [lift_id'.{v, u}, lift_umax.{v, u}] at h2
35+
exact max_le (max_le h2 h1.1) h1.2

‎Mathlib/RingTheory/Algebraic.lean‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -951,3 +951,16 @@ theorem transcendental_supported_X_iff [Nontrivial R] {i : σ} {s : Set σ} :
951951
transcendental_supported_polynomial_aeval_X_iff R (i := i) (s := s) (f := Polynomial.X)
952952

953953
end MvPolynomial
954+
955+
section Infinite
956+
957+
theorem Transcendental.infinite {R A : Type*} [CommRing R] [Ring A] [Algebra R A]
958+
[Nontrivial R] {x : A} (hx : Transcendental R x) : Infinite A :=
959+
.of_injective _ (transcendental_iff_injective.mp hx)
960+
961+
theorem Algebra.Transcendental.infinite (R A : Type*) [CommRing R] [Ring A] [Algebra R A]
962+
[Nontrivial R] [Algebra.Transcendental R A] : Infinite A :=
963+
have ⟨x, hx⟩ := ‹Algebra.Transcendental R A›
964+
hx.infinite
965+
966+
end Infinite

‎Mathlib/RingTheory/Algebraic/Cardinality.lean‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
/-
2+
Copyright (c) 2022 Chris Hughes. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Chris Hughes
5+
-/
6+
import Mathlib.Algebra.Polynomial.Cardinal
7+
import Mathlib.RingTheory.Algebraic
8+
9+
/-!
10+
# Cardinality of algebraic extensions
11+
12+
This file contains results on cardinality of algebraic extensions.
13+
-/
14+
15+
16+
universe u v
17+
18+
open scoped Cardinal Polynomial
19+
20+
open Cardinal
21+
22+
namespace Algebra.IsAlgebraic
23+
24+
variable (R : Type u) [CommRing R] (L : Type v) [CommRing L] [IsDomain L] [Algebra R L]
25+
variable [NoZeroSMulDivisors R L] [Algebra.IsAlgebraic R L]
26+
27+
theorem lift_cardinalMk_le_sigma_polynomial :
28+
lift.{u} #L ≤ #(Σ p : R[X], { x : L // x ∈ p.aroots L }) := by
29+
have := @lift_mk_le_lift_mk_of_injective L (Σ p : R[X], {x : L | x ∈ p.aroots L})
30+
(fun x : L =>
31+
let p := Classical.indefiniteDescription _ (Algebra.IsAlgebraic.isAlgebraic x)
32+
⟨p.1, x, by
33+
dsimp
34+
have := (Polynomial.map_ne_zero_iff (NoZeroSMulDivisors.algebraMap_injective R L)).2 p.2.1
35+
rw [Polynomial.mem_roots this, Polynomial.IsRoot, Polynomial.eval_map,
36+
← Polynomial.aeval_def, p.2.2]⟩)
37+
fun x y => by
38+
intro h
39+
simp only [Set.coe_setOf, ne_eq, Set.mem_setOf_eq, Sigma.mk.inj_iff] at h
40+
refine (Subtype.heq_iff_coe_eq ?_).1 h.2
41+
simp only [h.1, forall_true_iff]
42+
rwa [lift_umax, lift_id'.{v}] at this
43+
44+
theorem lift_cardinalMk_le_max : lift.{u} #L ≤ lift.{v} #R ⊔ ℵ₀ :=
45+
calc
46+
lift.{u} #L ≤ #(Σ p : R[X], { x : L // x ∈ p.aroots L }) :=
47+
lift_cardinalMk_le_sigma_polynomial R L
48+
_ = Cardinal.sum fun p : R[X] => #{x : L | x ∈ p.aroots L} := by
49+
rw [← mk_sigma]; rfl
50+
_ ≤ Cardinal.sum.{u, v} fun _ : R[X] => ℵ₀ :=
51+
(sum_le_sum _ _ fun _ => (Multiset.finite_toSet _).lt_aleph0.le)
52+
_ = lift.{v} #(R[X]) * ℵ₀ := by rw [sum_const, lift_aleph0]
53+
_ ≤ lift.{v} (#R ⊔ ℵ₀) ⊔ ℵ₀ ⊔ ℵ₀ := (mul_le_max _ _).trans <| by
54+
gcongr; simp only [lift_le, Polynomial.cardinalMk_le_max]
55+
_ = _ := by simp
56+
57+
variable (L : Type u) [CommRing L] [IsDomain L] [Algebra R L]
58+
variable [NoZeroSMulDivisors R L] [Algebra.IsAlgebraic R L]
59+
60+
theorem cardinalMk_le_sigma_polynomial :
61+
#L ≤ #(Σ p : R[X], { x : L // x ∈ p.aroots L }) := by
62+
simpa only [lift_id] using lift_cardinalMk_le_sigma_polynomial R L
63+
64+
@[deprecated (since := "2024-11-10")]
65+
alias cardinal_mk_le_sigma_polynomial := cardinalMk_le_sigma_polynomial
66+
67+
/-- The cardinality of an algebraic extension is at most the maximum of the cardinality
68+
of the base ring or `ℵ₀`. -/
69+
@[stacks 09GK]
70+
theorem cardinalMk_le_max : #L ≤ max #R ℵ₀ := by
71+
simpa only [lift_id] using lift_cardinalMk_le_max R L
72+
73+
@[deprecated (since := "2024-11-10")] alias cardinal_mk_le_max := cardinalMk_le_max
74+
75+
end Algebra.IsAlgebraic

‎Mathlib/RingTheory/AlgebraicIndependent.lean‎

Lines changed: 62 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@ Authors: Chris Hughes
66
import Mathlib.Algebra.MvPolynomial.Monad
77
import Mathlib.Data.Fin.Tuple.Reflection
88
import Mathlib.FieldTheory.Adjoin
9+
import Mathlib.FieldTheory.MvRatFunc.Rank
10+
import Mathlib.RingTheory.Algebraic.Cardinality
911
import Mathlib.RingTheory.MvPolynomial.Basic
1012

1113
/-!
@@ -56,7 +58,7 @@ open Function Set Subalgebra MvPolynomial Algebra
5658

5759
open scoped Classical
5860

59-
universe x u v w
61+
universe u v w
6062

6163
variable {ι : Type*} {ι' : Type*} (R : Type*) {K : Type*}
6264
variable {A : Type*} {A' : Type*}
@@ -741,3 +743,62 @@ theorem algebraicIndependent_empty [Nontrivial A] :
741743
algebraicIndependent_empty_type
742744

743745
end Field
746+
747+
section RankAndCardinality
748+
749+
open Cardinal
750+
751+
theorem IsTranscendenceBasis.lift_cardinalMk_eq_max_lift
752+
{F : Type u} {E : Type v} [CommRing F] [Nontrivial F] [CommRing E] [IsDomain E] [Algebra F E]
753+
{ι : Type w} {x : ι → E} [Nonempty ι] (hx : IsTranscendenceBasis F x) :
754+
lift.{max u w} #E = lift.{max v w} #F ⊔ lift.{max u v} #ι ⊔ ℵ₀ := by
755+
let K := Algebra.adjoin F (Set.range x)
756+
suffices #E = #K by simp [this, ← lift_mk_eq'.2 ⟨hx.1.aevalEquiv.toEquiv⟩]
757+
haveI : Algebra.IsAlgebraic K E := hx.isAlgebraic
758+
refine le_antisymm ?_ (mk_le_of_injective Subtype.val_injective)
759+
haveI : Infinite K := hx.1.aevalEquiv.infinite_iff.1 inferInstance
760+
simpa only [sup_eq_left.2 (aleph0_le_mk K)] using Algebra.IsAlgebraic.cardinalMk_le_max K E
761+
762+
theorem IsTranscendenceBasis.lift_rank_eq_max_lift
763+
{F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
764+
{ι : Type w} {x : ι → E} [Nonempty ι] (hx : IsTranscendenceBasis F x) :
765+
lift.{max u w} (Module.rank F E) = lift.{max v w} #F ⊔ lift.{max u v} #ι ⊔ ℵ₀ := by
766+
let K := IntermediateField.adjoin F (Set.range x)
767+
haveI : Algebra.IsAlgebraic K E := hx.isAlgebraic_field
768+
rw [← rank_mul_rank F K E, lift_mul, ← hx.1.aevalEquivField.toLinearEquiv.lift_rank_eq,
769+
MvRatFunc.rank_eq_max_lift, lift_max, lift_max, lift_lift, lift_lift, lift_aleph0]
770+
refine mul_eq_left le_sup_right ((lift_le.2 ((rank_le_card K E).trans
771+
(Algebra.IsAlgebraic.cardinalMk_le_max K E))).trans_eq ?_) (by simp [rank_pos.ne'])
772+
simp [← lift_mk_eq'.2 ⟨hx.1.aevalEquivField.toEquiv⟩]
773+
774+
theorem Algebra.Transcendental.rank_eq_cardinalMk
775+
(F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.Transcendental F E] :
776+
Module.rank F E = #E := by
777+
obtain ⟨ι, x, hx⟩ := exists_isTranscendenceBasis' _ (algebraMap F E).injective
778+
haveI := hx.nonempty_iff_transcendental.2 ‹_›
779+
simpa [← hx.lift_cardinalMk_eq_max_lift] using hx.lift_rank_eq_max_lift
780+
781+
theorem IntermediateField.rank_sup_le
782+
{F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) :
783+
Module.rank F ↥(A ⊔ B) ≤ Module.rank F A * Module.rank F B := by
784+
by_cases hA : Algebra.IsAlgebraic F A
785+
· exact rank_sup_le_of_isAlgebraic A B (Or.inl hA)
786+
by_cases hB : Algebra.IsAlgebraic F B
787+
· exact rank_sup_le_of_isAlgebraic A B (Or.inr hB)
788+
rw [← Algebra.transcendental_iff_not_isAlgebraic] at hA hB
789+
haveI : Algebra.Transcendental F ↥(A ⊔ B) := .ringHom_of_comp_eq (RingHom.id F)
790+
(inclusion le_sup_left) Function.surjective_id (inclusion_injective _) rfl
791+
haveI := Algebra.Transcendental.infinite F A
792+
haveI := Algebra.Transcendental.infinite F B
793+
simp_rw [Algebra.Transcendental.rank_eq_cardinalMk]
794+
rw [sup_def, mul_mk_eq_max, ← Cardinal.lift_le.{u}]
795+
refine (lift_cardinalMk_adjoin_le _ _).trans ?_
796+
calc
797+
_ ≤ Cardinal.lift.{v} #F ⊔ Cardinal.lift.{u} (#A ⊔ #B) ⊔ ℵ₀ := by
798+
gcongr
799+
rw [Cardinal.lift_le]
800+
exact (mk_union_le _ _).trans_eq (by simp)
801+
_ = _ := by
802+
simp [lift_mk_le_lift_mk_of_injective (algebraMap F A).injective]
803+
804+
end RankAndCardinality

0 commit comments

Comments
 (0)