87.2 Formal schemes à la EGA to 87.10 Countably indexed affine…

Section87.2 Formal schemes à la EGA #

Section 87.2 of the Stacks Project, Tag 0AHY. 7 tags here are carried by 38 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AHY, the section

Tag 0AHY in the Stacks Project.

AlgebraicGeometry.isIso_spfGammaHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FormalSpectrumGlobalSectionsIso.lean, line 585. The attribute's comment: “Γ(Spf A, 𝒪_{Spf A}) = A for an admissible topological ring”.

Stacks 0AHY, the source's deferred verification Γ(D(f) ∩ Spf A, 𝒪_{Spf A}) = A_{\{f\}} in the case f = 1: for an admissible topological ring the canonical map A → Γ(Spf A, 𝒪_{Spf A}) is an isomorphism of topological rings.

The global sections of 𝒪_{Spf A} = lim 𝒪_λ are the limit of the discrete rings Γ(Spec (A/I_λ), 𝒪) = A/I_λ, and an admissible ring is precisely the limit of its quotients by its ideals of definition.

theorem isIso_spfGammaHom [IsLinearTopology A A] (hA : IsAdmissible A) :
    IsIso (spfGammaHom A)

AlgebraicGeometry.spfGammaIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FormalSpectrumGlobalSectionsIso.lean, line 594. The attribute's comment: “Γ(Spf A, 𝒪_{Spf A}) = A for an admissible topological ring”.

Stacks 0AHY. The identification A = Γ(Spf A, 𝒪_{Spf A}) of topological rings, for an admissible topological ring A.

noncomputable def spfGammaIso [IsLinearTopology A A] (hA : IsAdmissible A) :
    TopCommRingCat.of A ≅ (spfPresheaf A).obj (op ⊤)

Tag 0AHZ, an equation

Tag 0AHZ in the Stacks Project.

AlgebraicGeometry.injective_spfLTRSMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FormalSpectrumBijection.lean, line 396. The attribute's comment: “injectivity of the comparison map Hom_cont(A, B) → Mor_LTRS(Spf B, Spf A)”. References: EGA I (10.4.6), “Affine case X = Spf B”; SGA 3 VIIB (1.1), “partial”.

Stacks 0AHZ, injectivity of the comparison map. In the identification Mor_{LTRS}((Spf B, 𝒪_{Spf B}), (Spf A, 𝒪_{Spf A})) = Hom_cont(A, B) the map from continuous ring homomorphisms to morphisms of formal spectra is injective as soon as B is separated and linearly topologized: a morphism determines the map it induces on global sections, that map is the homomorphism read through the canonical maps into global sections, and the canonical map of B is injective.

theorem injective_spfLTRSMap [IsLinearTopology B B] [T2Space B] :
    Function.Injective (spfLTRSMap A B hA I₀ hB)

AlgebraicGeometry.surjective_spfLTRSMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FormalSpectrumSurjectivity.lean, line 382. The attribute's comment: “surjectivity of the comparison map Hom_cont(A, B) → Mor_LTRS(Spf B, Spf A)”. References: EGA I (10.2.2); EGA I (10.4.6), “Affine case X = Spf B”; SGA 3 VIIB (1.1), “partial”.

Morphisms of formal spectra come from continuous ring maps. Every morphism g : Spf B → Spf A of locally topologically ringed spaces between the formal spectra of admissible topological rings comes from a continuous ring homomorphism A → B, namely from AlgebraicGeometry.ltrsGlobalSectionsRingHom g, the map g induces on global sections read through the identifications Γ(Spf A, 𝒪_{Spf A}) = A and Γ(Spf B, 𝒪_{Spf B}) = B of Stacks 0AHY.

theorem surjective_spfLTRSMap : Function.Surjective (spfLTRSMap A B hA.1 I₀ hB.1)

AlgebraicGeometry.bijective_spfLTRSMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FormalSpectrumSurjectivity.lean, line 400. The attribute's comment: “the full bijection Hom_cont(A, B) = Mor_LTRS(Spf B, Spf A) for admissible A, B”. References: SGA 3 VIIB (1.1), “partial”.

Stacks 0AHZ. For admissible topological rings A and B the comparison map taking a continuous ring homomorphism A → B to the induced morphism Spf B → Spf A of locally topologically ringed spaces is a bijection: it is injective by AlgebraicGeometry.injective_spfLTRSMap, separatedness of B making the canonical map B → Γ(Spf B, 𝒪_{Spf B}) injective, and surjective by AlgebraicGeometry.surjective_spfLTRSMap.

theorem bijective_spfLTRSMap : Function.Bijective (spfLTRSMap A B hA.1 I₀ hB.1)

Tag 0AI0, an equation

Tag 0AI0 in the Stacks Project.

AlgebraicGeometry.schemeToFormalScheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/SchemeToFormalScheme.lean, line 273.

Stacks 0AI0. The functor Schemes ⟶ Formal Schemes: pseudo-discretisation, a scheme being a formal scheme by AlgebraicGeometry.isFormalScheme_schemeToLTRSObj.

noncomputable def schemeToFormalScheme : Scheme.{u} ⥤ FormalScheme.{u}

AlgebraicGeometry.full_schemeToFormalScheme, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/SchemeToFormalScheme.lean, line 295. The attribute's comment: “full faithfulness: fullness”.

Stacks 0AI0. The functor from schemes to formal schemes is full: a morphism of the pseudo-discretised spaces has an automatically continuous comparison map, so it is the image of the morphism of schemes with the same data.

instance full_schemeToFormalScheme : schemeToFormalScheme.{u}.Full

AlgebraicGeometry.faithful_schemeToFormalScheme, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/SchemeToFormalScheme.lean, line 304. The attribute's comment: “full faithfulness: faithfulness”.

Stacks 0AI0. The functor from schemes to formal schemes is faithful: a morphism of schemes is recovered from its pseudo-discretisation by forgetting the topologies.

instance faithful_schemeToFormalScheme : schemeToFormalScheme.{u}.Faithful

Tag 0AI1, a lemma

Tag 0AI1 in the Stacks Project.

AlgebraicGeometry.injective_formalSchemeFunctorOfPoints_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPoints.lean, line 587. The attribute's comment: “injectivity: a morphism of formal schemes is determined by the induced transformation of functors of points”.

Stacks 0AI1, injectivity. A morphism of formal schemes whose source satisfies the size condition is determined by the natural transformation it induces on functors of points on the schemes of size below κ.

The morphisms Spec (A/I_λ) → Spf A ≅ 𝔛|_𝔘 → 𝔛 attached to the affine formal charts of 𝔛 are jointly epimorphic, and the size condition is exactly what makes them morphisms out of objects of Sch_κ, hence points of 𝔛 seen by the functor of points. Their underlying maps cover 𝔛 because each Spec (A/I_λ) → Spf A is a homeomorphism; and they separate the sections of 𝒪_𝔛, because 𝒪_𝔛 is a sheaf and the sections of 𝒪_{Spf A} = lim 𝒪_λ are a limit.

theorem injective_formalSchemeFunctorOfPoints_map {κ : Cardinal.{u}} {X Y : FormalScheme.{u}}
    (hX : IsSizeBoundedFormalScheme κ X.obj) :
    Function.Injective fun f : X ⟶ Y => (formalSchemeFunctorOfPoints κ).map f

AlgebraicGeometry.bijective_formalSchemeFunctorOfPoints_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsFull.lean, line 652. The attribute's comment: “the bijection Mor(𝔛, 𝔜) = Mor(h_𝔛, h_𝔜) for a formal scheme 𝔛 whose size is bounded by the cutoff”.

Morphisms of formal schemes are transformations of functors of points. For a formal scheme 𝔛 whose size is not too large — the schemes Spec (A/I_λ) cut out of its affine formal charts being objects of Sch_κ — and any formal scheme 𝔜,

Mor_{Formal Schemes}(𝔛, 𝔜) = Mor_{PSh(Sch_κ)}(h_𝔛, h_𝔜).

theorem bijective_formalSchemeFunctorOfPoints_map {κ : Cardinal.{u}} {X Y : FormalScheme.{u}}
    (hX : IsSizeBoundedFormalScheme κ X.obj) :
    Function.Bijective fun f : X ⟶ Y => (formalSchemeFunctorOfPoints κ).map f

AlgebraicGeometry.exists_formalSchemePointsFunctor_map_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsFullSupplement.lean, line 62. The attribute's comment: “surjectivity on all schemes: every transformation of functors of points is induced by a morphism of formal schemes, with no size hypothesis”.

Every transformation h_𝔛 → h_𝔜 of functors of points on the category of all schemes is induced by a morphism of formal schemes 𝔛 → 𝔜, with no size hypothesis.

theorem exists_formalSchemePointsFunctor_map_eq {X Y : FormalScheme.{u}}
    (φ : formalSchemePointsFunctor.obj X ⟶ formalSchemePointsFunctor.obj Y) :
    ∃ f : X ⟶ Y, formalSchemePointsFunctor.map f = φ

AlgebraicGeometry.bijective_formalSchemePointsFunctor_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsFullSupplement.lean, line 96. The attribute's comment: “the bijection Mor(𝔛, 𝔜) = Mor(h_𝔛, h_𝔜) on all schemes, with no size hypothesis”.

For formal schemes 𝔛 and 𝔜, the functor of points on the category of all schemes induces a bijection

Mor_{Formal Schemes}(𝔛, 𝔜) = Mor_{PSh(Sch)}(h_𝔛, h_𝔜),

with no size hypothesis.

theorem bijective_formalSchemePointsFunctor_map {X Y : FormalScheme.{u}} :
    Function.Bijective fun f : X ⟶ Y => formalSchemePointsFunctor.map f

AlgebraicGeometry.full_formalSchemePointsFunctor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsFullSupplement.lean, line 104. The attribute's comment: “fullness of the functor of points on morphisms, with no size hypothesis”.

The functor of points of formal schemes on the category of all schemes is full, with no size hypothesis.

instance full_formalSchemePointsFunctor : formalSchemePointsFunctor.{u}.Full

AlgebraicGeometry.injective_formalSchemePointsFunctor_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsSheaf.lean, line 73. The attribute's comment: “injectivity of the functor of points on morphisms, with no size hypothesis”.

A morphism of formal schemes is determined by the natural transformation it induces on functors of points on the category of all schemes.

theorem injective_formalSchemePointsFunctor_map {X Y : FormalScheme.{u}} :
    Function.Injective fun f : X ⟶ Y => formalSchemePointsFunctor.map f

Tag 0AI2, a lemma

Tag 0AI2 in the Stacks Project.

AlgebraicGeometry.isSheafFor_formalSchemeFunctorOfPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsFpqcDescent.lean, line 290.

Stacks 0AI2 for the functor of points of Stacks 0AI1, on the schemes of size below κ: it satisfies the sheaf condition for every family of morphisms of Sch_κ which is an fpqc covering.

Members of Sch_κ have their fibre products in Sch_κ (AlgebraicGeometry.Scheme.size_pullback_lt), so a family of points compatible on Sch_κ is compatible on all schemes, and AlgebraicGeometry.isSheaf_fpqcTopology_formalSchemePoints applies.

theorem isSheafFor_formalSchemeFunctorOfPoints {κ : Cardinal.{u}} (X : FormalScheme.{u})
    {T : (schemeCutoff κ).FullSubcategory} {R : Presieve T}
    (covering : R ∈ Scheme.fpqcPrecoverage.{u}.comap (schemeCutoff κ).ι T) :
    Presieve.IsSheafFor ((formalSchemeFunctorOfPoints κ).obj X) R

AlgebraicGeometry.isSheaf_fpqcTopology_formalSchemePoints_of_isoSpf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsFpqcDescentSupplement.lean, line 49. The attribute's comment: “sheaf condition with gluing, for a formal scheme isomorphic to a formal spectrum”.

Stacks 0AI2, the gluing clause included, for an affine formal scheme: the functor of points of a formal scheme isomorphic to a formal spectrum is an fpqc sheaf.

Transporting along the isomorphism reduces this to AlgebraicGeometry.isSheaf_fpqcTopology_formalSchemePoints_spfFormalScheme.

theorem isSheaf_fpqcTopology_formalSchemePoints_of_isoSpf {X : FormalScheme.{u}}
    (hA : IsAdmissible A) (e : X ≅ spfFormalScheme A hA) :
    Presieve.IsSheaf Scheme.fpqcTopology.{u} (formalSchemePoints X)

AlgebraicGeometry.isSheaf_fpqcTopology_formalSchemePoints_schemeToFormalScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsSheaf.lean, line 109. The attribute's comment: “sheaf condition with gluing, for a scheme seen as a formal scheme”.

The functor of points of a scheme seen as a formal scheme satisfies the sheaf condition, gluing included, for fpqc coverings of schemes.

theorem isSheaf_fpqcTopology_formalSchemePoints_schemeToFormalScheme (Z : Scheme.{u}) :
    Presieve.IsSheaf Scheme.fpqcTopology.{u}
      (formalSchemePoints (schemeToFormalScheme.obj Z))

AlgebraicGeometry.isSheaf_fpqcTopology_formalSchemePoints_of_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsSheaf.lean, line 119. The attribute's comment: “sheaf condition with gluing, for a formal scheme isomorphic to a scheme”.

The functor of points of a formal scheme isomorphic to a scheme satisfies the sheaf condition, gluing included, for fpqc coverings of schemes.

theorem isSheaf_fpqcTopology_formalSchemePoints_of_iso {X : FormalScheme.{u}} {Z : Scheme.{u}}
    (e : X ≅ schemeToFormalScheme.obj Z) :
    Presieve.IsSheaf Scheme.fpqcTopology.{u} (formalSchemePoints X)

AlgebraicGeometry.isSheaf_zariskiTopology_formalSchemePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsZariskiSheaf.lean, line 96. The attribute's comment: “Zariski case in full, separatedness and gluing: the functor of points is a sheaf for the big Zariski topology on all schemes”.

Stacks 0AI2, the Zariski case in full. The functor of points of a formal scheme, on the category of all schemes, is a sheaf for the big Zariski topology: a matching family of points on the members of any Zariski covering of a scheme has a unique amalgamation.

Zariski coverings are the jointly surjective families of open immersions, so this follows from AlgebraicGeometry.isSheafFor_ofArrows_formalSchemePoints once the sheaf condition for a Grothendieck topology generated by a precoverage is reduced to its covering families, which is CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange.

theorem isSheaf_zariskiTopology_formalSchemePoints (X : FormalScheme.{u}) :
    Presieve.IsSheaf Scheme.zariskiTopology.{u} (formalSchemePoints X)

AlgebraicGeometry.FormalSpace.isFppfSheafFormalSchemePoints_formalScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSchemeComparisonSheaf.lean, line 164. The attribute's comment: “the fpqc sheaf condition read on the big fppf site of a base scheme”.

Stacks 0AIR, the sheaf clause, for an arbitrary formal scheme: the functor of points of a formal scheme à la EGA satisfies the fppf sheaf condition on the big fppf site of S, with no hypothesis assumed.

This is the first sentence of the source's remark, "by Lemma 87.2.2 the functor of points h_𝔛 associated to a formal scheme 𝔛 is a sheaf in the fppf topology". It is AlgebraicGeometry.isSheaf_fpqcTopology_formalSchemePoints, the full statement of Stacks 0AI2, read on the big fppf site of S by AlgebraicGeometry.FormalSpace.isFppfSheafFormalSchemePoints_of_isSheaf_fpqcTopology.

theorem isFppfSheafFormalSchemePoints_formalScheme (X : FormalScheme.{u}) :
    IsFppfSheafFormalSchemePoints B S hS X

Tag 0AI3, a remark

Tag 0AI3 in the Stacks Project.

AlgebraicGeometry.isIso_spfwGammaHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FormalSpectrumGlobalSectionsIso.lean, line 621. The attribute's comment: “the identification the counterparts of Lemmas 87.2.1 and 87.2.2 consume: Γ(Spfw A, 𝒪) = A for a weakly admissible ring, over the whole system of weak ideals of definition”.

The counterpart for McQuillan's weakening of the identification Γ(Spf A, 𝒪_{Spf A}) = A. For a weakly admissible topological ring A the canonical map A → Γ(Spfw A, 𝒪) into the global sections of the formal spectrum taken along the weak ideals of definition of A is an isomorphism of topological rings.

The proof is the one for an admissible ring, run over the whole family of weak ideals of definition instead of over the powers of a single ideal of definition. What it needs of the family is exactly that its members are open, that it is closed under intersection, and that it is a fundamental system of open neighbourhoods of zero — the last two being the intersection clause and the fundamental-system clause of Stacks 0AI3 — together with completeness and separatedness of A. The cofinality of the powers Iⁿ of a single I, which an ideal of definition has and a weak ideal of definition need not, is used nowhere.

theorem isIso_spfwGammaHom [IsLinearTopology A A] (hA : IsWeaklyAdmissible A) :
    IsIso (spfGammaHomOn A IsWeakIdealOfDefinition)

AlgebraicGeometry.spfwGammaIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FormalSpectrumGlobalSectionsIso.lean, line 631. The attribute's comment: “the identification the counterparts of Lemmas 87.2.1 and 87.2.2 consume: A = Γ(Spfw A, 𝒪) as topological rings, for a weakly admissible ring”.

The identification A = Γ(Spfw A, 𝒪) of topological rings for a weakly admissible topological ring: McQuillan's counterpart of the identification Γ(Spf A, 𝒪_{Spf A}) = A.

noncomputable def spfwGammaIso [IsLinearTopology A A] (hA : IsWeaklyAdmissible A) :
    TopCommRingCat.of A ≅ (spfPresheafOn A IsWeakIdealOfDefinition).obj (op ⊤)

AlgebraicGeometry.IsMcQuillanFormalScheme, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/McQuillanFormalScheme.lean, line 115. The attribute's comment: “the larger category of formal schemes based on weak admissibility: its objects”.

An object of LTRS is a formal scheme in the sense of McQuillan when every point has an open neighbourhood isomorphic to the formal spectrum, taken along the weak ideals of definition, of a weakly admissible topological ring. As for AlgebraicGeometry.IsFormalScheme, the isomorphism is asked for as one of presheafed spaces of topological rings, which for objects of LTRS is the same as an isomorphism in LTRS.

def IsMcQuillanFormalScheme : ObjectProperty LTRS.{u}

AlgebraicGeometry.McQuillanFormalScheme, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/McQuillanFormalScheme.lean, line 126. The attribute's comment: “the larger category of formal schemes based on weak admissibility: the category”.

The category of McQuillan formal schemes: the full subcategory of LTRS on the objects locally isomorphic to a formal spectrum taken along the weak ideals of definition of a weakly admissible topological ring. A morphism is a morphism of LTRS.

abbrev McQuillanFormalScheme

AlgebraicGeometry.injective_mcQuillanFormalSchemeFunctorOfPoints_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/McQuillanFormalScheme.lean, line 255. The attribute's comment: “the counterpart of Lemma 87.2.1: a morphism of McQuillan formal schemes is determined by the induced transformation of functors of points”.

Stacks 0AI3, the counterpart of Lemma 87.2.1 in McQuillan's setting. A morphism of McQuillan formal schemes whose source satisfies the size condition is determined by the natural transformation it induces on functors of points on the schemes of size below κ.

The proof is the source's: the morphisms Spec (A/I_λ) → 𝔛|_𝔘 → 𝔛 attached to the charts of 𝔛 are jointly epimorphic, and the size condition makes them points of 𝔛 seen by the functor of points. Their underlying maps cover 𝔛 because each Spec (A/I_λ) is carried homeomorphically onto the space of open primes of A, a prime being open exactly when it contains the weak ideal of definition I_λ; and they separate the sections of 𝒪_𝔛 because 𝒪_𝔛 is a sheaf and the sections of the structure presheaf of the chart are the limit over the weak ideals of definition.

theorem injective_mcQuillanFormalSchemeFunctorOfPoints_map {κ : Cardinal.{u}}
    {X Y : McQuillanFormalScheme.{u}} (hX : IsSizeBoundedMcQuillanFormalScheme κ X.obj) :
    Function.Injective fun f : X ⟶ Y => (mcQuillanFormalSchemeFunctorOfPoints κ).map f

AlgebraicGeometry.injective_mcQuillanFormalSchemePointsFunctor_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/McQuillanFormalScheme.lean, line 272. The attribute's comment: “the counterpart of Lemma 87.2.1: injectivity of the functor of points on morphisms of McQuillan formal schemes, with no size hypothesis”.

Stacks 0AI3, the counterpart of Lemma 87.2.1 in McQuillan's setting, with no size hypothesis: a morphism of McQuillan formal schemes is determined by the transformation it induces on functors of points on all schemes. Every McQuillan formal scheme satisfies the size condition for some cutoff, and the functor of points on Sch_κ is the restriction of the functor of points on all schemes.

theorem injective_mcQuillanFormalSchemePointsFunctor_map {X Y : McQuillanFormalScheme.{u}} :
    Function.Injective fun f : X ⟶ Y => mcQuillanFormalSchemePointsFunctor.map f

AlgebraicGeometry.isSeparated_fpqcTopology_mcQuillanFormalSchemePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/McQuillanFormalScheme.lean, line 293. The attribute's comment: “the counterpart of Lemma 87.2.2: the functor of points of a McQuillan formal scheme on all schemes is separated for the fpqc topology”.

Stacks 0AI3, the counterpart of Lemma 87.2.2 in McQuillan's setting. The functor of points of a McQuillan formal scheme, on the category of all schemes, is separated for the fpqc topology: a point of 𝔛 over a scheme T is determined by its restrictions along any fpqc covering sieve of T.

The proof is the source's: an fpqc covering sieve contains an fpqc covering family, whose members are flat and jointly surjective, and a morphism from a scheme to a locally topologically ringed space is determined by its restrictions along such a family.

theorem isSeparated_fpqcTopology_mcQuillanFormalSchemePoints (X : McQuillanFormalScheme.{u}) :
    Presieve.IsSeparated Scheme.fpqcTopology.{u} (mcQuillanFormalSchemePoints X)

AlgebraicGeometry.isSeparatedFor_mcQuillanFormalSchemeFunctorOfPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/McQuillanFormalScheme.lean, line 306. The attribute's comment: “the counterpart of Lemma 87.2.2: the functor of points of a McQuillan formal scheme on the schemes of size below the cutoff is separated for the fpqc topology”.

Stacks 0AI3, the counterpart of Lemma 87.2.2 in McQuillan's setting, for the functor of points on the schemes of size below κ: a point of 𝔛 over a scheme T of Sch_κ is determined by its restrictions along a family of morphisms of Sch_κ which is an fpqc covering of T.

theorem isSeparatedFor_mcQuillanFormalSchemeFunctorOfPoints {κ : Cardinal.{u}}
    (X : McQuillanFormalScheme.{u}) {T : (schemeCutoff κ).FullSubcategory} {R : Presieve T}
    (hR : R ∈ Scheme.fpqcPrecoverage.{u}.comap (schemeCutoff κ).ι T) :
    Presieve.IsSeparatedFor ((mcQuillanFormalSchemeFunctorOfPoints κ).obj X) R

AlgebraicGeometry.isSheaf_zariskiTopology_mcQuillanFormalSchemePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/McQuillanFormalScheme.lean, line 381. The attribute's comment: “the counterpart of Lemma 87.2.2: the functor of points of a McQuillan formal scheme on all schemes is a sheaf for the big Zariski topology”.

Stacks 0AI3, the counterpart of Lemma 87.2.2 in McQuillan's setting, for the big Zariski topology. The functor of points of a McQuillan formal scheme, on the category of all schemes, is a sheaf for the big Zariski topology: a matching family of points on the members of any Zariski covering of a scheme has a unique amalgamation.

