Foundations of adic spaces, part IV — étale sites, families and dagger geometry

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremUnits of the Monsky–Washnitzer algebra#

Over a complete ultrametric normed field, an overconvergent series is a unit of W iff its constant coefficient is nonzero and strictly dominates the norm of every other coefficient.

TauCeti.Dagger.isUnit_washnitzerAlgebra_iff.{u_1, u_2} {σ : Type u_1} {K : Type u_2} [NormedField K]
  [IsUltrametricDist K] [CompleteSpace K] (f : ↥(TauCeti.Dagger.washnitzerAlgebra σ K)) :
  IsUnit f ↔
    MvPowerSeries.constantCoeff ↑f ≠ 0 ∧
      ∀ (t : σ →₀ ℕ), t ≠ 0 → ‖(MvPowerSeries.coeff t) ↑f‖ < ‖MvPowerSeries.constantCoeff ↑f‖

Lean

Formalized in Tau Ceti as TauCeti.Dagger.isUnit_washnitzerAlgebra_iff.

Sources

• Tau Ceti documentation: TauCeti.Dagger.isUnit_washnitzerAlgebra_iff
• Source of TauCeti.Dagger.isUnit_washnitzerAlgebra_iff in TauCeti/RingTheory/Dagger/WashnitzerAlgebra.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part IV — étale sites, families and dagger geometry

LeanTauCeti.Dagger.isUnit_washnitzerAlgebra_iff

Uses 3 · Used by 1

Statement usesTauCeti.Dagger.washnitzerAlgebra

Proof usesNeumann series criterion (MvPowerSeries.isNormMulUnit_of_norm_sub_C_lt) · TauCeti.Dagger.washnitzerAlgebra.toTate

Used byTauCeti.Dagger.washnitzerAlgebra.isUnit_toTate_iff

TheoremTauCeti.Dagger.washnitzerAlgebra.isUnit_toTate_iff#

An overconvergent series is a unit of the Tate algebra iff it is a unit of the Monsky–Washnitzer algebra: the inverse of an overconvergent series is overconvergent.

TauCeti.Dagger.washnitzerAlgebra.isUnit_toTate_iff.{u_1, u_2} {σ : Type u_1} {K : Type u_2}
  [NormedField K] [IsUltrametricDist K] [CompleteSpace K]
  (f : ↥(TauCeti.Dagger.washnitzerAlgebra σ K)) :
  IsUnit ((TauCeti.Dagger.washnitzerAlgebra.toTate σ K) f) ↔ IsUnit f

Lean

Formalized in Tau Ceti as TauCeti.Dagger.washnitzerAlgebra.isUnit_toTate_iff.

Sources

• Tau Ceti documentation: TauCeti.Dagger.washnitzerAlgebra.isUnit_toTate_iff
• Source of TauCeti.Dagger.washnitzerAlgebra.isUnit_toTate_iff in TauCeti/RingTheory/Dagger/WashnitzerAlgebra.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part IV — étale sites, families and dagger geometry

LeanTauCeti.Dagger.washnitzerAlgebra.isUnit_toTate_iff

Uses 3

Statement usesTauCeti.Dagger.washnitzerAlgebra · TauCeti.Dagger.washnitzerAlgebra.toTate

Proof usesUnits of the Monsky–Washnitzer algebra

TheoremPrimitives of overconvergent series are overconvergent#

Over an ultrametric normed field of characteristic zero, the termwise primitive with respect to Xᵢ of an overconvergent series is overconvergent. See MvPowerSeries.IsRestricted.primitive for the radius-by-radius version.

TauCeti.Dagger.primitive_mem_washnitzerAlgebra.{u_1, u_2} {σ : Type u_1} {K : Type u_2}
  [NormedField K] [IsUltrametricDist K] [CharZero K] {f : MvPowerSeries σ K}
  (hf : f ∈ TauCeti.Dagger.washnitzerAlgebra σ K) (i : σ) :
  (MvPowerSeries.primitive i) f ∈ TauCeti.Dagger.washnitzerAlgebra σ K

Lean

Formalized in Tau Ceti as TauCeti.Dagger.primitive_mem_washnitzerAlgebra.

Sources

