From c954df28facb8bac2b39b579c1c54a27ae16511b Mon Sep 17 00:00:00 2001 From: negiizhao Date: Thu, 27 Jul 2023 01:08:20 +0000 Subject: [PATCH] chore(FieldTheory/Adjoin): remove unnecessary assumptions in `minpolynatDegree_le` and `minpoly.degree_le` (#6152) Also - fix the names of `minpoly.natDegree_le` and `minpoly.degree_le` - rename `minpoly.ne_zero_of_finite_field_extension` to `minpoly.ne_zero_of_finite` - reduce typeclass assumptions of some lemmas in `RingTheory/Algebraic` - add two lemmas `isIntegral_of_finite` and `isAlgebraic_of_finite` - move `Algebra.isIntegral_of_finite` to `RingTheory/IntegralClosure` --- Mathlib/FieldTheory/Adjoin.lean | 13 +-- Mathlib/FieldTheory/IsAlgClosed/Basic.lean | 4 +- Mathlib/FieldTheory/Minpoly/Field.lean | 8 +- .../NumberTheory/NumberField/Embeddings.lean | 4 +- Mathlib/RingTheory/Algebraic.lean | 94 ++++++++++++------- Mathlib/RingTheory/IntegralClosure.lean | 20 ++++ 6 files changed, 97 insertions(+), 46 deletions(-) diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean index b2d7133f1ac99..35172fe813dd7 100644 --- a/Mathlib/FieldTheory/Adjoin.lean +++ b/Mathlib/FieldTheory/Adjoin.lean @@ -884,15 +884,16 @@ theorem adjoin.finrank {x : L} (hx : IsIntegral K x) : rfl #align intermediate_field.adjoin.finrank IntermediateField.adjoin.finrank -theorem minpoly.natDegree_le {x : L} [FiniteDimensional K L] (hx : IsIntegral K x) : +theorem _root_.minpoly.natDegree_le (x : L) [FiniteDimensional K L] : (minpoly K x).natDegree ≤ finrank K L := - le_of_eq_of_le (IntermediateField.adjoin.finrank hx).symm K⟮x⟯.toSubmodule.finrank_le -#align minpoly.nat_degree_le IntermediateField.minpoly.natDegree_le + le_of_eq_of_le (IntermediateField.adjoin.finrank (isIntegral_of_finite _ _)).symm + K⟮x⟯.toSubmodule.finrank_le +#align minpoly.nat_degree_le minpoly.natDegree_le -theorem minpoly.degree_le {x : L} [FiniteDimensional K L] (hx : IsIntegral K x) : +theorem _root_.minpoly.degree_le (x : L) [FiniteDimensional K L] : (minpoly K x).degree ≤ finrank K L := - degree_le_of_natDegree_le (minpoly.natDegree_le hx) -#align minpoly.degree_le IntermediateField.minpoly.degree_le + degree_le_of_natDegree_le (minpoly.natDegree_le x) +#align minpoly.degree_le minpoly.degree_le end PowerBasis diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean index 1a234768ea4a3..9c7aabb9ae750 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean @@ -309,7 +309,7 @@ theorem maximalSubfieldWithHom_eq_top : (maximalSubfieldWithHom K L M).carrier = letI : Algebra N M := (maximalSubfieldWithHom K L M).emb.toRingHom.toAlgebra obtain ⟨y, hy⟩ := IsAlgClosed.exists_aeval_eq_zero M (minpoly N x) <| (minpoly.degree_pos - (isAlgebraic_iff_isIntegral.1 (Algebra.isAlgebraic_of_larger_base _ _ hL x))).ne' + (isAlgebraic_iff_isIntegral.1 (Algebra.isAlgebraic_of_larger_base _ hL x))).ne' let O : Subalgebra N L := Algebra.adjoin N {(x : L)} letI : Algebra N O := Subalgebra.algebra O -- Porting note: there are some tricky unfolds going on here: @@ -549,7 +549,7 @@ theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly {F K} (A) [Field F] [F haveI : IsScalarTower F Fx A := IsScalarTower.of_ring_hom (AdjoinRoot.liftHom _ a ha) haveI : IsScalarTower F Fx K := IsScalarTower.of_ring_hom (AdjoinRoot.liftHom _ x hx) haveI : Fact (Irreducible <| minpoly F x) := ⟨minpoly.irreducible <| hFK x⟩ - let ψ₀ : K →ₐ[Fx] A := IsAlgClosed.lift (Algebra.isAlgebraic_of_larger_base F Fx hK) + let ψ₀ : K →ₐ[Fx] A := IsAlgClosed.lift (Algebra.isAlgebraic_of_larger_base Fx hK) exact ⟨ψ₀.restrictScalars F, (congr_arg ψ₀ (AdjoinRoot.lift_root hx).symm).trans <| diff --git a/Mathlib/FieldTheory/Minpoly/Field.lean b/Mathlib/FieldTheory/Minpoly/Field.lean index 8fa4f85d6a599..dd81c4e300824 100644 --- a/Mathlib/FieldTheory/Minpoly/Field.lean +++ b/Mathlib/FieldTheory/Minpoly/Field.lean @@ -42,9 +42,9 @@ theorem degree_le_of_ne_zero {p : A[X]} (pnz : p ≠ 0) (hp : Polynomial.aeval x _ = degree p := degree_mul_leadingCoeff_inv p pnz #align minpoly.degree_le_of_ne_zero minpoly.degree_le_of_ne_zero -theorem ne_zero_of_finite_field_extension (e : B) [FiniteDimensional A B] : minpoly A e ≠ 0 := - minpoly.ne_zero <| isIntegral_of_noetherian (IsNoetherian.iff_fg.2 inferInstance) _ -#align minpoly.ne_zero_of_finite_field_extension minpoly.ne_zero_of_finite_field_extension +theorem ne_zero_of_finite (e : B) [FiniteDimensional A B] : minpoly A e ≠ 0 := + minpoly.ne_zero <| isIntegral_of_finite _ _ +#align minpoly.ne_zero_of_finite_field_extension minpoly.ne_zero_of_finite /-- The minimal polynomial of an element `x` is uniquely characterized by its defining property: if there is another monic polynomial of minimal degree that has `x` as a root, then this polynomial @@ -178,7 +178,7 @@ def rootsOfMinPolyPiType (φ : E →ₐ[F] K) (x : range (FiniteDimensional.finBasis F E : _ → E)) : { l : K // l ∈ (((minpoly F x.1).map (algebraMap F K)).roots : Multiset K) } := ⟨φ x, by - rw [mem_roots_map (minpoly.ne_zero_of_finite_field_extension F x.val), + rw [mem_roots_map (minpoly.ne_zero_of_finite F x.val), ← aeval_def, aeval_algHom_apply, minpoly.aeval, map_zero]⟩ #align minpoly.roots_of_min_poly_pi_type minpoly.rootsOfMinPolyPiType diff --git a/Mathlib/NumberTheory/NumberField/Embeddings.lean b/Mathlib/NumberTheory/NumberField/Embeddings.lean index b5a2742268a88..af25bd5afc7a3 100644 --- a/Mathlib/NumberTheory/NumberField/Embeddings.lean +++ b/Mathlib/NumberTheory/NumberField/Embeddings.lean @@ -89,7 +89,7 @@ theorem coeff_bdd_of_norm_le {B : ℝ} {x : K} (h : ∀ φ : K →+* A, ‖φ x have hx := IsSeparable.isIntegral ℚ x rw [← norm_algebraMap' A, ← coeff_map (algebraMap ℚ A)] refine coeff_bdd_of_roots_le _ (minpoly.monic hx) - (IsAlgClosed.splits_codomain _) (IntermediateField.minpoly.natDegree_le hx) (fun z hz => ?_) i + (IsAlgClosed.splits_codomain _) (minpoly.natDegree_le x) (fun z hz => ?_) i classical rw [← Multiset.mem_toFinset] at hz obtain ⟨φ, rfl⟩ := (range_eval_eq_rootSet_minpoly K A x).symm.subset hz @@ -107,7 +107,7 @@ theorem finite_of_norm_le (B : ℝ) : {x : K | IsIntegral ℤ x ∧ ∀ φ : K have h_map_ℚ_minpoly := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx.1 refine ⟨_, ⟨?_, fun i => ?_⟩, mem_rootSet.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩ · rw [← (minpoly.monic hx.1).natDegree_map (algebraMap ℤ ℚ), ← h_map_ℚ_minpoly] - exact IntermediateField.minpoly.natDegree_le (isIntegral_of_isScalarTower hx.1) + exact minpoly.natDegree_le x rw [mem_Icc, ← abs_le, ← @Int.cast_le ℝ] refine (Eq.trans_le ?_ <| coeff_bdd_of_norm_le hx.2 i).trans (Nat.le_ceil _) rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs] diff --git a/Mathlib/RingTheory/Algebraic.lean b/Mathlib/RingTheory/Algebraic.lean index e395ee7d9f644..d47cbb9c0ae30 100644 --- a/Mathlib/RingTheory/Algebraic.lean +++ b/Mathlib/RingTheory/Algebraic.lean @@ -199,31 +199,23 @@ protected theorem Algebra.isAlgebraic_iff_isIntegral : end Field -namespace Algebra +section variable {K : Type _} {L : Type _} {R : Type _} {S : Type _} {A : Type _} -variable [Field K] [Field L] [CommRing R] [CommRing S] [CommRing A] +section Ring -variable [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A] +section CommRing -variable [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] +variable [CommRing R] [CommRing S] [Ring A] -/-- If L is an algebraic field extension of K and A is an algebraic algebra over L, -then A is algebraic over K. -/ -theorem isAlgebraic_trans (L_alg : IsAlgebraic K L) (A_alg : IsAlgebraic L A) : - IsAlgebraic K A := by - simp only [IsAlgebraic, isAlgebraic_iff_isIntegral] at L_alg A_alg ⊢ - exact isIntegral_trans L_alg A_alg -#align algebra.is_algebraic_trans Algebra.isAlgebraic_trans - -variable (K L) +variable [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] /-- If x is algebraic over R, then x is algebraic over S when S is an extension of R, and the map from `R` to `S` is injective. -/ -theorem _root_.isAlgebraic_of_larger_base_of_injective +theorem isAlgebraic_of_larger_base_of_injective (hinj : Function.Injective (algebraMap R S)) {x : A} - (A_alg : _root_.IsAlgebraic R x) : _root_.IsAlgebraic S x := + (A_alg : IsAlgebraic R x) : IsAlgebraic S x := let ⟨p, hp₁, hp₂⟩ := A_alg ⟨p.map (algebraMap _ _), by rwa [Ne.def, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot], by simpa⟩ @@ -231,35 +223,71 @@ theorem _root_.isAlgebraic_of_larger_base_of_injective /-- If A is an algebraic algebra over R, then A is algebraic over S when S is an extension of R, and the map from `R` to `S` is injective. -/ -theorem isAlgebraic_of_larger_base_of_injective (hinj : Function.Injective (algebraMap R S)) +theorem Algebra.isAlgebraic_of_larger_base_of_injective (hinj : Function.Injective (algebraMap R S)) (A_alg : IsAlgebraic R A) : IsAlgebraic S A := fun x => _root_.isAlgebraic_of_larger_base_of_injective hinj (A_alg x) #align algebra.is_algebraic_of_larger_base_of_injective Algebra.isAlgebraic_of_larger_base_of_injective +end CommRing + +section Field + +variable [Field K] [Field L] [Ring A] + +variable [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A] + +variable (L) + /-- If x is algebraic over K, then x is algebraic over L when L is an extension of K -/ -theorem _root_.isAlgebraic_of_larger_base {x : A} (A_alg : _root_.IsAlgebraic K x) : - _root_.IsAlgebraic L x := - _root_.isAlgebraic_of_larger_base_of_injective (algebraMap K L).injective A_alg +theorem isAlgebraic_of_larger_base {x : A} (A_alg : IsAlgebraic K x) : + IsAlgebraic L x := + isAlgebraic_of_larger_base_of_injective (algebraMap K L).injective A_alg #align is_algebraic_of_larger_base isAlgebraic_of_larger_base /-- If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K -/ -theorem isAlgebraic_of_larger_base (A_alg : IsAlgebraic K A) : IsAlgebraic L A := +theorem Algebra.isAlgebraic_of_larger_base (A_alg : IsAlgebraic K A) : IsAlgebraic L A := isAlgebraic_of_larger_base_of_injective (algebraMap K L).injective A_alg #align algebra.is_algebraic_of_larger_base Algebra.isAlgebraic_of_larger_base -/-- A field extension is integral if it is finite. -/ -theorem isIntegral_of_finite [FiniteDimensional K L] : Algebra.IsIntegral K L := fun x => - isIntegral_of_submodule_noetherian ⊤ (IsNoetherian.iff_fg.2 inferInstance) x Algebra.mem_top -#align algebra.is_integral_of_finite Algebra.isIntegral_of_finite +variable (K) + +theorem isAlgebraic_of_finite (e : A) [FiniteDimensional K A] : IsAlgebraic K e := + isAlgebraic_iff_isIntegral.mpr (isIntegral_of_finite K e) + +variable (A) /-- A field extension is algebraic if it is finite. -/ -theorem isAlgebraic_of_finite [FiniteDimensional K L] : IsAlgebraic K L := - Algebra.isAlgebraic_iff_isIntegral.mpr (isIntegral_of_finite K L) +theorem Algebra.isAlgebraic_of_finite [FiniteDimensional K A] : IsAlgebraic K A := + Algebra.isAlgebraic_iff_isIntegral.mpr (isIntegral_of_finite K A) #align algebra.is_algebraic_of_finite Algebra.isAlgebraic_of_finite -variable {K L} +end Field + +end Ring + +section CommRing + +variable [Field K] [Field L] [CommRing A] + +variable [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A] -theorem IsAlgebraic.algHom_bijective (ha : Algebra.IsAlgebraic K L) (f : L →ₐ[K] L) : +/-- If L is an algebraic field extension of K and A is an algebraic algebra over L, +then A is algebraic over K. -/ +theorem Algebra.isAlgebraic_trans (L_alg : IsAlgebraic K L) (A_alg : IsAlgebraic L A) : + IsAlgebraic K A := by + simp only [IsAlgebraic, isAlgebraic_iff_isIntegral] at L_alg A_alg ⊢ + exact isIntegral_trans L_alg A_alg +#align algebra.is_algebraic_trans Algebra.isAlgebraic_trans + +end CommRing + +section Field + +variable [Field K] [Field L] + +variable [Algebra K L] + +theorem Algebra.IsAlgebraic.algHom_bijective (ha : Algebra.IsAlgebraic K L) (f : L →ₐ[K] L) : Function.Bijective f := by refine' ⟨f.toRingHom.injective, fun b => _⟩ obtain ⟨p, hp, he⟩ := ha b @@ -271,7 +299,7 @@ theorem IsAlgebraic.algHom_bijective (ha : Algebra.IsAlgebraic K L) (f : L → exact ⟨a, Subtype.ext_iff.1 ha⟩ #align algebra.is_algebraic.alg_hom_bijective Algebra.IsAlgebraic.algHom_bijective -theorem _root_.AlgHom.bijective [FiniteDimensional K L] (ϕ : L →ₐ[K] L) : Function.Bijective ϕ := +theorem AlgHom.bijective [FiniteDimensional K L] (ϕ : L →ₐ[K] L) : Function.Bijective ϕ := (Algebra.isAlgebraic_of_finite K L).algHom_bijective ϕ #align alg_hom.bijective AlgHom.bijective @@ -279,7 +307,7 @@ variable (K L) /-- Bijection between algebra equivalences and algebra homomorphisms -/ @[simps] -noncomputable def IsAlgebraic.algEquivEquivAlgHom (ha : Algebra.IsAlgebraic K L) : +noncomputable def Algebra.IsAlgebraic.algEquivEquivAlgHom (ha : Algebra.IsAlgebraic K L) : (L ≃ₐ[K] L) ≃* (L →ₐ[K] L) where toFun ϕ := ϕ.toAlgHom invFun ϕ := AlgEquiv.ofBijective ϕ (ha.algHom_bijective ϕ) @@ -294,12 +322,14 @@ noncomputable def IsAlgebraic.algEquivEquivAlgHom (ha : Algebra.IsAlgebraic K L) /-- Bijection between algebra equivalences and algebra homomorphisms -/ @[reducible] -noncomputable def _root_.algEquivEquivAlgHom [FiniteDimensional K L] : +noncomputable def algEquivEquivAlgHom [FiniteDimensional K L] : (L ≃ₐ[K] L) ≃* (L →ₐ[K] L) := (Algebra.isAlgebraic_of_finite K L).algEquivEquivAlgHom K L #align alg_equiv_equiv_alg_hom algEquivEquivAlgHom -end Algebra +end Field + +end variable {R S : Type _} [CommRing R] [IsDomain R] [CommRing S] diff --git a/Mathlib/RingTheory/IntegralClosure.lean b/Mathlib/RingTheory/IntegralClosure.lean index c045aa282c1b8..811ea825f437c 100644 --- a/Mathlib/RingTheory/IntegralClosure.lean +++ b/Mathlib/RingTheory/IntegralClosure.lean @@ -115,6 +115,26 @@ end Ring section +variable {K A : Type _} + +variable [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] + +variable (K) + +theorem isIntegral_of_finite (e : A) : IsIntegral K e := + isIntegral_of_noetherian (IsNoetherian.iff_fg.2 inferInstance) _ + +variable (A) + +/-- A field extension is integral if it is finite. -/ +theorem Algebra.isIntegral_of_finite : Algebra.IsIntegral K A := fun x => + isIntegral_of_submodule_noetherian ⊤ (IsNoetherian.iff_fg.2 inferInstance) x Algebra.mem_top +#align algebra.is_integral_of_finite Algebra.isIntegral_of_finite + +end + +section + variable {R A B S : Type _} variable [CommRing R] [CommRing A] [CommRing B] [CommRing S]