Analytic adic geometry for diamonds

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

DefinitionMorphisms out of the Huber pair of a finite algebra#

Morphisms of Huber pairs (B, B⁺) → (D, D⁺) under (A, A⁺) are exactly the A-algebra maps B → D.

TauCeti.Huber.Pair.finiteAlgebra.homEquiv.{u_1, u_2, u_3} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] [IsTopologicalRing A] [TauCeti.Huber.IsHuberRing A]
  {S : TauCeti.Huber.Pair A} {B : Type u_2} [CommRing B] [Algebra A B] [Module.Finite A B]
  [TopologicalSpace B] [IsModuleTopology A B] [IsTopologicalRing B] [TauCeti.Huber.IsHuberRing B]
  {D : Type u_3} [CommRing D] [TopologicalSpace D] [IsTopologicalRing D]
  [TauCeti.Huber.IsHuberRing D] [Algebra A D] {V : TauCeti.Huber.Pair D} (χ : S.Hom V)
  (hχ : χ.toRingHom = algebraMap A D) :
  { ψ // ψ.comp (TauCeti.Huber.Pair.finiteAlgebra.algebraHom S B) = χ } ≃ (B →ₐ[A] D)
Lean

Formalized in Tau Ceti as TauCeti.Huber.Pair.finiteAlgebra.homEquiv.

Sources
LeanTauCeti.Huber.Pair.finiteAlgebra.homEquiv

TheoremA finite algebra over a Tate ring is a Tate ring#

If B is a commutative A-algebra, finite as an A-module and carrying its natural topology, then B is a Tate ring; the image of a pseudouniformiser of A is a pseudouniformiser of B.

TauCeti.Huber.IsTateRing.of_isModuleTopology.{u_1, u_2} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] {B : Type u_2} [CommRing B] [Algebra A B] [IsTopologicalRing A]
  [TopologicalSpace B] [IsModuleTopology A B] [Module.Finite A B] [TauCeti.Huber.IsTateRing A] :
  TauCeti.Huber.IsTateRing B
Lean

Formalized in Tau Ceti as TauCeti.Huber.IsTateRing.of_isModuleTopology.

Sources
LeanTauCeti.Huber.IsTateRing.of_isModuleTopology

TheoremTauCeti.isFiniteEtaleSplit_iff_exists_section#

A ring has no nonsplit finite étale covers if and only if every faithfully flat finite étale algebra over it admits a section. Faithful flatness is needed: over a nonzero ring the zero algebra is finite étale and totally split, but has no section.

TauCeti.isFiniteEtaleSplit_iff_exists_section.{u} {R : Type u} [CommRing R] :
  TauCeti.IsFiniteEtaleSplit R ↔
    ∀ (T : Type u) [inst : CommRing T] [inst_1 : Algebra R T] [Algebra.Etale R T]
      [Module.Finite R T] [Module.FaithfullyFlat R T], Nonempty (T →ₐ[R] R)
Lean

Formalized in Tau Ceti as TauCeti.isFiniteEtaleSplit_iff_exists_section.

Sources
LeanTauCeti.isFiniteEtaleSplit_iff_exists_section
Uses 1 · Used by 1
Statement usesTauCeti.IsFiniteEtaleSplit
Used byTauCeti.IsFiniteEtaleSplit.of_henselianLocalRing

TheoremTauCeti.IsFiniteEtaleSplit.of_henselianLocalRing#

A Henselian local ring with separably closed residue field, that is, a strictly Henselian local ring, has no nonsplit finite étale covers: a faithfully flat finite étale algebra has a point over the separably closed residue field, which lifts to a section.

TauCeti.IsFiniteEtaleSplit.of_henselianLocalRing.{u} (R : Type u) [CommRing R]
  [HenselianLocalRing R] [IsSepClosed (IsLocalRing.ResidueField R)] : TauCeti.IsFiniteEtaleSplit R
Lean