The proof is the source's: Zariski coverings are the jointly surjective families of open immersions, and a matching family of morphisms into a locally topologically ringed space on the members of an open covering glues uniquely.

theorem isSheaf_zariskiTopology_mcQuillanFormalSchemePoints (X : McQuillanFormalScheme.{u}) :
    Presieve.IsSheaf Scheme.zariskiTopology.{u} (mcQuillanFormalSchemePoints X)

AlgebraicGeometry.exists_comp_eq_of_flat_surjective_spfwLTRS, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakFormalSpectrumFpqcDescent.lean, line 125. The attribute's comment: “the counterpart of Lemma 87.2.2: existence of an amalgamation at an affine test scheme, for a point of McQuillan's formal spectrum of a weakly admissible ring along a faithfully flat morphism of affine schemes”.

Stacks 0AI3, the existence half of the counterpart of Lemma 87.2.2 at an affine test scheme. For a weakly admissible topological ring A, a point Spec S ⟶ Spfw A of McQuillan's formal spectrum whose two pullbacks along any pair of morphisms agreeing over Spec R agree descends along a faithfully flat morphism Spec S → Spec R of affine schemes.

This is the affine descent step the source's proof of Lemma 87.2.2 reduces to, and it is that proof unchanged: the weak ideals of definition of A form a weak ideal system, and the identification Γ(Spfw A, 𝒪) = A it consumes is AlgebraicGeometry.isIso_spfwGammaHom. The separatedness half, which together with this one is the sheaf condition for the covering {Spec S → Spec R}, is AlgebraicGeometry.isSeparated_fpqcTopology_mcQuillanFormalSchemePoints.

theorem exists_comp_eq_of_flat_surjective_spfwLTRS (hA : IsWeaklyAdmissible A)
    {R S : CommRingCat.{u}} (φ : R ⟶ S) (hflat : Flat (Spec.map φ))
    (hsurj : Surjective (Spec.map φ)) (u : schemeToLTRSObj (Spec S) ⟶ spfwLTRS A hA.1)
    (hu : ∀ {Z : Scheme.{u}} (p₁ p₂ : Z ⟶ Spec S), p₁ ≫ Spec.map φ = p₂ ≫ Spec.map φ →
      schemeToLTRS.map p₁ ≫ u = schemeToLTRS.map p₂ ≫ u) :
    ∃ t : schemeToLTRSObj (Spec R) ⟶ spfwLTRS A hA.1,
      schemeToLTRS.map (Spec.map φ) ≫ t = u

AlgebraicGeometry.isSheaf_fpqcTopology_mcQuillanFormalSchemePoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakFunctorOfPointsFpqcSheaf.lean, line 242. The attribute's comment: “the counterpart of Lemma 87.2.2: the functor of points of a McQuillan formal scheme on all schemes is a sheaf for the fpqc topology”.

Stacks 0AI3, the existence half of the counterpart of Lemma 87.2.2 in McQuillan's setting, and so the full sheaf condition. The functor of points of a McQuillan formal scheme 𝔛, on the category of all schemes, satisfies the sheaf condition for fpqc coverings.

The proof is the source's, and is the one already carried out for admissible rings in AlgebraicGeometry.isSheaf_fpqcTopology_formalSchemePoints. Uniqueness of amalgamations is AlgebraicGeometry.isSeparated_fpqcTopology_mcQuillanFormalSchemePoints. For existence, a compatible family of points first descends on underlying spaces to a continuous map g : T → 𝔛, continuous maps into a fixed space forming an fpqc sheaf. Around each point p of T choose a weak affine formal chart 𝔘 ≅ Spfw A of 𝔛 containing g p; over the open g⁻¹ 𝔘 every member of the pulled-back family lands in 𝔘, so it has an amalgamation by AlgebraicGeometry.exists_isAmalgamation_of_range_subset_weakChart. These local amalgamations glue because the functor of points is a Zariski sheaf (AlgebraicGeometry.isSheaf_zariskiTopology_mcQuillanFormalSchemePoints).

theorem isSheaf_fpqcTopology_mcQuillanFormalSchemePoints (X : McQuillanFormalScheme.{u}) :
    Presieve.IsSheaf Scheme.fpqcTopology.{u} (mcQuillanFormalSchemePoints X)

AlgebraicGeometry.isSheafFor_mcQuillanFormalSchemeFunctorOfPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakFunctorOfPointsFpqcSheaf.lean, line 288. The attribute's comment: “the counterpart of Lemma 87.2.2: the functor of points of a McQuillan formal scheme on the schemes of size below the cutoff is a sheaf for the fpqc topology”.

Stacks 0AI3, the counterpart of Lemma 87.2.2 in McQuillan's setting for the functor of points on the schemes of size below κ: it satisfies the sheaf condition for every family of morphisms of Sch_κ which is an fpqc covering.

Members of Sch_κ have their fibre products in Sch_κ (AlgebraicGeometry.Scheme.size_pullback_lt), so a family of points compatible on Sch_κ is compatible on all schemes, and AlgebraicGeometry.isSheaf_fpqcTopology_mcQuillanFormalSchemePoints applies.

theorem isSheafFor_mcQuillanFormalSchemeFunctorOfPoints {κ : Cardinal.{u}}
    (X : McQuillanFormalScheme.{u}) {T : (schemeCutoff κ).FullSubcategory} {R : Presieve T}
    (covering : R ∈ Scheme.fpqcPrecoverage.{u}.comap (schemeCutoff κ).ι T) :
    Presieve.IsSheafFor ((mcQuillanFormalSchemeFunctorOfPoints κ).obj X) R

AlgebraicGeometry.bijective_mcQuillanFormalSchemeFunctorOfPoints_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/WeakFunctorOfPointsFull.lean, line 596. The attribute's comment: “the counterpart of Lemma 87.2.1: the bijection Mor(𝔛, 𝔜) = Mor(h_𝔛, h_𝔜) for a McQuillan formal scheme 𝔛 whose size is bounded by the cutoff”.

Stacks 0AI3, the counterpart of Lemma 87.2.1 in McQuillan's setting, in full. For a McQuillan formal scheme 𝔛 whose size is not too large — the schemes Spec (A/I_λ) cut out of its weak affine formal charts being objects of Sch_κ — and any McQuillan formal scheme 𝔜,

Mor_{McQuillan Formal Schemes}(𝔛, 𝔜) = Mor_{PSh(Sch_κ)}(h_𝔛, h_𝔜).

Injectivity is AlgebraicGeometry.injective_mcQuillanFormalSchemeFunctorOfPoints_map and surjectivity is AlgebraicGeometry.exists_mcQuillanFormalSchemeFunctorOfPoints_map_eq.

theorem bijective_mcQuillanFormalSchemeFunctorOfPoints_map {κ : Cardinal.{u}}
    {X Y : McQuillanFormalScheme.{u}} (hX : IsSizeBoundedMcQuillanFormalScheme κ X.obj) :
    Function.Bijective fun f : X ⟶ Y => (mcQuillanFormalSchemeFunctorOfPoints κ).map f

TopologicalRing.isWeakIdealOfDefinition_inf_of_isOpen_right, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 218. The attribute's comment: “intersection”.

The intersection of a weak ideal of definition with an open ideal is a weak ideal of definition.

public lemma isWeakIdealOfDefinition_inf_of_isOpen_right {A : Type*} [CommRing A]
    [TopologicalSpace A] {I J : Ideal A} (hI : TopologicalRing.IsWeakIdealOfDefinition I)
    (hJ : IsOpen (J : Set A)) : TopologicalRing.IsWeakIdealOfDefinition (I ⊓ J)

TopologicalRing.hasBasis_nhds_zero_isWeakIdealOfDefinition, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 233. The attribute's comment: “weak_basis”.

In a weakly admissible linearly topologized ring, its weak ideals of definition form a fundamental system of neighborhoods of zero.

public lemma hasBasis_nhds_zero_isWeakIdealOfDefinition
    {A : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] (hA : TopologicalRing.IsWeaklyAdmissible A) :
    (nhds (0 : A)).HasBasis
      (fun I : Ideal A ↦ TopologicalRing.IsWeakIdealOfDefinition I)
      (fun I : Ideal A ↦ (I : Set A))

Declarations registered for the tag:

TopologicalRing.IsAdmissible, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 202 (StacksFrontier): “admissible_recall”.
TopologicalRing.IsWeakIdealOfDefinition, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 208 (StacksFrontier): “weak_admissibility”.
TopologicalRing.IsWeaklyAdmissible, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 209 (StacksFrontier): “weak_admissibility”.

Tag 0AI4, a remark

Tag 0AI4 in the Stacks Project.

CategoryTheory.TopologicalSheaf.sheafSize, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TopologicalSheaf.lean, line 48. The attribute's comment: “size”.

The size of a sheaf of topological spaces is the supremum of the cardinalities of its values on objects of the site.

public noncomputable abbrev sheafSize (H : Sheaf J TopCat.{w}) : Cardinal.{max u w}

CategoryTheory.TopologicalSheaf.exists_bounded_subsheaf_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TopologicalSheaf.lean, line 267. The attribute's comment: “bounded_subsheaf”.

Any map from a fixed presheaf of topological spaces to a sheaf factors through a subsheaf of uniformly bounded size.

public theorem exists_bounded_subsheaf_factorization (F : Cᵒᵖ ⥤ TopCat.{w}) :
    ∃ κ : Cardinal.{max u v w}, ∀ (G : Sheaf J TopCat.{w}) (f : F ⟶ G.obj),
      ∃ (G' : Sheaf J TopCat.{w}) (i : G' ⟶ G),
        Mono i ∧ Cardinal.lift.{v} (sheafSize G') ≤ κ ∧
          ∃ f' : F ⟶ G'.obj, f' ≫ i.hom = f

CategoryTheory.TopologicalSheaf.hasWeakSheafify_topCat, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TopologicalSheaf.lean, line 403. The attribute's comment: “sheafification”.

The inclusion of topological-space-valued sheaves into presheaves has a left adjoint.

public noncomputable instance hasWeakSheafify_topCat :
    HasWeakSheafify J TopCat.{max u v w}

Declarations registered for the tag:

CategoryTheory.Sheaf.hasLimitsOfSize registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/TopologicalSheaf.lean, line 55 (StacksFrontier): “limits”. References: EGA 0 (3.2.6), “partial”; SGA 3 IV (4.4.1), “(i)”; SGA 4 I (8.12.9), “partial”; SGA 4 II (4.1), “more general”; SGA 4 II (4.8), “more general”.
CategoryTheory.Sheaf.createsLimits registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/TopologicalSheaf.lean, line 61 (StacksFrontier): “limits”. References: EGA 0 (3.2.6), “more general”; SGA 3 IV (4.4.1), “more general”; SGA 4 II (4.1), “more general”.
CategoryTheory.GrothendieckTopology.Point.isSheaf_skyscraperPresheaf registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/TopologicalSheaf.lean, line 70 (StacksFrontier): “point_mapping_sheaf”.
CategoryTheory.GrothendieckTopology.Point.W_isInvertedBy_presheafFiber registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/TopologicalSheaf.lean, line 443 (StacksFrontier): “stalk_preservation”.

Sources

LeanAlgebraicGeometry.isIso_spfGammaHom · AlgebraicGeometry.spfGammaIso · AlgebraicGeometry.injective_spfLTRSMap · AlgebraicGeometry.surjective_spfLTRSMap · AlgebraicGeometry.bijective_spfLTRSMap · AlgebraicGeometry.schemeToFormalScheme · AlgebraicGeometry.full_schemeToFormalScheme · AlgebraicGeometry.faithful_schemeToFormalScheme

Section87.4 Topological rings and modules #

Section 87.4 of the Stacks Project, Tag 0AMQ. 12 tags here are carried by 41 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AMR, an example

Tag 0AMR in the Stacks Project.

TopologicalModule.Nonuniform.exists_pow_X_smul_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/NonuniformModule.lean, line 128. The attribute's comment: “nonuniform_module_example”.

The pointwise condition of the source: for every m and every x ∈ ⨁_{n ∈ ℕ} k[[t]] there is a j with t ^ j • x ∈ M m. It holds because x has only finitely many nonzero coordinates.

theorem exists_pow_X_smul_mem (m : ℕ) (x : ℕ →₀ PowerSeries k) :
    ∃ j : ℕ, (X : PowerSeries k) ^ j • x ∈ coordinateSubmodule k m

TopologicalModule.Nonuniform.not_exists_forall_pow_X_smul_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/NonuniformModule.lean, line 194. The attribute's comment: “nonuniform_module_example”.

The uniform condition fails: for m ≥ 1 there is no j with t ^ j • M ⊆ M m.

theorem not_exists_forall_pow_X_smul_mem {m : ℕ} (hm : 1 ≤ m) :
    ¬ ∃ j : ℕ, ∀ x : ℕ →₀ PowerSeries k,
      (X : PowerSeries k) ^ j • x ∈ coordinateSubmodule k m

TopologicalModule.Nonuniform.exists_isLinearTopology_not_exists_isOpen_ideal_smul_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/NonuniformModule.lean, line 217. The attribute's comment: “nonuniform_module_example”.

The source's example, as an existence statement: over R = k[[t]] with the t-adic topology there is a linearly topologized R-module M, with a fundamental system N of open submodules, for which no open ideal I of R satisfies I • M ⊆ N 1.

theorem exists_isLinearTopology_not_exists_isOpen_ideal_smul_mem :
    ∃ (τ : TopologicalSpace (ℕ →₀ PowerSeries k))
      (N : ℕ → Submodule (PowerSeries k) (ℕ →₀ PowerSeries k)),
      (@nhds _ τ 0).HasBasis (fun _ : ℕ ↦ True) (fun m ↦ (N m : Set (ℕ →₀ PowerSeries k))) ∧
      @IsTopologicalAddGroup _ τ _ ∧
      @ContinuousSMul (PowerSeries k) _ _ _ τ ∧
      @IsLinearTopology (PowerSeries k) _ _ _ _ τ ∧
      ¬ ∃ I : Ideal (PowerSeries k), IsOpen (I : Set (PowerSeries k)) ∧
          ∀ f ∈ I, ∀ x : ℕ →₀ PowerSeries k, f • x ∈ N 1

TopologicalModule.continuousSMul_iff_forall_exists_smul_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/ScalarContinuity.lean, line 53. The attribute's comment: “scalar_continuity_criterion”.

Tag 0AMR. Let I be a fundamental system of open ideals of a topological ring R and let N be a fundamental system of open submodules of an R-module M. Then scalar multiplication R × M → M is continuous exactly when I λ • x ⊆ N μ for some λ, for every x : M and every μ.

theorem continuousSMul_iff_forall_exists_smul_mem
    (hI : (𝓝 (0 : R)).HasBasis (fun _ : ι ↦ True) fun l ↦ (I l : Set R))
    (hN : (𝓝 (0 : M)).HasBasis (fun _ : κ ↦ True) fun m ↦ (N m : Set M)) :
    ContinuousSMul R M ↔ ∀ (x : M) (μ : κ), ∃ l : ι, ∀ f ∈ I l, f • x ∈ N μ

TopologicalModule.continuousSMul_iff_forall_exists_coset_smul_coset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/ScalarContinuity.lean, line 85. The attribute's comment: “scalar_continuity_criterion”.

Tag 0AMR. The displayed form of the continuity of R × M → M: for all f, x and μ there are λ and ν with (f + I λ) • (x + N ν) ⊆ f • x + N μ. The source deduces it from TopologicalModule.continuousSMul_iff_forall_exists_smul_mem using that f • N ν + I λ • N ν ⊆ N μ whenever N ν ⊆ N μ; here ν = μ always works.

theorem continuousSMul_iff_forall_exists_coset_smul_coset
    (hI : (𝓝 (0 : R)).HasBasis (fun _ : ι ↦ True) fun l ↦ (I l : Set R))
    (hN : (𝓝 (0 : M)).HasBasis (fun _ : κ ↦ True) fun m ↦ (N m : Set M)) :
    ContinuousSMul R M ↔ ∀ (f : R) (x : M) (μ : κ), ∃ (l : ι) (ν : κ),
      ∀ g ∈ I l, ∀ y ∈ N ν, (f + g) • (x + y) - f • x ∈ N μ

TopologicalRing.continuous_add_of_hasBasis_addSubgroup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 166. The attribute's comment: “addition_continuous”.

Addition is continuous when translates of additive subgroups form a neighborhood basis.

public theorem continuous_add_of_hasBasis_addSubgroup
    {M ι : Type*} [AddCommGroup M] [TopologicalSpace M]
    (Mμ : ι → AddSubgroup M)
    (hbasis : ∀ x : M, (nhds x).HasBasis (fun _ : ι => True)
      (fun μ => (fun y : M => x + y) '' (Mμ μ : Set M))) :
    Continuous (fun p : M × M => p.1 + p.2)

TopologicalRing.exists_isOpen_ideal_map_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 192. The attribute's comment: “continuous_ring_map_open_ideal”. References: EGA 0 (19.0.3), “𝔍B ⊂ 𝔎 clause”; EGA 0 (7.7.5), “existence of open J”.

Every open ideal in the target of a continuous ring homomorphism contains the extension of an open ideal from the source.

public theorem exists_isOpen_ideal_map_le {R S : Type*} [CommRing R] [CommRing S]
    [TopologicalSpace R] [TopologicalSpace S] (f : R →+* S) (hf : Continuous f)
    (J : Ideal S) (hJ : IsOpen (J : Set S)) :
    ∃ I : Ideal R, IsOpen (I : Set R) ∧ Ideal.map f I ≤ J

Tag 0AMS, a lemma

Tag 0AMS in the Stacks Project.

TopologicalRing.closure_eq_iInter_sup_of_hasBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 562.

Stacks Project, Tag 0AMS. Let M be a linearly topologized R-module and let L i, i : ι, be a fundamental system of open submodules of M. The closure of a submodule N ⊆ M is the intersection of the submodules N + L i.

public theorem closure_eq_iInter_sup_of_hasBasis {ι : Sort*} (L : ι → Submodule R M)
    (hopen : ∀ i, IsOpen ((L i : Set M)))
    (hbasis : (𝓝 (0 : M)).HasBasis (fun _ : ι ↦ True) fun i ↦ ((L i : Set M)))
    (N : Submodule R M) :
    closure (N : Set M) = ⋂ i, ((N ⊔ L i : Submodule R M) : Set M)

TopologicalRing.topologicalClosure_eq_iInf_sup_of_hasBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 577. The attribute's comment: “the same identity read as an equality of submodules”.

Stacks Project, Tag 0AMS, as an equality of submodules: the topological closure of a submodule N is the infimum of the submodules N + L i over a fundamental system L i of open submodules.

public theorem topologicalClosure_eq_iInf_sup_of_hasBasis [ContinuousConstSMul R M]
    {ι : Sort*} (L : ι → Submodule R M)
    (hopen : ∀ i, IsOpen ((L i : Set M)))
    (hbasis : (𝓝 (0 : M)).HasBasis (fun _ : ι ↦ True) fun i ↦ ((L i : Set M)))
    (N : Submodule R M) :
    N.topologicalClosure = ⨅ i, (N ⊔ L i : Submodule R M)

Tag 0ARZ, a lemma

Tag 0ARZ in the Stacks Project.

TopologicalRing.completionSubtype_injective, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 143. The attribute's comment: “part (1), injectivity”.

Stacks Project, Tag 0ARZ, part (1). The map from the completion of a submodule to the completion of the ambient linearly topologized module is injective.

public lemma completionSubtype_injective (N : Submodule R M) :
    Function.Injective (completionSubtype N)

TopologicalRing.exact_completionSubtype_completionQuotient, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 247. The attribute's comment: “part (1), exactness”.

Stacks Project, Tag 0ARZ, part (1). The image of the completed submodule is the kernel of the map from the completed module to the completion of its quotient.

public lemma exact_completionSubtype_completionQuotient (N : Submodule R M) :
    range (completionSubtype N) =
      {x | completionQuotient N x = (0 : M ⧸ N)}

TopologicalRing.range_completionSubtype_eq_closure, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 275. The attribute's comment: “part (2)”.

Stacks Project, Tag 0ARZ, part (2). In the completion of a linearly topologized module, the image of the completion of a submodule is precisely the closure of the image of that submodule.

public lemma range_completionSubtype_eq_closure (N : Submodule R M) :
    range (completionSubtype N) =
      closure (range fun x : N ↦ (x.1 : TopologicalCompletion M))

Tag 0AMT, a lemma

Tag 0AMT in the Stacks Project.

TopologicalRing.t2Space_quotient_of_isClosed, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 596. The attribute's comment: “the quotient is separated”.

Stacks Project, Tag 0AMT. The quotient of a linearly topologized module by a closed submodule is separated; this is the Hausdorff half of the completeness of M ⧸ N.

public lemma t2Space_quotient_of_isClosed {R : Type u} {M : Type v}
    [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M]
    [IsLinearTopology R M] (N : Submodule R M) (hN : IsClosed (N : Set M)) :
    T2Space (M ⧸ N)

TopologicalRing.completeSpace_quotient_of_isCountablyGenerated, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 608. The attribute's comment: “the quotient is complete”.

Stacks Project, Tag 0AMT. The quotient of a complete, linearly topologized module with a countable fundamental system of neighbourhoods of zero by a submodule is itself complete for the canonical uniformity of a topological additive group.

public lemma completeSpace_quotient_of_isCountablyGenerated {R : Type u} {M : Type v}
    [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M]
    [IsLinearTopology R M] (N : Submodule R M)
    (hM : @CompleteSpace M (IsTopologicalAddGroup.rightUniformSpace M))
    (hcount : (nhds (0 : M)).IsCountablyGenerated) :
    @CompleteSpace (M ⧸ N) (IsTopologicalAddGroup.rightUniformSpace (M ⧸ N))

Declarations registered for the tag:

Submodule.isOpenMap_mkQ registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 625 (StacksFrontier): “the map to the quotient is open”.

Tag 0AS0, a lemma

Tag 0AS0 in the Stacks Project.

TopologicalRing.completionQuotient_surjective_of_isCountablyGenerated, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 425. The attribute's comment: “part (1), surjectivity”.

Stacks Project, Tag 0AS0, part (1). For a linearly topologized module with a countable fundamental system of neighborhoods of zero, the canonical map from its completion to the completion of a quotient is surjective.

public lemma completionQuotient_surjective_of_isCountablyGenerated
    (N : Submodule R M) (hM : (nhds (0 : M)).IsCountablyGenerated) :
    Function.Surjective (TopologicalRing.completionQuotient N)

TopologicalRing.completionQuotient_isOpenMap_of_isCountablyGenerated, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 435. The attribute's comment: “part (3)”.

Stacks Project, Tag 0AS0, part (3). For a linearly topologized module with a countable fundamental system of neighborhoods of zero, the canonical map from its completion to the completion of a quotient is open.

public lemma completionQuotient_isOpenMap_of_isCountablyGenerated
    (N : Submodule R M) (hM : (nhds (0 : M)).IsCountablyGenerated) :
    IsOpenMap (TopologicalRing.completionQuotient N)

Declarations registered for the tag:

TopologicalRing.completionSubtype_injective, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 411 (StacksFrontier): “part (1), injectivity”.
TopologicalRing.exact_completionSubtype_completionQuotient, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 414 (StacksFrontier): “part (1), exactness at the middle term”.
TopologicalRing.range_completionSubtype_eq_closure, declared in the repository, registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 417 (StacksFrontier): “part (2)”.

Tag 0F1S, a lemma

Tag 0F1S in the Stacks Project.

TopologicalRing.exists_isOpen_adic_submodule_completionAlong, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionAlong.lean, line 439. The attribute's comment: “open_adic_completion”.

The completion of a module containing an open I-adic submodule again contains an open submodule with the I-adic topology.

public lemma exists_isOpen_adic_submodule_completionAlong
    {R : Type*} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    {M : Type*} [AddCommGroup M] [Module R M] [TopologicalSpace M]
    [IsTopologicalAddGroup M] [ContinuousSMul R M]
    (I : Ideal R) (hI : I.FG) (N : Submodule R M) (_hN : IsOpen (N : Set M))
    (_hAdic : (𝓝 (0 : N)).HasBasis (fun _ : ℕ ↦ True)
      (fun n ↦ ((I ^ n • ⊤ : Submodule R N) : Set N))) :
    ∃ P : Submodule R (TopologicalRing.CompletionAlong I N),
      @IsOpen (TopologicalRing.CompletionAlong I N)
          (TopologicalRing.CompletionAlong.limitTopology I N) (P : Set _) ∧
        TopologicalSpace.induced
          (fun p : P => (p : TopologicalRing.CompletionAlong I N))
          (TopologicalRing.CompletionAlong.limitTopology I N) = I.adicModuleTopology P

TopologicalRing.CompletionAlong.quotPowEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionAlong.lean, line 674. The attribute's comment: “completion_mod_ideal_power”.

The second conclusion of Tag 0F1S at the level of the filtration I ^ n N: M^ / I ^ n M^ = M / I ^ n M.

public noncomputable def quotPowEquiv (I : Ideal R) (hI : I.FG) (N : Submodule R M) (n : ℕ) :
    ((CompletionAlong I N) ⧸ (I ^ n • ⊤ : Submodule R (CompletionAlong I N))) ≃ₗ[R]
      (M ⧸ (I ^ n • ⊤ : Submodule R M))

TopologicalRing.exists_isOpen_adic_submodule_completionOverOpen, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionAlong.lean, line 874. The attribute's comment: “open_adic_completion”.

Tag 0F1S, first conclusion, over the completion of M taken over all of its open submodules: M^ has an open submodule whose topology is I-adic.

public lemma exists_isOpen_adic_submodule_completionOverOpen (I : Ideal R) (hI : I.FG)
    (N : Submodule R M) (hN : IsOpen (N : Set M))
    (hAdic : (𝓝 (0 : N)).HasBasis (fun _ : ℕ ↦ True)
      (fun n ↦ ((I ^ n • ⊤ : Submodule R N) : Set N))) :
    ∃ P : Submodule R (CompletionOverOpen R M),
      @IsOpen (CompletionOverOpen R M) (CompletionOverOpen.limitTopology R M) (P : Set _) ∧
        TopologicalSpace.induced (fun p : P ↦ (p : CompletionOverOpen R M))
          (CompletionOverOpen.limitTopology R M) = I.adicModuleTopology P

TopologicalRing.completionOverOpenQuotPowEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletionAlong.lean, line 914. The attribute's comment: “completion_mod_ideal_power”.

Tag 0F1S, second conclusion, over the completion of M taken over all of its open submodules: M^ / I ^ n M^ = M / I ^ n M for every n, in particular for every n ≥ 1.

public noncomputable def completionOverOpenQuotPowEquiv (I : Ideal R) (hI : I.FG)
    (N : Submodule R M) (hN : IsOpen (N : Set M))
    (hAdic : (𝓝 (0 : N)).HasBasis (fun _ : ℕ ↦ True)
      (fun n ↦ ((I ^ n • ⊤ : Submodule R N) : Set N))) (n : ℕ) :
    ((CompletionOverOpen R M) ⧸ (I ^ n • ⊤ : Submodule R (CompletionOverOpen R M))) ≃ₗ[R]
      (M ⧸ (I ^ n • ⊤ : Submodule R M))

Tag 0AMU, a definition

Tag 0AMU in the Stacks Project.

TopologicalRing.tensorProductTopology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletedTensorProduct.lean, line 207. The attribute's comment: “tensor product”. References: EGA 0 (20.4.1).

The topology on the usual tensor product whose fundamental open submodules are the images of P ⊗[R] N + M ⊗[R] Q for open P and Q.

def tensorProductTopology : TopologicalSpace (M ⊗[R] N)

TopologicalRing.CompletedTensorProduct, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletedTensorProduct.lean, line 297. The attribute's comment: “completed tensor product”. References: EGA 0 (7.7.2), “completed tensor product”; EGA 0 (7.7.1); EGA 0 (7.7.5), “completed tensor product”; SGA 3 VIIB (0.3), “def of L⊗̂M”; SGA 3 VIIB (0.5.A), “def of M⊗̂_k N”.

The completed tensor product of two topologized modules: the uniform completion of their tensor product with its tensor product topology.

abbrev CompletedTensorProduct

TopologicalRing.quotientTensorProductLimitIdentification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletedTensorProduct.lean, line 573. The attribute's comment: “second inverse-limit identification”. References: EGA 0 (7.7.2), “(M/V)⊗(N/W) identif.”; EGA 0 (7.7.1), “lim M/V ⊗ N/W”; EGA 0 (7.7.5), “lim M/Mμ ⊗ N/Nν”; SGA 3 VIIB (0.3), “lim (L/L')⊗(M/M')”.

The componentwise quotient-tensor-quotient equivalences identify the two inverse limits in Tag 0AMU. The specification records that the map is exactly TensorProduct.quotientTensorQuotientEquiv in every component.

noncomputable def quotientTensorProductLimitIdentification :
    { e : QuotientTensorProductLimit (R := R) (M := M) (N := N) ≃L[R]
        TensorProductQuotientLimit (R := R) (M := M) (N := N) //
      ∀ x : QuotientTensorProductLimit (R := R) (M := M) (N := N),
        ∀ i : TensorProductSubmoduleIndex (R := R) (M := M) (N := N),
          ((e x : TensorProductQuotientLimit (R := R) (M := M) (N := N)) :
              ∀ j : TensorProductSubmoduleIndex (R := R) (M := M) (N := N),
                TensorProductQuotient j) i =
            TensorProduct.quotientTensorQuotientEquiv i.1.1 i.2.1
              (((x : QuotientTensorProductLimit (R := R) (M := M) (N := N)) :
                  ∀ j : TensorProductSubmoduleIndex (R := R) (M := M) (N := N),
                    QuotientTensorProduct j) i) }

TopologicalRing.exists_completedTensorProductEquivQuotientLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletedTensorProduct.lean, line 840. The attribute's comment: “first inverse-limit identification”. References: EGA 0 (7.7.2), “lim (M⊗N)/(...) identif.”; EGA 0 (7.7.1), “limit identification”; EGA 0 (7.7.5), “lim (M⊗N)/(Mμ⊗N+M⊗Nν)”; SGA 3 VIIB (0.3), “P = lim quotients”.

The completion is canonically topologically linearly isomorphic to the inverse limit of its discrete quotients. Every component of the identification extends the usual quotient map.

theorem exists_completedTensorProductEquivQuotientLimit :
    ∃ e : CompletedTensorProduct (R := R) (M := M) (N := N) ≃L[R]
        TensorProductQuotientLimit (R := R) (M := M) (N := N),
      ∀ z : M ⊗[R] N,
        ∀ i : TensorProductSubmoduleIndex (R := R) (M := M) (N := N),
          ((e (↑z : CompletedTensorProduct (R := R) (M := M) (N := N)) :
              TensorProductQuotientLimit (R := R) (M := M) (N := N)) :
              ∀ j : TensorProductSubmoduleIndex (R := R) (M := M) (N := N),
                TensorProductQuotient j) i = Submodule.Quotient.mk z

Tag 0AMV, a definition

Tag 0AMV in the Stacks Project.

TopologicalRing.IsWeakIdealOfDefinition, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 72. The attribute's comment: “part (2)”.

A weak ideal of definition is an open ideal consisting entirely of topologically nilpotent elements.

abbrev IsWeakIdealOfDefinition {R : Type*} [CommRing R] [TopologicalSpace R]
    (I : Ideal R) : Prop

TopologicalRing.IsWeaklyPreAdmissible, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 79. The attribute's comment: “part (3)”.

A topological ring is weakly pre-admissible if it has a weak ideal of definition.

abbrev IsWeaklyPreAdmissible (R : Type*) [CommRing R] [TopologicalSpace R] : Prop

TopologicalRing.IsWeaklyAdmissible, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 86. The attribute's comment: “part (4)”.

A linearly topologized ring is weakly admissible if it is weakly pre-admissible, complete, and separated. Completeness uses the canonical uniformity of its additive topological group.

abbrev IsWeaklyAdmissible (R : Type*) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [IsLinearTopology R R] : Prop

Declarations registered for the tag:

IsTopologicallyNilpotent registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 65 (StacksFrontier): “part (1)”. References: EGA 0 (7.1.1); SGA 3 VIIB (0.1.2).

Tag 0DCZ, a lemma

Tag 0DCZ in the Stacks Project.

TopologicalRing.henselianPair_of_isWeaklyAdmissible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Completion.lean, line 502. References: EGA 0 (7.1.10).

Stacks Project, Tag 0DCZ. A weak ideal of definition in a weakly admissible topological ring forms a henselian pair with the ring.

theorem henselianPair_of_isWeaklyAdmissible
    (A : Type*) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] (hA : TopologicalRing.IsWeaklyAdmissible A)
    (I : Ideal A) (hI : TopologicalRing.IsWeakIdealOfDefinition I) :
    HenselianPair A I

