Rigid analytic geometry

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

TheoremThe maximum modulus principle#

On a nonzero affinoid algebra the supremum seminorm is attained at a classical point: for every f : A there is a maximal ideal x of A with |f(x)| = |f|sup.

TauCeti.IsAffinoidAlgebra.exists_pointNorm_eq_supSeminorm.{u_1, u_2} {K : Type u_1}
  [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [CommRing A]
  [Algebra K A] [Nontrivial A] (hA : TauCeti.IsAffinoidAlgebra K A) (f : A) :
  ∃ x, TauCeti.pointNorm K x f = TauCeti.supSeminorm K f
Lean

Formalized in Tau Ceti as TauCeti.IsAffinoidAlgebra.exists_pointNorm_eq_supSeminorm.

Sources
LeanTauCeti.IsAffinoidAlgebra.exists_pointNorm_eq_supSeminorm
Uses 9
Statement usesTauCeti.supSeminorm
Proof usesAffinoid Noether normalisation · Kedlaya's Hilbert basis theorem for restricted power series · The supremum seminorm is the spectral value of the minimal polynomial · TauCeti.IsAffinoidAlgebra.continuous_algHom · TauCeti.MvPowerSeries.supSeminorm_eq_norm · The Weierstrass division estimate (Bosch–Güntzer–Remmert §5.2.1, Theorem 2) · The Weierstrass division identity · Weierstrass preparation

TheoremTauCeti.MvPowerSeries.supSeminorm_eq_norm#

On a Tate algebra the supremum seminorm is the Gauss norm: |f|sup = ‖f‖.

TauCeti.MvPowerSeries.supSeminorm_eq_norm.{u_1} {K : Type u_1} [NontriviallyNormedField K]
  [IsUltrametricDist K] [CompleteSpace K] {n : ℕ}
  (f : ↥(MvPowerSeries.IsRestricted.subring fun x => 1)) : TauCeti.supSeminorm K f = ‖f‖
Lean

Formalized in Tau Ceti as TauCeti.MvPowerSeries.supSeminorm_eq_norm.

Sources
LeanTauCeti.MvPowerSeries.supSeminorm_eq_norm
Uses 5 · Used by 1
Statement usesTauCeti.supSeminorm
Proof usesKedlaya's Hilbert basis theorem for restricted power series · TauCeti.IsAffinoidAlgebra.continuous_algHom · The Weierstrass division estimate (Bosch–Güntzer–Remmert §5.2.1, Theorem 2) · The Weierstrass division identity
Used byThe maximum modulus principle

TheoremAffinoid Noether normalisation#

Every nonzero affinoid algebra over a complete ultrametric field is finite over an injectively embedded finite-variable Tate algebra. Finiteness uses the algebra structure induced by the displayed map.

TauCeti.IsAffinoidAlgebra.exists_finite_injective.{u, u_1} {K : Type u} [NormedField K]
  [IsUltrametricDist K] [CompleteSpace K] {A : Type u_1} [CommRing A] [Algebra K A] [Nontrivial A]
  (hA : TauCeti.IsAffinoidAlgebra K A) : ∃ n g, Function.Injective ⇑g ∧ g.Finite
Lean

Formalized in Tau Ceti as TauCeti.IsAffinoidAlgebra.exists_finite_injective.

Sources
LeanTauCeti.IsAffinoidAlgebra.exists_finite_injective
Uses 2 · Used by 2
Proof usesThe Weierstrass division estimate (Bosch–Güntzer–Remmert §5.2.1, Theorem 2) · The Weierstrass division identity
Used byHeights of maximal ideals of affinoid domains · The maximum modulus principle

TheoremTauCeti.IsAffinoidAlgebra.continuous_algHom#

Every homomorphism from a noetherian ultrametric Banach algebra to a completely normed affinoid algebra is continuous. The affinoid presentation is purely algebraic.

TauCeti.IsAffinoidAlgebra.continuous_algHom.{u_1, u_2, u_3} {K : Type u_1}
  [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2}
  [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A]
  (hA : TauCeti.IsAffinoidAlgebra K A) {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B]
  [IsUltrametricDist B] [CompleteSpace B] [IsNoetherianRing B] (f : B →ₐ[K] A) : Continuous ⇑f
Lean

Formalized in Tau Ceti as TauCeti.IsAffinoidAlgebra.continuous_algHom.

Sources
LeanTauCeti.IsAffinoidAlgebra.continuous_algHom
Uses 4 · Used by 8
Proof usesKedlaya's Hilbert basis theorem for restricted power series · The open mapping theorem over a Tate ring · The Weierstrass division estimate (Bosch–Güntzer–Remmert §5.2.1, Theorem 2) · The Weierstrass division identity
Used byAffinoid algebras are the algebras topologically of finite type · The adic spectrum of a classical affinoid algebra is an affinoid adic space · Equivalence of complete affinoid norms · Restricted series over an affinoid algebra form an affinoid algebra · TauCeti.MvPowerSeries.supSeminorm_eq_norm · The maximum modulus principle · The supremum seminorm is the spectral value of the minimal polynomial · The universal property of restricted series over an affinoid algebra

DefinitionEquivalence of complete affinoid norms#

An algebra isomorphism between completely normed affinoid algebras is a homeomorphism, whatever complete ultrametric algebra norms they carry. Applied to two such norms on one algebra, this says that they define the same topology.

TauCeti.IsAffinoidAlgebra.toContinuousAlgEquiv.{u_1, u_2, u_3} {K : Type u_1}
  [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2}
  [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {B : Type u_3}
  [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B]
  (hB : TauCeti.IsAffinoidAlgebra K B) (e : A ≃ₐ[K] B) : A ≃A[K] B
Lean

Formalized in Tau Ceti as TauCeti.IsAffinoidAlgebra.toContinuousAlgEquiv.

Sources
LeanTauCeti.IsAffinoidAlgebra.toContinuousAlgEquiv
Uses 2
Proof usesKedlaya's Hilbert basis theorem for restricted power series · TauCeti.IsAffinoidAlgebra.continuous_algHom

TheoremHeights of maximal ideals of affinoid domains#

Every maximal ideal of an affinoid domain A has height dim A.

TauCeti.IsAffinoidAlgebra.height_eq_ringKrullDim_of_isDomain.{u_1, u_2} {K : Type u_1}
  [NormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [CommRing A] [Algebra K A]
  [IsDomain A] (hA : TauCeti.IsAffinoidAlgebra K A) (m : Ideal A) [m.IsMaximal] :
  ↑m.height = ringKrullDim A
Lean

Formalized in Tau Ceti as TauCeti.IsAffinoidAlgebra.height_eq_ringKrullDim_of_isDomain.

Sources
LeanTauCeti.IsAffinoidAlgebra.height_eq_ringKrullDim_of_isDomain
Uses 5
Proof usesAffinoid Noether normalisation · Kedlaya's Hilbert basis theorem for restricted power series · The Weierstrass division estimate (Bosch–Güntzer–Remmert §5.2.1, Theorem 2) · The Weierstrass division identity · Weierstrass preparation

TheoremThe supremum seminorm is the spectral value of the minimal polynomial#

Let B be an affinoid algebra which is integral and torsion-free over an integrally closed domain A. For f : B with minimal polynomial X ^ d + ∑_{i < d} aᵢ X ^ i over A, |f|sup = max_{i < d} |aᵢ|sup ^ (1 / (d - i)).

TauCeti.IsAffinoidAlgebra.supSeminorm_eq_iSup_minpoly_coeff_rpow.{u_1, u_2, u_3} {K : Type u_1}
  [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2} [CommRing A]
  [Algebra K A] {B : Type u_3} [CommRing B] [Algebra K B] [Algebra A B] [IsScalarTower K A B]
  (hB : TauCeti.IsAffinoidAlgebra K B) [IsDomain A] [IsIntegrallyClosed A]
  [Module.IsTorsionFree A B] [Algebra.IsIntegral A B] (f : B) :
  TauCeti.supSeminorm K f =
    ⨆ i, TauCeti.supSeminorm K ((minpoly A f).coeff ↑i) ^ (1 / (↑(minpoly A f).natDegree - ↑↑i))
Lean

Formalized in Tau Ceti as TauCeti.IsAffinoidAlgebra.supSeminorm_eq_iSup_minpoly_coeff_rpow.

Sources
LeanTauCeti.IsAffinoidAlgebra.supSeminorm_eq_iSup_minpoly_coeff_rpow
Uses 5 · Used by 1
Statement usesTauCeti.supSeminorm
Proof usesKedlaya's Hilbert basis theorem for restricted power series · TauCeti.IsAffinoidAlgebra.continuous_algHom · The Weierstrass division estimate (Bosch–Güntzer–Remmert §5.2.1, Theorem 2) · The Weierstrass division identity
Used byThe maximum modulus principle

DefinitionTauCeti.supSeminorm#

The supremum seminorm |f|sup of f : A: the supremum of its absolute values |f(x)| at the maximal ideals x of A. It is zero on the zero algebra, which has no maximal ideals.

TauCeti.supSeminorm.{u_1, u_2} (K : Type u_1) [NontriviallyNormedField K] {A : Type u_2}
  [CommRing A] [Algebra K A] (f : A) : ℝ
Lean

Formalized in Tau Ceti as TauCeti.supSeminorm.

Sources
LeanTauCeti.supSeminorm
Used by 3
Used byTauCeti.MvPowerSeries.supSeminorm_eq_norm · The maximum modulus principle · The supremum seminorm is the spectral value of the minimal polynomial

TheoremRestricted series over an affinoid algebra form an affinoid algebra#

For an affinoid algebra A with a complete ultrametric algebra norm, the Gauss-normed algebra A⟨X₁, …, Xₘ⟩ of unit-radius restricted series is affinoid: a Tate presentation K⟨Y₁, …, Yₙ⟩ → A induces a presentation K⟨X₁, …, Xₘ, Y₁, …, Yₙ⟩ → A⟨X₁, …, Xₘ⟩.

TauCeti.IsAffinoidAlgebra.isRestricted_subring.{u_1, u_2, u_3} {K : Type u_1}
  [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2}
  [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {τ : Type u_3}
  [Finite τ] (hA : TauCeti.IsAffinoidAlgebra K A) :
  TauCeti.IsAffinoidAlgebra K ↥(MvPowerSeries.IsRestricted.subring fun x => 1)
Lean

Formalized in Tau Ceti as TauCeti.IsAffinoidAlgebra.isRestricted_subring.

Sources
LeanTauCeti.IsAffinoidAlgebra.isRestricted_subring
Uses 2 · Used by 1
Proof usesKedlaya's Hilbert basis theorem for restricted power series · TauCeti.IsAffinoidAlgebra.continuous_algHom
Used byThe universal property of restricted series over an affinoid algebra

TheoremThe universal property of restricted series over an affinoid algebra#

Let A and B be affinoid algebras with complete ultrametric algebra norms. A K-algebra map φ : A → B and power-bounded b₁, …, bₖ ∈ B extend to exactly one K-algebra map A⟨X₁, …, Xₖ⟩ → B sending each Xᵢ to bᵢ, namely TauCeti.IsAffinoidAlgebra.restrictedLift. It is continuous, as is every algebra map between such algebras (TauCeti.IsAffinoidAlgebra.continuous_algHom).

TauCeti.IsAffinoidAlgebra.existsUnique_algHom_isRestricted_subring.{u_1, u_2, u_3} {K : Type u_1}
  [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {A : Type u_2}
  [NormedCommRing A] [NormedAlgebra K A] [IsUltrametricDist A] [CompleteSpace A] {k : ℕ}
  (hA : TauCeti.IsAffinoidAlgebra K A) {B : Type u_3} [NormedCommRing B] [NormedAlgebra K B]
  [IsUltrametricDist B] [CompleteSpace B] (hB : TauCeti.IsAffinoidAlgebra K B) (φ : A →ₐ[K] B)
  {b : Fin k → B} (hb : ∀ (i : Fin k), TauCeti.Huber.IsPowerBounded (b i)) :
  ∃! ψ,
    (∀ (a : A), ψ ((algebraMap A ↥(MvPowerSeries.IsRestricted.subring fun x => 1)) a) = φ a) ∧
      ∀ (i : Fin k), ψ ⟨MvPowerSeries.X i, ⋯⟩ = b i
Lean

Formalized in Tau Ceti as TauCeti.IsAffinoidAlgebra.existsUnique_algHom_isRestricted_subring.

Sources
LeanTauCeti.IsAffinoidAlgebra.existsUnique_algHom_isRestricted_subring
Uses 3
Proof usesKedlaya's Hilbert basis theorem for restricted power series · Restricted series over an affinoid algebra form an affinoid algebra · TauCeti.IsAffinoidAlgebra.continuous_algHom

StructureTauCeti.GTopology#

Admissible covers on a family of subsets closed under finite intersections and containing the whole space. The family is represented by an order embedding ι, preserving intersections and the largest open. Covering families are sets, so repetitions and indexing choices carry no additional data.

TauCeti.GTopology.{u, v} {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B]
  (ι : B ↪o Set X) : Type v
Lean

Formalized in Tau Ceti as TauCeti.GTopology.

Sources
LeanTauCeti.GTopology
Used by 1
Used byTauCeti.GTopology.isSheaf_iff

TheoremTauCeti.GTopology.isSheaf_iff#

The site sheaf condition is precisely unique gluing of matching families on all admissible covers. Presieve.IsSheafFor is Mathlib's existence-and-uniqueness condition for amalgamations.

TauCeti.GTopology.isSheaf_iff.{u, v, w} {X : Type u} {B : Type v} [SemilatticeInf B] [OrderTop B]
  {ι : B ↪o Set X} (G : TauCeti.GTopology ι) (P : CategoryTheory.Functor Bᵒᵖ (Type w)) :
  CategoryTheory.Presieve.IsSheaf G.grothendieckTopology P ↔
    ∀ (U : B) (S : Set B),
      G.Covers U S → CategoryTheory.Presieve.IsSheafFor P (TauCeti.GTopology.coverPresieve U S)
Lean

Formalized in Tau Ceti as TauCeti.GTopology.isSheaf_iff.

Sources
LeanTauCeti.GTopology.isSheaf_iff
Uses 1
Statement usesTauCeti.GTopology

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.