Formalized in Tau Ceti as TauCeti.IsFiniteEtaleSplit.of_henselianLocalRing.

Sources
LeanTauCeti.IsFiniteEtaleSplit.of_henselianLocalRing
Uses 2
Statement usesTauCeti.IsFiniteEtaleSplit
Proof usesTauCeti.isFiniteEtaleSplit_iff_exists_section

TheoremHenselian pairs are stable under directed colimits#

If every (G i, I i) is a Henselian pair and the transition maps carry I i into I j, then the directed colimit Ring.DirectLimit G f is Henselian along the colimit ideal ⨆ i, (I i).map (of G f i).

Ring.DirectLimit.henselianRing.{u_1, u_2} {ι : Type u_1} [Preorder ι] {G : ι → Type u_2}
  [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i →+* G j} {I : (i : ι) → Ideal (G i)}
  [Nonempty ι] [IsDirectedOrder ι] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)]
  [∀ (i : ι), HenselianRing (G i) (I i)]
  (hI : ∀ (i j : ι) (hij : i ≤ j), I i ≤ Ideal.comap (f i j hij) (I j)) :
  HenselianRing (Ring.DirectLimit G fun x1 x2 x3 => ⇑(f x1 x2 x3))
    (⨆ i, Ideal.map (Ring.DirectLimit.of G (fun x1 x2 x3 => ⇑(f x1 x2 x3)) i) (I i))
Lean

Formalized in Tau Ceti as Ring.DirectLimit.henselianRing.

Sources
LeanRing.DirectLimit.henselianRing

ClassTauCeti.IsFiniteEtaleSplit#

A ring R has no nonsplit finite étale covers if every finite étale R-algebra is totally split. This is the conclusion of Scholze's Lemma 15.3 for the perfectoid tower A_∞.

TauCeti.IsFiniteEtaleSplit.{u} (R : Type u) [CommRing R] : Prop
Lean

Formalized in Tau Ceti as TauCeti.IsFiniteEtaleSplit.

Sources
LeanTauCeti.IsFiniteEtaleSplit
Used by 2
Used byTauCeti.isFiniteEtaleSplit_iff_exists_section · TauCeti.IsFiniteEtaleSplit.of_henselianLocalRing

DefinitionTauCeti.Huber.IsPseudoCoherentOver#

M is m-pseudocoherent over R: it has a resolution ⋯ → F₁ → F₀ → M → 0 by finite free modules Fᵢ = Fin (n i) → R, with augmentation ε and differentials d i : Fᵢ₊₁ → Fᵢ, which is exact at M, F₀, …, F_{m-1}. Thus 0-pseudocoherent means finitely generated, 1-pseudocoherent means finitely presented, and for m = ⊤ the whole resolution is exact (Kedlaya–Liu II, Definition 1.1.1; Stacks, Tag 064T, with the index negated).

TauCeti.Huber.IsPseudoCoherentOver.{u, v} (R : Type u) (M : Type v) [Ring R] [AddCommGroup M]
  [_root_.Module R M] (m : ℕ∞) : Prop
Lean

Formalized in Tau Ceti as TauCeti.Huber.IsPseudoCoherentOver.

Sources
LeanTauCeti.Huber.IsPseudoCoherentOver

DefinitionAnalytic points of a pre-adic space (Wedhorn, Proposition and Definition 8.36)#

the points x having an open neighbourhood U such that 𝒪_X(U) contains a pseudouniformiser, that is, a topologically nilpotent unit. On Spa(A, A⁺) these are the points whose support is not open (TauCeti.ValuationSpectrum.analyticPoints_presentationLimitPreAdicSpace).

TauCeti.PreAdicSpace.analyticPoints.{u} (X : TauCeti.PreAdicSpace) : Set ↑X.toTopCat
Lean

Formalized in Tau Ceti as TauCeti.PreAdicSpace.analyticPoints.

Sources
LeanTauCeti.PreAdicSpace.analyticPoints

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.