Tag 0AMW, a lemma

Tag 0AMW in the Stacks Project.

TopologicalRing.isClosed_topologicalNilradical, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 112. The attribute's comment: “closedness”.

In a linearly topologized commutative ring, the ideal of topologically nilpotent elements is closed.

public lemma isClosed_topologicalNilradical {B : Type*} [CommRing B] [TopologicalSpace B]
    [IsTopologicalRing B] [IsLinearTopology B B] :
    IsClosed (topologicalNilradical B : Set B)

TopologicalRing.topologicalNilradical_isRadical, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 130. The attribute's comment: “radicality”.

In a linearly topologized commutative ring, the ideal of topologically nilpotent elements is radical.

public lemma topologicalNilradical_isRadical {B : Type*} [CommRing B] [TopologicalSpace B]
    [IsLinearTopology B B] :
    (topologicalNilradical B).IsRadical

TopologicalRing.closure_map_le_topologicalNilradical, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 150. The attribute's comment: “part (2)”. References: SGA 3 VIIB (0.1.3), “r(A) ↦ r(B)”.

Extending an ideal consisting of topologically nilpotent elements along a continuous ring homomorphism and taking its closure still gives an ideal consisting of topologically nilpotent elements.

public lemma closure_map_le_topologicalNilradical
    {A B : Type*} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B]
    [IsLinearTopology A A] [IsTopologicalRing B] [IsLinearTopology B B]
    (φ : A →+* B) (hφ : Continuous φ)
    (I : Ideal A) (hI : I ≤ topologicalNilradical A) :
    Ideal.closure (I.map φ) ≤ topologicalNilradical B

Declarations registered for the tag:

topologicalNilradical registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 97 (StacksFrontier): “the ideal”. References: EGA 0 (7.1.3); EGA 0 (7.1.6).
IsTopologicallyNilpotent.map registered with add_to_stacks in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdmissible.lean, line 143 (StacksFrontier): “part (1)”. References: SGA 3 VIIB (0.1.3), “more general”.

Tag 0AMZ, a lemma

Tag 0AMZ in the Stacks Project.

TopologicalRing.closure_map_eq_ker_completedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletedTensorProduct.lean, line 1146.

The closure of the extension of I to B is the kernel of the canonical map B → B ⊗̂[A] (A ⧸ I).

public theorem closure_map_eq_ker_completedTensorProduct
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
    [TopologicalSpace A] [TopologicalSpace B]
    [IsTopologicalRing A] [IsTopologicalRing B]
    [IsLinearTopology A A] [IsLinearTopology B B]
    (h : Continuous (algebraMap A B)) (I : Ideal A) :
    (Ideal.closure (I.map (algebraMap A B)) : Set B) =
      {b : B | (↑(b ⊗ₜ[A] (1 : A ⧸ I)) :
        TopologicalRing.CompletedTensorProduct (R := A) (M := B) (N := A ⧸ I)) = 0}

Tag 0GB4, a lemma

Tag 0GB4 in the Stacks Project.

TopologicalRing.isAdicStar_completedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicStarBaseChange.lean, line 84. The attribute's comment: “the adic_finite clauses, assembled as membership in WAdm^{adic*}”.

The completed tensor product of two objects of WAdm^{adic*} over a third is again an object of WAdm^{adic*}: it is adic and it has a finitely generated ideal of definition.

theorem isAdicStar_completedTensorProduct {A₀ A₁ A : Type u}
    [CommRing A₀] [TopologicalSpace A₀] [IsTopologicalRing A₀] [IsLinearTopology A₀ A₀]
    [CommRing A₁] [TopologicalSpace A₁] [IsTopologicalRing A₁] [IsLinearTopology A₁ A₁]
    [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [Algebra A₀ A₁] [Algebra A₀ A]
    (h₁ : IsAdicStar A₁) (hA : IsAdicStar A)
    (hc₁ : Continuous (algebraMap A₀ A₁)) (hcA : Continuous (algebraMap A₀ A)) :
    IsAdicStar (CompletedTensorProduct (R := A₀) (M := A₁) (N := A))

TopologicalRing.isCountablyWeaklyAdmissible_completedTensorProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedBaseChange.lean, line 73. The attribute's comment: “the weakly_admissible and countable_basis clauses, assembled as membership in WAdm^count”.

Lemma 87.4.12 (Stacks 0GB4) on the class WAdm^count. The completed tensor product of two countably indexed weakly admissible topological rings over a third is again one: it is weakly admissible and its fundamental system of neighbourhoods of zero is countable.

This is the well definedness that the notion of stability under base change of Stacks 0GBC needs, and it is what the chart argument of Stacks 0GBD needs of the class beyond the stability clause itself, in order to transport P along the isomorphism identifying the chart ring of a fibre product of charts with the completed tensor product.

public theorem isCountablyWeaklyAdmissible_completedTensorProduct {A₀ A₁ A : Type u}
    [CommRing A₀] [TopologicalSpace A₀] [IsTopologicalRing A₀] [IsLinearTopology A₀ A₀]
    [CommRing A₁] [TopologicalSpace A₁] [IsTopologicalRing A₁] [IsLinearTopology A₁ A₁]
    [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [Algebra A₀ A₁] [Algebra A₀ A]
    (h₁ : IsCountablyWeaklyAdmissible A₁) (hA : IsCountablyWeaklyAdmissible A) :
    IsCountablyWeaklyAdmissible
      (CompletedTensorProduct (R := A₀) (M := A₁) (N := A))

TopologicalRing.completedTensorProduct_isAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletedTensorProduct/Adic.lean, line 364. The attribute's comment: “adic_finite”.

The completed tensor product of two pre-adic, linearly topologized algebras with finitely generated ideals of definition is adic.

public theorem completedTensorProduct_isAdic
    {B A C : Type*} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing C] [TopologicalSpace C] [IsTopologicalRing C]
    [IsLinearTopology C C] [Algebra B A] [Algebra B C]
    (_hBA : Continuous (algebraMap B A)) (_hBC : Continuous (algebraMap B C))
    (_hA : TopologicalRing.IsPreAdic A)
    (_hAfg : ∃ I : Ideal A, TopologicalRing.IsIdealOfDefinition I ∧ I.FG)
    (_hC : TopologicalRing.IsPreAdic C)
    (_hCfg : ∃ J : Ideal C, TopologicalRing.IsIdealOfDefinition J ∧ J.FG) :
    TopologicalRing.IsAdic (CompletedTensorProduct (R := B) (M := A) (N := C))

TopologicalRing.exists_fg_ideal_of_definition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletedTensorProduct/Adic.lean, line 383. The attribute's comment: “adic_finite”.

The completed tensor product has a finitely generated ideal of definition.

public theorem exists_fg_ideal_of_definition
    {B A C : Type*} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing C] [TopologicalSpace C] [IsTopologicalRing C]
    [IsLinearTopology C C] [Algebra B A] [Algebra B C]
    (_hBA : Continuous (algebraMap B A)) (_hBC : Continuous (algebraMap B C))
    (_hA : TopologicalRing.IsPreAdic A)
    (_hAfg : ∃ I : Ideal A, TopologicalRing.IsIdealOfDefinition I ∧ I.FG)
    (_hC : TopologicalRing.IsPreAdic C)
    (_hCfg : ∃ J : Ideal C, TopologicalRing.IsIdealOfDefinition J ∧ J.FG) :
    ∃ K : Ideal (CompletedTensorProduct (R := B) (M := A) (N := C)),
      K.FG ∧ TopologicalRing.IsIdealOfDefinition K

TopologicalRing.completedTensorProduct_isNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletedTensorProduct/Adic.lean, line 654. The attribute's comment: “adic_noetherian”.

If the induced quotient map is of finite type, the completed tensor product of pre-adic Noetherian algebras is Noetherian.

