/-
Copyright (c) 2026. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
-/
-- Targeted Mathlib imports rather than `import Mathlib`: the project's
-- `«Adic spaces».RestrictedPowerSeries` declares `MvPowerSeries.IsRestricted`, which clashes
-- with Mathlib's module of the same name, and `Solution.lean` must import both this file and
-- the library. A narrow import list is also easier for a reader to audit.
import Mathlib.RingTheory.Valuation.ValuativeRel.Basic
import Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
import Mathlib.RingTheory.Localization.Away.Basic
import Mathlib.Topology.Algebra.UniformRing
import Mathlib.Topology.Category.TopCommRingCat
import Mathlib.Topology.Sheaves.Sheaf
import Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.Analysis.Normed.Group.Ultra
import Mathlib.Analysis.Normed.Group.Completion
import Mathlib.Analysis.Normed.Module.Completion
import Mathlib.Analysis.Normed.Field.Basic
import Mathlib.Algebra.MonoidAlgebra.Basic
import Mathlib.Topology.Algebra.Valued.NormedValued
import Mathlib.Topology.Algebra.Valued.ValuedField
import Mathlib.RingTheory.DiscreteValuationRing.Basic
import Mathlib.Topology.Algebra.Ring.Basic
import Mathlib.RingTheory.Noetherian.Defs
import Mathlib.Topology.MetricSpace.Ultra.Basic

/-!
# Palomar challenge — the definitions (GENERATED from `Challenge.lean`)

**Do not edit.** This file is `Challenge.lean` minus its statements section,
regenerated by `scripts/gen-defs.py`. It exists because Comparator's Solution module must
contain the same definitions as the Challenge without importing the Challenge module.

The headline theorem of *Uniform sheafy Tate rings that are not stably uniform*
(Birkbeck–Torzewski, Theorem 1.1) — the finite-jet pinching algebra `𝓐` over a complete
discretely valued nonarchimedean field is a uniform, strongly sheafy, nonnoetherian Tate domain
with `𝓐° = 𝓐₀` that is **not stably uniform** — as nine statements with `sorry` proofs in §12,
for verification by [leanprover/comparator](https://github.com/leanprover/comparator) against
`Solution.lean`. This answers Question 7 of Kedlaya's *Nonarchimedean Scottish Book*
(is a sheafy uniform Huber pair stably uniform?) in the negative.

## Why this file repeats the definitions

Palomar requires a Challenge's import closure to be Mathlib-only, and Mathlib has no theory of
Huber rings or adic spaces; so every notion the statements use is defined here, following
Wedhorn's *Adic Spaces* (cited by number). §§1–3: bounded sets, Huber/Tate rings, uniformity.
§4: `Spv`, continuous valuations, `Spa (A, A⁺)`, rings of integral elements, rational subsets.
§§5–6: the localisation topology on `Aₛ`, the completed rational localisation `A⟨T/s⟩`
(Wedhorn §8.1), stable uniformity. §§7–8: the structure presheaf `𝒪_X(V) = lim A⟨T/s⟩` as a
`TopCat.Presheaf TopCommRingCat`, and **sheafiness** as Mathlib's `TopCat.Presheaf.IsSheaf`
(Wedhorn 8.26). The restriction maps are carried as a `RestrictionFamily` — data compatible
with the canonical maps from `A`, which pins them uniquely — rather than constructed;
`IsSheafy` asserts that one exists and that the resulting presheaf is a sheaf;
`IsSheafyComplete` is sheafiness for every ring of integral elements. §§9–11: `R⟨G⟩` is the
completion of `R[G]` for the Gauss norm; `𝓐` is the closure in `K⟨W, W⁻¹, Q⟩` of the polynomials
`f₀(W) + Q f₁(W) + Q² h`, `f₀, f₁ ∈ K[W]` ([FJP] (1.7)); `𝓐⟨X₁, …, Xₙ⟩ = Completion 𝓐[X]`; the
unit ball with a constant of norm `< 1` is a pair of definition, so `𝓐` is Tate.

`Solution.lean` proves each statement by showing these notions agree with the
library's (`Palomar/Bridge.lean`: same completed localisations, unique restriction families,
sheafiness here ↔ the library's rational-cover criterion; `Palomar/Bridge/Jet.lean`,
`Palomar/Bridge/TateExt.lean`: the rings are isometrically isomorphic to the library's) and
forwarding the library's theorems — so the certificate is about those theorems, not a private
vocabulary.

## Conventions and limitations

`K` is any complete ultrametric nontrivially normed field with DVR valuation ring (the paper's
complete discretely valued field) — a general base, not a witness field. `IsSheafyComplete`
quantifies over every `𝓐⁺`; the paper's "(𝓐, 𝓐°) sheafy" is the case `𝓐⁺ = 𝓐°`. Sheafiness
is defined at Tate (analytic) scope, where Proposition 8.2's restriction maps exist; `𝓐` and
its Tate algebras are Tate. One instance (`IsTopologicalRing R[G]`) is named at high priority
only so the statements elaborate identically in both environments; it is the same instance.

## References

* [T. Wedhorn, *Adic Spaces*][arXiv:1910.05934], §§5–8.
* [FJP] C. Birkbeck, A. Torzewski, *Uniform sheafy Tate rings that are not stably uniform*,
  https://cbirkbeck.github.io/uniform-sheafy-tate-domains/ — Definition 1.2, (1.7), Theorem 1.1.
-/

-- Style linters only: explicit `[IsTopologicalRing A]` binders and `Prop`-valued `def`s below
-- are deliberate (they mirror the library). Neither affects what is stated.
set_option linter.overlappingInstances false
set_option linter.defProp false

namespace Palomar

open Filter Topology Pointwise

universe u

/-! ## 1. Bounded and power-bounded subsets (Wedhorn §5) -/

section Bounded

variable {A : Type*} [CommRing A] [TopologicalSpace A]

/-- A subset `S ⊆ A` is **bounded** if for every neighbourhood `U` of `0` there is a
neighbourhood `V` of `0` with `S * V ⊆ U` (Wedhorn Definition 5.24). -/
def IsBounded (S : Set A) : Prop :=
  ∀ U ∈ 𝓝 (0 : A), ∃ V ∈ 𝓝 (0 : A), S * V ⊆ U

/-- An element `a` is **power-bounded** if `{aⁿ | n : ℕ}` is bounded
(Wedhorn Definition 5.27). -/
def IsPowerBounded (a : A) : Prop :=
  IsBounded (Set.range (a ^ · : ℕ → A))

/-- `A°`, the set of power-bounded elements of `A` (Wedhorn Definition 5.27). -/
def powerBoundedSubring (A : Type*) [CommRing A] [TopologicalSpace A] : Set A :=
  {a : A | IsPowerBounded a}

end Bounded

/-! ## 2. Huber rings and Tate rings (Wedhorn §6) -/

section Huber

/-- A **pair of definition** `(A₀, I)` for a topological ring `A`: an open subring `A₀`
together with a finitely generated ideal `I ⊆ A₀` whose `I`-adic topology is the subspace
topology (Wedhorn Definition 6.1). -/
structure PairOfDefinition (A : Type*) [CommRing A] [TopologicalSpace A] where
  /-- The ring of definition `A₀`, an open subring of `A`. -/
  A₀ : Subring A
  /-- The ideal of definition `I`, an ideal of `A₀`. -/
  I : Ideal A₀
  /-- `A₀` is open in `A`. -/
  isOpen : IsOpen (A₀ : Set A)
  /-- `I` is finitely generated. -/
  fg : I.FG
  /-- The subspace topology on `A₀` is the `I`-adic topology. -/
  isAdic : IsAdic I

/-- A topological ring is a **Huber ring** (f-adic ring) if it admits a pair of definition
(Wedhorn Definition 6.1). -/
class IsHuberRing (A : Type*) [CommRing A] [TopologicalSpace A] : Prop
    extends IsTopologicalRing A where
  /-- There exists a pair of definition. -/
  exists_pairOfDefinition : Nonempty (PairOfDefinition A)

/-- A Huber ring is a **Tate ring** if it contains a topologically nilpotent unit
(Wedhorn Definition 6.10). -/
class IsTateRing (A : Type*) [CommRing A] [TopologicalSpace A] : Prop extends IsHuberRing A where
  /-- There exists a topologically nilpotent unit. -/
  exists_topologicallyNilpotent_unit : ∃ u : Aˣ, IsTopologicallyNilpotent (u : A)

end Huber

/-! ## 3. Uniform rings (Wedhorn Definition 7.36) -/

section Uniform

variable (A : Type*) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]

