LiftedValuationInertia.lean

1 import PaperXI.LiftedFullResidue
2 
3 /-! The actual residue-action inertia of the generated field is trivial.
4 This is not an assumed ramification-index certificate. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.LiftedValuationInertia
8 open IsLocalRing PaperXI.LiftedResidueDegree PaperXI.LiftedFullResidue
9 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
10 variable (A : ValuationSubring L) [HenselianLocalRing A] [Fintype (ResidueField A)]
11 variable (s : IntermediateField (BaseResidue K A) (ResidueField A))
12 local instance subfieldFintype : Fintype s := Fintype.ofFinite s
13 
14 /-- A valuation-preserving automorphism with trivial residue action fixes every
15 Hensel generator and therefore the whole generated field. -/
16 theorem inertia_trivial : (valuation K A s).inertiaSubgroup K = ⊥ := by
17   apply le_antisymm ?_ bot_le
18   intro g hg
19   change g = 1
20   have he : (field K A s).val.comp g.val.toAlgHom = (field K A s).val := by
21     apply IntermediateField.adjoin_algHom_ext K
22     rintro _ ⟨a, rfl⟩
23     let z := HenselianResidueLift.lift s A s.val.toRingHom a
24     let e : field K A s := ⟨(z : L), HenselianFieldLift.element_mem s K A s.val.toRingHom a⟩
25     let v : valuation K A s := ⟨e, z.property⟩
26     let σ := MulSemiringAction.toRingAut ((valuation K A s).decompositionSubgroup K)
27       (valuation K A s) g
28     let inc : valuation K A s →+* A := ValuationResidueEmbedding.inclusion A (field K A s).val.toRingHom
29     have hv : v ^ Fintype.card s = v := by
30       apply Subtype.ext
31       apply Subtype.ext
32       exact congrArg (fun x : A => (x : L)) (HenselianResidueLift.lift_pow s A s.val.toRingHom a)
33     have hy : inc (σ v) ^ Fintype.card s = inc (σ v) := by
34       rw [← map_pow, ← map_pow, hv]
35     have hres : residue (valuation K A s) (σ v) = residue (valuation K A s) v := by
36       change residue (valuation K A s) (g • v) = _
37       rw [ResidueField.residue_smul]
38       change MulSemiringAction.toRingAut ((valuation K A s).decompositionSubgroup K)
39         (ResidueField (valuation K A s)) g = 1 at hg
40       exact RingEquiv.congr_fun hg (residue (valuation K A s) v)
41     have hresA : residue A (inc (σ v)) = residue A z :=
42       congrArg (ValuationResidueEmbedding.residueMap A (field K A s).val.toRingHom) hres
43     have hz := HenselianResidueLift.unique_lift s A s.val.toRingHom hy
44       (HenselianResidueLift.lift_pow s A s.val.toRingHom a) hresA
45     exact congrArg (fun x : A => (x : L)) hz
46   apply Subtype.ext
47   apply AlgEquiv.ext
48   intro x
49   exact (field K A s).val.injective (AlgHom.congr_fun he x)
50 
51 end PaperXI.LiftedValuationInertia

Back to source controls