From ef8c4e5e5c649b143296302bb9815d646f857385 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Tue, 5 May 2026 23:35:58 +0100 Subject: [PATCH 1/4] temp --- Mathlib/Algebra/Field/Subfield/Basic.lean | 6 ++++ .../IntermediateField/Adjoin/Algebra.lean | 5 +++ .../IntermediateField/Adjoin/Defs.lean | 7 ++++ .../TranscendenceBasis.lean | 32 +++++++++++++++++++ 4 files changed, 50 insertions(+) diff --git a/Mathlib/Algebra/Field/Subfield/Basic.lean b/Mathlib/Algebra/Field/Subfield/Basic.lean index 0f34ab90c7b2b1..97ff49468e4585 100644 --- a/Mathlib/Algebra/Field/Subfield/Basic.lean +++ b/Mathlib/Algebra/Field/Subfield/Basic.lean @@ -433,6 +433,12 @@ theorem coe_sSup_of_directedOn {S : Set (Subfield K)} (Sne : S.Nonempty) end Subfield +variable (L) in +/-- A field is finitely generated if it is the closure of a finite subset. -/ +@[mk_iff fg_iff] +protected class Field.FG : Prop where + finitely_generated : ∃ S : Finset L, Subfield.closure (S : Set L) = ⊤ + namespace RingHom variable {s : Subfield K} diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean index 037a6c723713d1..517d2987696954 100644 --- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean +++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean @@ -124,6 +124,11 @@ lemma essFiniteType_iff {K : IntermediateField F E} : adjoin_map, ← Set.range_comp, Function.comp_def, ← AlgHom.fieldRange_eq_map] using this exact ⟨fun ⟨s, _, hs⟩ ↦ ⟨s, hs⟩, fun ⟨s, hs⟩ ↦ ⟨s, hs ▸ subset_adjoin _ _, hs⟩⟩ +/-- A field is finitely generated if and only if it is essentially of finite type over its prime +subfield. -/ +theorem _root_.Field.fg_iff_essFiniteType : Field.FG F ↔ Algebra.EssFiniteType (⊥ : Subfield F) F := + Field.fg_iff_fg_top_bot.trans fg_top_iff + end FG section AdjoinSimple diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean index da6341a6aafb9a..3529d1cd78a178 100644 --- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean +++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean @@ -673,6 +673,13 @@ theorem fg_iSup {ι : Sort*} [Finite ι] {S : ι → IntermediateField F E} (h : simp_rw [← hs, ← adjoin_iUnion] exact fg_adjoin_of_finite (Set.finite_iUnion fun _ ↦ Finset.finite_toSet _) +/-- A field is finitely generated if and only if it is finitely generated over its prime +subfield. -/ +theorem _root_.Field.fg_iff_fg_top_bot : + Field.FG F ↔ (⊤ : IntermediateField (⊥ : Subfield F) F).FG := by + simp [Field.fg_iff, fg_def, Set.exists_finite_iff_finset, + ← toSubfield_inj, Subfield.algebraMap_ofSubfield, Subfield.closure_union] + theorem induction_on_adjoin_finset (S : Finset E) (P : IntermediateField F E → Prop) (base : P ⊥) (ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (K⟮x⟯.restrictScalars F)) : P (adjoin F S) := by diff --git a/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean b/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean index 1b261c9e579b6f..56cd4be0ba85ca 100644 --- a/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean +++ b/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean @@ -246,6 +246,38 @@ theorem IsTranscendenceBasis.isAlgebraic_field {F E : Type*} {x : ι → E} IsScalarTower.of_algebraMap_eq (congrFun rfl) exact Algebra.IsAlgebraic.extendScalars (R := adjoin F S) (Subalgebra.inclusion_injective _) +theorem Algebra.EssFiniteType.of_isScalarTower + (F K L : Type*) [Field F] [Field K] [Field L] [Algebra F K] [Algebra K L] + [Algebra F L] [IsScalarTower F K L] [Algebra.EssFiniteType F L] : + Algebra.EssFiniteType F K := by + obtain ⟨bFK, hbFK⟩ := exists_isTranscendenceBasis F K + obtain ⟨bKL, hbKL⟩ := exists_isTranscendenceBasis K L + have := hbFK.sumElim_comp hbKL + -- idea: L is finite over F adjoin hbFK ∪ hbKL + -- K adjoin hbKL is finite over F adjoin hbFK ∪ hbKL + -- K is algebraic over F adjoin hbFK + -- but adjoining transcendental elements won't affect the degree + -- so K is finite over F adjoin hbFK + -- so K is finitely generated over F + sorry + +theorem Algebra.EssFiniteType.of_algHom + {F K L : Type*} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] + (f : K →ₐ[F] L) [Algebra.EssFiniteType F L] : Algebra.EssFiniteType F K := by + let := RingHom.toAlgebra f.toRingHom + exact Algebra.EssFiniteType.of_isScalarTower F K L + +theorem IntermediateField.fg_of_le + {K L : Type*} [Field K] [Field L] [Algebra K L] (F E : IntermediateField K L) + (hFE : F ≤ E) (hE : E.FG) : F.FG := by + rw [← IntermediateField.essFiniteType_iff] at hE ⊢ + exact Algebra.EssFiniteType.of_algHom (IntermediateField.inclusion hFE) + +theorem Field.fg_of_algebra (K L : Type*) [Field K] [Field L] [Algebra K L] [Field.FG L] : + Field.FG K := by + rw [Field.fg_iff_fg_top_bot] at * + sorry + namespace AlgebraicIndependent variable (R A) [FaithfulSMul R A] From dfdcb07d39d6086931d997d289c51afa2d5eff90 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Wed, 6 May 2026 10:20:44 +0100 Subject: [PATCH 2/4] add --- .../TranscendenceBasis.lean | 22 +++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean b/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean index 56cd4be0ba85ca..a8f8c81bbc6603 100644 --- a/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean +++ b/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean @@ -252,8 +252,26 @@ theorem Algebra.EssFiniteType.of_isScalarTower Algebra.EssFiniteType F K := by obtain ⟨bFK, hbFK⟩ := exists_isTranscendenceBasis F K obtain ⟨bKL, hbKL⟩ := exists_isTranscendenceBasis K L - have := hbFK.sumElim_comp hbKL - -- idea: L is finite over F adjoin hbFK ∪ hbKL + let bFKL := algebraMap K L '' bFK + let bFL := bKL ∪ bFKL + have : Algebra.IsAlgebraic (IntermediateField.adjoin F bFL) L := by + suffices bFL = range (Sum.elim Subtype.val (algebraMap K L ∘ Subtype.val)) by + convert IsTranscendenceBasis.isAlgebraic_field (hbFK.sumElim_comp hbKL) + simp_rw [Sum.elim_range, range_comp, Subtype.range_coe_subtype, setOf_mem_eq, bFL, bFKL] + have : EssFiniteType (IntermediateField.adjoin F bFL) L := + .of_comp F (IntermediateField.adjoin F bFL) L + have : FiniteDimensional (IntermediateField.adjoin F bFL) L := + finite_of_essFiniteType_of_isAlgebraic + have h1 : IntermediateField.adjoin F bFL ≤ (IntermediateField.adjoin K bKL).restrictScalars F := by + sorry + -- figure out the best places for these things to live + -- and locate "adjoining transcendental elements won't affect the degree" + let f : IntermediateField.adjoin F bFL →ₐ[F] IntermediateField.adjoin K bKL := + IntermediateField.inclusion h1 + let := f.toAlgebra + have : FiniteDimensional (IntermediateField.adjoin F bFL) (IntermediateField.adjoin K bKL) := by + sorry + -- idea: L is finite over F adjoin hbFK ∪ hbKL (done) -- K adjoin hbKL is finite over F adjoin hbFK ∪ hbKL -- K is algebraic over F adjoin hbFK -- but adjoining transcendental elements won't affect the degree From fb1157e605d5d369c71ba5ea04cf08a16c96e015 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Wed, 6 May 2026 13:12:46 +0100 Subject: [PATCH 3/4] temp --- .../AlgebraicIndependent/TranscendenceBasis.lean | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean b/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean index a8f8c81bbc6603..e1d8b5ae3d5a2b 100644 --- a/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean +++ b/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean @@ -256,12 +256,22 @@ theorem Algebra.EssFiniteType.of_isScalarTower let bFL := bKL ∪ bFKL have : Algebra.IsAlgebraic (IntermediateField.adjoin F bFL) L := by suffices bFL = range (Sum.elim Subtype.val (algebraMap K L ∘ Subtype.val)) by - convert IsTranscendenceBasis.isAlgebraic_field (hbFK.sumElim_comp hbKL) - simp_rw [Sum.elim_range, range_comp, Subtype.range_coe_subtype, setOf_mem_eq, bFL, bFKL] + rw [this] + exact (hbFK.sumElim_comp hbKL).isAlgebraic_field + simp [range_comp, bFL, bFKL] have : EssFiniteType (IntermediateField.adjoin F bFL) L := .of_comp F (IntermediateField.adjoin F bFL) L have : FiniteDimensional (IntermediateField.adjoin F bFL) L := finite_of_essFiniteType_of_isAlgebraic + -- todo: K adjoin bKL is finite dimensional over F adjoint bFL + have : Algebra.IsAlgebraic (IntermediateField.adjoin F bFK) K := by + suffices bFK = range Subtype.val by + rw [this] + exact hbFK.isAlgebraic_field + simp + + + have h1 : IntermediateField.adjoin F bFL ≤ (IntermediateField.adjoin K bKL).restrictScalars F := by sorry -- figure out the best places for these things to live From 253be559dfa4e59ecebb241dc5aacd6bbecd3f8c Mon Sep 17 00:00:00 2001 From: tb65536 Date: Wed, 6 May 2026 16:24:25 +0100 Subject: [PATCH 4/4] revert --- .../TranscendenceBasis.lean | 60 ------------------- 1 file changed, 60 deletions(-) diff --git a/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean b/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean index e1d8b5ae3d5a2b..1b261c9e579b6f 100644 --- a/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean +++ b/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean @@ -246,66 +246,6 @@ theorem IsTranscendenceBasis.isAlgebraic_field {F E : Type*} {x : ι → E} IsScalarTower.of_algebraMap_eq (congrFun rfl) exact Algebra.IsAlgebraic.extendScalars (R := adjoin F S) (Subalgebra.inclusion_injective _) -theorem Algebra.EssFiniteType.of_isScalarTower - (F K L : Type*) [Field F] [Field K] [Field L] [Algebra F K] [Algebra K L] - [Algebra F L] [IsScalarTower F K L] [Algebra.EssFiniteType F L] : - Algebra.EssFiniteType F K := by - obtain ⟨bFK, hbFK⟩ := exists_isTranscendenceBasis F K - obtain ⟨bKL, hbKL⟩ := exists_isTranscendenceBasis K L - let bFKL := algebraMap K L '' bFK - let bFL := bKL ∪ bFKL - have : Algebra.IsAlgebraic (IntermediateField.adjoin F bFL) L := by - suffices bFL = range (Sum.elim Subtype.val (algebraMap K L ∘ Subtype.val)) by - rw [this] - exact (hbFK.sumElim_comp hbKL).isAlgebraic_field - simp [range_comp, bFL, bFKL] - have : EssFiniteType (IntermediateField.adjoin F bFL) L := - .of_comp F (IntermediateField.adjoin F bFL) L - have : FiniteDimensional (IntermediateField.adjoin F bFL) L := - finite_of_essFiniteType_of_isAlgebraic - -- todo: K adjoin bKL is finite dimensional over F adjoint bFL - have : Algebra.IsAlgebraic (IntermediateField.adjoin F bFK) K := by - suffices bFK = range Subtype.val by - rw [this] - exact hbFK.isAlgebraic_field - simp - - - - have h1 : IntermediateField.adjoin F bFL ≤ (IntermediateField.adjoin K bKL).restrictScalars F := by - sorry - -- figure out the best places for these things to live - -- and locate "adjoining transcendental elements won't affect the degree" - let f : IntermediateField.adjoin F bFL →ₐ[F] IntermediateField.adjoin K bKL := - IntermediateField.inclusion h1 - let := f.toAlgebra - have : FiniteDimensional (IntermediateField.adjoin F bFL) (IntermediateField.adjoin K bKL) := by - sorry - -- idea: L is finite over F adjoin hbFK ∪ hbKL (done) - -- K adjoin hbKL is finite over F adjoin hbFK ∪ hbKL - -- K is algebraic over F adjoin hbFK - -- but adjoining transcendental elements won't affect the degree - -- so K is finite over F adjoin hbFK - -- so K is finitely generated over F - sorry - -theorem Algebra.EssFiniteType.of_algHom - {F K L : Type*} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] - (f : K →ₐ[F] L) [Algebra.EssFiniteType F L] : Algebra.EssFiniteType F K := by - let := RingHom.toAlgebra f.toRingHom - exact Algebra.EssFiniteType.of_isScalarTower F K L - -theorem IntermediateField.fg_of_le - {K L : Type*} [Field K] [Field L] [Algebra K L] (F E : IntermediateField K L) - (hFE : F ≤ E) (hE : E.FG) : F.FG := by - rw [← IntermediateField.essFiniteType_iff] at hE ⊢ - exact Algebra.EssFiniteType.of_algHom (IntermediateField.inclusion hFE) - -theorem Field.fg_of_algebra (K L : Type*) [Field K] [Field L] [Algebra K L] [Field.FG L] : - Field.FG K := by - rw [Field.fg_iff_fg_top_bot] at * - sorry - namespace AlgebraicIndependent variable (R A) [FaithfulSMul R A]