ValuationContinuity.lean

def unramifiedDegreeHom (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (f : ℕ) (hf : 0 < f) :
    K.toSubgroup →ₜ* Multiplicative (ZMod f)

def unramifiedDegreeKernelWithin (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (f : ℕ) (hf : 0 < f) :
    Subgroup K.toSubgroup

theorem unramifiedDegreeKernelWithin_eq_ker (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (f : ℕ) (hf : 0 < f) :
    unramifiedDegreeKernelWithin D K f hf =
      (unramifiedDegreeHom D K f hf).toMonoidHom.ker

theorem unramifiedDegreeKernelWithin_isClosed (D : DegreeData G)
    (K : FiniteResidueAbstractField D)
    (f : ℕ) (hf : 0 < f) :
    IsClosed (unramifiedDegreeKernelWithin D K f hf :
      Set K.toSubgroup)

def unramifiedExtensionOfDegree (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D)
    (f : ℕ) (hf : 0 < f) : ClosedSubgroup G where
  toSubgroup :=
    (unramifiedDegreeKernelWithin D K f hf).map K.toSubgroup.subtype
  isClosed' := by
    change IsClosed
      (Subtype.val ''
        (unramifiedDegreeKernelWithin D K f hf : Set K.toSubgroup))
    exact K.field.isClosed'.isClosedEmbedding_subtypeVal.isClosedMap _
      (unramifiedDegreeKernelWithin_isClosed D K f hf)

theorem mem_unramifiedExtensionOfDegree_iff (D : DegreeData G)
    [IsTopologicalGroup G] (K : FiniteResidueAbstractField D)
    (f : ℕ) (hf : 0 < f) (g : G) :
    g ∈ unramifiedExtensionOfDegree D K f hf ↔
      ∃ k : K.toSubgroup,
        k ∈ unramifiedDegreeKernelWithin D K f hf ∧ k.1 = g

theorem unramifiedExtensionOfDegree_le (D : DegreeData G)
    [IsTopologicalGroup G] (K : FiniteResidueAbstractField D)
    (f : ℕ) (hf : 0 < f) :
    (unramifiedExtensionOfDegree D K f hf).toSubgroup ≤
      K.toSubgroup

theorem extensionSubgroup_unramifiedExtensionOfDegree (D : DegreeData G)
    [IsTopologicalGroup G] (K : FiniteResidueAbstractField D)
    (f : ℕ) (hf : 0 < f) :
    extensionSubgroup K.field (unramifiedExtensionOfDegree D K f hf)
        (unramifiedExtensionOfDegree_le D K f hf) =
      unramifiedDegreeKernelWithin D K f hf

theorem unramifiedDegreeHom_surjective (D : DegreeData G)
    (K : FiniteResidueAbstractField D)
    (f : ℕ) (hf : 0 < f) :
    Function.Surjective (unramifiedDegreeHom D K f hf)

instance unramifiedExtensionOfDegree_normal (D : DegreeData G)
    [IsTopologicalGroup G] (K : FiniteResidueAbstractField D)
    (f : ℕ) (hf : 0 < f) :
    (extensionSubgroup K.field (unramifiedExtensionOfDegree D K f hf)
      (unramifiedExtensionOfDegree_le D K f hf)).Normal

def finiteUnramifiedExtension (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D)
    (f : ℕ) (hf : 0 < f) : FiniteGaloisSubextension K.field where
  field := unramifiedExtensionOfDegree D K f hf
  below := unramifiedExtensionOfDegree_le D K f hf
  normal := inferInstance
  finite := by
    rw [extensionSubgroup_unramifiedExtensionOfDegree D K f hf]
    let : NeZero f := ⟨Nat.ne_of_gt hf⟩
    let : Finite (Multiplicative (ZMod f)) := by
      change Finite (ZMod f)
      infer_instance
    let q := (unramifiedDegreeHom D K f hf).toMonoidHom
    exact Finite.of_injective
      (QuotientGroup.quotientKerEquivOfSurjective q
        (unramifiedDegreeHom_surjective D K f hf))
      (QuotientGroup.quotientKerEquivOfSurjective q
        (unramifiedDegreeHom_surjective D K f hf)).injective

theorem extensionSubgroup_finiteUnramifiedExtension
    (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D) (f : ℕ) (hf : 0 < f) :
    extensionSubgroup K.field (D.finiteUnramifiedExtension K f hf).field
        (D.finiteUnramifiedExtension K f hf).below =
      unramifiedDegreeKernelWithin D K f hf

def finiteUnramifiedAbelianExtension (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D)
    (f : ℕ) (hf : 0 < f) : FiniteAbelianSubextension K.field where
  toFiniteGaloisExtension := finiteUnramifiedExtension D K f hf
  commutative := by
    let :
        (extensionSubgroup K.field
          (D.finiteUnramifiedExtension K f hf).field
          (D.finiteUnramifiedExtension K f hf).below).Normal :=
      (D.finiteUnramifiedExtension K f hf).normal
    change IsMulCommutative
      (K.toSubgroup ⧸
        extensionSubgroup K.field
          (D.finiteUnramifiedExtension K f hf).field
          (D.finiteUnramifiedExtension K f hf).below)
    let q := (unramifiedDegreeHom D K f hf).toMonoidHom
    have hsub :
        extensionSubgroup K.field
            (D.finiteUnramifiedExtension K f hf).field
            (D.finiteUnramifiedExtension K f hf).below =
          q.ker := by
      rw [D.extensionSubgroup_finiteUnramifiedExtension K f hf,
        D.unramifiedDegreeKernelWithin_eq_ker K f hf]
    let e :
        (K.toSubgroup ⧸
            extensionSubgroup K.field
              (D.finiteUnramifiedExtension K f hf).field
              (D.finiteUnramifiedExtension K f hf).below) ≃*
          Multiplicative (ZMod f) :=
      (QuotientGroup.quotientMulEquivOfEq hsub).trans
        (QuotientGroup.quotientKerEquivOfSurjective q
          (unramifiedDegreeHom_surjective D K f hf))
    exact
      { is_comm.comm := fun x y => by
          apply e.injective
          rw [map_mul, map_mul, mul_comm] }

theorem finiteUnramifiedAbelianExtension_toFiniteGaloisExtension
    (D : DegreeData G) [IsTopologicalGroup G]
    (K : FiniteResidueAbstractField D)
    (f : ℕ) (hf : 0 < f) :
    (D.finiteUnramifiedAbelianExtension K f hf).toFiniteGaloisExtension =
      D.finiteUnramifiedExtension K f hf

theorem unramifiedExtensionOfDegree_isUnramified (D : DegreeData G)
    [IsTopologicalGroup G] (K : FiniteResidueAbstractField D)
    (f : ℕ) (hf : 0 < f) :
    (DegreeData.AbstractExtension.mk (unramifiedExtensionOfDegree D K f hf) K.field
      (unramifiedExtensionOfDegree_le D K f hf)).IsUnramified D

theorem finiteUnramifiedExtension_degree (D : DegreeData G)
    [IsTopologicalGroup G] (K : FiniteResidueAbstractField D)
    (f : ℕ) (hf : 0 < f) :
    (((finiteUnramifiedExtension D K f hf).toFiniteAbstractExtension.degree : ℕ)) = f

theorem finiteUnramifiedExtension_residueDegree (D : DegreeData G)
    [IsTopologicalGroup G] (K : FiniteResidueAbstractField D)
    (f : ℕ) (hf : 0 < f) :
    (((finiteUnramifiedExtension D K f hf).toFiniteAbstractExtension.residueDegree D : ℕ)) = f

theorem exists_nsmul_mem_of_valueGroup_mem_nhds
    (v : ValuationData D A) {U : Set v.valueGroup}
    (hU : U ∈ 𝓝 (0 : v.valueGroup)) :
    ∃ f : ℕ, 0 < f ∧ ∀ z : v.valueGroup, f • z ∈ U

theorem normTopology_valuation_continuous
    [IsTopologicalGroup G] (v : ValuationData D A)
    (K : FiniteAbstractField G) :
    IsContinuousFromNormTopology A K.field (v.valuationAt K)