public theorem completedTensorProduct_isNoetherianRing
    {B A C : Type*} [CommRing B] [CommRing A] [CommRing C]
    [Algebra B A] [Algebra B C]
    [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
    [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [TopologicalSpace C] [IsTopologicalRing C] [IsLinearTopology C C]
    (hBA : Continuous (algebraMap B A)) (hBC : Continuous (algebraMap B C))
    [IsNoetherianRing A] [IsNoetherianRing C]
    (hA : TopologicalRing.IsPreAdic A) (hC : TopologicalRing.IsPreAdic C)
    (hFinite : ∃ h : topologicalNilradical B ≤
        (topologicalNilradical A).comap (algebraMap B A),
      (Ideal.quotientMap (topologicalNilradical A) (algebraMap B A) h).FiniteType) :
    IsNoetherianRing (CompletedTensorProduct (R := B) (M := A) (N := C))

TopologicalRing.completedTensorProduct_isAdmissible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletedTensorProduct/Adic.lean, line 815. The attribute's comment: “admissible”. References: EGA 0 (7.7.7), “admissibility”.

The completed tensor product of pre-admissible linearly topologized algebras is admissible.

public theorem completedTensorProduct_isAdmissible
    {B A C : Type*} [CommRing B] [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing C] [TopologicalSpace C]
    [IsTopologicalRing C] [IsLinearTopology C C]
    [Algebra B A] [Algebra B C]
    (hA : TopologicalRing.IsPreAdmissible A)
    (hC : TopologicalRing.IsPreAdmissible C) :
    TopologicalRing.IsAdmissible
      (TopologicalRing.CompletedTensorProduct (R := B) (M := A) (N := C))

TopologicalRing.isCountablyGenerated_nhds_zero_completedTensorProduct, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletedTensorProduct/Adic.lean, line 922. The attribute's comment: “countable_basis”.

The completed tensor product of two linearly topologized rings with countable fundamental systems of open ideals has a countable fundamental system of open ideals.

public lemma isCountablyGenerated_nhds_zero_completedTensorProduct
    {B A C : Type*} [CommRing B] [CommRing A] [CommRing C]
    [Algebra B A] [Algebra B C]
    [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [TopologicalSpace C] [IsTopologicalRing C] [IsLinearTopology C C]
    (hA : (nhds (0 : A)).IsCountablyGenerated)
    (hC : (nhds (0 : C)).IsCountablyGenerated) :
    (nhds
      (0 : TopologicalRing.CompletedTensorProduct (R := B) (M := A) (N := C))).IsCountablyGenerated

TopologicalRing.completedTensorProduct_isWeaklyAdmissible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletedTensorProduct/Adic.lean, line 951. The attribute's comment: “weakly_admissible”.

The completed tensor product of two weakly pre-admissible linearly topologized rings is weakly admissible.

public theorem completedTensorProduct_isWeaklyAdmissible
    {B A C : Type*} [CommRing B] [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing C] [TopologicalSpace C]
    [IsTopologicalRing C] [IsLinearTopology C C]
    [Algebra B A] [Algebra B C]
    (hA : TopologicalRing.IsWeaklyPreAdmissible A)
    (hC : TopologicalRing.IsWeaklyPreAdmissible C) :
    TopologicalRing.IsWeaklyAdmissible
      (TopologicalRing.CompletedTensorProduct (R := B) (M := A) (N := C))

TopologicalRing.projectionKernel_isWeakIdealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/CompletedTensorProduct/WeakIdeal.lean, line 157. The attribute's comment: “the projection kernels as weak ideals of definition”.

The projection kernel cut out by two weak ideals of definition is a weak ideal of definition of the completed tensor product. It is open by TopologicalRing.isOpen_projectionKernel, and it consists of topologically nilpotent elements because it is the closure of the sum of the two extended ideals.

public theorem projectionKernel_isWeakIdealOfDefinition (i : ι) (j : κ)
    (hI : TopologicalRing.IsWeakIdealOfDefinition (I i))
    (hJ : TopologicalRing.IsWeakIdealOfDefinition (J j)) :
    TopologicalRing.IsWeakIdealOfDefinition
      (projectionKernel (B := B) I J bI bJ i j)

Sources

LeanTopologicalModule.Nonuniform.exists_pow_X_smul_mem · TopologicalModule.Nonuniform.not_exists_forall_pow_X_smul_mem · TopologicalModule.Nonuniform.exists_isLinearTopology_not_exists_isOpen_ideal_smul_mem · TopologicalModule.continuousSMul_iff_forall_exists_smul_mem · TopologicalModule.continuousSMul_iff_forall_exists_coset_smul_coset · TopologicalRing.continuous_add_of_hasBasis_addSubgroup · TopologicalRing.exists_isOpen_ideal_map_le · TopologicalRing.closure_eq_iInter_sup_of_hasBasis

Section87.5 Taut ring maps #

Section 87.5 of the Stacks Project, Tag 0GX1. 10 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AMX, a definition

Tag 0AMX in the Stacks Project.

RingHom.IsTaut, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Taut.lean, line 53.

A ring homomorphism is taut if the closure of the extension of each open source ideal is open, and the resulting closed extended ideals form a neighbourhood basis of zero in the target.

For the Stacks definition, the source and target are linearly topologized rings and the homomorphism is continuous; those ambient hypotheses are imposed by statements using this predicate.

public abbrev IsTaut {A B : Type*} [CommRing A] [TopologicalSpace A]
    [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] (φ : A →+* B) : Prop

Tag 0AMY, a lemma

Tag 0AMY in the Stacks Project.

RingHom.isTaut_iff_hasBasis_isWeakIdealOfDefinition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Taut.lean, line 80.

A continuous homomorphism of weakly admissible topological rings is taut exactly when the closed extensions of the weak ideals of definition are weak ideals of definition and form a neighbourhood basis of zero in the target.

public theorem isTaut_iff_hasBasis_isWeakIdealOfDefinition
    {A B : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] (φ : A →+* B) (hφ : Continuous φ)
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hB : TopologicalRing.IsWeaklyAdmissible B) :
    RingHom.IsTaut φ ↔
      (∀ I : Ideal A, TopologicalRing.IsWeakIdealOfDefinition I →
        TopologicalRing.IsWeakIdealOfDefinition (Ideal.closure (I.map φ))) ∧
      (nhds (0 : B)).HasBasis
        (fun I : Ideal A ↦ TopologicalRing.IsWeakIdealOfDefinition I)
        (fun I : Ideal A ↦ (Ideal.closure (I.map φ) : Set B))

Tag 0GX2, a lemma

Tag 0GX2 in the Stacks Project.

RingHom.isTaut_completion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Taut.lean, line 352.

The canonical map from a linearly topologized ring to its completion is taut.

public theorem isTaut_completion {A : Type*} [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A] [IsLinearTopology A A] :
    letI : UniformSpace A := IsTopologicalAddGroup.rightUniformSpace A
    letI : IsUniformAddGroup A := isUniformAddGroup_of_addCommGroup
    RingHom.IsTaut (UniformSpace.Completion.coeRingHom :
      A →+* UniformSpace.Completion A)

Tag 0GX3, a lemma

Tag 0GX3 in the Stacks Project.

RingHom.isTaut_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Taut.lean, line 400.

The composite of continuous taut homomorphisms of linearly topologized rings is taut.

public lemma isTaut_comp {A B C : Type*}
    [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
    [CommRing C] [TopologicalSpace C] [IsTopologicalRing C] [IsLinearTopology C C]
    (φ : A →+* B) (ψ : B →+* C) (hφ : Continuous φ) (hψ : Continuous ψ)
    (hφ_taut : RingHom.IsTaut φ) (hψ_taut : RingHom.IsTaut ψ) :
    RingHom.IsTaut (ψ.comp φ)

Tag 0GX4, a lemma

Tag 0GX4 in the Stacks Project.

RingHom.isTaut_of_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Taut.lean, line 434.

If a composite of two continuous ring homomorphisms is taut, then its second map is taut.

public lemma isTaut_of_comp {A B C : Type*}
    [CommRing A] [TopologicalSpace A]
    [CommRing B] [TopologicalSpace B]
    [CommRing C] [TopologicalSpace C] [IsTopologicalRing C]
    (φ : A →+* B) (ψ : B →+* C) (hφ : Continuous φ) (hψ : Continuous ψ)
    (hcomp : RingHom.IsTaut (ψ.comp φ)) : RingHom.IsTaut ψ

Tag 0GX5, a lemma

Tag 0GX5 in the Stacks Project.

RingHom.isTaut_completedTensorProduct_baseChange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/TautTensor.lean, line 115.

Completed tensor-product base change preserves a taut homomorphism.

public lemma isTaut_completedTensorProduct_baseChange
    {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
    [Algebra A B] [Algebra A C]
    [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
    [TopologicalSpace C] [IsTopologicalRing C] [IsLinearTopology C C]
    (_hB : Continuous (algebraMap A B)) (hC : Continuous (algebraMap A C))
    (hTaut : RingHom.IsTaut (algebraMap A B)) :
    letI : Algebra C (B ⊗[A] C) := Algebra.TensorProduct.rightAlgebra
    RingHom.IsTaut
      (algebraMap C (TopologicalRing.CompletedTensorProduct (R := A) (M := B) (N := C)))

Tag 0GX6, a lemma

Tag 0GX6 in the Stacks Project.

RingHom.isCountablyGenerated_nhds_zero_of_isTaut, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Taut.lean, line 467.

The target of a taut continuous homomorphism of linearly topologized rings has a countable fundamental system of open ideals if the source does.

public lemma isCountablyGenerated_nhds_zero_of_isTaut
    {A B : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] (φ : A →+* B) (hφ : Continuous φ)
    (hφ_taut : RingHom.IsTaut φ) (hA : (nhds (0 : A)).IsCountablyGenerated) :
    (nhds (0 : B)).IsCountablyGenerated

Tag 0GX7, a lemma

Tag 0GX7 in the Stacks Project.

RingHom.isWeaklyPreAdmissible_of_isTaut, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Taut.lean, line 489.

Weak pre-admissibility ascends along a continuous taut homomorphism of linearly topologized rings.

public lemma isWeaklyPreAdmissible_of_isTaut
    {A B : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] (φ : A →+* B) (hφ : Continuous φ)
    (hφ_taut : RingHom.IsTaut φ) (hA : TopologicalRing.IsWeaklyPreAdmissible A) :
    TopologicalRing.IsWeaklyPreAdmissible B

Tag 0GX8, a lemma

Tag 0GX8 in the Stacks Project.

RingHom.isPreAdmissible_of_isTaut, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Taut.lean, line 525.

Pre-admissibility ascends along a continuous taut homomorphism of linearly topologized rings.

public lemma isPreAdmissible_of_isTaut {A : Type u} {B : Type v} [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A] [IsLinearTopology A A] [CommRing B] [TopologicalSpace B]
    [IsTopologicalRing B] [IsLinearTopology B B] (φ : A →+* B) (hφ : Continuous φ)
    (hφ_taut : RingHom.IsTaut φ) (hA : TopologicalRing.IsPreAdmissible A) :
    TopologicalRing.IsPreAdmissible B

Tag 0APT, a lemma

Tag 0APT in the Stacks Project.

RingHom.isOpenMap_of_isTaut_of_denseRange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Taut.lean, line 284. The attribute's comment: “openness”.

A continuous taut map with dense image from a complete countably based linearly topologized ring to a separated linearly topologized ring is open.

public lemma isOpenMap_of_isTaut_of_denseRange (φ : A →+* B) (hφ : Continuous φ)
    (hA : @CompleteSpace A (IsTopologicalAddGroup.rightUniformSpace A))
    (hcount : (nhds (0 : A)).IsCountablyGenerated) (htaut : RingHom.IsTaut φ)
    (hdense : DenseRange φ) : IsOpenMap φ

RingHom.surjective_of_isTaut_of_denseRange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Taut.lean, line 293. The attribute's comment: “surjectivity”.

A continuous taut map with dense image under the completeness and countability hypotheses is surjective.

public lemma surjective_of_isTaut_of_denseRange (φ : A →+* B) (hφ : Continuous φ)
    (hA : @CompleteSpace A (IsTopologicalAddGroup.rightUniformSpace A))
    (hcount : (nhds (0 : A)).IsCountablyGenerated) (htaut : RingHom.IsTaut φ)
    (hdense : DenseRange φ) : Function.Surjective φ

RingHom.completeSpace_of_isTaut_of_denseRange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Taut.lean, line 309. The attribute's comment: “completeness of the target”.

The separated target of a continuous taut dense map from a complete countably based linearly topologized ring is complete.

public lemma completeSpace_of_isTaut_of_denseRange (φ : A →+* B) (hφ : Continuous φ)
    (hA : @CompleteSpace A (IsTopologicalAddGroup.rightUniformSpace A))
    (hcount : (nhds (0 : A)).IsCountablyGenerated) (htaut : RingHom.IsTaut φ)
    (hdense : DenseRange φ) :
    @CompleteSpace B (IsTopologicalAddGroup.rightUniformSpace B)

RingHom.isClosed_ker_of_continuous, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Taut.lean, line 323. The attribute's comment: “closed kernel”.

The kernel of a continuous ring homomorphism into a space with closed points is closed.

public lemma isClosed_ker_of_continuous {R S : Type*} [CommRing R] [TopologicalSpace R]
    [CommRing S] [TopologicalSpace S] [T1Space S] (φ : R →+* S) (hφ : Continuous φ) :
    IsClosed (RingHom.ker φ : Set R)

RingHom.quotientKerEquiv_of_isTaut_of_denseRange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Taut.lean, line 332. The attribute's comment: “quotient presentation”.

The canonical map from the quotient by the kernel to the target is a homeomorphic ring equivalence.

public lemma quotientKerEquiv_of_isTaut_of_denseRange (φ : A →+* B) (hφ : Continuous φ)
    (hA : @CompleteSpace A (IsTopologicalAddGroup.rightUniformSpace A))
    (hcount : (nhds (0 : A)).IsCountablyGenerated) (htaut : RingHom.IsTaut φ)
    (hdense : DenseRange φ) :
    ∃ e : (A ⧸ RingHom.ker φ) ≃+* B,
      (∀ a : A, e (Ideal.Quotient.mk (RingHom.ker φ) a) = φ a) ∧ IsHomeomorph e

Sources

LeanRingHom.IsTaut · RingHom.isTaut_iff_hasBasis_isWeakIdealOfDefinition · RingHom.isTaut_completion · RingHom.isTaut_comp · RingHom.isTaut_of_comp · RingHom.isTaut_completedTensorProduct_baseChange · RingHom.isCountablyGenerated_nhds_zero_of_isTaut · RingHom.isWeaklyPreAdmissible_of_isTaut

Section87.6 Adic ring maps #

Section 87.6 of the Stacks Project, Tag 0GX9. 5 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GBR, a definition

Tag 0GBR in the Stacks Project.

RingHom.IsAdic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicRingMap.lean, line 44.

A ring homomorphism φ : A →+* B is adic if some ideal defining the topology of A extends along φ to an ideal defining the topology of B.

public abbrev IsAdic {A B : Type*} [CommRing A] [CommRing B]
    [TopologicalSpace A] [TopologicalSpace B] (φ : A →+* B) : Prop

Tag 0GXA, a lemma

Tag 0GXA in the Stacks Project.

RingHom.isAdic_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicRingMap.lean, line 362.

The composite of two continuous adic ring homomorphisms is adic.

public theorem isAdic_comp {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
    [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C]
    (f : A →+* B) (g : B →+* C) (hf_continuous : Continuous f)
    (hg_continuous : Continuous g) (hf : RingHom.IsAdic f)
    (hg : RingHom.IsAdic g) :
    RingHom.IsAdic (g.comp f)

Tag 0GXB, a lemma

Tag 0GXB in the Stacks Project.

RingHom.isAdic_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicRingMap.lean, line 384.

If a composite of continuous ring homomorphisms is adic and the middle ring is pre-adic, then the second homomorphism is adic.

public theorem isAdic_of_comp {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
    [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C]
    (f : A →+* B) (g : B →+* C) (hf_continuous : Continuous f)
    (hg_continuous : Continuous g) (hB : TopologicalRing.IsPreAdic B)
    (hgf : RingHom.IsAdic (g.comp f)) :
    RingHom.IsAdic g

Tag 0GXC, a lemma

Tag 0GXC in the Stacks Project.

RingHom.isTaut_of_isAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicRingMap.lean, line 436. The attribute's comment: “adic implies taut”.

A continuous adic homomorphism of linearly topologized rings is taut.

public theorem isTaut_of_isAdic
    {A B : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B]
    (φ : A →+* B) (hφ : Continuous φ) (hAdic : RingHom.IsAdic φ) :
    RingHom.IsTaut φ

Tag 0APU, a lemma

Tag 0APU in the Stacks Project.

RingHom.exists_fg_ideal_isAdic_of_isTaut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicRingMap.lean, line 306. The attribute's comment: “the target is adic with a finitely generated ideal of definition”.

The target of a taut continuous homomorphism from a pre-adic ring with a finitely generated ideal of definition is itself adic with a finitely generated ideal of definition, provided that the target is complete.

public theorem exists_fg_ideal_isAdic_of_isTaut
    {A B : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B]
    (φ : A →+* B) (hφ : Continuous φ) (hTaut : RingHom.IsTaut φ)
    (hA : ∃ I : Ideal A, I.FG ∧ _root_.IsAdic I)
    [@CompleteSpace B (IsTopologicalAddGroup.rightUniformSpace B)] [T2Space B] :
    ∃ J : Ideal B, J.FG ∧ _root_.IsAdic J

RingHom.isAdic_of_isTaut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/AdicRingMap.lean, line 322. The attribute's comment: “the homomorphism is adic”.

A taut continuous homomorphism from a pre-adic ring with a finitely generated ideal of definition to a complete linearly topologized ring is adic.

public theorem isAdic_of_isTaut
    {A B : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B]
    (φ : A →+* B) (hφ : Continuous φ) (hTaut : RingHom.IsTaut φ)
    (hA : ∃ I : Ideal A, I.FG ∧ _root_.IsAdic I)
    [@CompleteSpace B (IsTopologicalAddGroup.rightUniformSpace B)] [T2Space B] :
    RingHom.IsAdic φ

Sources

LeanRingHom.IsAdic · RingHom.isAdic_comp · RingHom.isAdic_of_comp · RingHom.isTaut_of_isAdic · RingHom.exists_fg_ideal_isAdic_of_isTaut · RingHom.isAdic_of_isTaut

Section87.7 Weakly adic rings #

Section 87.7 of the Stacks Project, Tag 0GXD. 6 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GXE, a definition

Tag 0GXE in the Stacks Project.

TopologicalRing.IsWeaklyPreAdic, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdic.lean, line 46. The attribute's comment: “part (1)”.

A linearly topologized ring is weakly pre-adic if the closures of the powers of some ideal are open and form a neighborhood basis at zero.

public class IsWeaklyPreAdic (A : Type*) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] : Prop

TopologicalRing.IsWeaklyAdic, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdic.lean, line 55. The attribute's comment: “part (2)”.

A linearly topologized ring is weakly adic if it is weakly pre-adic, complete, and separated. Completeness uses the canonical uniformity of its additive topological group.

public class IsWeaklyAdic (A : Type*) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] : Prop extends IsWeaklyPreAdic A, T2Space A

Tag 0GXF, a lemma

Tag 0GXF in the Stacks Project.

TopologicalRing.weaklyPreAdic_tfae, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdic.lean, line 118. The attribute's comment: “weakly_pre_adic_characterizations”.

The four equivalent characterizations of a weakly pre-adic linearly topologized ring.

public lemma weaklyPreAdic_tfae (A : Type u) [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A] [IsLinearTopology A A] :
    List.TFAE
      [ TopologicalRing.IsWeaklyPreAdic A,
        HasTautPreAdicSource.{u, max u v} A,
        TopologicalRing.IsPreAdmissible A ∧
          ∃ I : Ideal A, TopologicalRing.IsIdealOfDefinition I ∧
            (∀ n : ℕ, 1 ≤ n → IsOpen ((I ^ n).topologicalClosure : Set A)),
        TopologicalRing.IsPreAdmissible A ∧
          (∀ I : Ideal A, TopologicalRing.IsIdealOfDefinition I →
            ∀ n : ℕ, 1 ≤ n → IsOpen ((I ^ n).topologicalClosure : Set A)) ]

TopologicalRing.isLinearTopology_completion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdic.lean, line 284. The attribute's comment: “completion_weakly_adic”.

Completion preserves the linear topology of a linearly topologized ring.

public instance isLinearTopology_completion (A : Type*) [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A] [IsLinearTopology A A] :
    letI : UniformSpace A := IsTopologicalAddGroup.rightUniformSpace A
    letI : IsUniformAddGroup A := isUniformAddGroup_of_addCommGroup
    IsLinearTopology (UniformSpace.Completion A) (UniformSpace.Completion A)

TopologicalRing.isWeaklyAdic_completion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdic.lean, line 295. The attribute's comment: “completion_weakly_adic”.

The completion of a weakly pre-adic linearly topologized ring is weakly adic.

public instance isWeaklyAdic_completion (A : Type*) [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A] [IsLinearTopology A A] [TopologicalRing.IsWeaklyPreAdic A] :
    letI : UniformSpace A := IsTopologicalAddGroup.rightUniformSpace A
    letI : IsUniformAddGroup A := isUniformAddGroup_of_addCommGroup
    TopologicalRing.IsWeaklyAdic (UniformSpace.Completion A)

TopologicalRing.isAdmissible_of_isWeaklyAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdic.lean, line 354. The attribute's comment: “weakly_adic_admissible”.

A weakly adic linearly topologized ring is admissible.

public theorem isAdmissible_of_isWeaklyAdic (A : Type*) [CommRing A]
    [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [TopologicalRing.IsWeaklyAdic A] : TopologicalRing.IsAdmissible A

TopologicalRing.exists_countable_basis_open_ideals, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdic.lean, line 371. The attribute's comment: “weakly_adic_countable_basis”.

A weakly adic linearly topologized ring has a countable fundamental system of open ideals.

public theorem exists_countable_basis_open_ideals (A : Type*) [CommRing A]
    [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    [TopologicalRing.IsWeaklyAdic A] :
    ∃ I : ℕ → Ideal A, (∀ n : ℕ, IsOpen (I n : Set A)) ∧
      (𝓝 (0 : A)).HasBasis (fun _ : ℕ ↦ True) (fun n ↦ (I n : Set A))

Tag 0GXG, a lemma

Tag 0GXG in the Stacks Project.

TopologicalRing.exists_fg_isAdic_of_fg_closure_powers_basis, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdic.lean, line 641.

A complete linearly topologized ring whose topology is the fundamental system given by the closures of the powers of a finitely generated ideal is adic with a finitely generated ideal of definition.

public lemma exists_fg_isAdic_of_fg_closure_powers_basis
    {A : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [T2Space A]
    [hcomplete : @CompleteSpace A (IsTopologicalAddGroup.rightUniformSpace A)]
    (I : Ideal A) (hIfg : I.FG)
    (hopen : ∀ n : ℕ, IsOpen ((I ^ n).topologicalClosure : Set A))
    (hbasis : (𝓝 (0 : A)).HasBasis (fun _ : ℕ ↦ True)
      (fun n ↦ ((I ^ n).topologicalClosure : Set A))) :
    ∃ J : Ideal A, J.FG ∧ _root_.IsAdic J

Tag 0GXH, a lemma

Tag 0GXH in the Stacks Project.

TopologicalRing.exists_fg_isAdic_of_quotient_closure_sq_finite, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdic.lean, line 701.

A weakly adic ring with an ideal of definition I for which I / closure(I ^ 2) is finite has a finitely generated ideal defining its topology.

public lemma exists_fg_isAdic_of_quotient_closure_sq_finite
    {A : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [TopologicalRing.IsWeaklyAdic A]
    (I : Ideal A) (hI : TopologicalRing.IsIdealOfDefinition I)
    [Module.Finite A
      (I ⧸ Submodule.comap I.subtype (I ^ 2).topologicalClosure)] :
    ∃ J : Ideal A, J.FG ∧ _root_.IsAdic J

Tag 0GXI, a lemma

Tag 0GXI in the Stacks Project.

TopologicalRing.isWeaklyPreAdic_of_isTaut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdic.lean, line 724.

The target of a continuous taut homomorphism from a weakly pre-adic linearly topologized ring is weakly pre-adic.

public theorem isWeaklyPreAdic_of_isTaut {A B : Type*} [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A] [IsLinearTopology A A] [CommRing B] [TopologicalSpace B]
    [IsTopologicalRing B] [IsLinearTopology B B] (φ : A →+* B) (hφ : Continuous φ)
    [TopologicalRing.IsWeaklyPreAdic A] (hφ_taut : RingHom.IsTaut φ) :
    TopologicalRing.IsWeaklyPreAdic B

Tag 0GXJ, a lemma

Tag 0GXJ in the Stacks Project.

TopologicalRing.completedTensorProduct_isWeaklyAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/WeaklyAdic.lean, line 778.

The completed tensor product of weakly pre-adic linearly topologized rings over a commutative ring is weakly adic.

public theorem completedTensorProduct_isWeaklyAdic
    {B A C : Type*} [CommRing B] [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing C] [TopologicalSpace C] [IsTopologicalRing C]
    [IsLinearTopology C C] [Algebra B A] [Algebra B C]
    (hA : TopologicalRing.IsWeaklyPreAdic A) (hC : TopologicalRing.IsWeaklyPreAdic C) :
    TopologicalRing.IsWeaklyAdic
      (TopologicalRing.CompletedTensorProduct (R := B) (M := A) (N := C))

Sources

LeanTopologicalRing.IsWeaklyPreAdic · TopologicalRing.IsWeaklyAdic · TopologicalRing.weaklyPreAdic_tfae · TopologicalRing.isLinearTopology_completion · TopologicalRing.isWeaklyAdic_completion · TopologicalRing.isAdmissible_of_isWeaklyAdic · TopologicalRing.exists_countable_basis_open_ideals · TopologicalRing.exists_fg_isAdic_of_fg_closure_powers_basis

Section87.8 Descending properties #

Section 87.8 of the Stacks Project, Tag 0GXK. 5 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GXL, a lemma

Tag 0GXL in the Stacks Project.

TopologicalRing.isCountablyGenerated_nhds_zero_of_isTaut_of_faithfullyFlat_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Descent.lean, line 74.

A countable fundamental system of open ideals descends along a continuous taut map whose induced maps on quotients by open ideals are faithfully flat.

public theorem isCountablyGenerated_nhds_zero_of_isTaut_of_faithfullyFlat_quotient
    {A : Type u} {B : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] (φ : A →+* B) (hφ : Continuous φ)
    (hφ_taut : RingHom.IsTaut φ)
    (hφ_quotient : ∀ (I : Ideal A), IsOpen (I : Set A) →
      (Ideal.quotientMap (Ideal.closure (I.map φ)) φ
        (Ideal.map_le_iff_le_comap.mp (fun _ hx ↦ subset_closure hx))).FaithfullyFlat)
    (hB : (nhds (0 : B)).IsCountablyGenerated) :
    (nhds (0 : A)).IsCountablyGenerated

Tag 0GXM, a lemma

Tag 0GXM in the Stacks Project.

TopologicalRing.isWeaklyPreAdmissible_of_isTaut_of_faithfullyFlat_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Descent.lean, line 114.

Weak pre-admissibility descends along a taut map when the induced maps on quotients by open ideals and their closed extensions are faithfully flat.

public theorem isWeaklyPreAdmissible_of_isTaut_of_faithfullyFlat_quotient
    {A : Type u} {B : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    (φ : A →+* B)
    (hφ_taut : RingHom.IsTaut φ)
    (hφ_quotient : ∀ I : Ideal A, IsOpen (I : Set A) →
      (Ideal.quotientMap (I := I) (Ideal.closure (I.map φ)) φ (by
        exact Ideal.map_le_iff_le_comap.mp
          (show I.map φ ≤ Ideal.closure (I.map φ) from
            fun _ hx ↦ subset_closure hx))).FaithfullyFlat)
    (hB : TopologicalRing.IsWeaklyPreAdmissible B) :
    TopologicalRing.IsWeaklyPreAdmissible A

Tag 0GXN, a lemma

Tag 0GXN in the Stacks Project.

TopologicalRing.isPreAdmissible_of_isTaut_of_faithfullyFlat_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Descent.lean, line 150.

Pre-admissibility descends along a continuous taut homomorphism when all of the induced maps on quotients by open ideals and their closed extensions are faithfully flat.

public theorem isPreAdmissible_of_isTaut_of_faithfullyFlat_quotient
    {A : Type u} {B : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] (φ : A →+* B) (hφ : Continuous φ) (hφ_taut : RingHom.IsTaut φ)
    (hφ_quotient : ∀ (I : Ideal A), IsOpen (I : Set A) →
      (Ideal.quotientMap (Ideal.closure (I.map φ)) φ
        (Ideal.map_le_iff_le_comap.mp (fun _ hx ↦ subset_closure hx))).FaithfullyFlat)
    (hB : TopologicalRing.IsPreAdmissible B) :
    TopologicalRing.IsPreAdmissible A

Tag 0GXP, a lemma

Tag 0GXP in the Stacks Project.

TopologicalRing.isWeaklyPreAdic_of_isTaut_of_faithfullyFlat_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Descent.lean, line 255.

Weak pre-adicness descends along a continuous taut homomorphism when all maps on the corresponding quotients by open ideals are faithfully flat.

public theorem isWeaklyPreAdic_of_isTaut_of_faithfullyFlat_quotient
    {A : Type u} {B : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A] [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] (φ : A →+* B) (hφ : Continuous φ) (hφ_taut : RingHom.IsTaut φ)
    (hquot : ∀ I : Ideal A, IsOpen (I : Set A) →
      (Ideal.quotientMap (I := I) (Ideal.closure (I.map φ)) φ (by
        exact Ideal.map_le_iff_le_comap.mp
          (show I.map φ ≤ Ideal.closure (I.map φ) from
            fun _ hx ↦ subset_closure hx))).FaithfullyFlat)
    (hB : TopologicalRing.IsWeaklyPreAdic B) : TopologicalRing.IsWeaklyPreAdic A

Tag 0GXQ, a lemma

Tag 0GXQ in the Stacks Project.

TopologicalRing.exists_fg_ideal_of_definition_of_taut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/Descent.lean, line 476.

Adicness with a finitely generated ideal of definition descends along a continuous taut homomorphism when all the induced maps modulo open ideals are faithfully flat.

public theorem exists_fg_ideal_of_definition_of_taut
    {A B : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [IsLinearTopology A A]
    [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsLinearTopology B B]
    [@CompleteSpace A (IsTopologicalAddGroup.rightUniformSpace A)] [T2Space A]
    [@CompleteSpace B (IsTopologicalAddGroup.rightUniformSpace B)] [T2Space B]
    (φ : A →+* B) (_hφ : Continuous φ) (_htaut : RingHom.IsTaut φ)
    (_hquot : ∀ I : Ideal A, IsOpen (I : Set A) →
      (Ideal.quotientMap (Ideal.closure (I.map φ)) φ
        (Ideal.le_comap_of_map_le
          (show I.map φ ≤ Ideal.closure (I.map φ) from subset_closure))).FaithfullyFlat)
    (_hB : ∃ J : Ideal B, _root_.IsAdic J ∧ J.FG) :
    ∃ I : Ideal A, _root_.IsAdic I ∧ I.FG

Sources

LeanTopologicalRing.isCountablyGenerated_nhds_zero_of_isTaut_of_faithfullyFlat_quotient · TopologicalRing.isWeaklyPreAdmissible_of_isTaut_of_faithfullyFlat_quotient · TopologicalRing.isPreAdmissible_of_isTaut_of_faithfullyFlat_quotient · TopologicalRing.isWeaklyPreAdic_of_isTaut_of_faithfullyFlat_quotient · TopologicalRing.exists_fg_ideal_of_definition_of_taut

Section87.9 Affine formal algebraic spaces #

Section 87.9 of the Stacks Project, Tag 0AI6. 11 tags here are carried by 74 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AI7, a definition

Tag 0AI7 in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsAffineFormalAlgebraicSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine.lean, line 85.

An affine formal algebraic space over S is an fppf sheaf on the big fppf site of S which satisfies the set-theoretic condition AlgebraicGeometry.FormalSpace.SatisfiesSetTheoreticCondition and which is the colimit of a directed diagram of affine schemes over S all of whose transition morphisms are thickenings.

abbrev IsAffineFormalAlgebraicSpace (X : FppfSheaf B S hS) : Prop

AlgebraicGeometry.IsAffineFormalAlgebraicSpace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Defs.lean, line 70.

An affine formal algebraic space over S is a sheaf on the big fppf site of S which satisfies the set-theoretic condition and is a directed colimit of sheaves represented by affine schemes whose transition morphisms are thickenings.

abbrev IsAffineFormalAlgebraicSpace (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S)
    (X : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))) : Prop

Tag 0AI8, a lemma

Tag 0AI8 in the Stacks Project.

AlgebraicGeometry.FormalSpace.diagonal_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Diagonal.lean, line 646.

The diagonal of an affine formal algebraic space is representable and a closed immersion.

public theorem diagonal_isClosedImmersion
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type (u + 1)} [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (D : I ⥤ BigAffineFppf B S hS)
    (hD : ∀ ⦃i j : I⦄ (f : i ⟶ j),
      Stacks.Thickenings.IsThickening
        ((BigAffineFppf.toScheme B S hS).map (D.map f)))
    (X : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1)))
    (e : colimit
      (D ⋙ BigAffineFppf.inclusion B S hS ⋙
        Sheaf.sheafifiedYoneda
          (BigFppfOver.topology B S hS)) ≅ X) :
    (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@AlgebraicGeometry.IsClosedImmersion.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) (diag X)

Tag 0AI9, a lemma

Tag 0AI9 in the Stacks Project.

AlgebraicGeometry.FormalSpace.relativelyRepresentable_colimitι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/ThickeningStage.lean, line 300. The attribute's comment: “representability”.

Stacks 0AI9. A stage of a directed presentation of an affine formal algebraic space by affine schemes with thickening transition morphisms maps representably to the colimit: every base change of X_i ⟶ X along a morphism from a represented sheaf is again represented by an object of the site.

theorem relativelyRepresentable_colimitι (i : I) :
    (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
      (colimit.ι
        (D ⋙ BigAffineFppf.inclusion B S hS ⋙
          Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) i ≫ e.hom)

AlgebraicGeometry.FormalSpace.isThickening_colimitι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/ThickeningStage.lean, line 318. The attribute's comment: “thickening”.

Stacks 0AI9. A stage of a directed presentation of an affine formal algebraic space by affine schemes with thickening transition morphisms maps to the colimit by a thickening: the map X_i ⟶ X is representable, and each of its base changes along a represented sheaf is a thickening of schemes.

theorem isThickening_colimitι (i : I) :
    (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)))
      (colimit.ι
        (D ⋙ BigAffineFppf.inclusion B S hS ⋙
          Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) i ≫ e.hom)

Tag 0AIA, a lemma

Tag 0AIA in the Stacks Project.

AlgebraicGeometry.exists_factor_through_thickening', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Factorization.lean, line 189.

A morphism from a quasi-compact algebraic space to a presented affine formal algebraic space factors through one of its affine stages.

Two of the hypotheses of Stacks 0AIA are not asked for, because the argument does not use them. Of the target, only the presentation D, hD, e is used, so the set-theoretic condition of Stacks 0AIS -- the other half of being an affine formal algebraic space, and for a formal spectrum a condition on the size of the site -- is not assumed. Of the transition morphisms of the presentation, only that they are closed immersions is used, not that they are thickenings: surjectivity plays no part. The index of the presentation may lie in any universe, provided it is u + 1-small, the colimit being taken in sheaves of Type (u + 1). Of the source, only the surjective étale cover by a quasi-compact scheme that quasi-compactness provides is used, so Y is not assumed to be an algebraic space.

theorem exists_factor_through_thickening'
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (I : Type w₁) [Preorder I] [Small.{u + 1} I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (D : I ⥤ BigAffineFppf B S hS)
    (hD : ∀ ⦃i j : I⦄ (g : i ⟶ j),
      IsClosedImmersion ((BigAffineFppf.toScheme B S hS).map (D.map g)))
    (X : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1)))
    (e : X ≅ colimit
      (D ⋙ BigAffineFppf.inclusion B S hS ⋙
        Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)))
    (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hYqc : Space.IsQuasiCompactSpace B S hS Y)
    (f : (presheafToSheaf (BigFppfOver.topology B S hS)
      (Type (u + 1))).obj (Y ⋙ uliftFunctor.{u + 1, u}) ⟶ X) :
    ∃ i : I, ∃ g : (presheafToSheaf (BigFppfOver.topology B S hS)
        (Type (u + 1))).obj (Y ⋙ uliftFunctor.{u + 1, u}) ⟶
        (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj
          ((BigAffineFppf.inclusion B S hS).obj (D.obj i)),
      g ≫ colimit.ι
      (D ⋙ BigAffineFppf.inclusion B S hS ⋙
        Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) i ≫
        e.inv = f

Tag 0AIB, a lemma

Tag 0AIB in the Stacks Project.

AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Characterization.lean, line 580.

Stacks 0AIB. A sheaf on the big fppf site of S is an affine formal algebraic space if and only if every morphism to it from a sheaf represented by an affine scheme over S factors through a morphism from an affine scheme over S which is representable and a thickening, and the sheaf satisfies the set-theoretic condition of Stacks 0AIS.

theorem isAffineFormalAlgebraicSpace_iff
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))) :
    IsAffineFormalAlgebraicSpace B S hS X ↔
      ((∀ U : BigAffineFppf B S hS,
          ∀ f : (Sheaf.sheafifiedYoneda
            (BigFppfOver.topology B S hS)).obj
              ((BigAffineFppf.inclusion B S hS).obj U) ⟶ X,
          ∃ T : BigAffineFppf B S hS,
            ∃ g : (Sheaf.sheafifiedYoneda
              (BigFppfOver.topology B S hS)).obj
                ((BigAffineFppf.inclusion B S hS).obj U) ⟶
              (Sheaf.sheafifiedYoneda
                (BigFppfOver.topology B S hS)).obj
                  ((BigAffineFppf.inclusion B S hS).obj T),
            ∃ h : (Sheaf.sheafifiedYoneda
              (BigFppfOver.topology B S hS)).obj
                ((BigAffineFppf.inclusion B S hS).obj T) ⟶ X,
              (Sheaf.sheafifiedYoneda
                (BigFppfOver.topology B S hS)).relativelyRepresentable h ∧
              (MorphismProperty.relative
                (Sheaf.sheafifiedYoneda
                  (BigFppfOver.topology B S hS))
                (MorphismProperty.inverseImage
                  (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})
                  (BigFppfOver.toScheme B S hS))) h ∧
              g ≫ h = f) ∧
        SatisfiesSetTheoreticCondition B S hS X)

Tag 0AIC, a lemma

Tag 0AIC in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_isPresentingRing_of_hasAffineClosedImmersionCriterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionCriterionPresentation.lean, line 77. The attribute's comment: “(2) implies (1)”.

Stacks 0AIC, condition (2) implies condition (1). If some morphism from an affine formal algebraic space X to an affine scheme turns every closed immersion of an affine scheme into X into a closed immersion, then X is presented by a weakly admissible topological ring: the inverse limit of the section rings of any presentation of X by affine thickenings.

The stage rings are quotients of the sections of the given affine scheme, so that inverse limit is a ring in the universe of the schemes; its projections to the stage rings are surjective, and their kernels are weak ideals of definition forming a fundamental system of neighbourhoods of 0.

theorem exists_isPresentingRing_of_hasAffineClosedImmersionCriterion
    {X : FppfSheaf B S hS} (hX : HasAffineClosedImmersionCriterionMapToSpec B S hS X) :
    ∃ (A : Type u) (_ : CommRing A) (_ : TopologicalSpace A) (_ : IsTopologicalRing A)
      (_ : IsLinearTopology A A), IsPresentingRing B S hS A X

AlgebraicGeometry.FormalSpace.exists_isPresentingRing_of_hasSchemeClosedImmersionCriterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionCriterionPresentation.lean, line 132. The attribute's comment: “(3) implies (1)”.

Stacks 0AIC, condition (3) implies condition (1). The criterion for closed immersions of arbitrary schemes restricts to affine schemes, and then condition (2) gives condition (1).

theorem exists_isPresentingRing_of_hasSchemeClosedImmersionCriterion
    {X : FppfSheaf B S hS} (hX : HasSchemeClosedImmersionCriterionMapToSpec B S hS X) :
    ∃ (A : Type u) (_ : CommRing A) (_ : TopologicalSpace A) (_ : IsTopologicalRing A)
      (_ : IsLinearTopology A A), IsPresentingRing B S hS A X

AlgebraicGeometry.FormalSpace.HasAffineClosedImmersionCriterion.hasSchemeClosedImmersionCriterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/McQuillanCriterion.lean, line 268. The attribute's comment: “part (2) implies part (3)”.

Stacks 0AIC, condition (2) implies condition (3). If some morphism from X to an affine scheme over S turns every closed immersion of an affine scheme into X into a closed immersion of schemes, then it does so for every scheme of the site: a scheme closed-immersed in an affine formal algebraic space is already affine.

theorem HasAffineClosedImmersionCriterion.hasSchemeClosedImmersionCriterion
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) {X : FppfSheaf B S hS}
    (hX : HasAffineClosedImmersionCriterion B S hS X) :
    HasSchemeClosedImmersionCriterion B S hS X

