87.29 Algebras topologically of… to 87.34 The small étale site of a…

Section87.29 Algebras topologically of finite type#

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

Tag 0ANS, a definition

Tag 0ANS in the Stacks Project.

TopologicalRing.IsTopologicallyOfFiniteType, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/FiniteType/RestrictedPowerSeries.lean, line 44.

A ring homomorphism φ : A →+* B is topologically of finite type if there is an A-algebra map from a polynomial algebra in finitely many variables to B with dense image.

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

Tag 0ANT, a lemma

Tag 0ANT in the Stacks Project.

AlgebraicGeometry.FormalSpace.isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpectrumFiniteType.lean, line 383. The attribute's comment: “the implication (1) ⟹ (2) with tautness carried as a hypothesis: for a taut continuous homomorphism of weakly admissible topological rings over S whose formal spectrum map is of finite type, the homomorphism is topologically of finite type. Tautness is not deduced from (1), and (2) ⟹ (1) is not asserted; see the module docstring.”.

Stacks 0ANT, (1) ⟹ (2), granted tautness. Let φ : A ⟶ C be a taut continuous homomorphism of weakly admissible topological rings over S. If Spf (φ) is of finite type, then C is topologically of finite type over A. Tautness is a hypothesis rather than a conclusion because this library has only one implication of Stacks 0AN5; the implication (2) ⟹ (1) is not asserted.

theorem isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (hf : RingHom.IsTaut f.toRingHom) (hFT : IsFiniteType B S hS (formalSpectrumMap hA f)) :
    TopologicalRing.IsTopologicallyOfFiniteType f.toRingHom

AlgebraicGeometry.FormalSpace.exists_isPullback_isFiniteTypeULift_formalSpectrumMap_stage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpectrumFiniteType.lean, line 416. The attribute's comment: “the stage half of the implication (2) ⟹ (1): for a homomorphism satisfying condition (a) of Stacks 0ANU — tautness together with finite type modulo every weak ideal of definition, which condition (2) implies — the base change of the formal spectrum map along the point cut out by a thickening stage is represented by an object of the site and is of finite type. Condition (1) itself quantifies over every scheme-valued point of Spf A, not only those factoring through a stage, and is not asserted; see the module docstring.”.

Stacks 0ANT, the stage half of (2) ⟹ (1). Let φ : A ⟶ C be a continuous homomorphism of weakly admissible topological rings over S which is taut and of finite type modulo every weak ideal of definition, and let I be a weak ideal of definition of A. Then the base change of Spf (φ) along the point of Spf A cut out by the thickening stage Spec (A ⧸ I) is represented by an object of the site, and the representing morphism is of finite type.

theorem exists_isPullback_isFiniteTypeULift_formalSpectrumMap_stage
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (h : TopologicalRing.FiniteTypeModuloEveryWeakIdeal f.toRingHom)
    (I : Ideal A) (hI : TopologicalRing.IsWeakIdealOfDefinition I) :
    ∃ (V : BigFppfOver B S hS)
      (p : V ⟶ (BigAffineFppf.inclusion B S hS).obj (D.stage ⟨I, hI⟩))
      (q : (uliftYoneda.{u + 1}).obj V ⟶
        (sheafToPresheaf (BigFppfOver.topology B S hS) (Type (u + 1))).obj (formalSpectrum E)),
      IsPullback q ((uliftYoneda.{u + 1}).map p)
        ((sheafToPresheaf (BigFppfOver.topology B S hS) (Type (u + 1))).map
          (formalSpectrumMap hA f))
        ((sheafifiedYonedaObjIso B S hS
            ((BigAffineFppf.inclusion B S hS).obj (D.stage ⟨I, hI⟩))).hom ≫
          (sheafToPresheaf (BigFppfOver.topology B S hS) (Type (u + 1))).map
            (formalSpectrumInclusion D ⟨I, hI⟩)) ∧
      Space.IsFiniteTypeULift.{u + 1} B S hS ((uliftYoneda.{u + 1}).map p)

AlgebraicGeometry.FormalSpace.isFiniteType_formalSpectrumMap_of_isTaut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpectrumFiniteTypeAllPoints.lean, line 189. The attribute's comment: “the implication (2) ⟹ (1): a taut continuous homomorphism of weakly admissible topological rings over S whose target is topologically of finite type over its source has formal spectrum map of finite type, at every scheme-valued point of the target and not only at those factoring through a thickening stage. That the two formal spectra are affine formal algebraic spaces is Stacks 0AIF for a weakly admissible ring and belongs to the situation of the lemma, whose condition (1) speaks of a finite type morphism of them.”.

Stacks 0ANT, the implication (2) ⟹ (1). Let φ : A ⟶ C be a continuous homomorphism of weakly admissible topological rings over S which is taut and such that C is topologically of finite type over A. Then Spf (φ) : Spf C ⟶ Spf A is of finite type.

The base change of Spf (φ) along a point of Spf A out of an affine object of the site is an affine morphism of finite type of the site, and those two properties are Zariski local at the target, so the charts over the affine opens of an arbitrary test object glue.

theorem isFiniteType_formalSpectrumMap_of_isTaut
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (hD : IsAffineFormalAlgebraicSpace B S hS (formalSpectrum D))
    (hE : IsAffineFormalAlgebraicSpace B S hS (formalSpectrum E))
    (htaut : RingHom.IsTaut f.toRingHom)
    (hfin : TopologicalRing.IsTopologicallyOfFiniteType f.toRingHom) :
    IsFiniteType B S hS (formalSpectrumMap hA f)

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteTypeAndQuasiCompact_formalSpectrumMap_of_finiteTypeModuloEveryWeakIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpectrumFiniteTypeRepresentable.lean, line 171. The attribute's comment: “the implication (2) ⟹ (1) with its conclusion unrestricted: the base change of the formal spectrum map is taken along an arbitrary scheme-valued point of Spf A, not only along one factoring through a thickening stage. Condition (1) is concluded as Definition 0AM4, part (2), verbatim; what the argument produces is condition (2) of Stacks 0AJJ — representable by algebraic spaces plus of finite type in the Bootstrap sense of Stacks 03XZ — and Stacks 0AJJ, AlgebraicGeometry.FormalSpace.isFiniteType_iff_isBootstrapFiniteType, carries it to Definition 0AM4, part (2), unconditionally. Condition (2) is taken in the form of condition (a) of Stacks 0ANU, TopologicalRing.FiniteTypeModuloEveryWeakIdeal, which is what the source's proof of this implication derives from condition (2) in its first sentence; that derivation is TopologicalRing.finiteTypeModuloEveryWeakIdeal_of_topologicallyOfFiniteType and assumes no countability, so this implication is the source's with its hypothesis weakened. Condition (a) implies condition (2) back, with no countability assumption either, by TopologicalRing.isTopologicallyOfFiniteType_of_finiteTypeModuloEveryWeakIdeal; condition (2) verbatim is the hypothesis of this implication as it appears in AlgebraicGeometry.FormalSpace.isFiniteType_formalSpectrumMap_iff_isTaut_and_isTopologicallyOfFiniteType”.

Stacks 0ANT, the implication (2) ⟹ (1). Let φ : A ⟶ C be a continuous homomorphism of weakly admissible topological rings over S which is taut and of finite type modulo every weak ideal of definition. Then Spf (φ) : Spf C ⟶ Spf A is of finite type in the sense of Definition 0AM4, part (2): locally of finite type — representable by algebraic spaces, with its base change along every scheme-valued point of Spf A a morphism of algebraic spaces which is locally of finite type — and quasi-compact in the sense of Definition 0AJC.

What the argument produces is condition (2) of Stacks 0AJJ: representability by algebraic spaces together with every base change along a scheme-valued point of Spf A being a morphism of algebraic spaces of finite type. Stacks 0AJJ, AlgebraicGeometry.FormalSpace.isFiniteType_iff_isBootstrapFiniteType, carries that to Definition 0AM4, part (2), and is unconditional.

Over a point whose source is quasi-compact the Bootstrap condition is the source's own computation, AlgebraicGeometry.FormalSpace.compactPullbackRepresentable_formalSpectrumMap; the passage to an arbitrary point is the locality of the three conditions on the target.

theorem isLocallyOfFiniteTypeAndQuasiCompact_formalSpectrumMap_of_finiteTypeModuloEveryWeakIdeal
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (h : TopologicalRing.FiniteTypeModuloEveryWeakIdeal f.toRingHom) :
    IsFiniteType' B S hS (formalSpectrumMap hA f)

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_formalSpectrumMap_of_finiteTypeModuloEveryWeakIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpectrumFiniteTypeRepresentable.lean, line 199. The attribute's comment: “the implication (2) ⟹ (1) for the local condition of Stacks 0AM4 part (1), with the base change taken along an arbitrary scheme-valued point of Spf A; condition (2) is taken in the form of condition (a) of Stacks 0ANU, as on AlgebraicGeometry.FormalSpace.isLocallyOfFiniteTypeAndQuasiCompact_formalSpectrumMap_of_finiteTypeModuloEveryWeakIdeal”.

Stacks 0ANT, the implication (2) ⟹ (1), read for the local condition: a continuous homomorphism of weakly admissible topological rings over S which is taut and of finite type modulo every weak ideal of definition has formal spectrum map locally of finite type, with the base change taken along an arbitrary scheme-valued point of Spf A.

theorem isLocallyOfFiniteType_formalSpectrumMap_of_finiteTypeModuloEveryWeakIdeal
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (h : TopologicalRing.FiniteTypeModuloEveryWeakIdeal f.toRingHom) :
    IsLocallyOfFiniteType B S hS (formalSpectrumMap hA f)

AlgebraicGeometry.FormalSpace.isTaut_and_isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpectrumFiniteTypeRepresentable.lean, line 226. The attribute's comment: “the implication (1) ⟹ (2) in full, with condition (1) read as Definition 0AM4, part (2), verbatim: both halves of condition (2) are deduced from condition (1). Tautness is the implication (1) ⟹ (3) of Stacks 0AN5, AlgebraicGeometry.FormalSpace.isTaut_of_isRepresentableByAlgebraicSpaces_formalSpectrumMap, applied to the representability by algebraic spaces that being locally of finite type contains. No hypothesis beyond the source's: that implication of Stacks 0AN5 carries no side condition, because the library's Stacks 0AKN consumes of a formal spectrum only its presentation by affine thickenings, which is its construction”.

Stacks 0ANT, the implication (1) ⟹ (2). Let φ : A ⟶ C be a continuous homomorphism of weakly admissible topological rings over S. If Spf (φ) is of finite type — Definition 0AM4, part (2), verbatim — then φ is taut and C is topologically of finite type over A.

Tautness is the implication (1) ⟹ (3) of Stacks 0AN5 applied to the representability that being locally of finite type contains, and that implication carries no side condition. Only the locally-of-finite-type half of condition (1) is used, here and in the ring-theoretic half AlgebraicGeometry.FormalSpace.finiteType_quotientMap_of_isFiniteType_formalSpectrumMap, so no comparison with condition (2) of Stacks 0AJJ is needed.

theorem isTaut_and_isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap'
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (hFT : IsFiniteType' B S hS (formalSpectrumMap hA f)) :
    RingHom.IsTaut f.toRingHom ∧
      TopologicalRing.IsTopologicallyOfFiniteType f.toRingHom

AlgebraicGeometry.FormalSpace.isFiniteType_formalSpectrumMap_iff_isTaut_and_isTopologicallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpectrumFiniteTypeRepresentable.lean, line 301. The attribute's comment: “the equivalence, with condition (1) read as Definition 0AM4, part (2), verbatim and condition (2) read verbatim as tautness together with being topologically of finite type. The forward implication is AlgebraicGeometry.FormalSpace.isTaut_and_isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap' and uses only the locally-of-finite-type half of condition (1); the backward implication goes through condition (a) of Stacks 0ANU by TopologicalRing.finiteTypeModuloEveryWeakIdeal_of_topologicallyOfFiniteType and then produces condition (2) of Stacks 0AJJ — representable by algebraic spaces plus of finite type in the Bootstrap sense of Stacks 03XZ — and reaches Definition 0AM4, part (2), through Stacks 0AJJ, AlgebraicGeometry.FormalSpace.isFiniteType_iff_isBootstrapFiniteType, which is unconditional. No countability assumption is made: condition (2) and condition (a) of Stacks 0ANU imply one another outright, by TopologicalRing.isTopologicallyOfFiniteType_of_finiteTypeModuloEveryWeakIdeal and TopologicalRing.finiteTypeModuloEveryWeakIdeal_of_topologicallyOfFiniteType. No hypothesis beyond the source's: the implication (1) ⟹ (3) of Stacks 0AN5 that the forward direction needs carries no side condition, the library's Stacks 0AKN consuming of a formal spectrum only its presentation by affine thickenings”.

Stacks 0ANT, the equivalence, with both conditions read verbatim. Let φ : A ⟶ C be a continuous homomorphism of weakly admissible topological rings over S. Then Spf (φ) is of finite type — Definition 0AM4, part (2) — exactly when φ is taut and topologically of finite type.

The forward implication is isTaut_and_isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap' and uses only the locally-of-finite-type half of condition (1). The backward implication passes through condition (a) of Stacks 0ANU by TopologicalRing.finiteTypeModuloEveryWeakIdeal_of_topologicallyOfFiniteType and then produces condition (2) of Stacks 0AJJ, reaching Definition 0AM4, part (2), through Stacks 0AJJ, AlgebraicGeometry.FormalSpace.isFiniteType_iff_isBootstrapFiniteType, which is unconditional.

Condition (2) and condition (a) of Stacks 0ANU are interchangeable here with no countability assumption, in both directions: condition (a) implies condition (2) by TopologicalRing.isTopologicallyOfFiniteType_of_finiteTypeModuloEveryWeakIdeal, for which weak pre-admissibility of the source suffices, and condition (2) implies condition (a) by TopologicalRing.finiteTypeModuloEveryWeakIdeal_of_topologicallyOfFiniteType. Condition (2) is condition (c) of Stacks 0ANU, so this identification is the half of that lemma which needs no countability; what the countable generation in the hypothesis of Stacks 0ANU — a morphism of WAdm^count — is spent on in TopologicalRing.finiteType_tfae are its conditions (b), the cofinal form of condition (a), and (d), the restricted power series presentation, and neither appears here. Both of those uses are of the source's filter, so TopologicalRing.finiteType_tfae assumes countable generation of that filter only.

Nothing beyond the source's hypotheses is assumed. The forward implication needs the implication (1) ⟹ (3) of Stacks 0AN5, which carries no side condition because the library's Stacks 0AKN consumes of a formal spectrum only its presentation by affine thickenings, AlgebraicGeometry.FormalSpace.hasThickeningPresentation_formalSpectrum.

theorem isFiniteType_formalSpectrumMap_iff_isTaut_and_isTopologicallyOfFiniteType
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E) :
    IsFiniteType' B S hS (formalSpectrumMap hA f) ↔
      RingHom.IsTaut f.toRingHom ∧
        TopologicalRing.IsTopologicallyOfFiniteType f.toRingHom

AlgebraicGeometry.FormalSpace.isTaut_and_isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/TautOfRepresentableByAlgebraicSpaces.lean, line 72. The attribute's comment: “the implication (1) ⟹ (2): for a continuous homomorphism of weakly admissible topological rings over S whose formal spectrum map is of finite type, the homomorphism is taut and is topologically of finite type. That the two formal spectra are affine formal algebraic spaces is Stacks 0AIF for a weakly admissible ring and belongs to the situation of the lemma, whose condition (1) speaks of a finite type morphism of them.”.

Let φ : A ⟶ C be a continuous homomorphism of weakly admissible topological rings over S, so that Spf A and Spf C are affine formal algebraic spaces. If Spf (φ) is of finite type, then φ is taut and C is topologically of finite type over A.

theorem isTaut_and_isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (f : ContinuousHom D E)
    (hD : IsAffineFormalAlgebraicSpace B S hS (formalSpectrum D))
    (hE : IsAffineFormalAlgebraicSpace B S hS (formalSpectrum E))
    (hFT : IsFiniteType B S hS (formalSpectrumMap hA f)) :
    RingHom.IsTaut f.toRingHom ∧
      TopologicalRing.IsTopologicallyOfFiniteType f.toRingHom

Tag 0AL1, a lemma

Tag 0AL1 in the Stacks Project.

AlgebraicGeometry.FormalSpace.finiteTypeAlgebraSystemAntiEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/FiniteTypeClassification/AntiEquivalence.lean, line 541. The attribute's comment: “anti-equivalence”.

Stacks 0AL1. Let X be a McQuillan affine formal algebraic space over S presented as the formal spectrum of a weakly admissible topological ring A, and let J be a fundamental system of weak ideals of definition of A. The category of inverse systems of finite type algebras over the quotients of J is anti-equivalent to the category of finite type morphisms to X from affine formal algebraic spaces.

noncomputable def finiteTypeAlgebraSystemAntiEquivalence
    (B : AlgebraicGeometry.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 : Sheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) (Type (u + 1)))
    (hX : HasSomeSurjectivePresentation B S hS X)
    (P : WeakIdealColimitPresentation B S hS A X)
    (I : Type v) [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)]
    (J : IdealBasis A I) :
    (FiniteTypeAlgebraSystem A I J)ᵒᵖ ≌ AffineFiniteTypeOver B S hS X

Tag 0AJK, a remark

Tag 0AJK in the Stacks Project.

AlgebraicGeometry.FormalSpace.FiniteTypeAlgebraSystem.exists_uniform_generatedBy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/UniformGenerators.lean, line 210. The attribute's comment: “part (3), the asserted sentence: for the inverse system (B_λ) of finite type A / I_λ-algebras that Stacks 0AL1 attaches to a finite type morphism Y → X = Spf(A) of affine formal algebraic spaces, there is a fixed integer r such that B_λ is generated by r elements over A / I_λ for all λ. The clause of part (3) citing Stacks 0AL1 for the presentation Y = colim Spec(B_λ) is covered by the anti-equivalence itself; the question part (3) goes on to ask, whether there is an example in which Y is not McQuillan, is a question and is not asserted anywhere.”.

Stacks 0AJK, part (3): the uniform generator bound. For an inverse system (B_λ) of finite type algebras over the quotients of A by a fundamental system of weak ideals of definition — the system Stacks 0AL1 attaches to a finite type morphism Y → Spf(A) of affine formal algebraic spaces — there is a single integer r, independent of λ, such that B_λ is generated by r elements over A / I_λ for every λ.

The index r is produced from one member of the system, chosen using nonemptiness of the index, and transported to an arbitrary member through a common upper bound.

theorem exists_uniform_generatedBy [Nonempty I] [IsDirected I (· ≤ ·)]
    (P : FiniteTypeAlgebraSystem A I J) :
    ∃ r : ℕ, ∀ i : I, P.GeneratedBy r i

AlgebraicGeometry.FormalSpace.exists_taut_formalSpectrumMap_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MorphismsIntoMcQuillanAffine.lean, line 212. The attribute's comment: “part (1), every assertion of the item: for a closed immersion f : Y → X into X = Spf(A), the source Y is McQuillan (condition (4) of Stacks 0AIC) and f corresponds to a continuous homomorphism φ : A → B of weakly admissible topological rings, Y ≅ Spf(B) with f = Spf(φ) through that isomorphism, which is taut, has closed kernel K and has dense image. The source Y is an arbitrary fppf sheaf here, which generalizes the item's affine formal algebraic space. The question the item ends with, which conditions on A force B = (A/K)^∧, is a question and is asserted nowhere. Part (2) of the remark is a question in its entirety and asserts nothing.”.

Stacks 0AJK, part (1). Let A be a weakly admissible topological ring over S whose formal spectrum X = Spf(A) is an affine formal algebraic space, and let f : Y ⟶ X be a closed immersion. Then Y is a McQuillan affine formal algebraic space, and f corresponds to a continuous homomorphism φ : A ⟶ B of weakly admissible topological rings — Y is identified with Spf(B) and f with Spf(φ) — which is taut, whose kernel is a closed ideal of A, and whose image is dense in B.

theorem exists_taut_formalSpectrumMap_of_isClosedImmersion
    (hA : TopologicalRing.IsWeaklyAdmissible A) (D : QuotientSystem B S hS A)
    (hX : _root_.AlgebraicGeometry.IsAffineFormalAlgebraicSpace B S hS (formalSpectrum D))
    {Y : FppfSheaf B S hS} (f : Y ⟶ formalSpectrum D) (hf : IsClosedImmersion B S hS f) :
    HasSomeSurjectivePresentation B S hS Y ∧
      ∃ (C : Type u) (_ : CommRing C) (_ : TopologicalSpace C) (_ : IsTopologicalRing C)
        (_ : IsLinearTopology C C) (E : QuotientSystem B S hS C),
        TopologicalRing.IsWeaklyAdmissible C ∧
          ∃ (e : Y ≅ formalSpectrum E) (g : ContinuousHom D E),
            f = e.hom ≫ formalSpectrumMap hA g ∧ RingHom.IsTaut g.toRingHom ∧
              IsClosed (RingHom.ker g.toRingHom : Set A) ∧ DenseRange g.toRingHom

AlgebraicGeometry.FormalSpace.exists_finiteTypeAlgebraSystem_uniform_generatedBy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MorphismsIntoMcQuillanAffine.lean, line 249. The attribute's comment: “part (3), every assertion of the item: a finite type morphism f : Y → X of affine formal algebraic spaces with X = Spf(A) gives Y = colim Spec(B_λ) for an object (B_λ) of the category 𝒞 of Stacks 0AL1, namely the object the anti-equivalence of Stacks 0AL1 sends to f (that functor is the colimit of the spectra of the terms), and one integer r generates every B_λ over A/I_λ. The question the item ends with, whether there is an example in which Y is not McQuillan, is a question and is asserted nowhere.”.

Stacks 0AJK, part (3). Let A be a weakly admissible topological ring over S whose formal spectrum X = Spf(A) is an affine formal algebraic space, let (I_λ) be a fundamental system of weak ideals of definition of A, and let f : Y ⟶ X be a morphism of finite type from an affine formal algebraic space. Then Y = colim Spec(B_λ) for an object (B_λ) of the category 𝒞 of Stacks 0AL1 — the inverse system which the anti-equivalence of Stacks 0AL1 sends to f — and there is a single integer r such that B_λ is generated by r elements over A/I_λ for every λ.

theorem exists_finiteTypeAlgebraSystem_uniform_generatedBy
    (hA : TopologicalRing.IsWeaklyAdmissible A) (D : QuotientSystem B S hS A)
    (hX : _root_.AlgebraicGeometry.IsAffineFormalAlgebraicSpace B S hS (formalSpectrum D))
    (I : Type v) [Preorder I] [Nonempty I] [IsDirected I (· ≤ ·)] (J : IdealBasis A I)
    {Y : FppfSheaf B S hS} (hY : _root_.AlgebraicGeometry.IsAffineFormalAlgebraicSpace B S hS Y)
    (f : Y ⟶ formalSpectrum D) (hf : IsFiniteType B S hS f) :
    ∃ P : FiniteTypeAlgebraSystem A I J,
      Nonempty ((finiteTypeAlgebraSystemAntiEquivalence B S hS A hA (formalSpectrum D)
          (hasSomeSurjectivePresentation_formalSpectrum_of_isAffine B S hS hA D hX)
          D.weakIdealColimitPresentation I J).functor.obj (Opposite.op P) ≅
            ⟨Over.mk f, hY, hf⟩) ∧
        ∃ r : ℕ, ∀ i : I, P.GeneratedBy r i

AlgebraicGeometry.FormalSpace.exists_taut_isTopologicallyOfFiniteType_affineSpace_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MorphismsIntoMcQuillanAffine.lean, line 286. The attribute's comment: “part (4), every assertion of the item: for a finite type f : Y → X = Spf(A) with Y McQuillan, f corresponds to a continuous homomorphism φ : A → B of weakly admissible topological rings, Y ≅ Spf(B) with f = Spf(φ) through that isomorphism; φ is taut, which is derived from f being of finite type through Stacks 0AN5 and 0AKN; B is topologically of finite type over A; and f factors as Y → 𝔸ʳ_X → X with 𝔸ʳ_X = Spf A{x_1, ..., x_r} the formal spectrum of the completion of A[x_1, ..., x_r] over the weak ideals of definition of A, the second arrow Spf of the canonical map and the first a closed immersion, both its source and its target being McQuillan affine formal algebraic spaces. The item's closing remark that questions (1) and (2) are then in force for Y → 𝔸ʳ_X asserts nothing further.”.

Stacks 0AJK, part (4). Let A be a weakly admissible topological ring over S whose formal spectrum X = Spf(A) is an affine formal algebraic space, and let f : Y ⟶ X be a morphism of finite type with Y a McQuillan affine formal algebraic space. Then f corresponds to a continuous homomorphism φ : A ⟶ B of weakly admissible topological rings — Y is identified with Spf(B) and f with Spf(φ) — which is taut and makes B topologically of finite type over A. In other words f factors as Y ⟶ 𝔸ʳ_X ⟶ X, where 𝔸ʳ_X = Spf A{x₁, …, xᵣ} maps to X by Spf of the canonical homomorphism and the first arrow is a closed immersion of McQuillan affine formal algebraic spaces.

