ValuationExactSequence.lean

def valuationUnitsMulHom
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] : Kˣ →* Multiplicative Int

def valuationMap (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Additive Kˣ →+ Int

def valuationShortComplex (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Additive Kˣ →+ Int

theorem valuationMap_apply (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Additive Kˣ) :
    valuationMap K x = v K x

theorem valuationMap_surjective (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
    Function.Surjective (valuationMap K)

theorem valuationMap_uniformiser (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
    ∃ ϖ : Kˣ, valuationMap K (Additive.ofMul ϖ) = 1

def uniformizerFieldUnit
    (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (π : 𝒪[K])
    (hπ : (ValuativeRel.valuation K).IsUniformizer (π : K)) :
    Kˣ

theorem uniformizerFieldUnit_coe
    (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (π : 𝒪[K])
    (hπ : (ValuativeRel.valuation K).IsUniformizer (π : K)) :
    (uniformizerFieldUnit K π hπ : K) = (π : K)

theorem valuationMap_uniformizerFieldUnit
    (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (π : 𝒪[K])
    (hπ : (ValuativeRel.valuation K).IsUniformizer (π : K)) :
    valuationMap K
        (Additive.ofMul (uniformizerFieldUnit K π hπ)) =
      -1

theorem valuationMap_zero (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
    valuationMap K (0 : Additive Kˣ) = 0

theorem valuationMap_add (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x y : Additive Kˣ) :
    valuationMap K (x + y) = valuationMap K x + valuationMap K y

theorem valuationMap_neg (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Additive Kˣ) :
    valuationMap K (-x) = -valuationMap K x

theorem valuationMap_sub (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x y : Additive Kˣ) :
    valuationMap K (x - y) = valuationMap K x - valuationMap K y

theorem valuationMap_zsmul (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Int) (x : Additive Kˣ) :
    valuationMap K (n • x) = n • valuationMap K x

theorem valuationMap_eq_zero_iff_v_eq_zero (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Additive Kˣ) :
    valuationMap K x = 0 ↔ v K x = 0

theorem valuationMap_mem_ker_iff (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Additive Kˣ) :
    x ∈ AddMonoidHom.ker (valuationMap K) ↔ v K x = 0

theorem valuationMap_ofMul_one (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
    valuationMap K (Additive.ofMul (1 : Kˣ)) = 0

theorem valuationMap_ofMul_mul (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x y : Kˣ) :
    valuationMap K (Additive.ofMul (x * y)) =
      valuationMap K (Additive.ofMul x) + valuationMap K (Additive.ofMul y)

theorem valuationMap_ofMul_inv (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Kˣ) :
    valuationMap K (Additive.ofMul x⁻¹) =
      -valuationMap K (Additive.ofMul x)

theorem valuation_eq_one_of_valuationMap_eq_zero (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    {x : Kˣ} (hx : valuationMap K (Additive.ofMul x) = 0) :
    ValuativeRel.valuation K (x : K) = 1

theorem valuationMap_ofMul_div (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x y : Kˣ) :
    valuationMap K (Additive.ofMul (x / y)) =
      valuationMap K (Additive.ofMul x) - valuationMap K (Additive.ofMul y)

theorem valuationMap_ofMul_zpow (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Kˣ) (n : Int) :
    valuationMap K (Additive.ofMul (x ^ n)) =
      n * valuationMap K (Additive.ofMul x)

theorem valuationMap_ofMul_pow (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Kˣ) (n : Nat) :
    valuationMap K (Additive.ofMul (x ^ n)) =
      (n : Int) * valuationMap K (Additive.ofMul x)

theorem valuationMap_ofMul_eq_zero_iff (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Kˣ) :
    valuationMap K (Additive.ofMul x) = 0 ↔ v K (Additive.ofMul x) = 0

def additiveIntegerUnitsToFieldUnits (K : Type u) [Field K] [ValuativeRel K] :
    Additive 𝒪[K]ˣ →+ Additive Kˣ

theorem additiveIntegerUnitsToFieldUnits_apply (K : Type u) [Field K] [ValuativeRel K]
    (u : 𝒪[K]ˣ) :
    additiveIntegerUnitsToFieldUnits K (Additive.ofMul u) =
      Additive.ofMul (integerUnitsToFieldUnits K u)

def integerUnitOfValuationMapZero (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (x : Kˣ) (hx : valuationMap K (Additive.ofMul x) = 0) : 𝒪[K]ˣ where
  val := ⟨(x : K), by
    rw [valuation_integer_membership]
    have hv := valuation_eq_one_of_valuationMap_eq_zero K hx
    simp [hv]⟩
  inv := ⟨(x⁻¹ : K), by
    rw [valuation_integer_membership]
    have hv := valuation_eq_one_of_valuationMap_eq_zero K hx
    simp [hv]⟩
  val_inv := by
    ext
    simp
  inv_val := by
    ext
    simp

theorem integerUnitOfValuationMapZero_spec (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (x : Kˣ) (hx : valuationMap K (Additive.ofMul x) = 0) :
    integerUnitsToFieldUnits K (integerUnitOfValuationMapZero K x hx) = x

theorem integerUnitsToFieldUnits_mem_range_iff_valuationMap_eq_zero (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (x : Kˣ) :
    x ∈ MonoidHom.range (integerUnitsToFieldUnits K) ↔
      valuationMap K (Additive.ofMul x) = 0

theorem mem_powMonoidHom_range_integerUnits_iff (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ+) (x : 𝒪[K]ˣ) :
    x ∈ (powMonoidHom (n : ℕ) : 𝒪[K]ˣ →* 𝒪[K]ˣ).range ↔
      integerUnitsToFieldUnits K x ∈
        (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range

theorem additiveIntegerUnitsToFieldUnits_range_eq_ker_valuationMap (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
    AddMonoidHom.range (additiveIntegerUnitsToFieldUnits K) =
      AddMonoidHom.ker (valuationMap K)

def fieldUnitsModIntegerUnitsAddEquivInt (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
    Additive Kˣ ⧸ AddMonoidHom.range (additiveIntegerUnitsToFieldUnits K) ≃+ Int

theorem fieldUnitsModIntegerUnitsAddEquivInt_mk (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (x : Additive Kˣ) :
    fieldUnitsModIntegerUnitsAddEquivInt K (QuotientAddGroup.mk x) =
      valuationMap K x

theorem fieldUnitsModIntegerUnitsAddEquivInt_mk_eq_zero_iff (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (x : Additive Kˣ) :
    fieldUnitsModIntegerUnitsAddEquivInt K (QuotientAddGroup.mk x) = 0 ↔
      valuationMap K x = 0

theorem fieldUnitsModIntegerUnitsAddEquivInt_mk_eq_mk_iff (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (x y : Additive Kˣ) :
    (QuotientAddGroup.mk x :
        Additive Kˣ ⧸ AddMonoidHom.range (additiveIntegerUnitsToFieldUnits K)) =
      QuotientAddGroup.mk y ↔ valuationMap K x = valuationMap K y

theorem fieldUnitsModIntegerUnitsAddEquivInt_mk_sub_eq_zero_iff (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (x y : Additive Kˣ) :
    fieldUnitsModIntegerUnitsAddEquivInt K (QuotientAddGroup.mk (x - y)) = 0 ↔
      valuationMap K x = valuationMap K y

theorem uniformizerUnitFactorValuationZero (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (ϖ x : Kˣ) (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) :
    valuationMap K
      (Additive.ofMul (x / ϖ ^ valuationMap K (Additive.ofMul x))) = 0

def uniformizerUnitFactor (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (ϖ : Kˣ) (hϖ : valuationMap K (Additive.ofMul ϖ) = 1)
    (x : Kˣ) : 𝒪[K]ˣ

theorem integerUnitsToFieldUnits_uniformizerUnitFactor (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (ϖ : Kˣ) (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) (x : Kˣ) :
    integerUnitsToFieldUnits K (uniformizerUnitFactor K ϖ hϖ x) =
      x / ϖ ^ valuationMap K (Additive.ofMul x)

theorem uniformizerUnitFactor_mul_uniformizer_zpow (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (ϖ : Kˣ) (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) (x : Kˣ) :
    integerUnitsToFieldUnits K (uniformizerUnitFactor K ϖ hϖ x) *
        ϖ ^ valuationMap K (Additive.ofMul x) = x

theorem exists_integerUnit_mul_uniformizer_zpow (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (ϖ : Kˣ) (hϖ : valuationMap K (Additive.ofMul ϖ) = 1) (x : Kˣ) :
    ∃ u : 𝒪[K]ˣ,
      integerUnitsToFieldUnits K u *
        ϖ ^ valuationMap K (Additive.ofMul x) = x

theorem valuationMap_surjective_apply (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Int) :
    ∃ x : Additive Kˣ, valuationMap K x = n

def chosenValuationMapSection (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Int → Additive Kˣ

theorem chosenValuationMapSection_spec (K : Type u) [Field K] [ValuativeRel K]
    [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : Int) :
    valuationMap K (chosenValuationMapSection K n) = n