/-
Copyright (c) 2026 LANA Project. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: LANA Project
-/
import Mathlib
import TemperedFundamentalGroups.Setup.Schmidt

/-!
# The canonical valuation of a completion of a number field

Let `F` be a number field, `v` a finite place of `F` and `F_v = v.adicCompletion F` the
completion, with valuation ring `O_v = v.adicCompletionIntegers F` (a discrete valuation ring,
`Mathlib`). This module proves the facts about `O_v` consumed by André's Theorem A
(`TemperedFundamentalGroups.andreEquiv'`) for the tempered fundamental groups over `F_v`:

* `isAdicComplete`: `O_v` is complete and separated for its `𝔪`-adic topology (the `𝔪`-adic
  topology is the subspace topology from `F_v`, `isAdic`, and `O_v` is closed in the complete
  field `F_v`);
* `henselianLocalRing`: `O_v` is henselian (Hensel's lemma for complete local rings);
* `finite_residueField`: the residue field of `O_v` is finite (it is generated by the image of
  `𝓞 F ⧸ v`, by density of `F` in `F_v`);
* `canonicalValuationSubring_eq`: by F. K. Schmidt's theorem (in
  lana-agents/tempered-fundamental-groups) the canonical valuation subring of `F_v` used by the
  tempered fundamental group (`TemperedFundamentalGroups.canonicalValuationSubring`) is `O_v`;
* `charZero`: `F_v` has characteristic `0`;
* consequently the canonical valuation subring of `F_v` is a complete discrete valuation ring
  with perfect residue field of mixed characteristic (`isDiscreteValuationRing_canonical`,
  `isAdicComplete_canonical`, `perfectField_residueField_canonical`, `exists_prime_canonical`).
-/

namespace Iut.Anabelian.AdicCompletion

open IsDedekindDomain HeightOneSpectrum IsLocalRing Topology NumberField
  TemperedFundamentalGroups
open scoped WithZero

variable {F : Type*} [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F))

local notation "Kv" => v.adicCompletion F
local notation "Ov" => v.adicCompletionIntegers F

/-- `F_v` has characteristic `0`. -/
instance charZero : CharZero Kv :=
  charZero_of_injective_algebraMap (algebraMap F Kv).injective

/-- A uniformizer of `O_v`: an irreducible element, of valuation `< 1`. -/
lemma exists_uniformizer :
    ∃ ϖ : Ov, Irreducible ϖ ∧ Valued.v (ϖ : Kv) < 1 := by
  obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible Ov
  refine ⟨ϖ, hϖ, ?_⟩
  have hint := adicCompletionIntegers.integers F v
  refine lt_of_le_of_ne (hint.map_le_one ϖ) fun h => hϖ.not_isUnit ?_
  exact hint.isUnit_iff_valuation_eq_one.2 h

lemma mem_maximalIdeal_pow {ϖ : Ov} (hϖ : Irreducible ϖ) (n : ℕ) (x : Ov) :
    x ∈ maximalIdeal Ov ^ n ↔ Valued.v (x : Kv) ≤ Valued.v (ϖ : Kv) ^ n := by
  rw [hϖ.maximalIdeal_eq, Ideal.span_singleton_pow, Ideal.mem_span_singleton,
    (adicCompletionIntegers.integers F v).dvd_iff_le, map_pow, map_pow]
  rfl