theorem exists_taut_isTopologicallyOfFiniteType_affineSpace_factorization
    (hA : TopologicalRing.IsWeaklyAdmissible A) (D : QuotientSystem B S hS A)
    (hX : _root_.AlgebraicGeometry.IsAffineFormalAlgebraicSpace B S hS (formalSpectrum D))
    {Y : FppfSheaf B S hS} (hYM : HasSomeSurjectivePresentation B S hS Y)
    (f : Y ⟶ formalSpectrum D) (hf : IsFiniteType B S hS f) :
    ∃ (C : Type u) (_ : CommRing C) (_ : TopologicalSpace C) (_ : IsTopologicalRing C)
      (_ : IsLinearTopology C C) (E : QuotientSystem B S hS C),
      TopologicalRing.IsWeaklyAdmissible C ∧
        ∃ (e : Y ≅ formalSpectrum E) (g : ContinuousHom D E),
          f = e.hom ≫ formalSpectrumMap hA g ∧ RingHom.IsTaut g.toRingHom ∧
            TopologicalRing.IsTopologicallyOfFiniteType g.toRingHom ∧
            ∃ (r : ℕ) (E' : QuotientSystem B S hS
                (TopologicalRing.CompletionOver (MvPolynomial.C : A →+* MvPolynomial (Fin r) A)))
              (π : ContinuousHom D E') (ι : ContinuousHom E' E),
              π.toRingHom = TopologicalRing.CompletionOver.canonicalMap MvPolynomial.C ∧
                HasSomeSurjectivePresentation B S hS (formalSpectrum E') ∧
                IsClosedImmersion B S hS (formalSpectrumMap
                  (TopologicalRing.completionOver_isWeaklyAdmissible MvPolynomial.C hA) ι) ∧
                f = e.hom ≫ formalSpectrumMap
                  (TopologicalRing.completionOver_isWeaklyAdmissible MvPolynomial.C hA) ι ≫
                    formalSpectrumMap hA π

Declarations registered for the tag:

• finiteTypeAlgebraSystemAntiEquivalence registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/UniformGenerators.lean, line 226 (StacksFrontier): “part (3), the clause citing Stacks 0AL1: a morphism f : Y → X = Spf(A) of affine formal algebraic spaces which is of finite type corresponds to an object (B_λ) of the category 𝒞, so that Y = colim Spec(B_λ). The uniform bound part (3) asserts next, that one integer r generates every B_λ over A/I_λ, is AlgebraicGeometry.FormalSpace.FiniteTypeAlgebraSystem.exists_uniform_generatedBy in this file. The question part (3) closes with, whether there is an example in which Y is not McQuillan, is a question and is asserted nowhere.”.
• hasSomeSurjectivePresentation_of_isClosedImmersion registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionMcQuillan.lean, line 160 (StacksFrontier): “part (1), the conclusion that Y is McQuillan: the source of a closed immersion of formal algebraic spaces whose target is a McQuillan affine formal algebraic space is again a McQuillan affine formal algebraic space. Part (1)'s conclusions about the presenting homomorphism φ : A → B are tagged separately. The question part (1) raises, which conditions on A force B = (A/K)^∧, is a question and is asserted nowhere.”.
• isClosed_ker_toRingHom registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionMcQuillan.lean, line 331 (StacksFrontier): “part (1), the conclusion that the kernel K ⊂ A of the homomorphism φ : A → B presenting a closed immersion is a closed ideal. It is proved here in the stronger form that needs only continuity of the homomorphism and separatedness of its target, so no closed-immersion hypothesis appears.”.
• denseRange_of_isClosedImmersion_formalSpectrumMap registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionMcQuillan.lean, line 391 (StacksFrontier): “part (1), the conclusion that the image φ(A) of the homomorphism φ : A → B presenting a closed immersion is dense in B. Whether φ is moreover surjective and open, equivalently whether B is the quotient A/K itself, is the question part (2) of the remark raises and is asserted nowhere.”.
• hasSomeSurjectivePresentation_of_isClosedImmersion registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionMcQuillanRefined.lean, line 46 (StacksFrontier): “part (1), the conclusion that Y is McQuillan: the source of a closed immersion of formal algebraic spaces whose target is a McQuillan affine formal algebraic space is again a McQuillan affine formal algebraic space. Part (1)'s three conclusions about the presenting homomorphism φ : A → B — that it is taut, that its kernel K is closed and that its image is dense — are tagged separately on AlgebraicGeometry.FormalSpace.isTaut_of_isClosedImmersion_formalSpectrumMap, AlgebraicGeometry.FormalSpace.isClosed_ker_toRingHom and AlgebraicGeometry.FormalSpace.denseRange_of_isClosedImmersion_formalSpectrumMap. The question part (1) raises, which conditions on A force B = (A/K)^∧, is a question and is asserted nowhere.”.
• isClosed_ker_toRingHom registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionMcQuillanRefined.lean, line 72 (StacksFrontier): “part (1), the conclusion that the kernel K ⊂ A of the homomorphism φ : A → B presenting a closed immersion is a closed ideal. It is proved here in the stronger form that needs only continuity of the homomorphism and separatedness of its target, so no closed-immersion hypothesis appears.”.
• denseRange_of_isClosedImmersion_formalSpectrumMap registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionMcQuillanRefined.lean, line 78 (StacksFrontier): “part (1), the conclusion that the image φ(A) of the homomorphism φ : A → B presenting a closed immersion is dense in B. Whether φ is moreover surjective and open, equivalently whether B is the quotient A/K itself, is the question part (2) of the remark raises and is asserted nowhere.”.
• isTaut_of_isClosedImmersion_formalSpectrumMap registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionMcQuillanRefined.lean, line 100 (StacksFrontier): “part (1), the conclusion that the homomorphism φ : A → B presenting a closed immersion is taut.”.
• exists_formalSpectrumMap_of_isClosedImmersion registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionMcQuillanRefined.lean, line 228 (StacksFrontier): “part (1), the conclusion that f corresponds to a continuous homomorphism φ : A → B of weakly admissible topological rings: a closed immersion f into X = Spf(A) whose source Y is a formal algebraic space is Spf(φ) for a weakly admissible B presenting Y, read through the identification of Y with Spf(B). The three conclusions part (1) draws about φ are tagged on AlgebraicGeometry.FormalSpace.isTaut_of_isClosedImmersion_formalSpectrumMap, AlgebraicGeometry.FormalSpace.isClosed_ker_toRingHom and AlgebraicGeometry.FormalSpace.denseRange_of_isClosedImmersion_formalSpectrumMap, and that Y is McQuillan on AlgebraicGeometry.FormalSpace.hasSomeSurjectivePresentation_of_isClosedImmersion.”.
• isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/SpectrumFiniteType.lean, line 393 (StacksFrontier): “part (4), the conclusion that B is topologically of finite type over A for a finite type f : Y → X with Y McQuillan, and with it part (4)'s restatement that f factors as Y → A^r_X → X with the first arrow a closed immersion: the conclusion TopologicalRing.IsTopologicallyOfFiniteType produces the integer r together with a homomorphism A[x_1, ..., x_r] → B restricting to φ on constants and having dense image, which is that factorization and the dense image of its first arrow. Tautness of φ, part (4)'s other conclusion, is carried here as a hypothesis rather than deduced, as the clause of Stacks 0ANT on this declaration records. Part (4) closes by observing that questions (1) and (2) are then in force for Y → A^r_X; those are questions and are asserted nowhere.”.
• isTaut_and_isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap' registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/SpectrumFiniteTypeRepresentable.lean, line 239 (StacksFrontier): “part (4), both of its conclusions, for a finite type f : Y → X with Y McQuillan: the homomorphism f comes from is taut, and its target is topologically of finite type over its source -- φ : A → B in the source's letters, φ : A ⟶ C here, the formal spectrum of a weakly admissible topological ring being McQuillan by construction. With the second goes part (4)'s restatement that f factors as Y → A^r_X → X with the first arrow a closed immersion: the conclusion TopologicalRing.IsTopologicallyOfFiniteType produces the integer r together with a homomorphism A[x_1, ..., x_r] → C restricting to φ on constants and having dense image, which is that factorization and the dense image of its first arrow. Neither conclusion is carried as a hypothesis: tautness is deduced from finite type, by the implication (1) ⟹ (3) of Stacks 0AN5. Part (4) closes by observing that questions (1) and (2) are then in force for Y → A^r_X; those are questions and are asserted nowhere.”.
• isTaut_and_isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/TautOfRepresentableByAlgebraicSpaces.lean, line 87 (StacksFrontier): “part (4) in full. For a finite type f : Y → X with Y McQuillan, the homomorphism φ : A → B presenting f is taut and B is topologically of finite type over A, which are part (4)'s two conclusions; and with the second comes part (4)'s restatement that f factors as Y → A^r_X → X with the first arrow a closed immersion of McQuillan affine formal algebraic spaces, since TopologicalRing.IsTopologicallyOfFiniteType produces the integer r together with a homomorphism A[x_1, ..., x_r] → B restricting to φ on constants and having dense image, which is that factorization and the dense image of its first arrow. Part (4) closes by observing that questions (1) and (2) are then in force for Y → A^r_X; those are questions and are asserted nowhere.”.

Tag 0AQI, a lemma

Tag 0AQI in the Stacks Project.

AlgebraicGeometry.FormalSpace.isCountablyIndexedAffine_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionCountablyIndexed.lean, line 118. The attribute's comment: “that Y is a countably indexed affine formal algebraic space”.

Stacks 0AQI, the first conclusion. The source of a closed immersion of fppf sheaves over S whose target is a countably indexed affine formal algebraic space is again a countably indexed affine formal algebraic space.

theorem isCountablyIndexedAffine_of_isClosedImmersion {X Y : FppfSheaf B S hS}
    (hX : IsCountablyIndexedAffine B S hS X) (f : Y ⟶ X)
    (hf : IsClosedImmersion B S hS f) :
    IsCountablyIndexedAffine B S hS Y

AlgebraicGeometry.FormalSpace.exists_spfPresentation_continuousHom_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionCountablyIndexed.lean, line 151. The attribute's comment: “that f corresponds to a morphism of WAdm^count”.

Stacks 0AQI, the correspondence part of the second conclusion. A closed immersion f : Y ⟶ X of fppf sheaves over S whose target is a countably indexed affine formal algebraic space is, after identifying X with Spf A and Y with Spf C for objects A and C of WAdm^count, the formal spectrum of a continuous homomorphism A ⟶ C over S, itself again a closed immersion.

theorem exists_spfPresentation_continuousHom_of_isClosedImmersion {X Y : FppfSheaf B S hS}
    (hX : IsCountablyIndexedAffine B S hS X) (f : Y ⟶ X)
    (hf : IsClosedImmersion B S hS f) :
    ∃ (P : SpfPresentation B S hS X) (Q : SpfPresentation B S hS Y)
      (hA : TopologicalRing.IsWeaklyAdmissible P.ring),
      (nhds (0 : P.ring)).IsCountablyGenerated ∧
      TopologicalRing.IsWeaklyAdmissible Q.ring ∧
      (nhds (0 : Q.ring)).IsCountablyGenerated ∧
      ∃ (eX : X ≅ formalSpectrum P.system) (eY : Y ≅ formalSpectrum Q.system)
        (g : ContinuousHom P.system Q.system),
        IsClosedImmersion B S hS (formalSpectrumMap hA g) ∧
          f = eY.hom ≫ formalSpectrumMap hA g ≫ eX.inv

AlgebraicGeometry.FormalSpace.isClosed_ker_and_quotientKerEquiv_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionCountablyIndexed.lean, line 196. The attribute's comment: “the quotient by a closed ideal, given the tautness of Stacks 0AN5”.

Stacks 0AQI, the quotient part of the second conclusion. Let A be an object of WAdm^count, that is, a weakly admissible topological ring over S with a countable fundamental system of neighbourhoods of 0, let C be weakly admissible, and let g : A ⟶ C be a continuous homomorphism over S whose formal spectrum is a closed immersion. If g is taut, then K = ker g is a closed ideal of A and g identifies A/K with C topologically, so the closed immersion is Spf of A ⟶ A/K.

Tautness is the one hypothesis not proved here: it is the implication (1) ⟹ (3) of Stacks 0AN5, which this library does not carry. Everything else is proved.

theorem isClosed_ker_and_quotientKerEquiv_of_isClosedImmersion
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (hC : TopologicalRing.IsWeaklyAdmissible C)
    (hcount : (nhds (0 : A)).IsCountablyGenerated)
    {D : QuotientSystem B S hS A} {E : QuotientSystem B S hS C} (g : ContinuousHom D E)
    (hg : IsClosedImmersion B S hS (formalSpectrumMap hA g))
    (htaut : RingHom.IsTaut g.toRingHom) :
    IsClosed (RingHom.ker g.toRingHom : Set A) ∧
      ∃ e : (A ⧸ RingHom.ker g.toRingHom) ≃+* C,
        (∀ a : A, e (Ideal.Quotient.mk (RingHom.ker g.toRingHom) a) = g.toRingHom a) ∧
          IsHomeomorph e

AlgebraicGeometry.FormalSpace.isCountablyIndexedAffine_and_exists_closedIdealQuotient_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionCountablyIndexed.lean, line 235. The attribute's comment: “given the tautness of Stacks 0AN5”.

Stacks 0AQI in full, given the implication (1) ⟹ (3) of Stacks 0AN5 as the hypothesis hAN5. Let X be a countably indexed affine formal algebraic space over S and let f : Y ⟶ X be a closed immersion of fppf sheaves over S. Then Y is a countably indexed affine formal algebraic space, and f is Spf of a continuous homomorphism g : A ⟶ C of objects of WAdm^count whose kernel K is a closed ideal of A and which identifies A/K with C topologically; that is, f corresponds to A ⟶ A/K.

The hypothesis hAN5 is exactly the implication of Stacks 0AN5 that a continuous homomorphism of weakly admissible topological rings over S whose formal spectrum is a closed immersion — hence representable by algebraic spaces — is taut. It is the one input this library does not carry; the unconditional halves of the lemma are AlgebraicGeometry.FormalSpace.isCountablyIndexedAffine_of_isClosedImmersion and AlgebraicGeometry.FormalSpace.exists_spfPresentation_continuousHom_of_isClosedImmersion.

theorem isCountablyIndexedAffine_and_exists_closedIdealQuotient_of_isClosedImmersion
    (hAN5 : ∀ {A C : Type u} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
      [IsLinearTopology A A] [CommRing C] [TopologicalSpace C] [IsTopologicalRing C]
      [IsLinearTopology C C] (hA : TopologicalRing.IsWeaklyAdmissible A)
      (_hC : TopologicalRing.IsWeaklyAdmissible C)
      {D : QuotientSystem B S hS A} {E : QuotientSystem B S hS C} (g : ContinuousHom D E),
      IsClosedImmersion B S hS (formalSpectrumMap hA g) → RingHom.IsTaut g.toRingHom)
    {X Y : FppfSheaf B S hS} (hX : IsCountablyIndexedAffine B S hS X) (f : Y ⟶ X)
    (hf : IsClosedImmersion B S hS f) :
    IsCountablyIndexedAffine B S hS Y ∧
      ∃ (P : SpfPresentation B S hS X) (Q : SpfPresentation B S hS Y)
        (hA : TopologicalRing.IsWeaklyAdmissible P.ring),
        (nhds (0 : P.ring)).IsCountablyGenerated ∧
        TopologicalRing.IsWeaklyAdmissible Q.ring ∧
        ∃ (eX : X ≅ formalSpectrum P.system) (eY : Y ≅ formalSpectrum Q.system)
          (g : ContinuousHom P.system Q.system),
          IsClosed (RingHom.ker g.toRingHom : Set P.ring) ∧
          (∃ e : (P.ring ⧸ RingHom.ker g.toRingHom) ≃+* Q.ring,
            (∀ a : P.ring,
              e (Ideal.Quotient.mk (RingHom.ker g.toRingHom) a) = g.toRingHom a) ∧
            IsHomeomorph e) ∧
          f = eY.hom ≫ formalSpectrumMap hA g ≫ eX.inv

AlgebraicGeometry.FormalSpace.IsClosedImmersion.isCountablyIndexedAffine_and_exists_closedIdealQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionCountablyIndexedQuotient.lean, line 44.

Let X be a countably indexed affine formal algebraic space over S and let f : Y ⟶ X be a closed immersion of fppf sheaves over S. Then Y is a countably indexed affine formal algebraic space, and f is Spf of a continuous homomorphism g : A ⟶ C of objects of WAdm^count whose kernel K is a closed ideal of A and which identifies A/K with C topologically; that is, f corresponds to A ⟶ A/K.

theorem IsClosedImmersion.isCountablyIndexedAffine_and_exists_closedIdealQuotient
    {X Y : FppfSheaf B S hS} (hX : IsCountablyIndexedAffine B S hS X) (f : Y ⟶ X)
    (hf : IsClosedImmersion B S hS f) :
    IsCountablyIndexedAffine B S hS Y ∧
      ∃ (P : SpfPresentation B S hS X) (Q : SpfPresentation B S hS Y)
        (hA : TopologicalRing.IsWeaklyAdmissible P.ring),
        (nhds (0 : P.ring)).IsCountablyGenerated ∧
        TopologicalRing.IsWeaklyAdmissible Q.ring ∧
        ∃ (eX : X ≅ formalSpectrum P.system) (eY : Y ≅ formalSpectrum Q.system)
          (g : ContinuousHom P.system Q.system),
          IsClosed (RingHom.ker g.toRingHom : Set P.ring) ∧
          (∃ e : (P.ring ⧸ RingHom.ker g.toRingHom) ≃+* Q.ring,
            (∀ a : P.ring,
              e (Ideal.Quotient.mk (RingHom.ker g.toRingHom) a) = g.toRingHom a) ∧
            IsHomeomorph e) ∧
          f = eY.hom ≫ formalSpectrumMap hA g ≫ eX.inv

AlgebraicGeometry.FormalSpace.isClosed_ker_and_quotientKerEquiv_of_isClosedImmersion', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ClosedImmersionCountablyIndexedRefined.lean, line 62. The attribute's comment: “the quotient by a closed ideal”.

Let A be an object of WAdm^count, that is, a weakly admissible topological ring over S with a countable fundamental system of neighbourhoods of 0, let C be weakly admissible, and let g : A ⟶ C be a continuous homomorphism over S whose formal spectrum is a closed immersion. Then K = ker g is a closed ideal of A and g identifies A/K with C topologically, so the closed immersion is Spf of A ⟶ A/K.

theorem isClosed_ker_and_quotientKerEquiv_of_isClosedImmersion'
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (hC : TopologicalRing.IsWeaklyAdmissible C)
    (hcount : (nhds (0 : A)).IsCountablyGenerated)
    {D : QuotientSystem B S hS A} {E : QuotientSystem B S hS C} (g : ContinuousHom D E)
    (hg : IsClosedImmersion B S hS (formalSpectrumMap hA g)) :
    IsClosed (RingHom.ker g.toRingHom : Set A) ∧
      ∃ e : (A ⧸ RingHom.ker g.toRingHom) ≃+* C,
        (∀ a : A, e (Ideal.Quotient.mk (RingHom.ker g.toRingHom) a) = g.toRingHom a) ∧
          IsHomeomorph e

AlgebraicGeometry.FormalSpace.hasSurjectiveOnPullbackCharts_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/RigSurjectiveClosedImmersionCharts.lean, line 675. The attribute's comment: “the surjectivity clause alone, on the pullback charts of a closed immersion, carrying nothing: the chart map is a closed immersion by Stacks 0GHX, conjugation by the presenting isomorphisms of the two charts preserves that, the implication (1) implies (3) of Stacks 0AN5 makes the chart homomorphism taut -- its two HasLargeSite conditions being free on chart rings, which are adic and carry quotient systems, by mk_lt_cutoff_of_quotientSystem_of_isAdic and hasLargeSite_of_mk_lt_cutoff -- and the quotient part of Stacks 0AQI, isClosed_ker_and_quotientKerEquiv_of_isClosedImmersion, turns the tautness into the presentation of the chart ring as a quotient. The adic and topologically finite type clauses of Stacks 0AQI are not asserted”.

The chart homomorphisms of a closed immersion are surjective, carrying nothing beyond the closed immersion itself. This is the surjectivity clause of Stacks 0AQI on the pullback charts of f.

The chart map t : U ⟶ V is a closed immersion because closed immersions are stable under base change (Stacks 0GHX, AlgebraicGeometry.FormalSpace.isClosedImmersion_of_isPullback), and conjugating it by the presenting isomorphisms of the two charts leaves a closed immersion, an isomorphism square being cartesian; so Spf g is a closed immersion. Its representability is the first component of the closed-immersion predicate of Stacks 0ANP, so the implication (1) ⟹ (3) of Stacks 0AN5, AlgebraicGeometry.FormalSpace.isTaut_of_isRepresentableByAlgebraicSpacesULift_formalSpectrumMap, makes g taut. That implication carries the two set-theoretic conditions AlgebraicGeometry.FormalSpace.QuotientSystem.HasLargeSite, and both are free here: the chart rings are Noetherian with adic topologies carrying quotient systems, so AlgebraicGeometry.FormalSpace.mk_lt_cutoff_of_quotientSystem_of_isAdic bounds each by the cutoff of the site and AlgebraicGeometry.FormalSpace.hasLargeSite_of_mk_lt_cutoff supplies the condition. This is why the surjectivity clause of Stacks 0AQI is not a missing input: it is blocked on nothing.

The passage from tautness to the presentation of the chart ring as a quotient is then the quotient part of Stacks 0AQI, AlgebraicGeometry.FormalSpace.isClosed_ker_and_quotientKerEquiv_of_isClosedImmersion, whose remaining inputs are free as well: the source is adic, so the powers of an ideal of definition are a countable fundamental system of neighbourhoods of zero, and the target is weakly admissible by TopologicalRing.isWeaklyAdmissible_of_isAdic applied to the ideal of definition for which it is adically complete. Surjectivity is read off the resulting ring equivalence A ⧸ ker g ≃+* C, which agrees with g on representatives.

theorem hasSurjectiveOnPullbackCharts_of_isClosedImmersion {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hf : IsClosedImmersion B S hS f) :
    HasSurjectiveOnPullbackCharts B S hS f

Tag 0ANU, a lemma

Tag 0ANU in the Stacks Project.

TopologicalRing.finiteType_tfae', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/FiniteType/Equivalences.lean, line 684. The attribute's comment: “equivalent_conditions”.

The four finite-type conditions for a morphism of countably indexed weakly admissible rings are equivalent.

Stacks 0ANU states this for an arrow of WAdm^count, both rings weakly admissible with a countable fundamental system of neighbourhoods of zero. Countable generation is assumed here of the source only, which is strictly weaker and so covers every arrow of WAdm^count. The hypothesis is spent twice and both times on the source: on condition (b), the cofinal form, by finiteTypeModuloEveryWeakIdeal_to_cofinal, and on condition (d), the restricted power series presentation, by restrictedPowerSeriesPresentation_of_taut_dense. Condition (c) costs no countability at all — it is condition (2) of Stacks 0ANT verbatim, and isTopologicallyOfFiniteType_of_finiteTypeModuloEveryWeakIdeal gets it from condition (a) for any weakly pre-admissible source.

public theorem finiteType_tfae' (φ : B →+* A) (hφ : Continuous φ)
    (hB : TopologicalRing.IsWeaklyAdmissible B)
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (hBcount : (nhds (0 : B)).IsCountablyGenerated) :
    List.TFAE [
      FiniteTypeModuloEveryWeakIdeal φ,
      FiniteTypeModuloCofinalWeakIdeals φ,
      RingHom.IsTaut φ ∧ TopologicalRing.IsTopologicallyOfFiniteType φ,
      HasRestrictedPowerSeriesPresentation φ]

TopologicalRing.topologicallyFiniteType_localizationPreserves, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/FiniteTypeIsLocal.lean, line 329. The attribute's comment: “local_property”.

Tautness together with topological finite type ascends along a completed étale localization diagram of countably indexed weakly admissible rings.

public theorem topologicallyFiniteType_localizationPreserves :
    LocalizationPreserves.{u} IsCountablyWeaklyAdmissible
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
        (f : B →+* A) ↦ RingHom.IsTaut f ∧ IsTopologicallyOfFiniteType f)

TopologicalRing.topologicallyFiniteType_faithfullyFlatDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/FiniteTypeIsLocal.lean, line 345. The attribute's comment: “local_property”.

Tautness together with topological finite type descends along a completed étale localization diagram whose upper horizontal ring map is faithfully flat.

public theorem topologicallyFiniteType_faithfullyFlatDescent :
    FaithfullyFlatDescent.{u} IsCountablyWeaklyAdmissible
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
        (f : B →+* A) ↦ RingHom.IsTaut f ∧ IsTopologicallyOfFiniteType f)

TopologicalRing.topologicallyFiniteType_finiteProductPreserves, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/FiniteTypeIsLocal.lean, line 426. The attribute's comment: “local_property”.

Tautness together with topological finite type is preserved by finite products of targets.

public theorem topologicallyFiniteType_finiteProductPreserves :
    FiniteProductPreserves.{u} IsCountablyWeaklyAdmissible
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
        (f : B →+* A) ↦ RingHom.IsTaut f ∧ IsTopologicallyOfFiniteType f)

TopologicalRing.topologicallyFiniteType_propertyIsLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/FiniteTypeIsLocal.lean, line 439. The attribute's comment: “local_property”.

Tautness together with topological finite type is a local property of morphisms of countably indexed weakly admissible topological rings.

public theorem topologicallyFiniteType_propertyIsLocal :
    PropertyIsLocal.{u}
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
        (f : B →+* A) ↦ RingHom.IsTaut f ∧ IsTopologicallyOfFiniteType f)

TopologicalRing.topologicallyFiniteType_isomorphismInvariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/FiniteTypeIsLocalRefined.lean, line 146. The attribute's comment: “local_property”.

Tautness together with topological finite type is independent of the presentations of the source and the target.

public theorem topologicallyFiniteType_isomorphismInvariant :
    IsomorphismInvariant.{u}
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
        (f : B →+* A) ↦ RingHom.IsTaut f ∧ IsTopologicallyOfFiniteType f)
      IsCountablyWeaklyAdmissible

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

Tautness together with topological finite type is a local property of morphisms of countably indexed weakly admissible topological rings.

