Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_PlaceCompletion.lean

definition module

Adic completions at places and their functoriality

Throughout, a place V of a field extension F/K is the project's Place K F: a valuation subring \mathcal O_V\subseteq F containing \operatorname{im}(K\to F), proper in F and a principal ideal ring, hence a discrete valuation ring, with heightOneSpectrum its maximal ideal, adicValuation the induced \mathbb Z^{m0}-valued valuation on F and ord minus its logarithm. Here adicCompletion and adicCompletionIntegers name the completion \hat F_V of F at that height-one prime and its valuation subring \hat{\mathcal O}_V, in Mathlib's sense.

For K\subseteq F\subseteq F' with F'/F integral and a place W of F', write V=W.\mathrm{restrict}\,F (the contraction of \mathcal O_W along F\to F') and e=W.\mathrm{ramificationIndex}\,F (the least positive value attained by \mathrm{ord}_W on nonzero elements of F). The valuation identity v_W(\iota x)=v_V(x)^e is proved on F, then on the WithVal models, where the induced map is shown uniformly continuous; completing it gives the ring homomorphism kw_ffgc_adicCompletionComap \hat F_V\to\hat{F'}_W, continuous, compatible with the coercions from F, and satisfying v(\varphi x)=v(x)^e; it carries \hat{\mathcal O}_V into \hat{\mathcal O}_W, whence a map of integer rings and the corresponding algebra structures, scalar towers and continuity of scalar multiplication. Further declarations: a rank-one structure on the valuation of \hat F_V coming from its discreteness (base 2), the real absolute value y\mapsto\lVert y\rVert^{1/e} on \hat{F'}_W, compatibility of the two algebra maps out of F, the \hat F_V-linear map sending a family of coefficients to the corresponding combination of the images of an F-basis of F', its dense range, finite-dimensionality of \hat{F'}_W over \hat F_V when [F':F]<\infty, the trace \operatorname{Tr}_{\hat{F'}_W/\hat F_V} and its F-linear restriction along F'\to\hat{F'}_W. Finally: v_V of the image of x\in F equals V.\mathrm{adicValuation}\,x; the image lies in \hat{\mathcal O}_V exactly when x\in\mathcal O_V; every element of \hat F_V differs from an element of F by an element of \hat{\mathcal O}_V; and K maps into \hat{\mathcal O}_V, giving \hat{\mathcal O}_V a K-algebra structure. A general instance makes any K-algebra an algebra over a valuation subring of K.

Relation to Mathlib

The completion and its integers are Mathlib's IsDedekindDomain.HeightOneSpectrum.adicCompletion for the maximal ideal of the valuation ring of a Place; Place, its restrict and ramificationIndex are the project's own notions, and the map between completions along restrict, together with the associated algebra and trace structure, is built here.

Where it is used

These definitions supply the local vocabulary (completions at places, ramification indices, local traces and approximation by global elements) used in the project's treatment of divisors and residues on curves, which feeds the modular-curve part of the argument.

References

  1. J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer, 1979
  2. J. Tate, Residues of differentials on curves, Annales scientifiques de l'École Normale Supérieure (4) 1 (1968), 149–159
  3. H. Stichtenoth, Algebraic Function Fields and Codes, Springer, 1993

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_AlgebraicCurve_PlaceCompletion.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicCurve_DivisorClassGroup
import Definitions.Def_AlgebraicCurve_DivisorPushPull
import Definitions.Def_DedekindDomain_AdicValuation_InlineSpecific

set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 1600000

instance {K L : Type*} [Field K] [Semiring L] (O : ValuationSubring K) [Algebra K L] :
    Algebra O L where
  smul r x := r.1 • x
  algebraMap := (algebraMap K L).comp (algebraMap O K)
  commutes' _ _ := by simp [Algebra.commutes]
  smul_def' _ _ := by simp [← Algebra.smul_def]; rfl

set_option autoImplicit false

set_option synthInstance.maxHeartbeats 800000
set_option maxHeartbeats 1600000

noncomputable section

open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom

namespace AlgebraicCurve.Place

