LaurentLocalField.lean

theorem isValuativeTopology_of_valued_ofValuation'
    (L : Type u) (Γ : Type w) [Field L]
    [LinearOrderedCommGroupWithZero Γ] [MulArchimedean Γ]
    [Valued L Γ]
    [Valuation.IsNontrivial (Valued.v : Valuation L Γ)] :
    letI := ValuativeRel.ofValuation (Valued.v : Valuation L Γ)
    IsValuativeTopology L := by
  let vL : Valuation L Γ := Valued.v
  let : ValuativeRel L := ValuativeRel.ofValuation vL
  let : vL.Compatible := Valuation.Compatible.ofValuation vL
  let : ValuativeRel.IsNontrivial L :=
    (ValuativeRel.isNontrivial_iff_isNontrivial vL).2 inferInstance
  apply IsValuativeTopology.of_zero
  intro s
  rw [Valued.mem_nhds_zero]
  constructor
  · rintro ⟨δ, hδ⟩
    refine
      ⟨δ.mapEquiv
          (ValuativeRel.ValueGroupWithZero.orderMonoidIso vL).symm, ?_⟩
    intro z hz
    apply hδ
    exact
      (ValuativeRel.valuation_lt_symm_orderMonoidIso
        vL δ.1 z).1
        (by simpa using hz)
  · rintro ⟨γ, hγ⟩
    refine
      ⟨γ.mapEquiv
          (ValuativeRel.ValueGroupWithZero.orderMonoidIso vL), ?_⟩
    intro z hz
    apply hγ
    have hz' :
        vL.restrict z <
          (ValuativeRel.ValueGroupWithZero.orderMonoidIso vL)
            (γ : ValuativeRel.ValueGroupWithZero L) := by
      exact hz
    exact
      (ValuativeRel.restrict_lt_orderMonoidIso
        vL (γ : ValuativeRel.ValueGroupWithZero L) z).1 hz'

theorem continuous_laurentSeries_ofPowerSeries
    [TopologicalSpace k] [DiscreteTopology k] :
    Continuous (HahnSeries.ofPowerSeries ℤ k : k⟦X⟧ → k⸨X⸩)

def powerSeriesToLaurentInteger (k : Type u) [Field k] :
    k⟦X⟧ → Valued.integer k⸨X⸩

theorem continuous_powerSeriesToLaurentInteger
    [TopologicalSpace k] [DiscreteTopology k] :
    Continuous (powerSeriesToLaurentInteger k)

theorem powerSeriesToLaurentInteger_surjective :
    Function.Surjective (powerSeriesToLaurentInteger k)

def powerSeriesEquivLaurentInteger
    (k : Type u) [Field k] :
    k⟦X⟧ ≃+* Valued.integer k⸨X⸩ where
  toFun := powerSeriesToLaurentInteger k
  invFun x := Classical.choose
    ((LaurentSeries.val_le_one_iff_eq_coe k (x : k⸨X⸩)).1 x.property)
  left_inv f := by
    exact (HahnSeries.ofPowerSeries_injective (Γ := ℤ) (R := k))
      (Classical.choose_spec
        ((LaurentSeries.val_le_one_iff_eq_coe k
          ((powerSeriesToLaurentInteger k f :
            Valued.integer k⸨X⸩) : k⸨X⸩)).1
            (powerSeriesToLaurentInteger k f).property))
  right_inv x := by
    apply Subtype.ext
    exact Classical.choose_spec
      ((LaurentSeries.val_le_one_iff_eq_coe k (x : k⸨X⸩)).1 x.property)
  map_add' f g := by
    apply Subtype.ext
    exact map_add (HahnSeries.ofPowerSeries ℤ k) f g
  map_mul' f g := by
    apply Subtype.ext
    exact map_mul (HahnSeries.ofPowerSeries ℤ k) f g

theorem powerSeriesEquivLaurentInteger_coe
    (f : k⟦X⟧) :
    ((powerSeriesEquivLaurentInteger k f :
      Valued.integer k⸨X⸩) : k⸨X⸩) = (f : k⸨X⸩)

theorem powerSeriesEquivLaurentInteger_X_irreducible :
    Irreducible
      (powerSeriesEquivLaurentInteger k (PowerSeries.X : k⟦X⟧))