public theorem topologicallyFiniteType_propertyIsLocal' :
    PropertyIsLocal'.{u}
      (fun {B A : Type u} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
        [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
        (f : B →+* A) ↦ RingHom.IsTaut f ∧ IsTopologicallyOfFiniteType f)

Tag 0CB6, a lemma

Tag 0CB6 in the Stacks Project.

TopologicalRing.finiteTypeModuloEveryWeakIdeal_iff_exists_idealOfDefinition, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AdicTopology/FiniteType/IdealOfDefinition.lean, line 46.

For a pre-admissible source, finite type modulo every weak ideal of definition is equivalent to finite type modulo some ideal of definition, with tautness in both conditions.

public lemma finiteTypeModuloEveryWeakIdeal_iff_exists_idealOfDefinition
    {B A : Type*} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
    [IsLinearTopology B B] [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A] [IsLinearTopology A A]
    (φ : B →+* A) (hB : TopologicalRing.IsPreAdmissible B) :
    TopologicalRing.FiniteTypeModuloEveryWeakIdeal φ ↔
      (RingHom.IsTaut φ ∧
        ∃ J : Ideal B, TopologicalRing.IsIdealOfDefinition J ∧
          (Ideal.quotientMap (I := J) (Ideal.closure (J.map φ)) φ
            (Ideal.map_le_iff_le_comap.mp subset_closure)).FiniteType)

Tag 0ANV, a lemma

Tag 0ANV in the Stacks Project.

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_tfae_of_isAffineFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeCharacterizationAffine.lean, line 115. The attribute's comment: “the equivalence at the source's hypotheses: f an arbitrary morphism of affine formal algebraic spaces with countably indexed target. Countable indexing of the source is derived from condition (1) by Stacks 0AKN and Stacks 0AKP, the presentations as formal spectra by Stacks 0AN1 and the presenting homomorphism by Stacks 0AN0. Condition (3) is the existence of such presentations of X and Y by rings of WAdm^count and of a continuous homomorphism with formal spectrum map f satisfying the conditions of Stacks 0ANU, in the forms (a) and (c)”.

Stacks 0ANV. Let f : X ⟶ Y be a morphism of affine formal algebraic spaces over S with Y countably indexed. Then f being locally of finite type, f being of finite type in the sense of Definition 0AM4, part (2), and f corresponding to a morphism B → A of WAdm^{count} satisfying the equivalent conditions of Stacks 0ANU — taken in the two forms (a), of finite type modulo every weak ideal of definition, and (c), taut and topologically of finite type — are all equivalent.

As in the source, the source X is not assumed countably indexed. If f is locally of finite type it is representable by algebraic spaces, hence affine by Stacks 0AKN, and X is then countably indexed by Stacks 0AKP; the two steps together are clause (1) of Stacks 0AKQ, AlgebraicGeometry.FormalSpace.isCountablyIndexed_of_isRepresentable'. Both spaces are then formal spectra of rings of WAdm^{count} by Stacks 0AN1, AlgebraicGeometry.FormalSpace.exists_quotientSystem_of_isCountablyIndexed, and f is the formal spectrum map of a continuous homomorphism by Stacks 0AN0, AlgebraicGeometry.FormalSpace.existsUnique_continuousHom_formalSpectrumMap_eq. The equivalence for that homomorphism is Stacks 0ANT together with Stacks 0ANU, in the form AlgebraicGeometry.FormalSpace.formalSpectrumMap_finiteType_tfae_countablyWeaklyAdmissible. Being locally of finite type upgrades to being of finite type by Stacks 0AKN, AlgebraicGeometry.FormalSpace.IsLocallyOfFiniteType.isFiniteType_of_isAffineFormal, and Stacks 0AJJ.

theorem isLocallyOfFiniteType_tfae_of_isAffineFormalAlgebraicSpace {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (hY : IsAffineFormalAlgebraicSpace B S hS Y) (hYc : IsCountablyIndexed B S hS Y) :
    List.TFAE
      [IsLocallyOfFiniteType B S hS f,
        IsFiniteType' B S hS f,
        CorrespondsToCountablyWeaklyAdmissibleMap B S hS
          (fun φ ↦ TopologicalRing.FiniteTypeModuloEveryWeakIdeal φ) f,
        CorrespondsToCountablyWeaklyAdmissibleMap B S hS
          TopologicalRing.IsTautTopologicallyOfFiniteTypeHom f]

AlgebraicGeometry.FormalSpace.chartPropertyIsLocallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeCharacterizationRefined.lean, line 129. The attribute's comment: “the equivalence, read on countably indexed affine charts rather than on formal spectra: a map of countably indexed affine formal algebraic spaces over S is locally of finite type exactly when every morphism of WAdm^{count} presenting it is taut and topologically of finite type”.

A map of countably indexed affine formal algebraic spaces over S is locally of finite type exactly when every morphism of WAdm^{count} presenting it is taut and topologically of finite type.

A countably indexed affine formal algebraic space is the formal spectrum of a weakly admissible topological ring with a countable fundamental system of neighbourhoods of zero — item (6) of Stacks 0AIK — and a map of formal spectra comes from a unique continuous homomorphism by Stacks 0AN0, so the chart condition is never vacuous here and both directions are the corresponding implications of Stacks 0ANV for that homomorphism. The implication out of being locally of finite type is Stacks 0AN5 (1) ⟹ (3) for tautness together with the implication (1) ⟹ (2) of Stacks 0ANT, the two being combined in isTaut_and_isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap once Stacks 0AKN has upgraded locally of finite type to of finite type; the implication back is the implication (2) ⟹ (1) of Stacks 0ANT, isFiniteType_formalSpectrumMap_of_isTaut. Being locally of finite type is carried across the two comparison isomorphisms by Stacks 0AQ4, an isomorphism being representable étale.

theorem chartPropertyIsLocallyOfFiniteType :
    ChartPropertyIsLocallyOfFiniteType B S hS

AlgebraicGeometry.FormalSpace.formalSpectrumMap_finiteType_tfae_countablyWeaklyAdmissible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeCharacterizationVariants.lean, line 107. The attribute's comment: “the equivalence, under the source's hypotheses exactly: only the target Spf A is assumed countably indexed, by hAcount. Condition (3) is taken in the two forms (a) and (c) of Stacks 0ANU, each conjoined with membership of the source ring in WAdm^count, which is what f corresponds to a morphism of WAdm^count still asserts once the target ring's membership is the standing hypothesis. That membership is a conclusion of conditions (1) and (2) rather than an assumption: every one of the four conditions supplies tautness, and a taut continuous homomorphism carries a countable fundamental system of open ideals from source ring to target ring by Stacks 0GX6, RingHom.isCountablyGenerated_nhds_zero_of_isTaut — which replaces the source's appeal to Stacks 0AKN and Stacks 0AKP and, like the library's Stacks 0AKN, needs no affineness of the two formal spectra. The finite type condition is Definition 0AM4, part (2), verbatim; the implication (2) ⟹ (1) of Stacks 0ANT concludes it through condition (2) of Stacks 0AJJ — representable by algebraic spaces plus of finite type in the Bootstrap sense of Stacks 03XZ — which Stacks 0AJJ, AlgebraicGeometry.FormalSpace.isFiniteType_iff_isBootstrapFiniteType, identifies with Definition 0AM4, part (2), unconditionally. The two forms of condition (3) are identified with no countability assumption, by TopologicalRing.isTopologicallyOfFiniteType_of_finiteTypeModuloEveryWeakIdeal and TopologicalRing.finiteTypeModuloEveryWeakIdeal_of_topologicallyOfFiniteType, so Stacks 0ANU's own countability hypotheses are not needed here; the implication (1) ⟹ (3) of Stacks 0AN5 that supplies tautness, AlgebraicGeometry.FormalSpace.isTaut_of_isRepresentableByAlgebraicSpaces_formalSpectrumMap, carries no side condition either”.

Stacks 0ANV. Let φ : A ⟶ C be a continuous homomorphism of weakly admissible topological rings over S and assume the neighbourhood filter of zero of A — the target Spf A — countably generated. Then Spf (φ) : Spf C → Spf A being locally of finite type, Spf (φ) being of finite type in the sense of Definition 0AM4, part (2), φ being a morphism of WAdm^{count} of finite type modulo every weak ideal of definition, and φ being a morphism of WAdm^{count} which is taut and topologically of finite type are all equivalent.

Only the target is assumed countably indexed, as in the source. That the source Spf C is countably indexed is part of what condition (3) asserts — membership of φ in WAdm^{count} — and so is a conclusion of conditions (1) and (2), not a hypothesis; the target's own membership is the standing hypothesis hAcount together with hA. The step that produces it is Stacks 0GX6, RingHom.isCountablyGenerated_nhds_zero_of_isTaut: a taut continuous homomorphism carries a countable fundamental system of open ideals from source ring to target ring, and every one of the four conditions supplies tautness. This replaces the appeal to Stacks 0AKN and Stacks 0AKP that the source makes, and like them it needs no affineness of the two formal spectra.

The last two conditions are conditions (a) and (c) of Stacks 0ANU, each conjoined with membership in WAdm^{count}. They are identified here without any countability assumption, by TopologicalRing.isTopologicallyOfFiniteType_of_finiteTypeModuloEveryWeakIdeal — for which weak pre-admissibility of A suffices — and TopologicalRing.finiteTypeModuloEveryWeakIdeal_of_topologicallyOfFiniteType, so Stacks 0ANU's own countability hypotheses are not needed. With hAcount and the WAdm^{count} conjunct in hand, Stacks 0ANU identifies these two with its remaining conditions (b) and (d) as well, which is why reading condition (3) off either form is faithful.

The implication from locally of finite type to condition (a) splits into tautness, which is the implication (1) ⟹ (3) of Stacks 0AN5, and finite type of the stage quotient maps, which is the ring-theoretic half of Stacks 0ANT; the implication from condition (a) back is the implication (2) ⟹ (1) of Stacks 0ANT, and being locally of finite type is the first half of the conjunction that being of finite type is.

The quasi-compactness of Definition 0AJC that the second condition contains is not established directly anywhere in the cycle: the implication (2) ⟹ (1) of Stacks 0ANT produces condition (2) of Stacks 0AJJ, AlgebraicGeometry.FormalSpace.IsBootstrapFiniteType, whose quasi-compactness assertion is the Bootstrap one, and Stacks 0AJJ identifies that condition with Definition 0AM4, part (2), unconditionally; see AlgebraicGeometry.FormalSpace.isFiniteType_iff_isBootstrapFiniteType.

Nothing beyond the source's hypotheses is assumed. The tautness step is the implication (1) ⟹ (3) of Stacks 0AN5, AlgebraicGeometry.FormalSpace.isTaut_of_isRepresentableByAlgebraicSpaces_formalSpectrumMap, which carries no side condition of its own.

theorem formalSpectrumMap_finiteType_tfae_countablyWeaklyAdmissible {A C : Type u} [CommRing A]
    [TopologicalSpace A] [IsTopologicalRing A] [IsLinearTopology A A] [CommRing C]
    [TopologicalSpace C] [IsTopologicalRing C] [IsLinearTopology C C]
    (hA : TopologicalRing.IsWeaklyAdmissible A) (hC : TopologicalRing.IsWeaklyAdmissible C)
    (hAcount : (nhds (0 : A)).IsCountablyGenerated)
    (D : QuotientSystem B S hS A) (E : QuotientSystem B S hS C) (g : ContinuousHom D E) :
    List.TFAE
      [IsLocallyOfFiniteType B S hS (formalSpectrumMap hA g),
        IsFiniteType' B S hS (formalSpectrumMap hA g),
        TopologicalRing.IsCountablyWeaklyAdmissible C ∧
          TopologicalRing.FiniteTypeModuloEveryWeakIdeal g.toRingHom,
        TopologicalRing.IsCountablyWeaklyAdmissible C ∧
          RingHom.IsTaut g.toRingHom ∧
            TopologicalRing.IsTopologicallyOfFiniteType g.toRingHom]

Tag 0ANW, a lemma

Tag 0ANW in the Stacks Project.

AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_tfae', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FiniteTypeCharacterizationRefined.lean, line 199. The attribute's comment: “the equivalence of its four conditions, at the source's own hypotheses. The presented refinement of a covering of the source is the library's hasEtaleRefinementOfSourceCover_isCountablyWeaklyAdmissible (Stacks 0AJ2, quasi-compactness of an affine formal algebraic space and Stacks 0AN8) and the implication (2) ⟹ (1) of Stacks 0AKX is the library's isCountablyIndexed_of_isRepresentableEtale_of_isLocallyCountablyIndexed”.

For a morphism f : X ⟶ Y of locally countably indexed formal algebraic spaces over S, the condition that every affine representable étale square over f carry a taut, topologically of finite type morphism of WAdm^{count}, the existence of an affine étale covering of Y together with affine étale coverings of the fibre products of its members with X on which that condition holds, the existence of an affine étale covering of X whose members factor through affine representable étale charts of Y by such morphisms, and f being locally of finite type, are all equivalent.

The first three are the three conditions of Stacks 0ANG for the class of countably indexed weakly admissible topological rings and the property of being taut and topologically of finite type, which Stacks 0ANU makes a local property of such arrows; the comparison with the fourth is Stacks 0ANV on charts together with the implications (1) ⟹ (3) and (4) ⟹ (5) ⟹ (1) of Stacks 0ANL.

theorem isLocallyOfFiniteType_tfae' {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsLocallyCountablyIndexed B S hS X) (hY : IsLocallyCountablyIndexed B S hS Y) :
    List.TFAE
      [HasPropertyOnEveryAffineEtaleDiagram B S hS
          TopologicalRing.IsCountablyWeaklyAdmissible
          TopologicalRing.IsTautTopologicallyOfFiniteTypeHom f,
        HasPropertyAfterTargetCover B S hS
          TopologicalRing.IsCountablyWeaklyAdmissible
          TopologicalRing.IsTautTopologicallyOfFiniteTypeHom f,
        HasPropertyAfterSourceCover B S hS
          TopologicalRing.IsCountablyWeaklyAdmissible
          TopologicalRing.IsTautTopologicallyOfFiniteTypeHom f,
        IsLocallyOfFiniteType B S hS f]

Sources

• Section 87.29, Tag 0ALL
• AxiomMath/Stacks at 5ed82d14

LeanTopologicalRing.IsTopologicallyOfFiniteType · AlgebraicGeometry.FormalSpace.isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap · AlgebraicGeometry.FormalSpace.exists_isPullback_isFiniteTypeULift_formalSpectrumMap_stage · AlgebraicGeometry.FormalSpace.isFiniteType_formalSpectrumMap_of_isTaut · AlgebraicGeometry.FormalSpace.isLocallyOfFiniteTypeAndQuasiCompact_formalSpectrumMap_of_finiteTypeModuloEveryWeakIdeal · AlgebraicGeometry.FormalSpace.isLocallyOfFiniteType_formalSpectrumMap_of_finiteTypeModuloEveryWeakIdeal · AlgebraicGeometry.FormalSpace.isTaut_and_isTopologicallyOfFiniteType_of_isFiniteType_formalSpectrumMap' · AlgebraicGeometry.FormalSpace.isFiniteType_formalSpectrumMap_iff_isTaut_and_isTopologicallyOfFiniteType

Section87.30 Separation axioms for morphisms#

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

Tag 0ARN, a definition

Tag 0ARN in the Stacks Project.

AlgebraicGeometry.FormalSpace.HasQuasiCompactDiagonal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphism.lean, line 112. The attribute's comment: “part (2): quasi-separated, the relative diagonal quasi-compact in the sense of Stacks 0AJC”.

Stacks 0ARN, part (2). A morphism of formal algebraic spaces over S is quasi-separated when its relative diagonal X ⟶ X ×_Y X is a quasi-compact morphism of formal algebraic spaces, quasi-compactness being AlgebraicGeometry.FormalSpace.IsQuasiCompact, the condition of Stacks 0AJC. The condition makes sense, and is stated, for an arbitrary morphism of fppf sheaves on the big fppf site of S.

abbrev HasQuasiCompactDiagonal {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop

AlgebraicGeometry.FormalSpace.IsSeparatedMorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 113. The attribute's comment: “part (1): separated”. References: EGA I (10.15.1), “separated morphism”.

A morphism of formal algebraic spaces over S is separated when its relative diagonal is a closed immersion, stated for an arbitrary morphism of fppf sheaves on the big fppf site of S.

abbrev IsSeparatedMorphism {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop

Tag 0ARP, a lemma

Tag 0ARP in the Stacks Project.

AlgebraicGeometry.FormalSpace.HasQuasiCompactDiagonal.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphism.lean, line 134. The attribute's comment: “quasi-separated”.

Stacks 0ARP for the quasi-separatedness axiom of Stacks 0ARN: a base change of a quasi-separated morphism of formal algebraic spaces over S is quasi-separated. In a cartesian square of fppf sheaves on the big fppf site of S whose right-hand column f is quasi-separated, the left-hand column snd is quasi-separated, since the relative diagonal of snd is a base change of the relative diagonal of f and quasi-compact morphisms are stable under base change. As with the definition itself, no hypothesis that the four sheaves are formal algebraic spaces is needed.

theorem HasQuasiCompactDiagonal.of_isPullback {X Y Y' W : FppfSheaf B S hS}
    {fst : W ⟶ X} {snd : W ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback fst snd f g)
    (hf : HasQuasiCompactDiagonal B S hS f) : HasQuasiCompactDiagonal B S hS snd

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 139. The attribute's comment: “separated”.

A base change of a separated morphism of formal algebraic spaces over S is separated: in a cartesian square of fppf sheaves on the big fppf site of S whose right-hand column f is separated, the left-hand column snd is separated.

theorem isSeparatedMorphism_of_isPullback {X Y Y' W : FppfSheaf B S hS}
    {fst : W ⟶ X} {snd : W ⟶ Y'} {f : X ⟶ Y} {g : Y' ⟶ Y} (sq : IsPullback fst snd f g)
    (hf : IsSeparatedMorphism B S hS f) : IsSeparatedMorphism B S hS snd

Tag 0ARQ, a lemma

Tag 0ARQ in the Stacks Project.

AlgebraicGeometry.FormalSpace.isQuasiCompact_mapDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphism.lean, line 163. The attribute's comment: “part (3), for Z ⟶ T quasi-separated. Both notions are the source's own: the hypothesis is quasi-separatedness as Stacks 0ARN, part (2) declares it, the relative diagonal quasi-compact in the sense of Stacks 0AJC (HasQuasiCompactDiagonal of this file), and the conclusion is quasi-compactness of a morphism of formal algebraic spaces in that same sense of Stacks 0AJC (IsQuasiCompact of QuasiCompactMorphism.lean). Nothing is carried and nothing is assumed beyond the tag's own hypothesis on Z ⟶ T; in particular this is independent of Stacks 0AN2 and of Stacks 0AIP, which parts (1) and (2) of the tag need. Parts (1) and (2) are registered in SeparatedMorphism.lean”.

Stacks 0ARQ, part (3). For morphisms f : X ⟶ Z, g : Y ⟶ Z and h : Z ⟶ T of formal algebraic spaces over S with h quasi-separated, the comparison X ×_Z Y ⟶ X ×_T Y of the two fibre products is a quasi-compact morphism of formal algebraic spaces.

The whole content is one cartesian square, the magic diagram of Mathlib's CategoryTheory.Limits.pullback_map_diagonal_isPullback: the comparison is a base change of the relative diagonal of h, along the morphism X ×_T Y ⟶ Z ×_T Z induced by f and g. Quasi-separatedness of h says that relative diagonal is quasi-compact, and quasi-compactness is stable under base change by AlgebraicGeometry.FormalSpace.IsQuasiCompact.of_isPullback. No hypothesis on f, g or the four sheaves is needed, so the statement is made for arbitrary fppf sheaves, as both conditions occurring in it are.

theorem isQuasiCompact_mapDesc {X Y Z T : FppfSheaf B S hS} (f : X ⟶ Z) (g : Y ⟶ Z)
    (h : Z ⟶ T) (hh : HasQuasiCompactDiagonal B S hS h) :
    IsQuasiCompact B S hS (pullback.mapDesc f g h)

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_mapDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1345. The attribute's comment: “part (1): separated, separatedness read in the sense of Stacks 0ARN”.

The comparison X ×_Z Y ⟶ X ×_T Y of two fibre products of fppf sheaves on the big fppf site of S is separated in the sense of Stacks 0ARN.

theorem isSeparatedMorphism_mapDesc (f : X ⟶ Z) (g : Y ⟶ Z) (h : Z ⟶ T) :
    IsSeparatedMorphism B S hS (pullback.mapDesc f g h)

AlgebraicGeometry.FormalSpace.relativelyRepresentable_mapDesc_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1378. The attribute's comment: “part (1): representable by schemes, unconditionally for Z an affine formal algebraic space”.

When Z is an affine formal algebraic space, the comparison X ×_Z Y ⟶ X ×_T Y is representable by schemes.

theorem relativelyRepresentable_mapDesc_of_isAffineFormal (f : X ⟶ Z) (g : Y ⟶ Z) (h : Z ⟶ T)
    (hZ : IsAffineFormalAlgebraicSpace B S hS Z) :
    (fppfYoneda B S hS).relativelyRepresentable (pullback.mapDesc f g h)

AlgebraicGeometry.FormalSpace.relative_locallyQuasiFinite_mapDesc_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1389. The attribute's comment: “part (1): locally quasi-finite, unconditionally for Z an affine formal algebraic space”.

When Z is an affine formal algebraic space, every represented base change of the comparison X ×_Z Y ⟶ X ×_T Y is a locally quasi-finite, locally of finite type morphism of schemes.

theorem relative_locallyQuasiFinite_mapDesc_of_isAffineFormal (f : X ⟶ Z) (g : Y ⟶ Z)
    (h : Z ⟶ T) (hZ : IsAffineFormalAlgebraicSpace B S hS Z) :
    (MorphismProperty.inverseImage
      ((@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) ⊓
        (@AlgebraicGeometry.LocallyQuasiFinite.{u} : MorphismProperty Scheme.{u}))
      (BigFppfOver.toScheme B S hS)).relative (fppfYoneda B S hS)
      (pullback.mapDesc f g h)

AlgebraicGeometry.FormalSpace.relative_locallyOfFiniteType_mapDesc_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1403. The attribute's comment: “part (1): locally of finite type, unconditionally for Z an affine formal algebraic space”.

When Z is an affine formal algebraic space, every represented base change of the comparison X ×_Z Y ⟶ X ×_T Y is a locally of finite type morphism of schemes.

theorem relative_locallyOfFiniteType_mapDesc_of_isAffineFormal (f : X ⟶ Z) (g : Y ⟶ Z)
    (h : Z ⟶ T) (hZ : IsAffineFormalAlgebraicSpace B S hS Z) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative (fppfYoneda B S hS)
      (pullback.mapDesc f g h)

AlgebraicGeometry.FormalSpace.relative_isSeparated_mapDesc_of_isAffineFormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1416. The attribute's comment: “part (1): separated in the represented-base-change sense of Stacks 0AN2, unconditionally for Z an affine formal algebraic space”.

When Z is an affine formal algebraic space, every represented base change of the comparison X ×_Z Y ⟶ X ×_T Y is a separated morphism of schemes.

theorem relative_isSeparated_mapDesc_of_isAffineFormal (f : X ⟶ Z) (g : Y ⟶ Z) (h : Z ⟶ T)
    (hZ : IsAffineFormalAlgebraicSpace B S hS Z) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.IsSeparated.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative (fppfYoneda B S hS)
      (pullback.mapDesc f g h)

AlgebraicGeometry.FormalSpace.relativelyRepresentable_mapDesc_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1427. The attribute's comment: “part (1): representable by schemes, for Z an arbitrary formal algebraic space”.

When Z is a formal algebraic space, the comparison X ×_Z Y ⟶ X ×_T Y is representable by schemes.

theorem relativelyRepresentable_mapDesc_of_isFormalAlgebraicSpace (f : X ⟶ Z) (g : Y ⟶ Z)
    (h : Z ⟶ T) (hZ : IsFormalAlgebraicSpace B S hS Z) :
    (fppfYoneda B S hS).relativelyRepresentable (pullback.mapDesc f g h)

AlgebraicGeometry.FormalSpace.relative_locallyQuasiFinite_mapDesc_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1436. The attribute's comment: “part (1): locally quasi-finite, for Z an arbitrary formal algebraic space”.

When Z is a formal algebraic space, every represented base change of the comparison X ×_Z Y ⟶ X ×_T Y is a locally quasi-finite, locally of finite type morphism of schemes.

theorem relative_locallyQuasiFinite_mapDesc_of_isFormalAlgebraicSpace (f : X ⟶ Z) (g : Y ⟶ Z)
    (h : Z ⟶ T) (hZ : IsFormalAlgebraicSpace B S hS Z) :
    (MorphismProperty.inverseImage
      ((@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) ⊓
        (@AlgebraicGeometry.LocallyQuasiFinite.{u} : MorphismProperty Scheme.{u}))
      (BigFppfOver.toScheme B S hS)).relative (fppfYoneda B S hS)
      (pullback.mapDesc f g h)

AlgebraicGeometry.FormalSpace.relative_locallyOfFiniteType_mapDesc_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1449. The attribute's comment: “part (1): locally of finite type, for Z an arbitrary formal algebraic space”.

When Z is a formal algebraic space, every represented base change of the comparison X ×_Z Y ⟶ X ×_T Y is a locally of finite type morphism of schemes.

theorem relative_locallyOfFiniteType_mapDesc_of_isFormalAlgebraicSpace (f : X ⟶ Z) (g : Y ⟶ Z)
    (h : Z ⟶ T) (hZ : IsFormalAlgebraicSpace B S hS Z) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative (fppfYoneda B S hS)
      (pullback.mapDesc f g h)

AlgebraicGeometry.FormalSpace.relative_isSeparated_mapDesc_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1462. The attribute's comment: “part (1): separated in the represented-base-change sense of Stacks 0AN2, for Z an arbitrary formal algebraic space”.

When Z is a formal algebraic space, every represented base change of the comparison X ×_Z Y ⟶ X ×_T Y is a separated morphism of schemes.

theorem relative_isSeparated_mapDesc_of_isFormalAlgebraicSpace (f : X ⟶ Z) (g : Y ⟶ Z)
    (h : Z ⟶ T) (hZ : IsFormalAlgebraicSpace B S hS Z) :
    (MorphismProperty.inverseImage
      (@AlgebraicGeometry.IsSeparated.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative (fppfYoneda B S hS)
      (pullback.mapDesc f g h)

AlgebraicGeometry.FormalSpace.isClosedImmersion_mapDesc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1474. The attribute's comment: “part (2), for Z ⟶ T separated”.

If h : Z ⟶ T is separated then the comparison X ×_Z Y ⟶ X ×_T Y is a closed immersion.

theorem isClosedImmersion_mapDesc (f : X ⟶ Z) (g : Y ⟶ Z) (h : Z ⟶ T)
    (hh : IsSeparatedMorphism B S hS h) :
    IsClosedImmersion B S hS (pullback.mapDesc f g h)

Declarations registered for the tag:

• CategoryTheory.Limits.pullback.mono_mapDesc, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1502 (StacksFrontier): “part (1): monomorphism”.

Tag 0ARR, a lemma

Tag 0ARR in the Stacks Project.

AlgebraicGeometry.FormalSpace.isQuasiSeparatedMorphism_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphismComposition.lean, line 195. The attribute's comment: “part (2): quasi-separated, with quasi-compactness of the relative diagonal read as the condition AlgebraicGeometry.Space.IsQuasiCompactULift that this library's AlgebraicGeometry.FormalSpace.IsQuasiSeparatedMorphism is built from; the comparison of the two relative self-products is quasi-compact by Stacks 0ARQ, part (3), and that condition is stable under composition over formal algebraic spaces by AlgebraicGeometry.Space.isQuasiCompactULift_comp_of_presheaf”.

Stacks 0ARR for the quasi-separatedness axiom of Stacks 0ARN. A composite of two morphisms of fppf sheaves on the big fppf site of S with quasi-compact relative diagonal again has quasi-compact relative diagonal: the relative diagonal of f ≫ g factors as the relative diagonal of f, quasi-compact since f is quasi-separated, followed by the comparison X ×_Y X ⟶ X ×_Z X, quasi-compact since g is quasi-separated by Stacks 0ARQ, part (3); and the quasi-compactness condition is stable under composition with no hypothesis that the objects are algebraic spaces.

Quasi-compactness is read throughout as AlgebraicGeometry.Space.IsQuasiCompactULift, the condition AlgebraicGeometry.FormalSpace.IsQuasiSeparatedMorphism is built from. As with the definition, no hypothesis that the three sheaves are formal algebraic spaces is needed.

theorem isQuasiSeparatedMorphism_comp {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : IsQuasiSeparatedMorphism B S hS f) (hg : IsQuasiSeparatedMorphism B S hS g) :
    IsQuasiSeparatedMorphism B S hS (f ≫ g)

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphismComposition.lean, line 122. The attribute's comment: “part (1): separated, separatedness read in the sense of Stacks 0ARN; the comparison of the two relative self-products is a closed immersion by Stacks 0ARQ, part (2), and closed immersions compose by Stacks 0GHW”.

Stacks 0ARR for the separatedness axiom of Stacks 0ARN. A composite of two separated morphisms of fppf sheaves on the big fppf site of S is separated: the relative diagonal of f ≫ g factors as the relative diagonal of f, a closed immersion since f is separated, followed by the comparison X ×_Y X ⟶ X ×_Z X, a closed immersion since g is separated by Stacks 0ARQ, part (2); and closed immersions of formal algebraic spaces compose by Stacks 0GHW.

theorem isSeparatedMorphism_comp {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : IsSeparatedMorphism B S hS f) (hg : IsSeparatedMorphism B S hS g) :
    IsSeparatedMorphism B S hS (f ≫ g)

AlgebraicGeometry.FormalSpace.hasRelativeDiagonal_quasiCompact_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphismComposition.lean, line 139. The attribute's comment: “part (2): quasi-separated, with quasi-compactness of the relative diagonal read as the relative diagonal condition for quasi-compact morphisms of schemes, which is the second of the two cases of Stacks 0ARN in the uniform shape of Stacks 0ARS; stability under composition of quasi-compact morphisms of schemes is taken from Mathlib”.

Stacks 0ARR for the quasi-separatedness axiom of Stacks 0ARN, with quasi-compactness of the relative diagonal read as the relative diagonal condition for quasi-compact morphisms of schemes: if the relative diagonals of f and of g are quasi-compact in that sense, then so is the relative diagonal of f ≫ g. Quasi-compact morphisms of schemes are stable under composition, so this is the case P = AlgebraicGeometry.QuasiCompact of AlgebraicGeometry.FormalSpace.hasRelativeDiagonal_comp.

theorem hasRelativeDiagonal_quasiCompact_comp {X Y Z : FppfSheaf B S hS} (f : X ⟶ Y)
    (g : Y ⟶ Z)
    (hf : HasRelativeDiagonal B S hS
      (@AlgebraicGeometry.QuasiCompact.{u} : MorphismProperty Scheme.{u}) f)
    (hg : HasRelativeDiagonal B S hS
      (@AlgebraicGeometry.QuasiCompact.{u} : MorphismProperty Scheme.{u}) g) :
    HasRelativeDiagonal B S hS
      (@AlgebraicGeometry.QuasiCompact.{u} : MorphismProperty Scheme.{u}) (f ≫ g)

Tag 0ARS, a lemma

Tag 0ARS in the Stacks Project.

AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_iff_forall_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphismComparison.lean, line 328. The attribute's comment: “clauses (1) and (2) for the quasi-separated axiom of Stacks 0ARN: a morphism of formal algebraic spaces with relatively representable relative diagonal is quasi-separated if and only if its base change to every scheme over the target is quasi-separated; the representability hypothesis is discharged for a source which is a formal algebraic space in …hasQuasiCompactDiagonal_iff_forall_baseChange_of_isFormalAlgebraicSpace”.

Stacks 0ARS, clauses (1) and (2) for the quasi-separatedness axiom of Stacks 0ARN. A morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S whose relative diagonal is representable by objects of the site is quasi-separated exactly when its base change to every scheme over the target is quasi-separated.

The hypothesis hf is carried: unlike the separatedness axiom, whose spelling in this library contains representability of the relative diagonal, the quasi-separatedness axiom does not, and the comparison with the relative diagonal condition of AlgebraicGeometry.FormalSpace.HasRelativeDiagonal needs it. It is discharged for a source which is a formal algebraic space — the hypothesis of Stacks 0ARS itself — in …hasQuasiCompactDiagonal_iff_forall_baseChange_of_isFormalAlgebraicSpace below.

theorem hasQuasiCompactDiagonal_iff_forall_baseChange {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hf : (fppfYoneda B S hS).relativelyRepresentable (pullback.diagonal f)) :
    HasQuasiCompactDiagonal B S hS f ↔
      ∀ (U : BigFppfOver B S hS) (g : (fppfYoneda B S hS).obj U ⟶ Y),
        HasQuasiCompactDiagonal B S hS (pullback.snd f g)

AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_iff_forall_baseChange_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphismComparison.lean, line 354. The attribute's comment: “clauses (1) and (2) for the quasi-separated axiom of Stacks 0ARN, in the source's form with no extra hypothesis: a morphism of formal algebraic spaces is quasi-separated if and only if its base change to every scheme over the target is quasi-separated”.

Stacks 0ARS, clauses (1) and (2) for the quasi-separatedness axiom of Stacks 0ARN, in the source's own form: a morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S whose source is a formal algebraic space is quasi-separated exactly when its base change to every scheme over the target is quasi-separated. The representability hypothesis of AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_iff_forall_baseChange is discharged here: the relative diagonal of f is a base change of the absolute diagonal of X, which is representable by objects of the site by Stacks 0AIP.

theorem hasQuasiCompactDiagonal_iff_forall_baseChange_of_isFormalAlgebraicSpace
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hX : IsFormalAlgebraicSpace B S hS X) :
    HasQuasiCompactDiagonal B S hS f ↔
      ∀ (U : BigFppfOver B S hS) (g : (fppfYoneda B S hS).obj U ⟶ Y),
        HasQuasiCompactDiagonal B S hS (pullback.snd f g)

AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_iff_forall_affine_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphismComparison.lean, line 381. The attribute's comment: “clauses (1) and (3) for the quasi-separated axiom of Stacks 0ARN: a morphism of formal algebraic spaces with relatively representable relative diagonal is quasi-separated if and only if its base change to every affine scheme over the target is quasi-separated; the representability hypothesis is discharged for a source which is a formal algebraic space in …hasQuasiCompactDiagonal_iff_forall_affine_baseChange_of_isFormalAlgebraicSpace”.

Stacks 0ARS, clauses (1) and (3) for the quasi-separatedness axiom of Stacks 0ARN. A morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S whose relative diagonal is representable by objects of the site is quasi-separated exactly when its base change to every affine scheme over the target is quasi-separated. Quasi-compactness of morphisms of schemes is Zariski local on the target, which is what lets the test objects be restricted to the affine ones.

As in clauses (1) and (2), the hypothesis hf is carried, and is discharged for a source which is a formal algebraic space in …hasQuasiCompactDiagonal_iff_forall_affine_baseChange_of_isFormalAlgebraicSpace below.

theorem hasQuasiCompactDiagonal_iff_forall_affine_baseChange {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hf : (fppfYoneda B S hS).relativelyRepresentable (pullback.diagonal f)) :
    HasQuasiCompactDiagonal B S hS f ↔
      ∀ (U : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj U) →
        ∀ (g : (fppfYoneda B S hS).obj U ⟶ Y),
          HasQuasiCompactDiagonal B S hS (pullback.snd f g)

AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_iff_forall_affine_baseChange_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphismComparison.lean, line 405. The attribute's comment: “clauses (1) and (3) for the quasi-separated axiom of Stacks 0ARN, in the source's form with no extra hypothesis: a morphism of formal algebraic spaces is quasi-separated if and only if its base change to every affine scheme over the target is quasi-separated”.

Stacks 0ARS, clauses (1) and (3) for the quasi-separatedness axiom of Stacks 0ARN, in the source's own form: a morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S whose source is a formal algebraic space is quasi-separated exactly when its base change to every affine scheme over the target is quasi-separated. The representability hypothesis of AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_iff_forall_affine_baseChange is discharged by Stacks 0AIP and Stacks 0AN2 as before.

theorem hasQuasiCompactDiagonal_iff_forall_affine_baseChange_of_isFormalAlgebraicSpace
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hX : IsFormalAlgebraicSpace B S hS X) :
    HasQuasiCompactDiagonal B S hS f ↔
      ∀ (U : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj U) →
        ∀ (g : (fppfYoneda B S hS).obj U ⟶ Y),
          HasQuasiCompactDiagonal B S hS (pullback.snd f g)

AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_iff_isQuasiSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphismComparison.lean, line 436. The attribute's comment: “clauses (3) and (4) for the quasi-separated axiom of Stacks 0ARN: a morphism of formal algebraic spaces to an affine scheme with relatively representable relative diagonal is quasi-separated if and only if its source is a quasi-separated formal algebraic space; the representability hypothesis is discharged for a source which is a formal algebraic space in …hasQuasiCompactDiagonal_iff_isQuasiSeparated_of_isFormalAlgebraicSpace”.

Stacks 0ARS, clauses (3) and (4) for the quasi-separatedness axiom of Stacks 0ARN. A morphism f : X ⟶ Z of fppf sheaves on the big fppf site of S whose target is represented by an affine scheme of the site and whose relative diagonal is representable by objects of the site is quasi-separated exactly when the source X is quasi-separated as a single sheaf, in the sense of clause (1) of Stacks 0AJ7 — that is, clause (3) of Stacks 0AJ5: the fibre product over X of any two affine scheme-valued points of X has quasi-compact underlying scheme.

Both directions are the argument of the source read through the comparison of the two fibre product descriptions U ×_X V = X ×_{Δ, X ×_Z X} (U ×_Z V), which is AlgebraicGeometry.FormalSpace.pair_diagonal_square in one direction and AlgebraicGeometry.FormalSpace.diagonal_test_pair_square in the other. The scheme-level inputs are that a quasi-compact morphism into a quasi-compact scheme has quasi-compact source, and conversely that a morphism from a quasi-compact scheme to an affine one is quasi-compact.

theorem hasQuasiCompactDiagonal_iff_isQuasiSeparated {X : FppfSheaf B S hS}
    {Z : BigFppfOver B S hS} (hZ : IsAffine ((BigFppfOver.toScheme B S hS).obj Z))
    (f : X ⟶ (fppfYoneda B S hS).obj Z)
    (hf : (fppfYoneda B S hS).relativelyRepresentable (pullback.diagonal f)) :
    HasQuasiCompactDiagonal B S hS f ↔ IsQuasiSeparated B S hS X

AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_iff_isQuasiSeparated_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphismComparison.lean, line 487. The attribute's comment: “clauses (3) and (4) for the quasi-separated axiom of Stacks 0ARN, in the source's form with no extra hypothesis: a morphism from a formal algebraic space to an affine scheme is quasi-separated if and only if its source is a quasi-separated formal algebraic space”.

Stacks 0ARS, clauses (3) and (4) for the quasi-separatedness axiom of Stacks 0ARN, in the source's own form: a morphism from a formal algebraic space to a sheaf represented by an affine scheme of the site is quasi-separated exactly when its source is a quasi-separated formal algebraic space, quasi-separatedness of a single sheaf being read as clause (1) of Stacks 0AJ7. The representability hypothesis of AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_iff_isQuasiSeparated is discharged by Stacks 0AIP and Stacks 0AN2.

theorem hasQuasiCompactDiagonal_iff_isQuasiSeparated_of_isFormalAlgebraicSpace
    {X : FppfSheaf B S hS} {Z : BigFppfOver B S hS}
    (hZ : IsAffine ((BigFppfOver.toScheme B S hS).obj Z))
    (f : X ⟶ (fppfYoneda B S hS).obj Z) (hX : IsFormalAlgebraicSpace B S hS X) :
    HasQuasiCompactDiagonal B S hS f ↔ IsQuasiSeparated B S hS X

AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_of_locallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphismComparison.lean, line 507. The attribute's comment: “the descent step of clause (5) for the quasi-separated axiom of Stacks 0ARN: quasi-separatedness descends along a single locally surjective morphism onto the relative self-product, which is the atlas clause with the covering of Definition 0AIM replaced by one locally surjective morphism, and is not the atlas form itself”.

Stacks 0ARS, the descent step of clause (5) for the quasi-separatedness axiom of Stacks 0ARN. Quasi-separatedness of a morphism of fppf sheaves whose relative diagonal is relatively representable descends along a locally surjective morphism onto the relative self-product. Quasi-compactness of morphisms of schemes is fppf local on the target by Stacks 02WH, which is what the descent step consumes.

theorem hasQuasiCompactDiagonal_of_locallySurjective {X Y W : FppfSheaf B S hS} (f : X ⟶ Y)
    (b : W ⟶ pullback f f) (hb : Sheaf.IsLocallySurjective b)
    (hrep : (fppfYoneda B S hS).relativelyRepresentable (pullback.diagonal f))
    (hbase : (MorphismProperty.inverseImage (@AlgebraicGeometry.QuasiCompact.{u})
      (BigFppfOver.toScheme B S hS)).relative (fppfYoneda B S hS)
      (pullback.snd (pullback.diagonal f) b)) :
    HasQuasiCompactDiagonal B S hS f

AlgebraicGeometry.FormalSpace.exists_atlas_hasQuasiCompactDiagonal_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphismComparison.lean, line 529. The attribute's comment: “clause (5) in the covering form of Definition 0AIM, necessity for the quasi-separated axiom of Stacks 0ARN: a quasi-separated morphism of formal algebraic spaces has quasi-separated base change to every member of some covering of the target as in Definition 0AIM”.

Stacks 0ARS, clause (1) implies clause (5) for the quasi-separatedness axiom of Stacks 0ARN, in the covering form. If Y is a formal algebraic space and f : X ⟶ Y is quasi-separated then there is a covering {Y_j ⟶ Y} as in Definition 0AIM along which every base change of f is quasi-separated. The covering is the atlas of Y furnished by Definition 0AIM; the base changes inherit the condition by Stacks 0ARP.

theorem exists_atlas_hasQuasiCompactDiagonal_pullback_snd {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hY : IsFormalAlgebraicSpace B S hS Y) (hf : HasQuasiCompactDiagonal B S hS f) :
    letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) := Sheaf.instHasColimitsOfSize
    ∃ (I : Type (u + 1)) (Yj : I → FppfSheaf B S hS) (g : ∀ j, Yj j ⟶ Y),
      (∀ j, IsAffineFormalAlgebraicSpace B S hS (Yj j)) ∧
      (∀ j, ∃ hgj : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (g j).hom,
        Space.HasPropertyULift.{u + 1} B S hS
          (fun _ _ k ↦ Space.IsEtaleULift.{u + 1} B S hS k.hom) (g j).hom hgj) ∧
      Sheaf.IsLocallySurjective (Sigma.desc g) ∧
      ∀ j, HasQuasiCompactDiagonal B S hS (pullback.snd f (g j))

AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_of_atlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphismComparison.lean, line 560. The attribute's comment: “clause (5) in the covering form of Definition 0AIM, sufficiency for the quasi-separated axiom of Stacks 0ARN: a morphism of formal algebraic spaces with relatively representable relative diagonal is quasi-separated as soon as its base change to every member of a covering of the target as in Definition 0AIM is quasi-separated; the representability hypothesis is discharged for a source which is a formal algebraic space in …hasQuasiCompactDiagonal_of_atlas_of_isFormalAlgebraicSpace”.

Stacks 0ARS, clause (5) implies clause (1) for the quasi-separatedness axiom of Stacks 0ARN, in the covering form of Definition 0AIM. Let f : X ⟶ Y be a morphism of fppf sheaves on the big fppf site of S whose relative diagonal is representable by objects of the site. If there is a family {Y_j ⟶ Y} whose induced morphism from the coproduct is a surjection of sheaves — the covering condition of Definition 0AIM — such that every base change Y_j ×_Y X ⟶ Y_j of f is quasi-separated, then f is quasi-separated.

The hypothesis hrep is carried, and is discharged for a source which is a formal algebraic space in AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_of_atlas_of_isFormalAlgebraicSpace below.

theorem hasQuasiCompactDiagonal_of_atlas {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (I : Type (u + 1)) (Yj : I → FppfSheaf B S hS) (g : ∀ j, Yj j ⟶ Y)
    (hsurj : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
        Sheaf.instHasColimitsOfSize
      Sheaf.IsLocallySurjective (Sigma.desc g))
    (hrep : (fppfYoneda B S hS).relativelyRepresentable (pullback.diagonal f))
    (hqs : ∀ j, HasQuasiCompactDiagonal B S hS (pullback.snd f (g j))) :
    HasQuasiCompactDiagonal B S hS f

AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_of_atlas_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphismComparison.lean, line 588. The attribute's comment: “clause (5) in the covering form of Definition 0AIM, sufficiency for the quasi-separated axiom of Stacks 0ARN, in the source's form with no extra hypothesis: a morphism of formal algebraic spaces is quasi-separated as soon as its base change to every member of a covering of the target as in Definition 0AIM is quasi-separated”.

Stacks 0ARS, clause (5) implies clause (1) for the quasi-separatedness axiom of Stacks 0ARN, in the covering form of Definition 0AIM and in the source's own form: a morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S whose source is a formal algebraic space is quasi-separated as soon as its base change to every member of some covering of the target as in Definition 0AIM is. The representability hypothesis of AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_of_atlas is discharged by Stacks 0AIP and Stacks 0AN2.

theorem hasQuasiCompactDiagonal_of_atlas_of_isFormalAlgebraicSpace {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (I : Type (u + 1)) (Yj : I → FppfSheaf B S hS) (g : ∀ j, Yj j ⟶ Y)
    (hsurj : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
        Sheaf.instHasColimitsOfSize
      Sheaf.IsLocallySurjective (Sigma.desc g))
    (hX : IsFormalAlgebraicSpace B S hS X)
    (hqs : ∀ j, HasQuasiCompactDiagonal B S hS (pullback.snd f (g j))) :
    HasQuasiCompactDiagonal B S hS f

AlgebraicGeometry.FormalSpace.separationAxiom_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/QuasiSeparatedMorphismComparison.lean, line 703. The attribute's comment: “in full: the five conditions are equivalent for each of the two separation axioms of Definition 0ARN, quasi-separated and separated, for any morphism of formal algebraic spaces”.

Stacks 0ARS. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S. For each of the two separation axioms P of Stacks 0ARN — quasi-separated (the relative diagonal quasi-compact) and separated (the relative diagonal a closed immersion) — the following are equivalent: (1) f is P; (2) every base change Z ×_Y X ⟶ Z along a scheme Z ⟶ Y is P; (3) every such base change with Z affine is P; (4) for every affine scheme Z ⟶ Y the formal algebraic space Z ×_Y X is P in the sense of Stacks 0AJ7; (5) there is a covering {Y_j ⟶ Y} as in Definition 0AIM with every base change Y_j ×_Y X ⟶ Y_j being P.

The first conjunct is AlgebraicGeometry.FormalSpace.hasQuasiCompactDiagonal_tfae, the second AlgebraicGeometry.FormalSpace.isSeparatedMorphism_tfae.

theorem separationAxiom_tfae {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y) :
    letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) := Sheaf.instHasColimitsOfSize
    List.TFAE
      [HasQuasiCompactDiagonal B S hS f,
        ∀ (Z : BigFppfOver B S hS) (g : (fppfYoneda B S hS).obj Z ⟶ Y),
          HasQuasiCompactDiagonal B S hS (pullback.snd f g),
        ∀ (Z : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
          ∀ (g : (fppfYoneda B S hS).obj Z ⟶ Y),
            HasQuasiCompactDiagonal B S hS (pullback.snd f g),
        ∀ (Z : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
          ∀ (g : (fppfYoneda B S hS).obj Z ⟶ Y), IsQuasiSeparated B S hS (pullback f g),
        ∃ (I : Type (u + 1)) (Yj : I → FppfSheaf B S hS) (g : ∀ j, Yj j ⟶ Y),
          (∀ j, IsAffineFormalAlgebraicSpace B S hS (Yj j)) ∧
          (∀ j, ∃ hgj : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (g j).hom,
            Space.HasPropertyULift.{u + 1} B S hS
              (fun _ _ k ↦ Space.IsEtaleULift.{u + 1} B S hS k.hom) (g j).hom hgj) ∧
          Sheaf.IsLocallySurjective (Sigma.desc g) ∧
          ∀ j, HasQuasiCompactDiagonal B S hS (pullback.snd f (g j))] ∧
    List.TFAE
      [IsSeparatedMorphism B S hS f,
        ∀ (Z : BigFppfOver B S hS) (g : (fppfYoneda B S hS).obj Z ⟶ Y),
          IsSeparatedMorphism B S hS (pullback.snd f g),
        ∀ (Z : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
          ∀ (g : (fppfYoneda B S hS).obj Z ⟶ Y),
            IsSeparatedMorphism B S hS (pullback.snd f g),
        ∀ (Z : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj Z) →
          ∀ (g : (fppfYoneda B S hS).obj Z ⟶ Y), IsSeparated B S hS (pullback f g),
        ∃ (I : Type (u + 1)) (Yj : I → FppfSheaf B S hS) (g : ∀ j, Yj j ⟶ Y),
          (∀ j, IsAffineFormalAlgebraicSpace B S hS (Yj j)) ∧
          (∀ j, ∃ hgj : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (g j).hom,
            Space.HasPropertyULift.{u + 1} B S hS
              (fun _ _ k ↦ Space.IsEtaleULift.{u + 1} B S hS k.hom) (g j).hom hgj) ∧
          Sheaf.IsLocallySurjective (Sigma.desc g) ∧
          ∀ j, IsSeparatedMorphism B S hS (pullback.snd f (g j))]

AlgebraicGeometry.FormalSpace.hasRelativeDiagonal_iff_forall_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 632. The attribute's comment: “clauses (1) and (2): a relative diagonal condition holds for a morphism of formal algebraic spaces if and only if it holds for its base change to every scheme over the target”.

A morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S has relative diagonal P exactly when, for every object Z of the site and every morphism from the sheaf it represents to Y, the base change Z ×_Y X ⟶ Z of f has relative diagonal P.

theorem hasRelativeDiagonal_iff_forall_baseChange (P : MorphismProperty Scheme.{u})
    [P.RespectsIso] {X Y : FppfSheaf B S hS} (f : X ⟶ Y) :
    HasRelativeDiagonal B S hS P f ↔
      ∀ (U : BigFppfOver B S hS) (g : (fppfYoneda B S hS).obj U ⟶ Y),
        HasRelativeDiagonal B S hS P (pullback.snd f g)

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_iff_forall_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 651. The attribute's comment: “clauses (1) and (2) for separatedness: a morphism of formal algebraic spaces is separated if and only if its base change to every scheme over the target is separated”.

A morphism of fppf sheaves on the big fppf site of S is separated exactly when its base change to every scheme over the target is separated.

theorem isSeparatedMorphism_iff_forall_baseChange {X Y : FppfSheaf B S hS} (f : X ⟶ Y) :
    IsSeparatedMorphism B S hS f ↔
      ∀ (U : BigFppfOver B S hS) (g : (fppfYoneda B S hS).obj U ⟶ Y),
        IsSeparatedMorphism B S hS (pullback.snd f g)

AlgebraicGeometry.FormalSpace.hasRelativeDiagonal_iff_forall_affine_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 670. The attribute's comment: “clauses (1) and (3): a Zariski-local relative diagonal condition holds for a morphism of formal algebraic spaces if and only if its relative diagonal is relatively representable and the condition holds for the base change to every affine scheme over the target”.

A morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S has relative diagonal P, for P a Zariski-local property of morphisms of schemes, exactly when its relative diagonal is relatively representable and, for every affine object Z of the site and every morphism from the sheaf it represents to Y, the base change Z ×_Y X ⟶ Z of f has relative diagonal P.

theorem hasRelativeDiagonal_iff_forall_affine_baseChange (P : MorphismProperty Scheme.{u})
    [IsZariskiLocalAtTarget P] {X Y : FppfSheaf B S hS} (f : X ⟶ Y) :
    HasRelativeDiagonal B S hS P f ↔
      (fppfYoneda B S hS).relativelyRepresentable (pullback.diagonal f) ∧
        ∀ (U : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj U) →
          ∀ (g : (fppfYoneda B S hS).obj U ⟶ Y),
            HasRelativeDiagonal B S hS P (pullback.snd f g)

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_iff_forall_affine_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 691. The attribute's comment: “clauses (1) and (3) for separatedness: a morphism of formal algebraic spaces is separated if and only if its relative diagonal is relatively representable and its base change to every affine scheme over the target is separated”.

A morphism of fppf sheaves on the big fppf site of S is separated exactly when its relative diagonal is relatively representable and its base change to every affine scheme over the target is separated.

theorem isSeparatedMorphism_iff_forall_affine_baseChange {X Y : FppfSheaf B S hS} (f : X ⟶ Y) :
    IsSeparatedMorphism B S hS f ↔
      (fppfYoneda B S hS).relativelyRepresentable (pullback.diagonal f) ∧
        ∀ (U : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj U) →
          ∀ (g : (fppfYoneda B S hS).obj U ⟶ Y),
            IsSeparatedMorphism B S hS (pullback.snd f g)

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_iff_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 780. The attribute's comment: “clauses (3) and (4) for separatedness: a morphism of formal algebraic spaces to an affine scheme is separated if and only if its relative diagonal is relatively representable and its source is a separated formal algebraic space”.

A morphism f : X ⟶ Z of fppf sheaves on the big fppf site of S whose target is represented by an affine scheme of the site is separated exactly when its relative diagonal is relatively representable and the source X is separated as a single sheaf, in the sense of clause (2) of Stacks 0AJ6: the fibre product over X of any two affine scheme-valued points of X is affine with surjective comparison from the tensor product of their coordinate rings.

theorem isSeparatedMorphism_iff_isSeparated {X : FppfSheaf B S hS} {Z : BigFppfOver B S hS}
    (hZ : IsAffine ((BigFppfOver.toScheme B S hS).obj Z)) (f : X ⟶ (fppfYoneda B S hS).obj Z) :
    IsSeparatedMorphism B S hS f ↔
      (fppfYoneda B S hS).relativelyRepresentable (pullback.diagonal f) ∧
        IsSeparated B S hS X

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_iff_forall_affine_baseChange_of_relativelyRepresentable_diag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 846. The attribute's comment: “clauses (1) and (3) for separatedness with no extra conjunct, generalized past the source: the binder hX asks only that the absolute diagonal of the source be relatively representable, which every formal algebraic space satisfies by Stacks 0AIP, so the source's own case needs no such binder and is proved outright in …isSeparatedMorphism_iff_forall_affine_baseChange_of_isFormalAlgebraicSpace”.

A morphism of fppf sheaves whose source has relatively representable absolute diagonal is separated exactly when its base change to every affine scheme over the target is separated.

theorem isSeparatedMorphism_iff_forall_affine_baseChange_of_relativelyRepresentable_diag
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hX : (fppfYoneda B S hS).relativelyRepresentable (diag X)) :
    IsSeparatedMorphism B S hS f ↔
      ∀ (U : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj U) →
        ∀ (g : (fppfYoneda B S hS).obj U ⟶ Y),
          IsSeparatedMorphism B S hS (pullback.snd f g)

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_iff_isSeparated_of_relativelyRepresentable_diag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 863. The attribute's comment: “clauses (3) and (4) for separatedness with no extra conjunct, generalized past the source: the binder hX asks only that the absolute diagonal of the source be relatively representable, which every formal algebraic space satisfies by Stacks 0AIP, so the source's own case needs no such binder and is proved outright in …isSeparatedMorphism_iff_isSeparated_of_isFormalAlgebraicSpace”.

A morphism to an affine scheme out of a sheaf with relatively representable absolute diagonal is separated exactly when that sheaf is separated.

theorem isSeparatedMorphism_iff_isSeparated_of_relativelyRepresentable_diag
    {X : FppfSheaf B S hS} {Z : BigFppfOver B S hS}
    (hZ : IsAffine ((BigFppfOver.toScheme B S hS).obj Z)) (f : X ⟶ (fppfYoneda B S hS).obj Z)
    (hX : (fppfYoneda B S hS).relativelyRepresentable (diag X)) :
    IsSeparatedMorphism B S hS f ↔ IsSeparated B S hS X

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_iff_forall_affine_baseChange_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 877. The attribute's comment: “clauses (1) and (3) for separatedness, in the source's form with no extra conjunct: a morphism of formal algebraic spaces is separated if and only if its base change to every affine scheme over the target is separated”.

A morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S whose source is a formal algebraic space is separated exactly when its base change to every affine scheme over the target is separated.

theorem isSeparatedMorphism_iff_forall_affine_baseChange_of_isFormalAlgebraicSpace
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (hX : IsFormalAlgebraicSpace B S hS X) :
    IsSeparatedMorphism B S hS f ↔
      ∀ (U : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj U) →
        ∀ (g : (fppfYoneda B S hS).obj U ⟶ Y),
          IsSeparatedMorphism B S hS (pullback.snd f g)

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_iff_isSeparated_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 892. The attribute's comment: “clauses (3) and (4) for separatedness, in the source's form with no extra conjunct: a morphism from a formal algebraic space to an affine scheme is separated if and only if its source is a separated formal algebraic space”.

A morphism from a formal algebraic space to a sheaf represented by an affine scheme of the site is separated exactly when its source is a separated formal algebraic space, separatedness of a single sheaf being read as clause (2) of Stacks 0AJ6.

theorem isSeparatedMorphism_iff_isSeparated_of_isFormalAlgebraicSpace
    {X : FppfSheaf B S hS} {Z : BigFppfOver B S hS}
    (hZ : IsAffine ((BigFppfOver.toScheme B S hS).obj Z)) (f : X ⟶ (fppfYoneda B S hS).obj Z)
    (hX : IsFormalAlgebraicSpace B S hS X) :
    IsSeparatedMorphism B S hS f ↔ IsSeparated B S hS X

AlgebraicGeometry.FormalSpace.hasRelativeDiagonal_iff_forall_affine_baseChange_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 907. The attribute's comment: “clauses (1) and (3) for a relative diagonal condition, in the source's form with no extra conjunct: the condition holds for a morphism of formal algebraic spaces if and only if it holds for the base change to every affine scheme over the target”.

A morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S whose source is a formal algebraic space has relative diagonal P, for P a Zariski-local property of morphisms of schemes, exactly when its base change to every affine scheme over the target has relative diagonal P.

theorem hasRelativeDiagonal_iff_forall_affine_baseChange_of_isFormalAlgebraicSpace
    (P : MorphismProperty Scheme.{u}) [IsZariskiLocalAtTarget P] {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) (hX : IsFormalAlgebraicSpace B S hS X) :
    HasRelativeDiagonal B S hS P f ↔
      ∀ (U : BigFppfOver B S hS), IsAffine ((BigFppfOver.toScheme B S hS).obj U) →
        ∀ (g : (fppfYoneda B S hS).obj U ⟶ Y),
          HasRelativeDiagonal B S hS P (pullback.snd f g)

AlgebraicGeometry.FormalSpace.hasRelativeDiagonal_of_locallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1064. The attribute's comment: “the descent step of clause (5): a relative diagonal condition descends along a single locally surjective morphism onto the relative self-product, which is the atlas clause with the covering of Definition 0AIM replaced by one locally surjective morphism, and is not the atlas form itself”.

A relative diagonal condition for an fppf-local property P of morphisms of schemes descends along a locally surjective morphism b onto the relative self-product X ×_Y X: if the base change of the relative diagonal of f along b has P relative to the site, and the relative diagonal is relatively representable, then f has relative diagonal P.

theorem hasRelativeDiagonal_of_locallySurjective (P : MorphismProperty Scheme.{u})
    [P.IsStableUnderBaseChange] [P.IsLocalAtTarget Scheme.fppfPrecoverage]
    {X Y W : FppfSheaf B S hS} (f : X ⟶ Y) (b : W ⟶ pullback f f)
    (hb : Sheaf.IsLocallySurjective b)
    (hrep : (fppfYoneda B S hS).relativelyRepresentable (pullback.diagonal f))
    (hbase : (MorphismProperty.inverseImage P (BigFppfOver.toScheme B S hS)).relative
      (fppfYoneda B S hS) (pullback.snd (pullback.diagonal f) b)) :
    HasRelativeDiagonal B S hS P f

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_of_locallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1088. The attribute's comment: “the descent step of clause (5) for separatedness: separatedness descends along a single locally surjective morphism onto the relative self-product, which is the atlas clause with the covering of Definition 0AIM replaced by one locally surjective morphism, and is not the atlas form itself”.

Separatedness of a morphism of fppf sheaves whose relative diagonal is relatively representable descends along a locally surjective morphism onto the relative self-product.

theorem isSeparatedMorphism_of_locallySurjective {X Y W : FppfSheaf B S hS} (f : X ⟶ Y)
    (b : W ⟶ pullback f f) (hb : Sheaf.IsLocallySurjective b)
    (hrep : (fppfYoneda B S hS).relativelyRepresentable (pullback.diagonal f))
    (hbase : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.IsClosedImmersion.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).relative (fppfYoneda B S hS)
      (pullback.snd (pullback.diagonal f) b)) :
    IsSeparatedMorphism B S hS f

AlgebraicGeometry.FormalSpace.hasRelativeDiagonal_of_locallySurjectiveFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1111. The attribute's comment: “the descent step of clause (5) for a covering family: a relative diagonal condition descends along a family of morphisms onto the relative self-product whose induced morphism out of the coproduct is a surjection of sheaves”.

A relative diagonal condition for an fppf-local property P of morphisms of schemes descends along a family (b i : W i ⟶ X ×_Y X) of morphisms onto the relative self-product whose induced morphism out of the coproduct is a surjection of sheaves: if the base change of the relative diagonal of f along each b i has P relative to the site, and the relative diagonal is relatively representable, then f has relative diagonal P.

theorem hasRelativeDiagonal_of_locallySurjectiveFamily (P : MorphismProperty Scheme.{u})
    [P.IsStableUnderBaseChange] [P.IsLocalAtTarget Scheme.fppfPrecoverage]
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y) (I : Type (u + 1)) (W : I → FppfSheaf B S hS)
    (b : ∀ i, W i ⟶ pullback f f)
    (hb : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
        Sheaf.instHasColimitsOfSize
      Sheaf.IsLocallySurjective (Sigma.desc b))
    (hrep : (fppfYoneda B S hS).relativelyRepresentable (pullback.diagonal f))
    (hbase : ∀ i, (MorphismProperty.inverseImage P (BigFppfOver.toScheme B S hS)).relative
      (fppfYoneda B S hS) (pullback.snd (pullback.diagonal f) (b i))) :
    HasRelativeDiagonal B S hS P f

AlgebraicGeometry.FormalSpace.exists_atlas_hasRelativeDiagonal_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1141. The attribute's comment: “clause (5) in the covering form of Definition 0AIM, necessity: a relative diagonal condition for a morphism of formal algebraic spaces holds for the base change to every member of some covering of the target as in Definition 0AIM”.

If Y is a formal algebraic space and the morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S has relative diagonal P, then there is a covering {Y_j ⟶ Y} as in Definition 0AIM such that the base change Y_j ×_Y X ⟶ Y_j of f has relative diagonal P for every j.

theorem exists_atlas_hasRelativeDiagonal_pullback_snd (P : MorphismProperty Scheme.{u})
    [P.RespectsIso] {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hY : IsFormalAlgebraicSpace B S hS Y) (hf : HasRelativeDiagonal B S hS P f) :
    letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) := Sheaf.instHasColimitsOfSize
    ∃ (I : Type (u + 1)) (Yj : I → FppfSheaf B S hS) (g : ∀ j, Yj j ⟶ Y),
      (∀ j, IsAffineFormalAlgebraicSpace B S hS (Yj j)) ∧
      (∀ j, ∃ hgj : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (g j).hom,
        Space.HasPropertyULift.{u + 1} B S hS
          (fun _ _ k ↦ Space.IsEtaleULift.{u + 1} B S hS k.hom) (g j).hom hgj) ∧
      Sheaf.IsLocallySurjective (Sigma.desc g) ∧
      ∀ j, HasRelativeDiagonal B S hS P (pullback.snd f (g j))

AlgebraicGeometry.FormalSpace.exists_atlas_isSeparatedMorphism_pullback_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1161. The attribute's comment: “clause (5) in the covering form of Definition 0AIM, necessity for separatedness: a separated morphism of formal algebraic spaces has separated base change to every member of some covering of the target as in Definition 0AIM”.

If Y is a formal algebraic space and f : X ⟶ Y is separated then there is a covering {Y_j ⟶ Y} as in Definition 0AIM along which every base change of f is separated.

theorem exists_atlas_isSeparatedMorphism_pullback_snd {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hY : IsFormalAlgebraicSpace B S hS Y) (hf : IsSeparatedMorphism B S hS f) :
    letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) := Sheaf.instHasColimitsOfSize
    ∃ (I : Type (u + 1)) (Yj : I → FppfSheaf B S hS) (g : ∀ j, Yj j ⟶ Y),
      (∀ j, IsAffineFormalAlgebraicSpace B S hS (Yj j)) ∧
      (∀ j, ∃ hgj : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS (g j).hom,
        Space.HasPropertyULift.{u + 1} B S hS
          (fun _ _ k ↦ Space.IsEtaleULift.{u + 1} B S hS k.hom) (g j).hom hgj) ∧
      Sheaf.IsLocallySurjective (Sigma.desc g) ∧
      ∀ j, IsSeparatedMorphism B S hS (pullback.snd f (g j))

AlgebraicGeometry.FormalSpace.hasRelativeDiagonal_of_atlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1228. The attribute's comment: “clause (5) in the covering form of Definition 0AIM, sufficiency for a relative diagonal condition: the condition holds for a morphism of formal algebraic spaces with relatively representable relative diagonal as soon as it holds for the base change to every member of a covering of the target as in Definition 0AIM”.

Let f : X ⟶ Y be a morphism of fppf sheaves on the big fppf site of S and let P be a property of morphisms of schemes which is stable under base change and local on the target for the fppf topology. If there is a family {Y_j ⟶ Y} whose induced morphism from the coproduct is a surjection of sheaves — the covering condition of Definition 0AIM — such that every base change Y_j ×_Y X ⟶ Y_j of f has relative diagonal P, and the relative diagonal of f is relatively representable, then f has relative diagonal P.

theorem hasRelativeDiagonal_of_atlas (P : MorphismProperty Scheme.{u})
    [P.IsStableUnderBaseChange] [P.IsLocalAtTarget Scheme.fppfPrecoverage]
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (I : Type (u + 1)) (Yj : I → FppfSheaf B S hS) (g : ∀ j, Yj j ⟶ Y)
    (hsurj : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
        Sheaf.instHasColimitsOfSize
      Sheaf.IsLocallySurjective (Sigma.desc g))
    (hrep : (fppfYoneda B S hS).relativelyRepresentable (pullback.diagonal f))
    (hP : ∀ j, HasRelativeDiagonal B S hS P (pullback.snd f (g j))) :
    HasRelativeDiagonal B S hS P f

AlgebraicGeometry.FormalSpace.hasRelativeDiagonal_of_atlas_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1256. The attribute's comment: “clause (5) in the covering form of Definition 0AIM, sufficiency for a relative diagonal condition, in the source's form with no extra conjunct: the condition holds for a morphism of formal algebraic spaces as soon as it holds for the base change to every member of a covering of the target as in Definition 0AIM”.

A morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S whose source is a formal algebraic space has relative diagonal P as soon as its base change to every member of some covering of the target as in Definition 0AIM does.

theorem hasRelativeDiagonal_of_atlas_of_isFormalAlgebraicSpace (P : MorphismProperty Scheme.{u})
    [P.IsStableUnderBaseChange] [P.IsLocalAtTarget Scheme.fppfPrecoverage]
    {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (I : Type (u + 1)) (Yj : I → FppfSheaf B S hS) (g : ∀ j, Yj j ⟶ Y)
    (hsurj : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
        Sheaf.instHasColimitsOfSize
      Sheaf.IsLocallySurjective (Sigma.desc g))
    (hX : IsFormalAlgebraicSpace B S hS X)
    (hP : ∀ j, HasRelativeDiagonal B S hS P (pullback.snd f (g j))) :
    HasRelativeDiagonal B S hS P f

AlgebraicGeometry.FormalSpace.isSeparatedMorphism_of_atlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SeparatedMorphism.lean, line 1277. The attribute's comment: “clause (5) in the covering form of Definition 0AIM, sufficiency for separatedness: a morphism of formal algebraic spaces is separated as soon as its base change to every member of a covering of the target as in Definition 0AIM is separated”.

Let f : X ⟶ Y be a morphism of fppf sheaves on the big fppf site of S. If there is a family {Y_j ⟶ Y} whose induced morphism from the coproduct is a surjection of sheaves — which is the covering condition of Definition 0AIM — such that every base change Y_j ×_Y X ⟶ Y_j of f is separated, then f is separated.

theorem isSeparatedMorphism_of_atlas {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (I : Type (u + 1)) (Yj : I → FppfSheaf B S hS) (g : ∀ j, Yj j ⟶ Y)
    (hsurj : letI : HasColimitsOfSize.{u + 1, u + 1} (FppfSheaf B S hS) :=
        Sheaf.instHasColimitsOfSize
      Sheaf.IsLocallySurjective (Sigma.desc g))
    (hsep : ∀ j, IsSeparatedMorphism B S hS (pullback.snd f (g j))) :
    IsSeparatedMorphism B S hS f

Sources

• Section 87.30, Tag 0ARM
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.FormalSpace.HasQuasiCompactDiagonal · AlgebraicGeometry.FormalSpace.IsSeparatedMorphism · AlgebraicGeometry.FormalSpace.HasQuasiCompactDiagonal.of_isPullback · AlgebraicGeometry.FormalSpace.isSeparatedMorphism_of_isPullback · AlgebraicGeometry.FormalSpace.isQuasiCompact_mapDesc · AlgebraicGeometry.FormalSpace.isSeparatedMorphism_mapDesc · AlgebraicGeometry.FormalSpace.relativelyRepresentable_mapDesc_of_isAffineFormal · AlgebraicGeometry.FormalSpace.relative_locallyQuasiFinite_mapDesc_of_isAffineFormal

Section87.31 Proper morphisms#

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

Tag 0AM6, a definition

Tag 0AM6 in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsProper, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Proper.lean, line 111.

Stacks 0AM6. A morphism of formal algebraic spaces over S is proper when it is representable by algebraic spaces and every base change of it along a scheme-valued point of its target is a morphism of algebraic spaces which is proper, that is, separated, of finite type and universally closed. The condition makes sense, and is stated, for an arbitrary morphism of fppf sheaves on the big fppf site of S.

abbrev IsProper {X Y : FppfSheaf B S hS} (f : X ⟶ Y) : Prop

AlgebraicGeometry.FormalSpace.isProper_of_forall_surjective_etale_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ProperEtaleLocal.lean, line 85. The attribute's comment: “local on the target”.

Properness of morphisms of formal algebraic spaces is local on the target. A morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S is proper in the sense of Stacks 0AM6 as soon as every scheme-valued point ξ : U ⟶ Y of its target admits a morphism q : U' ⟶ U of the site, surjective and étale on underlying schemes, such that the base change of f along U' ⟶ U ⟶ Y is an algebraic space over S proper over U'.

Being an algebraic space descends along q by Stacks 0BGR and properness by Stacks 0422, both applied to the base change of the universe-lifted Yoneda image of q along the projection of the base change of f along ξ.

theorem isProper_of_forall_surjective_etale_cover {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (h : ∀ (U : BigFppfOver B S hS) (ξ : (uliftYoneda.{u + 1}).obj U ⟶ Y.obj),
      ∃ (U' : BigFppfOver B S hS) (q : U' ⟶ U),
        Surjective ((BigFppfOver.toScheme B S hS).map q) ∧
        Etale ((BigFppfOver.toScheme B S hS).map q) ∧
        Space.IsAlgebraicSpaceULift.{u + 1} B S hS
          (pullback ((uliftYoneda.{u + 1}).map q ≫ ξ) f.hom) ∧
        Space.IsProperULift.{u + 1} B S hS
          (pullback.fst ((uliftYoneda.{u + 1}).map q ≫ ξ) f.hom)) :
    IsProper B S hS f

AlgebraicGeometry.FormalSpace.isProper_of_isRepresentable_of_forall_fppfFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ProperEtaleLocal.lean, line 152. The attribute's comment: “local on the target for a covering family, given representability”.

Properness of a morphism representable by algebraic spaces is local on the target for a covering family of the site. Let f : X ⟶ Y be a morphism of fppf sheaves on the big fppf site of S which is representable by algebraic spaces, and suppose every scheme-valued point ξ : U ⟶ Y of its target admits a family {qᵢ : Vᵢ ⟶ U} of morphisms of the site whose Yoneda images form an fppf covering family of U, such that the base change of f along each Vᵢ ⟶ U ⟶ Y is proper as a morphism of algebraic spaces. Then f is proper in the sense of Stacks 0AM6.

Unlike AlgebraicGeometry.FormalSpace.isProper_of_forall_surjective_etale_cover this takes a family and not one morphism, so it needs no coproduct of the members inside the site; what it asks instead is that f be representable by algebraic spaces, since being an algebraic space is the half of properness which the family form of Stacks 0422 does not descend. The base change of f along Vᵢ ⟶ U ⟶ Y is compared with the base change along qᵢ of the base change along ξ by CategoryTheory.Limits.pullbackRightPullbackFstIso.

theorem isProper_of_isRepresentable_of_forall_fppfFamily {X Y : FppfSheaf B S hS} (f : X ⟶ Y)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (h : ∀ (U : BigFppfOver B S hS) (ξ : (uliftYoneda.{u + 1}).obj U ⟶ Y.obj),
      ∃ (Idx : Type (u + 1)) (V : Idx → BigFppfOver B S hS) (q : ∀ i, V i ⟶ U),
        Space.IsFppfCovering B S hS (fun i => yoneda.obj (V i))
          (fun i => yoneda.map (q i)) ∧
        ∀ i, Space.IsProperULift.{u + 1} B S hS
          (pullback.fst ((uliftYoneda.{u + 1}).map (q i) ≫ ξ) f.hom)) :
    IsProper B S hS f

Tag 0ART, a lemma

Tag 0ART in the Stacks Project.

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

Stacks 0ART, (1) implies (2). A base change of a proper morphism of formal algebraic spaces over S along a scheme over S in the site is proper. This is the base change stability of properness, which needs no hypothesis on the base.

theorem IsProper.isProperOnSchemeBaseChanges {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (hf : IsProper B S hS f) : IsProperOnSchemeBaseChanges B S hS f

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

Stacks 0ART, (2) implies (1). A morphism of formal algebraic spaces over S all of whose base changes along schemes over S in the site are proper is proper: the base change along a scheme-valued point of the target, read at the identity point of its own target, is that base change itself.

theorem isProper_of_isProperOnSchemeBaseChanges {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (h : IsProperOnSchemeBaseChanges B S hS f) : IsProper B S hS f

AlgebraicGeometry.FormalSpace.isProper_iff_isProperOnSchemeBaseChanges, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Proper.lean, line 276. The attribute's comment: “(1) is equivalent to (2)”.

Stacks 0ART, (1) is equivalent to (2). A morphism of formal algebraic spaces over S is proper exactly when each of its base changes along a scheme over S in the site is proper.

theorem isProper_iff_isProperOnSchemeBaseChanges {X Y : FppfSheaf B S hS} (f : X ⟶ Y) :
    IsProper B S hS f ↔ IsProperOnSchemeBaseChanges B S hS f

AlgebraicGeometry.FormalSpace.IsProperOnSchemeBaseChanges.isProperOnAffineBaseChanges, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Proper.lean, line 284. The attribute's comment: “(2) implies (3)”.

Stacks 0ART, (2) implies (3). The base change condition over all schemes over S in the site restricts to the affine ones.

theorem IsProperOnSchemeBaseChanges.isProperOnAffineBaseChanges {X Y : FppfSheaf B S hS}
    {f : X ⟶ Y} (h : IsProperOnSchemeBaseChanges B S hS f) :
    IsProperOnAffineBaseChanges B S hS f

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

Stacks 0ART, (3) implies (4). If every base change of a morphism of formal algebraic spaces over S along an affine scheme Z over S in the site is proper, then every such base change is an algebraic space over S and its projection to Z is proper as a morphism of algebraic spaces: both are the content of properness of that base change read at the identity point of Z.

theorem IsProperOnAffineBaseChanges.isAlgebraicAndProper {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (h : IsProperOnAffineBaseChanges B S hS f) :
    IsAlgebraicAndProperOnAffineBaseChanges B S hS f

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

Stacks 0ART, (1) implies (5). A proper morphism of formal algebraic spaces over S has a covering of its target as in Definition 0AIM all of whose base changes of the morphism are proper: any atlas of the target witnessing that it is a formal algebraic space will do, properness being stable under base change.

theorem IsProper.hasProperFormalAtlas {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (hY : IsFormalAlgebraicSpace B S hS Y) (hf : IsProper B S hS f) :
    HasProperFormalAtlas B S hS f

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

Stacks 0ART, (4) implies (3). If every base change of a morphism of formal algebraic spaces over S along an affine scheme Z over S in the site is an algebraic space over S whose projection to Z is proper as a morphism of algebraic spaces, then every such base change is proper as a morphism of formal algebraic spaces: over a scheme of the site the two conditions agree, properness of morphisms of algebraic spaces being stable under base change along a scheme-valued point.

theorem IsAlgebraicAndProperOnAffineBaseChanges.isProperOnAffineBaseChanges
    {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (h : IsAlgebraicAndProperOnAffineBaseChanges B S hS f) :
    IsProperOnAffineBaseChanges B S hS f

AlgebraicGeometry.FormalSpace.isProperOnAffineBaseChanges_iff_isAlgebraicAndProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ProperAffineCriterion.lean, line 262. The attribute's comment: “(3) is equivalent to (4)”.

Stacks 0ART, (3) is equivalent to (4). Over an affine scheme of the site, properness of the base change as a morphism of formal algebraic spaces and the conjunction of being an algebraic space with properness of the projection as a morphism of algebraic spaces are the same condition.

theorem isProperOnAffineBaseChanges_iff_isAlgebraicAndProper {X Y : FppfSheaf B S hS}
    (f : X ⟶ Y) :
    IsProperOnAffineBaseChanges B S hS f ↔
      IsAlgebraicAndProperOnAffineBaseChanges B S hS f

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

Stacks 0ART, (3) implies (1). A morphism of formal algebraic spaces over S all of whose base changes along affine schemes over S in the site are proper is proper.

Condition (3) gives, at an affine point Z ⟶ Y, properness of the chosen base change as a morphism of formal algebraic spaces; read at the identity point of Z (Stacks 0ART, (3) implies (4)) that is exactly the hypothesis of AlgebraicGeometry.FormalSpace.isProper_of_affine_base_changes, namely that the base change is an algebraic space over S proper over Z.

theorem IsProperOnAffineBaseChanges.isProper {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (h : IsProperOnAffineBaseChanges B S hS f) : IsProper B S hS f

AlgebraicGeometry.FormalSpace.isProper_iff_isProperOnAffineBaseChanges, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ProperAffineLocal.lean, line 242. The attribute's comment: “(1) is equivalent to (3)”.

Stacks 0ART, (1) is equivalent to (3). A morphism of formal algebraic spaces over S is proper exactly when each of its base changes along an affine scheme over S in the site is proper.

theorem isProper_iff_isProperOnAffineBaseChanges {X Y : FppfSheaf B S hS} (f : X ⟶ Y) :
    IsProper B S hS f ↔ IsProperOnAffineBaseChanges B S hS f

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

Stacks 0ART, (5) implies (1). A morphism of formal algebraic spaces over S admitting one covering of its target as in Definition 0AIM all of whose base changes of the morphism are proper is itself proper.

Properness is local on the target for a surjective étale covering by one object of the site, and such a covering of each scheme-valued point of Y is assembled from the given covering: its joint surjectivity puts every point of the scheme-valued point inside an affine étale neighbourhood over which the point factors through one member of the covering, and the coproduct of a u-small refinement of those neighbourhoods is the covering object.

theorem HasProperFormalAtlas.isProper {X Y : FppfSheaf B S hS} {f : X ⟶ Y}
    (h : HasProperFormalAtlas B S hS f) : IsProper B S hS f

AlgebraicGeometry.FormalSpace.isProper_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ProperTfae.lean, line 76. The attribute's comment: “(1), (2), (3) and (4) are equivalent”.

Stacks 0ART, conditions (1), (2), (3) and (4) are equivalent. For a morphism of fppf sheaves on the big fppf site of S: being proper, having every base change along a scheme of the site proper, having every base change along an affine scheme of the site proper, and having every base change along an affine scheme Z of the site be an algebraic space over S proper over Z, are the same condition.

The cycle is closed by (3) ⇒ (1). Condition (5) of the source asks nothing of X or Y in AlgebraicGeometry.FormalSpace.HasProperFormalAtlas.isProper but needs Y to be a formal algebraic space to follow from the others, so it is added to the list separately in AlgebraicGeometry.FormalSpace.isProper_tfae_of_isFormalAlgebraicSpace.

theorem isProper_tfae {X Y : FppfSheaf B S hS} (f : X ⟶ Y) :
    List.TFAE
      [IsProper B S hS f,
        IsProperOnSchemeBaseChanges B S hS f,
        IsProperOnAffineBaseChanges B S hS f,
        IsAlgebraicAndProperOnAffineBaseChanges B S hS f]

AlgebraicGeometry.FormalSpace.isProper_tfae_of_isFormalAlgebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ProperTfae.lean, line 100. The attribute's comment: “all five conditions are equivalent”.

Stacks 0ART. For a morphism f : X ⟶ Y of fppf sheaves on the big fppf site of S whose target is a formal algebraic space over S, the five conditions of the source are equivalent: f is proper; every base change of f along a scheme of the site is proper; every base change of f along an affine scheme of the site is proper; every base change of f along an affine scheme Z of the site is an algebraic space over S proper over Z; and there is one covering of Y as in Definition 0AIM all of whose base changes of f are proper.

The first four are AlgebraicGeometry.FormalSpace.isProper_tfae, which needs no hypothesis on Y; the fifth is attached by AlgebraicGeometry.FormalSpace.IsProper.hasProperFormalAtlas, which reads an atlas of Y off the hypothesis, and by AlgebraicGeometry.FormalSpace.HasProperFormalAtlas.isProper.

theorem isProper_tfae_of_isFormalAlgebraicSpace {X Y : FppfSheaf B S hS}
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE
      [IsProper B S hS f,
        IsProperOnSchemeBaseChanges B S hS f,
        IsProperOnAffineBaseChanges B S hS f,
        IsAlgebraicAndProperOnAffineBaseChanges B S hS f,
        HasProperFormalAtlas B S hS f]

Tag 0GBT, a lemma

Tag 0GBT in the Stacks Project.

AlgebraicGeometry.FormalSpace.IsProper.of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Proper.lean, line 146.

Stacks 0GBT. A base change of a proper morphism of formal algebraic spaces over S is proper: representability by algebraic spaces is stable under base change, and so is the Bootstrap condition of Stacks 03XZ, properness of morphisms of algebraic spaces being invariant under isomorphism.

theorem IsProper.of_isPullback {W X Z Y : FppfSheaf B S hS}
    {p : W ⟶ Z} {q : W ⟶ X} {g : Z ⟶ Y} {f : X ⟶ Y} (sq : IsPullback p q g f)
    (hf : IsProper B S hS f) : IsProper B S hS p

Sources

• Section 87.31, Tag 0AM5
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.FormalSpace.IsProper · AlgebraicGeometry.FormalSpace.isProper_of_forall_surjective_etale_cover · AlgebraicGeometry.FormalSpace.isProper_of_isRepresentable_of_forall_fppfFamily · AlgebraicGeometry.FormalSpace.IsProper.isProperOnSchemeBaseChanges · AlgebraicGeometry.FormalSpace.isProper_of_isProperOnSchemeBaseChanges · AlgebraicGeometry.FormalSpace.isProper_iff_isProperOnSchemeBaseChanges · AlgebraicGeometry.FormalSpace.IsProperOnSchemeBaseChanges.isProperOnAffineBaseChanges · AlgebraicGeometry.FormalSpace.IsProperOnAffineBaseChanges.isAlgebraicAndProper

Section87.32 Formal algebraic spaces and fpqc coverings#

Section 87.32 of the Stacks Project, Tag 0AQC. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AQD, a lemma

Tag 0AQD in the Stacks Project.

AlgebraicGeometry.FormalSpace.isSheaf_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/FpqcSheafGlueing.lean, line 182.

Stacks 0AQD. A formal algebraic space X over a scheme S contained in a big fppf site B satisfies the sheaf property for the fpqc topology of the big fppf site of S.

By AlgebraicGeometry.FormalSpace.isSheaf_fpqc_of_isSheafFor_singleton_affine_of_formal it is enough to check the sheaf condition for one surjective, flat, quasi-compact morphism of the site, which is AlgebraicGeometry.FormalSpace.isSheafFor_singleton_of_isFormalAlgebraicSpace.

theorem isSheaf_fpqc {X : FppfSheaf B S hS}
    (hX : IsFormalAlgebraicSpace B S hS X) :
    Presheaf.IsSheaf
      ((Scheme.fpqcPrecoverage.comap (BigFppfOver.toScheme B S hS)).toGrothendieck) X.obj

Sources

• Section 87.32, Tag 0AQC
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.FormalSpace.isSheaf_fpqc

Section87.33 Maps out of affine formal schemes#

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

Tag 0AQF, a lemma

Tag 0AQF in the Stacks Project.

AlgebraicGeometry.FormalSpace.exists_formalSpectrumToSpec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MapsToAffine.lean, line 180. The attribute's comment: “canonical map”.

The canonical formal-to-ordinary-spectrum map exists and restricts to the quotient-spectrum map at every stage.

public theorem exists_formalSpectrumToSpec
    (D : QuotientSystem B S hS A)
    (hAS : B.Contains (Spec (.of A))) (fA : Spec (.of A) ⟶ S)
    (hcompat : ∀ J : { I : Ideal A // TopologicalRing.IsWeakIdealOfDefinition I },
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk J.1)) ≫ fA = D.overS J) :
    ∃ q : formalSpectrum D ⟶
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj
        ((BigAffineFppf.inclusion B S hS).obj (specOver hAS fA)),
      ∀ J : { I : Ideal A // TopologicalRing.IsWeakIdealOfDefinition I },
        formalSpectrumInclusion D (OrderDual.toDual J) ≫ q =
          (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).map
            ((BigAffineFppf.inclusion B S hS).map
              (stageToSpec D hAS fA J (hcompat J)))

AlgebraicGeometry.FormalSpace.bijective_map_into_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MapsToAffine.lean, line 495. The attribute's comment: “bijectivity”.

For an affine target over S, restriction to the quotient spectra is a bijection on morphisms over S. The ordinary spectrum need not belong to the chosen big fppf site.

public theorem bijective_map_into_affine
    [IsTopologicalRing A] [IsLinearTopology A A]
    (hA : TopologicalRing.IsWeaklyAdmissible A)
    (D : QuotientSystem B S hS A)
    (fA : Spec (.of A) ⟶ S)
    (hcompat : ∀ J : { I : Ideal A // TopologicalRing.IsWeakIdealOfDefinition I },
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk J.1)) ≫ fA = D.overS J)
    (X : BigAffineFppf B S hS) :
    Function.Bijective (restrictToFormalSpectrum D fA hcompat
      ((BigAffineFppf.inclusion B S hS).obj X))

Tag 0AQG, a lemma

Tag 0AQG in the Stacks Project.

AlgebraicGeometry.FormalSpace.existsUnique_equiv_specHom_formalSpectrumHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MapsToScheme.lean, line 610. References: SGA 3 XV (1.4).

The canonical bijection between maps from a spectrum and from its formal spectrum to an S-scheme, characterized by restriction to every weak quotient.

public theorem existsUnique_equiv_specHom_formalSpectrumHom
    {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)
    (D : QuotientSystem B S hS A)
    (p : Spec (.of A) ⟶ S)
    (hp : ∀ J : { I : Ideal A // TopologicalRing.IsWeakIdealOfDefinition I },
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk J.1)) ≫ p = D.overS J)
    (I : Ideal A) (hI : TopologicalRing.IsWeakIdealOfDefinition I)
    [IsLocalRing (A ⧸ I)]
    (X : Scheme.{u}) (hX : B.Contains X) (xS : X ⟶ S) :
    let Xo : BigFppfOver B S hS :=
      Over.mk (ObjectProperty.homMk xS : B.obj hX ⟶ B.obj hS)
    ∃! e : ((Over.mk p : Over S) ⟶ (Over.mk xS : Over S)) ≃
        (formalSpectrum D ⟶
          (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj Xo),
      ∀ (f : (Over.mk p : Over S) ⟶ (Over.mk xS : Over S))
    (J : { I : Ideal A // TopologicalRing.IsWeakIdealOfDefinition I }),
        ∃ g : (BigAffineFppf.inclusion B S hS).obj (D.stage J) ⟶ Xo,
          B.inclusion.map g.left =
              Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk J.1)) ≫ f.left ∧
            formalSpectrumInclusion D (OrderDual.toDual J) ≫ e f =
              (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).map g

Tag 0AQH, a lemma

Tag 0AQH in the Stacks Project.

AlgebraicGeometry.FormalSpace.injective_map_into_algebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MapsToAlgebraicSpace.lean, line 288. The attribute's comment: “injectivity”. References: SGA 3 XV (1.4), “injectivity of (*)”; SGA 3 XI (3.3), “injectivity”.

The injectivity half of Stacks 0AQH, in the shape of the bijectivity statement: restriction along the canonical map Spf R ⟶ Spec R is injective on morphisms to an algebraic space over S.

Only the second cofinality condition on the weak ideals of definition is used — that every power of the maximal ideal contains one — and the Noetherian hypothesis on R enters only through locality and completeness.

public theorem injective_map_into_algebraicSpace
    {R : Type u} [CommRing R] [TopologicalSpace R]
    (hR : IsNoetherianCompleteLocalRing R)
    (D : QuotientSystem B S hS R)
    (hD : ∀ n : ℕ, ∃ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      J.1 ≤ (@IsLocalRing.maximalIdeal R _ hR.isLocal) ^ n)
    (hRS : B.Contains (Spec (.of R))) (p : Spec (.of R) ⟶ S)
    (hp : ∀ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk J.1)) ≫ p = D.overS J)
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X) :
    Function.Injective (fun f :
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj
        ((BigAffineFppf.inclusion B S hS).obj (specOver hRS p)) ⟶ upliftedSheaf X hX =>
      formalSpectrumToSpec D hRS p hp ≫ f)

AlgebraicGeometry.FormalSpace.surjective_map_into_algebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MapsToAlgebraicSpace.lean, line 2885. The attribute's comment: “surjectivity”.

The surjectivity half of Stacks 0AQH. Restriction along the canonical map Spf R ⟶ Spec R hits every morphism from the formal spectrum of a Noetherian complete local S-algebra R to an algebraic space over S.

Both cofinality conditions on the weak ideals of definition are used, so that the formal spectrum of the quotient system is the 𝔪-adic one.

public theorem surjective_map_into_algebraicSpace
    {R : Type u} [CommRing R] [TopologicalSpace R]
    (hR : IsNoetherianCompleteLocalRing R)
    (D : QuotientSystem B S hS R)
    (hD₁ : ∀ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      ∃ n : ℕ, (@IsLocalRing.maximalIdeal R _ hR.isLocal) ^ n ≤ J.1)
    (hD : ∀ n : ℕ, ∃ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      J.1 ≤ (@IsLocalRing.maximalIdeal R _ hR.isLocal) ^ n)
    (hRS : B.Contains (Spec (.of R))) (p : Spec (.of R) ⟶ S)
    (hp : ∀ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk J.1)) ≫ p = D.overS J)
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X) :
    Function.Surjective (fun f :
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj
        ((BigAffineFppf.inclusion B S hS).obj (specOver hRS p)) ⟶ upliftedSheaf X hX =>
      formalSpectrumToSpec D hRS p hp ≫ f)

AlgebraicGeometry.FormalSpace.bijective_map_into_algebraicSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/MapsToAlgebraicSpace.lean, line 2907.

Stacks 0AQH. For R a Noetherian complete local S-algebra and X an algebraic space over S, restriction along Spf R ⟶ Spec R is a bijection Mor_S(Spec R, X) ⟶ Mor_S(Spf R, X).

public theorem bijective_map_into_algebraicSpace
    {R : Type u} [CommRing R] [TopologicalSpace R]
    (hR : IsNoetherianCompleteLocalRing R)
    (D : QuotientSystem B S hS R)
    (hD₁ : ∀ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      ∃ n : ℕ, (@IsLocalRing.maximalIdeal R _ hR.isLocal) ^ n ≤ J.1)
    (hD : ∀ n : ℕ, ∃ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      J.1 ≤ (@IsLocalRing.maximalIdeal R _ hR.isLocal) ^ n)
    (hRS : B.Contains (Spec (.of R))) (p : Spec (.of R) ⟶ S)
    (hp : ∀ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk J.1)) ≫ p = D.overS J)
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X) :
    Function.Bijective (fun f :
      (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj
        ((BigAffineFppf.inclusion B S hS).obj (specOver hRS p)) ⟶ upliftedSheaf X hX =>
      formalSpectrumToSpec D hRS p hp ≫ f)

Tag 0GBU, a lemma

Tag 0GBU in the Stacks Project.

AlgebraicGeometry.FormalSpace.existsUnique_algebraization_of_adic_into_completion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicMapsIntoCompletion.lean, line 369. The attribute's comment: “The algebraization, its existence and uniqueness, and both inclusions of its fibre condition g⁻¹(T) = {𝔪}, the second of them by Krull's intersection theorem.”.

Stacks 0GBU. Let S be a scheme, X an algebraic space over S and T a closed set of points of X whose complementary open subspace has quasi-compact inclusion into X. Let R be a Noetherian complete local S-algebra whose spectrum lies in the site, equipped with a quotient system whose weak ideals of definition are cofinal among the powers of the maximal ideal. Then an adic morphism p : Spf R ⟶ X_{/T} into the completion of X along T admits a unique algebraization: a unique morphism g : Spec R ⟶ X restricting on Spf R to the composite Spf R ⟶ X_{/T} ⟶ X and satisfying g⁻¹(T) = {𝔪}.

The existence and uniqueness of the algebraization are the two halves of Stacks 0AQH, AlgebraicGeometry.FormalSpace.bijective_map_into_algebraicSpace. The inclusion {𝔪} ⊆ g⁻¹(T) of the fibre condition is AlgebraicGeometry.FormalSpace.pointsMap_mem_of_pointsToScheme_eq_closedPoint and the reverse inclusion g⁻¹(T) ⊆ {𝔪} is AlgebraicGeometry.FormalSpace.preimageSubsetClosedPoint_of_comp_eq.

public theorem existsUnique_algebraization_of_adic_into_completion
    {R : Type u} [CommRing R] [TopologicalSpace R]
    (hR : IsNoetherianCompleteLocalRing R)
    (D : QuotientSystem B S hS R)
    (hD₁ : ∀ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      ∃ n : ℕ, (@IsLocalRing.maximalIdeal R _ hR.isLocal) ^ n ≤ J.1)
    (hD : ∀ n : ℕ, ∃ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      J.1 ≤ (@IsLocalRing.maximalIdeal R _ hR.isLocal) ^ n)
    (hRS : B.Contains (Spec (.of R))) (q : Spec (.of R) ⟶ S)
    (hq : ∀ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk J.1)) ≫ q = D.overS J)
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (T : Set (Space.points B S hS X))
    (hT : @IsClosed _ (Space.pointTopology B S hS X) T)
    (_hTqc : letI : TopologicalSpace (Space.points B S hS X) := Space.pointTopology B S hS X
      Space.IsQuasiCompact B S hS
        ((Space.openSubspacesOrderIso B S hS X hX).symm ⟨Tᶜ, hT.isOpen_compl⟩).1.ι)
    (P : formalSpectrum D ⟶ Space.completionSheaf B S hS X T)
    (hPadic : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS P.hom) :
    ∃! g : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj
        ((BigAffineFppf.inclusion B S hS).obj (specOver hRS q)) ⟶ upliftedSheaf X hX,
      formalSpectrumToSpec D hRS q hq ≫ g = P ≫ completionToUpliftedSheaf X hX T ∧
        PreimageEqClosedPoint hR T hRS q
          (Sheaf.sectionEquiv (BigFppfOver.topology B S hS) g).down

AlgebraicGeometry.FormalSpace.adicCompletionHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicMapsIntoCompletionEquiv.lean, line 628. The attribute's comment: “The bijection between adic morphisms Spf R ⟶ X_{/T} and morphisms g : Spec R ⟶ X with g⁻¹(T) = {𝔪}.”.

Stacks 0GBU. Let S be a scheme, X an algebraic space over S and T a closed set of points of X whose complementary open subspace has quasi-compact inclusion into X. Let R be a Noetherian complete local S-algebra whose spectrum lies in the site, equipped with a quotient system whose weak ideals of definition are cofinal among the powers of the maximal ideal 𝔪. Then the adic morphisms p : Spf R ⟶ X_{/T} correspond bijectively to the morphisms g : Spec R ⟶ X with g⁻¹(T) = {𝔪}.

The bijection sends p to the unique g restricting on Spf R to p followed by X_{/T} ⟶ X (AlgebraicGeometry.FormalSpace.existsUnique_algebraization_of_adic_into_completion), and its inverse sends g to AlgebraicGeometry.FormalSpace.adicOfAlgebraization; the correspondence is characterised by AlgebraicGeometry.FormalSpace.adicCompletionHomEquiv_apply_eq_iff.

def adicCompletionHomEquiv
    {R : Type u} [CommRing R] [TopologicalSpace R]
    (hR : IsNoetherianCompleteLocalRing R)
    (D : QuotientSystem B S hS R)
    (hD₁ : ∀ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      ∃ n : ℕ, (@IsLocalRing.maximalIdeal R _ hR.isLocal) ^ n ≤ J.1)
    (hD : ∀ n : ℕ, ∃ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      J.1 ≤ (@IsLocalRing.maximalIdeal R _ hR.isLocal) ^ n)
    (hRS : B.Contains (Spec (.of R))) (q : Spec (.of R) ⟶ S)
    (hq : ∀ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk J.1)) ≫ q = D.overS J)
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (T : Set (Space.points B S hS X))
    (hT : @IsClosed _ (Space.pointTopology B S hS X) T)
    (hTqc : letI : TopologicalSpace (Space.points B S hS X) := Space.pointTopology B S hS X
      Space.IsQuasiCompact B S hS
        ((Space.openSubspacesOrderIso B S hS X hX).symm ⟨Tᶜ, hT.isOpen_compl⟩).1.ι) :
    { p : formalSpectrum D ⟶ Space.completionSheaf B S hS X T //
        Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS p.hom } ≃
      { g : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj
          ((BigAffineFppf.inclusion B S hS).obj (specOver hRS q)) ⟶ upliftedSheaf X hX //
        PreimageEqClosedPoint hR T hRS q
          (Sheaf.sectionEquiv (BigFppfOver.topology B S hS) g).down }