section AdicCompletion

variable {K F : Type*} [Field K] [Field F] [Algebra K F] (V : Place K F)

abbrev adicCompletion : Type _ := V.heightOneSpectrum.adicCompletion F

abbrev adicCompletionIntegers : ValuationSubring V.adicCompletion :=
  V.heightOneSpectrum.adicCompletionIntegers F

end AdicCompletion

section WithValLevel

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

theorem kw_ffgc_adicValuation_algebraMap (x : F) :
    W.adicValuation (algebraMap F F' x)
      = (W.restrict F).adicValuation x ^ W.ramificationIndex F := by
  rcases eq_or_ne x 0 with rfl | hx
  · simp [adicValuation, zero_pow (W.ramificationIndex_pos (F := F)).ne']
  · have hord := W.ord_restrict (F := F) x
    have hax : algebraMap F F' x ≠ 0 :=
      (map_ne_zero_iff _ (algebraMap F F').injective).mpr hx
    have hV0 : (W.restrict F).adicValuation x ≠ 0 := (W.restrict F).adicValuation_ne_zero hx
    have hW0 : W.adicValuation (algebraMap F F' x) ≠ 0 := W.adicValuation_ne_zero hax
    unfold ord at hord
    have hlog : WithZero.log (W.adicValuation (algebraMap F F' x))
        = WithZero.log ((W.restrict F).adicValuation x ^ W.ramificationIndex F) := by
      rw [← zpow_natCast, log_zpow, zsmul_eq_mul, Int.cast_natCast]; linarith
    rw [← exp_log hW0, hlog, exp_log (pow_ne_zero _ hV0)]

theorem kw_ffgc_valued_withValMapAlgebraMap
    (x : WithVal ((W.restrict F).heightOneSpectrum.valuation F)) :
    Valued.v (WithVal.map ((W.restrict F).heightOneSpectrum.valuation F)
      (W.heightOneSpectrum.valuation F') (algebraMap F F') x)
        = Valued.v x ^ W.ramificationIndex F := by
  rw [WithVal.map_apply, WithVal.valued_toVal]
  exact kw_ffgc_adicValuation_algebraMap F W x.ofVal

set_option backward.isDefEq.respectTransparency false in

theorem kw_ffgc_uniformContinuous_withValMapAlgebraMap :
    UniformContinuous (WithVal.map ((W.restrict F).heightOneSpectrum.valuation F)
      (W.heightOneSpectrum.valuation F') (algebraMap F F')) := by
  refine uniformContinuous_of_continuousAt_zero _ ?_
  simp_rw [ContinuousAt, map_zero, (Valued.hasBasis_nhds_zero _ _).tendsto_iff
    (Valued.hasBasis_nhds_zero _ _), true_and, forall_const]
  intro γ

  have hγ0 : (ValueGroup₀.embedding (γ.val) : ℤᵐ⁰) ≠ 0 :=
    (γ.isUnit.map ValueGroup₀.embedding).ne_zero
  have hc0 : min (ValueGroup₀.embedding γ.val) (1 : ℤᵐ⁰) ≠ 0 :=
    (lt_min (zero_lt_iff.mpr hγ0) zero_lt_one).ne'

  obtain ⟨x₀, hx₀⟩ :=
    (W.restrict F).heightOneSpectrum.valuation_surjective F
      (min (ValueGroup₀.embedding γ.val) 1)
  have hx₀v : Valued.v (WithVal.toVal ((W.restrict F).heightOneSpectrum.valuation F) x₀) =
      min (ValueGroup₀.embedding γ.val) 1 := by
    rw [WithVal.valued_toVal, hx₀]
  have hδ0 : Valued.v.restrict
      (WithVal.toVal ((W.restrict F).heightOneSpectrum.valuation F) x₀) ≠ 0 := by
    rw [ne_eq, Valuation.restrict_eq_zero_iff, hx₀v]
    exact hc0
  refine ⟨Units.mk0 _ hδ0, fun x hx => ?_⟩
  simp only [Set.mem_setOf_eq, Units.val_mk0] at hx ⊢
  rw [Valuation.restrict_lt_iff, hx₀v] at hx

  rw [Valuation.restrict_lt_iff_lt_embedding, kw_ffgc_valued_withValMapAlgebraMap F W x]

  calc Valued.v x ^ W.ramificationIndex F
      ≤ Valued.v x ^ 1 :=
        pow_le_pow_right_of_le_one' (hx.trans_le (min_le_right _ _)).le
          (W.ramificationIndex_pos (F := F))
    _ = Valued.v x := pow_one _
    _ < ValueGroup₀.embedding γ.val := hx.trans_le (min_le_left _ _)

end WithValLevel

section CompletionComap

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

def kw_ffgc_adicCompletionComap : (W.restrict F).adicCompletion →+* W.adicCompletion :=
  ((IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv F' W.heightOneSpectrum).symm.toRingHom.comp
    (UniformSpace.Completion.mapRingHom
      (WithVal.map ((W.restrict F).heightOneSpectrum.valuation F)
        (W.heightOneSpectrum.valuation F') (algebraMap F F'))
      (kw_ffgc_uniformContinuous_withValMapAlgebraMap F W).continuous)).comp
    (IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv F (W.restrict F).heightOneSpectrum).toRingHom

theorem kw_ffgc_continuous_adicCompletionComap :
    Continuous (kw_ffgc_adicCompletionComap F W) := by
  have h : ⇑(kw_ffgc_adicCompletionComap F W) =
      IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion ∘ UniformSpace.Completion.map
        (WithVal.map ((W.restrict F).heightOneSpectrum.valuation F)
          (W.heightOneSpectrum.valuation F') (algebraMap F F')) ∘
        IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion := rfl
  rw [h]
  exact (IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_ofCompletion F' _).comp
    (UniformSpace.Completion.continuous_map.comp
      (IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_toCompletion F _))

theorem kw_ffgc_adicCompletionComap_coe
    (x : WithVal ((W.restrict F).heightOneSpectrum.valuation F)) :
    kw_ffgc_adicCompletionComap F W (x : (W.restrict F).adicCompletion)
      = (WithVal.map ((W.restrict F).heightOneSpectrum.valuation F)
          (W.heightOneSpectrum.valuation F') (algebraMap F F') x : W.adicCompletion) :=
  by
  apply IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
  exact UniformSpace.Completion.mapRingHom_coe
    (kw_ffgc_uniformContinuous_withValMapAlgebraMap F W).continuous x

open WithZeroTopology in

theorem kw_ffgc_valued_adicCompletionComap (x : (W.restrict F).adicCompletion) :
    Valued.v (kw_ffgc_adicCompletionComap F W x)
      = Valued.v x ^ W.ramificationIndex F := by
  obtain ⟨x, rfl⟩ :=
    IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_surjective F _ x
  induction x using UniformSpace.Completion.induction_on with
  | hp =>
    refine isClosed_eq
      ((Valued.continuous_valuation_of_surjective
        (W.heightOneSpectrum.valuedAdicCompletion_surjective F')).comp
        ((kw_ffgc_continuous_adicCompletionComap F W).comp
          (IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_ofCompletion F _)))
      (((Valued.continuous_valuation_of_surjective
        ((W.restrict F).heightOneSpectrum.valuedAdicCompletion_surjective F)).comp
          (IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_ofCompletion F _)).pow _)
  | ih a =>
    rw [kw_ffgc_adicCompletionComap_coe]
    simp only [IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion,
      Valued.valuedCompletion_apply]
    exact kw_ffgc_valued_withValMapAlgebraMap F W a

end CompletionComap

end AlgebraicCurve.Place

set_option autoImplicit false

set_option synthInstance.maxHeartbeats 800000
set_option maxHeartbeats 1600000

noncomputable section

open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero MonoidWithZeroHom

namespace AlgebraicCurve.Place

section IntegerComap

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

theorem kw_ffgc_adicCompletionComap_mem_integers
    {x : (W.restrict F).adicCompletion} (hx : x ∈ (W.restrict F).adicCompletionIntegers) :
    kw_ffgc_adicCompletionComap F W x ∈ W.adicCompletionIntegers := by
  rw [HeightOneSpectrum.mem_adicCompletionIntegers] at hx ⊢
  rw [kw_ffgc_valued_adicCompletionComap]
  exact pow_le_one' hx _

def kw_ffgc_adicCompletionComapIntegers :
    (W.restrict F).adicCompletionIntegers →+* W.adicCompletionIntegers :=
  (kw_ffgc_adicCompletionComap F W).restrict _ _
    fun _ hx => kw_ffgc_adicCompletionComap_mem_integers F W hx

@[simp]
theorem kw_ffgc_adicCompletionComapIntegers_coe
    (x : (W.restrict F).adicCompletionIntegers) :
    (kw_ffgc_adicCompletionComapIntegers F W x : W.adicCompletion)
      = kw_ffgc_adicCompletionComap F W (x : (W.restrict F).adicCompletion) := rfl

end IntegerComap

end AlgebraicCurve.Place

set_option autoImplicit false
set_option synthInstance.maxHeartbeats 800000
set_option maxHeartbeats 1600000

noncomputable section

open Polynomial IsLocalRing IsDedekindDomain

namespace AlgebraicCurve.Place

section CompletionAlgebra

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

scoped instance kw_ffgc_algebraAdicCompletionComap :
    Algebra (W.restrict F).adicCompletion W.adicCompletion :=
  (kw_ffgc_adicCompletionComap F W).toAlgebra

theorem kw_ffgc_algebraMap_adicCompletionComap_eq :
    algebraMap (W.restrict F).adicCompletion W.adicCompletion
      = kw_ffgc_adicCompletionComap F W := rfl

scoped instance kw_ffgc_algebraAdicCompletionComapIntegers :
    Algebra (W.restrict F).adicCompletionIntegers W.adicCompletionIntegers :=
  (kw_ffgc_adicCompletionComapIntegers F W).toAlgebra

scoped instance kw_ffgc_algebraAdicCompletionIntegersToCompletion :
    Algebra (W.restrict F).adicCompletionIntegers W.adicCompletion :=
  ((kw_ffgc_adicCompletionComap F W).comp
    (algebraMap (W.restrict F).adicCompletionIntegers (W.restrict F).adicCompletion)).toAlgebra

instance kw_ffgc_isScalarTower_integersCompletionCompletion :
    IsScalarTower (W.restrict F).adicCompletionIntegers
      (W.restrict F).adicCompletion W.adicCompletion :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

instance kw_ffgc_isScalarTower_integersIntegersCompletion :
    IsScalarTower (W.restrict F).adicCompletionIntegers
      W.adicCompletionIntegers W.adicCompletion :=
  IsScalarTower.of_algebraMap_eq fun x => (kw_ffgc_adicCompletionComapIntegers_coe F W x).symm

end CompletionAlgebra

section SpectralSetup

open scoped Valued NNReal WithZero

open WithZeroMulInt Valuation.IsRankOneDiscrete

variable {K F : Type*} [Field K] [Field F] [Algebra K F] (V : Place K F)

@[implicit_reducible]
noncomputable def kw_ffgc_rankOne_adicCompletion :
    (Valued.v : Valuation V.adicCompletion ℤᵐ⁰).RankOne :=
  Valuation.IsRankOneDiscrete.rankOne _ (one_lt_two (α := ℝ≥0))

end SpectralSetup

section AbsoluteValue

open scoped Valued NNReal WithZero

open WithZeroMulInt Valuation.IsRankOneDiscrete

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

noncomputable def kw_ffgc_absoluteValue : AbsoluteValue W.adicCompletion ℝ :=
  letI := kw_ffgc_rankOne_adicCompletion W
  have hr : (0 : ℝ) < ((W.ramificationIndex F : ℝ))⁻¹ :=
    inv_pos.mpr (Nat.cast_pos.mpr (W.ramificationIndex_pos (F := F)))
  { toFun := fun y => ‖y‖ ^ ((W.ramificationIndex F : ℝ))⁻¹
    map_mul' := fun x y => by rw [norm_mul, Real.mul_rpow (norm_nonneg x) (norm_nonneg y)]
    nonneg' := fun x => Real.rpow_nonneg (norm_nonneg x) _
    eq_zero' := fun x => by
      rw [Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg x), norm_eq_zero]
      exact ⟨fun h => h.1, fun h => ⟨h, hr.ne'⟩⟩
    add_le' := fun x y => by
      have hmax : ‖x + y‖ ≤ max ‖x‖ ‖y‖ := Valuation.norm_add_le Valued.v x y
      refine (Real.rpow_le_rpow (norm_nonneg _) hmax hr.le).trans ?_
      rcases max_cases ‖x‖ ‖y‖ with ⟨hm, _⟩ | ⟨hm, _⟩ <;> rw [hm]
      · exact le_add_of_nonneg_right (Real.rpow_nonneg (norm_nonneg _) _)
      · exact le_add_of_nonneg_left (Real.rpow_nonneg (norm_nonneg _) _) }

end AbsoluteValue

section ClosedAdjoin

open scoped Valued NNReal WithZero

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

instance kw_ffgc_continuousSMul_adicCompletionComap :
    ContinuousSMul (W.restrict F).adicCompletion W.adicCompletion :=
  continuousSMul_of_algebraMap _ _ (by
    rw [kw_ffgc_algebraMap_adicCompletionComap_eq]
    exact kw_ffgc_continuous_adicCompletionComap F W)

end ClosedAdjoin

end AlgebraicCurve.Place

set_option autoImplicit false
set_option synthInstance.maxHeartbeats 800000
set_option maxHeartbeats 1600000

noncomputable section

open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing WithZero

open scoped Valued WithZero

namespace AlgebraicCurve.Place

section FiniteDimensional

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

theorem kw_ffgc_adicCompletionComap_algebraMap_algebraMap (c : F) :
    algebraMap F' W.adicCompletion (algebraMap F F' c)
      = algebraMap (W.restrict F).adicCompletion W.adicCompletion
          (algebraMap F (W.restrict F).adicCompletion c) := by
  rw [kw_ffgc_algebraMap_adicCompletionComap_eq,
    show algebraMap F (W.restrict F).adicCompletion c
      = ((WithVal.toVal ((W.restrict F).heightOneSpectrum.valuation F) c
          : WithVal ((W.restrict F).heightOneSpectrum.valuation F))
          : (W.restrict F).adicCompletion) from rfl,
    kw_ffgc_adicCompletionComap_coe]
  rfl

theorem kw_ffgc_algebraMap_smul_algebraMap (c : F) (b : F') :
    algebraMap F (W.restrict F).adicCompletion c • algebraMap F' W.adicCompletion b
      = algebraMap F' W.adicCompletion (c • b) := by
  rw [Algebra.smul_def, Algebra.smul_def, map_mul,
    kw_ffgc_adicCompletionComap_algebraMap_algebraMap]

def kw_ffgc_completionLinearCombination {ι : Type*} [Fintype ι] (b : Module.Basis ι F F') :
    (ι → (W.restrict F).adicCompletion)
      →ₗ[(W.restrict F).adicCompletion] W.adicCompletion :=
  Fintype.linearCombination (W.restrict F).adicCompletion
    (fun i => algebraMap F' W.adicCompletion (b i))

theorem kw_ffgc_denseRange_completionLinearCombination {ι : Type*} [Fintype ι]
    (b : Module.Basis ι F F') :
    DenseRange (kw_ffgc_completionLinearCombination F W b) := by
  apply (IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap F' W.heightOneSpectrum).mono
  rintro _ ⟨l, rfl⟩
  refine ⟨fun i => algebraMap F (W.restrict F).adicCompletion (b.repr l i), ?_⟩
  simp only [kw_ffgc_completionLinearCombination, Fintype.linearCombination_apply,
    kw_ffgc_algebraMap_smul_algebraMap, ← map_sum]
  congr 1
  exact b.sum_repr l

instance kw_ffgc_finiteDimensional_adicCompletion [FiniteDimensional F F'] :
    FiniteDimensional (W.restrict F).adicCompletion W.adicCompletion := by
  letI := kw_ffgc_rankOne_adicCompletion (W.restrict F)
  letI : NontriviallyNormedField (W.restrict F).adicCompletion :=
    Valued.toNontriviallyNormedField (W.restrict F).adicCompletion ℤᵐ⁰
  let b := Module.finBasis F F'
  exact Module.Finite.of_surjective (kw_ffgc_completionLinearCombination F W b) (by
    rw [← Set.range_eq_univ, ← LinearMap.coe_range,
      ← (LinearMap.range
          (kw_ffgc_completionLinearCombination F W b)).closed_of_finiteDimensional.closure_eq]
    exact (kw_ffgc_denseRange_completionLinearCombination F W b).closure_range)

end FiniteDimensional

section CompletionTrace

variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (F)
variable [Algebra F F'] [IsScalarTower K F F'] [Algebra.IsIntegral F F'] (W : Place K F')

abbrev kw_ffgc_completionTrace [FiniteDimensional F F'] :
    W.adicCompletion →ₗ[(W.restrict F).adicCompletion] (W.restrict F).adicCompletion :=
  Algebra.trace (W.restrict F).adicCompletion W.adicCompletion

def kw_ffgc_completionTraceF' [FiniteDimensional F F'] : F' →ₗ[F] (W.restrict F).adicCompletion :=
  { toFun := fun g => kw_ffgc_completionTrace F W (algebraMap F' W.adicCompletion g)
    map_add' := fun x y => by simp only [map_add]
    map_smul' := fun c x => by
      simp only [Algebra.smul_def, map_mul, RingHom.id_apply,
        kw_ffgc_adicCompletionComap_algebraMap_algebraMap]
      rw [← Algebra.smul_def, LinearMap.map_smul, Algebra.smul_def]
      rfl }

end CompletionTrace

end AlgebraicCurve.Place

set_option autoImplicit false
set_option maxHeartbeats 1600000
set_option synthInstance.maxHeartbeats 800000
set_option linter.unusedSectionVars false

open AlgebraicCurve AlgebraicCurve.Place IsDedekindDomain

noncomputable section

namespace AlgebraicCurve

section LocalResidueCompletion

variable {K E : Type*} [Field K] [Field E] [Algebra K E]

theorem kwHgfV352_valued_algebraMap_adicCompletion (v : Place K E) (x : E) :
    Valued.v (algebraMap E v.adicCompletion x) = v.heightOneSpectrum.valuation E x := by
  have h := IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation'
    (K := E) v.heightOneSpectrum x
  first
    | exact h
    | (rw [IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion]; exact h)

namespace Place

private theorem mem_of_ord_nonneg_placeCompletionAux {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring := by
  obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible v.toValuationSubring
  obtain ⟨u, hu⟩ := v.exists_unit_mul_zpow hf hπ
  rw [hu, show v.ord f = (((v.ord f).toNat : ℕ) : ℤ) from (Int.toNat_of_nonneg h).symm,
    zpow_natCast]
  exact mul_mem (u : v.toValuationSubring).2 (pow_mem (π : v.toValuationSubring).2 _)

private theorem ord_nonneg_of_mem_placeCompletionAux {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f := by
  rcases eq_or_ne f 0 with rfl | hf0
  · simp
  obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible v.toValuationSubring
  obtain ⟨n, u, hu⟩ :=
    IsDiscreteValuationRing.eq_unit_mul_pow_irreducible
      (x := (⟨f, hf⟩ : v.toValuationSubring)) (by simpa [Subtype.ext_iff] using hf0) hπ
  have hcoe : f = ((u : v.toValuationSubring) : F) * ((π : F) ^ (n : ℤ)) := by
    have h := congrArg (Subtype.val) hu
    push_cast at h
    rw [zpow_natCast]
    exact h
  rw [hcoe, v.ord_unit_smul_zpow u hπ (n : ℤ)]
  exact Int.natCast_nonneg n

end Place

theorem kwHgfV352_algebraMap_mem_adicCompletionIntegers_iff (v : Place K E) (x : E) :
    algebraMap E v.adicCompletion x ∈ v.adicCompletionIntegers ↔ x ∈ v.toValuationSubring := by
  rcases eq_or_ne x 0 with rfl | hx0
  · simp only [map_zero]; exact iff_of_true (zero_mem _) (zero_mem _)
  have hval : Valued.v (algebraMap E v.adicCompletion x) = v.adicValuation x :=
    kwHgfV352_valued_algebraMap_adicCompletion v x
  have hne : v.adicValuation x ≠ 0 := v.adicValuation_ne_zero hx0
  have hlog_iff : WithZero.log (v.adicValuation x) ≤ 0 ↔ v.adicValuation x ≤ 1 := by
    rw [WithZero.log_le_iff_le_exp hne, WithZero.exp_zero]
  constructor
  · intro h
    refine v.mem_of_ord_nonneg_placeCompletionAux hx0 (neg_nonneg.mpr ?_)
    exact hlog_iff.mpr (hval ▸ h)
  · intro h
    show Valued.v (algebraMap E v.adicCompletion x) ≤ 1
    rw [hval]
    exact hlog_iff.mp (neg_nonneg.mp (v.ord_nonneg_of_mem_placeCompletionAux h))

theorem kwHgfV352_exists_sub_mem_adicCompletionIntegers (v : Place K E)
    (xh : v.adicCompletion) :
    ∃ x : E, algebraMap E v.adicCompletion x - xh ∈ v.adicCompletionIntegers := by
  have hdense : DenseRange (algebraMap E v.adicCompletion) :=
    IsDedekindDomain.HeightOneSpectrum.denseRange_algebraMap E v.heightOneSpectrum
  have hopen : IsOpen ((xh + ·) '' (v.adicCompletionIntegers : Set v.adicCompletion)) :=
    (Homeomorph.addLeft xh).isOpenMap _ (Valued.isOpen_valuationSubring v.adicCompletion)
  have hmem : xh ∈ (xh + ·) '' (v.adicCompletionIntegers : Set v.adicCompletion) :=
    ⟨0, zero_mem _, by simp⟩
  obtain ⟨e, he⟩ := hdense.exists_mem_open hopen ⟨xh, hmem⟩
  obtain ⟨o, hoMem, hoEq⟩ := he
  exact ⟨e, by rw [← hoEq]; simpa using hoMem⟩

end LocalResidueCompletion

end AlgebraicCurve

set_option autoImplicit false
set_option maxHeartbeats 1600000
set_option synthInstance.maxHeartbeats 800000
set_option linter.unusedSectionVars false

open AlgebraicCurve AlgebraicCurve.Place LinearMap Submodule
open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum IsLocalRing

noncomputable section

namespace ModularCurve.KwF4gRRTate

section PoleWindowShift

variable {K L : Type*} [Field K] [Field L] [Algebra K L] (u : Place K L)

theorem algebraMap_K_mem_adicCompletionIntegers (c : K) :
    algebraMap K u.adicCompletion c ∈ u.adicCompletionIntegers := by
  rw [IsScalarTower.algebraMap_apply K L u.adicCompletion]
  exact (kwHgfV352_algebraMap_mem_adicCompletionIntegers_iff u _).mpr (u.algebraMap_mem' c)

def algebraMapKIntegers : K →+* u.adicCompletionIntegers where
  toFun c := ⟨algebraMap K u.adicCompletion c, algebraMap_K_mem_adicCompletionIntegers u c⟩
  map_one' := Subtype.ext (map_one _)
  map_mul' x y := Subtype.ext (map_mul _ x y)
  map_zero' := Subtype.ext (map_zero _)
  map_add' x y := Subtype.ext (map_add _ x y)

instance instAlgebraKAdicCompletionIntegers : Algebra K u.adicCompletionIntegers :=
  (algebraMapKIntegers u).toAlgebra

end PoleWindowShift

end ModularCurve.KwF4gRRTate

end

Statements phrased using this module (8)