/-- The `𝔪`-adic topology of `O_v` is its subspace topology from `F_v`. -/
theorem isAdic : IsAdic (maximalIdeal Ov) := by
  obtain ⟨ϖ, hϖ, hlt⟩ := exists_uniformizer v
  have hne : (ϖ : Kv) ≠ 0 := by
    intro h
    exact hϖ.ne_zero (Subtype.ext h)
  rw [isAdic_iff]
  refine ⟨fun n => ?_, fun s hs => ?_⟩
  · have hpow : Valued.v ((ϖ : Kv) ^ n) ≠ 0 := by simp [hne]
    have : ((maximalIdeal Ov ^ n : Ideal Ov) : Set Ov) =
        Subtype.val ⁻¹' ((fun y : Kv => y * ((ϖ : Kv) ^ n)⁻¹) ⁻¹' (Ov : Set Kv)) := by
      ext x
      simp only [SetLike.mem_coe, Set.mem_preimage, mem_maximalIdeal_pow v hϖ,
        mem_adicCompletionIntegers, map_mul, map_inv₀]
      rw [mul_inv_le_iff₀ (zero_lt_iff.2 hpow), one_mul, map_pow]
    rw [this]
    exact ((Valued.isOpen_valuationSubring Kv).preimage (continuous_mul_const _)).preimage
      continuous_subtype_val
  · rw [mem_nhds_subtype] at hs
    obtain ⟨u, hu, hus⟩ := hs
    rw [ZeroMemClass.coe_zero, Valued.mem_nhds_zero] at hu
    obtain ⟨δ, hδ⟩ := hu
    obtain ⟨n, hn⟩ := exists_pow_lt₀ hlt (Units.map (MonoidWithZeroHom.ValueGroup₀.embedding
      (f := .ofClass (Valued.v : Valuation Kv ℤᵐ⁰))) δ)
    refine ⟨n, fun x hx => hus (hδ ?_)⟩
    simp only [Set.mem_setOf_eq, Valuation.restrict_lt_iff_lt_embedding]
    exact ((mem_maximalIdeal_pow v hϖ n x).1 hx).trans_lt hn

/-- **`O_v` is `𝔪`-adically complete.** -/
instance isAdicComplete : IsAdicComplete (maximalIdeal Ov) Ov := by
  rw [(isAdic v).isAdicComplete_iff]
  haveI : IsClosed (Ov : Set Kv) := Valued.isClosed_valuationSubring Kv
  exact ⟨IsClosed.completeSpace_coe, inferInstance⟩

/-- **`O_v` is henselian.** -/
instance henselianLocalRing : HenselianLocalRing Ov :=
  ⟨fun f hf a₀ h₁ h₂ => HenselianRing.is_henselian f hf a₀ h₁ (h₂.map _)⟩

/-- An element of `O_v` of valuation `< 1` lies in the maximal ideal. -/
lemma mem_maximalIdeal_of_lt {y : Ov} (hy : Valued.v (y : Kv) < 1) : y ∈ maximalIdeal Ov := by
  rw [mem_maximalIdeal, mem_nonunits_iff,
    (adicCompletionIntegers.integers F v).isUnit_iff_valuation_eq_one]
  exact hy.ne

/-- An element of `O_v` of valuation `1` is a unit. -/
lemma isUnit_of_eq_one {y : Ov} (hy : Valued.v (y : Kv) = 1) : IsUnit y :=
  (adicCompletionIntegers.integers F v).isUnit_iff_valuation_eq_one.2 hy