AlgebraicGeometry.FormalSpace.adicCompletionHomEquiv_apply_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AdicMapsIntoCompletionEquiv.lean, line 703. The attribute's comment: “The bijection is the correspondence: p ↦ g exactly when g restricts on Spf R to p followed by X_{/T} ⟶ X.”.

Stacks 0GBU, the correspondence. The bijection adicCompletionHomEquiv sends an adic p : Spf R ⟶ X_{/T} to g : Spec R ⟶ X with g⁻¹(T) = {𝔪} exactly when g restricts on Spf R to p followed by X_{/T} ⟶ X.

theorem adicCompletionHomEquiv_apply_eq_iff
    {R : Type u} [CommRing R] [TopologicalSpace R]
    (hR : IsNoetherianCompleteLocalRing R)
    (D : QuotientSystem B S hS R)
    (hD₁ : ∀ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      ∃ n : ℕ, (@IsLocalRing.maximalIdeal R _ hR.isLocal) ^ n ≤ J.1)
    (hD : ∀ n : ℕ, ∃ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      J.1 ≤ (@IsLocalRing.maximalIdeal R _ hR.isLocal) ^ n)
    (hRS : B.Contains (Spec (.of R))) (q : Spec (.of R) ⟶ S)
    (hq : ∀ J : { I : Ideal R // TopologicalRing.IsWeakIdealOfDefinition I },
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk J.1)) ≫ q = D.overS J)
    (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B S hS X)
    (T : Set (Space.points B S hS X))
    (hT : @IsClosed _ (Space.pointTopology B S hS X) T)
    (hTqc : letI : TopologicalSpace (Space.points B S hS X) := Space.pointTopology B S hS X
      Space.IsQuasiCompact B S hS
        ((Space.openSubspacesOrderIso B S hS X hX).symm ⟨Tᶜ, hT.isOpen_compl⟩).1.ι)
    (p : { p : formalSpectrum D ⟶ Space.completionSheaf B S hS X T //
        Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS p.hom })
    (g : { g : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj
          ((BigAffineFppf.inclusion B S hS).obj (specOver hRS q)) ⟶ upliftedSheaf X hX //
        PreimageEqClosedPoint hR T hRS q
          (Sheaf.sectionEquiv (BigFppfOver.topology B S hS) g).down }) :
    adicCompletionHomEquiv hR D hD₁ hD hRS q hq X hX T hT hTqc p = g ↔
      formalSpectrumToSpec D hRS q hq ≫ g.1 = p.1 ≫ completionToUpliftedSheaf X hX T