AlgebraicGeometry.FormalSpace.HasAffineClosedImmersionCriterion.hasAllSurjectivePresentations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/McQuillanCriterion.lean, line 374. The attribute's comment: “part (2) implies part (5), and with it part (2) implies part (4). No hypothesis beyond condition (2) is carried. What remains open in this tag is the implication (4) implies (1) for a presentation indexed by an arbitrary directed type in Type (u + 1): the ring it asks for is the limit of the section rings of the presentation, which then lies in Type (u + 1) rather than Type u, so a smallness argument on the index is needed that this development does not have. The sequential case is exists_quotientSystem_formalSpectrum_iso and the countably indexed case is isPresentingRing_of_isCountablyIndexed. The implication (1) implies (2) is open for the reason recorded in the implementation notes above: conditions (2) and (3) ask for an affine scheme over S, and the ring of a presentation carries structure morphisms only on its quotients”.

Stacks 0AIC, condition (2) implies condition (5). Condition (2) is read on every presentation of X by affine thickenings at once, which is condition (5).

theorem HasAffineClosedImmersionCriterion.hasAllSurjectivePresentations
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) {X : FppfSheaf B S hS}
    (hX : HasAffineClosedImmersionCriterion B S hS X) :
    HasAllSurjectivePresentations B S hS X

AlgebraicGeometry.FormalSpace.HasAffineClosedImmersionCriterion.hasSomeSurjectivePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/McQuillanCriterion.lean, line 387. The attribute's comment: “part (2) implies part (4)”.

Stacks 0AIC, condition (2) implies condition (4). The presentation by affine thickenings that affineness of X supplies has surjective section-ring projections.

theorem HasAffineClosedImmersionCriterion.hasSomeSurjectivePresentation
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) {X : FppfSheaf B S hS}
    (hX : HasAffineClosedImmersionCriterion B S hS X) :
    HasSomeSurjectivePresentation B S hS X

AlgebraicGeometry.FormalSpace.HasSchemeClosedImmersionCriterion.hasSomeSurjectivePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/McQuillanCriterion.lean, line 396. The attribute's comment: “part (3) implies part (4)”.

Stacks 0AIC, condition (3) implies condition (4). The criterion for all schemes of the site restricts to the affine ones, which is already enough.

theorem HasSchemeClosedImmersionCriterion.hasSomeSurjectivePresentation
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) {X : FppfSheaf B S hS}
    (hX : HasSchemeClosedImmersionCriterion B S hS X) :
    HasSomeSurjectivePresentation B S hS X

AlgebraicGeometry.FormalSpace.HasAffineClosedImmersionCriterionMapToSpec.hasAllSurjectivePresentations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/McQuillanCriterionPresentation.lean, line 160. The attribute's comment: “(2) implies (5)”.

Stacks 0AIC, condition (2) implies condition (5). If some morphism from X to an affine scheme turns every closed immersion of an affine scheme into X into a closed immersion, then every presentation of X by affine thickenings has surjective section-ring projections.

theorem HasAffineClosedImmersionCriterionMapToSpec.hasAllSurjectivePresentations
    {X : FppfSheaf B S hS} (hX : HasAffineClosedImmersionCriterionMapToSpec B S hS X) :
    HasAllSurjectivePresentations B S hS X

AlgebraicGeometry.FormalSpace.HasSchemeClosedImmersionCriterionMapToSpec.hasAllSurjectivePresentations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/McQuillanCriterionPresentation.lean, line 170. The attribute's comment: “(3) implies (5)”.

Stacks 0AIC, condition (3) implies condition (5). The criterion for closed immersions of arbitrary schemes restricts to affine schemes, and then condition (2) gives condition (5).

theorem HasSchemeClosedImmersionCriterionMapToSpec.hasAllSurjectivePresentations
    {X : FppfSheaf B S hS} (hX : HasSchemeClosedImmersionCriterionMapToSpec B S hS X) :
    HasAllSurjectivePresentations B S hS X

AlgebraicGeometry.FormalSpace.HasSchemeClosedImmersionCriterionMapToSpec.hasSomeSurjectivePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/McQuillanCriterionPresentation.lean, line 179. The attribute's comment: “(3) implies (4)”.

Stacks 0AIC, condition (3) implies condition (4). Every presentation of X by affine thickenings has surjective section-ring projections, and X has one.

theorem HasSchemeClosedImmersionCriterionMapToSpec.hasSomeSurjectivePresentation
    {X : FppfSheaf B S hS} (hX : HasSchemeClosedImmersionCriterionMapToSpec B S hS X) :
    HasSomeSurjectivePresentation B S hS X

AlgebraicGeometry.FormalSpace.HasAffineClosedImmersionCriterionMapToSpec.hasSchemeClosedImmersionCriterionMapToSpec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/McQuillanCriterionSupplement.lean, line 28. The attribute's comment: “part (2) implies part (3)”.

Stacks 0AIC, condition (2) implies condition (3), for the conditions with the morphism to Spec A recorded as a AlgebraicGeometry.FormalSpace.MapToScheme. If some morphism from X to an affine scheme turns every closed immersion of an affine scheme into X into a closed immersion of schemes, then it does so for every scheme of the site: a scheme closed-immersed in an affine formal algebraic space is already affine.

theorem HasAffineClosedImmersionCriterionMapToSpec.hasSchemeClosedImmersionCriterionMapToSpec
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) {X : FppfSheaf B S hS}
    (hX : HasAffineClosedImmersionCriterionMapToSpec B S hS X) :
    HasSchemeClosedImmersionCriterionMapToSpec B S hS X

AlgebraicGeometry.FormalSpace.HasSchemeClosedImmersionCriterionMapToSpec.hasAffineClosedImmersionCriterionMapToSpec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/McQuillanSupplement.lean, line 89. The attribute's comment: “(3) implies (2)”.

Stacks 0AIC, condition (3) implies condition (2), for the conditions with the morphism to Spec A recorded as a AlgebraicGeometry.FormalSpace.MapToScheme. The affine schemes of the site are among its schemes, so the criterion for all schemes restricts to them.

theorem HasSchemeClosedImmersionCriterionMapToSpec.hasAffineClosedImmersionCriterionMapToSpec
    {X : FppfSheaf B S hS} (hX : HasSchemeClosedImmersionCriterionMapToSpec B S hS X) :
    HasAffineClosedImmersionCriterionMapToSpec B S hS X

AlgebraicGeometry.FormalSpace.exists_continuous_ringEquiv_sections_of_weakIdealColimitPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/PresentingRingSectionLimit.lean, line 341. The attribute's comment: “the associated ring is A = lim Γ(X_λ, 𝒪), with its limit topology, for an arbitrary presentation”.

Stacks 0AIC, the concluding clause. If X is the colimit of the spectra of the quotients of a weakly admissible topological ring A by its weak ideals of definition, then for any presentation X = colim Xᵢ of X by affine thickenings the ring A is the inverse limit lim Γ(Xᵢ, 𝒪) of the section rings of that presentation, as a topological ring: the comparison map is an isomorphism of rings which is a homeomorphism for the limit topology of AlgebraicGeometry.FormalSpace.topologicalSpaceSections.

Reduction modulo the weak ideals of definition Jᵢ cut out by the stages is the comparison homomorphism; it is injective because those ideals are cofinal and A is separated, surjective because A is complete, continuous because each Jᵢ is open, and open because the Jᵢ are cofinal.

theorem exists_continuous_ringEquiv_sections_of_weakIdealColimitPresentation
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (A : Type u) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    (hA : TopologicalRing.IsWeaklyAdmissible A) {X : FppfSheaf B S hS}
    (P : WeakIdealColimitPresentation B S hS A X)
    (I : Type (u + 1)) [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (D : I ⥤ BigAffineFppf B S hS)
    (hD : ∀ ⦃i j : I⦄ (f : i ⟶ j),
      Stacks.Thickenings.IsThickening ((BigAffineFppf.toScheme B S hS).map (D.map f)))
    (eD : X ≅ colimit (D ⋙ BigAffineFppf.inclusion B S hS ⋙
      Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))) :
    ∃ e : A ≃+* (sectionDiagram B S hS D ⋙ forget CommRingCat.{u}).sections,
      Continuous e ∧ Continuous e.symm

AlgebraicGeometry.FormalSpace.exists_continuous_ringEquiv_of_isPresentingRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/PresentingRingUniqueness.lean, line 332. The attribute's comment: “the associated ring of a McQuillan affine formal algebraic space is well defined: two rings presenting one affine formal algebraic space are isomorphic as topological rings”.

Stacks 0AIC: the presenting ring of a McQuillan affine formal algebraic space is unique up to isomorphism of topological rings. If the weakly admissible topological rings A and C over S both present the affine formal algebraic space X — each exhibiting X as the colimit of the spectra of its quotients by weak ideals of definition — then A and C are isomorphic as topological rings.

theorem exists_continuous_ringEquiv_of_isPresentingRing {X : FppfSheaf B S hS}
    (hAX : IsPresentingRing B S hS A X) (hCX : IsPresentingRing B S hS C X) :
    ∃ φ : A ≃+* C, Continuous φ ∧ Continuous φ.symm

AlgebraicGeometry.FormalSpace.SequentialQuotients.exists_quotientSystem_formalSpectrum_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SectionLimitPresentation.lean, line 359. The attribute's comment: “(4) implies (1), for a sequential presentation”.

A sheaf presented as the colimit of a sequence of affine thickenings whose section rings are the quotients of a linearly topologized ring A by a fundamental system of weak ideals of definition is the formal spectrum of A.

theorem exists_quotientSystem_formalSpectrum_iso :
    ∃ Q : QuotientSystem B S hS A, Nonempty (X ≅ formalSpectrum Q)

AlgebraicGeometry.FormalSpace.SequentialQuotients.exists_quotientSystem_formalSpectrum_iso', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SectionLimitPresentationRefined.lean, line 79. The attribute's comment: “(4) implies (1), for a sequential presentation”.

A sheaf presented as the colimit of a sequence of affine thickenings whose section rings are the quotients of a linearly topologized ring A by a fundamental system of weak ideals of definition is the formal spectrum of A.

theorem exists_quotientSystem_formalSpectrum_iso' (P : SequentialQuotients B S hS X A) :
    ∃ Q : QuotientSystem B S hS A, Nonempty (X ≅ formalSpectrum Q)

AlgebraicGeometry.FormalSpace.HasSomeSurjectivePresentation.hasAllSurjectivePresentations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SectionsIndependentOfPresentation.lean, line 619. The attribute's comment: “part (4) implies part (5)”.

If some presentation of an affine formal algebraic space by affine thickenings has all its section-ring projections surjective, then every such presentation does.

public theorem HasSomeSurjectivePresentation.hasAllSurjectivePresentations
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) {X : FppfSheaf B S hS}
    (hX : HasSomeSurjectivePresentation B S hS X) :
    HasAllSurjectivePresentations B S hS X

AlgebraicGeometry.FormalSpace.exists_isPresentingRing_of_hasSomeSurjectivePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SurjectivePresentationRing.lean, line 187. The attribute's comment: “(4) implies (1)”.

Stacks 0AIC, condition (4) implies condition (1). An affine formal algebraic space with a presentation by affine thickenings whose section-ring projections are surjective is presented by a weakly admissible topological ring, namely the inverse limit of the section rings of that presentation.

The presentation has only u-many stages up to isomorphism over X, so a polynomial ring on the sections of a u-small cofinal family of stages surjects compatibly onto every stage ring; the weakly admissible completion of that polynomial ring is the presenting ring.

theorem exists_isPresentingRing_of_hasSomeSurjectivePresentation
    {X : FppfSheaf B S hS} (hX : HasSomeSurjectivePresentation B S hS X) :
    ∃ (A : Type u) (_ : CommRing A) (_ : TopologicalSpace A) (_ : IsTopologicalRing A)
      (_ : IsLinearTopology A A), IsPresentingRing B S hS A X

AlgebraicGeometry.FormalSpace.exists_isPresentingRing_of_hasAllSurjectivePresentations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SurjectivePresentationRing.lean, line 239. The attribute's comment: “(5) implies (1)”.

Stacks 0AIC, condition (5) implies condition (1). A presentation whose section-ring projections are all surjective exists as soon as every presentation has that property.

