ValuationIntegralModel.lean

1 import PaperXI.HenselianGaloisResidue
2 import Mathlib.RingTheory.DedekindDomain.IntegralClosure
3 import Mathlib.RingTheory.Valuation.Integral
4 import Mathlib.RingTheory.Flat.TorsionFree
5 
6 /-! Integral closure and finiteness of an invariant valuation ring. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.ValuationIntegralModel
10 open IsLocalRing
11 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
12 variable (A : ValuationSubring L)
13 abbrev base := A.comap (algebraMap K L)
14 
15 instance baseAlgebra : Algebra (base K A) A :=
16   (ValuationResidueEmbedding.inclusion A (algebraMap K L)).toAlgebra
17 instance baseTower : IsScalarTower (base K A) A L :=
18   IsScalarTower.of_algebraMap_eq' rfl
19 instance baseFieldTower : IsScalarTower (base K A) K L :=
20   IsScalarTower.of_algebraMap_eq' rfl
21 instance baseLocal : IsLocalHom (algebraMap (base K A) A) :=
22   ValuationResidueEmbedding.inclusion_local A (algebraMap K L)
23 
24 variable (stable : ∀ g : L ≃ₐ[K] L, g ∈ A.decompositionSubgroup K)
25 @[instance_reducible] def ringAction : MulSemiringAction (L ≃ₐ[K] L) A :=
26   MulSemiringAction.compHom A (HenselianGaloisResidue.decompositionMap K A stable)
27 
28 variable [FiniteDimensional K L] [IsGalois K L]
29 
30 /-- Fixed integral elements belong to the literally restricted base valuation ring. -/
31 theorem invariant : letI := ringAction K A stable
32     Algebra.IsInvariant (base K A) A (L ≃ₐ[K] L) := by
33   let := ringAction K A stable
34   constructor
35   intro x hx
36   have hxK : (x : L) ∈ (⊥ : IntermediateField K L) := by
37     rw [IsGalois.mem_bot_iff_fixed]
38     intro g
39     exact congrArg (fun a : A => (a : L)) (hx g)
40   obtain ⟨b, hb⟩ := IntermediateField.mem_bot.mp hxK
41   have hbA : b ∈ base K A := by
42     change algebraMap K L b ∈ A
43     rw [hb]
44     exact x.property
45   exact ⟨⟨b, hbA⟩, Subtype.ext hb⟩
46 
47 include stable
48 
49 /-- Integrality is derived from the finite Galois action. -/
50 theorem integral : Algebra.IsIntegral (base K A) A := by
51   let := ringAction K A stable
52   let := invariant K A stable
53   exact Algebra.IsInvariant.isIntegral (base K A) A (L ≃ₐ[K] L)
54 
55 /-- The invariant valuation ring is the actual integral closure of its base. -/
56 theorem integralClosure : IsIntegralClosure A (base K A) L := by
57   let := integral K A stable
58   infer_instance
59 
60 /-- No module-finiteness certificate is assumed: derive it from separability
61 and a Noetherian base valuation ring. -/
62 theorem finite [IsNoetherianRing (base K A)] : Module.Finite (base K A) A := by
63   let := integralClosure K A stable
64   exact IsIntegralClosure.finite (base K A) K L A
65 
66 /-- A DVR base provides the standard integral rank comparison. -/
67 theorem rank [IsDiscreteValuationRing (base K A)] :
68     Module.finrank (base K A) A = Module.finrank K L := by
69   let := integralClosure K A stable
70   exact IsIntegralClosure.rank (base K A) K L A
71 
72 end PaperXI.ValuationIntegralModel

Back to source controls