Sources

• Section 87.33, Tag 0AQE
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.FormalSpace.exists_formalSpectrumToSpec · AlgebraicGeometry.FormalSpace.bijective_map_into_affine · AlgebraicGeometry.FormalSpace.existsUnique_equiv_specHom_formalSpectrumHom · AlgebraicGeometry.FormalSpace.injective_map_into_algebraicSpace · AlgebraicGeometry.FormalSpace.surjective_map_into_algebraicSpace · AlgebraicGeometry.FormalSpace.bijective_map_into_algebraicSpace · AlgebraicGeometry.FormalSpace.existsUnique_algebraization_of_adic_into_completion · AlgebraicGeometry.FormalSpace.adicCompletionHomEquiv

Section87.34 The small étale site of a formal algebraic space#

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

Tag 0DEA, a definition

Tag 0DEA in the Stacks Project.

AlgebraicGeometry.FormalSpace.Reduction.SmallEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSite.lean, line 224. The attribute's comment: “(1) the small étale site, as a category; read against a given reduction, which Stacks 0AIN supplies”.

The small étale site X_étale of a formal algebraic space X with reduction X_red, as a category: the small étale site X_{red, étale} of the reduction, in the sense of Stacks 03ED, whose objects are the étale scheme charts of X_red.

abbrev SmallEtale (R : Reduction B S hS X)