theorem exists_isPresentingRing_of_hasAllSurjectivePresentations
    {X : FppfSheaf B S hS} (hX : HasAllSurjectivePresentations B S hS X) :
    ∃ (A : Type u) (_ : CommRing A) (_ : TopologicalSpace A) (_ : IsTopologicalRing A)
      (_ : IsLinearTopology A A), IsPresentingRing B S hS A X

AlgebraicGeometry.FormalSpace.hasSomeSurjectivePresentation_iff_exists_isPresentingRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SurjectivePresentationRing.lean, line 253. The attribute's comment: “(1), (4) and (5) are equivalent”.

Stacks 0AIC, conditions (1), (4) and (5) are equivalent. For an fppf sheaf satisfying the set-theoretic condition of Stacks 0AIS, being presented by a weakly admissible topological ring is the same as having one presentation by affine thickenings with surjective section-ring projections, and the same as having that property for every presentation. This is the form a consumer wants: McQuillan's condition and the existence of the presenting ring may be exchanged freely, with no ring and no structure morphism given in advance.

theorem hasSomeSurjectivePresentation_iff_exists_isPresentingRing
    {X : FppfSheaf B S hS} (hX : SatisfiesSetTheoreticCondition B S hS X) :
    HasSomeSurjectivePresentation B S hS X ↔
      ∃ (A : Type u) (_ : CommRing A) (_ : TopologicalSpace A) (_ : IsTopologicalRing A)
        (_ : IsLinearTopology A A), IsPresentingRing B S hS A X

AlgebraicGeometry.FormalSpace.hasAllSurjectivePresentations_iff_exists_isPresentingRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SurjectivePresentationRing.lean, line 265. The attribute's comment: “(1), (4) and (5) are equivalent”.

Stacks 0AIC, conditions (4) and (5) are equivalent to condition (1). The statement above for the "every presentation" form of McQuillan's condition.

theorem hasAllSurjectivePresentations_iff_exists_isPresentingRing
    {X : FppfSheaf B S hS} (hX : SatisfiesSetTheoreticCondition B S hS X) :
    HasAllSurjectivePresentations B S hS X ↔
      ∃ (A : Type u) (_ : CommRing A) (_ : TopologicalSpace A) (_ : IsTopologicalRing A)
        (_ : IsLinearTopology A A), IsPresentingRing B S hS A X

AlgebraicGeometry.FormalSpace.isThickening_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ThickeningClassification.lean, line 507. The attribute's comment: “thickening_classification”.

Every weak ideal of definition gives a thickening of the formal space.

public theorem isThickening_quotient
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (J : WeakIdeals A) :
    (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)))
      (quotientMap B S hS A X P J)

AlgebraicGeometry.FormalSpace.relativelyRepresentable_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ThickeningClassification.lean, line 538. The attribute's comment: “thickening_classification”.

Every weak ideal of definition gives a representable morphism from its quotient scheme to the formal space.

public theorem relativelyRepresentable_quotient
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (J : WeakIdeals A) :
    (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).relativelyRepresentable
      (quotientMap B S hS A X P J)

AlgebraicGeometry.FormalSpace.existsUnique_weakIdeal_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ThickeningClassification.lean, line 547. The attribute's comment: “thickening_classification”.

Any representable thickening from a scheme into the formal space is, uniquely up to its weak ideal, a quotient stage of the canonical presentation.

public theorem existsUnique_weakIdeal_quotient
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (T : BigFppfOver B S hS)
    (f : (Sheaf.sheafifiedYoneda
      (BigFppfOver.topology B S hS)).obj T ⟶ X)
    (_hf_repr : (Sheaf.sheafifiedYoneda
      (BigFppfOver.topology B S hS)).relativelyRepresentable f)
    (hf_thick : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f) :
    ∃! J : WeakIdeals A,
      ∃ e : T ≅ (BigAffineFppf.inclusion B S hS).obj (P.diagram.obj J),
      (Sheaf.sheafifiedYoneda
          (BigFppfOver.topology B S hS)).map e.hom ≫
          quotientMap B S hS A X P J = f

AlgebraicGeometry.FormalSpace.inducedSectionHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ThickeningClassification.lean, line 712. The attribute's comment: “thickening_classification”.

The homomorphism on global sections induced by a representable thickening into the formal space. The uniqueness and compatibility statements below show that this construction does not depend on the chosen quotient description.

public noncomputable def inducedSectionHom
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (T : BigFppfOver B S hS)
    (f : (Sheaf.sheafifiedYoneda
      (BigFppfOver.topology B S hS)).obj T ⟶ X)
    (hf_repr : (Sheaf.sheafifiedYoneda
      (BigFppfOver.topology B S hS)).relativelyRepresentable f)
    (hf_thick : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f) :
    A →+* Γ((BigFppfOver.toScheme B S hS).obj T, ⊤)

AlgebraicGeometry.FormalSpace.inducedSectionHom_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ThickeningClassification.lean, line 734. The attribute's comment: “thickening_classification”.

At every quotient description compatible with the morphism to the formal space, the induced map on sections is the canonical quotient map followed by the affine global-sections isomorphism and transport to T.

public theorem inducedSectionHom_quotient
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (T : BigFppfOver B S hS)
    (f : (Sheaf.sheafifiedYoneda
      (BigFppfOver.topology B S hS)).obj T ⟶ X)
    (hf_repr : (Sheaf.sheafifiedYoneda
      (BigFppfOver.topology B S hS)).relativelyRepresentable f)
    (hf_thick : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f)
    (J : WeakIdeals A)
    (e : T ≅ (BigAffineFppf.inclusion B S hS).obj (P.diagram.obj J))
    (he : (Sheaf.sheafifiedYoneda
      (BigFppfOver.topology B S hS)).map e.hom ≫
        quotientMap B S hS A X P J = f) :
    inducedSectionHom B S hS A X P hA T f hf_repr hf_thick =
      sectionHomOfQuotientIso B S hS A X P J T e

AlgebraicGeometry.FormalSpace.quotient_ker_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ThickeningClassification.lean, line 777. The attribute's comment: “thickening_classification”.

The classifying ideal of a representable thickening is the kernel of the homomorphism from the associated ring to its global sections.

public theorem quotient_ker_sections
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (T : BigFppfOver B S hS)
    (f : (Sheaf.sheafifiedYoneda
      (BigFppfOver.topology B S hS)).obj T ⟶ X)
    (hf_repr : (Sheaf.sheafifiedYoneda
      (BigFppfOver.topology B S hS)).relativelyRepresentable f)
    (hf_thick : (MorphismProperty.relative
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS))
      (MorphismProperty.inverseImage
        (@Stacks.Thickenings.IsThickening : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS))) f)
    (J : WeakIdeals A)
    (e : T ≅ (BigAffineFppf.inclusion B S hS).obj (P.diagram.obj J))
    (he : (Sheaf.sheafifiedYoneda
      (BigFppfOver.topology B S hS)).map e.hom ≫
        quotientMap B S hS A X P J = f) :
    RingHom.ker (inducedSectionHom B S hS A X P hA T f hf_repr hf_thick) = J.1

AlgebraicGeometry.FormalSpace.isClosedImmersion_toSpec_of_weakIdealColimitPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/WeakIdealClosedImmersionCriterion.lean, line 84. The attribute's comment: “(1) implies (2)”.

Stacks 0AIC, condition (1) implies condition (2). Let A be a weakly admissible topological ring and let the fppf sheaf X, satisfying the set-theoretic condition of Stacks 0AIS, be the colimit of the spectra of the quotients of A by its weak ideals of definition. Then X is an affine formal algebraic space, and every closed immersion of an affine scheme T of the site into X factors through the spectrum of a quotient A ⧸ K in such a way that the resulting morphism T ⟶ Spec A — which is the composition of T ⟶ X with the canonical X ⟶ Spec A — is a closed immersion of schemes.

theorem isClosedImmersion_toSpec_of_weakIdealColimitPresentation
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (A : Type u) [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    (hA : TopologicalRing.IsWeaklyAdmissible A) {X : FppfSheaf B S hS}
    (hset : SatisfiesSetTheoreticCondition B S hS X)
    (P : WeakIdealColimitPresentation B S hS A X) :
    IsAffineFormalAlgebraicSpace B S hS X ∧
      ∀ (T : BigAffineFppf B S hS)
        (g : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj
            ((BigAffineFppf.inclusion B S hS).obj T) ⟶ X),
        IsClosedImmersionInto B S hS g →
        ∃ (K : WeakIdeals A) (c : T ⟶ P.diagram.obj K),
          (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).map
              ((BigAffineFppf.inclusion B S hS).map c) ≫
            colimit.ι (P.diagram ⋙ BigAffineFppf.inclusion B S hS ⋙
              Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) K ≫ P.colimitIso.inv = g ∧
          IsClosedImmersion ((BigAffineFppf.toScheme B S hS).map c ≫
            (P.quotientIso K).hom ≫
              Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk K.1)))

AlgebraicGeometry.FormalSpace.hasAffineClosedImmersionCriterion_of_weakIdealColimitPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/WeakIdealMapToSpec.lean, line 336. The attribute's comment: “(1) implies (2)”.

Stacks 0AIC, condition (1) implies condition (2). Let A be a weakly admissible topological ring and let the fppf sheaf X, satisfying the set-theoretic condition of Stacks 0AIS, be the colimit of the spectra of the quotients of A by its weak ideals of definition. Then X is an affine formal algebraic space, and there are a ring and a morphism of sheaves from X to its spectrum such that every closed immersion of an affine scheme of the site into X composes to a closed immersion of schemes; the witnesses are A itself and AlgebraicGeometry.FormalSpace.weakIdealToSpecPoints.

This is the library's AlgebraicGeometry.FormalSpace.HasAffineClosedImmersionCriterionMapToSpec: the morphism to Spec A is given at every object of the site, not only at those carrying a closed immersion into X. The implication is unconditional — no morphism Spec A ⟶ S and no compatibility with the structure morphisms of the stages is assumed — because condition (2), like the source's, asks for none.

theorem hasAffineClosedImmersionCriterion_of_weakIdealColimitPresentation
    (hA : TopologicalRing.IsWeaklyAdmissible A) {X : FppfSheaf B S hS}
    (hset : SatisfiesSetTheoreticCondition B S hS X)
    (P : WeakIdealColimitPresentation B S hS A X) :
    HasAffineClosedImmersionCriterionMapToSpec B S hS X

AlgebraicGeometry.FormalSpace.hasSchemeClosedImmersionCriterion_of_weakIdealColimitPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/WeakIdealMapToSpec.lean, line 349. The attribute's comment: “(1) implies (3)”.

Stacks 0AIC, condition (1) implies condition (3). Condition (1) gives condition (2), and a scheme closed-immersed in an affine formal algebraic space is affine, so the criterion extends from the affine schemes of the site to all of them.

theorem hasSchemeClosedImmersionCriterion_of_weakIdealColimitPresentation
    (hA : TopologicalRing.IsWeaklyAdmissible A) {X : FppfSheaf B S hS}
    (hset : SatisfiesSetTheoreticCondition B S hS X)
    (P : WeakIdealColimitPresentation B S hS A X) :
    HasSchemeClosedImmersionCriterionMapToSpec B S hS X

AlgebraicGeometry.FormalSpace.hasAffineClosedImmersionCriterion_of_hasSomeSurjectivePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/WeakIdealMapToSpec.lean, line 373. The attribute's comment: “(4) implies (2)”.

Stacks 0AIC, condition (4) implies condition (2). An affine formal algebraic space with some presentation by affine thickenings whose section-ring projections are surjective admits a ring A and a morphism X ⟶ Spec A through which every closed immersion of an affine scheme of the site into X composes to a closed immersion of schemes.

The ring is the one condition (4) produces, namely the inverse limit of the section rings of the presentation, and the morphism is the global family built above. No structure morphism Spec A ⟶ S is involved anywhere, which is what makes this arrow available: that limit carries none, so a condition (2) demanding one would have no arrow out of condition (4).

theorem hasAffineClosedImmersionCriterion_of_hasSomeSurjectivePresentation
    {X : FppfSheaf B S hS} (hX : HasSomeSurjectivePresentation B S hS X) :
    HasAffineClosedImmersionCriterionMapToSpec B S hS X

AlgebraicGeometry.FormalSpace.hasSchemeClosedImmersionCriterion_of_hasSomeSurjectivePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/WeakIdealMapToSpec.lean, line 388. The attribute's comment: “(4) implies (3)”.

Stacks 0AIC, condition (4) implies condition (3). Condition (4) gives condition (2), and a scheme closed-immersed in an affine formal algebraic space is affine, so the criterion extends from the affine schemes of the site to all of them.

theorem hasSchemeClosedImmersionCriterion_of_hasSomeSurjectivePresentation
    {X : FppfSheaf B S hS} (hX : HasSomeSurjectivePresentation B S hS X) :
    HasSchemeClosedImmersionCriterionMapToSpec B S hS X

AlgebraicGeometry.FormalSpace.hasAffineClosedImmersionCriterion_of_hasAllSurjectivePresentations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/WeakIdealMapToSpec.lean, line 398. The attribute's comment: “(5) implies (2)”.

Stacks 0AIC, condition (5) implies condition (2). Condition (5) gives condition (4) by instantiating its quantifier at the presentation an affine formal algebraic space comes with, and condition (4) gives condition (2).

theorem hasAffineClosedImmersionCriterion_of_hasAllSurjectivePresentations
    {X : FppfSheaf B S hS} (hX : HasAllSurjectivePresentations B S hS X) :
    HasAffineClosedImmersionCriterionMapToSpec B S hS X

AlgebraicGeometry.FormalSpace.hasAllSurjectivePresentations_of_exists_weaklyAdmissible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/WeakIdealPresentation.lean, line 1410. The attribute's comment: “(1) implies (5)”.

Stacks 0AIC, (1) ⇒ (5). Condition (1) of Stacks 0AIC — the existence of a weakly admissible topological ring over S presenting X as the colimit of the spectra of its quotients by weak ideals of definition — implies condition (5): X is an affine formal algebraic space and every presentation of it by affine thickenings has surjective section-ring projections.

theorem hasAllSurjectivePresentations_of_exists_weaklyAdmissible
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) {X : FppfSheaf B S hS}
    (hX : SatisfiesSetTheoreticCondition B S hS X)
    (h : ∃ (A : Type u) (_ : CommRing A) (_ : TopologicalSpace A)
        (_ : IsTopologicalRing A) (_ : IsLinearTopology A A),
      letI : CommRing A := ‹CommRing A›
      letI : TopologicalSpace A := ‹TopologicalSpace A›
      letI : IsTopologicalRing A := ‹IsTopologicalRing A›
      letI : IsLinearTopology A A := ‹IsLinearTopology A A›
      TopologicalRing.IsWeaklyAdmissible A ∧
        Nonempty (WeakIdealColimitPresentation B S hS A X)) :
    HasAllSurjectivePresentations B S hS X

Tag 0AID, a definition

Tag 0AID in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsClassical, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Types.lean, line 84. The attribute's comment: “classical”.

Stacks 0AID (1). A McQuillan affine formal algebraic space is classical when its associated weakly admissible topological ring is admissible, that is has an ideal of definition and is complete.

abbrev IsClassical (X : FppfSheaf B S hS) : Prop

AlgebraicGeometry.FormalSpace.IsWeaklyAdic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Types.lean, line 94. The attribute's comment: “weakly adic”.

Stacks 0AID (2). A McQuillan affine formal algebraic space is weakly adic when its associated weakly admissible topological ring is weakly adic, that is the closed powers of a single ideal form a fundamental system of open ideals.

abbrev IsWeaklyAdic (X : FppfSheaf B S hS) : Prop

AlgebraicGeometry.FormalSpace.IsAdic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Types.lean, line 104. The attribute's comment: “adic”.

Stacks 0AID (3). A McQuillan affine formal algebraic space is adic when its associated weakly admissible topological ring is adic, that is its topology is the adic topology of an ideal of definition and it is complete.

abbrev IsAdic (X : FppfSheaf B S hS) : Prop

AlgebraicGeometry.FormalSpace.IsAdicStar, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Types.lean, line 114. The attribute's comment: “adic star”.

Stacks 0AID (4). A McQuillan affine formal algebraic space is adic* when its associated weakly admissible topological ring is adic and moreover has a finitely generated ideal of definition.

abbrev IsAdicStar (X : FppfSheaf B S hS) : Prop

AlgebraicGeometry.FormalSpace.IsNoetherian, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Types.lean, line 124. The attribute's comment: “Noetherian”.

Stacks 0AID (5). A McQuillan affine formal algebraic space is Noetherian when its associated weakly admissible topological ring is both a Noetherian ring and adic.

abbrev IsNoetherian (X : FppfSheaf B S hS) : Prop

Declarations registered for the tag:

AlgebraicGeometry.FormalSpace.HasSomeSurjectivePresentation, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/Types.lean, line 69 (StacksFrontier): “McQuillan”.

Tag 0AIE, a remark

Tag 0AIE in the Stacks Project.

AlgebraicGeometry.surjective_spfQuotientPointsColimitMap_app_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsAffine.lean, line 390. The attribute's comment: “the comparison map of the colimit formula is surjective at an affine test scheme”.

Stacks 0AIE, the affine case of the colimit formula. The comparison map colim h_{Spec (A/I)} → h_{Spf A} is surjective on the points over an affine scheme: such a point factors through one of the quotients by AlgebraicGeometry.exists_factor_spfQuotientPointOn.

theorem surjective_spfQuotientPointsColimitMap_app_of_isAffine (hA : IsAdmissible A)
    (T : Scheme.{u}) [IsAffine T] :
    Function.Surjective ((spfQuotientPointsColimitMap A hA).app (op T))

AlgebraicGeometry.isLocallySurjective_spfQuotientPointsColimitMap_of_isAdmissible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsAffine.lean, line 414. The attribute's comment: “the comparison map of the colimit formula is locally surjective, with no hypothesis beyond admissibility”.

Stacks 0AIE, the colimit formula, with no hypothesis beyond admissibility: the comparison map colim h_{Spec (A/I)} → h_{Spf A} is locally surjective for the Zariski topology. Together with AlgebraicGeometry.isLocallyInjective_spfQuotientPointsColimitMap this is the source's h_{Spf A} = colim h_{Spec (A/I)}, read — as it must be — as an isomorphism of the associated sheaves.

This discharges the hypothesis of AlgebraicGeometry.isLocallySurjective_spfQuotientPointsColimitMap, which was the affine case, i.e. the surjectivity half of Stacks 0AHZ.

theorem isLocallySurjective_spfQuotientPointsColimitMap_of_isAdmissible (hA : IsAdmissible A) :
    Presheaf.IsLocallySurjective Scheme.zariskiTopology.{u}
      (spfQuotientPointsColimitMap A hA)

AlgebraicGeometry.spfQuotientPointsColimitMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsColimit.lean, line 263. The attribute's comment: “the comparison map h_colim → h_Spf A of the colimit formula”.

Stacks 0AIE. The comparison map of the source's colimit formula h_{Spf A} = colim h_{Spec (A/I)}: the morphism out of the colimit of the functors of points of the quotient spectra determined by the morphisms Spec (A/I) → Spf A.

noncomputable def spfQuotientPointsColimitMap [IsLinearTopology A A] (hA : IsAdmissible A) :
    colimit (spfQuotientPointsDiagram A) ⟶ formalSchemePoints (spfFormalScheme A hA)

AlgebraicGeometry.injective_spfQuotientPointsColimitMap_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsColimit.lean, line 294. The attribute's comment: “the comparison map of the colimit formula is injective at every test scheme”.

Stacks 0AIE. The comparison map of the colimit formula is injective on the points over every scheme: two morphisms T → Spec (A/I) and T → Spec (A/J) inducing the same point of Spf A already agree over Spec (A/(I ∩ J)).

theorem injective_spfQuotientPointsColimitMap_app [IsLinearTopology A A] (hA : IsAdmissible A)
    (T : Scheme.{u}) :
    Function.Injective ((spfQuotientPointsColimitMap A hA).app (op T))

AlgebraicGeometry.mono_spfQuotientPointsColimitMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsColimit.lean, line 351. The attribute's comment: “the comparison map of the colimit formula is a monomorphism of presheaves”.

Stacks 0AIE. The colimit of the functors of points of the quotient spectra is a subfunctor of the functor of points of Spf A: the comparison map is a monomorphism of presheaves, being injective on the points over every scheme.

theorem mono_spfQuotientPointsColimitMap [IsLinearTopology A A] (hA : IsAdmissible A) :
    Mono (spfQuotientPointsColimitMap A hA)

AlgebraicGeometry.isLocallyInjective_spfQuotientPointsColimitMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsColimit.lean, line 361. The attribute's comment: “the comparison map of the colimit formula is locally injective”.

Stacks 0AIE. The comparison map of the colimit formula is locally injective for the Zariski topology on schemes, being injective on the points over every scheme.

theorem isLocallyInjective_spfQuotientPointsColimitMap [IsLinearTopology A A]
    (hA : IsAdmissible A) :
    Presheaf.IsLocallyInjective Scheme.zariskiTopology.{u}
      (spfQuotientPointsColimitMap A hA)

AlgebraicGeometry.isLocallySurjective_spfQuotientPointsColimitMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalScheme/FunctorOfPointsColimit.lean, line 380. The attribute's comment: “the colimit formula is locally surjective, assuming its affine case (the surjectivity half of Stacks 0AHZ)”.

Stacks 0AIE. The reduction of the colimit formula to the affine case. If every point of Spf A over an affine scheme factors through one of the quotients Spec (A/I), then the comparison map of the colimit formula is locally surjective for the Zariski topology, because every scheme has an affine open cover.

The hypothesis is the surjectivity half of the identification Mor(Spec B, Spf A) = Hom_cont(A, Γ(Spec B, 𝒪)) of Stacks 0AHZ. It is proved in AlgebraicGeometry.exists_factor_spfQuotientPointOn, so the conclusion holds with no hypothesis beyond admissibility; that is AlgebraicGeometry.isLocallySurjective_spfQuotientPointsColimitMap_of_isAdmissible.

theorem isLocallySurjective_spfQuotientPointsColimitMap [IsLinearTopology A A]
    (hA : IsAdmissible A)
    (haff : ∀ T : Scheme.{u}, IsAffine T →
      Function.Surjective ((spfQuotientPointsColimitMap A hA).app (op T))) :
    Presheaf.IsLocallySurjective Scheme.zariskiTopology.{u}
      (spfQuotientPointsColimitMap A hA)

AlgebraicGeometry.FormalSpace.isClassical_formalSchemePointsFppfSheaf_of_contains, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineFormalSchemeEquivalence.lean, line 368. The attribute's comment: “if the coproduct of the Spec(A/I) over the ideals of definition belongs to the site, then h_X is a classical affine formal algebraic space”.

Stacks 0AIE. Over a terminal base, the functor of points of an affine formal scheme Spf A is a classical affine formal algebraic space as soon as the coproduct of the schemes Spec (A/I), over the ideals of definition of A, belongs to the big fppf site.

theorem isClassical_formalSchemePointsFppfSheaf_of_contains (hterm : IsTerminal S)
    (hA : TopologicalRing.IsAdmissible A) {X : FormalScheme.{u}} (e : X ≅ spfFormalScheme A hA)
    (hB : B.Contains (∐ fun I : IdealsOfDefinition A => Spec (spfQuotient A I))) :
    IsClassical B S hS (formalSchemePointsFppfSheaf B S hS X)

AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_formalSchemePointsFppfSheaf_of_contains, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineFormalSchemeEquivalence.lean, line 382. The attribute's comment: “if the coproduct of the Spec(A/I) over the ideals of definition belongs to the site, then h_X is an affine formal algebraic space”.