def laurentValuativeIntegerEquiv
    (k : Type u) [Field k] :
    letI : ValuativeRel k⸨X⸩ := ValuativeRel.ofValuation
      (Valued.v : Valuation k⸨X⸩ ℤᵐ⁰)
    (ValuativeRel.valuation k⸨X⸩).integer ≃+*
      Valued.integer k⸨X⸩ := by
  let L := k⸨X⸩
  let vL := (Valued.v : Valuation L ℤᵐ⁰)
  letI : ValuativeRel L := ValuativeRel.ofValuation vL
  letI : vL.Compatible := Valuation.Compatible.ofValuation vL
  let wL := ValuativeRel.valuation L
  exact
    { toFun := fun x => ⟨x, by
        have hxrel : (x : L) ≤ᵥ (1 : L) :=
          wL.vle_iff_le.mpr x.property
        change vL (x : L) ≤ 1
        simpa only [map_one] using vL.vle_iff_le.mp hxrel⟩
      invFun := fun x => ⟨x, by
        have hxv : vL (x : L) ≤ 1 := x.property
        have hxrel : (x : L) ≤ᵥ (1 : L) :=
          vL.vle_iff_le.mpr (by simpa only [map_one] using hxv)
        exact wL.vle_iff_le.mp hxrel⟩
      left_inv := fun _ => rfl
      right_inv := fun _ => rfl
      map_add' := fun _ _ => rfl
      map_mul' := fun _ _ => rfl }

def powerSeriesEquivLaurentValuativeInteger
    (k : Type u) [Field k] :
    letI : ValuativeRel k⸨X⸩ := ValuativeRel.ofValuation
      (Valued.v : Valuation k⸨X⸩ ℤᵐ⁰)
    k⟦X⟧ ≃+* (ValuativeRel.valuation k⸨X⸩).integer := by
  letI : ValuativeRel k⸨X⸩ := ValuativeRel.ofValuation
    (Valued.v : Valuation k⸨X⸩ ℤᵐ⁰)
  exact (powerSeriesEquivLaurentInteger k).trans
    (laurentValuativeIntegerEquiv k).symm

theorem powerSeriesEquivLaurentValuativeInteger_X_irreducible :
    letI : ValuativeRel k⸨X⸩ := ValuativeRel.ofValuation
      (Valued.v : Valuation k⸨X⸩ ℤᵐ⁰)
    Irreducible
      (powerSeriesEquivLaurentValuativeInteger k
        (PowerSeries.X : k⟦X⟧)) := by
  let : ValuativeRel k⸨X⸩ := ValuativeRel.ofValuation
    (Valued.v : Valuation k⸨X⸩ ℤᵐ⁰)
  exact PowerSeries.X_irreducible.map
    (powerSeriesEquivLaurentValuativeInteger k)

theorem laurentSeriesIntegerCompactSpace
    (k : Type u) [Field k] [Finite k] :
    CompactSpace (Valued.integer k⸨X⸩)

theorem laurentSeriesLocallyCompactSpace
    (k : Type u) [Field k] [Finite k] :
    LocallyCompactSpace k⸨X⸩

def equalCharacteristicLaurentValuativeRel
    {K : Type u} [Field K] (F : LocalField.{u, v} K) :
    ValuativeRel F.residueField⸨X⸩

theorem equalCharacteristicLaurentIsNonarchimedeanLocalField
    {K : Type u} [Field K] (F : LocalField.{u, v} K) :
    letI := equalCharacteristicLaurentValuativeRel F
    IsNonarchimedeanLocalField F.residueField⸨X⸩ := by
  let L := F.residueField⸨X⸩
  let vL := (Valued.v : Valuation L ℤᵐ⁰)
  let : ValuativeRel L := equalCharacteristicLaurentValuativeRel F
  let : vL.Compatible := Valuation.Compatible.ofValuation vL
  let x : L :=
    ((PowerSeries.X : F.residueField⟦X⟧) : F.residueField⸨X⸩)
  have hxv : vL x = WithZero.exp (-1 : ℤ) := by
    change (Valued.v : Valuation F.residueField⸨X⸩ ℤᵐ⁰)
      (((PowerSeries.X : F.residueField⟦X⟧) :
        F.residueField⸨X⸩)) = _
    simpa using LaurentSeries.valuation_X_pow F.residueField 1
  have hx0 : x ≠ 0 := by
    intro hx
    have : vL x = 0 := by rw [hx, map_zero]
    rw [hxv] at this
    exact WithZero.exp_ne_zero this
  have hxlt : vL x < 1 := by
    rw [hxv, ← WithZero.exp_zero, WithZero.exp_lt_exp]
    omega
  let : vL.IsNontrivial :=
    (Valuation.isNontrivial_iff_exists_lt_one vL).2 ⟨x, hx0, hxlt⟩
  let : ValuativeRel.IsNontrivial L :=
    (ValuativeRel.isNontrivial_iff_isNontrivial vL).2 inferInstance
  let : IsValuativeTopology L :=
    isValuativeTopology_of_valued_ofValuation' L ℤᵐ⁰
  let : LocallyCompactSpace L :=
    laurentSeriesLocallyCompactSpace F.residueField
  exact
    { toIsValuativeTopology := inferInstance
      toLocallyCompactSpace := inferInstance
      toIsNontrivial := inferInstance }