/-- A topological ring is **uniform** if `A°` is bounded (Wedhorn Definition 7.36). -/
class IsUniform : Prop where
  /-- The set `A°` of power-bounded elements is bounded. -/
  isBounded_powerBounded : IsBounded (powerBoundedSubring A)

end Uniform

/-! ## 4. The adic spectrum (Wedhorn §7) -/

section AdicSpectrum

/-- The **valuation spectrum** `Spv A`: valuative relations on `A`
(Wedhorn Definition 4.1, in Mathlib's `ValuativeRel` presentation). -/
structure ValuationSpectrum (A : Type*) [CommRing A] extends ValuativeRel A

@[inherit_doc] notation "Spv" => ValuationSpectrum

namespace ValuationSpectrum

variable {A : Type*} [CommRing A]

/-- The basic open `Spv(A)(f/s) = { v | v f ≤ v s, v s ≠ 0 }` (Wedhorn Definition 4.1). -/
def basicOpen (f s : A) : Set (Spv A) :=
  { v | v.vle f s ∧ ¬ v.vle s 0 }

/-- `Spv A` carries the topology generated by the basic opens. -/
instance instTopologicalSpace : TopologicalSpace (Spv A) :=
  TopologicalSpace.generateFrom { U | ∃ f s : A, U = basicOpen f s }

/-- A point of `Spv A` is **continuous** if its canonical valuation is
(Wedhorn Definition 7.7). -/
def IsContinuous [TopologicalSpace A] (v : Spv A) : Prop :=
  letI : ValuativeRel A := v.toValuativeRel
  ∀ γ : (ValuativeRel.ValueGroupWithZero A), IsOpen { a : A | ValuativeRel.valuation A a < γ }

/-- `Cont A`, the set of continuous points of `Spv A` (Wedhorn Definition 7.7). -/
def Cont (A : Type*) [CommRing A] [TopologicalSpace A] : Set (Spv A) :=
  { v : Spv A | v.IsContinuous }

/-- A commutative ring equipped with a designated subring `A⁺`. -/
class PlusSubring (A : Type*) [CommRing A] where
  /-- The subring of integral elements `A⁺`. -/
  toSubring : Subring A

/-- The designated subring `A⁺`. -/
def ringPlus (A : Type*) [CommRing A] [PlusSubring A] : Subring A :=
  PlusSubring.toSubring

@[inherit_doc ringPlus] scoped postfix:max "⁺" => ringPlus

/-- `B` is a **ring of integral elements** of `A`: open, integrally closed, and contained in
`A°` (Wedhorn Definition 7.14). -/
class IsRingOfIntegralElements {A : Type*} [CommRing A] [TopologicalSpace A]
    (B : Subring A) : Prop where
  /-- `B` is open in `A`. -/
  isOpen : IsOpen (B : Set A)
  /-- `B` is integrally closed in `A`. -/
  isIntegrallyClosed : ∀ a : A, IsIntegral (↥B) a → a ∈ B
  /-- `B ⊆ A°`. -/
  subset_powerBounded : (B : Set A) ⊆ powerBoundedSubring A

variable [TopologicalSpace A]

/-- The **adic spectrum** `Spa(A, A⁺)` (Wedhorn Definition 7.23). -/
def Spa (A : Type*) [CommRing A] [TopologicalSpace A] (Aplus : Subring A) : Set (Spv A) :=
  { v ∈ Cont A | ∀ f ∈ Aplus, v.vle f 1 }

variable [PlusSubring A]

/-- The **rational subset** `R(T/s) ⊆ Spa(A, A⁺)` (Wedhorn Definition 7.29). -/
def rationalOpen (T : Finset A) (s : A) : Set (Spv A) :=
  { v ∈ Spa A A⁺ | (∀ t ∈ T, v.vle t s) ∧ ¬ v.vle s 0 }

end ValuationSpectrum

end AdicSpectrum

namespace PairOfDefinition

variable {A : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]

theorem pow_isOpen (P : PairOfDefinition A) (n : ℕ) : IsOpen ((P.I ^ n : Ideal P.A₀) : Set P.A₀) :=
  (isAdic_iff.mp P.isAdic).1 n

theorem pow_image_isOpen (P : PairOfDefinition A) (n : ℕ) :
    IsOpen (Subtype.val '' ((P.I ^ n : Ideal P.A₀) : Set P.A₀) : Set A) :=
  P.isOpen.isOpenMap_subtype_val _ (P.pow_isOpen n)

theorem hasBasis_nhds_zero (P : PairOfDefinition A) : (𝓝 (0 : A)).HasBasis (fun _ : ℕ ↦ True)
    (fun n ↦ Subtype.val '' ((P.I ^ n : Ideal P.A₀) : Set P.A₀)) :=
  Filter.HasBasis.mk fun U ↦ by
    constructor
    · intro hU
      have hU' : Subtype.val ⁻¹' U ∈ 𝓝 (0 : ↥P.A₀) :=
        continuous_subtype_val.continuousAt.preimage_mem_nhds (by simpa using hU)
      obtain ⟨n, -, hn⟩ := P.isAdic.hasBasis_nhds_zero.mem_iff.mp hU'
      exact ⟨n, trivial, (Set.image_mono hn).trans (Set.image_preimage_subset _ _)⟩
    · rintro ⟨n, -, hn⟩
      exact mem_nhds_iff.mpr
        ⟨_, hn, P.pow_image_isOpen n, Set.mem_image_of_mem _ (P.I ^ n).zero_mem⟩

end PairOfDefinition

/-! ## 5. The localisation topology on `Aₛ` (Wedhorn §8.1) -/

namespace ValuationSpectrum

open scoped ValuationSpectrum

variable {A : Type*} [CommRing A] [TopologicalSpace A]

/-- The fraction `t/s` in `Localization.Away s`. -/
noncomputable def divByS (t s : A) : Localization.Away s :=
  IsLocalization.mk' (Localization.Away s) t (⟨s, ⟨1, pow_one s⟩⟩ : Submonoid.powers s)

/-- The ring of definition `D = A₀[t₁/s, …, tₙ/s]` of `Aₛ` (Wedhorn §8.1). -/
noncomputable def locSubring (P : PairOfDefinition A) (T : Finset A) (s : A) :
    Subring (Localization.Away s) :=
  Subring.closure ((algebraMap A (Localization.Away s)) '' (P.A₀ : Set A) ∪
    Set.range (fun t : T ↦ divByS (t : A) s))

theorem algebraMap_A₀_subset_locSubring (P : PairOfDefinition A) (T : Finset A) (s : A) :
    (algebraMap A (Localization.Away s)) '' (P.A₀ : Set A) ⊆
      (locSubring P T s : Set (Localization.Away s)) :=
  Set.subset_union_left.trans Subring.subset_closure

/-- Wedhorn §8.1's openness condition on `(P, T, s)`: high powers of the ideal of definition
divide into `D`. It is what makes `locNhd` a neighbourhood basis for a ring topology on `Aₛ`. -/
def LocOpen (P : PairOfDefinition A) (T : Finset A) (s : A) : Prop :=
  ∃ N : ℕ, ∀ b : P.A₀, b ∈ P.I ^ N → divByS (↑b : A) s ∈ locSubring P T s

/-- `A₀ →+* D`, induced by `algebraMap` with codomain restricted to `D`. -/
noncomputable def algebraMapD (P : PairOfDefinition A) (T : Finset A) (s : A) :
    P.A₀ →+* (locSubring P T s) :=
  ((algebraMap A (Localization.Away s)).comp P.A₀.subtype).codRestrict (locSubring P T s)
    (fun a ↦ algebraMap_A₀_subset_locSubring P T s ⟨a, a.property, rfl⟩)

/-- The ideal of definition `J = I · D` of `D`. -/
noncomputable def locIdeal (P : PairOfDefinition A) (T : Finset A) (s : A) :
    Ideal (locSubring P T s) :=
  Ideal.map (algebraMapD P T s) P.I

/-- The `n`-th neighbourhood of `0` in `Aₛ`: the image of `Jⁿ`. -/
noncomputable def locNhd (P : PairOfDefinition A) (T : Finset A) (s : A) (n : ℕ) :
    AddSubgroup (Localization.Away s) :=
  ((locIdeal P T s) ^ n).toAddSubgroup.map (locSubring P T s).subtype.toAddMonoidHom

theorem locNhd_antitone (P : PairOfDefinition A) (T : Finset A) (s : A) :
    Antitone (locNhd P T s) :=
  fun _ _ h ↦ AddSubgroup.map_mono (Submodule.toAddSubgroup_mono (Ideal.pow_le_pow_right h))

theorem locNhd_mul (P : PairOfDefinition A) (T : Finset A) (s : A) (i : ℕ) :
    ∃ j, (locNhd P T s j : Set (Localization.Away s)) *
      (locNhd P T s j : Set (Localization.Away s)) ⊆
        (locNhd P T s i : Set (Localization.Away s)) := by
  refine ⟨i, ?_⟩
  rintro _ ⟨_, ⟨d₁, hd₁, rfl⟩, _, ⟨d₂, hd₂, rfl⟩, rfl⟩
  exact ⟨d₁ * d₂, Ideal.pow_le_pow_right (Nat.le_add_left i i)
    (pow_add (locIdeal P T s) i i ▸ Ideal.mul_mem_mul hd₁ hd₂), MulMemClass.coe_mul ..⟩

theorem locNhd_invS_mem (P : PairOfDefinition A) (T : Finset A) (s : A)
    (N : ℕ) (hN : ∀ b : P.A₀, b ∈ P.I ^ N → divByS (↑b : A) s ∈ locSubring P T s)
    {d : locSubring P T s} (hd : d ∈ locIdeal P T s ^ N) :
    divByS 1 s * ↑d ∈ locSubring P T s := by
  rw [locIdeal, ← Ideal.map_pow, ← Ideal.span_eq (P.I ^ N), Ideal.map_span] at hd
  refine Submodule.span_induction (p := fun d _ ↦ divByS 1 s * ↑d ∈ locSubring P T s)
    ?_ ?_ ?_ ?_ hd
  · rintro d ⟨b, hb, rfl⟩
    change divByS 1 s * algebraMap A _ ↑b ∈ _
    rw [show divByS 1 s * algebraMap A (Localization.Away s) ↑b = divByS (↑b) s from by
      unfold divByS
      rw [← IsLocalization.mk'_one (M := Submonoid.powers s) (S := Localization.Away s)
        (↑b : A), ← IsLocalization.mk'_mul, one_mul, mul_one]]
    exact hN b hb
  · simp [(locSubring P T s).zero_mem]
  · intro d1 d2 _ _ h1 h2
    simp only [AddMemClass.coe_add, mul_add]
    exact (locSubring P T s).add_mem h1 h2
  · intro r d1 _ h1
    rw [show (↑(r • d1) : Localization.Away s) = ↑r * ↑d1 from MulMemClass.coe_mul ..,
        mul_left_comm]
    exact (locSubring P T s).mul_mem r.property h1

theorem locNhd_invS_step (P : PairOfDefinition A) (T : Finset A) (s : A)
    (N : ℕ) (hN : ∀ b : P.A₀, b ∈ P.I ^ N → divByS (↑b : A) s ∈ locSubring P T s)
    (n : ℕ) (y : Localization.Away s)
    (hy : y ∈ locNhd P T s (n + N)) : divByS 1 s * y ∈ locNhd P T s n := by
  obtain ⟨d, hd, rfl⟩ := hy
  change divByS 1 s * ↑d ∈ locNhd P T s n
  rw [Nat.add_comm, pow_add] at hd
  refine Submodule.mul_induction_on hd ?_ ?_
  · intro a ha b hb
    change divByS 1 s * (↑a * ↑b) ∈ locNhd P T s n
    rw [← mul_assoc]
    exact ⟨⟨divByS 1 s * ↑a, locNhd_invS_mem P T s N hN ha⟩ * b, Ideal.mul_mem_left _ _ hb,
      MulMemClass.coe_mul ..⟩
  · intro y1 y2 h1 h2
    simp only [AddMemClass.coe_add, mul_add]
    exact (locNhd P T s n).add_mem h1 h2

variable [IsTopologicalRing A]

theorem locNhd_algMap_step (P : PairOfDefinition A) (T : Finset A) (s : A) (i : ℕ) (a : A) :
    ∃ j, ∀ y ∈ locNhd P T s j,
      algebraMap A (Localization.Away s) a * y ∈ locNhd P T s i := by
  obtain ⟨m₀, -, hm₀⟩ := P.hasBasis_nhds_zero.mem_iff.mp
    (continuous_const_mul a |>.continuousAt.preimage_mem_nhds
      (by rw [mul_zero]; exact P.hasBasis_nhds_zero.mem_of_mem trivial (i := i)))
  refine ⟨m₀, ?_⟩
  rintro y ⟨d, hd, rfl⟩
  change algebraMap A (Localization.Away s) a * ↑d ∈ locNhd P T s i
  rw [locIdeal, ← Ideal.map_pow, ← Ideal.span_eq (P.I ^ m₀), Ideal.map_span] at hd
  refine Submodule.span_induction (p := fun d _ ↦
    algebraMap A (Localization.Away s) a * ↑d ∈ locNhd P T s i) ?_ ?_ ?_ ?_ hd
  · rintro d ⟨b, hb, rfl⟩
    obtain ⟨c, hc, hval⟩ := hm₀ ⟨b, hb, rfl⟩
    change algebraMap A _ a * algebraMap A _ ↑b ∈ _
    rw [← map_mul, show a * (↑b : A) = ↑c from hval.symm]
    exact ⟨algebraMapD P T s c,
      by rw [locIdeal, ← Ideal.map_pow]; exact Ideal.mem_map_of_mem _ hc, rfl⟩
  · simp [(locNhd P T s i).zero_mem]
  · intro d1 d2 _ _ h1 h2
    simp only [AddMemClass.coe_add, mul_add]
    exact (locNhd P T s i).add_mem h1 h2
  · intro r d1 _ h1
    rw [show (↑(r • d1) : Localization.Away s) = ↑r * ↑d1 from MulMemClass.coe_mul ..,
        mul_left_comm]
    obtain ⟨e, he, he_eq⟩ := h1
    exact ⟨r * e, Ideal.mul_mem_left _ r he,
      congrArg ((↑r : Localization.Away s) * ·) he_eq⟩

theorem locNhd_leftMul (P : PairOfDefinition A) (T : Finset A) (s : A) (hopen : LocOpen P T s)
    (x : Localization.Away s) (i : ℕ) : ∃ j, (locNhd P T s j : Set (Localization.Away s)) ⊆
      (x * ·) ⁻¹' (locNhd P T s i : Set (Localization.Away s)) := by
  obtain ⟨N, hN⟩ := hopen
  induction x using Localization.induction_on with
  | H p =>
    obtain ⟨a, ⟨_, k, rfl⟩⟩ := p
    induction k generalizing a with
    | zero =>
      simp only [pow_zero]
      obtain ⟨j, hj⟩ := locNhd_algMap_step P T s i a
      exact ⟨j, fun _ hy ↦ hj _ hy⟩
    | succ k ih =>
      have hk1 : s ^ (k + 1) ∈ Submonoid.powers s := ⟨k + 1, rfl⟩
      have hk : s ^ k ∈ Submonoid.powers s := ⟨k, rfl⟩
      have hdecomp : Localization.mk a ⟨s ^ (k + 1), hk1⟩ =
          Localization.mk a ⟨s ^ k, hk⟩ * divByS 1 s := by
        rw [divByS, ← Localization.mk_eq_mk', Localization.mk_mul, mul_one]
        congr 1; exact Subtype.ext (pow_succ s k)
      obtain ⟨j₁, hj₁⟩ := ih a
      refine ⟨j₁ + N, fun y hy ↦ ?_⟩
      simp only [Set.mem_preimage]
      rw [hdecomp, mul_assoc]
      exact hj₁ (locNhd_invS_step P T s N hN j₁ _ hy)

set_option linter.defProp false in
/-- The `RingSubgroupsBasis` giving the localisation topology on `Aₛ`. -/
noncomputable def locBasis (P : PairOfDefinition A) (T : Finset A) (s : A)
    (hopen : LocOpen P T s) : RingSubgroupsBasis (locNhd P T s) :=
  .of_comm _ (fun i j ↦ ⟨max i j, le_inf (locNhd_antitone P T s (le_max_left i j))
    (locNhd_antitone P T s (le_max_right i j))⟩) (locNhd_mul P T s) (locNhd_leftMul P T s hopen)

/-- The localisation topology on `Aₛ`, with `{image Jⁿ}` a basis of neighbourhoods of `0`. -/
@[reducible] noncomputable def locTopology (P : PairOfDefinition A) (T : Finset A) (s : A)
    (hopen : LocOpen P T s) : TopologicalSpace (Localization.Away s) :=
  (locBasis P T s hopen).topology

/-! ## 6. Rational localisation data and the structure presheaf (Wedhorn §8.1) -/

variable [IsTopologicalRing A]

/-- A **rational localisation datum**: a pair of definition, a finite set `T`, an element
`s`, and the openness condition making the localisation topology on `Aₛ` well behaved
(Wedhorn §8.1). -/
structure RationalLocData (A : Type*) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] where
  /-- A pair of definition for `A`. -/
  P : PairOfDefinition A
  /-- The finite set `T ⊆ A`. -/
  T : Finset A
  /-- The element `s ∈ A`. -/
  s : A
  /-- High powers of `I` divide into the ring of definition `D`. -/
  hopen : LocOpen P T s

/-- Wedhorn Definition 7.29's openness condition: `D` presents a rational subset exactly
when the ideal generated by `T` is open. -/
def RationalLocData.IsRational (D : RationalLocData A) : Prop :=
  IsOpen ((Ideal.span (D.T : Set A) : Ideal A) : Set A)

namespace RationalLocData

/-- The localisation topology on `Aₛ` determined by the datum. -/
@[reducible] noncomputable def topology (D : RationalLocData A) :
    TopologicalSpace (Localization.Away D.s) :=
  locTopology D.P D.T D.s D.hopen

@[reducible] noncomputable def isTopologicalRing (D : RationalLocData A) :
    @IsTopologicalRing (Localization.Away D.s) D.topology _ :=
  (locBasis D.P D.T D.s D.hopen).toRingFilterBasis.isTopologicalRing

@[reducible] noncomputable def isTopologicalAddGroup (D : RationalLocData A) :
    @IsTopologicalAddGroup (Localization.Away D.s) D.topology _ :=
  @IsTopologicalRing.to_topologicalAddGroup _ _ D.topology D.isTopologicalRing

@[reducible] noncomputable def uniformSpace (D : RationalLocData A) :
    UniformSpace (Localization.Away D.s) :=
  @IsTopologicalAddGroup.rightUniformSpace _ _ D.topology D.isTopologicalAddGroup

@[reducible] noncomputable def isUniformAddGroup (D : RationalLocData A) :
    @IsUniformAddGroup (Localization.Away D.s) D.uniformSpace _ :=
  @isUniformAddGroup_of_addCommGroup _ _ D.topology D.isTopologicalAddGroup

end RationalLocData

/-- The **presheaf value** `𝒪_X(R(T/s)) = A⟨T/s⟩`: the completion of `Aₛ` for the
localisation topology (Wedhorn §8.1, equation 8.1.1). -/
noncomputable def presheafValue (D : RationalLocData A) : Type _ :=
  @UniformSpace.Completion (Localization.Away D.s) D.uniformSpace

noncomputable instance presheafValue.instCommRing (D : RationalLocData A) : CommRing (presheafValue D) :=
  @UniformSpace.Completion.commRing _ _ D.uniformSpace D.isUniformAddGroup D.isTopologicalRing

noncomputable instance presheafValue.instUniformSpace (D : RationalLocData A) : UniformSpace (presheafValue D) :=
  @UniformSpace.Completion.uniformSpace (Localization.Away D.s) D.uniformSpace

noncomputable instance presheafValue.instTopologicalSpace (D : RationalLocData A) :
    TopologicalSpace (presheafValue D) :=
  @UniformSpace.toTopologicalSpace _ (@UniformSpace.Completion.uniformSpace
    (Localization.Away D.s) D.uniformSpace)

noncomputable instance presheafValue.instIsTopologicalRing (D : RationalLocData A) :
    IsTopologicalRing (presheafValue D) :=
  @UniformSpace.Completion.topologicalRing _ _ D.uniformSpace
    D.isTopologicalRing D.isUniformAddGroup

instance presheafValue.instCompleteSpace (D : RationalLocData A) : CompleteSpace (presheafValue D) :=
  @UniformSpace.Completion.completeSpace _ D.uniformSpace

instance presheafValue.instT0Space (D : RationalLocData A) : T0Space (presheafValue D) :=
  @UniformSpace.Completion.t0Space _ D.uniformSpace

/-- The completion map `Aₛ →+* A⟨T/s⟩`, with dense image. -/
noncomputable def RationalLocData.coeRingHom (D : RationalLocData A) :
    Localization.Away D.s →+* presheafValue D :=
  @UniformSpace.Completion.coeRingHom _ _ D.uniformSpace D.isTopologicalRing D.isUniformAddGroup

/-- The canonical map `ρ : A →+* A⟨T/s⟩`. -/
noncomputable def RationalLocData.canonicalMap (D : RationalLocData A) :
    A →+* presheafValue D :=
  D.coeRingHom.comp (algebraMap A (Localization.Away D.s))

/-- **Stable uniformity** (Wedhorn Definition 7.37): every rational localisation `A⟨T/s⟩` of the
Huber ring `A` is uniform. -/
class IsStablyUniform (A : Type*) [CommRing A] [TopologicalSpace A] [IsHuberRing A] : Prop where
  /-- The completed rational localisation is uniform for every datum that actually presents a
  rational subset.

  The `D.IsRational` hypothesis is Wedhorn 7.37's, and is essential. `RationalLocData` is raw
  data and carries no guarantee that `T` generates an open ideal; `IsRational` is the separate
  predicate saying it does — the same one `RationalIndex` carries. Without it this class would
  be *stronger* than stable uniformity, and so its negation *weaker* than the standard failure,
  which is the only way the statements below use it. -/
  presheafValue_isUniform : ∀ D : RationalLocData A, D.IsRational →
      IsBounded (powerBoundedSubring (presheafValue D))

/-! ## 7. The adic spectrum as a space, and its rational opens (Wedhorn Theorem 7.35) -/

open CategoryTheory TopologicalSpace Opposite

section Spectrum

variable {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [PlusSubring A]

/-- The adic spectrum `Spa(A, A⁺)` as an object of `TopCat`. -/
def SpaTop (A : Type u) [CommRing A] [TopologicalSpace A] [PlusSubring A] : TopCat :=
  TopCat.of ↥(Spa A A⁺)

/-- A rational subset, as a subset of `Spa(A, A⁺)`. -/
def spaOpen (D : RationalLocData A) : Set ↥(SpaTop A) :=
  Subtype.val ⁻¹' rationalOpen D.T D.s

/-- The index of the projective limit at an open `V`: the *valid* rational data
(Wedhorn Definition 7.29) whose rational subset is contained in `V`. -/
structure RationalIndex (V : Opens ↥(SpaTop A)) where
  /-- The underlying rational localisation datum. -/
  D : RationalLocData A
  /-- The datum presents a rational subset. -/
  isRational : D.IsRational
  /-- Its rational subset is contained in `V`. -/
  subset : spaOpen D ⊆ (V : Set ↥(SpaTop A))

/-- Reindexing along `W ≤ V`. -/
def RationalIndex.mono {V W : Opens ↥(SpaTop A)} (h : W ≤ V) (i : RationalIndex W) :
    RationalIndex V :=
  ⟨i.D, i.isRational, i.subset.trans h⟩

end Spectrum

/-! ## 8. The structure presheaf and sheafiness (Wedhorn §8.1, Definition 8.26) -/

section Sheafy

-- `TopCommRingCat.{u}` forces the carrier into universe `u`.
variable {A : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [PlusSubring A]

/-- A **family of restriction maps** for the structure presheaf (Wedhorn Proposition 8.2):
for every containment of rational subsets `R(T'/s') ⊆ R(T/s)`, a continuous ring map
`A⟨T/s⟩ → A⟨T'/s'⟩` compatible with the canonical maps from `A`.

The family is carried as data rather than constructed. Proposition 8.2 builds one, and
`res_compat` pins it uniquely: a ring map out of `Aₛ` is determined by its restriction to `A`,
the image of `Aₛ` is dense in `A⟨T/s⟩`, and the target is Hausdorff. Keeping the family
abstract keeps the localisation-lift theory behind Proposition 8.2 (Wedhorn 7.41, 7.52) out
of this file without changing what is stated: `Solution.lean` proves that every such family is
the canonical one. -/
structure RestrictionFamily (A : Type u) [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A] [PlusSubring A] where
  /-- The restriction map `A⟨T/s⟩ → A⟨T'/s'⟩` for `R(T'/s') ⊆ R(T/s)`. -/
  res : ∀ (D D' : RationalLocData A),
    rationalOpen D'.T D'.s ⊆ rationalOpen D.T D.s → presheafValue D →+* presheafValue D'
  /-- It is continuous. -/
  res_continuous : ∀ D D' h, Continuous (res D D' h)
  /-- It is compatible with the canonical maps from `A`. -/
  res_compat : ∀ D D' h, (res D D' h).comp D.canonicalMap = D'.canonicalMap

variable (R : RestrictionFamily A)

/-- Wedhorn's `𝒪_X(V) = lim_{R(T/s) ⊆ V} A⟨T/s⟩` (§8.1): families of elements of the completed
rational localisations, indexed by the rational subsets inside `V`, compatible under
restriction. -/
def limitSections (V : Opens ↥(SpaTop A)) : Subring (∀ i : RationalIndex V, presheafValue i.D) where
  carrier := {x | ∀ (i j : RationalIndex V)
    (h : rationalOpen j.D.T j.D.s ⊆ rationalOpen i.D.T i.D.s), R.res i.D j.D h (x i) = x j}
  one_mem' := fun i j h => by simp only [Pi.one_apply, map_one]
  mul_mem' := fun hx hy i j h => by simp only [Pi.mul_apply, map_mul, hx i j h, hy i j h]
  zero_mem' := fun i j h => by simp only [Pi.zero_apply, map_zero]
  add_mem' := fun hx hy i j h => by simp only [Pi.add_apply, map_add, hx i j h, hy i j h]
  neg_mem' := fun hx i j h => by simp only [Pi.neg_apply, map_neg, hx i j h]

/-- Restriction along `W ≤ V`: forget the indices outside `W`. -/
noncomputable def limitRestrict {V W : Opens ↥(SpaTop A)} (h : W ≤ V) :
    ↥(limitSections R V) →+* ↥(limitSections R W) where
  toFun x := ⟨fun i => x.1 (i.mono h), fun i j hij => x.2 (i.mono h) (j.mono h) hij⟩
  map_one' := rfl
  map_mul' _ _ := rfl
  map_zero' := rfl
  map_add' _ _ := rfl

theorem limitRestrict_continuous {V W : Opens ↥(SpaTop A)} (h : W ≤ V) :
    Continuous (limitRestrict R h) :=
  Continuous.subtype_mk
    (continuous_pi fun i => (continuous_apply (i.mono h)).comp continuous_subtype_val) _

/-- **The structure presheaf** `𝒪_X` of `(A, A⁺)` (Wedhorn §8.1), built from the restriction
family `R`, as a presheaf of topological commutative rings in Mathlib's sense. -/
noncomputable def structurePresheaf : TopCat.Presheaf TopCommRingCat.{u} (SpaTop A) where
  obj V := TopCommRingCat.of ↥(limitSections R V.unop)
  map {V W} i := ⟨limitRestrict R (leOfHom i.unop), limitRestrict_continuous R _⟩
  map_id V := Subtype.ext (RingHom.ext fun x => Subtype.ext (funext fun i => rfl))
  map_comp i j := Subtype.ext (RingHom.ext fun x => Subtype.ext (funext fun i => rfl))

/-- **Sheafiness** (Wedhorn Definition 8.26): the structure presheaf of `(A, A⁺)` is a sheaf of
topological rings — `TopCat.Presheaf.IsSheaf`, Mathlib's sheaf condition, for the presheaf
`structurePresheaf R` valued in Mathlib's `TopCommRingCat`.

Stated as: a family of restriction maps exists, and for every such family the resulting
structure presheaf is a sheaf. Since the family is unique (see `RestrictionFamily`), this is
one presheaf, and the existence conjunct rules out a vacuous universal statement. -/
def IsSheafy (A : Type u) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [PlusSubring A] : Prop :=
  Nonempty (RestrictionFamily A) ∧
    ∀ R : RestrictionFamily A, TopCat.Presheaf.IsSheaf (structurePresheaf R)

/-- **Sheafiness of a complete ring** (Wedhorn Definition 8.26): `(A, A⁺)` is sheafy for *every*
ring of integral elements `A⁺ ⊆ A`. -/
def IsSheafyComplete (A : Type u) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] :
    Prop :=
  ∀ B : Subring A, IsRingOfIntegralElements B → letI : PlusSubring A := ⟨B⟩; IsSheafy A

end Sheafy

end ValuationSpectrum

/-! ## 9. Tate algebras over a nonarchimedean normed ring

`R⟨G⟩`, the completion of the polynomial ring `R[G]` for the **Gauss norm** (the largest norm of
a coefficient). For `G = ℤ × ℕ` this is `R⟨W, W⁻¹, Q⟩`, the restricted series in `W^{±1}, Q`;
for `G = Fin n →₀ ℕ` it is the Tate algebra `R⟨X₁, …, Xₙ⟩`. -/

section Gauss

open scoped NNReal

variable {R : Type u} [NormedCommRing R] [IsUltrametricDist R] {G : Type} [AddCommMonoid G]

/-- The Gauss norm of a polynomial: the largest norm of a coefficient. -/
noncomputable def gauss (x : AddMonoidAlgebra R G) : ℝ≥0 :=
  x.coeff.support.sup fun m => ‖x.coeff m‖₊

theorem nnnorm_coeff_le_gauss (x : AddMonoidAlgebra R G) (m : G) : ‖x.coeff m‖₊ ≤ gauss x := by
  by_cases h : m ∈ x.coeff.support
  · exact Finset.le_sup (f := fun m => ‖x.coeff m‖₊) h
  · rw [Finsupp.notMem_support_iff.mp h, nnnorm_zero]; exact zero_le

theorem gauss_le_iff {x : AddMonoidAlgebra R G} {C : ℝ≥0} :
    gauss x ≤ C ↔ ∀ m, ‖x.coeff m‖₊ ≤ C :=
  ⟨fun h m => (nnnorm_coeff_le_gauss x m).trans h, fun h => Finset.sup_le fun m _ => h m⟩

theorem gauss_eq_zero_iff {x : AddMonoidAlgebra R G} : gauss x = 0 ↔ x = 0 := by
  refine ⟨fun h => AddMonoidAlgebra.coeff_injective (Finsupp.ext fun m => ?_), ?_⟩
  · simpa using gauss_le_iff.mp h.le m
  · rintro rfl; simp [gauss]

theorem gauss_add_le (x y : AddMonoidAlgebra R G) : gauss (x + y) ≤ max (gauss x) (gauss y) :=
  gauss_le_iff.mpr fun m => by
    rw [AddMonoidAlgebra.coeff_add, Finsupp.add_apply]
    exact (IsUltrametricDist.nnnorm_add_le_max _ _).trans
      (max_le_max (nnnorm_coeff_le_gauss x m) (nnnorm_coeff_le_gauss y m))

theorem gauss_neg (x : AddMonoidAlgebra R G) : gauss (-x) = gauss x := by
  simp [gauss, AddMonoidAlgebra.coeff_neg]

theorem gauss_mul_le (x y : AddMonoidAlgebra R G) : gauss (x * y) ≤ gauss x * gauss y := by
  classical
  refine gauss_le_iff.mpr fun m => ?_
  rw [AddMonoidAlgebra.coeff_mul, ← NNReal.coe_le_coe, coe_nnnorm, NNReal.coe_mul]
  simp only [Finsupp.sum]
  refine IsUltrametricDist.norm_sum_le_of_forall_le_of_nonneg (by positivity) fun m₁ _ => ?_
  refine IsUltrametricDist.norm_sum_le_of_forall_le_of_nonneg (by positivity) fun m₂ _ => ?_
  split_ifs
  · calc ‖x.coeff m₁ * y.coeff m₂‖ ≤ ‖x.coeff m₁‖ * ‖y.coeff m₂‖ := norm_mul_le _ _
      _ ≤ gauss x * gauss y :=
        mul_le_mul (NNReal.coe_le_coe.mpr (nnnorm_coeff_le_gauss x m₁))
          (NNReal.coe_le_coe.mpr (nnnorm_coeff_le_gauss y m₂)) (norm_nonneg _) (by positivity)
  · simp only [norm_zero]; positivity

noncomputable def gaussGroupNorm : AddGroupNorm (AddMonoidAlgebra R G) where
  toFun x := gauss x
  map_zero' := by simp [gauss]
  add_le' x y := by
    have h : ((gauss (x + y) : ℝ≥0) : ℝ) ≤ max ((gauss x : ℝ≥0) : ℝ) ((gauss y : ℝ≥0) : ℝ) := by
      exact_mod_cast gauss_add_le x y
    exact h.trans (max_le_add_of_nonneg (by positivity) (by positivity))
  neg' x := by simp [gauss_neg]
  eq_zero_of_map_eq_zero' x hx := gauss_eq_zero_iff.mp (by exact_mod_cast hx)

noncomputable instance gaussNormedAddCommGroup : NormedAddCommGroup (AddMonoidAlgebra R G) :=
  gaussGroupNorm.toNormedAddCommGroup

theorem nnnorm_eq_gauss (x : AddMonoidAlgebra R G) : ‖x‖₊ = gauss x := rfl

/-- `R[G]` with the Gauss norm is a normed ring. -/
noncomputable instance gaussNormedCommRing : NormedCommRing (AddMonoidAlgebra R G) :=
  { (inferInstance : NormedAddCommGroup (AddMonoidAlgebra R G)),
    (inferInstance : CommRing (AddMonoidAlgebra R G)) with
    norm_mul_le := fun x y => by exact_mod_cast gauss_mul_le x y }

instance gaussIsUltrametricDist : IsUltrametricDist (AddMonoidAlgebra R G) :=
  IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm fun x y => by exact_mod_cast gauss_add_le x y

-- Pinned at high priority so the statements elaborate identically in every environment (see
-- the module docstring); it is the same instance. All instances here are named explicitly,
-- since auto-generated instance names can depend on the module name.
instance (priority := 1100) gaussIsTopologicalRing : IsTopologicalRing (AddMonoidAlgebra R G) :=
  inferInstance

instance gaussNormOneClass [NormOneClass R] : NormOneClass (AddMonoidAlgebra R G) where
  norm_one := by
    classical
    rw [← coe_nnnorm, nnnorm_eq_gauss, NNReal.coe_eq_one]
    refine le_antisymm (gauss_le_iff.mpr fun m => ?_) ?_
    · rw [AddMonoidAlgebra.one_def, AddMonoidAlgebra.coeff_single, Finsupp.single_apply]
      split_ifs <;> simp
    · simpa using nnnorm_coeff_le_gauss (1 : AddMonoidAlgebra R G) 0

/-- Scaling by a field constant scales the Gauss norm exactly. -/
theorem gauss_smul {K : Type u} [NormedField K] [IsUltrametricDist K] (c : K)
    (x : AddMonoidAlgebra K G) : gauss (c • x) = ‖c‖₊ * gauss x := by
  have key : ∀ (c : K) (x : AddMonoidAlgebra K G), gauss (c • x) ≤ ‖c‖₊ * gauss x :=
    fun c x => gauss_le_iff.mpr fun m => by
      rw [AddMonoidAlgebra.coeff_smul, Finsupp.smul_apply, smul_eq_mul, nnnorm_mul]
      gcongr
      exact nnnorm_coeff_le_gauss x m
  refine le_antisymm (key c x) ?_
  by_cases hc : c = 0
  · simp [hc]
  calc ‖c‖₊ * gauss x = ‖c‖₊ * gauss (c⁻¹ • (c • x)) := by rw [inv_smul_smul₀ hc]
    _ ≤ ‖c‖₊ * (‖c⁻¹‖₊ * gauss (c • x)) := by gcongr; exact key _ _
    _ = gauss (c • x) := by
      rw [← mul_assoc, ← nnnorm_mul, mul_inv_cancel₀ hc, nnnorm_one, one_mul]

/-- **The Tate algebra** `R⟨G⟩`: the completion of `R[G]` for the Gauss norm. -/
abbrev TateAlgebra (R : Type u) [NormedCommRing R] [IsUltrametricDist R] (G : Type)
    [AddCommMonoid G] : Type u :=
  UniformSpace.Completion (AddMonoidAlgebra R G)

instance tateAlgebraIsUltrametricDist : IsUltrametricDist (TateAlgebra R G) := by
  refine IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm fun x y => ?_
  induction x, y using UniformSpace.Completion.induction_on₂ with
  | hp => exact isClosed_le (by fun_prop) (by fun_prop)
  | ih a b =>
    rw [← UniformSpace.Completion.coe_add, UniformSpace.Completion.norm_coe,
      UniformSpace.Completion.norm_coe, UniformSpace.Completion.norm_coe]
    exact IsUltrametricDist.norm_add_le_max a b

instance tateAlgebraNormOneClass [NormOneClass R] : NormOneClass (TateAlgebra R G) where
  norm_one := by
    rw [← UniformSpace.Completion.coe_one, UniformSpace.Completion.norm_coe, norm_one]

/-- Multiplication by a field constant scales the norm on `K⟨G⟩` exactly. -/
theorem norm_algebraMap_mul {K : Type u} [NormedField K] [IsUltrametricDist K] (c : K)
    (x : TateAlgebra K G) :
    ‖(algebraMap K (AddMonoidAlgebra K G) c : TateAlgebra K G) * x‖ = ‖c‖ * ‖x‖ := by
  induction x using UniformSpace.Completion.induction_on with
  | hp => exact isClosed_eq (by fun_prop) (by fun_prop)
  | ih p =>
    rw [← UniformSpace.Completion.coe_mul, UniformSpace.Completion.norm_coe,
      UniformSpace.Completion.norm_coe, ← Algebra.smul_def, ← coe_nnnorm, ← coe_nnnorm,
      ← coe_nnnorm, nnnorm_eq_gauss, nnnorm_eq_gauss, gauss_smul, NNReal.coe_mul]

end Gauss

/-! ## 10. The unit ball of a nonarchimedean normed ring, as a pair of definition -/

section UnitBall

variable (E : Type*) [NormedCommRing E] [IsUltrametricDist E] [NormOneClass E]

/-- The closed unit ball of a nonarchimedean normed ring, as a subring. -/
noncomputable def unitBall : Subring E where
  carrier := {x | ‖x‖ ≤ 1}
  zero_mem' := by simp
  one_mem' := norm_one.le
  add_mem' ha hb := (IsUltrametricDist.norm_add_le_max _ _).trans (max_le ha hb)
  neg_mem' ha := by simpa only [Set.mem_setOf_eq, norm_neg] using ha
  mul_mem' ha hb := (norm_mul_le _ _).trans (mul_le_one₀ ha (norm_nonneg _) hb)

theorem isOpen_unitBall : IsOpen (unitBall E : Set E) := by
  show IsOpen {x : E | ‖x‖ ≤ 1}
  simpa only [Metric.closedBall, dist_zero_right] using
    IsUltrametricDist.isOpen_closedBall (0 : E) one_ne_zero

variable {E}

omit [IsUltrametricDist E] [NormOneClass E] in
theorem norm_pow_mul_of_scale {t : E} (hscale : ∀ x : E, ‖t * x‖ = ‖t‖ * ‖x‖) (n : ℕ) (x : E) :
    ‖t ^ n * x‖ = ‖t‖ ^ n * ‖x‖ := by
  induction n with
  | zero => simp
  | succ m ih => rw [pow_succ, pow_succ, mul_comm (t ^ m) t, mul_assoc, hscale, ih]; ring

theorem mem_span_unitBall_pow_iff {t : E} (htu : IsUnit t) (ht1 : ‖t‖ ≤ 1) (ht0 : 0 < ‖t‖)
    (hscale : ∀ x : E, ‖t * x‖ = ‖t‖ * ‖x‖) (x : unitBall E) (n : ℕ) :
    x ∈ (Ideal.span {(⟨t, ht1⟩ : unitBall E)}) ^ n ↔ ‖(x : E)‖ ≤ ‖t‖ ^ n := by
  rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton']
  constructor
  · rintro ⟨c, hc⟩
    have hcoe : (c : E) * t ^ n = (x : E) := congrArg Subtype.val hc
    rw [← hcoe, mul_comm, norm_pow_mul_of_scale hscale]
    exact (mul_le_mul_of_nonneg_left c.2 (by positivity)).trans_eq (mul_one _)
  · intro hx
    set y : E := ((htu.unit⁻¹ : Eˣ) : E) ^ n * (x : E) with hy
    have hyx : t ^ n * y = (x : E) := by
      rw [hy, ← mul_assoc, ← mul_pow, htu.mul_val_inv, one_pow, one_mul]
    have hnorm : ‖(x : E)‖ = ‖t‖ ^ n * ‖y‖ := by rw [← hyx, norm_pow_mul_of_scale hscale]
    have hymem : ‖y‖ ≤ 1 := by
      have hpos : (0 : ℝ) < ‖t‖ ^ n := by positivity
      rw [hnorm] at hx
      exact le_of_mul_le_mul_left (by linarith) hpos
    exact ⟨⟨y, hymem⟩, Subtype.ext (show y * t ^ n = (x : E) by rw [mul_comm]; exact hyx)⟩

/-- The unit-ball pair of definition `(E⁰, (t))` attached to a norm-scaling unit `t` of norm `< 1`
(a pseudouniformizer): the unit ball is open, and its `t`-adic topology is the subspace topology
because `tⁿ E⁰` is the closed ball of radius `‖t‖ⁿ`. -/
noncomputable def unitBallPod (t : E) (htu : IsUnit t) (ht1 : ‖t‖ < 1) (ht0 : 0 < ‖t‖)
    (hscale : ∀ x : E, ‖t * x‖ = ‖t‖ * ‖x‖) : PairOfDefinition E where
  A₀ := unitBall E
  I := Ideal.span {⟨t, ht1.le⟩}
  isOpen := isOpen_unitBall E
  fg := ⟨{⟨t, ht1.le⟩}, by simp⟩
  isAdic := by
    rw [isAdic_iff]
    refine ⟨fun n => ?_, fun s hs => ?_⟩
    · rw [isOpen_iff_mem_nhds]
      intro x hx
      rw [SetLike.mem_coe, mem_span_unitBall_pow_iff htu ht1.le ht0 hscale] at hx
      rw [mem_nhds_subtype]
      refine ⟨Metric.ball (x : E) (‖t‖ ^ n), Metric.ball_mem_nhds _ (by positivity), ?_⟩
      intro y hy
      rw [Set.mem_preimage, Metric.mem_ball, dist_eq_norm] at hy
      rw [SetLike.mem_coe, mem_span_unitBall_pow_iff htu ht1.le ht0 hscale]
      calc ‖(y : E)‖ = ‖((y : E) - (x : E)) + (x : E)‖ := by ring_nf
        _ ≤ max ‖(y : E) - (x : E)‖ ‖(x : E)‖ := IsUltrametricDist.norm_add_le_max _ _
        _ ≤ ‖t‖ ^ n := max_le hy.le hx
    · rw [mem_nhds_subtype] at hs
      obtain ⟨U, hU, hUs⟩ := hs
      obtain ⟨ε, hε, hball⟩ := Metric.mem_nhds_iff.mp (by simpa using hU)
      obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hε ht1
      refine ⟨n, fun x hx => hUs ?_⟩
      rw [SetLike.mem_coe, mem_span_unitBall_pow_iff htu ht1.le ht0 hscale] at hx
      exact hball (by rw [Metric.mem_ball, dist_zero_right]; exact lt_of_le_of_lt hx hn)

/-- A nonarchimedean normed ring with a norm-scaling unit of norm `< 1` is a Tate ring. -/
theorem isTateRing_of_scale (t : E) (htu : IsUnit t) (ht1 : ‖t‖ < 1) (ht0 : 0 < ‖t‖)
    (hscale : ∀ x : E, ‖t * x‖ = ‖t‖ * ‖x‖) : IsTateRing E := by
  have _ : IsHuberRing E := ⟨⟨unitBallPod t htu ht1 ht0 hscale⟩⟩
  refine ⟨⟨htu.unit, ?_⟩⟩
  show Filter.Tendsto (fun n : ℕ => ((htu.unit : Eˣ) : E) ^ n) Filter.atTop (𝓝 0)
  simp only [IsUnit.unit_spec]
  rw [tendsto_zero_iff_norm_tendsto_zero]
  have hnorm : ∀ n : ℕ, ‖t ^ n‖ = ‖t‖ ^ n := fun n => by
    simpa using norm_pow_mul_of_scale (E := E) hscale n 1
  simp only [hnorm]
  exact tendsto_pow_atTop_nhds_zero_of_lt_one ht0.le ht1

end UnitBall

/-! ## 11. The finite-jet pinching algebra `𝓐` ([FJP] §1) -/

section FiniteJet

variable (K : Type u) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]

/-- The Laurent polynomials in `W` and polynomials in `Q` whose `Q⁰`- and `Q¹`-coefficients have
nonnegative `W`-support: `f₀(W) + Q f₁(W) + Q² h` with `f₀, f₁ ∈ K[W]`, `h ∈ K[W, W⁻¹, Q]`
([FJP] (1.7)). The index `(a, q)` is the monomial `W^a Q^q`. -/
def jetPolys : Subring (AddMonoidAlgebra K (ℤ × ℕ)) where
  carrier := {p | ∀ (a : ℤ) (q : ℕ), q ≤ 1 → a < 0 → p.coeff (a, q) = 0}
  zero_mem' _ _ _ _ := rfl
  one_mem' a q _ ha := by
    rw [AddMonoidAlgebra.one_def, AddMonoidAlgebra.coeff_single, Finsupp.single_apply, if_neg]
    rintro ⟨⟩; exact ha.ne rfl
  add_mem' hp hq a q h1 h2 := by
    rw [AddMonoidAlgebra.coeff_add, Finsupp.add_apply, hp a q h1 h2, hq a q h1 h2, add_zero]
  neg_mem' hp a q h1 h2 := by rw [AddMonoidAlgebra.coeff_neg, Finsupp.neg_apply, hp a q h1 h2, neg_zero]
  mul_mem' {p q} hp hq a k hk ha := by
    rw [AddMonoidAlgebra.coeff_mul]
    simp only [Finsupp.sum]
    refine Finset.sum_eq_zero fun x _ => Finset.sum_eq_zero fun y _ => ?_
    split_ifs with h
    · obtain ⟨h1, h2⟩ := Prod.mk.inj h
      rcases lt_or_ge x.1 0 with hx | hx
      · rw [hp x.1 x.2 (by omega) hx, zero_mul]
      · rw [hq y.1 y.2 (by omega) (by omega), mul_zero]
    · rfl

/-- **`𝓐`, the finite-jet pinching algebra** ([FJP] Definition 1.2): the closure in `K⟨W, W⁻¹, Q⟩`
of `jetPolys` — the restricted series `f₀(W) + Q f₁(W) + Q² h` with `f₀, f₁ ∈ K⟨W⟩` and
`h ∈ K⟨W, W⁻¹, Q⟩` ([FJP] (1.7)), with the Gauss norm. -/
noncomputable def jetSubring : Subring (TateAlgebra K (ℤ × ℕ)) :=
  ((jetPolys K).map UniformSpace.Completion.coeRingHom).topologicalClosure

/-- The finite-jet pinching algebra `𝓐`, as a type. -/
abbrev JetA : Type u := ↥(jetSubring K)

/-- The constants `K → 𝓐`. -/
noncomputable def C : K →+* JetA K :=
  (UniformSpace.Completion.coeRingHom.comp (algebraMap K (AddMonoidAlgebra K (ℤ × ℕ)))).codRestrict
    (jetSubring K) fun c => Subring.le_topologicalClosure _ ⟨algebraMap K _ c, fun a q _ ha => by
      rw [AddMonoidAlgebra.coe_algebraMap, Function.comp_apply, AddMonoidAlgebra.coeff_single,
        Finsupp.single_apply, if_neg]
      rintro ⟨⟩; exact ha.ne rfl, rfl⟩

omit [CompleteSpace K] in
theorem norm_C_mul (c : K) (x : JetA K) : ‖C K c * x‖ = ‖c‖ * ‖x‖ :=
  norm_algebraMap_mul c (x : TateAlgebra K (ℤ × ℕ))

/-- `𝓐` is a Tate ring: the constants of norm `< 1` are norm-scaling topologically nilpotent
units, and the unit ball `𝓐₀` with the ideal they generate is a pair of definition. -/
instance jetAIsTateRing : IsTateRing (JetA K) := by
  obtain ⟨c, hc⟩ := NontriviallyNormedField.non_trivial (α := K)
  have hc0 : c ≠ 0 := by rintro rfl; norm_num at hc
  have hC : ‖C K c⁻¹‖ = ‖c⁻¹‖ := by simpa using norm_C_mul K c⁻¹ 1
  refine isTateRing_of_scale (C K c⁻¹) ⟨⟨C K c⁻¹, C K c, ?_, ?_⟩, rfl⟩ ?_ ?_
    fun x => by rw [norm_C_mul, hC]
  · rw [← map_mul, inv_mul_cancel₀ hc0, map_one]
  · rw [← map_mul, mul_inv_cancel₀ hc0, map_one]
  · rw [hC, norm_inv]; exact inv_lt_one_of_one_lt₀ hc
  · rw [hC, norm_inv]; exact inv_pos.mpr (zero_lt_one.trans hc)

/-- The Tate algebra `𝓐⟨X₁, …, Xₙ⟩` over `𝓐`: the completion of `𝓐[X₁, …, Xₙ]` for the Gauss
norm. -/
abbrev JetAExt (n : ℕ) : Type u := TateAlgebra (JetA K) (Fin n →₀ ℕ)

end FiniteJet

end Palomar