Stacks 0AIE. Over a terminal base, the functor of points of an affine formal scheme Spf A is an affine formal algebraic space as soon as the coproduct of the schemes Spec (A/I), over the ideals of definition of A, belongs to the big fppf site.

theorem isAffineFormalAlgebraicSpace_formalSchemePointsFppfSheaf_of_contains
    (hterm : IsTerminal S) (hA : TopologicalRing.IsAdmissible A) {X : FormalScheme.{u}}
    (e : X ≅ spfFormalScheme A hA)
    (hB : B.Contains (∐ fun I : IdealsOfDefinition A => Spec (spfQuotient A I))) :
    IsAffineFormalAlgebraicSpace B S hS (formalSchemePointsFppfSheaf B S hS X)

AlgebraicGeometry.FormalSpace.isEquivalence_smallAffineFormalSchemePointsFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineFormalSchemeEquivalence.lean, line 460. The attribute's comment: “the category of affine formal schemes is equivalent to the category of classical affine formal algebraic spaces, by the functor of points”.

Stacks 0AIE, the equivalence. Over a terminal base S (the source's Spec(ℤ)), the functor of points 𝔛 ↦ h_𝔛 is an equivalence from the category of affine formal schemes Spf A whose coproduct ∐_I Spec (A/I) belongs to the big fppf site B (the source's "compatible choices of big site") to the category of classical affine formal algebraic spaces over S.

theorem isEquivalence_smallAffineFormalSchemePointsFunctor (hterm : IsTerminal S) :
    (smallAffineFormalSchemePointsFunctor B S hS hterm).IsEquivalence

AlgebraicGeometry.FormalSpace.isClassical_iff_exists_admissible_quotientSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClassicalCharacterization.lean, line 94. The attribute's comment: “the objects: a sheaf is a classical affine formal algebraic space exactly when it is the formal spectrum of an admissible topological ring”.

Stacks 0AIE, the objects. An fppf sheaf over S satisfying the set-theoretic condition of Stacks 0AIS is a classical affine formal algebraic space in the sense of Stacks 0AID (1) exactly when it is isomorphic to the formal spectrum of Stacks 0AIF of an admissible topological ring over S.

This is the object half of the correspondence the source's remark describes, read on the formal-space side of the bridge: the classical affine formal algebraic spaces are the Spf A for A admissible, and nothing else. Both directions hold, with no hypothesis beyond the set-theoretic condition, which the left-hand side implies.

The correspondence with affine formal schemes, and the equivalence of categories the source concludes with, need in addition the identification of the formal spectrum with the functor of points of Spf A and the full faithfulness of Stacks 0AI1; see the implementation notes of this file.

theorem isClassical_iff_exists_admissible_quotientSystem {X : FppfSheaf B S hS}
    (hX : SatisfiesSetTheoreticCondition B S hS X) :
    IsClassical B S hS X ↔
      ∃ (A : Type u) (_ : CommRing A) (_ : TopologicalSpace A) (_ : IsTopologicalRing A)
        (_ : IsLinearTopology A A),
        TopologicalRing.IsAdmissible A ∧
          ∃ D : QuotientSystem B S hS A, Nonempty (X ≅ formalSpectrum D)

AlgebraicGeometry.FormalSpace.final_idealOfDefinitionIndex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSchemeSpectrumComparison.lean, line 196. The attribute's comment: “the ideals of definition are cofinal among the weak ideals of definition, so the colimit of the remark and the formal spectrum of Stacks 0AIF have the same index”.

Stacks 0AIE, the index reconciliation. In a pre-admissible topological ring the ideals of definition are cofinal below the weak ideals of definition — the intersection of a weak ideal of definition with an ideal of definition is an ideal of definition — so the functor they induce on index categories is final, and colimits may be computed over either index.

This is what reconciles the colimit of Stacks 0AIE, taken over the ideals of definition of an admissible ring, with the formal spectrum of Stacks 0AIF, taken over the weak ideals of definition.

theorem final_idealOfDefinitionIndex (hA : TopologicalRing.IsPreAdmissible A) :
    (idealOfDefinitionIndex A).monotone.functor.Final

AlgebraicGeometry.FormalSpace.QuotientSystem.formalSpectrumIsoIdealOfDefinitionColimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSchemeSpectrumComparison.lean, line 225. The attribute's comment: “the colimit over the ideals of definition is the formal spectrum of Stacks 0AIF”.

Stacks 0AIE, the colimit of the remark. The colimit of the represented quotient spectra over the ideals of definition of a pre-admissible topological ring is the formal spectrum of Stacks 0AIF, whose colimit runs over the weak ideals of definition. The two indices have the same colimit by AlgebraicGeometry.FormalSpace.final_idealOfDefinitionIndex.

def QuotientSystem.formalSpectrumIsoIdealOfDefinitionColimit
    (hA : TopologicalRing.IsPreAdmissible A) (D : QuotientSystem B S hS A) :
    colimit D.idealOfDefinitionDiagram ≅ formalSpectrum D

AlgebraicGeometry.FormalSpace.isIso_spfFormalSchemeFppfComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSchemeSpectrumComparisonIso.lean, line 406. The attribute's comment: “h_{Spf A} = colim h_{Spec (A/I)} as fppf sheaves: the comparison morphism from the formal spectrum to the functor of points of the affine formal scheme is an isomorphism”.

Stacks 0AIE, the colimit formula. The comparison morphism from the formal spectrum of an admissible topological ring A over a terminal base to the functor of points of the affine formal scheme Spf A is an isomorphism of fppf sheaves over S.

theorem isIso_spfFormalSchemeFppfComparison (hterm : IsTerminal S)
    (hA : TopologicalRing.IsAdmissible A) (D : QuotientSystem B S hS A) :
    IsIso (spfFormalSchemeFppfComparison hA D)

AlgebraicGeometry.FormalSpace.isClassical_formalSchemePointsFppfSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSchemeSpectrumComparisonIso.lean, line 446. The attribute's comment: “the functor of points of an affine formal scheme over a terminal base is a classical affine formal algebraic space”.

Stacks 0AIE, the type of the functor of points. The functor of points of the affine formal scheme Spf A of an admissible topological ring A over a terminal base is a classical affine formal algebraic space over S in the sense of Stacks 0AID (1).

Nothing is assumed beyond admissibility of A and the source's own size conditions: that the quotient spectra lie in the chosen big fppf site, which is part of the datum of a quotient system, and that their coproduct does, which is AlgebraicGeometry.FormalSpace.QuotientSystem.HasLargeSite. The fppf sheaf condition on the functor of points is AlgebraicGeometry.FormalSpace.isFppfSheafFormalSchemePoints_formalScheme and the identification with the formal spectrum is AlgebraicGeometry.FormalSpace.isIso_spfFormalSchemeFppfComparison.

theorem isClassical_formalSchemePointsFppfSheaf (hterm : IsTerminal S)
    (hA : TopologicalRing.IsAdmissible A) (D : QuotientSystem B S hS A)
    (hB : D.HasLargeSite) :
    IsClassical B S hS (formalSchemePointsFppfSheaf B S hS (spfFormalScheme A hA))

AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_formalSchemePointsFppfSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSchemeSpectrumComparisonIso.lean, line 458. The attribute's comment: “the functor of points of an affine formal scheme over a terminal base is an affine formal algebraic space”.

Stacks 0AIE. The functor of points of an affine formal scheme over a terminal base is an affine formal algebraic space over S; it is the affineness half of AlgebraicGeometry.FormalSpace.isClassical_formalSchemePointsFppfSheaf.

theorem isAffineFormalAlgebraicSpace_formalSchemePointsFppfSheaf (hterm : IsTerminal S)
    (hA : TopologicalRing.IsAdmissible A) (D : QuotientSystem B S hS A)
    (hB : D.HasLargeSite) :
    IsAffineFormalAlgebraicSpace B S hS
      (formalSchemePointsFppfSheaf B S hS (spfFormalScheme A hA))

AlgebraicGeometry.FormalSpace.isClassical_formalSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSpectrumClassical.lean, line 137. The attribute's comment: “the formal spectrum of an admissible topological ring is a classical affine formal algebraic space”.

Stacks 0AIE. Let A be an admissible topological ring over S. If the coproduct of the spectra of the quotients of A by its weak ideals of definition lies in the chosen big fppf site, then the formal spectrum Spf A is a classical affine formal algebraic space over S in the sense of Stacks 0AID (1).

This is the second conclusion of the source's remark, for the object its colimit formula produces. The size hypothesis is the source's own: the source needs the coproduct of the quotient spectra to lie in the chosen big fppf site, which is what supplies the representable atlas demanded by the set-theoretic condition of Stacks 0AIS. The source's colimit runs over the ideals of definition of A and this one over its weak ideals of definition; the two agree, because in a pre-admissible ring the ideals of definition are cofinal below the weak ideals of definition (TopologicalRing.exists_isIdealOfDefinition_le_of_isWeakIdealOfDefinition).

Only this direction holds: see the implementation notes of this file.

theorem isClassical_formalSpectrum (hA : TopologicalRing.IsAdmissible A)
    (D : QuotientSystem B S hS A) (hB : D.HasLargeSite) :
    IsClassical B S hS (formalSpectrum D)

Tag 0AIF, a definition

Tag 0AIF in the Stacks Project.

AlgebraicGeometry.FormalSpace.formalSpectrum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSpectrum.lean, line 260. The attribute's comment: “construction”.

The formal spectrum of a weakly admissible topological ring over S: the fppf-sheaf colimit of its quotient spectra by weak ideals of definition.

public def formalSpectrum (D : QuotientSystem B S hS A) :
    Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))

AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_formalSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSpectrum.lean, line 385. The attribute's comment: “affine formal algebraic space”.

The formal spectrum is affine as a formal algebraic space over the base.

public theorem isAffineFormalAlgebraicSpace_formalSpectrum
    [IsTopologicalRing A] [IsLinearTopology A A]
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (D : QuotientSystem B S hS A) (hB : D.HasLargeSite) :
    IsAffineFormalAlgebraicSpace B S hS (formalSpectrum D)

AlgebraicGeometry.FormalSpace.existsUnique_formalSpectrumMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSpectrum.lean, line 786. The attribute's comment: “quotient-stage characterization”.

The map of formal spectra is uniquely characterized by its effect on every quotient stage. This is the universal-property construction of Spf(f).

public theorem existsUnique_formalSpectrumMap
    {D : QuotientSystem B S hS A} {E : QuotientSystem B S hS C}
    [IsTopologicalRing A] [IsLinearTopology A A]
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (f : ContinuousHom D E) :
    ∃! φ : formalSpectrum E ⟶ formalSpectrum D,
      ∀ (J : { I : Ideal A // TopologicalRing.IsWeakIdealOfDefinition I })
        (K : { I : Ideal C // TopologicalRing.IsWeakIdealOfDefinition I })
        (h : J.1 ≤ Ideal.comap f.toRingHom K.1),
        formalSpectrumInclusion E (OrderDual.toDual K) ≫ φ =
          (Sheaf.sheafifiedYoneda
            (BigFppfOver.topology B S hS)).map
              ((BigAffineFppf.inclusion B S hS).map
                (f.stageMap J K h)) ≫
        formalSpectrumInclusion D (OrderDual.toDual J)

AlgebraicGeometry.FormalSpace.formalSpectrumMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSpectrum.lean, line 814. The attribute's comment: “functorial map”.

The canonical contravariant map on formal spectra.

public noncomputable def formalSpectrumMap
    {D : QuotientSystem B S hS A} {E : QuotientSystem B S hS C}
    [IsTopologicalRing A] [IsLinearTopology A A]
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (f : ContinuousHom D E) : formalSpectrum E ⟶ formalSpectrum D

AlgebraicGeometry.FormalSpace.formalSpectrumMap_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSpectrum.lean, line 840. The attribute's comment: “identity law”.

The formal-spectrum map of the identity homomorphism is the identity.

public theorem formalSpectrumMap_id
    {D : QuotientSystem B S hS A}
    [IsTopologicalRing A] [IsLinearTopology A A]
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (f : ContinuousHom D D) (hf : f.toRingHom = RingHom.id A) :
    formalSpectrumMap hA f = 𝟙 (formalSpectrum D)

AlgebraicGeometry.FormalSpace.formalSpectrumMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FormalSpectrum.lean, line 876. The attribute's comment: “composition law”.

Formal spectrum reverses composition of continuous maps over the base.

public theorem formalSpectrumMap_comp
    {D : QuotientSystem B S hS A} {E : QuotientSystem B S hS C}
    {G : Type u} [CommRing G] [TopologicalSpace G]
    {F : QuotientSystem B S hS G}
    [IsTopologicalRing A] [IsLinearTopology A A]
    [IsTopologicalRing C] [IsLinearTopology C C]
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (hC : TopologicalRing.IsWeaklyAdmissible C)
    (f : ContinuousHom D E) (g : ContinuousHom E F)
    (gf : ContinuousHom D F)
    (hgf : gf.toRingHom = g.toRingHom.comp f.toRingHom) :
    formalSpectrumMap hC g ≫ formalSpectrumMap hA f =
      formalSpectrumMap hA gf

AlgebraicGeometry.FormalSpace.formalSpectrumMap_comp_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigFlatComposition.lean, line 181. The attribute's comment: “composition law for the composite continuous hom”.

Stacks 0AIF. The formal spectrum turns ContinuousHom.comp into composition of morphisms of formal spectra, in the direction that reverses the order.

theorem formalSpectrumMap_comp_eq (hw₂ : TopologicalRing.IsWeaklyAdmissible A₂)
    (hw₃ : TopologicalRing.IsWeaklyAdmissible A₃)
    (q : ContinuousHom D₂ D₁) (r : ContinuousHom D₃ D₂) :
    formalSpectrumMap hw₂ q ≫ formalSpectrumMap hw₃ r =
      formalSpectrumMap hw₃ (ContinuousHom.comp hw₂ hw₃ q r)

Tag 0AN0, a lemma

Tag 0AN0 in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_continuous_ringEquiv_of_formalSpectrum_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/PresentingRingUniqueness.lean, line 299. The attribute's comment: “the isomorphism of topological rings underlying an isomorphism of formal spectra, from the existence and uniqueness of the two continuous homomorphisms”.

Stacks 0AN0, applied in both directions. An isomorphism of the formal spectra of two weakly admissible topological rings over S is the formal spectrum of a ring equivalence which is continuous in both directions. Each direction of the isomorphism is Spf of a unique continuous ring map over S, and each composite is a continuous ring map over S whose formal spectrum is the identity, hence by uniqueness is the identity ring map. The equivalence is the one those two ring maps make: its two directions are g and g', whose formal spectra are the two directions of the given isomorphism.

theorem exists_continuous_ringEquiv_of_formalSpectrum_iso
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    {D : QuotientSystem B S hS A} {E : QuotientSystem B S hS C}
    (e : formalSpectrum E ≅ formalSpectrum D) :
    ∃ (g : ContinuousHom D E) (g' : ContinuousHom E D) (φ : A ≃+* C),
      formalSpectrumMap hA g = e.hom ∧ formalSpectrumMap hC g' = e.inv ∧
        ⇑φ = ⇑g.toRingHom ∧ ⇑φ.symm = ⇑g'.toRingHom ∧
          Continuous φ ∧ Continuous φ.symm

AlgebraicGeometry.FormalSpace.existsUnique_continuousHom_formalSpectrumMap_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpectrumFullyFaithful.lean, line 549. References: EGA I (10.4.6), “X affine formal”.

Stacks 0AN0. Let A and C be weakly admissible topological rings over S. Every morphism f : Spf C ⟶ Spf A of affine formal algebraic spaces over S is Spf (f^♯) for a unique continuous ring map f^♯ : A → C over S.

theorem existsUnique_continuousHom_formalSpectrumMap_eq
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    {D : QuotientSystem B S hS A} {E : QuotientSystem B S hS C}
    (f : formalSpectrum E ⟶ formalSpectrum D) :
    ∃! g : ContinuousHom D E, formalSpectrumMap hA g = f

Tag 0AIG, a lemma

Tag 0AIG in the Stacks Project.

AlgebraicGeometry.FormalSpace.relativelyRepresentable_of_isAffineFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/QuasiFiniteRepresentable.lean, line 331.

Let S be a scheme contained in a big fppf site B and let f : X ⟶ Y be a morphism of presheaves on the big fppf site of S. If X is an affine formal algebraic space and f is representable by algebraic spaces and locally quasi-finite, then f is representable by schemes.

X is a sheaf of Type u, the universe of the schemes, and the hypothesis that it is an affine formal algebraic space is imposed on the sheaf obtained from it by lifting its values one universe up. Local quasi-finiteness of a morphism which is only representable by algebraic spaces is the assertion that each of its base changes along a scheme-valued point of the target, an algebraic space over S, is locally quasi-finite over that point.

theorem relativelyRepresentable_of_isAffineFormalAlgebraicSpace
    (X : Sheaf (BigFppfOver.topology B S hS) (Type u))
    (Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : X.1 ⟶ Y)
    (hX : IsAffineFormalAlgebraicSpace B S hS
      ((presheafToSheaf (BigFppfOver.topology B S hS) (Type (u + 1))).obj
        (X.1 ⋙ uliftFunctor.{u + 1, u})))
    (hf : Space.IsRepresentableByAlgebraicSpaces B S hS f)
    (hlqf : ∀ (T : BigFppfOver B S hS) (ξ : yoneda.obj T ⟶ Y),
      Space.IsLocallyQuasiFinite B S hS (pullback.fst ξ f)) :
    yoneda.relativelyRepresentable f

AlgebraicGeometry.FormalSpace.relativelyRepresentable_of_isAffineFormalAlgebraicSpaceULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/QuasiFiniteRepresentableULift.lean, line 112. The attribute's comment: “the tag read at the value universe Type (u+1), where a formal algebraic space and the affine formal algebraic spaces of its atlas of Definition 0AIM live, so that the tag applies to an atlas member. Nothing is assumed beyond the Type u reading: the smallness that one asks of its affine formal algebraic space is supplied by the set-theoretic condition of Stacks 0AIS, which an affine formal algebraic space carries, and the smallness of the base change by its being an algebraic space”.

Let S be a scheme contained in a big fppf site B, let X be an affine formal algebraic space over S and let f : X ⟶ Y be a morphism to a presheaf of Type (u + 1) on the big fppf site of S which is representable by algebraic spaces and whose represented base changes are locally quasi-finite. Then f is representable by objects of the site.

theorem relativelyRepresentable_of_isAffineFormalAlgebraicSpaceULift
    {X : FppfSheaf B S hS} {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (u + 1)} (f : X.obj ⟶ Y)
    (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hf : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f)
    (hlqf : ∀ (T : BigFppfOver B S hS) (ξ : uliftYoneda.{u + 1}.obj T ⟶ Y),
      Space.HoldsOnEveryEtaleChartULift.{u + 1} B S hS
        ((@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) ⊓
          (@AlgebraicGeometry.LocallyQuasiFinite.{u} : MorphismProperty Scheme.{u}))
        (pullback.fst ξ f)) :
    uliftYoneda.{u + 1}.relativelyRepresentable f

AlgebraicGeometry.FormalSpace.relativelyRepresentable_of_isEtale_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AtlasChartRepresentable.lean, line 49. The attribute's comment: “the case of an etale morphism, at the value universe Type (u+1) where a formal algebraic space and the affine formal algebraic spaces of its atlas of Definition 0AIM live. Nothing is assumed beyond the tag: an etale morphism of schemes is locally of finite type and locally quasi-finite by Stacks 03WS, which is the tag's hypothesis”.

A morphism g : X ⟶ Y of fppf sheaves on the big fppf site of S whose source is an affine formal algebraic space, which is representable by algebraic spaces and étale, is representable by objects of the site.

theorem relativelyRepresentable_of_isEtale_of_isAffineFormal {X Y : FppfSheaf B S hS}
    (g : X ⟶ Y) (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS g.hom)
    (het : Space.HasPropertyULift.{u + 1} B S hS
      (fun _ _ k ↦ Space.IsEtaleULift.{u + 1} B S hS k.hom) g.hom hrep) :
    uliftYoneda.{u + 1}.relativelyRepresentable g.hom

Sources

LeanAlgebraicGeometry.FormalSpace.IsAffineFormalAlgebraicSpace · AlgebraicGeometry.IsAffineFormalAlgebraicSpace · AlgebraicGeometry.FormalSpace.diagonal_isClosedImmersion · AlgebraicGeometry.FormalSpace.relativelyRepresentable_colimitι · AlgebraicGeometry.FormalSpace.isThickening_colimitι · AlgebraicGeometry.exists_factor_through_thickening' · AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_iff · AlgebraicGeometry.FormalSpace.exists_isPresentingRing_of_hasAffineClosedImmersionCriterion

Section87.10 Countably indexed affine formal algebraic spaces #

Section 87.10 of the Stacks Project, Tag 0AIH. 5 tags here are carried by 29 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AII, a lemma

Tag 0AII in the Stacks Project.

AlgebraicGeometry.exists_sequential_presentation_iff_exists_countable_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/CountablyIndexed.lean, line 75.

Stacks 0AII. A sequential affine presentation by thickenings exists exactly when a countably indexed directed affine presentation by thickenings exists.

theorem exists_sequential_presentation_iff_exists_countable_presentation
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))) :
    (∃ D : ℕ ⥤ BigAffineFppf B S hS,
      (∀ ⦃i j : ℕ⦄ (f : i ⟶ j),
        Stacks.Thickenings.IsThickening
          ((BigAffineFppf.toScheme B S hS).map (D.map f))) ∧
        Nonempty (X ≅ colimit
          (D ⋙ BigAffineFppf.inclusion B S hS ⋙
            Sheaf.sheafifiedYoneda
              (BigFppfOver.topology B S hS)))) ↔
    (∃ (I : Type (u + 1)) (pre : Preorder I),
      letI : Preorder I := pre
      Nonempty I ∧ IsDirected I (· ≤ ·) ∧ Countable I ∧
        ∃ D : I ⥤ BigAffineFppf B S hS,
          (∀ ⦃i j : I⦄ (f : i ⟶ j),
            Stacks.Thickenings.IsThickening
              ((BigAffineFppf.toScheme B S hS).map (D.map f))) ∧
            Nonempty (X ≅ colimit
              (D ⋙ BigAffineFppf.inclusion B S hS ⋙
                Sheaf.sheafifiedYoneda
                  (BigFppfOver.topology B S hS))))

AlgebraicGeometry.FormalSpace.isCountablyIndexed_iff_exists_countable_presentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablePresentation.lean, line 59.

Stacks Project, Tag 0AII. An fppf sheaf has a sequential presentation by affine schemes and thickenings if and only if it has one indexed by a countable nonempty directed preorder.

theorem isCountablyIndexed_iff_exists_countable_presentation (X : FppfSheaf B S hS) :
    IsCountablyIndexed B S hS X ↔
      ∃ (I : Type (u + 1)) (pre : Preorder I),
        letI : Preorder I := pre
        Nonempty I ∧ IsDirected I (· ≤ ·) ∧ Countable I ∧
          ∃ D : I ⥤ BigAffineFppf B S hS,
            (∀ ⦃i j : I⦄ (f : i ⟶ j),
              Stacks.Thickenings.IsThickening
                ((BigAffineFppf.toScheme B S hS).map (D.map f))) ∧
              Nonempty (X ≅ colimit
                (D ⋙ BigAffineFppf.inclusion B S hS ⋙
                  Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)))

Tag 0AIJ, a definition

Tag 0AIJ in the Stacks Project.

AlgebraicGeometry.IsCountablyIndexed, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/CountablyIndexed.lean, line 58.

Stacks 0AIJ. A sheaf on the big fppf site of S is countably indexed when it is the colimit of a sequence of sheaves represented by affine schemes whose transition morphisms are thickenings.

abbrev IsCountablyIndexed (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1))) : Prop

