TameAbhyankar.finiteUnramifiedExtension_algEquiv
Finite unramifiedness is invariant under a valuation-preserving algebra equivalence.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations
open DiscreteValuationField.FieldCompositumLean source · full declaration
theorem finiteUnramifiedExtension_algEquiv
{K A B : Type*} [Field K] [Field A] [Field B]
[Algebra K A] [Algebra K B] [FiniteDimensional K A]
(e : A ≃ₐ[K] B)
(v : LubinTate.Valuations.ExponentialValuation K)
(wA : LubinTate.Valuations.ExponentialValuation A)
(wB : LubinTate.Valuations.ExponentialValuation B)
(hKA : ∀ a : K, wA (algebraMap K A a) = v a)
(hKB : ∀ a : K, wB (algebraMap K B a) = v a)
(he : ∀ x : A, wB (e x) = wA x)
(hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
(LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
(hA : FiniteUnramifiedExtension v wA hKA) :
letI : FiniteDimensional K B := e.toLinearEquiv.finiteDimensional
FiniteUnramifiedExtension v wB hKB := by
classical
let : FiniteDimensional K B := e.toLinearEquiv.finiteDimensional
let V := LubinTate.Valuations.exponentialValuationSubring v
obtain ⟨a, F, haGen, hFfield, _hFresidueMinpoly,
hFreduction, _haSeparable⟩ :=
exists_primitive_lift_minpoly_of_finiteUnramifiedExtension
v wA hKA hhens hA
let aB : LubinTate.Valuations.exponentialValuationSubring wB :=
⟨e (a : A), by
change (0 : WithTop ℝ) ≤ wB (e (a : A))
rw [he]
exact a.property⟩
have haGenBIF : IntermediateField.adjoin K ({(aB : B)} : Set B) = ⊤ := by
rw [show (aB : B) = e (a : A) from rfl]
rw [← Set.image_singleton]
change IntermediateField.adjoin K
(e.toAlgHom '' ({(a : A)} : Set A)) = ⊤
rw [← IntermediateField.adjoin_map, haGen]
ext x
constructor
· intro _hx
trivial
· intro _hx
exact ⟨e.symm x, by simp, e.apply_symm_apply x⟩
have haGenB : Algebra.adjoin K ({(aB : B)} : Set B) = ⊤ := by
apply Algebra.adjoin_eq_top_of_intermediateField
(fun x _hx ↦ Algebra.IsAlgebraic.isAlgebraic x)
exact haGenBIF
have hFmonic : F.Monic := by
have hmappedMonic : (F.map V.subtype).Monic := by
rw [hFfield]
exact minpoly.monic (Algebra.IsIntegral.isIntegral (a : A))
exact (V.subtype_injective.monic_map_iff (p := F)).2 hmappedMonic
have hFrootA :
(F.map ((algebraMap K A).comp V.subtype)).eval (a : A) = 0 := by
have hmin : Polynomial.aeval (a : A) (minpoly K (a : A)) = 0 :=
minpoly.aeval K (a : A)
rw [Polynomial.aeval_def, Polynomial.eval₂_eq_eval_map] at hmin
have hpoly :
F.map ((algebraMap K A).comp V.subtype) =
(F.map V.subtype).map (algebraMap K A) := by
rw [Polynomial.map_map]
rw [hpoly, hFfield]
exact hmin
have hFmapB :
F.map ((algebraMap K B).comp V.subtype) =
(F.map ((algebraMap K A).comp V.subtype)).map
e.toRingEquiv.toRingHom := by
rw [Polynomial.map_map]
apply Polynomial.ext
intro n
simp only [Polynomial.coeff_map, RingHom.coe_comp, Function.comp_apply]
exact (e.commutes (F.coeff n : K)).symm
have hFrootB :
(F.map ((algebraMap K B).comp V.subtype)).eval (aB : B) = 0 := by
rw [hFmapB]
change ((F.map ((algebraMap K A).comp V.subtype)).map
e.toRingEquiv.toRingHom).eval (e (a : A)) = 0
calc
_ = e ((F.map ((algebraMap K A).comp V.subtype)).eval (a : A)) :=
Polynomial.eval_map_apply e.toRingEquiv.toRingHom (a : A)
_ = e 0 := congrArg e hFrootA
_ = 0 := map_zero e
exact finiteUnramifiedExtension_of_primitive_separable_integral_model
v wB hKB hhens aB F hFmonic hFrootB hFreduction haGenB