• Tau Ceti documentation: TauCeti.Dagger.primitive_mem_washnitzerAlgebra
• Source of TauCeti.Dagger.primitive_mem_washnitzerAlgebra in TauCeti/RingTheory/Dagger/WashnitzerAlgebra.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part IV — étale sites, families and dagger geometry

LeanTauCeti.Dagger.primitive_mem_washnitzerAlgebra

Uses 1

Statement usesTauCeti.Dagger.washnitzerAlgebra

TheoremThe Gauss norm bound for primitives#

Over a normed field of characteristic zero, for polyradii 0 ≤ c' ≤ c with c'ᵢ < cᵢ, there is C ≥ 0 such that for every f with a Gauss norm at c, ∫ f dXᵢ has a Gauss norm at c' and gaussNorm c' (∫ f dXᵢ) ≤ C * gaussNorm c f.

MvPowerSeries.exists_gaussNorm_primitive_le.{u_1, u_2} {σ : Type u_1} {K : Type u_2} [NormedField K]
  [CharZero K] (c c' : σ → ℝ) (i : σ) (hc' : ∀ (j : σ), 0 ≤ c' j) (hle : ∀ (j : σ), c' j ≤ c j)
  (hlt : c' i < c i) :
  ∃ C,
    0 ≤ C ∧
      ∀ (f : MvPowerSeries σ K),
        MvPowerSeries.HasGaussNorm norm c f →
          MvPowerSeries.HasGaussNorm norm c' ((MvPowerSeries.primitive i) f) ∧
            MvPowerSeries.gaussNorm norm c' ((MvPowerSeries.primitive i) f) ≤
              C * MvPowerSeries.gaussNorm norm c f

Lean

Formalized in Tau Ceti as MvPowerSeries.exists_gaussNorm_primitive_le.

Sources

• Tau Ceti documentation: MvPowerSeries.exists_gaussNorm_primitive_le
• Source of MvPowerSeries.exists_gaussNorm_primitive_le in TauCeti/RingTheory/MvPowerSeries/Primitive/GaussNorm.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part IV — étale sites, families and dagger geometry

LeanMvPowerSeries.exists_gaussNorm_primitive_le

TheoremDistinguishing automorphisms of Monsky–Washnitzer algebras#

Over a complete nonarchimedean field K, every nonzero overconvergent series f in the variables Option σ, for finite σ, is carried by a triangular automorphism Y ↦ Y, Xᵢ ↦ Xᵢ + Y ^ α i of K⟨X, Y⟩† to a series which, as a restricted series in the variable Y = none over the Tate algebra in the variables σ, is distinguished of some degree s at radius 1 with a unit coefficient in degree s.

TauCeti.Dagger.washnitzerAlgebra.exists_triangularEquiv_isDistinguished_isUnit.{u_1, u_3}
  {σ : Type u_1} {K : Type u_3} [NormedField K] [IsUltrametricDist K] [CompleteSpace K] [Finite σ]
  (f : ↥(TauCeti.Dagger.washnitzerAlgebra (Option σ) K)) (hf : f ≠ 0) :
  ∃ α,
    ∃ (hα : ∀ (i : σ), α i ≠ 0),
      ∃ s,
        TauCeti.PowerSeries.IsDistinguished 1 s
            ↑(MvPowerSeries.restrictedOptionEquiv
                ((TauCeti.Dagger.washnitzerAlgebra.toTate (Option σ) K)
                  ((TauCeti.Dagger.washnitzerAlgebra.triangularEquiv α hα) f))) ∧
          IsUnit
            ((PowerSeries.coeff s)
              ↑(MvPowerSeries.restrictedOptionEquiv
                  ((TauCeti.Dagger.washnitzerAlgebra.toTate (Option σ) K)
                    ((TauCeti.Dagger.washnitzerAlgebra.triangularEquiv α hα) f))))

Lean

Formalized in Tau Ceti as TauCeti.Dagger.washnitzerAlgebra.exists_triangularEquiv_isDistinguished_isUnit.

Sources

• Tau Ceti documentation: TauCeti.Dagger.washnitzerAlgebra.exists_triangularEquiv_isDistinguished_isUnit
• Source of TauCeti.Dagger.washnitzerAlgebra.exists_triangularEquiv_isDistinguished_isUnit in TauCeti/RingTheory/Dagger/Distinguished.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part IV — étale sites, families and dagger geometry

LeanTauCeti.Dagger.washnitzerAlgebra.exists_triangularEquiv_isDistinguished_isUnit

Uses 3

Statement usesIsomorphisms of Monsky–Washnitzer algebras from inverse substitutions · TauCeti.Dagger.washnitzerAlgebra · TauCeti.Dagger.washnitzerAlgebra.toTate

TheoremRadius selection for distinguished overconvergent series#

Let g be an overconvergent series in the variables Option σ which, as a series in Y = X none over the Tate algebra in the variables σ, is distinguished of degree s at radius 1 with a unit coefficient g_s. Then for every ρ₀ > 1 there are radii 1 < ρ ≤ r ≤ ρ₀ such that g is restricted at r, and its coefficient slices gₘ, which are restricted at ρ, form a series G = ∑ₘ gₘ Yᵐ over the series restricted at ρ that is distinguished of degree s at radius r, with g_s a unit.

This is the radius selection behind Weierstrass division by g inside the Monsky–Washnitzer algebra. A single common radius ρ = r > 1 does not suffice in general.

TauCeti.Dagger.exists_isDistinguished_isUnit_of_isDistinguished_one.{u_1, u_3} {σ : Type u_1}
  {K : Type u_3} [NormedField K] [IsUltrametricDist K] [CompleteSpace K]
  {g : ↥(TauCeti.Dagger.washnitzerAlgebra (Option σ) K)} {s : ℕ}
  (hg :
    TauCeti.PowerSeries.IsDistinguished 1 s
      ↑(MvPowerSeries.restrictedOptionEquiv
          ((TauCeti.Dagger.washnitzerAlgebra.toTate (Option σ) K) g)))
  (hu :
    IsUnit
      ((PowerSeries.coeff s)
        ↑(MvPowerSeries.restrictedOptionEquiv
            ((TauCeti.Dagger.washnitzerAlgebra.toTate (Option σ) K) g))))
  {ρ₀ : ℝ} (hρ₀ : 1 < ρ₀) :
  ∃ ρ,
    ∃ (x : Fact (0 < ρ)),
      ∃ r,
        1 < ρ ∧
          ρ ≤ r ∧
            r ≤ ρ₀ ∧
              MvPowerSeries.IsRestricted (fun x => r) ↑g ∧
                ∃ G,
                  (∀ (m : ℕ),
                      ↑((PowerSeries.coeff m) G) =
                        (PowerSeries.coeff m) ((MvPowerSeries.optionEquivLeft σ K) ↑g)) ∧
                    TauCeti.PowerSeries.IsDistinguished r s G ∧ IsUnit ((PowerSeries.coeff s) G)

Lean

Formalized in Tau Ceti as TauCeti.Dagger.exists_isDistinguished_isUnit_of_isDistinguished_one.

Sources

• Tau Ceti documentation: TauCeti.Dagger.exists_isDistinguished_isUnit_of_isDistinguished_one
• Source of TauCeti.Dagger.exists_isDistinguished_isUnit_of_isDistinguished_one in TauCeti/RingTheory/Dagger/Distinguished.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part IV — étale sites, families and dagger geometry

LeanTauCeti.Dagger.exists_isDistinguished_isUnit_of_isDistinguished_one

Uses 3

Statement usesTauCeti.Dagger.washnitzerAlgebra · TauCeti.Dagger.washnitzerAlgebra.toTate

Proof usesNeumann series criterion (MvPowerSeries.isNormMulUnit_of_norm_sub_C_lt)

DefinitionTauCeti.Dagger.washnitzerAlgebra#

The Monsky–Washnitzer algebra R⟨X⟩† of overconvergent power series: the series restricted at some constant radius ρ > 1.

TauCeti.Dagger.washnitzerAlgebra.{u_1, u_2} (σ : Type u_1) (R : Type u_2) [NormedCommRing R]
  [IsUltrametricDist R] : Subalgebra R (MvPowerSeries σ R)

Lean

Formalized in Tau Ceti as TauCeti.Dagger.washnitzerAlgebra.

Sources

• Tau Ceti documentation: TauCeti.Dagger.washnitzerAlgebra
• Source of TauCeti.Dagger.washnitzerAlgebra in TauCeti/RingTheory/Dagger/WashnitzerAlgebra.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part IV — étale sites, families and dagger geometry

LeanTauCeti.Dagger.washnitzerAlgebra

Used by 8

Used byDistinguishing automorphisms of Monsky–Washnitzer algebras · Isomorphisms of Monsky–Washnitzer algebras from inverse substitutions · Primitives of overconvergent series are overconvergent · Radius selection for distinguished overconvergent series · TauCeti.Dagger.washnitzerAlgebra.isUnit_toTate_iff · TauCeti.Dagger.washnitzerAlgebra.toTate · Units of the Monsky–Washnitzer algebra · The Cauchy estimate at unit radius

DefinitionTauCeti.Dagger.washnitzerAlgebra.toTate#

The inclusion of the Monsky–Washnitzer algebra into the unit-radius Tate algebra R{X/1}, through which W carries the Gauss norm.

TauCeti.Dagger.washnitzerAlgebra.toTate.{u_1, u_2} (σ : Type u_1) (R : Type u_2) [NormedCommRing R]
  [IsUltrametricDist R] :
  ↥(TauCeti.Dagger.washnitzerAlgebra σ R) →ₐ[R] ↥(MvPowerSeries.IsRestricted.subring fun x => 1)

Lean

Formalized in Tau Ceti as TauCeti.Dagger.washnitzerAlgebra.toTate.

Sources

• Tau Ceti documentation: TauCeti.Dagger.washnitzerAlgebra.toTate
• Source of TauCeti.Dagger.washnitzerAlgebra.toTate in TauCeti/RingTheory/Dagger/WashnitzerAlgebra.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part IV — étale sites, families and dagger geometry

LeanTauCeti.Dagger.washnitzerAlgebra.toTate

Uses 1 · Used by 6

Statement usesTauCeti.Dagger.washnitzerAlgebra

Used byDistinguishing automorphisms of Monsky–Washnitzer algebras · Isomorphisms of Monsky–Washnitzer algebras from inverse substitutions · Radius selection for distinguished overconvergent series · TauCeti.Dagger.washnitzerAlgebra.isUnit_toTate_iff · Units of the Monsky–Washnitzer algebra · The Cauchy estimate at unit radius

DefinitionIsomorphisms of Monsky–Washnitzer algebras from inverse substitutions#

If two families of unit-ball polynomials without constant term are inverse to each other under substitution, the substitutions are mutually inverse R-algebra isomorphisms R⟨X⟩† ≃ R⟨Y⟩†.

TauCeti.Dagger.washnitzerAlgebra.substEquiv.{u_1, u_2, u_3} {σ : Type u_1} {τ : Type u_2}
  {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ]
  (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0)
  (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) [Finite τ] (b : τ → MvPolynomial σ R)
  (hb₀ : ∀ (t : τ), MvPolynomial.constantCoeff (b t) = 0)
  (hb₁ : ∀ (t : τ) (u : σ →₀ ℕ), ‖(b t).coeff u‖ ≤ 1)
  (hab : ∀ (s : σ), (MvPolynomial.aeval b) (a s) = MvPolynomial.X s)
  (hba : ∀ (t : τ), (MvPolynomial.aeval a) (b t) = MvPolynomial.X t) :
  ↥(TauCeti.Dagger.washnitzerAlgebra σ R) ≃ₐ[R] ↥(TauCeti.Dagger.washnitzerAlgebra τ R)

Lean

Formalized in Tau Ceti as TauCeti.Dagger.washnitzerAlgebra.substEquiv.

Sources

• Tau Ceti documentation: TauCeti.Dagger.washnitzerAlgebra.substEquiv
• Source of TauCeti.Dagger.washnitzerAlgebra.substEquiv in TauCeti/RingTheory/Dagger/Subst.lean
• Tau Ceti roadmap status: Foundations of adic spaces, part IV — étale sites, families and dagger geometry

LeanTauCeti.Dagger.washnitzerAlgebra.substEquiv

Uses 2 · Used by 1

Statement usesTauCeti.Dagger.washnitzerAlgebra

Proof usesTauCeti.Dagger.washnitzerAlgebra.toTate

Used byDistinguishing automorphisms of Monsky–Washnitzer algebras

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.