AlgebraicGeometry.FormalSpace.IsCountablyIndexed, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexed.lean, line 47.

Stacks 0AIJ. An fppf sheaf is countably indexed when it admits a presentation indexed by ℕ by affine schemes whose transition maps are thickenings. For an affine formal algebraic space this is the countably indexed property.

abbrev IsCountablyIndexed (X : FppfSheaf B S hS) : Prop

Tag 0AIK, a lemma

Tag 0AIK in the Stacks Project.

AlgebraicGeometry.FormalSpace.isAdicStar_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/TypeImplications.lean, line 79. The attribute's comment: “noetherian_adic_star”.

Stacks 0AIK, item (1). A Noetherian affine formal algebraic space is adic*: its presenting ring is adic, and an ideal of definition of a Noetherian ring is finitely generated.

theorem isAdicStar_of_isNoetherian {X : FppfSheaf B S hS} (hX : IsNoetherian B S hS X) :
    IsAdicStar B S hS X

AlgebraicGeometry.FormalSpace.isAdic_of_isAdicStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/TypeImplications.lean, line 91. The attribute's comment: “adic_star_adic”.

Stacks 0AIK, item (2). An adic* affine formal algebraic space is adic: adic* is adicness of the presenting ring together with the extra demand that some ideal of definition be finitely generated.

theorem isAdic_of_isAdicStar {X : FppfSheaf B S hS} (hX : IsAdicStar B S hS X) :
    IsAdic B S hS X

AlgebraicGeometry.FormalSpace.isWeaklyAdic_of_isAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/TypeImplications.lean, line 99. The attribute's comment: “adic_weakly_adic”.

Stacks 0AIK, item (3). An adic affine formal algebraic space is weakly adic, because an adic linearly topologized ring is weakly adic.

theorem isWeaklyAdic_of_isAdic {X : FppfSheaf B S hS} (hX : IsAdic B S hS X) :
    IsWeaklyAdic B S hS X

AlgebraicGeometry.FormalSpace.isClassical_of_isWeaklyAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/TypeImplications.lean, line 107. The attribute's comment: “weakly_adic_classical”.

Stacks 0AIK, item (4). A weakly adic affine formal algebraic space is classical, because a weakly adic linearly topologized ring is admissible (Stacks 0GXF).

theorem isClassical_of_isWeaklyAdic {X : FppfSheaf B S hS} (hX : IsWeaklyAdic B S hS X) :
    IsClassical B S hS X

AlgebraicGeometry.FormalSpace.isCountablyIndexed_of_isWeaklyAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/TypeImplications.lean, line 125. The attribute's comment: “weakly_adic_countable”.

Stacks 0AIK, item (5). A weakly adic affine formal algebraic space is countably indexed.

Let A be the presenting ring, W one of its weak ideals of definition, and I an ideal whose closed powers are open and form a fundamental system of neighbourhoods of 0, which is what weak adicness of A provides. The ideals W ⊓ (I ^ n)‾ are then weak ideals of definition, they decrease in n, and every weak ideal of definition contains one of them, being open. So the sequence they form is a final functor into the index of the canonical weak-ideal presentation of X, and restricting that presentation along it exhibits X as the colimit of a sequence of affine schemes whose transition morphisms are thickenings.

theorem isCountablyIndexed_of_isWeaklyAdic {X : FppfSheaf B S hS}
    (hX : IsWeaklyAdic B S hS X) : IsCountablyIndexed B S hS X

AlgebraicGeometry.FormalSpace.hasSomeSurjectivePresentation_of_isCountablyIndexed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedMcQuillan.lean, line 125. The attribute's comment: “countable_mcquillan”.

Stacks Project, Tag 0AIK, item (6). A countably indexed affine formal algebraic space is McQuillan: it has a presentation by affine thickenings all of whose section-ring projections are surjective, which is condition (4) of Stacks 0AIC.

theorem hasSomeSurjectivePresentation_of_isCountablyIndexed {X : FppfSheaf B S hS}
    (hX : IsAffineFormalAlgebraicSpace B S hS X) (hc : IsCountablyIndexed B S hS X) :
    HasSomeSurjectivePresentation B S hS X

AlgebraicGeometry.FormalSpace.isPresentingRing_of_isCountablyIndexed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedMcQuillan.lean, line 207. The attribute's comment: “(6), countably indexed implies McQuillan”.

Stacks Project, Tag 0AIK, item (6). A countably indexed affine formal algebraic space is McQuillan: it has a presentation by affine thickenings all of whose section-ring projections are surjective, which is condition (4) of Stacks 0AIC, and it is the formal spectrum of a weakly admissible topological ring, which is condition (1).

theorem isPresentingRing_of_isCountablyIndexed {X : FppfSheaf B S hS}
    (hX : IsAffineFormalAlgebraicSpace B S hS X) (hc : IsCountablyIndexed B S hS X) :
    HasSomeSurjectivePresentation B S hS X ∧
      ∃ (A : Type u) (_ : CommRing A) (_ : TopologicalSpace A) (_ : IsTopologicalRing A)
        (_ : IsLinearTopology A A), IsPresentingRing B S hS A X

Tag 0AN1, a lemma

Tag 0AN1 in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_countable_isPresentingRing_of_isCountablyIndexed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablePresentingRing.lean, line 78. The attribute's comment: “condition (1) implies condition (2), with X = Spf A read as the weak-ideal colimit presentation of Stacks 0AIC rather than as an isomorphism with a formal spectrum”.

Stacks 0AN1, condition (1) implies condition (2), in the IsPresentingRing shape. A countably indexed affine formal algebraic space over S has a presenting weakly admissible topological ring whose neighbourhood filter of zero is countably generated.

theorem exists_countable_isPresentingRing_of_isCountablyIndexed (X : FppfSheaf B S hS)
    (hX : IsAffineFormalAlgebraicSpace B S hS X) (hXc : IsCountablyIndexed B S hS X) :
    ∃ (C : Type u) (_ : CommRing C) (_ : TopologicalSpace C) (_ : IsTopologicalRing C)
      (_ : IsLinearTopology C C), IsPresentingRing B S hS C X ∧
        (nhds (0 : C)).IsCountablyGenerated

AlgebraicGeometry.FormalSpace.isCountablyIndexed_of_isPresentingRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablePresentingRing.lean, line 93. The attribute's comment: “condition (2) implies condition (1), with X = Spf A read as the weak-ideal colimit presentation of Stacks 0AIC rather than as an isomorphism with a formal spectrum”.

Stacks 0AN1, condition (2) implies condition (1), in the IsPresentingRing shape. If a weakly admissible topological ring with countably generated neighbourhood filter of zero presents X, then X is countably indexed.

theorem isCountablyIndexed_of_isPresentingRing (X : FppfSheaf B S hS) (A : Type u) [CommRing A]
    [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A]
    (hA : IsPresentingRing B S hS A X) (hc : (nhds (0 : A)).IsCountablyGenerated) :
    IsCountablyIndexed B S hS X

AlgebraicGeometry.FormalSpace.hasCountableWeakPresentation_iff_hasWeakIdealChain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedSpectrum.lean, line 249. The attribute's comment: “conditions (2) and (3)”.

Stacks 0AN1, conditions (2) and (3) are equivalent. A countably generated filter of neighbourhoods of 0 in a weakly admissible ring is based on a descending chain of weak ideals of definition, and such a chain is in particular a countable fundamental system.

theorem hasCountableWeakPresentation_iff_hasWeakIdealChain (X : FppfSheaf B S hS) :
    HasCountableWeakPresentation B S hS X ↔ HasWeakIdealChain B S hS X

AlgebraicGeometry.FormalSpace.hasWeakIdealChain_iff_hasNilpotentIdealChain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedSpectrum.lean, line 264. The attribute's comment: “conditions (3) and (4)”.

Stacks 0AN1, conditions (3) and (4) are equivalent. A chain of weak ideals of definition has locally nilpotent successive quotients because its members consist of topologically nilpotent elements; conversely, if the successive quotients are locally nilpotent then every element of a member of the chain is topologically nilpotent, so each member is a weak ideal of definition and the ring is weakly pre-admissible.

theorem hasWeakIdealChain_iff_hasNilpotentIdealChain (X : FppfSheaf B S hS) :
    HasWeakIdealChain B S hS X ↔ HasNilpotentIdealChain B S hS X

AlgebraicGeometry.FormalSpace.isLimitOfNilpotentQuotients_of_hasWeakIdealChain, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedSpectrum.lean, line 369. The attribute's comment: “condition (3) implies condition (5)”.

Stacks 0AN1, condition (3) implies condition (5). A chain of weak ideals of definition basing the topology of a weakly admissible A exhibits A itself as the inverse limit lim A/Iₙ with the limit topology, and the S-algebra of condition (5) can be taken to be A: the successive quotients Iₙ/Iₙ₊₁ are locally nilpotent, the kernels of the quotient maps are the Iₙ, and the structure morphisms of the quotient system are already indexed by weak ideals of definition, each of which contains some Iₙ.

theorem isLimitOfNilpotentQuotients_of_hasWeakIdealChain (X : FppfSheaf B S hS)
    (hX : HasWeakIdealChain B S hS X) : IsLimitOfNilpotentQuotients B S hS X

AlgebraicGeometry.FormalSpace.hasCountableWeakPresentation_of_isLimitOfNilpotentQuotients, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedSpectrum.lean, line 488. The attribute's comment: “condition (5) implies condition (2)”.

Stacks 0AN1, condition (5) implies condition (2). The presenting ring of an inverse limit presentation is weakly admissible, and the kernels of the projections are a countable fundamental system of neighbourhoods of 0.

theorem hasCountableWeakPresentation_of_isLimitOfNilpotentQuotients (X : FppfSheaf B S hS)
    (hX : IsLimitOfNilpotentQuotients B S hS X) : HasCountableWeakPresentation B S hS X

AlgebraicGeometry.FormalSpace.isCountablyIndexedAffine_of_hasCountableWeakPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedSpectrum.lean, line 623. The attribute's comment: “condition (2) implies condition (1)”.

Stacks 0AN1, condition (2) implies condition (1). The formal spectrum of a weakly admissible ring over S is an affine formal algebraic space (Stacks 0AIF) once the site is large enough, which a countable fundamental system of neighbourhoods of 0 guarantees, and it is countably indexed because such a system is cofinal in the weak ideals of definition.

theorem isCountablyIndexedAffine_of_hasCountableWeakPresentation (X : FppfSheaf B S hS)
    (hX : HasCountableWeakPresentation B S hS X) : IsCountablyIndexedAffine B S hS X

AlgebraicGeometry.FormalSpace.hasCountableWeakPresentation_of_isCountablyIndexedAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedSpectrum.lean, line 639. The attribute's comment: “condition (1) implies condition (2)”.

Stacks 0AN1, condition (1) implies condition (2). A countably indexed affine formal algebraic space is the formal spectrum of the limit of the section rings of a sequential presentation (Stacks 0AIK, item (6)); that ring is weakly admissible and the kernels of its projections are a countable fundamental system of neighbourhoods of 0.

theorem hasCountableWeakPresentation_of_isCountablyIndexedAffine (X : FppfSheaf B S hS)
    (hX : IsCountablyIndexedAffine B S hS X) : HasCountableWeakPresentation B S hS X

AlgebraicGeometry.FormalSpace.isCountablyIndexedAffine_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/CountablyIndexedSpectrum.lean, line 658.

Stacks 0AN1. For an fppf sheaf X on the big fppf site of S the following are equivalent:

X is a countably indexed affine formal algebraic space;

X = Spf A for a weakly admissible topological S-algebra A with a countable fundamental system of neighbourhoods of 0;

X = Spf A for a weakly admissible A with a descending chain of weak ideals of definition as a fundamental system of neighbourhoods of 0;

X = Spf A for a complete and separated A with a descending chain of open ideals with locally nilpotent successive quotients as a fundamental system of neighbourhoods of 0;

X = Spf A for A the inverse limit of a sequence of quotients of a ring with locally nilpotent successive quotients, with the limit topology.

theorem isCountablyIndexedAffine_tfae (X : FppfSheaf B S hS) :
    List.TFAE
      [IsCountablyIndexedAffine B S hS X,
        HasCountableWeakPresentation B S hS X,
        HasWeakIdealChain B S hS X,
        HasNilpotentIdealChain B S hS X,
        IsLimitOfNilpotentQuotients B S hS X]

Tag 0AKM, a lemma

Tag 0AKM in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasNoetherianClosedSubschemes_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionComparison.lean, line 212. The attribute's comment: “(1) ⇒ (2)”.

Stacks 0AKM, (1) ⇒ (2). Every scheme of the site admitting a closed immersion into a Noetherian affine formal algebraic space X is a Noetherian scheme.

By the implication (1) ⇒ (3) of the same tag, X has a presentation by Noetherian affine schemes. A closed immersion T ⟶ X in the sense of Stacks 0ANP is one in the sense of Stacks 0AIC, so the geometric step of Stacks 0AIC factors it through a stage of that presentation by a closed immersion of schemes T ⟶ X_λ. As X_λ is Noetherian, so is T.

theorem hasNoetherianClosedSubschemes_of_isNoetherian {X : FppfSheaf B S hS}
    (hX : IsNoetherian B S hS X) : HasNoetherianClosedSubschemes B S hS X

AlgebraicGeometry.FormalSpace.isNoetherian_tfae', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionComparison.lean, line 241.

Stacks 0AKM. For an fppf sheaf X on the big fppf site of S the following are equivalent:

X is a Noetherian affine formal algebraic space;

X is adic* and every scheme of the site closed-immersed in X is Noetherian;

X is adic* and some presentation of it by affine thickenings has Noetherian stages;

X is weakly adic and some presentation of it by affine thickenings has Noetherian stages.

Each condition already contains the requirement that X be a McQuillan affine formal algebraic space. This is the primed form of AlgebraicGeometry.FormalSpace.isNoetherian_tfae, which records the equivalence of conditions (1), (3) and (4) alone.

theorem isNoetherian_tfae' (X : FppfSheaf B S hS) :
    List.TFAE
      [IsNoetherian B S hS X,
        IsAdicStar B S hS X ∧ HasNoetherianClosedSubschemes B S hS X,
        IsAdicStar B S hS X ∧ HasNoetherianAffinePresentation B S hS X,
        IsWeaklyAdic B S hS X ∧ HasNoetherianAffinePresentation B S hS X]

AlgebraicGeometry.FormalSpace.isAdicStar_and_hasNoetherianAffinePresentation_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/NoetherianCharacterization.lean, line 311. The attribute's comment: “(1) ⇒ (3)”.

Stacks 0AKM, (1) ⇒ (3). A Noetherian affine formal algebraic space is adic* and every presentation of it by affine thickenings has Noetherian stages. Indeed an ideal of definition of a Noetherian ring is finitely generated, and every stage of a presentation is the spectrum of a quotient of the presenting ring, hence of a Noetherian ring.

theorem isAdicStar_and_hasNoetherianAffinePresentation_of_isNoetherian
    {X : FppfSheaf B S hS} (hX : IsNoetherian B S hS X) :
    IsAdicStar B S hS X ∧ HasNoetherianAffinePresentation B S hS X

AlgebraicGeometry.FormalSpace.isNoetherian_of_isAdicStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/NoetherianCharacterization.lean, line 337. The attribute's comment: “(3) ⇒ (1)”.

Stacks 0AKM, (3) ⇒ (1). An adic* affine formal algebraic space with a presentation by Noetherian affine schemes is Noetherian. Let I be a finitely generated ideal of definition of the presenting ring A. The weak ideals of definition cutting out the stages are cofinal, so one of them is contained in I; the corresponding stage being Noetherian makes A ⧸ I a quotient of a Noetherian ring, and A is I-adically complete, so Stacks 05GH makes A Noetherian.

theorem isNoetherian_of_isAdicStar {X : FppfSheaf B S hS} (hX : IsAdicStar B S hS X)
    (hpres : HasNoetherianAffinePresentation B S hS X) : IsNoetherian B S hS X

AlgebraicGeometry.FormalSpace.isWeaklyAdic_of_isAdicStar, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/NoetherianCharacterization.lean, line 363. The attribute's comment: “(3) ⇒ (4)”.

Stacks 0AKM, (3) ⇒ (4). An adic* affine formal algebraic space is weakly adic, because an adic topological ring is weakly adic.

theorem isWeaklyAdic_of_isAdicStar {X : FppfSheaf B S hS} (hX : IsAdicStar B S hS X) :
    IsWeaklyAdic B S hS X

AlgebraicGeometry.FormalSpace.isAdicStar_of_isWeaklyAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/NoetherianCharacterization.lean, line 380. The attribute's comment: “(4) ⇒ (3)”.

Stacks 0AKM, (4) ⇒ (3). A weakly adic affine formal algebraic space with a presentation by Noetherian affine schemes is adic*.

Let A be the presenting ring and I an ideal of definition, which exists because a weakly adic ring is admissible. By Stacks 0GXF the closure I₂ of I ^ 2 is open, so it is a weak ideal of definition; cofinality of the weak ideals cutting out the stages produces a stage contained in I₂, whence A ⧸ I₂ is Noetherian. The image of I in A ⧸ I₂ is then a finitely generated module, that is I / I₂ is a finite A-module, and Stacks 0GXH produces a finitely generated ideal defining the topology of A.

theorem isAdicStar_of_isWeaklyAdic {X : FppfSheaf B S hS} (hX : IsWeaklyAdic B S hS X)
    (hpres : HasNoetherianAffinePresentation B S hS X) : IsAdicStar B S hS X

AlgebraicGeometry.FormalSpace.hasNoetherianAffinePresentation_of_hasNoetherianClosedSubschemes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/NoetherianCharacterization.lean, line 424. The attribute's comment: “(2) ⇒ (3)”.

Stacks 0AKM, (2) ⇒ (3). If every scheme closed-immersed in an affine formal algebraic space X is Noetherian, then every presentation of X by affine thickenings has Noetherian stages: by Stacks 0AI9 each stage inclusion X_λ → X is a thickening, in particular a closed immersion of formal algebraic spaces, so the hypothesis applies to its source.

theorem hasNoetherianAffinePresentation_of_hasNoetherianClosedSubschemes
    {X : FppfSheaf B S hS} (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hclosed : HasNoetherianClosedSubschemes B S hS X) :
    HasNoetherianAffinePresentation B S hS X

AlgebraicGeometry.FormalSpace.isNoetherian_of_hasNoetherianClosedSubschemes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/NoetherianCharacterization.lean, line 446. The attribute's comment: “(2) ⇒ (1)”.

Stacks 0AKM, (2) ⇒ (1). An adic* affine formal algebraic space all of whose closed subschemes that are schemes are Noetherian is itself Noetherian: the stages of any presentation are such closed subschemes, so condition (3) holds and (3) ⇒ (1) applies.

theorem isNoetherian_of_hasNoetherianClosedSubschemes {X : FppfSheaf B S hS}
    (hX : IsAdicStar B S hS X) (hclosed : HasNoetherianClosedSubschemes B S hS X) :
    IsNoetherian B S hS X

AlgebraicGeometry.FormalSpace.isNoetherian_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/NoetherianCharacterization.lean, line 460. The attribute's comment: “clauses (1), (3) and (4)”.

Stacks 0AKM, conditions (1), (3) and (4). For an fppf sheaf X on the big fppf site of S the following are equivalent: X is a Noetherian affine formal algebraic space; X is adic* and has a presentation by Noetherian affine schemes; X is weakly adic and has a presentation by Noetherian affine schemes. Each condition already contains the requirement that X be a McQuillan affine formal algebraic space.

theorem isNoetherian_tfae (X : FppfSheaf B S hS) :
    List.TFAE
      [IsNoetherian B S hS X,
        IsAdicStar B S hS X ∧ HasNoetherianAffinePresentation B S hS X,
        IsWeaklyAdic B S hS X ∧ HasNoetherianAffinePresentation B S hS X]

Sources

LeanAlgebraicGeometry.exists_sequential_presentation_iff_exists_countable_presentation · AlgebraicGeometry.FormalSpace.isCountablyIndexed_iff_exists_countable_presentation · AlgebraicGeometry.IsCountablyIndexed · AlgebraicGeometry.FormalSpace.IsCountablyIndexed · AlgebraicGeometry.FormalSpace.isAdicStar_of_isNoetherian · AlgebraicGeometry.FormalSpace.isAdic_of_isAdicStar · AlgebraicGeometry.FormalSpace.isWeaklyAdic_of_isAdic · AlgebraicGeometry.FormalSpace.isClassical_of_isWeaklyAdic

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

87.2 Formal schemes à la EGA to 87.10 Countably indexed affine…

Section87.2 Formal schemes à la EGA#

Tag 0AHY, the section

Tag 0AHZ, an equation

Tag 0AI0, an equation

Tag 0AI1, a lemma

Tag 0AI2, a lemma

Tag 0AI3, a remark

Tag 0AI4, a remark

Sources

Section87.4 Topological rings and modules#

Tag 0AMR, an example

Tag 0AMS, a lemma

Tag 0ARZ, a lemma

Tag 0AMT, a lemma

Tag 0AS0, a lemma

Tag 0F1S, a lemma

Tag 0AMU, a definition

Tag 0AMV, a definition

Tag 0DCZ, a lemma

Tag 0AMW, a lemma

Tag 0AMZ, a lemma

Tag 0GB4, a lemma

Sources

Section87.5 Taut ring maps#

Tag 0AMX, a definition

Tag 0AMY, a lemma

Tag 0GX2, a lemma

Tag 0GX3, a lemma

Tag 0GX4, a lemma

Tag 0GX5, a lemma

Tag 0GX6, a lemma

Tag 0GX7, a lemma

Tag 0GX8, a lemma

Tag 0APT, a lemma

Sources

Section87.6 Adic ring maps#

Tag 0GBR, a definition

Tag 0GXA, a lemma

Tag 0GXB, a lemma

Tag 0GXC, a lemma

Tag 0APU, a lemma

Sources

Section87.7 Weakly adic rings#

Tag 0GXE, a definition

Tag 0GXF, a lemma

Tag 0GXG, a lemma

Tag 0GXH, a lemma

Tag 0GXI, a lemma

Tag 0GXJ, a lemma

Sources

Section87.8 Descending properties#

Tag 0GXL, a lemma

Tag 0GXM, a lemma

Tag 0GXN, a lemma

Tag 0GXP, a lemma

Tag 0GXQ, a lemma

Sources

Section87.9 Affine formal algebraic spaces#

Tag 0AI7, a definition

Tag 0AI8, a lemma

Tag 0AI9, a lemma

Tag 0AIA, a lemma

Tag 0AIB, a lemma

Tag 0AIC, a lemma

Tag 0AID, a definition

Tag 0AIE, a remark

Tag 0AIF, a definition

Tag 0AN0, a lemma

Tag 0AIG, a lemma

Sources

Section87.10 Countably indexed affine formal algebraic spaces#

Tag 0AII, a lemma

Tag 0AIJ, a definition

Tag 0AIK, a lemma

Tag 0AN1, a lemma

Tag 0AKM, a lemma

Sources

Section87.2 Formal schemes à la EGA #

Section87.4 Topological rings and modules #

Section87.5 Taut ring maps #

Section87.6 Adic ring maps #

Section87.7 Weakly adic rings #

Section87.8 Descending properties #

Section87.9 Affine formal algebraic spaces #

Section87.10 Countably indexed affine formal algebraic spaces #