NormalizedIntegerValuation.lean

def localIntegerValuation :
    _root_.Valuation K (WithZero (Multiplicative ℤ))

theorem localIntegerValuation_apply (x : K) :
    localIntegerValuation K x =
      IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt K
        (ValuativeRel.valuation K x)

theorem localCompleteDVF_valuation_eq :
    (localCompleteDVF K).valuation = ValuativeRel.valuation K

theorem integerRing_moduleFinite_of_finite_separable
    (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L]
    [Algebra.IsSeparable K L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)] :
    Module.Finite
      (ValuativeRel.valuation K).integer
      (ValuativeRel.valuation L).integer

theorem localIntegerValuation_valuationSubring_eq :
    (localIntegerValuation K).valuationSubring =
      (localCompleteDVF K).valuation.valuationSubring

theorem localIntegerValuation_surjective :
    Function.Surjective (localIntegerValuation K)

def localIntegerValuationSubringEquiv :
    (localIntegerValuation K).valuationSubring ≃+*
      (localCompleteDVF K).valuationSubring where
  toFun := fun x => ⟨x, by
    change (localCompleteDVF K).valuation (x : K) ≤ 1
    rw [localCompleteDVF_valuation_eq]
    have hx :
        IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt K
            (ValuativeRel.valuation K (x : K)) ≤
          IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt K 1 := by
      have hxmem := x.property
      change localIntegerValuation K (x : K) ≤ 1 at hxmem
      rw [localIntegerValuation_apply] at hxmem
      simpa only [map_one] using hxmem
    exact
      (map_le_map_iff
        (IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt K)).mp hx⟩
  invFun := fun x => ⟨x, by
    have hx : ValuativeRel.valuation K (x : K) ≤ 1 := by
      have hxmem := x.property
      change (localCompleteDVF K).valuation (x : K) ≤ 1 at hxmem
      rw [localCompleteDVF_valuation_eq] at hxmem
      exact hxmem
    change
      IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt K
          (ValuativeRel.valuation K (x : K)) ≤ 1
    simpa only [localIntegerValuation, _root_.Valuation.map_apply,
      map_one] using
      (map_le_map_iff
        (IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt K)).mpr hx⟩
  left_inv := fun x => by ext; rfl
  right_inv := fun x => by ext; rfl
  map_mul' := fun x y => by ext; rfl
  map_add' := fun x y => by ext; rfl

theorem localIntegerValuationSubringEquiv_apply_coe
    (x : (localIntegerValuation K).valuationSubring) :
    ((localIntegerValuationSubringEquiv K x :
      (localCompleteDVF K).valuationSubring) : K) = x

theorem localIntegerValuationSubringEquiv_mem_maximalIdeal_iff
    (x : (localIntegerValuation K).valuationSubring) :
    localIntegerValuationSubringEquiv K x ∈
        IsLocalRing.maximalIdeal (localCompleteDVF K).valuationSubring ↔
      x ∈ IsLocalRing.maximalIdeal
        (localIntegerValuation K).valuationSubring

theorem localIntegerValuationSubringEquiv_map_maximalIdeal :
    (IsLocalRing.maximalIdeal
        (localIntegerValuation K).valuationSubring).map
      (localIntegerValuationSubringEquiv K :
        (localIntegerValuation K).valuationSubring →+*
          (localCompleteDVF K).valuationSubring) =
      IsLocalRing.maximalIdeal (localCompleteDVF K).valuationSubring

instance localIntegerValuation_isCompleteDiscrete :
    ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete
      (localIntegerValuation K) where
  isRankOneDiscrete := by
    let v := localIntegerValuation K
    have : v.IsNontrivial := by
      obtain ⟨x, hx⟩ :=
        localIntegerValuation_surjective K (WithZero.exp (-1 : ℤ))
      refine ⟨⟨x, ?_, ?_⟩⟩
      · rw [hx]
        simp
      · rw [hx]
        change WithZero.exp (-1 : ℤ) ≠ WithZero.exp (0 : ℤ)
        simp
    have : IsCyclic (MonoidWithZeroHom.valueGroup v.toMonoidWithZeroHom) :=
      Subgroup.isCyclic_of_le
        (show MonoidWithZeroHom.valueGroup v.toMonoidWithZeroHom ≤ ⊤ from le_top)
    exact _root_.Valuation.IsRankOneDiscrete.mk' v
  isAdicComplete := by
    let e := localIntegerValuationSubringEquiv K
    let : IsAdicComplete
        (IsLocalRing.maximalIdeal (localCompleteDVF K).valuationSubring)
        (localCompleteDVF K).valuationSubring :=
      (localCompleteDVF K).isAdicComplete
    have hcomplete :
        IsAdicComplete
          ((IsLocalRing.maximalIdeal
            (localCompleteDVF K).valuationSubring).map
              (e.symm : (localCompleteDVF K).valuationSubring →+*
                (localIntegerValuation K).valuationSubring))
          (localIntegerValuation K).valuationSubring :=
      ValuationTheory.DiscreteValuationField.isAdicComplete_map_ringEquiv
        (I := IsLocalRing.maximalIdeal
          (localCompleteDVF K).valuationSubring) e.symm
    have hmap :
        (IsLocalRing.maximalIdeal
          (localCompleteDVF K).valuationSubring).map
            (e.symm : (localCompleteDVF K).valuationSubring →+*
              (localIntegerValuation K).valuationSubring) =
          IsLocalRing.maximalIdeal
            (localIntegerValuation K).valuationSubring := by
      ext x
      rw [Ideal.mem_map_iff_of_surjective
        (e.symm : (localCompleteDVF K).valuationSubring →+*
          (localIntegerValuation K).valuationSubring) e.symm.surjective]
      constructor
      · rintro ⟨y, hy, rfl⟩
        exact
          (localIntegerValuationSubringEquiv_mem_maximalIdeal_iff K
            (e.symm y)).1 (by simpa [e] using hy)
      · intro hx
        refine ⟨e x, ?_, by simp [e]⟩
        exact
          (localIntegerValuationSubringEquiv_mem_maximalIdeal_iff K x).2 hx
    simpa [hmap] using hcomplete

instance localIntegerValuation_residueFinite :
    Finite
      (IsLocalRing.ResidueField
        (localIntegerValuation K).valuationSubring)