AlgebraicGeometry.FormalSpace.Reduction.smallEtaleTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSite.lean, line 230. The attribute's comment: “(1) the topology of the small étale site; read against a given reduction, which Stacks 0AIN supplies”.

The topology of the small étale site of X: that of X_{red, étale}.

abbrev smallEtaleTopology (R : Reduction B S hS X) : GrothendieckTopology R.SmallEtale

AlgebraicGeometry.FormalSpace.Reduction.SpacesEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSite.lean, line 239. The attribute's comment: “(2) the spaces-étale site, as a category; read against a given reduction, which Stacks 0AIN supplies”.

The site X_{spaces, étale} of a formal algebraic space X with reduction X_red, as a category: the spaces-étale site X_{red, spaces, étale} of the reduction, in the sense of Stacks 03G0, whose objects are the algebraic spaces étale over X_red.

abbrev SpacesEtale (R : Reduction B S hS X)

AlgebraicGeometry.FormalSpace.Reduction.spacesEtaleTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSite.lean, line 245. The attribute's comment: “(2) the topology of the spaces-étale site; read against a given reduction, which Stacks 0AIN supplies”.

The topology of X_{spaces, étale}: that of X_{red, spaces, étale}.

abbrev spacesEtaleTopology (R : Reduction B S hS X) : GrothendieckTopology R.SpacesEtale

AlgebraicGeometry.FormalSpace.Reduction.AffineEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSite.lean, line 253. The attribute's comment: “(3) the affine étale site, as a category; read against a given reduction, which Stacks 0AIN supplies”.

The site X_{affine, étale} of a formal algebraic space X with reduction X_red, as a category: the affine étale site X_{red, affine, étale} of the reduction, whose objects are the étale charts of X_red with affine source.

abbrev AffineEtale (R : Reduction B S hS X)

AlgebraicGeometry.FormalSpace.Reduction.affineEtaleTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSite.lean, line 259. The attribute's comment: “(3) the topology of the affine étale site; read against a given reduction, which Stacks 0AIN supplies”.

The topology of X_{affine, étale}: that of X_{red, affine, étale}.

abbrev affineEtaleTopology (R : Reduction B S hS X) : GrothendieckTopology R.AffineEtale

AlgebraicGeometry.FormalSpace.canonicalSmallEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonical.lean, line 158. The attribute's comment: “(1) the small étale site, as a category”.

Stacks 0DEA, part (1). The small étale site X_étale of a formal algebraic space X over S, as a category: the small étale site X_{red, étale} of its reduction, in the sense of Stacks 03ED, whose objects are the étale scheme charts of X_red.

abbrev canonicalSmallEtale (hX : IsFormalAlgebraicSpace B S hS X)

AlgebraicGeometry.FormalSpace.canonicalSmallEtaleTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonical.lean, line 164. The attribute's comment: “(1) the topology of the small étale site”.

Stacks 0DEA, part (1). The topology of the small étale site of X: that of X_{red, étale}.

noncomputable abbrev canonicalSmallEtaleTopology (hX : IsFormalAlgebraicSpace B S hS X) :
    GrothendieckTopology (canonicalSmallEtale hX)

AlgebraicGeometry.FormalSpace.canonicalSpacesEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonical.lean, line 172. The attribute's comment: “(2) the spaces-étale site, as a category”.

Stacks 0DEA, part (2). The site X_{spaces, étale} of a formal algebraic space X over S, as a category: the spaces-étale site X_{red, spaces, étale} of its reduction, in the sense of Stacks 03G0, whose objects are the algebraic spaces étale over X_red.

abbrev canonicalSpacesEtale (hX : IsFormalAlgebraicSpace B S hS X)

AlgebraicGeometry.FormalSpace.canonicalSpacesEtaleTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonical.lean, line 178. The attribute's comment: “(2) the topology of the spaces-étale site”.

Stacks 0DEA, part (2). The topology of X_{spaces, étale}: that of X_{red, spaces, étale}.

noncomputable abbrev canonicalSpacesEtaleTopology (hX : IsFormalAlgebraicSpace B S hS X) :
    GrothendieckTopology (canonicalSpacesEtale hX)

AlgebraicGeometry.FormalSpace.canonicalAffineEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonical.lean, line 186. The attribute's comment: “(3) the affine étale site, as a category”.

Stacks 0DEA, part (3). The site X_{affine, étale} of a formal algebraic space X over S, as a category: the affine étale site X_{red, affine, étale} of its reduction, whose objects are the étale charts of X_red with affine source.

abbrev canonicalAffineEtale (hX : IsFormalAlgebraicSpace B S hS X)

AlgebraicGeometry.FormalSpace.canonicalAffineEtaleTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonical.lean, line 192. The attribute's comment: “(3) the topology of the affine étale site”.

Stacks 0DEA, part (3). The topology of X_{affine, étale}: that of X_{red, affine, étale}.

noncomputable abbrev canonicalAffineEtaleTopology (hX : IsFormalAlgebraicSpace B S hS X) :
    GrothendieckTopology (canonicalAffineEtale hX)

AlgebraicGeometry.FormalSpace.SmallEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteChosenReduction.lean, line 74. The attribute's comment: “(1) the small étale site, as a category”.

Stacks 0DEA, part (1). The small étale site X_étale of a formal algebraic space X over S, as a category: the small étale site X_{red, étale} of the reduction, in the sense of Stacks 03ED, whose objects are the étale scheme charts of X_red.

abbrev SmallEtale (X : FppfSheaf B S hS) (hX : IsFormalAlgebraicSpace B S hS X)

AlgebraicGeometry.FormalSpace.smallEtaleTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteChosenReduction.lean, line 80. The attribute's comment: “(1) the topology of the small étale site”.

Stacks 0DEA, part (1). The topology of the small étale site of X: that of X_{red, étale}.

noncomputable abbrev smallEtaleTopology (X : FppfSheaf B S hS)
    (hX : IsFormalAlgebraicSpace B S hS X) :
    GrothendieckTopology (SmallEtale B S hS X hX)

AlgebraicGeometry.FormalSpace.SpacesEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteChosenReduction.lean, line 89. The attribute's comment: “(2) the spaces-étale site, as a category”.

Stacks 0DEA, part (2). The site X_{spaces, étale} of a formal algebraic space X over S, as a category: the spaces-étale site X_{red, spaces, étale} of the reduction, in the sense of Stacks 03G0, whose objects are the algebraic spaces étale over X_red.

abbrev SpacesEtale (X : FppfSheaf B S hS) (hX : IsFormalAlgebraicSpace B S hS X)

AlgebraicGeometry.FormalSpace.spacesEtaleTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteChosenReduction.lean, line 95. The attribute's comment: “(2) the topology of the spaces-étale site”.

Stacks 0DEA, part (2). The topology of X_{spaces, étale}: that of X_{red, spaces, étale}.

noncomputable abbrev spacesEtaleTopology (X : FppfSheaf B S hS)
    (hX : IsFormalAlgebraicSpace B S hS X) :
    GrothendieckTopology (SpacesEtale B S hS X hX)

AlgebraicGeometry.FormalSpace.AffineEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteChosenReduction.lean, line 106. The attribute's comment: “(3) the affine étale site, as a category”.

Stacks 0DEA, part (3). The site X_{affine, étale} of a formal algebraic space X over S, as a category: the affine étale site X_{red, affine, étale} of the reduction, whose objects are the étale charts of X_red with affine source. The site named by Properties of Spaces Lemma 04JS is AlgebraicGeometry.Space.AffineEtale, which in this library carries the tag Stacks 0H01.

abbrev AffineEtale (X : FppfSheaf B S hS) (hX : IsFormalAlgebraicSpace B S hS X)

AlgebraicGeometry.FormalSpace.affineEtaleTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteChosenReduction.lean, line 112. The attribute's comment: “(3) the topology of the affine étale site”.

Stacks 0DEA, part (3). The topology of X_{affine, étale}: that of X_{red, affine, étale}.

noncomputable abbrev affineEtaleTopology (X : FppfSheaf B S hS)
    (hX : IsFormalAlgebraicSpace B S hS X) :
    GrothendieckTopology (AffineEtale B S hS X hX)

Tag 0DEB, an equation

Tag 0DEB in the Stacks Project.

AlgebraicGeometry.FormalSpace.canonicalSmallEtaleToposEquivSpacesEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleTopos.lean, line 134. The attribute's comment: “Sh(X_étale) = Sh(X_spaces,étale), for sheaves in any category with the limits of the Comparison Lemma”.

Stacks 0DEB, Sh(X_étale) = Sh(X_{spaces, étale}). For a formal algebraic space X over S, the topos of the small étale site X_étale of Stacks 0DEA, part (1), is equivalent to that of the site X_{spaces, étale} of Stacks 0DEA, part (2): restriction along the inclusion of étale scheme charts of X_red among algebraic spaces étale over X_red is an equivalence. This holds for sheaves valued in any category A with the limits the Comparison Lemma asks for, which includes sheaves of sets; see AlgebraicGeometry.FormalSpace.canonicalSmallEtaleToposEquivSpacesEtaleSets.