lemma valued_algebraMap (r : 𝓞 F) :
    Valued.v ((algebraMap (𝓞 F) Ov r : Ov) : Kv) = v.intValuation r := by
  rw [algebraMap_adicCompletionIntegers_apply]
  exact (valuedAdicCompletion_eq_valuation' (v := v) (algebraMap (𝓞 F) F r)).trans
    (valuation_of_algebraMap v r)

/-- **The residue field of `O_v` is finite.** -/
instance finite_residueField : Finite (ResidueField Ov) := by
  haveI : (v.asIdeal).IsMaximal := v.isPrime.isMaximal v.ne_bot
  letI : Field (𝓞 F ⧸ v.asIdeal) := Ideal.Quotient.field _
  haveI : Finite (𝓞 F ⧸ v.asIdeal) := Ideal.finiteQuotientOfFreeOfNeBot _ v.ne_bot
  -- the reduction map `𝓞 F ⧸ v → κ(O_v)`
  have hker : ∀ r ∈ v.asIdeal, (residue Ov).comp (algebraMap (𝓞 F) Ov) r = 0 := by
    intro r hr
    rw [RingHom.comp_apply, residue_eq_zero_iff]
    apply mem_maximalIdeal_of_lt
    rw [valued_algebraMap]
    exact (v.intValuation_lt_one_iff_mem r).2 hr
  let ψ : 𝓞 F ⧸ v.asIdeal →+* ResidueField Ov := Ideal.Quotient.lift _ _ hker
  have hψ (r : 𝓞 F) : ψ (Ideal.Quotient.mk _ r) = residue Ov (algebraMap (𝓞 F) Ov r) := rfl
  refine Finite.of_surjective (fun pq : (𝓞 F ⧸ v.asIdeal) × (𝓞 F ⧸ v.asIdeal) =>
    ψ pq.1 * (ψ pq.2)⁻¹) ?_
  intro z
  obtain ⟨x, rfl⟩ := residue_surjective z
  -- approximate `x` by an element `a` of `F`
  have hU : {y : Kv | Valued.v (y - (x : Kv)) < 1} ∈ 𝓝 (x : Kv) := by
    rw [Valued.mem_nhds]
    refine ⟨1, fun y hy => ?_⟩
    simpa [Valuation.restrict_lt_iff_lt_embedding] using hy
  obtain ⟨_, ⟨a, rfl⟩, ha⟩ := (denseRange_algebraMap (R := 𝓞 F) F v).inter_nhds_nonempty hU
  have ha' : Valued.v (algebraMap F Kv a - x) < 1 := ha
  have ha1 : Valued.v (algebraMap F Kv a) ≤ 1 := by
    have := Valued.v.map_add (algebraMap F Kv a - x) x
    rw [sub_add_cancel] at this
    exact this.trans (max_le ha'.le x.2)
  have hav : v.valuation F a ≤ 1 :=
    (valuedAdicCompletion_eq_valuation' (v := v) a).symm.trans_le ha1
  obtain ⟨n, d, hnd⟩ := v.exists_primeCompl_mul_eq_of_integer a hav
  let a' : Ov := ⟨algebraMap F Kv a, ha1⟩
  have hxa : residue Ov x = residue Ov a' := by
    apply Ideal.Quotient.eq.2
    apply mem_maximalIdeal_of_lt
    change Valued.v ((x : Kv) - algebraMap F Kv a) < 1
    rwa [Valuation.map_sub_swap]
  have hmul : a' * algebraMap (𝓞 F) Ov d = algebraMap (𝓞 F) Ov n := by
    apply Subtype.ext
    change algebraMap F Kv a * algebraMap F Kv (algebraMap (𝓞 F) F d) =
      algebraMap F Kv (algebraMap (𝓞 F) F n)
    rw [← map_mul, hnd]
  have hd : residue Ov (algebraMap (𝓞 F) Ov d) ≠ 0 := by
    rw [ne_eq, residue_eq_zero_iff]
    refine fun h => (mem_maximalIdeal _).1 h (isUnit_of_eq_one v ?_)
    rw [valued_algebraMap]
    exact (v.intValuation_eq_one_iff_mem_primeCompl d).2 d.prop
  refine ⟨(Ideal.Quotient.mk _ n, Ideal.Quotient.mk _ d), ?_⟩
  simp only [hψ, hxa]
  rw [mul_inv_eq_iff_eq_mul₀ hd, ← map_mul, hmul]

/-- **F. K. Schmidt**: the canonical valuation subring of `F_v`
(`TemperedFundamentalGroups.canonicalValuationSubring`, a henselian discrete valuation ring of
`F_v`, unique by F. K. Schmidt's theorem) is `O_v`. -/
theorem canonicalValuationSubring_eq : canonicalValuationSubring Kv = Ov :=
  canonicalValuationSubring_eq_of_isHenselianDVR ⟨inferInstance, inferInstance⟩

instance isDiscreteValuationRing_canonical :
    IsDiscreteValuationRing (canonicalValuationSubring Kv) := by
  rw [canonicalValuationSubring_eq]
  infer_instance

instance isAdicComplete_canonical :
    IsAdicComplete (maximalIdeal (canonicalValuationSubring Kv))
      (canonicalValuationSubring Kv) := by
  rw [canonicalValuationSubring_eq]
  infer_instance

instance finite_residueField_canonical :
    Finite (ResidueField (canonicalValuationSubring Kv)) := by
  rw [canonicalValuationSubring_eq]
  infer_instance

instance perfectField_residueField_canonical :
    PerfectField (ResidueField (canonicalValuationSubring Kv)) :=
  inferInstance

/-- The canonical valuation subring of `F_v` has **mixed characteristic** `(0, p)`. -/
theorem exists_prime_canonical :
    ∃ p : ℕ, p.Prime ∧ (p : canonicalValuationSubring Kv) ∈ maximalIdeal _ := by
  let κ := ResidueField (canonicalValuationSubring Kv)
  obtain ⟨p, hchar⟩ := CharP.exists κ
  refine ⟨p, (CharP.char_is_prime_or_zero κ p).resolve_right
    (CharP.char_ne_zero_of_finite κ p), ?_⟩
  rw [← residue_eq_zero_iff, map_natCast, CharP.cast_eq_zero κ p]

end Iut.Anabelian.AdicCompletion