From f8f5894f0b703e3bfef7f0877f313811ffe76974 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 27 Mar 2026 22:13:01 +0800 Subject: [PATCH 01/30] Create TranscendentalSeparable.lean add basic definitions --- .../FieldTheory/TranscendentalSeparable.lean | 28 +++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 Mathlib/FieldTheory/TranscendentalSeparable.lean diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean new file mode 100644 index 00000000000000..c2a8fbc5789572 --- /dev/null +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -0,0 +1,28 @@ +/- +Copyright (c) 2026 Nailin Guan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Nailin Guan +-/ +module + +public import Mathlib.FieldTheory.Separable +public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis + +/-! +# Transcendental separable extensions +-/ + +universe u v + +variable (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] + +@[expose] public section + +class Algebra.IsSeparablyGenerated : Prop where + isSeparable' : ∃ (ι : Type v) (f : ι → A), + IsTranscendenceBasis R f ∧ + Algebra.IsSeparable (Algebra.adjoin R (Set.range f)) A + +class Algebra.IsTranscendentalSeparable : Prop where + forall_isSeparablyGenerated : ∀ (A' : Subalgebra R A), + Algebra.EssFiniteType R A' → Algebra.IsSeparablyGenerated R A' From 80c1fb127644c33e2bc8d263d3f2c89bd4feb549 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 27 Mar 2026 22:13:51 +0800 Subject: [PATCH 02/30] Update Mathlib.lean --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 3a02d09d826968..deafc942169b12 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -4387,6 +4387,7 @@ public import Mathlib.FieldTheory.SeparablyGenerated public import Mathlib.FieldTheory.SplittingField.Construction public import Mathlib.FieldTheory.SplittingField.IsSplittingField public import Mathlib.FieldTheory.Tower +public import Mathlib.FieldTheory.TranscendentalSeparable public import Mathlib.Geometry.Convex.Cone.Basic public import Mathlib.Geometry.Convex.Cone.Dual public import Mathlib.Geometry.Convex.Cone.Pointed From ea2eb132930dccd3ec46654689a7a5a0c9ccfebc Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 28 Mar 2026 13:57:39 +0800 Subject: [PATCH 03/30] Update TranscendentalSeparable.lean --- Mathlib/FieldTheory/TranscendentalSeparable.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index c2a8fbc5789572..e2517d3deacef7 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -26,3 +26,8 @@ class Algebra.IsSeparablyGenerated : Prop where class Algebra.IsTranscendentalSeparable : Prop where forall_isSeparablyGenerated : ∀ (A' : Subalgebra R A), Algebra.EssFiniteType R A' → Algebra.IsSeparablyGenerated R A' + +lemma tensorProduct_of_isSeparablyGenerated {k : Type*} [Field k] + {S : Type*} [CommRing S] [IsReduced S] [Algebra k S] {K : Type*} [Field K] [Algebra k K] : + IsReduced (TensorProduct k K S) := by + sorry From 93d1c451b1d99700990e986da17703682a42ce9c Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 28 Mar 2026 14:26:26 +0800 Subject: [PATCH 04/30] Update TranscendentalSeparable.lean --- Mathlib/FieldTheory/TranscendentalSeparable.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index e2517d3deacef7..e8b36d783f61ff 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -5,6 +5,7 @@ Authors: Nailin Guan -/ module +public import Mathlib.FieldTheory.Perfect public import Mathlib.FieldTheory.Separable public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis @@ -31,3 +32,7 @@ lemma tensorProduct_of_isSeparablyGenerated {k : Type*} [Field k] {S : Type*} [CommRing S] [IsReduced S] [Algebra k S] {K : Type*} [Field K] [Algebra k K] : IsReduced (TensorProduct k K S) := by sorry + +lemma Algebra.isTranscendentalSeparable_of_perfectField {k : Type*} [Field k] [PerfectField k] + {K : Type*} [Field K] [Algebra k K] : Algebra.IsTranscendentalSeparable k K := by + sorry From acd045e73239cd00864a6984e8d7c270784121ff Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 28 Mar 2026 22:08:28 +0800 Subject: [PATCH 05/30] Update TranscendentalSeparable.lean --- .../FieldTheory/TranscendentalSeparable.lean | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index e8b36d783f61ff..f42a3f31a06ab6 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -5,6 +5,8 @@ Authors: Nailin Guan -/ module +public import Mathlib.RingTheory.Flat.Basic +public import Mathlib.RingTheory.TensorProduct.DirectLimitFG public import Mathlib.FieldTheory.Perfect public import Mathlib.FieldTheory.Separable public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis @@ -19,6 +21,8 @@ variable (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] @[expose] public section +open TensorProduct + class Algebra.IsSeparablyGenerated : Prop where isSeparable' : ∃ (ι : Type v) (f : ι → A), IsTranscendenceBasis R f ∧ @@ -28,6 +32,38 @@ class Algebra.IsTranscendentalSeparable : Prop where forall_isSeparablyGenerated : ∀ (A' : Subalgebra R A), Algebra.EssFiniteType R A' → Algebra.IsSeparablyGenerated R A' +set_option backward.isDefEq.respectTransparency false in +/-- If `R ⊗[k] S` is nonreduced, then this already occurs on finitely generated `k`-subalgebras +of `R` and `S`. -/ +lemma exists_subalgebra_fg_of_not_isReduced_tensorProduct + (k R S : Type*) [Field k] [CommRing R] [CommRing S] [Algebra k R] [Algebra k S] + (h : ¬ IsReduced (R ⊗[k] S)) : + ∃ R' : Subalgebra k R, ∃ S' : Subalgebra k S, R'.FG ∧ S'.FG ∧ ¬ IsReduced (R' ⊗[k] S') := by + obtain ⟨z, hz_ne, ⟨n, hn⟩⟩ := exists_isNilpotent_of_not_isReduced h + rcases TensorProduct.Algebra.exists_of_fg z with ⟨R', fgR, ⟨y, hy⟩⟩ + rcases TensorProduct.Algebra.exists_of_fg ((TensorProduct.comm k _ _) y) with ⟨S', fgS, ⟨x, hx⟩⟩ + use R', S', fgR, fgS + rw [isReduced_iff, not_forall₂] + use (TensorProduct.comm k _ _) x + refine exists_prop.mpr ⟨?_, ?_⟩ + · use n + have hx' : (Algebra.TensorProduct.rTensor _ S'.val) x = + (Algebra.TensorProduct.comm k _ _) y := hx + have : x ^ n = 0 := by + rw [← map_eq_zero_iff (Algebra.TensorProduct.rTensor R' S'.val) + (Module.Flat.rTensor_preserves_injective_linearMap S'.val.toLinearMap + Subtype.val_injective), map_pow, hx', ← map_pow, + map_eq_zero_iff _ (AlgEquiv.injective _), ← map_eq_zero_iff + (Algebra.TensorProduct.rTensor S R'.val) (Module.Flat.rTensor_preserves_injective_linearMap + R'.val.toLinearMap Subtype.val_injective), map_pow, ← hn, ← hy] + rfl + rwa [← map_eq_zero_iff (Algebra.TensorProduct.comm k _ _) (AlgEquiv.injective _), map_pow] + at this + · rw [LinearEquiv.map_eq_zero_iff] + by_contra eq0 + rw [eq0, map_zero, eq_comm, LinearEquiv.map_eq_zero_iff] at hx + simp [hx, map_zero, eq_comm, hz_ne] at hy + lemma tensorProduct_of_isSeparablyGenerated {k : Type*} [Field k] {S : Type*} [CommRing S] [IsReduced S] [Algebra k S] {K : Type*} [Field K] [Algebra k K] : IsReduced (TensorProduct k K S) := by From 1654a9c23e5125e9e108984fb53e6dc5d1e475ad Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sun, 29 Mar 2026 11:01:11 +0800 Subject: [PATCH 06/30] fix def --- .../FieldTheory/TranscendentalSeparable.lean | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index f42a3f31a06ab6..39202c1e4355c3 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -17,20 +17,24 @@ public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis universe u v -variable (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A] - @[expose] public section open TensorProduct +section + +variable (k : Type u) (K : Type v) [Field k] [Field K] [Algebra k K] + class Algebra.IsSeparablyGenerated : Prop where - isSeparable' : ∃ (ι : Type v) (f : ι → A), - IsTranscendenceBasis R f ∧ - Algebra.IsSeparable (Algebra.adjoin R (Set.range f)) A + isSeparable' : ∃ (ι : Type v) (f : ι → K), + IsTranscendenceBasis k f ∧ + Algebra.IsSeparable (Algebra.adjoin k (Set.range f)) K class Algebra.IsTranscendentalSeparable : Prop where - forall_isSeparablyGenerated : ∀ (A' : Subalgebra R A), - Algebra.EssFiniteType R A' → Algebra.IsSeparablyGenerated R A' + forall_isSeparablyGenerated : ∀ (A' : IntermediateField k K), + Algebra.EssFiniteType k A' → Algebra.IsSeparablyGenerated k A' + +end set_option backward.isDefEq.respectTransparency false in /-- If `R ⊗[k] S` is nonreduced, then this already occurs on finitely generated `k`-subalgebras From 43d49ad4db063d4d2f30e9151161ad2f4c20533d Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sun, 29 Mar 2026 14:34:36 +0800 Subject: [PATCH 07/30] Update TranscendentalSeparable.lean --- .../FieldTheory/TranscendentalSeparable.lean | 42 +++++++++++++++++-- 1 file changed, 39 insertions(+), 3 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 39202c1e4355c3..ad22cb8324e0dc 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -10,6 +10,9 @@ public import Mathlib.RingTheory.TensorProduct.DirectLimitFG public import Mathlib.FieldTheory.Perfect public import Mathlib.FieldTheory.Separable public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis +public import Mathlib.RingTheory.Ideal.MinimalPrime.Basic +public import Mathlib.RingTheory.Localization.AtPrime.Basic +public import Mathlib.RingTheory.LocalProperties.Reduced /-! # Transcendental separable extensions @@ -36,6 +39,39 @@ class Algebra.IsTranscendentalSeparable : Prop where end +lemma localization_minimal_isField {S : Type*} [CommRing S] [IsReduced S] + (p : Ideal S) (min : p ∈ minimalPrimes S) : + letI := min.1.1 + IsField (Localization.AtPrime p) := by + let := min.1.1 + rw [IsLocalRing.isField_iff_maximalIdeal_eq, eq_bot_iff] + intro x hx + apply IsReduced.eq_zero x (nilpotent_iff_mem_prime.mpr (fun q hq ↦ ?_)) + convert hx + have : Ideal.comap (algebraMap S (Localization.AtPrime p)) q ≤ p := by + apply le_of_le_of_eq _ (IsLocalization.AtPrime.comap_maximalIdeal (Localization.AtPrime p) p) + exact Ideal.comap_mono (IsLocalRing.le_maximalIdeal_of_isPrime q) + rw [← Localization.AtPrime.eq_maximalIdeal_iff_comap_eq] + exact le_antisymm this (min.2 ⟨q.comap_isPrime _, bot_le⟩ this) + +def toLocalizationMinimal (S : Type*) [CommRing S] := + (Pi.ringHom (fun (p : minimalPrimes S) ↦ + letI := Ideal.minimalPrimes_isPrime p.2 + algebraMap S (Localization.AtPrime p.1))) + +lemma isReduced_injective_to_prod_localizations {S : Type*} [CommRing S] [IsReduced S] : + Function.Injective (toLocalizationMinimal S) := by + rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero] + intro x hx + apply IsReduced.eq_zero x (nilpotent_iff_mem_prime.mpr (fun q hq ↦ ?_)) + rcases Ideal.exists_minimalPrimes_le (bot_le (a := q)) with ⟨p, min, hp⟩ + let := min.1.1 + apply hp + rw [← IsLocalization.AtPrime.comap_maximalIdeal (Localization.AtPrime p) p, Ideal.mem_comap] + have : (toLocalizationMinimal S) x ⟨p, min⟩ = 0 := by simp [hx] + simp only [toLocalizationMinimal, Pi.ringHom_apply] at this + simp [this] + set_option backward.isDefEq.respectTransparency false in /-- If `R ⊗[k] S` is nonreduced, then this already occurs on finitely generated `k`-subalgebras of `R` and `S`. -/ @@ -68,9 +104,9 @@ lemma exists_subalgebra_fg_of_not_isReduced_tensorProduct rw [eq0, map_zero, eq_comm, LinearEquiv.map_eq_zero_iff] at hx simp [hx, map_zero, eq_comm, hz_ne] at hy -lemma tensorProduct_of_isSeparablyGenerated {k : Type*} [Field k] - {S : Type*} [CommRing S] [IsReduced S] [Algebra k S] {K : Type*} [Field K] [Algebra k K] : - IsReduced (TensorProduct k K S) := by +lemma tensorProduct_of_isTranscendentalSeparable_of_isReduced {k : Type*} [Field k] + {S : Type*} [CommRing S] [IsReduced S] [Algebra k S] {K : Type*} [Field K] [Algebra k K] + [Algebra.IsTranscendentalSeparable k K] : IsReduced (TensorProduct k K S) := by sorry lemma Algebra.isTranscendentalSeparable_of_perfectField {k : Type*} [Field k] [PerfectField k] From f69bdbd8ea962b9f5e69481978f6f3221d07fa2a Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sun, 29 Mar 2026 15:18:48 +0800 Subject: [PATCH 08/30] Update TranscendentalSeparable.lean --- Mathlib/FieldTheory/TranscendentalSeparable.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index ad22cb8324e0dc..f533098ff8cbfd 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -104,6 +104,11 @@ lemma exists_subalgebra_fg_of_not_isReduced_tensorProduct rw [eq0, map_zero, eq_comm, LinearEquiv.map_eq_zero_iff] at hx simp [hx, map_zero, eq_comm, hz_ne] at hy +lemma tensorProduct_of_isTranscendentalSeparable_of_isDomain {k : Type*} [Field k] + {S : Type*} [CommRing S] [IsDomain S] [Algebra k S] {K : Type*} [Field K] [Algebra k K] + [Algebra.IsTranscendentalSeparable k K] : IsReduced (TensorProduct k K S) := by + sorry + lemma tensorProduct_of_isTranscendentalSeparable_of_isReduced {k : Type*} [Field k] {S : Type*} [CommRing S] [IsReduced S] [Algebra k S] {K : Type*} [Field K] [Algebra k K] [Algebra.IsTranscendentalSeparable k K] : IsReduced (TensorProduct k K S) := by From 7a80074c680bbf48a71129283ad475275ea4501d Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 7 Apr 2026 17:19:03 +0800 Subject: [PATCH 09/30] Update TranscendentalSeparable.lean --- .../FieldTheory/TranscendentalSeparable.lean | 23 +++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index f533098ff8cbfd..87b4300377406e 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -104,14 +104,29 @@ lemma exists_subalgebra_fg_of_not_isReduced_tensorProduct rw [eq0, map_zero, eq_comm, LinearEquiv.map_eq_zero_iff] at hx simp [hx, map_zero, eq_comm, hz_ne] at hy +lemma IsReduced.tensorProduct_of_forall_fg_intermediateField {k : Type*} [Field k] + {S : Type*} [CommRing S] [Algebra k S] {K : Type*} [Field K] [Algebra k K] + (h : ∀ (L : IntermediateField k K), L.FG → IsReduced (TensorProduct k S L)) : + IsReduced (TensorProduct k S K) := by + refine IsReduced.tensorProduct_of_flat_of_forall_fg (fun B ⟨T, hT⟩ ↦ ?_) + have := h _ (IntermediateField.fg_adjoin_finset T) + have le : B ≤ (IntermediateField.adjoin k (T : Set K)).toSubalgebra := by + simp [← hT, Algebra.adjoin_le_iff] + have : Function.Injective (Algebra.TensorProduct.lTensor S (Subalgebra.inclusion le)) := + Module.Flat.lTensor_preserves_injective_linearMap (Subalgebra.inclusion le).toLinearMap + (Subalgebra.inclusion_injective le) + exact isReduced_of_injective _ this + lemma tensorProduct_of_isTranscendentalSeparable_of_isDomain {k : Type*} [Field k] - {S : Type*} [CommRing S] [IsDomain S] [Algebra k S] {K : Type*} [Field K] [Algebra k K] - [Algebra.IsTranscendentalSeparable k K] : IsReduced (TensorProduct k K S) := by + {S : Type*} [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsDomain S] + {K : Type*} [Field K] [Algebra k K] [Algebra.IsTranscendentalSeparable k K] + [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by sorry lemma tensorProduct_of_isTranscendentalSeparable_of_isReduced {k : Type*} [Field k] - {S : Type*} [CommRing S] [IsReduced S] [Algebra k S] {K : Type*} [Field K] [Algebra k K] - [Algebra.IsTranscendentalSeparable k K] : IsReduced (TensorProduct k K S) := by + {S : Type*} [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsReduced S] + {K : Type*} [Field K] [Algebra k K] [Algebra.IsTranscendentalSeparable k K] + [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by sorry lemma Algebra.isTranscendentalSeparable_of_perfectField {k : Type*} [Field k] [PerfectField k] From b4e9079c5cbabe6763ad12ff01394705ecec2951 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 7 Apr 2026 17:23:57 +0800 Subject: [PATCH 10/30] Update TranscendentalSeparable.lean --- Mathlib/FieldTheory/TranscendentalSeparable.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 87b4300377406e..f5ab151acf055b 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -117,18 +117,20 @@ lemma IsReduced.tensorProduct_of_forall_fg_intermediateField {k : Type*} [Field (Subalgebra.inclusion_injective le) exact isReduced_of_injective _ this -lemma tensorProduct_of_isTranscendentalSeparable_of_isDomain {k : Type*} [Field k] +variable {k : Type*} [Field k] + +lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain {S : Type*} [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsDomain S] {K : Type*} [Field K] [Algebra k K] [Algebra.IsTranscendentalSeparable k K] [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by sorry -lemma tensorProduct_of_isTranscendentalSeparable_of_isReduced {k : Type*} [Field k] +lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced {S : Type*} [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsReduced S] {K : Type*} [Field K] [Algebra k K] [Algebra.IsTranscendentalSeparable k K] [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by sorry -lemma Algebra.isTranscendentalSeparable_of_perfectField {k : Type*} [Field k] [PerfectField k] +lemma Algebra.isTranscendentalSeparable_of_perfectField [PerfectField k] {K : Type*} [Field K] [Algebra k K] : Algebra.IsTranscendentalSeparable k K := by sorry From ec4d38249a2a49850a350df7a54f963706689919 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 7 Apr 2026 18:24:27 +0800 Subject: [PATCH 11/30] Update TranscendentalSeparable.lean --- .../FieldTheory/TranscendentalSeparable.lean | 27 ++++++++++++++----- 1 file changed, 21 insertions(+), 6 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index f5ab151acf055b..99bd2d60254778 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -117,20 +117,35 @@ lemma IsReduced.tensorProduct_of_forall_fg_intermediateField {k : Type*} [Field (Subalgebra.inclusion_injective le) exact isReduced_of_injective _ this -variable {k : Type*} [Field k] +variable (k : Type*) [Field k] lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain - {S : Type*} [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsDomain S] - {K : Type*} [Field K] [Algebra k K] [Algebra.IsTranscendentalSeparable k K] + (S : Type*) [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsDomain S] + (K : Type*) [Field K] [Algebra k K] [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by sorry -lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced - {S : Type*} [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsReduced S] - {K : Type*} [Field K] [Algebra k K] [Algebra.IsTranscendentalSeparable k K] +lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFiniteType + (S : Type*) [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsReduced S] + (K : Type*) [Field K] [Algebra k K] [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by sorry +lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced + {S : Type*} [CommRing S] [Algebra k S] [IsReduced S] + {K : Type*} [Field K] [Algebra k K] [Algebra.IsTranscendentalSeparable k K] : + IsReduced (TensorProduct k K S) := by + refine IsReduced.tensorProduct_of_flat_of_forall_fg (fun B hB ↦ ?_) + have : Algebra.FiniteType k B := (Subalgebra.fg_iff_finiteType B).mp hB + have : IsReduced B := isReduced_of_injective B.val Subtype.val_injective + have : IsReduced (TensorProduct k B K) := by + refine IsReduced.tensorProduct_of_forall_fg_intermediateField (fun L hL ↦ ?_) + rw [← IntermediateField.essFiniteType_iff] at hL + have := Algebra.IsTranscendentalSeparable.forall_isSeparablyGenerated L hL + have := tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFiniteType k B L + exact isReduced_of_injective _ (Algebra.TensorProduct.comm k B L).injective + exact isReduced_of_injective _ (Algebra.TensorProduct.comm k K B).injective + lemma Algebra.isTranscendentalSeparable_of_perfectField [PerfectField k] {K : Type*} [Field K] [Algebra k K] : Algebra.IsTranscendentalSeparable k K := by sorry From 837631aa178cb2ebd61c00d30a08ee9e5b61bbbf Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 7 Apr 2026 18:40:54 +0800 Subject: [PATCH 12/30] remove unused lemma --- .../FieldTheory/TranscendentalSeparable.lean | 32 ------------------- 1 file changed, 32 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 99bd2d60254778..a29fb5363eba70 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -72,38 +72,6 @@ lemma isReduced_injective_to_prod_localizations {S : Type*} [CommRing S] [IsRedu simp only [toLocalizationMinimal, Pi.ringHom_apply] at this simp [this] -set_option backward.isDefEq.respectTransparency false in -/-- If `R ⊗[k] S` is nonreduced, then this already occurs on finitely generated `k`-subalgebras -of `R` and `S`. -/ -lemma exists_subalgebra_fg_of_not_isReduced_tensorProduct - (k R S : Type*) [Field k] [CommRing R] [CommRing S] [Algebra k R] [Algebra k S] - (h : ¬ IsReduced (R ⊗[k] S)) : - ∃ R' : Subalgebra k R, ∃ S' : Subalgebra k S, R'.FG ∧ S'.FG ∧ ¬ IsReduced (R' ⊗[k] S') := by - obtain ⟨z, hz_ne, ⟨n, hn⟩⟩ := exists_isNilpotent_of_not_isReduced h - rcases TensorProduct.Algebra.exists_of_fg z with ⟨R', fgR, ⟨y, hy⟩⟩ - rcases TensorProduct.Algebra.exists_of_fg ((TensorProduct.comm k _ _) y) with ⟨S', fgS, ⟨x, hx⟩⟩ - use R', S', fgR, fgS - rw [isReduced_iff, not_forall₂] - use (TensorProduct.comm k _ _) x - refine exists_prop.mpr ⟨?_, ?_⟩ - · use n - have hx' : (Algebra.TensorProduct.rTensor _ S'.val) x = - (Algebra.TensorProduct.comm k _ _) y := hx - have : x ^ n = 0 := by - rw [← map_eq_zero_iff (Algebra.TensorProduct.rTensor R' S'.val) - (Module.Flat.rTensor_preserves_injective_linearMap S'.val.toLinearMap - Subtype.val_injective), map_pow, hx', ← map_pow, - map_eq_zero_iff _ (AlgEquiv.injective _), ← map_eq_zero_iff - (Algebra.TensorProduct.rTensor S R'.val) (Module.Flat.rTensor_preserves_injective_linearMap - R'.val.toLinearMap Subtype.val_injective), map_pow, ← hn, ← hy] - rfl - rwa [← map_eq_zero_iff (Algebra.TensorProduct.comm k _ _) (AlgEquiv.injective _), map_pow] - at this - · rw [LinearEquiv.map_eq_zero_iff] - by_contra eq0 - rw [eq0, map_zero, eq_comm, LinearEquiv.map_eq_zero_iff] at hx - simp [hx, map_zero, eq_comm, hz_ne] at hy - lemma IsReduced.tensorProduct_of_forall_fg_intermediateField {k : Type*} [Field k] {S : Type*} [CommRing S] [Algebra k S] {K : Type*} [Field K] [Algebra k K] (h : ∀ (L : IntermediateField k K), L.FG → IsReduced (TensorProduct k S L)) : From 7a5d58fe43f049f275687e018c4d51cf1e3b2211 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Tue, 7 Apr 2026 19:21:54 +0800 Subject: [PATCH 13/30] Update TranscendentalSeparable.lean --- .../FieldTheory/TranscendentalSeparable.lean | 33 ++++++++++++++++--- 1 file changed, 28 insertions(+), 5 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index a29fb5363eba70..1197ec5191f5a6 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -13,6 +13,8 @@ public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis public import Mathlib.RingTheory.Ideal.MinimalPrime.Basic public import Mathlib.RingTheory.Localization.AtPrime.Basic public import Mathlib.RingTheory.LocalProperties.Reduced +public import Mathlib.RingTheory.TensorProduct.Pi +public import Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian /-! # Transcendental separable extensions @@ -59,7 +61,7 @@ def toLocalizationMinimal (S : Type*) [CommRing S] := letI := Ideal.minimalPrimes_isPrime p.2 algebraMap S (Localization.AtPrime p.1))) -lemma isReduced_injective_to_prod_localizations {S : Type*} [CommRing S] [IsReduced S] : +lemma isReduced_injective_to_prod_localizations (S : Type*) [CommRing S] [IsReduced S] : Function.Injective (toLocalizationMinimal S) := by rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero] intro x hx @@ -81,14 +83,13 @@ lemma IsReduced.tensorProduct_of_forall_fg_intermediateField {k : Type*} [Field have le : B ≤ (IntermediateField.adjoin k (T : Set K)).toSubalgebra := by simp [← hT, Algebra.adjoin_le_iff] have : Function.Injective (Algebra.TensorProduct.lTensor S (Subalgebra.inclusion le)) := - Module.Flat.lTensor_preserves_injective_linearMap (Subalgebra.inclusion le).toLinearMap - (Subalgebra.inclusion_injective le) + Module.Flat.lTensor_preserves_injective_linearMap _ (Subalgebra.inclusion_injective le) exact isReduced_of_injective _ this variable (k : Type*) [Field k] lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain - (S : Type*) [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsDomain S] + (S : Type*) [CommRing S] [Algebra k S] [IsDomain S] (K : Type*) [Field K] [Algebra k K] [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by sorry @@ -97,7 +98,29 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFi (S : Type*) [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsReduced S] (K : Type*) [Field K] [Algebra k K] [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by - sorry + classical + have : IsNoetherianRing S := Algebra.FiniteType.isNoetherianRing k S + have h (x : k) (y : S) : (toLocalizationMinimal S) (x • y) = x • (toLocalizationMinimal S) y := by + ext p + simp [toLocalizationMinimal, Algebra.smul_def, ← IsScalarTower.algebraMap_apply] + let f := AlgHom.mk' (toLocalizationMinimal S) h + have inj : Function.Injective (Algebra.TensorProduct.lTensor K f) := + Module.Flat.lTensor_preserves_injective_linearMap _ + (isReduced_injective_to_prod_localizations S) + let : Fintype (minimalPrimes S) := (minimalPrimes.finite_of_isNoetherianRing S).fintype + have (p : minimalPrimes S) : + letI := Ideal.minimalPrimes_isPrime p.2 + IsReduced (K ⊗[k] Localization.AtPrime p.1) := by + let := (localization_minimal_isField p.1 p.2).toField + exact tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain k _ K + have : IsReduced (K ⊗[k] ((p : (minimalPrimes S)) → + letI := Ideal.minimalPrimes_isPrime p.2 + Localization.AtPrime p.1)) := by + apply isReduced_of_injective _ (Algebra.TensorProduct.piRight k k K + (fun (p : (minimalPrimes S)) ↦ + letI := Ideal.minimalPrimes_isPrime p.2 + Localization.AtPrime p.1)).injective + exact isReduced_of_injective _ inj lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced {S : Type*} [CommRing S] [Algebra k S] [IsReduced S] From de4f43f925d06a7f416a80bb474a7539e935365e Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 9 Apr 2026 14:59:09 +0800 Subject: [PATCH 14/30] Update TranscendentalSeparable.lean --- .../FieldTheory/TranscendentalSeparable.lean | 29 ++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 1197ec5191f5a6..366045b2ebdbc8 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -15,6 +15,7 @@ public import Mathlib.RingTheory.Localization.AtPrime.Basic public import Mathlib.RingTheory.LocalProperties.Reduced public import Mathlib.RingTheory.TensorProduct.Pi public import Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian +public import Mathlib.FieldTheory.PrimitiveElement /-! # Transcendental separable extensions @@ -33,7 +34,7 @@ variable (k : Type u) (K : Type v) [Field k] [Field K] [Algebra k K] class Algebra.IsSeparablyGenerated : Prop where isSeparable' : ∃ (ι : Type v) (f : ι → K), IsTranscendenceBasis k f ∧ - Algebra.IsSeparable (Algebra.adjoin k (Set.range f)) K + Algebra.IsSeparable (IntermediateField.adjoin k (Set.range f)) K class Algebra.IsTranscendentalSeparable : Prop where forall_isSeparablyGenerated : ∀ (A' : IntermediateField k K), @@ -88,10 +89,36 @@ lemma IsReduced.tensorProduct_of_forall_fg_intermediateField {k : Type*} [Field variable (k : Type*) [Field k] +open IntermediateField.algebraAdjoinAdjoin in lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain (S : Type*) [CommRing S] [Algebra k S] [IsDomain S] (K : Type*) [Field K] [Algebra k K] [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by + classical + obtain ⟨ι, f, isT, sep⟩ : Algebra.IsSeparablyGenerated k K := ‹_› + set K' := IntermediateField.adjoin k (Set.range f) + have : Algebra.IsAlgebraic K' K := isT.isAlgebraic_field + have : Algebra.EssFiniteType K' K := Algebra.EssFiniteType.of_comp k K' K + have : FiniteDimensional K' K := Algebra.finite_of_essFiniteType_of_isAlgebraic + obtain ⟨y, hy⟩ := Field.exists_primitive_element K' K + let kx := Algebra.adjoin k (Set.range f) + let e : TensorProduct k kx S ≃ₐ[k] MvPolynomial ι S := + (Algebra.TensorProduct.congr (AlgebraicIndependent.aevalEquiv isT.1).symm AlgEquiv.refl).trans + MvPolynomial.scalarRTensorAlgEquiv + have isd1 : IsDomain (TensorProduct k kx S) := e.injective.isDomain + let nz := nonZeroDivisors kx + have : IsLocalization nz K' := inferInstanceAs (IsFractionRing _ K') + have isl := IsLocalization.tensorRight K' nz (S := TensorProduct k kx S) + let : Algebra (kx ⊗[k] S) (K' ⊗[kx] (kx ⊗[k] S)) := Algebra.TensorProduct.rightAlgebra + have le_nz : nz.map (algebraMap kx (kx ⊗[k] S)) ≤ nonZeroDivisors (↥kx ⊗[k] S) := by + rw [Submonoid.map_le_iff_le_comap] + intro x + simp only [mem_nonZeroDivisors_iff_ne_zero, ne_eq, Submonoid.mem_comap, nz] + exact fun hx ↦ (map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective kx (kx ⊗[k] S))).mpr hx + have isd2 := @IsLocalization.isDomain_of_le_nonZeroDivisors _ _ _ _ _ _ isl isd1 le_nz + have isd3 : IsDomain (K' ⊗[k] S) := + (Algebra.TensorProduct.cancelBaseChange k kx kx K' S).symm.injective.isDomain + sorry lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFiniteType From b4a283cf8de34a2159a48df6fe03c793d6ff49a2 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 9 Apr 2026 17:17:15 +0800 Subject: [PATCH 15/30] Update TranscendentalSeparable.lean --- .../FieldTheory/TranscendentalSeparable.lean | 69 ++++++++++++++++--- 1 file changed, 60 insertions(+), 9 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 366045b2ebdbc8..9d4bdb7ba32b8f 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -87,13 +87,55 @@ lemma IsReduced.tensorProduct_of_forall_fg_intermediateField {k : Type*} [Field Module.Flat.lTensor_preserves_injective_linearMap _ (Subalgebra.inclusion_injective le) exact isReduced_of_injective _ this -variable (k : Type*) [Field k] +variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] (S : Type*) [CommRing S] + +open scoped Polynomial + +lemma isReduced_of_quotient_separable [IsDomain S] (f : S[X]) + (sep : f.Separable) : IsReduced (S[X] ⧸ Ideal.span {f}) := by + sorry + +noncomputable def polynomialTensorProductEquiv [Algebra k S] : K[X] ⊗[k] S ≃ₐ[K] (K ⊗[k] S)[X] := + ((((Algebra.TensorProduct.congr (polyEquivTensor' k K) AlgEquiv.refl).trans + (Algebra.TensorProduct.assoc k k K K k[X] S)).trans + (Algebra.TensorProduct.congr AlgEquiv.refl (Algebra.TensorProduct.comm k k[X] S))).trans + (Algebra.TensorProduct.assoc k k K K S k[X]).symm).trans + ((polyEquivTensor' k (K ⊗[k] S)).symm.restrictScalars K) + +lemma polynomialTensorProductEquiv_map_algebraMap [Algebra k S] (f : K[X]) : + f.map (algebraMap K (K ⊗[k] S)) = + (polynomialTensorProductEquiv k K S) ((algebraMap K[X] (K[X] ⊗[k] S)) f) := by + obtain ⟨g, rfl⟩ := (polyEquivTensor' k K).symm.surjective f + induction g with + | zero => simp + | add g1 g2 hg1 hg2 => simp only [map_add, Polynomial.map_add, hg1, hg2] + | tmul x y => + have : Polynomial.map (algebraMap K (K ⊗[k] S)) ((polyEquivTensor k K).symm (x ⊗ₜ[k] y)) = + (polyEquivTensor k (K ⊗[k] S)).symm (x ⊗ₜ[k] 1 ⊗ₜ[k] y) := by + simp [Polynomial.map_map, ← IsScalarTower.algebraMap_eq] + simpa [- polyEquivTensor_symm_apply_tmul_eq_smul, polynomialTensorProductEquiv] + +noncomputable def quotientPolynomialTensorProductEquiv (f : K[X]) [Algebra k S] : + (K[X] ⧸ Ideal.span {f}) ⊗[k] S ≃ₐ[K] + (K ⊗[k] S)[X] ⧸ Ideal.span {f.map (algebraMap K (K ⊗[k] S))} := + let : IsScalarTower K (K[X] ⧸ Ideal.span {f}) + (K[X] ⊗[k] S ⧸ Ideal.map (algebraMap K[X] (K[X] ⊗[k] S)) (Ideal.span {f})) := + IsScalarTower.of_algebraMap_eq' rfl + let e : (K[X] ⧸ Ideal.span {f}) ⊗[K[X]] (K[X] ⊗[k] S) ≃ₐ[K] + (K[X] ⊗[k] S) ⧸ ((Ideal.span {f}).map (algebraMap K[X] (K[X] ⊗[k] S))) := + (Algebra.TensorProduct.quotIdealMapEquivQuotTensor _ _).symm.restrictScalars K + (((Algebra.TensorProduct.cancelBaseChange k K[X] K[X] (K[X] ⧸ Ideal.span {f}) + S).symm.restrictScalars K).trans + ((Algebra.TensorProduct.quotIdealMapEquivQuotTensor _ _).symm.restrictScalars K)).trans + (Ideal.quotientEquivAlg _ _ (polynomialTensorProductEquiv k K S) (by + simp only [Ideal.map_span, Set.image_singleton, RingHom.coe_coe, + polynomialTensorProductEquiv_map_algebraMap])) open IntermediateField.algebraAdjoinAdjoin in lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain (S : Type*) [CommRing S] [Algebra k S] [IsDomain S] - (K : Type*) [Field K] [Algebra k K] [Algebra.IsSeparablyGenerated k K] - [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by + [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : + IsReduced (TensorProduct k K S) := by classical obtain ⟨ι, f, isT, sep⟩ : Algebra.IsSeparablyGenerated k K := ‹_› set K' := IntermediateField.adjoin k (Set.range f) @@ -118,13 +160,22 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain have isd2 := @IsLocalization.isDomain_of_le_nonZeroDivisors _ _ _ _ _ _ isl isd1 le_nz have isd3 : IsDomain (K' ⊗[k] S) := (Algebra.TensorProduct.cancelBaseChange k kx kx K' S).symm.injective.isDomain - - sorry + let f := minpoly K' y + have fsep : f.Separable := sep.1 y + let eK : K ≃ₐ[K'] K'[X] ⧸ Ideal.span {f} := + (IntermediateField.topEquiv.symm.trans (IntermediateField.equivOfEq hy).symm).trans + (IntermediateField.adjoinRootEquivAdjoin K' (Algebra.IsIntegral.isIntegral y)).symm + let eTen : K ⊗[k] S ≃ₐ[K'] (K' ⊗[k] S)[X] ⧸ Ideal.span {f.map (algebraMap K' (K' ⊗[k] S))} := + (Algebra.TensorProduct.congr eK AlgEquiv.refl).trans + (quotientPolynomialTensorProductEquiv k K' S f) + have red : IsReduced ((K' ⊗[k] S)[X] ⧸ Ideal.span {f.map (algebraMap K' (K' ⊗[k] S))}) := + isReduced_of_quotient_separable _ _ fsep.map + exact isReduced_of_injective _ eTen.injective lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFiniteType (S : Type*) [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsReduced S] - (K : Type*) [Field K] [Algebra k K] [Algebra.IsSeparablyGenerated k K] - [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by + [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : + IsReduced (TensorProduct k K S) := by classical have : IsNoetherianRing S := Algebra.FiniteType.isNoetherianRing k S have h (x : k) (y : S) : (toLocalizationMinimal S) (x • y) = x • (toLocalizationMinimal S) y := by @@ -139,7 +190,7 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFi letI := Ideal.minimalPrimes_isPrime p.2 IsReduced (K ⊗[k] Localization.AtPrime p.1) := by let := (localization_minimal_isField p.1 p.2).toField - exact tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain k _ K + exact tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain k K _ have : IsReduced (K ⊗[k] ((p : (minimalPrimes S)) → letI := Ideal.minimalPrimes_isPrime p.2 Localization.AtPrime p.1)) := by @@ -160,7 +211,7 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced refine IsReduced.tensorProduct_of_forall_fg_intermediateField (fun L hL ↦ ?_) rw [← IntermediateField.essFiniteType_iff] at hL have := Algebra.IsTranscendentalSeparable.forall_isSeparablyGenerated L hL - have := tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFiniteType k B L + have := tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFiniteType k L B exact isReduced_of_injective _ (Algebra.TensorProduct.comm k B L).injective exact isReduced_of_injective _ (Algebra.TensorProduct.comm k K B).injective From 570e712f34ba8a1f0271d81de79a0e769cdf768b Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 9 Apr 2026 17:23:45 +0800 Subject: [PATCH 16/30] fix --- Mathlib/FieldTheory/TranscendentalSeparable.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 9d4bdb7ba32b8f..6ceddf6d630903 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -91,7 +91,7 @@ variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] (S : Type*) [ open scoped Polynomial -lemma isReduced_of_quotient_separable [IsDomain S] (f : S[X]) +lemma isReduced_of_quotient_separable [IsDomain S] (f : S[X]) (mon : f.Monic) (sep : f.Separable) : IsReduced (S[X] ⧸ Ideal.span {f}) := by sorry @@ -162,6 +162,7 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain (Algebra.TensorProduct.cancelBaseChange k kx kx K' S).symm.injective.isDomain let f := minpoly K' y have fsep : f.Separable := sep.1 y + have fmon : f.Monic := minpoly.monic (Algebra.IsIntegral.isIntegral y) let eK : K ≃ₐ[K'] K'[X] ⧸ Ideal.span {f} := (IntermediateField.topEquiv.symm.trans (IntermediateField.equivOfEq hy).symm).trans (IntermediateField.adjoinRootEquivAdjoin K' (Algebra.IsIntegral.isIntegral y)).symm @@ -169,7 +170,7 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain (Algebra.TensorProduct.congr eK AlgEquiv.refl).trans (quotientPolynomialTensorProductEquiv k K' S f) have red : IsReduced ((K' ⊗[k] S)[X] ⧸ Ideal.span {f.map (algebraMap K' (K' ⊗[k] S))}) := - isReduced_of_quotient_separable _ _ fsep.map + isReduced_of_quotient_separable _ _ (fmon.map _) fsep.map exact isReduced_of_injective _ eTen.injective lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFiniteType From 2930e53a5634d96f6022edf0b0f458d2f96f025f Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 9 Apr 2026 19:38:24 +0800 Subject: [PATCH 17/30] finish 10.43.6 --- .../FieldTheory/TranscendentalSeparable.lean | 48 ++++++++++++++++++- 1 file changed, 46 insertions(+), 2 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 6ceddf6d630903..051bb3dd20a1a3 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -87,13 +87,55 @@ lemma IsReduced.tensorProduct_of_forall_fg_intermediateField {k : Type*} [Field Module.Flat.lTensor_preserves_injective_linearMap _ (Subalgebra.inclusion_injective le) exact isReduced_of_injective _ this -variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] (S : Type*) [CommRing S] +variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] open scoped Polynomial +lemma isReduced_of_quotient_separable_of_field (S : Type*) [Field S] (f : S[X]) + (sep : f.Separable) : IsReduced (S[X] ⧸ Ideal.span {f}) := by + generalize deg : f.natDegree = n + induction n using Nat.case_strong_induction_on generalizing f with + | hz => + rcases Polynomial.natDegree_eq_zero.mp deg with ⟨s, rfl⟩ + by_cases eq0 : s = 0 + · have : (Ideal.span {Polynomial.C s}).IsPrime := by simpa [eq0] using Ideal.isPrime_bot + infer_instance + · have : Subsingleton (S[X] ⧸ Ideal.span {Polynomial.C s}) := by simp [eq0] + infer_instance + | hi n ih => + have nu : ¬IsUnit f := Polynomial.not_isUnit_of_natDegree_pos f (by simp [deg]) + have ne0 : f ≠ 0 := Polynomial.Separable.ne_zero sep + rcases WfDvdMonoid.exists_irreducible_factor nu ne0 with ⟨p, irr, ⟨g, rfl⟩⟩ + rw [← Ideal.span_singleton_mul_span_singleton] + have cop : IsCoprime (Ideal.span {p}) (Ideal.span {g}) := by + rw [Ideal.isCoprime_span_singleton_iff, Irreducible.coprime_iff_not_dvd irr] + by_contra ⟨h, rfl⟩ + absurd sep.squarefree + simp only [Squarefree, not_forall] + use p + simp [← mul_assoc, irr.not_isUnit] + have red1 : (Ideal.span {p}).IsPrime := (Ideal.span_singleton_prime irr.ne_zero).mpr irr.prime + have red2 : IsReduced (S[X] ⧸ Ideal.span {g}) := by + have : p.natDegree > 0 := Irreducible.natDegree_pos irr + have := deg.symm.trans (Polynomial.natDegree_mul irr.ne_zero (right_ne_zero_of_mul ne0)) + exact ih g.natDegree (by linarith) g sep.of_mul_right rfl + exact isReduced_of_injective _ (Ideal.quotientMulEquivQuotientProd _ _ cop).injective + +variable (S : Type*) [CommRing S] + lemma isReduced_of_quotient_separable [IsDomain S] (f : S[X]) (mon : f.Monic) (sep : f.Separable) : IsReduced (S[X] ⧸ Ideal.span {f}) := by - sorry + let iS := (algebraMap S (FractionRing S)) + have eq : (Ideal.span {f.map iS}).comap (Polynomial.mapRingHom iS) = Ideal.span {f} := by + ext g + simpa [Ideal.map_span, Ideal.mem_span_singleton] using + Polynomial.map_dvd_map iS (FaithfulSMul.algebraMap_injective _ _) mon + let iQ : (S[X] ⧸ Ideal.span {f}) →+* ((FractionRing S)[X] ⧸ Ideal.span {f.map iS}) := + Ideal.Quotient.lift _ ((Ideal.Quotient.mk _).comp (Polynomial.mapRingHom iS)) (fun x hx ↦ by + simpa [Ideal.Quotient.eq_zero_iff_mem] using le_of_eq eq.symm hx) + have := isReduced_of_quotient_separable_of_field _ (f.map iS) sep.map + apply isReduced_of_injective iQ ((Ideal.injective_lift_iff _).mpr _) + simp [← RingHom.comap_ker, eq] noncomputable def polynomialTensorProductEquiv [Algebra k S] : K[X] ⊗[k] S ≃ₐ[K] (K ⊗[k] S)[X] := ((((Algebra.TensorProduct.congr (polyEquivTensor' k K) AlgEquiv.refl).trans @@ -216,6 +258,8 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced exact isReduced_of_injective _ (Algebra.TensorProduct.comm k B L).injective exact isReduced_of_injective _ (Algebra.TensorProduct.comm k K B).injective +/- lemma Algebra.isTranscendentalSeparable_of_perfectField [PerfectField k] {K : Type*} [Field K] [Algebra k K] : Algebra.IsTranscendentalSeparable k K := by sorry +-/ From 5f0fbbe61ab9694c2160f033cd667ec448d4a85d Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 9 Apr 2026 19:56:23 +0800 Subject: [PATCH 18/30] golf for generalization --- .../FieldTheory/TranscendentalSeparable.lean | 25 ++++++++++++------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 051bb3dd20a1a3..fe6898573865f4 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -87,7 +87,7 @@ lemma IsReduced.tensorProduct_of_forall_fg_intermediateField {k : Type*} [Field Module.Flat.lTensor_preserves_injective_linearMap _ (Subalgebra.inclusion_injective le) exact isReduced_of_injective _ this -variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] +variable (k : Type u) [Field k] (K : Type v) [Field K] [Algebra k K] open scoped Polynomial @@ -163,9 +163,6 @@ noncomputable def quotientPolynomialTensorProductEquiv (f : K[X]) [Algebra k S] let : IsScalarTower K (K[X] ⧸ Ideal.span {f}) (K[X] ⊗[k] S ⧸ Ideal.map (algebraMap K[X] (K[X] ⊗[k] S)) (Ideal.span {f})) := IsScalarTower.of_algebraMap_eq' rfl - let e : (K[X] ⧸ Ideal.span {f}) ⊗[K[X]] (K[X] ⊗[k] S) ≃ₐ[K] - (K[X] ⊗[k] S) ⧸ ((Ideal.span {f}).map (algebraMap K[X] (K[X] ⊗[k] S))) := - (Algebra.TensorProduct.quotIdealMapEquivQuotTensor _ _).symm.restrictScalars K (((Algebra.TensorProduct.cancelBaseChange k K[X] K[X] (K[X] ⧸ Ideal.span {f}) S).symm.restrictScalars K).trans ((Algebra.TensorProduct.quotIdealMapEquivQuotTensor _ _).symm.restrictScalars K)).trans @@ -174,15 +171,15 @@ noncomputable def quotientPolynomialTensorProductEquiv (f : K[X]) [Algebra k S] polynomialTensorProductEquiv_map_algebraMap])) open IntermediateField.algebraAdjoinAdjoin in -lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain - (S : Type*) [CommRing S] [Algebra k S] [IsDomain S] - [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : +lemma tensorProduct_isReduced_of_isTranscendentalBasis_of_isSeparable_of_essFiniteType + [Algebra k S] [IsDomain S] + {ι : Type v} (f : ι → K) (isT : IsTranscendenceBasis k f) + [sep : Algebra.IsSeparable (IntermediateField.adjoin k (Set.range f)) K] + [Algebra.EssFiniteType (IntermediateField.adjoin k (Set.range f)) K] : IsReduced (TensorProduct k K S) := by classical - obtain ⟨ι, f, isT, sep⟩ : Algebra.IsSeparablyGenerated k K := ‹_› set K' := IntermediateField.adjoin k (Set.range f) have : Algebra.IsAlgebraic K' K := isT.isAlgebraic_field - have : Algebra.EssFiniteType K' K := Algebra.EssFiniteType.of_comp k K' K have : FiniteDimensional K' K := Algebra.finite_of_essFiniteType_of_isAlgebraic obtain ⟨y, hy⟩ := Field.exists_primitive_element K' K let kx := Algebra.adjoin k (Set.range f) @@ -215,6 +212,16 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain isReduced_of_quotient_separable _ _ (fmon.map _) fsep.map exact isReduced_of_injective _ eTen.injective +open IntermediateField.algebraAdjoinAdjoin in +lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain + (S : Type*) [CommRing S] [Algebra k S] [IsDomain S] + [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : + IsReduced (TensorProduct k K S) := by + classical + obtain ⟨ι, f, isT, sep⟩ : Algebra.IsSeparablyGenerated k K := ‹_› + have := Algebra.EssFiniteType.of_comp k (IntermediateField.adjoin k (Set.range f)) K + exact tensorProduct_isReduced_of_isTranscendentalBasis_of_isSeparable_of_essFiniteType k K S f isT + lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFiniteType (S : Type*) [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsReduced S] [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : From b51131cdd0ee1c7d65b70ccf1532d03329298408 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Thu, 9 Apr 2026 20:04:42 +0800 Subject: [PATCH 19/30] golf for generalization --- .../FieldTheory/TranscendentalSeparable.lean | 33 ++++++++++++------- 1 file changed, 21 insertions(+), 12 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index fe6898573865f4..6848fa046ea4e5 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -171,9 +171,8 @@ noncomputable def quotientPolynomialTensorProductEquiv (f : K[X]) [Algebra k S] polynomialTensorProductEquiv_map_algebraMap])) open IntermediateField.algebraAdjoinAdjoin in -lemma tensorProduct_isReduced_of_isTranscendentalBasis_of_isSeparable_of_essFiniteType - [Algebra k S] [IsDomain S] - {ι : Type v} (f : ι → K) (isT : IsTranscendenceBasis k f) +lemma tensorProduct_isReduced_of_isTranscendentalBasis_of_isDomain + [Algebra k S] [IsDomain S] {ι : Type v} (f : ι → K) (isT : IsTranscendenceBasis k f) [sep : Algebra.IsSeparable (IntermediateField.adjoin k (Set.range f)) K] [Algebra.EssFiniteType (IntermediateField.adjoin k (Set.range f)) K] : IsReduced (TensorProduct k K S) := by @@ -213,26 +212,27 @@ lemma tensorProduct_isReduced_of_isTranscendentalBasis_of_isSeparable_of_essFini exact isReduced_of_injective _ eTen.injective open IntermediateField.algebraAdjoinAdjoin in -lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain +lemma tensorProduct_isReduced_of_isSeparablyGenerated_isDomain (S : Type*) [CommRing S] [Algebra k S] [IsDomain S] [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by - classical obtain ⟨ι, f, isT, sep⟩ : Algebra.IsSeparablyGenerated k K := ‹_› have := Algebra.EssFiniteType.of_comp k (IntermediateField.adjoin k (Set.range f)) K - exact tensorProduct_isReduced_of_isTranscendentalBasis_of_isSeparable_of_essFiniteType k K S f isT + exact tensorProduct_isReduced_of_isTranscendentalBasis_of_isDomain k K S f isT -lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFiniteType - (S : Type*) [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsReduced S] - [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : +lemma tensorProduct_isReduced_of_isTranscendentalBasis_of_isReduced + [Algebra k S] [IsReduced S] [Algebra.FiniteType k S] + {ι : Type v} (f : ι → K) (isT : IsTranscendenceBasis k f) + [sep : Algebra.IsSeparable (IntermediateField.adjoin k (Set.range f)) K] + [Algebra.EssFiniteType (IntermediateField.adjoin k (Set.range f)) K] : IsReduced (TensorProduct k K S) := by classical have : IsNoetherianRing S := Algebra.FiniteType.isNoetherianRing k S have h (x : k) (y : S) : (toLocalizationMinimal S) (x • y) = x • (toLocalizationMinimal S) y := by ext p simp [toLocalizationMinimal, Algebra.smul_def, ← IsScalarTower.algebraMap_apply] - let f := AlgHom.mk' (toLocalizationMinimal S) h - have inj : Function.Injective (Algebra.TensorProduct.lTensor K f) := + let g := AlgHom.mk' (toLocalizationMinimal S) h + have inj : Function.Injective (Algebra.TensorProduct.lTensor K g) := Module.Flat.lTensor_preserves_injective_linearMap _ (isReduced_injective_to_prod_localizations S) let : Fintype (minimalPrimes S) := (minimalPrimes.finite_of_isNoetherianRing S).fintype @@ -240,7 +240,7 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFi letI := Ideal.minimalPrimes_isPrime p.2 IsReduced (K ⊗[k] Localization.AtPrime p.1) := by let := (localization_minimal_isField p.1 p.2).toField - exact tensorProduct_isReduced_of_isTranscendentalSeparable_of_isDomain k K _ + exact tensorProduct_isReduced_of_isTranscendentalBasis_of_isDomain k K _ f isT have : IsReduced (K ⊗[k] ((p : (minimalPrimes S)) → letI := Ideal.minimalPrimes_isPrime p.2 Localization.AtPrime p.1)) := by @@ -250,6 +250,15 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFi Localization.AtPrime p.1)).injective exact isReduced_of_injective _ inj +lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFiniteType + (S : Type*) [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsReduced S] + [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : + IsReduced (TensorProduct k K S) := by + classical + obtain ⟨ι, f, isT, sep⟩ : Algebra.IsSeparablyGenerated k K := ‹_› + have := Algebra.EssFiniteType.of_comp k (IntermediateField.adjoin k (Set.range f)) K + exact tensorProduct_isReduced_of_isTranscendentalBasis_of_isReduced k K S f isT + lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced {S : Type*} [CommRing S] [Algebra k S] [IsReduced S] {K : Type*} [Field K] [Algebra k K] [Algebra.IsTranscendentalSeparable k K] : From d1fdacf96b04eb2c006dcaea6a73433b794d6fb1 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 10 Apr 2026 17:27:46 +0800 Subject: [PATCH 20/30] Update TranscendentalSeparable.lean --- .../FieldTheory/TranscendentalSeparable.lean | 75 ++++++++++++++++++- 1 file changed, 72 insertions(+), 3 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 6848fa046ea4e5..fab4c7bf8d804e 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -16,6 +16,8 @@ public import Mathlib.RingTheory.LocalProperties.Reduced public import Mathlib.RingTheory.TensorProduct.Pi public import Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian public import Mathlib.FieldTheory.PrimitiveElement +public import Mathlib.RingTheory.Nilpotent.GeometricallyReduced +public import Mathlib.FieldTheory.SeparablyGenerated /-! # Transcendental separable extensions @@ -31,11 +33,13 @@ section variable (k : Type u) (K : Type v) [Field k] [Field K] [Algebra k K] +@[mk_iff] class Algebra.IsSeparablyGenerated : Prop where isSeparable' : ∃ (ι : Type v) (f : ι → K), IsTranscendenceBasis k f ∧ Algebra.IsSeparable (IntermediateField.adjoin k (Set.range f)) K +@[mk_iff] class Algebra.IsTranscendentalSeparable : Prop where forall_isSeparablyGenerated : ∀ (A' : IntermediateField k K), Algebra.EssFiniteType k A' → Algebra.IsSeparablyGenerated k A' @@ -259,9 +263,8 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFi have := Algebra.EssFiniteType.of_comp k (IntermediateField.adjoin k (Set.range f)) K exact tensorProduct_isReduced_of_isTranscendentalBasis_of_isReduced k K S f isT -lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced - {S : Type*} [CommRing S] [Algebra k S] [IsReduced S] - {K : Type*} [Field K] [Algebra k K] [Algebra.IsTranscendentalSeparable k K] : +lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced [Algebra k S] [IsReduced S] + (K : Type*) [Field K] [Algebra k K] [Algebra.IsTranscendentalSeparable k K] : IsReduced (TensorProduct k K S) := by refine IsReduced.tensorProduct_of_flat_of_forall_fg (fun B hB ↦ ?_) have : Algebra.FiniteType k B := (Subalgebra.fg_iff_finiteType B).mp hB @@ -274,6 +277,72 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced exact isReduced_of_injective _ (Algebra.TensorProduct.comm k B L).injective exact isReduced_of_injective _ (Algebra.TensorProduct.comm k K B).injective +variable (p : ℕ) [ExpChar k p] + +instance : ExpChar (AlgebraicClosure k) p := ExpChar.of_injective_algebraMap' k _ + +/- +def adjoinPthRoots : IntermediateField k (AlgebraicClosure k) where + carrier := {x | x ^ p ∈ (⊥ : IntermediateField k _)} + mul_mem' {a b} ha hb := by simpa [mul_pow] using mul_mem ha hb + one_mem' := by simp + add_mem' {a b} ha hb := by simpa [add_pow_expChar a b p] using add_mem ha hb + zero_mem' := by simp [zero_pow hp.ne_zero] + algebraMap_mem' x := pow_mem ((⊥ : IntermediateField k _).algebraMap_mem x) p + inv_mem' {a} ha := by simpa +-/ + +def adjoinPthRoots (p : ℕ) [ExpChar k p] := k + +instance : Field (adjoinPthRoots k p) := inferInstanceAs (Field k) + +instance : Algebra k (adjoinPthRoots k p) := (frobenius k p).toAlgebra + +lemma Algebra.isTranscendentalSeparable_tfae (hp : Nat.Prime p) : + [ Algebra.IsTranscendentalSeparable k K, + ∀ s : Finset K, + LinearIndepOn k _root_.id (s : Set K) → LinearIndepOn k (· ^ p) (s : Set K), + IsReduced (TensorProduct k (adjoinPthRoots k p) K), + Algebra.IsGeometricallyReduced k K].TFAE := by + tfae_have 1 → 4 := by + intro sep + have := tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced + k (AlgebraicClosure k) K + apply (Algebra.isGeometricallyReduced_iff k K).mpr + exact isReduced_of_injective _ (Algebra.TensorProduct.comm k _ K).injective + tfae_have 4 → 3 := by + /- + simp only [isGeometricallyReduced_iff] + intro red + have : Function.Injective (Algebra.TensorProduct.rTensor K (adjoinPthRoots k p).val) := + Module.Flat.rTensor_preserves_injective_linearMap _ Subtype.val_injective + exact isReduced_of_injective _ this + -/ + sorry + tfae_have 3 → 2 := by + --only one missing + sorry + tfae_have 2 → 1 := by + simp only [Algebra.isTranscendentalSeparable_iff, Algebra.isSeparablyGenerated_iff] + intro h L hL + classical + have h' (s : Finset L) : LinearIndepOn k _root_.id (s : Set L) → + LinearIndepOn k (fun x ↦ x ^ p) (s : Set L) := by + intro li + have li' := h (s.image L.val) (by + simpa using (li.map_injOn L.val.toLinearMap Subtype.val_injective.injOn).id_image) + simp only [IntermediateField.coe_val, Finset.coe_image] at li' + have li'' := li'.comp_of_image Subtype.val_injective.injOn + have : (fun x ↦ x ^ p) ∘ Subtype.val = L.val.toLinearMap ∘ (fun x ↦ x ^ p) := rfl + rw [this] at li'' + exact li''.of_comp + rcases exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType p hp h' + with ⟨T, isT, sep⟩ + use T, Subtype.val, isT + convert sep + <;> simp + tfae_finish + /- lemma Algebra.isTranscendentalSeparable_of_perfectField [PerfectField k] {K : Type*} [Field K] [Algebra k K] : Algebra.IsTranscendentalSeparable k K := by From 4fca9d00670207a7311a969eea83c91a4a71936e Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 10 Apr 2026 19:32:43 +0800 Subject: [PATCH 21/30] refactor API --- .../FieldTheory/TranscendentalSeparable.lean | 41 +++++++++++++++---- 1 file changed, 32 insertions(+), 9 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index fab4c7bf8d804e..901a228bee2577 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -277,10 +277,6 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced [Algebra exact isReduced_of_injective _ (Algebra.TensorProduct.comm k B L).injective exact isReduced_of_injective _ (Algebra.TensorProduct.comm k K B).injective -variable (p : ℕ) [ExpChar k p] - -instance : ExpChar (AlgebraicClosure k) p := ExpChar.of_injective_algebraMap' k _ - /- def adjoinPthRoots : IntermediateField k (AlgebraicClosure k) where carrier := {x | x ^ p ∈ (⊥ : IntermediateField k _)} @@ -294,10 +290,36 @@ def adjoinPthRoots : IntermediateField k (AlgebraicClosure k) where def adjoinPthRoots (p : ℕ) [ExpChar k p] := k +variable (p : ℕ) [ExpChar k p] + instance : Field (adjoinPthRoots k p) := inferInstanceAs (Field k) instance : Algebra k (adjoinPthRoots k p) := (frobenius k p).toAlgebra +def adjoinPthRootsSelf : (adjoinPthRoots k p) →+* k := RingHom.id k + +lemma adjoinPthRootsSelf_algebraMap (x : adjoinPthRoots k p) : + algebraMap k (adjoinPthRoots k p) (adjoinPthRootsSelf k p x) = x ^ p := rfl + +lemma adjoinPthRoots_pth_power_mem_bot (x : adjoinPthRoots k p) : + x ^ p ∈ (⊥ : IntermediateField k (adjoinPthRoots k p)) := by + use adjoinPthRootsSelf k p x + rfl + +set_option backward.isDefEq.respectTransparency false in +instance [Fact (Nat.Prime p)] : Algebra.IsAlgebraic k (adjoinPthRoots k p) where + isAlgebraic x := by + use Polynomial.X ^ p - Polynomial.C (adjoinPthRootsSelf k p x) + refine ⟨(Polynomial.monic_X_pow_sub_C _ (NeZero.ne' p).symm).ne_zero, ?_⟩ + simp [adjoinPthRootsSelf_algebraMap] + +def adjoinPthRootsPthRoot : k →+* (adjoinPthRoots k p) := RingHom.id k + +lemma adjoinPthRootsPthRoot_pow (x : k) : algebraMap k (adjoinPthRoots k p) x = + (adjoinPthRootsPthRoot k p x) ^ p := rfl + +instance : ExpChar (AlgebraicClosure k) p := ExpChar.of_injective_algebraMap' k _ + lemma Algebra.isTranscendentalSeparable_tfae (hp : Nat.Prime p) : [ Algebra.IsTranscendentalSeparable k K, ∀ s : Finset K, @@ -311,14 +333,15 @@ lemma Algebra.isTranscendentalSeparable_tfae (hp : Nat.Prime p) : apply (Algebra.isGeometricallyReduced_iff k K).mpr exact isReduced_of_injective _ (Algebra.TensorProduct.comm k _ K).injective tfae_have 4 → 3 := by - /- + let : Fact (Nat.Prime p) := ⟨hp⟩ simp only [isGeometricallyReduced_iff] intro red - have : Function.Injective (Algebra.TensorProduct.rTensor K (adjoinPthRoots k p).val) := - Module.Flat.rTensor_preserves_injective_linearMap _ Subtype.val_injective + let f : (adjoinPthRoots k p) →ₐ[k] (AlgebraicClosure k) := + (IsAlgClosure.equiv k (AlgebraicClosure (adjoinPthRoots k p)) + (AlgebraicClosure k)).toAlgHom.comp (IsScalarTower.toAlgHom k (adjoinPthRoots k p) _) + have : Function.Injective (Algebra.TensorProduct.rTensor K f) := + Module.Flat.rTensor_preserves_injective_linearMap _ (RingHom.injective _) exact isReduced_of_injective _ this - -/ - sorry tfae_have 3 → 2 := by --only one missing sorry From 34a2c5488554a04183957d98eee2a8a3ac888da1 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Fri, 10 Apr 2026 21:04:34 +0800 Subject: [PATCH 22/30] finish 10.44.2 --- .../FieldTheory/TranscendentalSeparable.lean | 58 ++++++++++++++----- 1 file changed, 42 insertions(+), 16 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 901a228bee2577..82476e76289bb2 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -277,17 +277,6 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced [Algebra exact isReduced_of_injective _ (Algebra.TensorProduct.comm k B L).injective exact isReduced_of_injective _ (Algebra.TensorProduct.comm k K B).injective -/- -def adjoinPthRoots : IntermediateField k (AlgebraicClosure k) where - carrier := {x | x ^ p ∈ (⊥ : IntermediateField k _)} - mul_mem' {a b} ha hb := by simpa [mul_pow] using mul_mem ha hb - one_mem' := by simp - add_mem' {a b} ha hb := by simpa [add_pow_expChar a b p] using add_mem ha hb - zero_mem' := by simp [zero_pow hp.ne_zero] - algebraMap_mem' x := pow_mem ((⊥ : IntermediateField k _).algebraMap_mem x) p - inv_mem' {a} ha := by simpa --/ - def adjoinPthRoots (p : ℕ) [ExpChar k p] := k variable (p : ℕ) [ExpChar k p] @@ -306,7 +295,6 @@ lemma adjoinPthRoots_pth_power_mem_bot (x : adjoinPthRoots k p) : use adjoinPthRootsSelf k p x rfl -set_option backward.isDefEq.respectTransparency false in instance [Fact (Nat.Prime p)] : Algebra.IsAlgebraic k (adjoinPthRoots k p) where isAlgebraic x := by use Polynomial.X ^ p - Polynomial.C (adjoinPthRootsSelf k p x) @@ -315,9 +303,49 @@ instance [Fact (Nat.Prime p)] : Algebra.IsAlgebraic k (adjoinPthRoots k p) where def adjoinPthRootsPthRoot : k →+* (adjoinPthRoots k p) := RingHom.id k +lemma adjoinPthRootsPthRoot_bijective : Function.Bijective (adjoinPthRootsPthRoot k p) := + (RingEquiv.refl k).bijective + lemma adjoinPthRootsPthRoot_pow (x : k) : algebraMap k (adjoinPthRoots k p) x = (adjoinPthRootsPthRoot k p x) ^ p := rfl +set_option backward.isDefEq.respectTransparency false in +lemma linearIndepOn_pow_of_isReduced_tensorProduct (hp : Nat.Prime p) + (red : IsReduced (TensorProduct k (adjoinPthRoots k p) K)) (s : Finset K) + (li : LinearIndepOn k _root_.id (s : Set K)) : LinearIndepOn k (· ^ p) (s : Set K) := by + simp only [LinearIndepOn, LinearIndependent, SetLike.coe_sort_coe, ← LinearMap.ker_eq_bot, + LinearMap.ker_eq_bot'] + intro y hy + have li' := Module.Flat.linearIndependent_one_tmul (S := (adjoinPthRoots k p)) li + let rooty := Finsupp.mapRange.addMonoidHom (adjoinPthRootsPthRoot k p).toAddMonoidHom y + have : Fact (Nat.Prime p) := ⟨hp⟩ + let : Nontrivial (adjoinPthRoots k p ⊗[k] K) := by + apply Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_flat_left + exact RingHom.injective _ + have : CharP (adjoinPthRoots k p ⊗[k] K) p := by + apply (Algebra.charP_iff k _ p).mp + induction ‹ExpChar k p› with + | zero => exact (Nat.not_prime_one hp).elim + | prime hq => assumption + have rooty_supp : rooty.support = y.support := + Finsupp.support_mapRange_of_injective (map_zero _) y (adjoinPthRootsPthRoot_bijective k p).1 + have rooty_app (x : s) : (rooty x) ^ p = algebraMap k _ (y x) := adjoinPthRootsPthRoot_pow k p _ + have h0 : frobenius _ p (rooty.sum fun (i : s) (c : adjoinPthRoots k p) ↦ c ⊗ₜ[k] i.1) = 0 := by + simp only [Finsupp.sum, map_sum, frobenius_def, Algebra.TensorProduct.tmul_pow, rooty_app] + simp only [Finsupp.linearCombination, Finsupp.coe_lsum, Finsupp.sum, LinearMap.coe_smulRight, + LinearMap.id_coe, id_eq, ← rooty_supp] at hy + apply Eq.trans _ ((Algebra.TensorProduct.includeRight.congr_arg hy).trans (map_zero _)) + simp only [map_sum, map_smul, Algebra.TensorProduct.includeRight_apply] + congr + ext x + simp [Algebra.algebraMap_eq_smul_one, ← TensorProduct.smul_tmul'] + have : (Finsupp.linearCombination (adjoinPthRoots k p) + fun (x : s) ↦ (1 : adjoinPthRoots k p) ⊗ₜ[k] x.1) rooty = 0 := by + simpa [Finsupp.linearCombination, rooty, Algebra.smul_def] using eq_zero_of_pow_eq_zero h0 + exact (map_eq_zero_iff (Finsupp.mapRange.addMonoidHom (adjoinPthRootsPthRoot k p).toAddMonoidHom) + (Finsupp.mapRange_injective _ (map_zero _) (adjoinPthRootsPthRoot_bijective k p).1)).mp + ((map_eq_zero_iff _ li').mp this) + instance : ExpChar (AlgebraicClosure k) p := ExpChar.of_injective_algebraMap' k _ lemma Algebra.isTranscendentalSeparable_tfae (hp : Nat.Prime p) : @@ -333,7 +361,7 @@ lemma Algebra.isTranscendentalSeparable_tfae (hp : Nat.Prime p) : apply (Algebra.isGeometricallyReduced_iff k K).mpr exact isReduced_of_injective _ (Algebra.TensorProduct.comm k _ K).injective tfae_have 4 → 3 := by - let : Fact (Nat.Prime p) := ⟨hp⟩ + have : Fact (Nat.Prime p) := ⟨hp⟩ simp only [isGeometricallyReduced_iff] intro red let f : (adjoinPthRoots k p) →ₐ[k] (AlgebraicClosure k) := @@ -342,9 +370,7 @@ lemma Algebra.isTranscendentalSeparable_tfae (hp : Nat.Prime p) : have : Function.Injective (Algebra.TensorProduct.rTensor K f) := Module.Flat.rTensor_preserves_injective_linearMap _ (RingHom.injective _) exact isReduced_of_injective _ this - tfae_have 3 → 2 := by - --only one missing - sorry + tfae_have 3 → 2 := fun red s li ↦ linearIndepOn_pow_of_isReduced_tensorProduct k K p hp red s li tfae_have 2 → 1 := by simp only [Algebra.isTranscendentalSeparable_iff, Algebra.isSeparablyGenerated_iff] intro h L hL From 77fa3b7571bef72bd9a303d186127c10e6594d19 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 11 Apr 2026 12:27:55 +0800 Subject: [PATCH 23/30] add other version of 10.43.6 for separably generated implying separable --- .../FieldTheory/TranscendentalSeparable.lean | 50 +++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 82476e76289bb2..ccafe56a8784f4 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -277,6 +277,56 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced [Algebra exact isReduced_of_injective _ (Algebra.TensorProduct.comm k B L).injective exact isReduced_of_injective _ (Algebra.TensorProduct.comm k K B).injective +lemma tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced [Algebra k S] [IsReduced S] + (K : Type*) [Field K] [Algebra k K] [Algebra.IsSeparablyGenerated k K] : + IsReduced (TensorProduct k K S) := by + refine IsReduced.tensorProduct_of_flat_of_forall_fg (fun B hB ↦ ?_) + have : Algebra.FiniteType k B := (Subalgebra.fg_iff_finiteType B).mp hB + have : IsReduced B := isReduced_of_injective B.val Subtype.val_injective + have : IsReduced (TensorProduct k B K) := by + refine IsReduced.tensorProduct_of_forall_fg_intermediateField (fun L ⟨G, hG⟩ ↦ ?_) + rcases ‹Algebra.IsSeparablyGenerated k K› with ⟨ι, f, isT, sep⟩ + set M := IntermediateField.adjoin k (Set.range f) + let M' := IntermediateField.adjoin k ((Set.range f) ∪ (G : Set K)) + have : IsReduced (TensorProduct k B M') := by + have mem (x : ι) : f x ∈ M' := IntermediateField.subset_adjoin _ _ (by simp) + let f' : ι → M' := fun x ↦ ⟨f x, mem x⟩ + have imagef' : Subtype.val '' Set.range f' = Set.range f := by + ext + simp [f'] + have isT' : IsTranscendenceBasis k f' := isT.of_comp M'.val Subtype.val_injective + have : Algebra.IsSeparable (IntermediateField.adjoin k (Set.range f')) M' := by + have Mle : M ≤ M' := IntermediateField.adjoin.mono _ _ _ (by simp) + let := (IntermediateField.inclusion Mle).toRingHom.toAlgebra + let : IsScalarTower M M' K := IsScalarTower.of_algebraMap_eq' rfl + have : Algebra.IsSeparable M M' := Algebra.isSeparable_tower_bot_of_isSeparable M M' K + have eq : (IntermediateField.adjoin k (Set.range f')).map M'.val = M := by + simp [IntermediateField.adjoin_map, f', M, imagef'] + let e := ((IntermediateField.adjoin k (Set.range f')).equivMap M'.val).trans + (IntermediateField.equivOfEq eq) + apply Algebra.IsSeparable.of_equiv_equiv e.toRingEquiv.symm (RingEquiv.refl M') + ext m + have : (e.symm m).1.1 = (e (e.symm m)).1 := by simp [- AlgEquiv.apply_symm_apply, e] + simpa only [e.apply_symm_apply] using this + have : Algebra.EssFiniteType (IntermediateField.adjoin k (Set.range f')) ↥M' := by + rw [← IntermediateField.fg_top_iff] + use G.preimage M'.val Subtype.val_injective.injOn + refine le_antisymm le_top (fun x hx ↦ ?_) + rw [← IntermediateField.mem_restrictScalars k, IntermediateField.adjoin_adjoin_left] + simp only [IntermediateField.coe_val, Finset.coe_preimage, ← IntermediateField.mem_lift, + IntermediateField.lift_adjoin, Set.image_union, imagef'] + convert x.2 + ext z + have : z ∈ G → z ∈ M' := fun hz ↦ IntermediateField.subset_adjoin _ _ (by simp [hz]) + simpa + have := tensorProduct_isReduced_of_isTranscendentalBasis_of_isReduced k _ B f' isT' + exact isReduced_of_injective _ (Algebra.TensorProduct.comm k B _).injective + have le : L ≤ M' := le_of_eq_of_le hG.symm (IntermediateField.adjoin.mono _ _ _ (by simp)) + have : Function.Injective (Algebra.TensorProduct.lTensor B (IntermediateField.inclusion le)) := + Module.Flat.lTensor_preserves_injective_linearMap _ (IntermediateField.inclusion_injective le) + exact isReduced_of_injective _ this + exact isReduced_of_injective _ (Algebra.TensorProduct.comm k K B).injective + def adjoinPthRoots (p : ℕ) [ExpChar k p] := k variable (p : ℕ) [ExpChar k p] From 9ca68012fcdd8c4d4e5f83243d649943e68ce187 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 11 Apr 2026 16:29:10 +0800 Subject: [PATCH 24/30] finish 10.44.3 10.45.2 --- .../FieldTheory/TranscendentalSeparable.lean | 33 +++++++++++++++++-- 1 file changed, 30 insertions(+), 3 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index ccafe56a8784f4..1a08885c5813d4 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -327,6 +327,8 @@ lemma tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced [Algebra k S] exact isReduced_of_injective _ this exact isReduced_of_injective _ (Algebra.TensorProduct.comm k K B).injective +section charp + def adjoinPthRoots (p : ℕ) [ExpChar k p] := k variable (p : ℕ) [ExpChar k p] @@ -442,8 +444,33 @@ lemma Algebra.isTranscendentalSeparable_tfae (hp : Nat.Prime p) : <;> simp tfae_finish -/- +end charp + +lemma Algebra.isSeparablyGenerated_of_charZero [CharZero k] : Algebra.IsSeparablyGenerated k K := by + rcases exists_isTranscendenceBasis' k K with ⟨ι, f, isT⟩ + use ι, f, isT + have : Algebra.IsAlgebraic (IntermediateField.adjoin k (Set.range f)) K := isT.isAlgebraic_field + exact Algebra.IsSeparable.of_integral _ K + +lemma Algebra.isTranscendentalSeparable_of_charZero [CharZero k] : + Algebra.IsTranscendentalSeparable k K := + ⟨fun L _ ↦ isSeparablyGenerated_of_charZero k L⟩ + +lemma Algebra.isTranscendentalSeparable_of_isSeparablyGenerated [Algebra.IsSeparablyGenerated k K] : + Algebra.IsTranscendentalSeparable k K := by + rcases CharP.exists' k with char0|⟨p, prime, charp⟩ + · exact Algebra.isTranscendentalSeparable_of_charZero k K + · apply ((Algebra.isTranscendentalSeparable_tfae k K p prime.out).out 0 2).mpr + have := tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced k (adjoinPthRoots k p) K + exact isReduced_of_injective _ (Algebra.TensorProduct.comm k _ _).injective + lemma Algebra.isTranscendentalSeparable_of_perfectField [PerfectField k] {K : Type*} [Field K] [Algebra k K] : Algebra.IsTranscendentalSeparable k K := by - sorry --/ + rcases CharP.exists' k with char0|⟨p, prime, charp⟩ + · exact Algebra.isTranscendentalSeparable_of_charZero k K + · apply ((Algebra.isTranscendentalSeparable_tfae k K p prime.out).out 0 2).mpr + have perf : PerfectRing k p := inferInstance + have bij : Function.Bijective (Algebra.ofId k (adjoinPthRoots k p)) := perf.bijective_frobenius + let e := (Algebra.TensorProduct.congr (AlgEquiv.ofBijective _ bij).symm AlgEquiv.refl).trans + (Algebra.TensorProduct.lid k K) + exact isReduced_of_injective _ e.injective From 2d9bc7f00779fa8fdc99172d465271bee5643307 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 11 Apr 2026 16:59:54 +0800 Subject: [PATCH 25/30] add lemma for fg case --- .../FieldTheory/TranscendentalSeparable.lean | 27 ++++++++++++++++--- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 1a08885c5813d4..4bd1c11078bb82 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -23,7 +23,7 @@ public import Mathlib.FieldTheory.SeparablyGenerated # Transcendental separable extensions -/ -universe u v +universe u v w @[expose] public section @@ -39,6 +39,20 @@ class Algebra.IsSeparablyGenerated : Prop where IsTranscendenceBasis k f ∧ Algebra.IsSeparable (IntermediateField.adjoin k (Set.range f)) K +variable {k K} in +lemma Algebra.isSeparablyGenerated_of_equiv {K' : Type w} [Field K'] [Algebra k K'] (e : K ≃ₐ[k] K') + [Algebra.IsSeparablyGenerated k K] : Algebra.IsSeparablyGenerated k K' := by + rcases ‹Algebra.IsSeparablyGenerated k K› with ⟨ι, f, isT, sep⟩ + have : Small.{w} ι := small_of_injective (e.injective.comp isT.1.injective) + let g := (e ∘ f) ∘ (equivShrink ι).symm + use Shrink.{w} ι, g, (e.isTranscendenceBasis isT).comp_equiv (equivShrink ι).symm + have eq : (IntermediateField.adjoin k (Set.range f)).map e = + (IntermediateField.adjoin k (Set.range g)) := by + simp [IntermediateField.adjoin_map, g, Set.range_comp e f] + let e' := ((IntermediateField.adjoin k (Set.range f)).equivMap e.toAlgHom).trans + (IntermediateField.equivOfEq eq) + exact Algebra.IsSeparable.of_equiv_equiv e'.toRingEquiv e.toRingEquiv rfl + @[mk_iff] class Algebra.IsTranscendentalSeparable : Prop where forall_isSeparablyGenerated : ∀ (A' : IntermediateField k K), @@ -291,9 +305,7 @@ lemma tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced [Algebra k S] have : IsReduced (TensorProduct k B M') := by have mem (x : ι) : f x ∈ M' := IntermediateField.subset_adjoin _ _ (by simp) let f' : ι → M' := fun x ↦ ⟨f x, mem x⟩ - have imagef' : Subtype.val '' Set.range f' = Set.range f := by - ext - simp [f'] + have imagef' : Subtype.val '' Set.range f' = Set.range f := (Set.range_comp _ _).symm have isT' : IsTranscendenceBasis k f' := isT.of_comp M'.val Subtype.val_injective have : Algebra.IsSeparable (IntermediateField.adjoin k (Set.range f')) M' := by have Mle : M ≤ M' := IntermediateField.adjoin.mono _ _ _ (by simp) @@ -464,6 +476,13 @@ lemma Algebra.isTranscendentalSeparable_of_isSeparablyGenerated [Algebra.IsSepar have := tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced k (adjoinPthRoots k p) K exact isReduced_of_injective _ (Algebra.TensorProduct.comm k _ _).injective +lemma Algebra.isTranscendentalSeparable_iff_isSeparablyGenerated_of_essFiniteType + [Algebra.EssFiniteType k K] : + Algebra.IsTranscendentalSeparable k K ↔ Algebra.IsSeparablyGenerated k K := by + refine ⟨fun h ↦ ?_, fun _ ↦ Algebra.isTranscendentalSeparable_of_isSeparablyGenerated k K⟩ + have := h.1 ⊤ (IntermediateField.essFiniteType_iff.mpr (IntermediateField.fg_top_iff.mpr ‹_›)) + exact Algebra.isSeparablyGenerated_of_equiv IntermediateField.topEquiv + lemma Algebra.isTranscendentalSeparable_of_perfectField [PerfectField k] {K : Type*} [Field K] [Algebra k K] : Algebra.IsTranscendentalSeparable k K := by rcases CharP.exists' k with char0|⟨p, prime, charp⟩ From e1b6691fb71193e39b9a43d334d795b3807f9d6b Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 11 Apr 2026 18:01:59 +0800 Subject: [PATCH 26/30] add doc --- .../FieldTheory/TranscendentalSeparable.lean | 64 ++++++++++++++++++- 1 file changed, 61 insertions(+), 3 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 4bd1c11078bb82..4180e6675eaf6d 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -21,6 +21,46 @@ public import Mathlib.FieldTheory.SeparablyGenerated /-! # Transcendental separable extensions + +In this file we introduce the concept of separably generated field extensions and +transcendental separable field extensions. We then formalizes the following result: + +Let `K/k` be arbitrary field extension with characteristic `p > 0`, then TFAE +1. `K/k` is transcendental separable. +2. If `{ sᵢ } ⊆ K` is an arbitrary `k`-linearly independent set, + `{ sᵢᵖ } ⊆ K` is also `k`-linearly independent. +3. `K ⊗ₖ k^{1/p}` is reduced. +4. `K` is geometrically reduced over `k`. + +# Main definitions and results + +* `Algebra.IsSeparablyGenerated` : A field extension is separably generated if there exists + an transcendental basis such that the extension above it is separable. + +* `Algebra.IsTranscendentalSeparable` : A field extension is transcendental separable if + every finitely generated subextension is separably generated. + +* `tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced` : Tensor product of + a transcendental separable field extension with a reduced algebra is reduced. + +* `tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced` : Tensor product of + a separably generated field extension with a reduced algebra is reduced. + +* `adjoinPthRoots`: Adjoining all `p`-th root to a field of characteristic `p`. + It is defined as the field itself with algebra map being the frobenius map. + +* `adjoinPthRootsPthRoot` : The map `k → adjoinPthRoots k p` for taking `p`-th root + with underlying map `RingHom.id`. + +* `Algebra.isTranscendentalSeparable_tfae` : The equivalent characterization of + transcendental separable field extension mentioned above. + +* `Algebra.isTranscendentalSeparable_of_isSeparablyGenerated` : + Separably generated field extension is transcendental separable. + +* `Algebra.isTranscendentalSeparable_of_perfectField` : + All extension over perfect field is transcendental separable. + -/ universe u v w @@ -33,7 +73,9 @@ section variable (k : Type u) (K : Type v) [Field k] [Field K] [Algebra k K] -@[mk_iff] +/-- A field extension is separably generated if there exists an transcendental basis such that +the extension above it is separable. -/ +@[mk_iff, stacks 030O "Part 1"] class Algebra.IsSeparablyGenerated : Prop where isSeparable' : ∃ (ι : Type v) (f : ι → K), IsTranscendenceBasis k f ∧ @@ -53,7 +95,9 @@ lemma Algebra.isSeparablyGenerated_of_equiv {K' : Type w} [Field K'] [Algebra k (IntermediateField.equivOfEq eq) exact Algebra.IsSeparable.of_equiv_equiv e'.toRingEquiv e.toRingEquiv rfl -@[mk_iff] +/-- A field extension is transcendental separable if every finitely generated subextension is +separably generated. -/ +@[mk_iff, stacks 030O "Part 2"] class Algebra.IsTranscendentalSeparable : Prop where forall_isSeparablyGenerated : ∀ (A' : IntermediateField k K), Algebra.EssFiniteType k A' → Algebra.IsSeparablyGenerated k A' @@ -75,11 +119,13 @@ lemma localization_minimal_isField {S : Type*} [CommRing S] [IsReduced S] rw [← Localization.AtPrime.eq_maximalIdeal_iff_comap_eq] exact le_antisymm this (min.2 ⟨q.comap_isPrime _, bot_le⟩ this) +/-- The map of a ring to product of its localizations at minimal primes. -/ def toLocalizationMinimal (S : Type*) [CommRing S] := (Pi.ringHom (fun (p : minimalPrimes S) ↦ letI := Ideal.minimalPrimes_isPrime p.2 algebraMap S (Localization.AtPrime p.1))) +/-- The map of a reduced ring to product of its localizations at minimal primes is injective. -/ lemma isReduced_injective_to_prod_localizations (S : Type*) [CommRing S] [IsReduced S] : Function.Injective (toLocalizationMinimal S) := by rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero] @@ -155,6 +201,7 @@ lemma isReduced_of_quotient_separable [IsDomain S] (f : S[X]) (mon : f.Monic) apply isReduced_of_injective iQ ((Ideal.injective_lift_iff _).mpr _) simp [← RingHom.comap_ker, eq] +/-- The canonical isomorphism `K[X] ⊗[k] S ≃ₐ[K] (K ⊗[k] S)[X]` for `k`-algebra `S, K`. -/ noncomputable def polynomialTensorProductEquiv [Algebra k S] : K[X] ⊗[k] S ≃ₐ[K] (K ⊗[k] S)[X] := ((((Algebra.TensorProduct.congr (polyEquivTensor' k K) AlgEquiv.refl).trans (Algebra.TensorProduct.assoc k k K K k[X] S)).trans @@ -175,6 +222,7 @@ lemma polynomialTensorProductEquiv_map_algebraMap [Algebra k S] (f : K[X]) : simp [Polynomial.map_map, ← IsScalarTower.algebraMap_eq] simpa [- polyEquivTensor_symm_apply_tmul_eq_smul, polynomialTensorProductEquiv] +/-- The equivalence of adjoining on root inside tensor product and outside tensor product. -/ noncomputable def quotientPolynomialTensorProductEquiv (f : K[X]) [Algebra k S] : (K[X] ⧸ Ideal.span {f}) ⊗[k] S ≃ₐ[K] (K ⊗[k] S)[X] ⧸ Ideal.span {f.map (algebraMap K (K ⊗[k] S))} := @@ -277,6 +325,7 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFi have := Algebra.EssFiniteType.of_comp k (IntermediateField.adjoin k (Set.range f)) K exact tensorProduct_isReduced_of_isTranscendentalBasis_of_isReduced k K S f isT +@[stacks 030U "Part 1"] lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced [Algebra k S] [IsReduced S] (K : Type*) [Field K] [Algebra k K] [Algebra.IsTranscendentalSeparable k K] : IsReduced (TensorProduct k K S) := by @@ -291,6 +340,7 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced [Algebra exact isReduced_of_injective _ (Algebra.TensorProduct.comm k B L).injective exact isReduced_of_injective _ (Algebra.TensorProduct.comm k K B).injective +@[stacks 030U "Part 2"] lemma tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced [Algebra k S] [IsReduced S] (K : Type*) [Field K] [Algebra k K] [Algebra.IsSeparablyGenerated k K] : IsReduced (TensorProduct k K S) := by @@ -341,6 +391,9 @@ lemma tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced [Algebra k S] section charp +/-- Adjoining all `p`-th root to a field of characteristic `p`. +It is defined as the field itself with algebra map being the frobenius map. -/ +@[nolint unusedArguments] def adjoinPthRoots (p : ℕ) [ExpChar k p] := k variable (p : ℕ) [ExpChar k p] @@ -349,6 +402,7 @@ instance : Field (adjoinPthRoots k p) := inferInstanceAs (Field k) instance : Algebra k (adjoinPthRoots k p) := (frobenius k p).toAlgebra +/-- The map `adjoinPthRoots k p → k` with underlying map `RingHom.id`. -/ def adjoinPthRootsSelf : (adjoinPthRoots k p) →+* k := RingHom.id k lemma adjoinPthRootsSelf_algebraMap (x : adjoinPthRoots k p) : @@ -365,6 +419,7 @@ instance [Fact (Nat.Prime p)] : Algebra.IsAlgebraic k (adjoinPthRoots k p) where refine ⟨(Polynomial.monic_X_pow_sub_C _ (NeZero.ne' p).symm).ne_zero, ?_⟩ simp [adjoinPthRootsSelf_algebraMap] +/-- The map `k → adjoinPthRoots k p` for taking `p`-th root with underlying map `RingHom.id`. -/ def adjoinPthRootsPthRoot : k →+* (adjoinPthRoots k p) := RingHom.id k lemma adjoinPthRootsPthRoot_bijective : Function.Bijective (adjoinPthRootsPthRoot k p) := @@ -373,7 +428,6 @@ lemma adjoinPthRootsPthRoot_bijective : Function.Bijective (adjoinPthRootsPthRoo lemma adjoinPthRootsPthRoot_pow (x : k) : algebraMap k (adjoinPthRoots k p) x = (adjoinPthRootsPthRoot k p x) ^ p := rfl -set_option backward.isDefEq.respectTransparency false in lemma linearIndepOn_pow_of_isReduced_tensorProduct (hp : Nat.Prime p) (red : IsReduced (TensorProduct k (adjoinPthRoots k p) K)) (s : Finset K) (li : LinearIndepOn k _root_.id (s : Set K)) : LinearIndepOn k (· ^ p) (s : Set K) := by @@ -412,6 +466,7 @@ lemma linearIndepOn_pow_of_isReduced_tensorProduct (hp : Nat.Prime p) instance : ExpChar (AlgebraicClosure k) p := ExpChar.of_injective_algebraMap' k _ +@[stacks 030W] lemma Algebra.isTranscendentalSeparable_tfae (hp : Nat.Prime p) : [ Algebra.IsTranscendentalSeparable k K, ∀ s : Finset K, @@ -468,6 +523,8 @@ lemma Algebra.isTranscendentalSeparable_of_charZero [CharZero k] : Algebra.IsTranscendentalSeparable k K := ⟨fun L _ ↦ isSeparablyGenerated_of_charZero k L⟩ +/-- Separably generated field extension is transcendental separable. -/ +@[stacks 030X] lemma Algebra.isTranscendentalSeparable_of_isSeparablyGenerated [Algebra.IsSeparablyGenerated k K] : Algebra.IsTranscendentalSeparable k K := by rcases CharP.exists' k with char0|⟨p, prime, charp⟩ @@ -483,6 +540,7 @@ lemma Algebra.isTranscendentalSeparable_iff_isSeparablyGenerated_of_essFiniteTyp have := h.1 ⊤ (IntermediateField.essFiniteType_iff.mpr (IntermediateField.fg_top_iff.mpr ‹_›)) exact Algebra.isSeparablyGenerated_of_equiv IntermediateField.topEquiv +@[stacks 030Y "Equivalence to the alternative definition."] lemma Algebra.isTranscendentalSeparable_of_perfectField [PerfectField k] {K : Type*} [Field K] [Algebra k K] : Algebra.IsTranscendentalSeparable k K := by rcases CharP.exists' k with char0|⟨p, prime, charp⟩ From 6241660d5a63b1dd2ec8d064e277d6202644dfb3 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 11 Apr 2026 18:11:23 +0800 Subject: [PATCH 27/30] move doc --- Mathlib/FieldTheory/SeparablyGenerated.lean | 25 ++++++++----------- .../FieldTheory/TranscendentalSeparable.lean | 5 ++++ 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/Mathlib/FieldTheory/SeparablyGenerated.lean b/Mathlib/FieldTheory/SeparablyGenerated.lean index ab7f432dd2d92a..3f343526ea17ad 100644 --- a/Mathlib/FieldTheory/SeparablyGenerated.lean +++ b/Mathlib/FieldTheory/SeparablyGenerated.lean @@ -15,20 +15,17 @@ public import Mathlib.RingTheory.Polynomial.GaussLemma /-! -# Separably generated extensions +# Characterization of separably generated extensions -We aim to formalize the following result: - -Let `K/k` be a finitely generated field extension with characteristic `p > 0`, then TFAE -1. `K/k` is separably generated -2. If `{ sᵢ } ⊆ K` is an arbitrary `k`-linearly independent set, - `{ sᵢᵖ } ⊆ K` is also `k`-linearly independent -3. `K ⊗ₖ k^{1/p}` is reduced -4. `K` is geometrically reduced over `k`. -5. `k` and `Kᵖ` are linearly disjoint over `kᵖ` in `K`. +In this file we prove for finitely generated field extension `K/k`, +if `{ sᵢ } ⊆ K` is an arbitrary `k`-linearly independent set implies +`{ sᵢᵖ } ⊆ K` is also `k`-linearly independent, then `K/k` is finite separably generated. ## Main result -- `exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow`: (2) ⇒ (1) +- `exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType`: + Suppose `k` has characteristic `p` and `K/k` is finitely generated. + Suppose furthermore that if `{ sᵢ } ⊆ K` is an arbitrary `k`-linearly independent set, + `{ sᵢᵖ } ⊆ K` is also `k`-linearly independent, then `K/k` is finite separably generated. -/ @@ -274,11 +271,9 @@ lemma exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin /-- Suppose `k` has characteristic `p` and `K/k` is finitely generated. Suppose furthermore that if `{ sᵢ } ⊆ K` is an arbitrary `k`-linearly independent set, -`{ sᵢᵖ } ⊆ K` is also `k`-linearly independent (which is true when `K ⊗ₖ k^{1/p}` is reduced). - -Then `K/k` is finite separably generated. +`{ sᵢᵖ } ⊆ K` is also `k`-linearly independent, then `K/k` is finite separably generated. -TODO: show that this is an if and only if. +For if and only if, see `Algebra.isTranscendentalSeparable_tfae`. -/ @[stacks 030W "(2) ⇒ (1) finitely generated case"] lemma exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 4180e6675eaf6d..8e9cfaf2274961 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -61,6 +61,11 @@ Let `K/k` be arbitrary field extension with characteristic `p > 0`, then TFAE * `Algebra.isTranscendentalSeparable_of_perfectField` : All extension over perfect field is transcendental separable. +# TODO +Prove that "`k` and `Kᵖ` are linearly disjoint over `kᵖ` in `K`" is also equivalent to the +four equivalent characterization of being transcendental seprarable for +finitely generated field extension `K/k`. + -/ universe u v w From d15a0d80afe6cafd2a2cd0d38777bfd9682f0f07 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 11 Apr 2026 22:44:46 +0800 Subject: [PATCH 28/30] definition of transcendental separable --- Mathlib.lean | 1 + .../FieldTheory/TranscendentalSeparable.lean | 68 +++++++++++++++++++ 2 files changed, 69 insertions(+) create mode 100644 Mathlib/FieldTheory/TranscendentalSeparable.lean diff --git a/Mathlib.lean b/Mathlib.lean index 9a7f9231df7463..396dbad444eb22 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -4400,6 +4400,7 @@ public import Mathlib.FieldTheory.SeparablyGenerated public import Mathlib.FieldTheory.SplittingField.Construction public import Mathlib.FieldTheory.SplittingField.IsSplittingField public import Mathlib.FieldTheory.Tower +public import Mathlib.FieldTheory.TranscendentalSeparable public import Mathlib.Geometry.Convex.Cone.Basic public import Mathlib.Geometry.Convex.Cone.Dual public import Mathlib.Geometry.Convex.Cone.DualFinite diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean new file mode 100644 index 00000000000000..af1b4992269ae9 --- /dev/null +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -0,0 +1,68 @@ +/- +Copyright (c) 2026 Nailin Guan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Nailin Guan +-/ +module + +public import Mathlib.FieldTheory.IntermediateField.Adjoin.Defs +public import Mathlib.FieldTheory.Separable +public import Mathlib.RingTheory.AlgebraicIndependent.Basic +public import Mathlib.RingTheory.EssentialFiniteness + +/-! +# Transcendental separable extensions + +In this file we introduce the concept of separably generated field extensions and +transcendental separable field extensions. + +# Main definitions and results + +* `Algebra.IsSeparablyGenerated` : A field extension is separably generated if there exists + an transcendental basis such that the extension above it is separable. + +* `Algebra.IsTranscendentalSeparable` : A field extension is transcendental separable if + every finitely generated subextension is separably generated. + +-/ + +universe u v w + +@[expose] public section + +open TensorProduct + +section + +variable (k : Type u) (K : Type v) [Field k] [Field K] [Algebra k K] + +/-- A field extension is separably generated if there exists an transcendental basis such that +the extension above it is separable. -/ +@[mk_iff, stacks 030O "Part 1"] +class Algebra.IsSeparablyGenerated : Prop where + isSeparable' : ∃ (ι : Type v) (f : ι → K), + IsTranscendenceBasis k f ∧ + Algebra.IsSeparable (IntermediateField.adjoin k (Set.range f)) K + +variable {k K} in +lemma Algebra.isSeparablyGenerated_of_equiv {K' : Type w} [Field K'] [Algebra k K'] (e : K ≃ₐ[k] K') + [Algebra.IsSeparablyGenerated k K] : Algebra.IsSeparablyGenerated k K' := by + rcases ‹Algebra.IsSeparablyGenerated k K› with ⟨ι, f, isT, sep⟩ + have : Small.{w} ι := small_of_injective (e.injective.comp isT.1.injective) + let g := (e ∘ f) ∘ (equivShrink ι).symm + use Shrink.{w} ι, g, (e.isTranscendenceBasis isT).comp_equiv (equivShrink ι).symm + have eq : (IntermediateField.adjoin k (Set.range f)).map e = + (IntermediateField.adjoin k (Set.range g)) := by + simp [IntermediateField.adjoin_map, g, Set.range_comp e f] + let e' := ((IntermediateField.adjoin k (Set.range f)).equivMap e.toAlgHom).trans + (IntermediateField.equivOfEq eq) + exact Algebra.IsSeparable.of_equiv_equiv e'.toRingEquiv e.toRingEquiv rfl + +/-- A field extension is transcendental separable if every finitely generated subextension is +separably generated. -/ +@[mk_iff, stacks 030O "Part 2"] +class Algebra.IsTranscendentalSeparable : Prop where + forall_isSeparablyGenerated : ∀ (A' : IntermediateField k K), + Algebra.EssFiniteType k A' → Algebra.IsSeparablyGenerated k A' + +end From e38fc33f5abfebade2b8cfd238c2e5dfcf9b85f5 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Sat, 11 Apr 2026 22:53:56 +0800 Subject: [PATCH 29/30] fix import --- Mathlib/FieldTheory/TranscendentalSeparable.lean | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 8e9cfaf2274961..7100efc21e54e3 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -5,19 +5,11 @@ Authors: Nailin Guan -/ module -public import Mathlib.RingTheory.Flat.Basic -public import Mathlib.RingTheory.TensorProduct.DirectLimitFG -public import Mathlib.FieldTheory.Perfect -public import Mathlib.FieldTheory.Separable -public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis -public import Mathlib.RingTheory.Ideal.MinimalPrime.Basic -public import Mathlib.RingTheory.Localization.AtPrime.Basic -public import Mathlib.RingTheory.LocalProperties.Reduced -public import Mathlib.RingTheory.TensorProduct.Pi +public import Mathlib.FieldTheory.SeparablyGenerated public import Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian -public import Mathlib.FieldTheory.PrimitiveElement +public import Mathlib.RingTheory.LocalProperties.Reduced public import Mathlib.RingTheory.Nilpotent.GeometricallyReduced -public import Mathlib.FieldTheory.SeparablyGenerated +public import Mathlib.RingTheory.TensorProduct.Pi /-! # Transcendental separable extensions From 5840e822c22acbd16a20109e401cba0e73edc562 Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Mon, 13 Apr 2026 13:28:47 +0800 Subject: [PATCH 30/30] fix variable --- .../FieldTheory/TranscendentalSeparable.lean | 49 +++++++++---------- 1 file changed, 22 insertions(+), 27 deletions(-) diff --git a/Mathlib/FieldTheory/TranscendentalSeparable.lean b/Mathlib/FieldTheory/TranscendentalSeparable.lean index 7100efc21e54e3..7caf4e0e86d86c 100644 --- a/Mathlib/FieldTheory/TranscendentalSeparable.lean +++ b/Mathlib/FieldTheory/TranscendentalSeparable.lean @@ -103,9 +103,9 @@ end lemma localization_minimal_isField {S : Type*} [CommRing S] [IsReduced S] (p : Ideal S) (min : p ∈ minimalPrimes S) : - letI := min.1.1 + letI := Ideal.minimalPrimes_isPrime min IsField (Localization.AtPrime p) := by - let := min.1.1 + let := Ideal.minimalPrimes_isPrime min rw [IsLocalRing.isField_iff_maximalIdeal_eq, eq_bot_iff] intro x hx apply IsReduced.eq_zero x (nilpotent_iff_mem_prime.mpr (fun q hq ↦ ?_)) @@ -129,7 +129,7 @@ lemma isReduced_injective_to_prod_localizations (S : Type*) [CommRing S] [IsRedu intro x hx apply IsReduced.eq_zero x (nilpotent_iff_mem_prime.mpr (fun q hq ↦ ?_)) rcases Ideal.exists_minimalPrimes_le (bot_le (a := q)) with ⟨p, min, hp⟩ - let := min.1.1 + let := Ideal.minimalPrimes_isPrime min apply hp rw [← IsLocalization.AtPrime.comap_maximalIdeal (Localization.AtPrime p) p, Ideal.mem_comap] have : (toLocalizationMinimal S) x ⟨p, min⟩ = 0 := by simp [hx] @@ -182,7 +182,7 @@ lemma isReduced_of_quotient_separable_of_field (S : Type*) [Field S] (f : S[X]) exact ih g.natDegree (by linarith) g sep.of_mul_right rfl exact isReduced_of_injective _ (Ideal.quotientMulEquivQuotientProd _ _ cop).injective -variable (S : Type*) [CommRing S] +variable (S : Type*) [CommRing S] [Algebra k S] lemma isReduced_of_quotient_separable [IsDomain S] (f : S[X]) (mon : f.Monic) (sep : f.Separable) : IsReduced (S[X] ⧸ Ideal.span {f}) := by @@ -199,14 +199,14 @@ lemma isReduced_of_quotient_separable [IsDomain S] (f : S[X]) (mon : f.Monic) simp [← RingHom.comap_ker, eq] /-- The canonical isomorphism `K[X] ⊗[k] S ≃ₐ[K] (K ⊗[k] S)[X]` for `k`-algebra `S, K`. -/ -noncomputable def polynomialTensorProductEquiv [Algebra k S] : K[X] ⊗[k] S ≃ₐ[K] (K ⊗[k] S)[X] := +noncomputable def polynomialTensorProductEquiv : K[X] ⊗[k] S ≃ₐ[K] (K ⊗[k] S)[X] := ((((Algebra.TensorProduct.congr (polyEquivTensor' k K) AlgEquiv.refl).trans (Algebra.TensorProduct.assoc k k K K k[X] S)).trans (Algebra.TensorProduct.congr AlgEquiv.refl (Algebra.TensorProduct.comm k k[X] S))).trans (Algebra.TensorProduct.assoc k k K K S k[X]).symm).trans ((polyEquivTensor' k (K ⊗[k] S)).symm.restrictScalars K) -lemma polynomialTensorProductEquiv_map_algebraMap [Algebra k S] (f : K[X]) : +lemma polynomialTensorProductEquiv_map_algebraMap (f : K[X]) : f.map (algebraMap K (K ⊗[k] S)) = (polynomialTensorProductEquiv k K S) ((algebraMap K[X] (K[X] ⊗[k] S)) f) := by obtain ⟨g, rfl⟩ := (polyEquivTensor' k K).symm.surjective f @@ -220,7 +220,7 @@ lemma polynomialTensorProductEquiv_map_algebraMap [Algebra k S] (f : K[X]) : simpa [- polyEquivTensor_symm_apply_tmul_eq_smul, polynomialTensorProductEquiv] /-- The equivalence of adjoining on root inside tensor product and outside tensor product. -/ -noncomputable def quotientPolynomialTensorProductEquiv (f : K[X]) [Algebra k S] : +noncomputable def quotientPolynomialTensorProductEquiv (f : K[X]) : (K[X] ⧸ Ideal.span {f}) ⊗[k] S ≃ₐ[K] (K ⊗[k] S)[X] ⧸ Ideal.span {f.map (algebraMap K (K ⊗[k] S))} := let : IsScalarTower K (K[X] ⧸ Ideal.span {f}) @@ -234,8 +234,8 @@ noncomputable def quotientPolynomialTensorProductEquiv (f : K[X]) [Algebra k S] polynomialTensorProductEquiv_map_algebraMap])) open IntermediateField.algebraAdjoinAdjoin in -lemma tensorProduct_isReduced_of_isTranscendentalBasis_of_isDomain - [Algebra k S] [IsDomain S] {ι : Type v} (f : ι → K) (isT : IsTranscendenceBasis k f) +lemma tensorProduct_isReduced_of_isTranscendentalBasis_of_isDomain [IsDomain S] + {ι : Type v} (f : ι → K) (isT : IsTranscendenceBasis k f) [sep : Algebra.IsSeparable (IntermediateField.adjoin k (Set.range f)) K] [Algebra.EssFiniteType (IntermediateField.adjoin k (Set.range f)) K] : IsReduced (TensorProduct k K S) := by @@ -275,17 +275,15 @@ lemma tensorProduct_isReduced_of_isTranscendentalBasis_of_isDomain exact isReduced_of_injective _ eTen.injective open IntermediateField.algebraAdjoinAdjoin in -lemma tensorProduct_isReduced_of_isSeparablyGenerated_isDomain - (S : Type*) [CommRing S] [Algebra k S] [IsDomain S] +lemma tensorProduct_isReduced_of_isSeparablyGenerated_isDomain [IsDomain S] [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by obtain ⟨ι, f, isT, sep⟩ : Algebra.IsSeparablyGenerated k K := ‹_› have := Algebra.EssFiniteType.of_comp k (IntermediateField.adjoin k (Set.range f)) K exact tensorProduct_isReduced_of_isTranscendentalBasis_of_isDomain k K S f isT -lemma tensorProduct_isReduced_of_isTranscendentalBasis_of_isReduced - [Algebra k S] [IsReduced S] [Algebra.FiniteType k S] - {ι : Type v} (f : ι → K) (isT : IsTranscendenceBasis k f) +lemma tensorProduct_isReduced_of_isTranscendentalBasis_of_isReduced [IsReduced S] + [Algebra.FiniteType k S] {ι : Type v} (f : ι → K) (isT : IsTranscendenceBasis k f) [sep : Algebra.IsSeparable (IntermediateField.adjoin k (Set.range f)) K] [Algebra.EssFiniteType (IntermediateField.adjoin k (Set.range f)) K] : IsReduced (TensorProduct k K S) := by @@ -314,18 +312,16 @@ lemma tensorProduct_isReduced_of_isTranscendentalBasis_of_isReduced exact isReduced_of_injective _ inj lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced_of_essFiniteType - (S : Type*) [CommRing S] [Algebra k S] [Algebra.FiniteType k S] [IsReduced S] - [Algebra.IsSeparablyGenerated k K] [Algebra.EssFiniteType k K] : - IsReduced (TensorProduct k K S) := by + [Algebra.FiniteType k S] [IsReduced S] [Algebra.IsSeparablyGenerated k K] + [Algebra.EssFiniteType k K] : IsReduced (TensorProduct k K S) := by classical obtain ⟨ι, f, isT, sep⟩ : Algebra.IsSeparablyGenerated k K := ‹_› have := Algebra.EssFiniteType.of_comp k (IntermediateField.adjoin k (Set.range f)) K exact tensorProduct_isReduced_of_isTranscendentalBasis_of_isReduced k K S f isT @[stacks 030U "Part 1"] -lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced [Algebra k S] [IsReduced S] - (K : Type*) [Field K] [Algebra k K] [Algebra.IsTranscendentalSeparable k K] : - IsReduced (TensorProduct k K S) := by +lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced [IsReduced S] + [Algebra.IsTranscendentalSeparable k K] : IsReduced (TensorProduct k K S) := by refine IsReduced.tensorProduct_of_flat_of_forall_fg (fun B hB ↦ ?_) have : Algebra.FiniteType k B := (Subalgebra.fg_iff_finiteType B).mp hB have : IsReduced B := isReduced_of_injective B.val Subtype.val_injective @@ -338,9 +334,8 @@ lemma tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced [Algebra exact isReduced_of_injective _ (Algebra.TensorProduct.comm k K B).injective @[stacks 030U "Part 2"] -lemma tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced [Algebra k S] [IsReduced S] - (K : Type*) [Field K] [Algebra k K] [Algebra.IsSeparablyGenerated k K] : - IsReduced (TensorProduct k K S) := by +lemma tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced [IsReduced S] + [Algebra.IsSeparablyGenerated k K] : IsReduced (TensorProduct k K S) := by refine IsReduced.tensorProduct_of_flat_of_forall_fg (fun B hB ↦ ?_) have : Algebra.FiniteType k B := (Subalgebra.fg_iff_finiteType B).mp hB have : IsReduced B := isReduced_of_injective B.val Subtype.val_injective @@ -473,7 +468,7 @@ lemma Algebra.isTranscendentalSeparable_tfae (hp : Nat.Prime p) : tfae_have 1 → 4 := by intro sep have := tensorProduct_isReduced_of_isTranscendentalSeparable_of_isReduced - k (AlgebraicClosure k) K + k K (AlgebraicClosure k) apply (Algebra.isGeometricallyReduced_iff k K).mpr exact isReduced_of_injective _ (Algebra.TensorProduct.comm k _ K).injective tfae_have 4 → 3 := by @@ -527,7 +522,7 @@ lemma Algebra.isTranscendentalSeparable_of_isSeparablyGenerated [Algebra.IsSepar rcases CharP.exists' k with char0|⟨p, prime, charp⟩ · exact Algebra.isTranscendentalSeparable_of_charZero k K · apply ((Algebra.isTranscendentalSeparable_tfae k K p prime.out).out 0 2).mpr - have := tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced k (adjoinPthRoots k p) K + have := tensorProduct_isReduced_of_isSeparablyGenerated_of_isReduced k K (adjoinPthRoots k p) exact isReduced_of_injective _ (Algebra.TensorProduct.comm k _ _).injective lemma Algebra.isTranscendentalSeparable_iff_isSeparablyGenerated_of_essFiniteType @@ -538,8 +533,8 @@ lemma Algebra.isTranscendentalSeparable_iff_isSeparablyGenerated_of_essFiniteTyp exact Algebra.isSeparablyGenerated_of_equiv IntermediateField.topEquiv @[stacks 030Y "Equivalence to the alternative definition."] -lemma Algebra.isTranscendentalSeparable_of_perfectField [PerfectField k] - {K : Type*} [Field K] [Algebra k K] : Algebra.IsTranscendentalSeparable k K := by +lemma Algebra.isTranscendentalSeparable_of_perfectField [PerfectField k] : + Algebra.IsTranscendentalSeparable k K := by rcases CharP.exists' k with char0|⟨p, prime, charp⟩ · exact Algebra.isTranscendentalSeparable_of_charZero k K · apply ((Algebra.isTranscendentalSeparable_tfae k K p prime.out).out 0 2).mpr