noncomputable def canonicalSmallEtaleToposEquivSpacesEtale (A : Type w) [Category.{w'} A]
    [∀ Y, HasLimitsOfShape
      (StructuredArrow Y (canonicalReduction hX).smallEtaleToSpacesEtale.op) A] :
    Sheaf (canonicalSmallEtaleTopology hX) A ≌ Sheaf (canonicalSpacesEtaleTopology hX) A

AlgebraicGeometry.FormalSpace.canonicalSmallEtaleToposEquivAffineEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleTopos.lean, line 148. The attribute's comment: “Sh(X_étale) = Sh(X_affine,étale), for sheaves in any category with the limits of the Comparison Lemma”.

Stacks 0DEB, Sh(X_étale) = Sh(X_{affine, étale}). For a formal algebraic space X over S, the topos of the small étale site X_étale of Stacks 0DEA, part (1), is equivalent to that of the site X_{affine, étale} of Stacks 0DEA, part (3): restriction along the inclusion of the étale charts of X_red with affine source is an equivalence. This holds for sheaves valued in any category A with the limits the Comparison Lemma asks for, which includes sheaves of sets; see AlgebraicGeometry.FormalSpace.canonicalSmallEtaleToposEquivAffineEtaleSets.

noncomputable def canonicalSmallEtaleToposEquivAffineEtale (A : Type w) [Category.{w'} A]
    [∀ Y, HasLimitsOfShape
      (StructuredArrow Y (canonicalReduction hX).affineEtaleInclusion.op) A] :
    Sheaf (canonicalSmallEtaleTopology hX) A ≌ Sheaf (canonicalAffineEtaleTopology hX) A

AlgebraicGeometry.FormalSpace.canonicalSmallEtaleToposEquivSpacesEtaleSets, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleTopos.lean, line 179. The attribute's comment: “Sh(X_étale) = Sh(X_spaces,étale), for sheaves of sets”.

Stacks 0DEB, Sh(X_étale) = Sh(X_{spaces, étale}), for sheaves of sets. These are sets in Type (u + 1), the universe of the small étale topoi of Stacks 0DEC, part (3), which pass through this identification.

noncomputable def canonicalSmallEtaleToposEquivSpacesEtaleSets :
    Sheaf (canonicalSmallEtaleTopology hX) (Type (u + 1)) ≌
      Sheaf (canonicalSpacesEtaleTopology hX) (Type (u + 1))

AlgebraicGeometry.FormalSpace.canonicalSmallEtaleToposEquivAffineEtaleSets, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleTopos.lean, line 188. The attribute's comment: “Sh(X_étale) = Sh(X_affine,étale), for sheaves of sets”.

Stacks 0DEB, Sh(X_étale) = Sh(X_{affine, étale}), for sheaves of sets. These are sets in Type (u + 1), the universe of the small étale topoi of Stacks 0DEC, part (3).

noncomputable def canonicalSmallEtaleToposEquivAffineEtaleSets :
    Sheaf (canonicalSmallEtaleTopology hX) (Type (u + 1)) ≌
      Sheaf (canonicalAffineEtaleTopology hX) (Type (u + 1))

Tag 0DEC, a lemma

Tag 0DEC in the Stacks Project.

AlgebraicGeometry.FormalSpace.Reduction.spacesBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSite.lean, line 308. The attribute's comment: “(1) the base-change functor Y_spaces,étale ⟶ X_spaces,étale; read against given reductions, which Stacks 0AIN supplies”.

The functor Y_{spaces, étale} ⟶ X_{spaces, étale} induced by a morphism f : X ⟶ Y of formal algebraic spaces: base change along the induced morphism of reductions, together with its cartesian projection, by Stacks 03G2, part (1).

noncomputable def spacesBaseChange (RX : Reduction B S hS X) (RY : Reduction B S hS Y)
    (f : X ⟶ Y) : Space.SpacesBaseChange B S hS (RX.map RY f)

AlgebraicGeometry.FormalSpace.Reduction.isContinuous_spacesBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSite.lean, line 316. The attribute's comment: “(1) continuity of the functor; read against given reductions, which Stacks 0AIN supplies”.

The functor Y_{spaces, étale} ⟶ X_{spaces, étale} is continuous.

theorem isContinuous_spacesBaseChange (RX : Reduction B S hS X) (RY : Reduction B S hS Y)
    (f : X ⟶ Y) :
    (RX.spacesBaseChange RY f).functor.IsContinuous RY.spacesEtaleTopology
      RX.spacesEtaleTopology

AlgebraicGeometry.FormalSpace.Reduction.spacesBaseChange_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSite.lean, line 327. The attribute's comment: “(1) the induced morphism of sites f_spaces,étale; read against given reductions, which Stacks 0AIN supplies”.

The continuous functor Y_{spaces, étale} ⟶ X_{spaces, étale} induces a morphism of sites f_{spaces, étale} : X_{spaces, étale} ⟶ Y_{spaces, étale}, in the sense of Stacks 00X1.

theorem spacesBaseChange_isMorphismOfSites (RX : Reduction B S hS X)
    (RY : Reduction B S hS Y) (f : X ⟶ Y) :
    (RX.spacesBaseChange RY f).functor.IsMorphismOfSites RY.spacesEtaleTopology
      RX.spacesEtaleTopology

AlgebraicGeometry.FormalSpace.Reduction.spacesBaseChangeComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSite.lean, line 339. The attribute's comment: “(2) compatibility with composition, as a canonical isomorphism of the underlying functors; read against given reductions, which Stacks 0AIN supplies”.

The rule f ↦ f_{spaces, étale} is compatible with composition: the underlying functor of (f ≫ g)_{spaces, étale} is canonically isomorphic to the composite of those of g_{spaces, étale} and f_{spaces, étale}, which is the composition of morphisms of sites of Stacks 03CC.

noncomputable def spacesBaseChangeComp (RX : Reduction B S hS X) (RY : Reduction B S hS Y)
    (RZ : Reduction B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z) :
    (RY.spacesBaseChange RZ g).functor ⋙ (RX.spacesBaseChange RY f).functor ≅
      (RX.spacesBaseChange RZ (f ≫ g)).functor

AlgebraicGeometry.FormalSpace.Reduction.spacesBaseChangeComp_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSite.lean, line 350. The attribute's comment: “(2) the composition isomorphism is compatible with the cartesian projections, which pins it down; read against given reductions, which Stacks 0AIN supplies”.

The composition isomorphism is compatible with the cartesian projections to the original object of Z_{spaces, étale}.

theorem spacesBaseChangeComp_projection (RX : Reduction B S hS X) (RY : Reduction B S hS Y)
    (RZ : Reduction B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z) (V : RZ.SpacesEtale) :
    ((RX.spacesBaseChangeComp RY RZ f g).hom.app V).hom.left ≫
        (RX.spacesBaseChange RZ (f ≫ g)).projection.app V =
      (RX.spacesBaseChange RY f).projection.app
          ((RY.spacesBaseChange RZ g).functor.obj V) ≫
        (RY.spacesBaseChange RZ g).projection.app V

AlgebraicGeometry.FormalSpace.Reduction.smallToposMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSite.lean, line 366. The attribute's comment: “(3) the morphism of small étale topoi f_small, through the identification (0DEB); read against given reductions, which Stacks 0AIN supplies”.

The morphism of topoi f_small : Sh(X_étale) ⟶ Sh(Y_étale) associated to f_{spaces, étale}, via the identification (0DEB) of the small étale topos with the spaces-étale topos. It is the morphism of small étale topoi of Stacks 03G2, part (3), at the induced morphism of reductions.

noncomputable def smallToposMorphism (RX : Reduction B S hS X) (RY : Reduction B S hS Y)
    (f : X ⟶ Y) :
    MorphismOfTopoi (Sheaf RX.smallEtaleTopology (Type (u + 1)))
      (Sheaf RY.smallEtaleTopology (Type (u + 1)))

AlgebraicGeometry.FormalSpace.Reduction.smallToposMorphismComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSite.lean, line 377. The attribute's comment: “(3) compatibility with composition of the morphisms of small étale topoi, on direct images; read against given reductions, which Stacks 0AIN supplies”.

The construction of f_small is compatible with composition: the direct image of the composite of g_small and f_small is canonically isomorphic to the direct image of (f ≫ g)_small.

noncomputable def smallToposMorphismComp (RX : Reduction B S hS X) (RY : Reduction B S hS Y)
    (RZ : Reduction B S hS Z) (f : X ⟶ Y) (g : Y ⟶ Z) :
    (MorphismOfTopoi.comp (RY.smallToposMorphism RZ g)
        (RX.smallToposMorphism RY f)).pushforward ≅
      (RX.smallToposMorphism RZ (f ≫ g)).pushforward

AlgebraicGeometry.FormalSpace.canonicalSpacesBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonical.lean, line 202. The attribute's comment: “(1) the base-change functor Y_spaces,étale ⟶ X_spaces,étale”.

Stacks 0DEC, part (1). The functor Y_{spaces, étale} ⟶ X_{spaces, étale} induced by a morphism f : X ⟶ Y of formal algebraic spaces: base change along the induced morphism of reductions, together with its cartesian projection, by Stacks 03G2, part (1).

noncomputable def canonicalSpacesBaseChange (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    Space.SpacesBaseChange B S hS ((canonicalReduction hX).map (canonicalReduction hY) f)

AlgebraicGeometry.FormalSpace.isContinuous_canonicalSpacesBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonical.lean, line 210. The attribute's comment: “(1) continuity of the functor”.

Stacks 0DEC, part (1). The functor Y_{spaces, étale} ⟶ X_{spaces, étale} is continuous.

theorem isContinuous_canonicalSpacesBaseChange (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    (canonicalSpacesBaseChange hX hY f).functor.IsContinuous
      (canonicalSpacesEtaleTopology hY) (canonicalSpacesEtaleTopology hX)

AlgebraicGeometry.FormalSpace.canonicalSpacesBaseChange_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonical.lean, line 220. The attribute's comment: “(1) the induced morphism of sites f_spaces,étale”.

Stacks 0DEC, part (1). The continuous functor Y_{spaces, étale} ⟶ X_{spaces, étale} induces a morphism of sites f_{spaces, étale} : X_{spaces, étale} ⟶ Y_{spaces, étale}, in the sense of Stacks 00X1.

theorem canonicalSpacesBaseChange_isMorphismOfSites (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    (canonicalSpacesBaseChange hX hY f).functor.IsMorphismOfSites
      (canonicalSpacesEtaleTopology hY) (canonicalSpacesEtaleTopology hX)

AlgebraicGeometry.FormalSpace.canonicalSpacesBaseChangeComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonical.lean, line 232. The attribute's comment: “(2) compatibility with composition, as a canonical isomorphism of the underlying functors”.

Stacks 0DEC, part (2). The rule f ↦ f_{spaces, étale} is compatible with composition: the underlying functor of (f ≫ g)_{spaces, étale} is canonically isomorphic to the composite of those of g_{spaces, étale} and f_{spaces, étale}, which is the composition of morphisms of sites of Stacks 03CC.

noncomputable def canonicalSpacesBaseChangeComp (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (hZ : IsFormalAlgebraicSpace B S hS Z) (f : X ⟶ Y)
    (g : Y ⟶ Z) :
    (canonicalSpacesBaseChange hY hZ g).functor ⋙ (canonicalSpacesBaseChange hX hY f).functor ≅
      (canonicalSpacesBaseChange hX hZ (f ≫ g)).functor

AlgebraicGeometry.FormalSpace.canonicalSpacesBaseChangeComp_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonical.lean, line 244. The attribute's comment: “(2) the composition isomorphism is compatible with the cartesian projections, which pins it down”.

Stacks 0DEC, part (2). The composition isomorphism is compatible with the cartesian projections to the original object of Z_{spaces, étale}, which pins it down.

theorem canonicalSpacesBaseChangeComp_projection (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (hZ : IsFormalAlgebraicSpace B S hS Z) (f : X ⟶ Y)
    (g : Y ⟶ Z) (V : canonicalSpacesEtale hZ) :
    ((canonicalSpacesBaseChangeComp hX hY hZ f g).hom.app V).hom.left ≫
        (canonicalSpacesBaseChange hX hZ (f ≫ g)).projection.app V =
      (canonicalSpacesBaseChange hX hY f).projection.app
          ((canonicalSpacesBaseChange hY hZ g).functor.obj V) ≫
        (canonicalSpacesBaseChange hY hZ g).projection.app V

AlgebraicGeometry.FormalSpace.canonicalSmallToposMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonical.lean, line 261. The attribute's comment: “(3) the morphism of small étale topoi f_small, through the identification (0DEB)”.

Stacks 0DEC, part (3). The morphism of topoi f_small : Sh(X_étale) ⟶ Sh(Y_étale) associated to f_{spaces, étale}, via the identification (0DEB) of the small étale topos with the spaces-étale topos. It is the morphism of small étale topoi of Stacks 03G2, part (3), at the induced morphism of reductions.

noncomputable def canonicalSmallToposMorphism (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    MorphismOfTopoi (Sheaf (canonicalSmallEtaleTopology hX) (Type (u + 1)))
      (Sheaf (canonicalSmallEtaleTopology hY) (Type (u + 1)))

AlgebraicGeometry.FormalSpace.canonicalSmallToposMorphismComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonical.lean, line 272. The attribute's comment: “(3) compatibility with composition of the morphisms of small étale topoi, on direct images”.

Stacks 0DEC, part (3). The construction of f_small is compatible with composition: the direct image of the composite of g_small and f_small is canonically isomorphic to the direct image of (f ≫ g)_small.

noncomputable def canonicalSmallToposMorphismComp (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (hZ : IsFormalAlgebraicSpace B S hS Z) (f : X ⟶ Y)
    (g : Y ⟶ Z) :
    (MorphismOfTopoi.comp (canonicalSmallToposMorphism hY hZ g)
        (canonicalSmallToposMorphism hX hY f)).pushforward ≅
      (canonicalSmallToposMorphism hX hZ (f ≫ g)).pushforward

AlgebraicGeometry.FormalSpace.spacesBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteChosenReduction.lean, line 125. The attribute's comment: “(1) the base-change functor Y_spaces,étale ⟶ X_spaces,étale”.

Stacks 0DEC, part (1). The functor Y_{spaces, étale} ⟶ X_{spaces, étale} induced by a morphism f : X ⟶ Y of formal algebraic spaces: base change along the induced morphism of reductions, together with its cartesian projection, by Stacks 03G2, part (1).

noncomputable def spacesBaseChange (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    Space.SpacesBaseChange B S hS
      ((reduction B S hS X hX).map (reduction B S hS Y hY) f)

AlgebraicGeometry.FormalSpace.isContinuous_spacesBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteChosenReduction.lean, line 134. The attribute's comment: “(1) continuity of the functor”.

Stacks 0DEC, part (1). The functor Y_{spaces, étale} ⟶ X_{spaces, étale} is continuous.

theorem isContinuous_spacesBaseChange (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    (spacesBaseChange B S hS hX hY f).functor.IsContinuous
      (spacesEtaleTopology B S hS Y hY) (spacesEtaleTopology B S hS X hX)

AlgebraicGeometry.FormalSpace.spacesBaseChange_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteChosenReduction.lean, line 144. The attribute's comment: “(1) the induced morphism of sites f_spaces,étale”.

Stacks 0DEC, part (1). The continuous functor Y_{spaces, étale} ⟶ X_{spaces, étale} induces a morphism of sites f_{spaces, étale} : X_{spaces, étale} ⟶ Y_{spaces, étale}, in the sense of Stacks 00X1.

theorem spacesBaseChange_isMorphismOfSites (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    (spacesBaseChange B S hS hX hY f).functor.IsMorphismOfSites
      (spacesEtaleTopology B S hS Y hY) (spacesEtaleTopology B S hS X hX)

AlgebraicGeometry.FormalSpace.spacesBaseChangeComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteChosenReduction.lean, line 156. The attribute's comment: “(2) compatibility with composition, as a canonical isomorphism of the underlying functors”.

Stacks 0DEC, part (2). The rule f ↦ f_{spaces, étale} is compatible with composition: the underlying functor of (f ≫ g)_{spaces, étale} is canonically isomorphic to the composite of those of g_{spaces, étale} and f_{spaces, étale}, which is the composition of morphisms of sites of Stacks 03CC.

noncomputable def spacesBaseChangeComp (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (hZ : IsFormalAlgebraicSpace B S hS Z) (f : X ⟶ Y)
    (g : Y ⟶ Z) :
    (spacesBaseChange B S hS hY hZ g).functor ⋙ (spacesBaseChange B S hS hX hY f).functor ≅
      (spacesBaseChange B S hS hX hZ (f ≫ g)).functor

AlgebraicGeometry.FormalSpace.spacesBaseChangeComp_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteChosenReduction.lean, line 168. The attribute's comment: “(2) the composition isomorphism is compatible with the cartesian projections, which pins it down”.

Stacks 0DEC, part (2). The composition isomorphism is compatible with the cartesian projections to the original object of Z_{spaces, étale}, which pins it down.

theorem spacesBaseChangeComp_projection (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (hZ : IsFormalAlgebraicSpace B S hS Z) (f : X ⟶ Y)
    (g : Y ⟶ Z) (V : SpacesEtale B S hS Z hZ) :
    ((spacesBaseChangeComp B S hS hX hY hZ f g).hom.app V).hom.left ≫
        (spacesBaseChange B S hS hX hZ (f ≫ g)).projection.app V =
      (spacesBaseChange B S hS hX hY f).projection.app
          ((spacesBaseChange B S hS hY hZ g).functor.obj V) ≫
        (spacesBaseChange B S hS hY hZ g).projection.app V

AlgebraicGeometry.FormalSpace.smallToposMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteChosenReduction.lean, line 185. The attribute's comment: “(3) the morphism of small étale topoi f_small, through the identification (0DEB)”.

Stacks 0DEC, part (3). The morphism of topoi f_small : Sh(X_étale) ⟶ Sh(Y_étale) associated to f_{spaces, étale}, via the identification (0DEB) of the small étale topos with the spaces-étale topos. It is the morphism of small étale topoi of Stacks 03G2, part (3), at the induced morphism of reductions.

noncomputable def smallToposMorphism (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    MorphismOfTopoi (Sheaf (smallEtaleTopology B S hS X hX) (Type (u + 1)))
      (Sheaf (smallEtaleTopology B S hS Y hY) (Type (u + 1)))

AlgebraicGeometry.FormalSpace.smallToposMorphismComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteChosenReduction.lean, line 196. The attribute's comment: “(3) compatibility with composition of the morphisms of small étale topoi, on direct images”.

Stacks 0DEC, part (3). The construction of f_small is compatible with composition: the direct image of the composite of g_small and f_small is canonically isomorphic to the direct image of (f ≫ g)_small.

noncomputable def smallToposMorphismComp (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (hZ : IsFormalAlgebraicSpace B S hS Z) (f : X ⟶ Y)
    (g : Y ⟶ Z) :
    (MorphismOfTopoi.comp (smallToposMorphism B S hS hY hZ g)
        (smallToposMorphism B S hS hX hY f)).pushforward ≅
      (smallToposMorphism B S hS hX hZ (f ≫ g)).pushforward

Tag 0DED, a lemma

Tag 0DED in the Stacks Project.

AlgebraicGeometry.FormalSpace.isEtale_canonicalReductionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonicalReduction.lean, line 83. The attribute's comment: “étaleness of the induced morphism of reductions, which is the content of the proof”.

Stacks 0DED, the content of the proof. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S which is representable by algebraic spaces and étale. Then the induced morphism of reductions X_red ⟶ Y_red is an étale morphism of algebraic spaces over S.

theorem isEtale_canonicalReductionMap (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (het : Space.HasPropertyULift.{u + 1} B S hS
      (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) f.hom hrep) :
    Space.IsEtale B S hS ((canonicalReduction hX).map (canonicalReduction hY) f).hom

AlgebraicGeometry.FormalSpace.canonicalSmallEtalePostcomp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonicalReduction.lean, line 96. The attribute's comment: “the functor j : X_étale ⟶ Y_étale”.

Stacks 0DED. The functor j : X_étale ⟶ Y_étale attached to a morphism f : X ⟶ Y of formal algebraic spaces over S which is representable by algebraic spaces and étale: postcomposition of an étale scheme chart of X_red with the induced étale morphism of reductions, which is the functor of Stacks 03LP at that morphism.

noncomputable def canonicalSmallEtalePostcomp (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (het : Space.HasPropertyULift.{u + 1} B S hS
      (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) f.hom hrep) :
    (canonicalReduction hX).SmallEtale ⥤ (canonicalReduction hY).SmallEtale

AlgebraicGeometry.FormalSpace.canonicalSmallEtalePostcomp_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonicalReduction.lean, line 107. The attribute's comment: “cocontinuity of j”.

Stacks 0DED. The functor j is cocontinuous: a covering sieve of jU in Y_étale pulls back to a covering sieve of U in X_étale.

instance canonicalSmallEtalePostcomp_isCocontinuous (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (het : Space.HasPropertyULift.{u + 1} B S hS
      (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) f.hom hrep) :
    (canonicalSmallEtalePostcomp hX hY f hrep het).IsCocontinuous
      (canonicalReduction hX).smallEtaleTopology (canonicalReduction hY).smallEtaleTopology

AlgebraicGeometry.FormalSpace.canonicalSmallEtalePostcomp_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonicalReduction.lean, line 119. The attribute's comment: “continuity of j, which is what makes Sites 00XR applicable”.

Stacks 0DED. The functor j is continuous as well, so Sites 00XR applies to it.

instance canonicalSmallEtalePostcomp_isContinuous (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (het : Space.HasPropertyULift.{u + 1} B S hS
      (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) f.hom hrep) :
    (canonicalSmallEtalePostcomp hX hY f hrep het).IsContinuous
      (canonicalReduction hX).smallEtaleTopology (canonicalReduction hY).smallEtaleTopology

AlgebraicGeometry.FormalSpace.canonicalSmallToposMorphism_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonicalReduction.lean, line 135. The attribute's comment: “f_small is the morphism of topoi that Sites 00XO attaches to j, identified on direct images”.

Stacks 0DED. The morphism of topoi f_small of Stacks 0DEC, part (3), is the morphism of topoi that Sites 00XO attaches to the cocontinuous functor j: its direct image is the direct image of j.

noncomputable def canonicalSmallToposMorphism_pushforwardIso
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (het : Space.HasPropertyULift.{u + 1} B S hS
      (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) f.hom hrep) :
    ((canonicalReduction hX).smallToposMorphism (canonicalReduction hY) f).pushforward ≅
      (canonicalSmallEtalePostcomp hX hY f hrep het).sheafPushforwardCocontinuous
        (Type (u + 1)) (canonicalReduction hX).smallEtaleTopology
        (canonicalReduction hY).smallEtaleTopology

AlgebraicGeometry.FormalSpace.canonicalSmallToposMorphism_inverseImageObjObjIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSiteCanonicalReduction.lean, line 152. The attribute's comment: “the formula on sections which Sites 00XR gives for j, continuous as well as cocontinuous”.

Stacks 0DED, the consequence of continuity of j recorded by Sites 00XR: the inverse image of f_small is restriction along j, so a section of f_small^{-1} G over an étale chart U of X_red is a section of G over the chart jU of Y_red.

noncomputable def canonicalSmallToposMorphism_inverseImageObjObjIso
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (het : Space.HasPropertyULift.{u + 1} B S hS
      (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) f.hom hrep)
    (G : Sheaf (canonicalReduction hY).smallEtaleTopology (Type (u + 1)))
    (U : (canonicalReduction hX).SmallEtale) :
    (((canonicalReduction hX).smallToposMorphism (canonicalReduction hY) f).inverseImage.obj
        G).obj.obj (Opposite.op U) ≅
      G.obj.obj (Opposite.op ((canonicalSmallEtalePostcomp hX hY f hrep het).obj U))

AlgebraicGeometry.FormalSpace.Reduction.isEtale_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSitePostcomposition.lean, line 196. The attribute's comment: “étaleness of the induced morphism of reductions, which is the content of the proof; read against given reductions, which Stacks 0AIN supplies”.

Stacks 0DED, the content of the proof. Let f : X ⟶ Y be a morphism of formal algebraic spaces over S which is representable by algebraic spaces and étale. Then the induced morphism of reductions X_red ⟶ Y_red is an étale morphism of algebraic spaces over S.

The fibre product X ×_Y Y_red is a reduction of X and every comparison morphism X_red ⟶ X ×_Y Y_red over X is an isomorphism — this is Stacks 0GB7, applicable because an étale morphism is smooth — so the morphism of reductions is, up to that isomorphism, the second projection of the fibre product. That projection is a base change of f, hence étale after every further base change along a scheme-valued point of Y_red; étaleness being étale local on the source and target, it satisfies the every-étale-chart condition of Stacks 03MJ, which descends to the value universe of the algebraic spaces.

theorem isEtale_map (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (RX : Reduction B S hS X) (RY : Reduction B S hS Y)
    (f : X ⟶ Y) (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (het : Space.HasPropertyULift.{u + 1} B S hS
      (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) f.hom hrep) :
    Space.IsEtale B S hS (RX.map RY f).hom

AlgebraicGeometry.FormalSpace.Reduction.smallEtalePostcomp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSitePostcomposition.lean, line 268. The attribute's comment: “the functor j : X_étale ⟶ Y_étale; read against given reductions, which Stacks 0AIN supplies”.

Stacks 0DED. The functor j : X_étale ⟶ Y_étale attached to a morphism f : X ⟶ Y of formal algebraic spaces over S which is representable by algebraic spaces and étale: postcomposition of an étale scheme chart of X_red with the induced étale morphism of reductions, which is the functor of Stacks 03LP at that morphism.

noncomputable def smallEtalePostcomp (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (RX : Reduction B S hS X)
    (RY : Reduction B S hS Y) (f : X ⟶ Y)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (het : Space.HasPropertyULift.{u + 1} B S hS
      (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) f.hom hrep) :
    RX.SmallEtale ⥤ RY.SmallEtale

AlgebraicGeometry.FormalSpace.Reduction.smallEtalePostcomp_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSitePostcomposition.lean, line 281. The attribute's comment: “cocontinuity of j; read against given reductions, which Stacks 0AIN supplies”.

Stacks 0DED. The functor j is cocontinuous: a covering sieve of jU in Y_étale pulls back to a covering sieve of U in X_étale.

instance smallEtalePostcomp_isCocontinuous (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (RX : Reduction B S hS X)
    (RY : Reduction B S hS Y) (f : X ⟶ Y)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (het : Space.HasPropertyULift.{u + 1} B S hS
      (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) f.hom hrep) :
    (smallEtalePostcomp hX hY RX RY f hrep het).IsCocontinuous RX.smallEtaleTopology
      RY.smallEtaleTopology

AlgebraicGeometry.FormalSpace.Reduction.smallEtalePostcomp_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSitePostcomposition.lean, line 295. The attribute's comment: “continuity of j, which is what makes Sites 00XR applicable; read against given reductions, which Stacks 0AIN supplies”.

Stacks 0DED. The functor j is continuous as well, so Sites 00XR applies to it.

instance smallEtalePostcomp_isContinuous (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (RX : Reduction B S hS X)
    (RY : Reduction B S hS Y) (f : X ⟶ Y)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (het : Space.HasPropertyULift.{u + 1} B S hS
      (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) f.hom hrep) :
    (smallEtalePostcomp hX hY RX RY f hrep het).IsContinuous RX.smallEtaleTopology
      RY.smallEtaleTopology

AlgebraicGeometry.FormalSpace.Reduction.smallToposMorphism_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSitePostcomposition.lean, line 312. The attribute's comment: “f_small is the morphism of topoi that Sites 00XO attaches to j, identified on direct images; read against given reductions, which Stacks 0AIN supplies”.

Stacks 0DED. The morphism of topoi f_small of Stacks 0DEC, part (3), is the morphism of topoi that Sites 00XO attaches to the cocontinuous functor j: its direct image is the direct image of j.

noncomputable def smallToposMorphism_pushforwardIso (hX : IsFormalAlgebraicSpace B S hS X)
    (hY : IsFormalAlgebraicSpace B S hS Y) (RX : Reduction B S hS X)
    (RY : Reduction B S hS Y) (f : X ⟶ Y)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (het : Space.HasPropertyULift.{u + 1} B S hS
      (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) f.hom hrep) :
    (RX.smallToposMorphism RY f).pushforward ≅
      (smallEtalePostcomp hX hY RX RY f hrep het).sheafPushforwardCocontinuous
        (Type (u + 1)) RX.smallEtaleTopology RY.smallEtaleTopology

AlgebraicGeometry.FormalSpace.Reduction.smallToposMorphism_inverseImageObjObjIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/EtaleSitePostcomposition.lean, line 329. The attribute's comment: “the formula on sections which Sites 00XR gives for j, continuous as well as cocontinuous; read against given reductions, which Stacks 0AIN supplies”.

Stacks 0DED, the consequence of continuity of j recorded by Sites 00XR: the inverse image of f_small is restriction along j, so a section of f_small^{-1} G over an étale chart U of X_red is a section of G over the chart jU of Y_red.

noncomputable def smallToposMorphism_inverseImageObjObjIso
    (hX : IsFormalAlgebraicSpace B S hS X) (hY : IsFormalAlgebraicSpace B S hS Y)
    (RX : Reduction B S hS X) (RY : Reduction B S hS Y) (f : X ⟶ Y)
    (hrep : Space.IsRepresentableByAlgebraicSpacesULift.{u + 1} B S hS f.hom)
    (het : Space.HasPropertyULift.{u + 1} B S hS
      (fun _ _ g ↦ Space.IsEtaleULift.{u + 1} B S hS g.hom) f.hom hrep)
    (G : Sheaf RY.smallEtaleTopology (Type (u + 1))) (U : RX.SmallEtale) :
    ((RX.smallToposMorphism RY f).inverseImage.obj G).obj.obj (Opposite.op U) ≅
      G.obj.obj (Opposite.op ((smallEtalePostcomp hX hY RX RY f hrep het).obj U))

Tag 0DEE, a lemma

Tag 0DEE in the Stacks Project.

AlgebraicGeometry.FormalSpace.AffineEtaleFormalCharts, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/EtaleSite.lean, line 130. The attribute's comment: “the category of the morphisms satisfying (1) and (2)”.

Stacks 0DEE, the category on the right-hand side: the morphisms φ : U ⟶ X of formal algebraic spaces with U an affine formal algebraic space and φ representable by algebraic spaces and étale, with the morphisms of fppf sheaves over X between them.

abbrev AffineEtaleFormalCharts (X : FppfSheaf B S hS)

AlgebraicGeometry.FormalSpace.reductionAffineEtaleComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/EtaleSite.lean, line 468. The attribute's comment: “the comparison functor from the category of the morphisms satisfying (1) and (2) to the affine étale site of X, carrying the reduction of X and its affineness as data rather than chosen from Stacks 0AIN; the functor is not shown to be an equivalence”.

Stacks 0DEE, the comparison functor into the affine étale site of X. Let X be an affine formal algebraic space over S whose reduction is the sheaf represented by an object V of the site with affine underlying scheme, by a morphism i. By Stacks 0DEA the affine étale site of X is the affine étale site of its reduction, that is of V, and this is the functor to it from the category of the morphisms φ : U ⟶ X with U an affine formal algebraic space and φ representable by algebraic spaces and étale, sending φ to U ×_X X_red.

The reduction is carried as data, with its affineness, rather than chosen from Stacks 0AIN; for an affine formal algebraic space the reduction is an affine scheme, which is why the datum is not a restriction. Stacks 0DEE asserts that this functor is an equivalence; the quasi-inverse is not constructed here.

noncomputable def reductionAffineEtaleComparison {X : FppfSheaf B S hS}
    (hX : IsAffineFormalAlgebraicSpace B S hS X) (V : BigFppfOver B S hS)
    (hV : IsAffine ((BigFppfOver.toScheme B S hS).obj V))
    (i : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj V ⟶ X)
    (_hred : IsReduction B S hS X
      ((Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj V) i) :
    AffineEtaleFormalCharts B S hS X ⥤ Space.AffineEtale B S hS (yoneda.obj V)

AlgebraicGeometry.FormalSpace.affineEtaleEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/EtaleSiteEquivalence.lean, line 528. The attribute's comment: “the equivalence of X_affine,étale with the category of the morphisms satisfying (1) and (2); fullness, faithfulness and essential surjectivity are all proved, and the affine étale site of Stacks 0DEA(3) is identified with the one the comparison functor targets”.

Stacks 0DEE. Let X be an affine formal algebraic space over S. Then X_{affine, étale} — the affine étale site of the reduction of X, in the sense of Stacks 0DEA part (3), at an arbitrary reduction datum — is equivalent to the category whose objects are the morphisms φ : U ⟶ X of formal algebraic spaces such that

1. U is an affine formal algebraic space,
2. φ is representable by algebraic spaces and étale.

The functor is the source's, (U ⟶ X) ↦ U ×_X X_red: it is AlgebraicGeometry.FormalSpace.reductionAffineEtaleComparison, read backwards and composed with the identification of X_{affine, étale} with the affine étale site of the Yoneda presheaf of the chosen affine reduction chart. Full faithfulness is AlgebraicGeometry.FormalSpace.full_affineEtaleComparison and AlgebraicGeometry.FormalSpace.faithful_affineEtaleComparison, both out of the unique extension of a morphism along a representable thickening; essential surjectivity is AlgebraicGeometry.FormalSpace.essSurj_affineEtaleComparison, whose quasi-inverse is the dependent product U_{W, q} and whose affineness is AlgebraicGeometry.FormalSpace.isAffineFormalAlgebraicSpace_liftAlong_of_affine. The source's omitted "verification that the constructions are mutually inverse to each other" is therefore supplied.

The reduction datum is a parameter, not a weakening: X_{affine, étale} is defined, in Stacks 0DEA, only for a formal algebraic space with a given reduction, and the datum exists for every affine formal algebraic space by Stacks 0AIN — in the shape used here by AlgebraicGeometry.FormalSpace.nonempty_affineReductionChart.

noncomputable def affineEtaleEquivalence (hX : IsAffineFormalAlgebraicSpace B S hS X)
    (R : Reduction B S hS X) : R.AffineEtale ≌ AffineEtaleFormalCharts B S hS X

AlgebraicGeometry.FormalSpace.reductionAffineEtaleComparison_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/EtaleSiteEquivalence.lean, line 545. The attribute's comment: “the comparison functor is an equivalence: it is full, faithful and essentially surjective”.

Stacks 0DEE. The comparison functor AlgebraicGeometry.FormalSpace.reductionAffineEtaleComparison of Stacks 0DEE is an equivalence of categories: it is full, faithful and essentially surjective. Its target is the affine étale site of X, which is identified with the site X_{affine, étale} of Stacks 0DEA part (3) by AlgebraicGeometry.FormalSpace.Reduction.affineEtaleIsoYonedaAffineReductionChart; the resulting equivalence stated with that site is AlgebraicGeometry.FormalSpace.affineEtaleEquivalence.

theorem reductionAffineEtaleComparison_isEquivalence
    (hX : IsAffineFormalAlgebraicSpace B S hS X) :
    (reductionAffineEtaleComparison' B S hS hX).IsEquivalence

AlgebraicGeometry.FormalSpace.reductionAffineEtaleComparison', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/EtaleSiteSupplement.lean, line 255. The attribute's comment: “the comparison functor from the category of the morphisms satisfying (1) and (2) to the affine étale site of X; that it is an equivalence is AlgebraicGeometry.FormalSpace.reductionAffineEtaleComparison_isEquivalence”.

Stacks 0DEE, the comparison functor into the affine étale site of X. Let X be an affine formal algebraic space over S. Its reduction X_red is the sheaf represented by an object of the site with affine underlying scheme — this is Stacks 0AIN for an affine formal algebraic space, in the form AlgebraicGeometry.FormalSpace.nonempty_affineReductionChart — and by Stacks 0DEA the affine étale site of X is the affine étale site of X_red. This is the functor to it from the category of the morphisms φ : U ⟶ X with U an affine formal algebraic space and φ representable by algebraic spaces and étale, sending φ to U ×_X X_red.

Nothing is carried as a hypothesis beyond X being an affine formal algebraic space: the reduction and its affineness are constructed, and which reduction is chosen is immaterial by AlgebraicGeometry.FormalSpace.AffineReductionChart.iso. Stacks 0DEE asserts that this functor is an equivalence; that is AlgebraicGeometry.FormalSpace.reductionAffineEtaleComparison_isEquivalence, in StacksFrontier/AlgebraicGeometry/FormalSpace/Affine/EtaleSiteEquivalence.lean.

noncomputable def reductionAffineEtaleComparison' {X : FppfSheaf B S hS}
    (hX : IsAffineFormalAlgebraicSpace B S hS X) :
    AffineEtaleFormalCharts B S hS X ⥤
      Space.AffineEtale B S hS (yoneda.obj (affineReductionChart B S hS hX).obj)

Tag 0DEF, a lemma

Tag 0DEF in the Stacks Project.

AlgebraicGeometry.FormalSpace.completionAffineEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SmallEtaleSite/CompletionToAffineEtale.lean, line 346. The attribute's comment: “the functor from the category of the completions B^∧ of its items (1) and (2) to the opposite of an affine étale site, on objects the quotient stage B^∧ ↦ Spec (B ⧸ JB) and on morphisms the map of quotient stages a continuous A-algebra homomorphism of completions induces. The site is the affine étale site of the stage Spec (A ⧸ J), the target of this library's Stacks 0DEE comparison functor at that affine object, rather than of the reduction of Spf A, which would have to be chosen from Stacks 0AIN. The functor is not shown to be an equivalence: the quasi-inverse would have to make Spf B^∧ ⟶ Spf A representable étale, which needs Stacks 0AKN and the locality on the target of the universe-lifted representability and étaleness conditions, neither of which this library carries”.

Stacks 0DEF, the functor from the category of the A-algebras B^∧ = lim B/JB of its items (1) and (2) to the opposite of an affine étale site, which is the direction in which Stacks 0DEF identifies that category with (X_{affine,étale})^{opp}. It sends an étale ring map A → B to the affine object Spec (B ⧸ JB) of the site, étale over Spec (A ⧸ J), and a continuous A-algebra homomorphism B₁^∧ → B₂^∧ to the morphism Spec (B₂ ⧸ JB₂) ⟶ Spec (B₁ ⧸ JB₁) it induces on quotient stages.

The site is the affine étale site of the stage Spec (A ⧸ J), which is the target of the comparison functor AlgebraicGeometry.FormalSpace.affineEtaleComparison of Stacks 0DEE at the affine object Spec (A ⧸ J) of the site and the stage inclusion Spec (A ⧸ J) ⟶ Spf A.

noncomputable def completionAffineEtale (D : QuotientSystem B S hS A)
    (J : WeakIdealOfDefinitionIndex A) :
    EtaleCompletion A ⥤ (Space.AffineEtale B S hS
      (yoneda.obj ((BigAffineFppf.inclusion B S hS).obj (D.stage J))))ᵒᵖ

AlgebraicGeometry.FormalSpace.EtaleCompletion, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SmallEtaleSite/McQuillanAffineEtale.lean, line 102. The attribute's comment: “item (1), the objects: an A-algebra of the form B^∧ = lim B/JB for an étale ring map A → B, named here by that ring map together with its étaleness, the completion being TopologicalRing.CompletionOver of it. The equivalence with (X_affine,étale)^opp is not constructed: it needs Stacks 0DEE as an equivalence, which this library has only as a comparison functor, and Stacks 0AN8 as an equivalence, which this library has only in the ring-theoretic form EtaleCompletion.etale_quotientMap”.

Stacks 0DEF, item (1): the datum naming an object of the category attached to a weakly admissible topological ring A. It is an étale ring map A → B; the A-algebra it names is the completion B^∧ = lim B/JB, the limit being over the weak ideals of definition J of A, see AlgebraicGeometry.FormalSpace.EtaleCompletion.completion.

structure EtaleCompletion

AlgebraicGeometry.FormalSpace.EtaleCompletion.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SmallEtaleSite/McQuillanAffineEtale.lean, line 135. The attribute's comment: “item (2), the morphisms: the continuous A-algebra homomorphisms between the objects, with the A-algebra structure of B^∧ given by the canonical map TopologicalRing.CompletionOver.canonicalMap. The equivalence with (X_affine,étale)^opp is not constructed, for the reasons recorded on EtaleCompletion”.

Stacks 0DEF, item (2): a morphism of the category, a continuous A-algebra homomorphism B₁^∧ → B₂^∧ between the completions named by two objects. The A-algebra structures are the canonical maps of Stacks 0AN6, so being an A-algebra homomorphism is the displayed commuting triangle.

structure Hom (Y Z : EtaleCompletion A)

AlgebraicGeometry.FormalSpace.mcQuillanAffineEtaleEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SmallEtaleSite/McQuillanEtaleEquivalence.lean, line 111. The attribute's comment: “the equivalence of (X_affine,étale)^opp with the category whose objects are the A-algebras B^∧ = lim B/JB for an étale ring map A → B (item (1)) and whose morphisms are the continuous A-algebra homomorphisms (item (2)), namely AlgebraicGeometry.FormalSpace.EtaleCompletion. It is the source's proof: Stacks 0DEE, affineEtaleEquivalence, composed with Stacks 0AN8, isEquivalence_etaleCompletionCharts, whose opposite is taken on the algebra side because Spf is contravariant; CategoryTheory.Equivalence.leftOp moves that one opposite to the geometric side, where the source writes it. The reduction datum is a parameter for the same reason as in Stacks 0DEE -- X_affine,étale of Stacks 0DEA(3) is defined only relative to one, and one exists by Stacks 0AIN -- and the quotient system D with its large-site condition is this library's spelling of A being a weakly admissible topological S-algebra whose Spf is an affine formal algebraic space, which is the source's hypothesis on X”.

Stacks 0DEF. Let S be a scheme contained in a big fppf site B and let X = Spf A be a McQuillan affine formal algebraic space over S: A is a weakly admissible topological ring presented over S by a quotient system D whose atlas lies in the site. Then (X_{affine,étale})^{opp} — the opposite of the affine étale site of Stacks 0DEA part (3), at an arbitrary reduction datum of X — is equivalent to the category whose

1. objects are the A-algebras B^∧ = lim B/JB for an étale ring map A → B, the limit being over the weak ideals of definition J of A, and
2. morphisms are the continuous A-algebra homomorphisms,

which is AlgebraicGeometry.FormalSpace.EtaleCompletion.

This is the source's proof: combine Stacks 0DEE, AlgebraicGeometry.FormalSpace.affineEtaleEquivalence, with Stacks 0AN8, AlgebraicGeometry.FormalSpace.isEquivalence_etaleCompletionCharts. The first identifies X_{affine,étale} with the category of the affine formal algebraic spaces representable étale over X, the second identifies that category with (EtaleCompletion A)ᵒᵖ; taking the opposite of the composite moves the single opposite from the algebra side, where Spf being contravariant puts it, to the geometric side, where Stacks 0DEF writes it.

def mcQuillanAffineEtaleEquivalence (hA : TopologicalRing.IsWeaklyAdmissible A)
    (D : QuotientSystem B S hS A) (hD : D.HasLargeSite)
    (R : Reduction B S hS (formalSpectrum D)) :
    R.AffineEtaleᵒᵖ ≌ EtaleCompletion A

Tag 0DEG, a lemma

Tag 0DEG in the Stacks Project.

AlgebraicGeometry.FormalSpace.spacesEtaleComparison_isEquivalence', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/LiftAlongAffineBase.lean, line 440. The attribute's comment: “the equivalence; full faithfulness and essential surjectivity are both proved, the latter from the source's assertion that U_{V, ψ} is a formal algebraic space, which is AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_liftAlong”.

Stacks 0DEG. The comparison functor from the category of the formal algebraic spaces representable étale over a formal algebraic space X to X_{spaces, étale} is an equivalence of categories.

Full faithfulness is AlgebraicGeometry.FormalSpace.bijective_spacesEtaleComparison_map and essential surjectivity is AlgebraicGeometry.FormalSpace.essSurj_spacesEtaleComparison. Every assertion of the source is proved: the sheaf U_{V, ψ} the source produces is constructed, in StacksFrontier/AlgebraicGeometry/FormalSpace/SpacesEtaleQuasiInverse.lean, its fibre product with X_red over X is identified with V, the source's omitted verification that U_{V, ψ} ⟶ X is representable by algebraic spaces and étale is proved, in StacksFrontier/AlgebraicGeometry/FormalSpace/SpacesEtaleQuasiInverseRepresentable.lean, and that U_{V, ψ} is a formal algebraic space is AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_liftAlong.

The reduction of X is a parameter, not a weakening: X_{spaces, étale} is defined, in Stacks 0DEA, only for a formal algebraic space with a given reduction, and the datum exists for every formal algebraic space by Stacks 0AIN.

theorem spacesEtaleComparison_isEquivalence' {X : FppfSheaf B S hS}
    (hX : IsFormalAlgebraicSpace B S hS X) (R : Reduction B S hS X) :
    (spacesEtaleComparison hX R).IsEquivalence

AlgebraicGeometry.FormalSpace.spacesEtaleComparison_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpacesEtaleIdentification.lean, line 295. The attribute's comment: “the equivalence; bijectivity on morphisms and essential surjectivity — the two verifications the source omits — are hypotheses, and the equivalence is read against a given reduction of X, which Stacks 0AIN supplies”.

The comparison functor from the category of the formal algebraic spaces representable étale over a formal algebraic space X to X_{spaces, étale} is an equivalence of categories.

Two hypotheses are carried, and they are exactly the two verifications the source omits. hhom is bijectivity on morphisms, which is the source's "we omit the verification that the constructions are mutually inverse to each other": it amounts to lifting a morphism over X along the thickening X_red ⟶ X against an étale target. hess is essential surjectivity, which is the source's construction of the quasi-inverse U_{V, ψ} together with its "we omit the verification that U_{V, ψ} ⟶ X is representable by algebraic spaces and étale". The reduction of X is a given as well, which is no weakening: X_{spaces, étale} is defined, in Stacks 0DEA, only for a formal algebraic space with a given reduction, and Stacks 0AIN supplies one.

theorem spacesEtaleComparison_isEquivalence {X : FppfSheaf B S hS}
    (hX : IsFormalAlgebraicSpace B S hS X) (R : Reduction B S hS X)
    (hhom : ∀ U U' : RepresentableEtaleFormalSpacesOver X,
      Function.Bijective fun f : U ⟶ U' ↦ (spacesEtaleComparison hX R).map f)
    (hess : ∀ V : R.SpacesEtale, ∃ U : RepresentableEtaleFormalSpacesOver X,
      Nonempty ((spacesEtaleComparison hX R).obj U ≅ V)) :
    (spacesEtaleComparison hX R).IsEquivalence

AlgebraicGeometry.FormalSpace.bijective_spacesEtaleComparison_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpacesEtaleIdentificationSupplement.lean, line 284. The attribute's comment: “bijectivity on morphisms: the source's 'we omit the verification that the constructions are mutually inverse to each other'”.

The comparison functor is bijective on morphisms: for φ : U ⟶ X and φ' : U' ⟶ X representable by algebraic spaces and étale, with U and U' formal algebraic spaces, the morphisms U ⟶ U' over X correspond bijectively to the morphisms U_red ⟶ U'_red over X_red.

This is the source's "we omit the verification that the constructions are mutually inverse to each other", on the side that needs the lifting of a morphism along the thickening U_red ⟶ U: a morphism of reductions over X_red is, by the fibre-product description U'_red = U' ×_X X_red of AlgebraicGeometry.FormalSpace.isPullback_inclusion_liftSheafMap_map, the same thing as a morphism U_red ⟶ U' over X, and such a morphism extends uniquely to U ⟶ U' over X by AlgebraicGeometry.FormalSpace.existsUnique_hom_of_isRepresentableThickening. In both directions the morphism of reductions is recovered from the extension by the characterisation AlgebraicGeometry.FormalSpace.Reduction.eq_map, so no naturality has to be checked.

theorem bijective_spacesEtaleComparison_map {X : FppfSheaf B S hS}
    (hX : IsFormalAlgebraicSpace B S hS X) (R : Reduction B S hS X)
    (U U' : RepresentableEtaleFormalSpacesOver X) :
    Function.Bijective fun f : U ⟶ U' ↦ (spacesEtaleComparison hX R).map f

AlgebraicGeometry.FormalSpace.faithful_spacesEtaleComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpacesEtaleIdentificationSupplement.lean, line 292. The attribute's comment: “faithfulness of the comparison functor”.

The comparison functor is faithful.

theorem faithful_spacesEtaleComparison {X : FppfSheaf B S hS}
    (hX : IsFormalAlgebraicSpace B S hS X) (R : Reduction B S hS X) :
    (spacesEtaleComparison hX R).Faithful

AlgebraicGeometry.FormalSpace.full_spacesEtaleComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpacesEtaleIdentificationSupplement.lean, line 299. The attribute's comment: “fullness of the comparison functor”.

The comparison functor is full.

theorem full_spacesEtaleComparison {X : FppfSheaf B S hS}
    (hX : IsFormalAlgebraicSpace B S hS X) (R : Reduction B S hS X) :
    (spacesEtaleComparison hX R).Full

AlgebraicGeometry.FormalSpace.spacesEtaleQuasiInverse, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpacesEtaleQuasiInverse.lean, line 223. The attribute's comment: “the quasi-inverse U_{V, ψ} of the proof, as an fppf sheaf; that U_{V, ψ} ⟶ X is representable by algebraic spaces and étale is proved in StacksFrontier/AlgebraicGeometry/FormalSpace/SpacesEtaleQuasiInverseRepresentable.lean, that U_{V, ψ} is a formal algebraic space is not, see the implementation notes”.

Stacks 0DEG. The quasi-inverse of the proof, at an object ψ : V ⟶ X_red of X_{spaces, étale}: the fppf sheaf U_{V, ψ} whose sections over T are the pairs (a, b) with a : T ⟶ X a morphism of formal algebraic spaces and b : T ×_{a, X} X_red ⟶ V a morphism over X_red.

This is the functor the source writes down, as an fppf sheaf. That it is a sheaf is AlgebraicGeometry.FormalSpace.isSheaf_liftAlongPresheaf.

def spacesEtaleQuasiInverse {X : FppfSheaf B S hS} (R : Reduction B S hS X)
    (V : R.SpacesEtale) : FppfSheaf B S hS

AlgebraicGeometry.FormalSpace.spacesEtaleQuasiInverseBase, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpacesEtaleQuasiInverse.lean, line 230. The attribute's comment: “the transformation U_{V, ψ} ⟶ X, (a, b) ↦ a”.

Stacks 0DEG. The transformation U_{V, ψ} ⟶ X, (a, b) ↦ a, which the source claims defines an object of the category of formal algebraic spaces representable étale over X.

def spacesEtaleQuasiInverseBase {X : FppfSheaf B S hS} (R : Reduction B S hS X)
    (V : R.SpacesEtale) : spacesEtaleQuasiInverse B S hS R V ⟶ X

AlgebraicGeometry.FormalSpace.isPullback_spacesEtaleQuasiInverseSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpacesEtaleQuasiInverse.lean, line 250. The attribute's comment: “the quasi-inverse is a right inverse: U_{V, ψ} ×_X X_red = V over X_red, which is one half of the source's 'the constructions are mutually inverse to each other'”.

Stacks 0DEG. V is the fibre product U_{V, ψ} ×_X X_red.

Since the comparison functor of Stacks 0DEG sends φ : U ⟶ X to U ×_X X_red — which is AlgebraicGeometry.FormalSpace.isPullback_inclusion_liftSheafMap_map — this says that the comparison functor applied to the quasi-inverse at (V, ψ) returns (V, ψ). It is the half of the source's "the constructions are mutually inverse to each other" that does not need the lifting of morphisms along the thickening X_red ⟶ X.

theorem isPullback_spacesEtaleQuasiInverseSection {X : FppfSheaf B S hS}
    (R : Reduction B S hS X) (V : R.SpacesEtale) :
    IsPullback (spacesEtaleQuasiInverseSection B S hS R V)
      (liftSheafMap B S hS V.obj.hom) (spacesEtaleQuasiInverseBase B S hS R V) R.inclusion

AlgebraicGeometry.FormalSpace.spacesEtaleQuasiInverseFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpacesEtaleQuasiInverse.lean, line 298. The attribute's comment: “the quasi-inverse as a functor into the slice over X — the source's 'thus we obtain our functor (V, ψ) ↦ (U_{V, ψ} ⟶ X) in the other direction'. That its values lie in the subcategory of the formal algebraic spaces representable étale over X is proved, in both of the source's assertions: isRepresentableEtale_spacesEtaleQuasiInverseBase here and isFormalAlgebraicSpace_liftAlong further down the import order; the codomain restriction and the equivalence assembled from them are spacesEtaleComparison_isEquivalence. The slice is an import-order artefact, not a missing step”.

Stacks 0DEG. The quasi-inverse as a functor, which is what the source produces: an object ψ : V ⟶ X_red of X_{spaces, étale} goes to the formal-space-shaped sheaf U_{V, ψ} with its morphism to X, and a morphism of X_{spaces, étale} goes to the morphism over X obtained by postcomposition on the second component.

It lands in the slice Over X rather than in the category of Stacks 0DEG for a reason of import order only. Both of the source's assertions about its values are proved: that the structure morphism is representable by algebraic spaces and étale is AlgebraicGeometry.FormalSpace.isRepresentableEtale_spacesEtaleQuasiInverseBase, and that U_{V, ψ} is a formal algebraic space is AlgebraicGeometry.FormalSpace.isFormalAlgebraicSpace_liftAlong, which lives further down the import order, in StacksFrontier/AlgebraicGeometry/FormalSpace/LiftAlongAffineBase.lean. The equivalence assembled from them is there as well, AlgebraicGeometry.FormalSpace.spacesEtaleComparison_isEquivalence. See the module documentation.

def spacesEtaleQuasiInverseFunctor {X : FppfSheaf B S hS} (R : Reduction B S hS X) :
    R.SpacesEtale ⥤ Over X

AlgebraicGeometry.FormalSpace.isRepresentableEtale_spacesEtaleQuasiInverseBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/SpacesEtaleQuasiInverseRepresentable.lean, line 471. The attribute's comment: “the omitted verification that U_{V, ψ} ⟶ X is representable by algebraic spaces and étale”.

Stacks 0DEG. The structure morphism U_{V, ψ} ⟶ X of the quasi-inverse of the proof is representable by algebraic spaces and étale. This is one of the two verifications the source omits — "we omit the verification that U_{V, ψ} ⟶ X is representable by algebraic spaces and étale" — and it is proved here outright.

theorem isRepresentableEtale_spacesEtaleQuasiInverseBase {X : FppfSheaf B S hS}
    (R : Reduction B S hS X) (V : R.SpacesEtale) :
    IsRepresentableEtale B S hS (spacesEtaleQuasiInverseBase B S hS R V)

Tag 0DEH, a lemma

Tag 0DEH in the Stacks Project.

AlgebraicGeometry.FormalSpace.affineEtaleReductionEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/AffineEtaleReductionEquivalence.lean, line 241.

Stacks 0DEH. Let S be a scheme and X a formal algebraic space over S. Then X_{affine, étale} is equivalent to the category whose objects are the morphisms φ : U ⟶ X of formal algebraic spaces with U an affine formal algebraic space and φ representable by algebraic spaces and étale; the equivalence is the functor U ↦ U_red, AlgebraicGeometry.FormalSpace.affineEtaleReductionFunctor.

def affineEtaleReductionEquivalence {X : FppfSheaf B S hS}
    (hX : IsFormalAlgebraicSpace B S hS X) (R : Reduction B S hS X) :
    AffineEtaleFormalCharts B S hS X ≌ R.AffineEtale

Sources

• Section 87.34, Tag 0DE9
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.FormalSpace.Reduction.SmallEtale · AlgebraicGeometry.FormalSpace.Reduction.smallEtaleTopology · AlgebraicGeometry.FormalSpace.Reduction.SpacesEtale · AlgebraicGeometry.FormalSpace.Reduction.spacesEtaleTopology · AlgebraicGeometry.FormalSpace.Reduction.AffineEtale · AlgebraicGeometry.FormalSpace.Reduction.affineEtaleTopology · AlgebraicGeometry.FormalSpace.canonicalSmallEtale · AlgebraicGeometry.FormalSpace.canonicalSmallEtaleTopology

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.