ValuationFixingField.lean

1 import PaperXI.HenselianFieldLift
2 
3 /-! Restricting the base field in the literal decomposition subgroup. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.ValuationFixingField
7 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
8 variable (A : ValuationSubring L) (E : IntermediateField K L)
9 
10 /-- Valuation-preserving automorphisms over E are exactly valuation-preserving
11 K-automorphisms fixing every element of E. -/
12 def decompositionEquiv : A.decompositionSubgroup E ≃*
13     E.fixingSubgroup.comap (A.decompositionSubgroup K).subtype where
14   toFun g := ⟨⟨g.val.restrictScalars K, g.property⟩, by
15     change g.val.restrictScalars K ∈ E.fixingSubgroup
16     rw [IntermediateField.mem_fixingSubgroup_iff]
17     intro x hx
18     exact g.val.commutes ⟨x,hx⟩⟩
19   invFun g := ⟨{ g.val.val.toRingEquiv with
20     commutes' := fun x => (IntermediateField.mem_fixingSubgroup_iff E g.val.val).mp g.property x x.property },
21     g.val.property⟩
22   left_inv g := by rfl
23   right_inv g := by rfl
24   map_mul' g h := by rfl
25 
26 /-- The equivalence preserves the ambient field automorphism literally. -/
27 @[simp] theorem decompositionEquiv_apply (g : A.decompositionSubgroup E) (x : L) :
28     (decompositionEquiv K A E g).val.val x = g.val x := rfl
29 
30 /-- In particular the induced actions on the valuation ring agree. -/
31 theorem ring_action (g : A.decompositionSubgroup E) (x : A) :
32     ((decompositionEquiv K A E g).val • x : A) = g • x := rfl
33 
34 /-- And their actual residue actions agree, not merely their degree indices. -/
35 theorem residue_action (g : A.decompositionSubgroup E) (x : IsLocalRing.ResidueField A) :
36     (decompositionEquiv K A E g).val • x = g • x := by
37   obtain ⟨a,rfl⟩ := IsLocalRing.residue_surjective x
38   rw [← IsLocalRing.ResidueField.residue_smul, ← IsLocalRing.ResidueField.residue_smul]
39   rfl
40 
41 end PaperXI.ValuationFixingField

Back to source controls