UnramifiedPolynomial.lean

1 import PaperXI.MonicResidueAlgebra
2 import Mathlib.RingTheory.DiscreteValuationRing.TFAE
3 import Mathlib.RingTheory.LocalRing.Etale
4 import Mathlib.RingTheory.Smooth.Fiber
5 import Mathlib.RingTheory.RamificationInertia.Ramification
6 import Mathlib.LinearAlgebra.Dimension.Localization
7 import Mathlib.RingTheory.Localization.FractionRing
8 import Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
9 
10 /-! An irreducible residue polynomial constructs a finite etale DVR and its
11 actual fraction field, without any supplied ambient Galois extension. -/
12 set_option autoImplicit false
13 noncomputable section
14 namespace PaperXI.UnramifiedPolynomial
15 open Polynomial IsLocalRing
16 open PaperXI.MonicResidueAlgebra
17 variable {R : Type*} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
18 variable (f : R[X]) [hm : Fact f.Monic]
19 variable [hi : Fact (Irreducible (f.map (residue R)))]
20 
21 theorem irreducible : Irreducible f :=
22   Polynomial.Monic.irreducible_of_irreducible_map (residue R) f hm.out hi.out
23 
24 instance domain : IsDomain (AdjoinRoot f) :=
25   AdjoinRoot.isDomain_of_prime ((irreducible_iff_prime).mp (irreducible f))
26 
27 instance faithful : FaithfulSMul R (AdjoinRoot f) :=
28   AdjoinRoot.faithfulSMul_of_monic_of_degree_pos hm.out (degree_pos f)
29 
30 theorem not_field : ¬ IsField (AdjoinRoot f) := by
31   intro h
32   have : IsField R := IsLocalHom.isField
33     (f := algebraMap R (AdjoinRoot f)) (FaithfulSMul.algebraMap_injective _ _) h
34   exact IsDiscreteValuationRing.not_isField R this
35 
36 /-- The monogenic local domain is a DVR, rather than merely a free module. -/
37 instance dvr : IsDiscreteValuationRing (AdjoinRoot f) := by
38   apply ((IsDiscreteValuationRing.TFAE (AdjoinRoot f) (not_field f)).out 5 1).mp
39   obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible R
40   rw [maximalIdeal_eq, specialIdeal, hπ.maximalIdeal_eq, Ideal.map_span, Set.image_singleton]
41   infer_instance
42 
43 /-- The uniformizer is unchanged. -/
44 theorem uniformizer (π : R) (hπ : Ideal.span {π} = maximalIdeal R) :
45     Ideal.span {algebraMap R (AdjoinRoot f) π} = maximalIdeal (AdjoinRoot f) := by
46   rw [maximalIdeal_eq, specialIdeal, ← hπ, Ideal.map_span, Set.image_singleton]
47 
48 
49 /-- The constructed upper field is the fraction field of the actual root DVR. -/
50 abbrev field := FractionRing (AdjoinRoot f)
51 
52 instance baseFieldAlgebra : Algebra (FractionRing R) (field f) :=
53   FractionRing.liftAlgebra R (field f)
54 
55 instance baseFieldTower : IsScalarTower R (FractionRing R) (field f) :=
56   FractionRing.isScalarTower_liftAlgebra R (field f)
57 
58 theorem natDegree_pos_of_residue_irreducible :
59     0 < f.natDegree :=
60   Polynomial.natDegree_pos_iff_degree_pos.mpr (degree_pos f)
61 
62 theorem field_degree : Module.finrank (FractionRing R) (field f) = f.natDegree := by
63   rw [IsFractionRing.finrank_eq R (FractionRing R) (AdjoinRoot f) (field f)]
64   exact MonicResidueAlgebra.rank f
65 
66 instance finiteFieldExtension : FiniteDimensional (FractionRing R) (field f) :=
67   .of_finrank_pos ((field_degree f).symm ▸ natDegree_pos_of_residue_irreducible f)
68 
69 
70 
71 theorem integralClosure : IsIntegralClosure (AdjoinRoot f) R (field f) := by
72   let := AdjoinRoot.isIntegral_of_monic hm.out
73   infer_instance
74 
75 variable [Finite (ResidueField R)]
76 
77 /-- Finite presentation, flatness and the separable residue identify the actual etale predicate. -/
78 theorem etale : Algebra.Etale R (AdjoinRoot f) := by
79   let : Algebra.FormallyUnramified R (AdjoinRoot f) :=
80     Algebra.FormallyUnramified.of_map_maximalIdeal (maximalIdeal_eq f).symm
81   let : Algebra.FinitePresentation R (AdjoinRoot f) :=
82     Algebra.FinitePresentation.of_finiteType.mp inferInstance
83   exact Algebra.Etale.of_formallyUnramified_of_flat
84 
85 theorem ramificationIdx_one :
86     (maximalIdeal (AdjoinRoot f)).ramificationIdx R = 1 := by
87   let := etale f
88   exact Ideal.ramificationIdx_eq_one _ _
89 
90 end PaperXI.UnramifiedPolynomial

Back to source controls