LiftedValuationFinite.lean

1 import PaperXI.ValuationIntegralModel
2 import PaperXI.LiftedFullResidue
3 import Mathlib.FieldTheory.Normal.Basic
4 
5 /-! The Hensel-generated field has the actual finite integral valuation ring. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.LiftedValuationFinite
9 open scoped Pointwise
10 open IsLocalRing PaperXI.LiftedResidueDegree PaperXI.LiftedFullResidue
11 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
12 variable (A : ValuationSubring L) [HenselianLocalRing A] [Fintype (ResidueField A)]
13 variable [FiniteDimensional K L] [IsGalois K L]
14 variable (stable : ∀ g : L ≃ₐ[K] L, g ∈ A.decompositionSubgroup K)
15 variable (s : IntermediateField (BaseResidue K A) (ResidueField A))
16 
17 instance baseAlgebra : Algebra (A.comap (algebraMap K L)) (valuation K A s) := by
18   change Algebra (ValuationIntegralModel.base K (valuation K A s)) (valuation K A s)
19   infer_instance
20 instance baseTower : IsScalarTower (A.comap (algebraMap K L)) (valuation K A s) (field K A s) := by
21   change IsScalarTower (ValuationIntegralModel.base K (valuation K A s)) (valuation K A s) (field K A s)
22   infer_instance
23 instance baseFieldTower : IsScalarTower (A.comap (algebraMap K L)) K (field K A s) := by
24   change IsScalarTower (ValuationIntegralModel.base K (valuation K A s)) K (field K A s)
25   infer_instance
26 instance baseLocal : IsLocalHom (algebraMap (A.comap (algebraMap K L)) (valuation K A s)) := by
27   change IsLocalHom (algebraMap (ValuationIntegralModel.base K (valuation K A s)) (valuation K A s))
28   infer_instance
29 
30 include stable
31 
32 /-- Every automorphism of the constructed field preserves its restricted valuation.
33 Extend it to L; no additional valuation-invariance input for E is supplied. -/
34 theorem stable_valuation (σ : field K A s ≃ₐ[K] field K A s) :
35     σ ∈ (valuation K A s).decompositionSubgroup K := by
36   let := galois K A stable s
37   rw [MulAction.mem_stabilizer_iff]
38   apply ValuationSubring.ext
39   intro x
40   rw [ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem]
41   change algebraMap (field K A s) L (σ.symm x) ∈ A ↔
42     algebraMap (field K A s) L x ∈ A
43   let g := σ.symm.liftNormal L
44   rw [← σ.symm.liftNormal_commutes L x]
45   have hg : g • A = A := (MulAction.mem_stabilizer_iff).mp (stable g)
46   simpa only [hg, AlgEquiv.smul_def, g] using
47     (ValuationSubring.smul_mem_pointwise_smul_iff
48       (g := g) (S := A) (x := algebraMap (field K A s) L x))
49 
50 /-- The literal ring C=A intersect E is the integral closure of B=A intersect K. -/
51 theorem integralClosure : IsIntegralClosure (valuation K A s)
52     (A.comap (algebraMap K L)) (field K A s) := by
53   let := galois K A stable s
54   exact ValuationIntegralModel.integralClosure K (valuation K A s)
55     (stable_valuation K A stable s)
56 
57 /-- Finiteness is proved from a Noetherian base, not assumed for C. -/
58 theorem finite [IsNoetherianRing (A.comap (algebraMap K L))] :
59     Module.Finite (A.comap (algebraMap K L)) (valuation K A s) := by
60   let := galois K A stable s
61   have : IsNoetherianRing (ValuationIntegralModel.base K (valuation K A s)) := by
62     change IsNoetherianRing (A.comap (algebraMap K L))
63     infer_instance
64   exact ValuationIntegralModel.finite K (valuation K A s)
65     (stable_valuation K A stable s)
66 
67 /-- The integral rank is the already derived field degree. -/
68 theorem rank [IsDiscreteValuationRing (A.comap (algebraMap K L))] :
69     Module.finrank (A.comap (algebraMap K L)) (valuation K A s) =
70       Module.finrank K (field K A s) := by
71   let := galois K A stable s
72   have : IsDiscreteValuationRing (ValuationIntegralModel.base K (valuation K A s)) := by
73     change IsDiscreteValuationRing (A.comap (algebraMap K L))
74     infer_instance
75   exact ValuationIntegralModel.rank K (valuation K A s)
76     (stable_valuation K A stable s)
77 
78 end PaperXI.LiftedValuationFinite

Back to source controls