ValuationResidueEmbedding.lean

1 import PaperXI.HenselianFieldLift
2 
3 /-! Residue embedding of an actual restricted valuation ring. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.ValuationResidueEmbedding
7 open IsLocalRing
8 variable {F L : Type*} [Field F] [Field L]
9 variable (A : ValuationSubring L) (f : F →+* L)
10 def inclusion : A.comap f →+* A where
11   toFun x := ⟨f x.val, x.property⟩
12   map_one' := Subtype.ext (map_one f)
13   map_zero' := Subtype.ext (map_zero f)
14   map_add' x y := Subtype.ext (map_add f x.val y.val)
15   map_mul' x y := Subtype.ext (map_mul f x.val y.val)
16 @[simp] theorem inclusion_val (x : A.comap f) :
17     (inclusion A f x : L) = f x.val := rfl
18 instance inclusion_local : IsLocalHom (inclusion A f) where
19   map_nonunit x hx := by
20     obtain ⟨y, hy⟩ := isUnit_iff_exists_inv.mp hx
21     have hp : f (x : F) * (y : L) = 1 := congrArg (fun z : A => (z : L)) hy
22     have hx0 : (x : F) ≠ 0 := by
23       intro h; simp [h] at hp
24     have hf0 : f (x : F) ≠ 0 := (map_ne_zero f).mpr hx0
25     have hyv : (y : L) = (f (x : F))⁻¹ := by
26       apply mul_left_cancel₀ hf0
27       rw [hp, mul_inv_cancel₀ hf0]
28     refine isUnit_iff_exists_inv.mpr ⟨⟨(x : F)⁻¹, ?_⟩, ?_⟩
29     · change f ((x : F)⁻¹) ∈ A
30       rw [map_inv₀, ← hyv]
31       exact y.property
32     · exact Subtype.ext (mul_inv_cancel₀ hx0)
33 def residueMap : ResidueField (A.comap f) →+* ResidueField A :=
34   ResidueField.map (inclusion A f)
35 @[simp] theorem residueMap_residue (x : A.comap f) :
36     residueMap A f (residue (A.comap f) x) = residue A (inclusion A f x) := rfl
37 theorem residueMap_injective : Function.Injective (residueMap A f) :=
38   (residueMap A f).injective
39 theorem mem_range_iff (z : ResidueField A) :
40     z ∈ Set.range (residueMap A f) ↔
41       ∃ x : F, ∃ hx : f x ∈ A, residue A ⟨f x, hx⟩ = z := by
42   constructor
43   · rintro ⟨a, ha⟩
44     obtain ⟨x, rfl⟩ := residue_surjective a
45     exact ⟨x.val, x.property, ha⟩
46   · rintro ⟨x, hx, h⟩
47     exact ⟨residue (A.comap f) ⟨x, hx⟩, h⟩
48 end PaperXI.ValuationResidueEmbedding

Back to source controls