LiftedEtale.lean

1 import PaperXI.LiftedValuationFinite
2 import PaperXI.LocalResidueRank
3 
4 /-! Actual finite-etale and ramification-index endpoints for the Hensel-generated
5 field over a DVR base. All ring/module properties are derived. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.LiftedEtale
9 open IsLocalRing PaperXI.LiftedResidueDegree PaperXI.LiftedFullResidue
10 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
11 variable (A : ValuationSubring L) [HenselianLocalRing A] [Fintype (ResidueField A)]
12 variable [FiniteDimensional K L] [IsGalois K L]
13 variable (stable : ∀ g : L ≃ₐ[K] L, g ∈ A.decompositionSubgroup K)
14 variable (s : IntermediateField (BaseResidue K A) (ResidueField A))
15 variable [IsDiscreteValuationRing (A.comap (algebraMap K L))]
16 
17 include stable
18 
19 /-- Construct a finite free integral valuation ring over the actual DVR base. -/
20 theorem free : Module.Free (A.comap (algebraMap K L)) (valuation K A s) := by
21   let := galois K A stable s
22   let := LiftedValuationFinite.integralClosure K A stable s
23   exact IsIntegralClosure.module_free (A.comap (algebraMap K L)) K
24     (field K A s) (valuation K A s)
25 
26 /-- Full residue equivalence for the canonical quotient module action.
27 This explicitly resolves the residue-module versus algebra-module typeclass path. -/
28 def canonicalResidueLinearEquiv :
29     ResidueField (valuation K A s) ≃ₗ[BaseResidue K A] s :=
30   { (residueEquiv K A s stable).toAddEquiv with
31     map_smul' := fun a x => by
32       obtain ⟨a, rfl⟩ := residue_surjective a
33       obtain ⟨x, rfl⟩ := residue_surjective x
34       apply Subtype.ext
35       rfl }
36 
37 /-- Field degree and full residue degree exhaust the integral rank. -/
38 theorem rank_residue :
39     Module.finrank (A.comap (algebraMap K L)) (valuation K A s) =
40       Module.finrank (BaseResidue K A) (ResidueField (valuation K A s)) := by
41   rw [(canonicalResidueLinearEquiv K A stable s).finrank_eq]
42   exact (LiftedValuationFinite.rank K A stable s).trans (degree K A stable s)
43 
44 /-- The actual maximal ideal is the extension of the base maximal ideal. -/
45 theorem maximalIdeal_map :
46     (maximalIdeal (A.comap (algebraMap K L))).map
47       (algebraMap (A.comap (algebraMap K L)) (valuation K A s)) =
48     maximalIdeal (valuation K A s) := by
49   let := LiftedValuationFinite.finite K A stable s
50   let := free K A stable s
51   exact LocalResidueRank.map_maximal_of_rank _ _ (rank_residue K A stable s)
52 
53 /-- Algebra.Etale is instantiated on the actual restricted valuation rings. -/
54 theorem etale : Algebra.Etale (A.comap (algebraMap K L)) (valuation K A s) := by
55   let := LiftedValuationFinite.finite K A stable s
56   let := free K A stable s
57   have : Finite (BaseResidue K A) := Finite.of_injective
58     (ValuationResidueEmbedding.residueMap A (algebraMap K L))
59     (ValuationResidueEmbedding.residueMap_injective A (algebraMap K L))
60   let : Algebra.FinitePresentation (A.comap (algebraMap K L)) (valuation K A s) :=
61     Algebra.FinitePresentation.of_finiteType.mp inferInstance
62   exact LocalResidueRank.etale _ _ (rank_residue K A stable s)
63 
64 /-- The library ramification index, not a new predicate with that name. -/
65 theorem ramificationIdx_one :
66     (maximalIdeal (valuation K A s)).ramificationIdx
67       (A.comap (algebraMap K L)) = 1 := by
68   let := etale K A stable s
69   exact Ideal.ramificationIdx_eq_one _ _
70 
71 /-- Every chosen generator of the base maximal ideal remains a generator upstairs. -/
72 theorem uniformizer_ideal (π : A.comap (algebraMap K L))
73     (hπ : Ideal.span {π} = maximalIdeal (A.comap (algebraMap K L))) :
74     Ideal.span {algebraMap (A.comap (algebraMap K L)) (valuation K A s) π} =
75       maximalIdeal (valuation K A s) := by
76   rw [← maximalIdeal_map K A stable s, ← hπ, Ideal.map_span, Set.image_singleton]
77 
78 /-- A genuine monogenic finite-etale presentation exists; its derivative is a unit.
79 The generator and polynomial are derived, not passed in as certificates. -/
80 theorem monogenic : ∃ β : valuation K A s,
81     Algebra.adjoin (A.comap (algebraMap K L)) {β} = ⊤ ∧
82     IsUnit (Polynomial.aeval β (minpoly (A.comap (algebraMap K L)) β).derivative) := by
83   let := LiftedValuationFinite.finite K A stable s
84   let := etale K A stable s
85   have : FaithfulSMul (A.comap (algebraMap K L)) (valuation K A s) :=
86     (faithfulSMul_iff_algebraMap_injective _ _).mpr
87       (by
88         intro x y h
89         apply Subtype.ext
90         exact (algebraMap K (field K A s)).injective (congrArg (fun a : valuation K A s => (a : field K A s)) h))
91   obtain ⟨β, hβ⟩ := IsLocalRing.exists_adjoin_eq_top
92     (R := A.comap (algebraMap K L)) (S := valuation K A s)
93   exact ⟨β, hβ, IsLocalRing.isUnit_aeval_derivative_minpoly_of_adjoin_eq_top hβ⟩
94 
95 end PaperXI.LiftedEtale

Back to source controls