76.8 Topological invariance of… to 76.14 Formally unramified…

Section76.8 Topological invariance of the étale site#

Section 76.8 of the Stacks Project, Tag 05ZG. 3 tags here are carried by 32 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05ZH, a theorem

Tag 05ZH in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_spacesBaseChange_of_isIntegralHom_of_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleEssSurj/IntegralUniversallyInjective.lean, line 227. The attribute's comment: “the equivalence at the tag's own class: integral, universally injective and surjective”.

For every integral, universally injective and surjective morphism f of algebraic spaces over S, base change V ↦ X ×_Y V is an equivalence from the spaces-étale site of Y to that of X.

theorem isEquivalence_spacesBaseChange_of_isIntegralHom_of_universallyInjective (f : X ⟶ Y)
    (hint : IsIntegralHom B S hS f.hom) (hui : UniversallyInjective B S hS f.hom)
    (hsurj : IsSurjective B S hS f.hom) :
    (spacesBaseChange B S hS f).functor.IsEquivalence

AlgebraicGeometry.Space.essSurj_spacesBaseChange_of_isFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleEssSurj/LiftedEtalePresentation.lean, line 592. The attribute's comment: “essential surjectivity at a first-order thickening”.

Base change V ↦ X ×_Y V is essentially surjective from the spaces-étale site of Y to that of X, for the inclusion f of a first-order thickening.

theorem essSurj_spacesBaseChange_of_isFirstOrderThickening (f : X ⟶ Y) [Mono f.hom]
    (hT : IsFirstOrderThickening B S hS Y (Subfunctor.range f.hom)) :
    (spacesBaseChange B S hS f).functor.EssSurj

AlgebraicGeometry.Space.isEquivalence_spacesBaseChange_of_isFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleEssSurj/LiftedEtalePresentation.lean, line 602. The attribute's comment: “the first-order thickening case, not the integral universally injective one”.

Base change V ↦ X ×_Y V is an equivalence from the spaces-étale site of Y to that of X, for the inclusion f of a first-order thickening.

theorem isEquivalence_spacesBaseChange_of_isFirstOrderThickening (f : X ⟶ Y) [Mono f.hom]
    (hT : IsFirstOrderThickening B S hS Y (Subfunctor.range f.hom)) :
    (spacesBaseChange B S hS f).functor.IsEquivalence

AlgebraicGeometry.Space.essSurj_spacesBaseChange_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleEssSurj/Thickening.lean, line 521. The attribute's comment: “ESSENTIAL SURJECTIVITY ONLY, at a thickening of ARBITRARY order. This lifts the FIRST-ORDER restriction of AlgebraicGeometry.Space.essSurj_spacesBaseChange_of_isFirstOrderThickening, which descends the two maps of the lifted etale equivalence relation by the square-zero lifting property of Stacks 0611; the route here is the source's own, where they are descended by FULLNESS at arbitrary order, AlgebraicGeometry.Space.full_spacesBaseChange_of_isThickening, and every uniqueness step is FAITHFULNESS at arbitrary order, AlgebraicGeometry.Space.faithful_spacesBaseChange_of_isThickening. Together with AlgebraicGeometry.Space.fullyFaithfulSpacesBaseChangeOfIsThickening this gives the EQUIVALENCE at arbitrary order, AlgebraicGeometry.Space.isEquivalence_spacesBaseChange_of_isThickening. The source states the tag for an arbitrary INTEGRAL, UNIVERSALLY INJECTIVE and SURJECTIVE morphism, which is a wider class: the library proves only that a thickening inclusion belongs to it (Stacks 05ZL, AlgebraicGeometry.Space.isIntegralHom_universallyInjective_isSurjective_ι_of_isThickening) and not the converse, so that wider class is NOT covered”.

Let G ⊂ Y be a thickening of algebraic spaces over S, of arbitrary order. Base change along the inclusion, V ↦ G ×_Y V, is essentially surjective from the spaces-étale site of Y to that of G.

theorem essSurj_spacesBaseChange_of_isThickening {G : Subfunctor Y.1}
    (hG : IsThickening B S hS Y G) :
    (spacesBaseChange B S hS (IsThickening.inclusion B S hS hG)).functor.EssSurj

AlgebraicGeometry.Space.isEquivalence_spacesBaseChange_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleEssSurj/Thickening.lean, line 540. The attribute's comment: “the EQUIVALENCE at a thickening of ARBITRARY order -- all three of faithfulness, fullness and essential surjectivity, with no hypothesis beyond the thickening and no monomorphism hypothesis. What is still NOT covered is the source's wider class of an arbitrary INTEGRAL, UNIVERSALLY INJECTIVE and SURJECTIVE morphism: the library proves only that a thickening inclusion lies in that class (Stacks 05ZL, AlgebraicGeometry.Space.isIntegralHom_universallyInjective_isSurjective_ι_of_isThickening), not the converse. The first-order statement AlgebraicGeometry.Space.isEquivalence_spacesBaseChange_of_isFirstOrderThickening is subsumed up to the identification of the source of f with the range of f.hom”.

Let G ⊂ Y be a thickening of algebraic spaces over S, of arbitrary order. Base change along the inclusion, V ↦ G ×_Y V, is an equivalence from the spaces-étale site of Y to that of G.

theorem isEquivalence_spacesBaseChange_of_isThickening {G : Subfunctor Y.1}
    (hG : IsThickening B S hS Y G) :
    (spacesBaseChange B S hS (IsThickening.inclusion B S hS hG)).functor.IsEquivalence

AlgebraicGeometry.Space.faithful_spacesBaseChange_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleFaithfulGeneral.lean, line 131. The attribute's comment: “FAITHFULNESS ONLY, for an arbitrary morphism surjective on points -- so at a thickening of ARBITRARY order, and under a hypothesis weaker than the source's integral, universally injective and surjective. The library's other Stacks 05ZH statements are restricted to a FIRST-ORDER thickening because they go through the square-zero lifting property of Stacks 0611; this one reproduces the source's own route instead. FULLNESS is also available at arbitrary order, at a thickening, as AlgebraicGeometry.Space.full_spacesBaseChange_of_isThickening; ESSENTIAL SURJECTIVITY remains first-order, see AlgebraicGeometry.Space.isEquivalence_spacesBaseChange_of_isFirstOrderThickening”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S which is surjective on points. Base change V ↦ X ×_Y V is faithful from the spaces-étale site of Y to that of X.

theorem faithful_spacesBaseChange_of_isSurjective (f : X ⟶ Y)
    (hf : IsSurjective B S hS f.hom) :
    (spacesBaseChange B S hS f).functor.Faithful

AlgebraicGeometry.Space.faithful_spacesBaseChange_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleFaithfulGeneral.lean, line 163. The attribute's comment: “FAITHFULNESS ONLY, at a thickening of ARBITRARY order. FULLNESS at arbitrary order is AlgebraicGeometry.Space.full_spacesBaseChange_of_isThickening; ESSENTIAL SURJECTIVITY at arbitrary order is AlgebraicGeometry.Space.essSurj_spacesBaseChange_of_isThickening”.

Let G ⊂ X be a thickening of algebraic spaces over S, of arbitrary order. Base change along the inclusion, V ↦ G ×_X V, is faithful from the spaces-étale site of X to that of G.

theorem faithful_spacesBaseChange_of_isThickening {G : Subfunctor X.1}
    (hG : IsThickening B S hS X G) :
    (spacesBaseChange B S hS (IsThickening.inclusion B S hS hG)).functor.Faithful

AlgebraicGeometry.Space.full_spacesBaseChange_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleFullGeneral.lean, line 334. The attribute's comment: “FULLNESS ONLY, at a thickening of ARBITRARY order. Together with AlgebraicGeometry.Space.faithful_spacesBaseChange_of_isThickening this gives FULL FAITHFULNESS at arbitrary order, bundled as AlgebraicGeometry.Space.fullyFaithfulSpacesBaseChangeOfIsThickening; ESSENTIAL SURJECTIVITY is not covered here; it is proved at arbitrary order in AlgebraicGeometry.Space.essSurj_spacesBaseChange_of_isThickening, and the equivalence in AlgebraicGeometry.Space.isEquivalence_spacesBaseChange_of_isThickening. The library's other fullness statement, AlgebraicGeometry.Space.full_spacesBaseChange_of_isFirstOrderThickening, is restricted to first order because it goes through the square-zero lifting property of Stacks 0611; this one reproduces the source's graph argument instead, and the source's integrality and universal injectivity hypotheses are not needed beyond what a thickening already gives”.

Let G ⊂ Y be a thickening of algebraic spaces over S, of arbitrary order. Base change along the inclusion, V ↦ G ×_Y V, is full from the spaces-étale site of Y to that of G.

theorem full_spacesBaseChange_of_isThickening {G : Subfunctor Y.1}
    (hG : IsThickening B S hS Y G) :
    (spacesBaseChange B S hS (IsThickening.inclusion B S hS hG)).functor.Full

AlgebraicGeometry.Space.fullyFaithfulSpacesBaseChangeOfIsThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleFullGeneral.lean, line 347. The attribute's comment: “FULL FAITHFULNESS ONLY, at a thickening of ARBITRARY order; ESSENTIAL SURJECTIVITY is not covered here, and is proved at arbitrary order in AlgebraicGeometry.Space.essSurj_spacesBaseChange_of_isThickening”.

Let G ⊂ Y be a thickening of algebraic spaces over S, of arbitrary order. Base change along the inclusion, V ↦ G ×_Y V, is fully faithful from the spaces-étale site of Y to that of G.

noncomputable def fullyFaithfulSpacesBaseChangeOfIsThickening {G : Subfunctor Y.1}
    (hG : IsThickening B S hS Y G) :
    (spacesBaseChange B S hS (IsThickening.inclusion B S hS hG)).functor.FullyFaithful

AlgebraicGeometry.Space.fullyFaithfulSpacesBaseChangeOfIsFirstOrderThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleFullyFaithful.lean, line 192. The attribute's comment: “full faithfulness at a first-order thickening”.

Base change V ↦ X ×_Y V along the inclusion f of a first-order thickening is fully faithful from the spaces-étale site of Y to that of X.

noncomputable def fullyFaithfulSpacesBaseChangeOfIsFirstOrderThickening [Mono f.hom]
    (hT : IsFirstOrderThickening B S hS Y (Subfunctor.range f.hom)) :
    (spacesBaseChange B S hS f).functor.FullyFaithful

AlgebraicGeometry.Space.faithful_spacesBaseChange_of_mono_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleFullyFaithful.lean, line 212. The attribute's comment: “faithfulness at an arbitrary thickening”.

Base change along the inclusion of a thickening — of no prescribed order — is faithful on spaces-étale sites.

theorem faithful_spacesBaseChange_of_mono_of_isThickening [Mono f.hom]
    (hT : IsThickening B S hS Y (Subfunctor.range f.hom)) :
    (spacesBaseChange B S hS f).functor.Faithful

AlgebraicGeometry.Space.full_spacesBaseChange_of_mono_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleFullyFaithful.lean, line 222. The attribute's comment: “fullness at an arbitrary thickening”.

Base change along the inclusion of a thickening — of no prescribed order — is full on spaces-étale sites.

theorem full_spacesBaseChange_of_mono_of_isThickening [Mono f.hom]
    (hT : IsThickening B S hS Y (Subfunctor.range f.hom)) :
    (spacesBaseChange B S hS f).functor.Full

AlgebraicGeometry.Space.fullyFaithfulSpacesBaseChangeOfMonoOfIsThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleFullyFaithful.lean, line 232. The attribute's comment: “full faithfulness at an arbitrary thickening”.

Base change V ↦ X ×_Y V is fully faithful from the spaces-étale site of Y to that of X, for f a monomorphism whose range is a thickening of Y of arbitrary order.

noncomputable def fullyFaithfulSpacesBaseChangeOfMonoOfIsThickening [Mono f.hom]
    (hT : IsThickening B S hS Y (Subfunctor.range f.hom)) :
    (spacesBaseChange B S hS f).functor.FullyFaithful

AlgebraicGeometry.Space.fullyFaithfulSpacesBaseChangeOfIsThickeningRange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleFullyFaithfulThickening.lean, line 63. The attribute's comment: “full faithfulness at a thickening of unbounded order, not the integral universally injective case”.

Base change V ↦ X ×_Y V is fully faithful from the spaces-étale site of Y to that of X, for the inclusion f of a thickening of algebraic spaces — a monomorphism whose range is a closed subspace with the same points, with no hypothesis on its defining ideal.

noncomputable def fullyFaithfulSpacesBaseChangeOfIsThickeningRange [Mono f.hom]
    (hT : IsThickening B S hS Y (Subfunctor.range f.hom)) :
    (spacesBaseChange B S hS f).functor.FullyFaithful

AlgebraicGeometry.Space.fullyFaithfulSpacesBaseChangeOfIsNthOrderThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleFullyFaithfulThickening.lean, line 88. The attribute's comment: “full faithfulness at a thickening of finite order”.

Base change V ↦ X ×_Y V is fully faithful from the spaces-étale site of Y to that of X, for the inclusion f of a thickening of order n, whose defining ideal has vanishing (n+1)st power.

noncomputable def fullyFaithfulSpacesBaseChangeOfIsNthOrderThickening {n : ℕ} [Mono f.hom]
    (hT : IsNthOrderThickening B S hS n Y (Subfunctor.range f.hom)) :
    (spacesBaseChange B S hS f).functor.FullyFaithful

Declarations registered for the tag:

• AlgebraicGeometry.Space.C1573.isEquivalence_spacesBaseChange_of_isThickeningHom, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleEquivalenceGeneral.lean, line 84 (StacksFrontier): “the equivalence, for the inclusion of a thickening of arbitrary order”.

Tag 07VW, a lemma

Tag 07VW in the Stacks Project.

AlgebraicGeometry.Space.smallEtalePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleTopologicalInvariance.lean, line 298. The attribute's comment: “the base-change functor on the étale schemes, which needs only integrality of f; the two equivalences are stated separately”.

Stacks 07VW, the base-change functor on the étale schemes. For an integral morphism f : X ⟶ Y of algebraic spaces over S, base change V ↦ X ×_Y V carries the small étale site of Y to that of X.

It is the restriction of base change on the spaces-étale sites along the fully faithful comparison functors of Stacks 03G1 — see AlgebraicGeometry.Space.smallEtalePullbackComparisonIso — which exists because the base change of a scheme étale over Y is a scheme, by the implication of Stacks 07VV from the target.

noncomputable def smallEtalePullback (f : X ⟶ Y) (hf : IsIntegralHom B S hS f.hom) :
    SmallEtale B S hS Y.1 ⥤ SmallEtale B S hS X.1

AlgebraicGeometry.Space.smallEtalePullbackComparisonIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleTopologicalInvariance.lean, line 311. The attribute's comment: “the restriction to the étale schemes is the spaces-étale base change”.

Stacks 07VW, canonicity of the base-change functor on the étale schemes. AlgebraicGeometry.Space.smallEtalePullback is the restriction of base change on the spaces-étale sites: composing it with the comparison functor of X recovers base change applied to the comparison functor of Y.

noncomputable def smallEtalePullbackComparisonIso (f : X ⟶ Y)
    (hf : IsIntegralHom B S hS f.hom) :
    smallEtalePullback B S hS f hf ⋙ comparisonFunctor B S hS X ≅
      comparisonFunctor B S hS Y ⋙ (spacesBaseChange B S hS f).functor

AlgebraicGeometry.Space.affineEtalePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleTopologicalInvariance.lean, line 372. The attribute's comment: “the base-change functor on the affine étale schemes, which needs only integrality of f; the two equivalences are stated separately”.

Stacks 07VW, the base-change functor on the affine étale schemes. For an integral morphism f : X ⟶ Y of algebraic spaces over S, base change V ↦ X ×_Y V carries the affine étale site of Y to that of X: a base change of an affine chart is affine, because the projection is integral and an integral morphism with affine target has affine source.

noncomputable def affineEtalePullback (f : X ⟶ Y) (hf : IsIntegralHom B S hS f.hom) :
    AffineEtale B S hS Y.1 ⥤ AffineEtale B S hS X.1

AlgebraicGeometry.Space.affineEtalePullbackInclusionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleTopologicalInvariance.lean, line 382. The attribute's comment: “the restriction to the affine étale schemes is the small étale base change”.

Stacks 07VW, canonicity of the base-change functor on the affine étale schemes. AlgebraicGeometry.Space.affineEtalePullback is the restriction of AlgebraicGeometry.Space.smallEtalePullback to the affine charts.

noncomputable def affineEtalePullbackInclusionIso (f : X ⟶ Y)
    (hf : IsIntegralHom B S hS f.hom) :
    affineEtalePullback B S hS f hf ⋙ AffineEtale.inclusion B S hS X.1 ≅
      AffineEtale.inclusion B S hS Y.1 ⋙ smallEtalePullback B S hS f hf

AlgebraicGeometry.Space.isEquivalence_smallEtalePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TopologicalInvariance/SmallEtale.lean, line 223. The attribute's comment: “the equivalence Y_étale ⟶ X_étale of small étale sites, the restriction of the equivalence of Stacks 05ZH on spaces-étale sites (that it is the restriction is AlgebraicGeometry.Space.smallEtalePullbackComparisonIso)”.

Stacks 07VW, on the étale schemes. Let f : X ⟶ Y be an integral, universally injective and surjective morphism of algebraic spaces over S. Then base change V ↦ X ×_Y V is an equivalence from the small étale site of Y to that of X; it is the restriction of the equivalence of Stacks 05ZH on the spaces-étale sites (AlgebraicGeometry.Space.smallEtalePullbackComparisonIso).

The equivalence of Stacks 05ZH restricts along the fully faithful comparison functors of Stacks 03G1 because, for V étale over Y, V is a scheme exactly when X ×_Y V is: the projection X ×_Y V ⟶ V is integral and bijective on points, so Stacks 07VV applies in both directions.

theorem isEquivalence_smallEtalePullback (f : X ⟶ Y) (hf : IsIntegralHom B S hS f.hom)
    (hinj : UniversallyInjective B S hS f.hom) (hsurj : IsSurjective B S hS f.hom) :
    (smallEtalePullback B S hS f hf).IsEquivalence

AlgebraicGeometry.Space.isEquivalence_affineEtalePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/TopologicalInvariance/SmallEtale.lean, line 261. The attribute's comment: “the equivalence Y_affine,étale ⟶ X_affine,étale of affine étale sites, the restriction of the equivalence on the small étale sites (that it is the restriction is AlgebraicGeometry.Space.affineEtalePullbackInclusionIso)”.

Stacks 07VW, on the affine étale schemes. Let f : X ⟶ Y be an integral, universally injective and surjective morphism of algebraic spaces over S. Then base change V ↦ X ×_Y V is an equivalence from the affine étale site of Y to that of X; it is the restriction of the equivalence on the small étale sites (AlgebraicGeometry.Space.affineEtalePullbackInclusionIso).

For V étale over Y and a scheme, V is affine exactly when X ×_Y V is: the projection is integral, so an affine V has affine base change, and it is surjective and universally closed, so an affine base change forces V affine by Stacks 07VT.

theorem isEquivalence_affineEtalePullback (f : X ⟶ Y) (hf : IsIntegralHom B S hS f.hom)
    (hinj : UniversallyInjective B S hS f.hom) (hsurj : IsSurjective B S hS f.hom) :
    (affineEtalePullback B S hS f hf).IsEquivalence

Tag 05ZI, a remark

Tag 05ZI in the Stacks Project.

AlgebraicGeometry.isIso_of_isFinite_of_etale_of_connectedSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Etale/AffineLineFiniteEtaleCovering.lean, line 29. The attribute's comment: “the input: A^1_k has no nontrivial connected finite étale covering when k is algebraically closed of characteristic 0 (details omitted in the source)”.

Over an algebraically closed field k of characteristic zero, a finite étale morphism Y ⟶ 𝐀¹_k = Spec k[X] with Y connected is an isomorphism.

theorem isIso_of_isFinite_of_etale_of_connectedSpace {k : Type u} [Field k] [IsAlgClosed k]
    [CharZero k] {Y : Scheme.{u}} (f : Y ⟶ Spec (.of k[X])) [IsFinite f] [Etale f]
    [ConnectedSpace Y] : IsIso f

AlgebraicGeometry.Space.universalHomeomorphism_squaringMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/UniversalHomeomorphism.lean, line 772. The attribute's comment: “the remark's own last sentence: there exists a universal homeomorphism X ⟶ 𝐀¹_k, exhibited directly by t ↦ t² on affine spaces. NOT asserted: that this X is the same as the quotient Y/G of the remark's alternative construction, that Y ⟶ X is a nontrivial connected finite étale covering, and that 𝐀¹_k has no nontrivial connected finite étale coverings”.

Stacks 05ZI, the last sentence: there is a universal homeomorphism X ⟶ 𝐀¹_k, exhibited directly by t ↦ t ^ 2 on affine space.

Here X is the quotient of the affine line by the relation identifying t with -t away from the origin, the algebraic space of Stacks 05Z6, and the morphism is the one Stacks 05VS descends from squaring the coordinate. It is universally closed by AlgebraicGeometry.Space.universallyClosed_squaringMap, universally injective by Stacks 05VS part (4), and surjective after every base change by AlgebraicGeometry.Space.isSurjective_pullback_fst_squaringMap; the criterion is AlgebraicGeometry.Space.universalHomeomorphism_of_universallyClosed_of_universallyInjective.

Stacks 05Z6 and Stacks 05ZI state this over an algebraically closed field of characteristic zero. Only 2 ≠ 0 in k is used, and only for universal injectivity.

theorem universalHomeomorphism_squaringMap (hchar : (2 : k) ≠ 0)
    (hk : B.Contains (Spec (.of k)))
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hk) (Type u)] :
    UniversalHomeomorphism B (Spec (.of k)) hk (squaringMap k B hk)

AlgebraicGeometry.AffineLineInvolution.whiskerLeft_punctured_comp_toQuotientSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/UniversalHomeomorphismEtaleFailure.lean, line 157. The attribute's comment: “a construction input only: the gluing datum of the covering Y of the remark, at the level of points. NEITHER assertion of the remark is asserted -- not that a universal homeomorphism of algebraic spaces need be non-representable, and not that Tag 05ZH fails for universal homeomorphisms”.

The overlap identity of Stacks 05ZI. The two maps from the punctured affine line to the quotient sheaf of Stacks 02Z1, one through the inclusion of the puncture and one through negation of the coordinate, agree. No hypothesis on the ground field is used.

theorem whiskerLeft_punctured_comp_toQuotientSheaf {C : Type v} [Category.{w} C]
    (J : GrothendieckTopology C) [HasSheafify J (Type u)] (F : C ⥤ Over (Spec (.of k))) :
    F.op.whiskerLeft (yoneda.map (puncturedAffineLineInclusion k)) ≫
        Stacks.Groupoids.toQuotientSheaf J F (involutionRelation k) =
      F.op.whiskerLeft (yoneda.map (puncturedAffineLineInclusion k ≫ affineLineNeg k)) ≫
        Stacks.Groupoids.toQuotientSheaf J F (involutionRelation k)

AlgebraicGeometry.AffineLineInvolution.yoneda_puncturedChart_comp_quotientChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/UniversalHomeomorphismEtaleFailure.lean, line 227. The attribute's comment: “a construction input only: the two chart maps of the doubled-origin line agree over the overlap, which is the remark's these agree on the overlap by construction of X. The morphism Y ⟶ X itself is not constructed and neither assertion of the remark is asserted”.

The gluing datum of the covering of Stacks 05ZI. The two maps from the punctured affine line to the quotient X of Stacks 05Z6, one through the inclusion of the puncture and one through negation of the coordinate, agree as morphisms of presheaves on the site.

This is the assertion that the two charts of the affine line with doubled origin have the same image in X over the overlap of the charts, which is what makes the covering of Stacks 05ZI well defined. No hypothesis on the ground field is used.

theorem yoneda_puncturedChart_comp_quotientChart :
    yoneda.map (puncturedChartInclusion k B hk) ≫ quotientChart k B hk =
      yoneda.map (puncturedChartNeg k B hk) ≫ quotientChart k B hk

AlgebraicGeometry.connectedSpace_affineSpaceWithDoubledZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/UniversalHomeomorphismEtaleFailure.lean, line 296. The attribute's comment: “a construction input only: the doubled-origin affine space is connected. That Y ⟶ X is a nontrivial connected finite etale covering is NOT asserted -- this library has no notion of a connected algebraic space”.

The connectedness input of Stacks 05ZI. In positive dimension affine n-space over a field with its origin doubled is a connected scheme: its two charts are spectra of a polynomial ring, hence irreducible, they cover the glued scheme, and their images share the image of the generic point.

theorem connectedSpace_affineSpaceWithDoubledZero (k : Type u) [Field k] (n : ℕ) (hn : 0 < n) :
    ConnectedSpace (affineSpaceWithDoubledZero k n)

AlgebraicGeometry.chartSwapNegationData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/UniversalHomeomorphismEtaleFailure.lean, line 384. The attribute's comment: “a construction input only: the involution of Y of the remark's alternative route, negating the coordinate and swapping the two charts. That the induced action of {+1,-1} is free and that X is its quotient are NOT asserted”.

Stacks 05ZI, the alternative construction. The endomorphism of affine space with doubled origin which negates the coordinates and swaps the two charts, packaged with its restriction to each chart.

The two chart maps agree over the overlap of the charts because negation preserves the complement of the origin, so AlgebraicGeometry.comp_chartInclusion_eq applies.

noncomputable def chartSwapNegationData (k : Type u) [Field k] (n : ℕ) :
    { f : affineSpaceWithDoubledZero k n ⟶ affineSpaceWithDoubledZero k n //
      chartInclusion k n 0 ≫ f = negAffineSpace k n ≫ chartInclusion k n 1 ∧
        chartInclusion k n 1 ≫ f = negAffineSpace k n ≫ chartInclusion k n 0 }

AlgebraicGeometry.chartSwapNegation_comp_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/UniversalHomeomorphismEtaleFailure.lean, line 441. The attribute's comment: “a construction input only: that involution is an involution”.

Stacks 05ZI, the alternative construction. Negating the coordinates and swapping the two charts of affine space with doubled origin is an involution, so it makes the group of order two act on that scheme.

theorem chartSwapNegation_comp_self (k : Type u) [Field k] (n : ℕ) :
    chartSwapNegation k n ≫ chartSwapNegation k n = 𝟙 _

AlgebraicGeometry.AffineLineInvolution.isPullback_chartPairToDoubledLine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DoubledLineEtaleCovering/CartesianSquare.lean, line 622. The attribute's comment: “the remark's cartesian square: Y ← Y₁ ⨿ Y₂ over X ← 𝐀¹_k is cartesian”.

Stacks 05ZI: the square of the remark is cartesian. Away from characteristic two a morphism into Y together with a morphism into the chart 𝐀¹_k of Stacks 05Z6 having the same image in X comes from a unique morphism into Y₁ ⨿ Y₂.

Locally on the source the morphism into Y factors through one of the two charts of the doubled line, and there the relation of Stacks 02Z1, being the kernel pair of the chart 𝐀¹_k ⟶ X, supplies the lift through AlgebraicGeometry.AffineLineInvolution.relationToChartPair. The local lifts agree because the two edges of the square are jointly monomorphic, so they glue; and the glued lift is unique for the same reason.

theorem isPullback_chartPairToDoubledLine (hchar : (2 : k) ≠ 0) :
    IsPullback (yoneda.map (chartPairToDoubledLine k B hk))
      (yoneda.map (chartPairToAffineLine k B hk)) (coveringMorphism k B hk)
      (quotientChart k B hk)

AlgebraicGeometry.AffineLineInvolution.nontrivial_connected_finiteEtale_degreeTwo_coveringMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DoubledLineEtaleCovering/FiniteEtaleDegreeTwo.lean, line 397. The attribute's comment: “the remark's covering: Y, the affine line with its origin doubled, is a nontrivial connected finite étale covering of X of degree two”.

Stacks 05ZI. The affine line with its origin doubled is a nontrivial connected finite étale covering of degree two of the algebraic space X = 𝐀¹_k/\{x ∼ -x ∣ x ≠ 0\} of Stacks 05Z6: the morphism Y ⟶ X of the remark is representable and finite locally free of degree two, it is étale, Y is a connected scheme, and Y ⟶ X admits no section.

The remark states this for k algebraically closed of characteristic zero; invertibility of two in the ground field is all that is used. Nontriviality is expressed by the absence of a section: a covering which is a finite disjoint union of copies of its base has one, so a covering without one is not such a disjoint union.

theorem nontrivial_connected_finiteEtale_degreeTwo_coveringMorphism (hchar : (2 : k) ≠ 0) :
    ((Stacks.Morphisms.IsFiniteLocallyFreeOfRank.property.{u} 2).inverseImage
        (BigFppfOver.toScheme B (Spec (.of k)) hk)).presheaf (coveringMorphism k B hk) ∧
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B (Spec (.of k)) hk)).presheaf (coveringMorphism k B hk) ∧
      ConnectedSpace (doubledLine k).left ∧
      ¬ ∃ s : (involutionQuotient k B hk).obj ⟶ yoneda.obj (doubledLineSite k B hk),
        s ≫ coveringMorphism k B hk = 𝟙 (involutionQuotient k B hk).obj

AlgebraicGeometry.AffineLineInvolution.doubledLine_freeAction_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DoubledLineInvolutionQuotient.lean, line 519. The attribute's comment: “the remark's alternative construction: G = {±1} acts freely on Y, -1 swapping the two charts and negating the coordinate, and X = Y/G in the sense of Spaces, Definition 02Z3”.

Stacks 05ZI, the remark's alternative construction. Away from characteristic two, the affine line with its origin doubled carries an action of the group G = \{+1, -1\} = ℤˣ in which -1 swaps the two charts and negates the coordinate. This action is free in the sense of condition (*) of Stacks 02Z2. The quotient Y/G of Spaces, Definition 02Z3, is an algebraic space, and it is the algebraic space X of Stacks 05Z6: an isomorphism X ≅ Y/G carries the covering Y ⟶ X of the remark to the projection Y ⟶ Y/G.

theorem doubledLine_freeAction_quotient (hchar : (2 : k) ≠ 0)
    [HasSheafify (BigFppfOver.topology B (Spec (.of k)) hk) (Type u)] :
    (∀ b : Bool, doubledChartHom k B hk b ≫ doubledLineInvolution k B hk =
        chartNeg k B hk ≫ doubledChartHom k B hk (!b)) ∧
      (doubledLineAction k B hk (-1)).asIso.hom =
        (Over.post B.inclusion).map (doubledLineInvolution k B hk) ∧
      Space.ActsNontriviallyOnFixedResidueFields
        (Space.underlyingOver B hk (doubledLineSite k B hk)) ℤˣ (doubledLineAction k B hk) ∧
      IsAlgebraicSpace B (Spec (.of k)) hk
        (Space.actionQuotient ℤˣ B hk (doubledLineSite k B hk) (doubledLineAction k B hk)) ∧
      ∃ e : (involutionQuotient k B hk).obj ≅
          Space.actionQuotient ℤˣ B hk (doubledLineSite k B hk) (doubledLineAction k B hk),
        coveringMorphism k B hk ≫ e.hom =
          Stacks.Groupoids.quotientChart (BigFppfOver.topology B (Spec (.of k)) hk)
            (Over.post B.inclusion) (doubledLineSite k B hk)
            (Space.actionRelation (Space.underlyingOver B hk (doubledLineSite k B hk)) ℤˣ
              (doubledLineAction k B hk))

AlgebraicGeometry.AffineLineInvolution.squaringMap_universalHomeomorphism_not_representable_not_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/SquaringMapEtaleSiteFailure.lean, line 383. The attribute's comment: “the remark's two assertions: X ⟶ 𝐀¹_k is a universal homeomorphism which is not representable, and base change along it is not an equivalence of spaces-étale sites (it is not essentially surjective), so Theorem 05ZH fails for universal homeomorphisms”.

Stacks 05ZI. Let k be an algebraically closed field of characteristic zero and let 𝐀¹_k ⟶ X ⟶ 𝐀¹_k be as in Stacks 05Z6, with X ⟶ 𝐀¹_k the morphism descended from squaring the coordinate. Then:

1. X and 𝐀¹_k are algebraic spaces and X ⟶ 𝐀¹_k is a universal homeomorphism;
2. it is not representable: a universal homeomorphism of algebraic spaces need not be representable;
3. base change V ↦ V ×_{𝐀¹_k} X from the spaces-étale site of 𝐀¹_k to that of X is not essentially surjective;
4. hence it is not an equivalence, so Theorem 05ZH fails for universal homeomorphisms.

The functor is AlgebraicGeometry.Space.spacesBaseChange, the one Stacks 05ZH is stated for. Only 2 ≠ 0 in k is used. The general statements are AlgebraicGeometry.AffineLineInvolution.not_relativelyRepresentable_squaringMap and AlgebraicGeometry.AffineLineInvolution.not_essSurj_spacesBaseChange_squaringMap. The proof of (3) does not use that 𝐀¹_k has no nontrivial connected finite étale covering. It shows directly that the doubled-origin covering of the remark is not a base change.

theorem squaringMap_universalHomeomorphism_not_representable_not_isEquivalence
    [IsAlgClosed k] [CharZero k] :
    IsAlgebraicSpace B (Spec (.of k)) hk (involutionQuotient k B hk).obj ∧
      IsAlgebraicSpace B (Spec (.of k)) hk
        (Stacks.Groupoids.points (Over.post (X := B.obj hk) B.inclusion) (affineLine k)) ∧
      Space.UniversalHomeomorphism B (Spec (.of k)) hk (squaringMap k B hk) ∧
      ¬ yoneda.relativelyRepresentable (squaringMap k B hk) ∧
      ¬ (Space.spacesBaseChange B (Spec (.of k)) hk
          (squaringSpaceHom k B hk two_ne_zero)).functor.EssSurj ∧
      ¬ (Space.spacesBaseChange B (Spec (.of k)) hk
          (squaringSpaceHom k B hk two_ne_zero)).functor.IsEquivalence

Sources

• Section 76.8, Tag 05ZG
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isEquivalence_spacesBaseChange_of_isIntegralHom_of_universallyInjective · AlgebraicGeometry.Space.essSurj_spacesBaseChange_of_isFirstOrderThickening · AlgebraicGeometry.Space.isEquivalence_spacesBaseChange_of_isFirstOrderThickening · AlgebraicGeometry.Space.essSurj_spacesBaseChange_of_isThickening · AlgebraicGeometry.Space.isEquivalence_spacesBaseChange_of_isThickening · AlgebraicGeometry.Space.faithful_spacesBaseChange_of_isSurjective · AlgebraicGeometry.Space.faithful_spacesBaseChange_of_isThickening · AlgebraicGeometry.Space.full_spacesBaseChange_of_isThickening

Section76.9 Thickenings#

Section 76.9 of the Stacks Project, Tag 05ZJ. 13 tags here are carried by 60 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05ZJ, the section

Tag 05ZJ in the Stacks Project.

AlgebraicGeometry.Space.exists_sieve_isNilpotent_of_mem_definingIdealAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LocallyNilpotentIdeal.lean, line 72. The attribute's comment: “any local section of the kernel I = Ker(i_X^#) of a thickening i_X : X -> X' is locally nilpotent (the paragraph after Lemma 05ZP), on the small etale site of X'”.

Section 05ZJ: the ideal of a thickening is locally nilpotent. Let G ⊂ X be a thickening of algebraic spaces over S, with ideal sheaf 𝓘 = Ker(i^♯) ⊆ 𝒪_X on the small étale site of X. Every local section s of 𝓘, over an arbitrary étale chart U of X, is locally nilpotent: there is a covering sieve of U along each of whose arrows the restriction of s is nilpotent.

The covering sieve is that of the arrows factoring through an affine étale chart, which covers by Stacks 04JS; on an affine chart the section is nilpotent by AlgebraicGeometry.Space.isNilpotent_of_mem_definingIdealAt_of_isThickening.

theorem exists_sieve_isNilpotent_of_mem_definingIdealAt (hG : IsThickening B S hS X G)
    (U : SmallEtale B S hS X.1)
    (s : ToType ((structureRingSheaf B S hS X).obj.obj (op U)))
    (hs : s ∈ definingIdealAt B S hS X ⟨G, hG.1⟩ (op U)) :
    ∃ T : Sieve U, T ∈ SmallEtale.topology B S hS X.1 U ∧
      ∀ (V : SmallEtale B S hS X.1) (m : V ⟶ U), T m →
        IsNilpotent (((structureRingSheaf B S hS X).obj.map m.op).hom s)

AlgebraicGeometry.Space.thickeningHom_structureSharp_compatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismStructureSquare.lean, line 95. The attribute's comment: “the paragraph on a morphism (f, f') : (X ⊂ X') -> (Y ⊂ Y') of thickenings over B: the vertical arrows of the square of etale topoi are equivalences, and (f')^# : f^{-1}O_{Y'} -> O_{X'} is a map of O_B-algebras fitting into the commutative square with f^#, i_X^# and i_Y^#, read as 2-isomorphisms of morphisms of small etale ringed topoi (the form of the hypotheses of Lemma 05ZN); (f')_small is moreover locally ringed”.

Section 05ZJ: the structure map of a morphism of thickenings over a base. Let G ⊂ X' and H ⊂ Y' be thickenings of algebraic spaces over T (structure morphisms pX', pY'), and let (f, f') be a morphism of thickenings over T: f : G ⟶ H, f' : X' ⟶ Y', f' ∘ i_X = i_Y ∘ f and pY' ∘ f' = pX'. Then

1. the direct images along i_X and i_Y of the small étale topoi are equivalences (the vertical arrows of the source's square of topoi);
2. (f')_small is a morphism of locally ringed topoi;
3. (f')^♯ fits into the source's commuting square with f^♯, i_X^♯ and i_Y^♯: (f')_small ∘ (i_X)_small is 2-isomorphic to (i_Y ∘ f)_small;
4. (f')^♯ is a map of 𝒪_T-algebras: (p_{Y'})_small ∘ (f')_small is 2-isomorphic to (p_{X'})_small.

Clauses 3 and 4 are the hypotheses hsquare and halgebra, and clause 2 the hypothesis hlocal, of AlgebraicGeometry.Space.existsUnique_thickeningHom_of_isLocallyRinged at Φ = (f')_small.

theorem thickeningHom_structureSharp_compatible (hG : IsThickening B S hS X' G)
    (hH : IsThickening B S hS Y' H) (pX' : X' ⟶ T) (pY' : Y' ⟶ T)
    (f : IsThickening.space B S hS hG ⟶ IsThickening.space B S hS hH) (f' : X' ⟶ Y')
    (hsq : IsThickening.inclusion B S hS hG ≫ f' = f ≫ IsThickening.inclusion B S hS hH)
    (hT : f' ≫ pY' = pX') :
    (smallToposMorphismTypeU B S hS
        (IsThickening.inclusion B S hS hG)).pushforward.IsEquivalence ∧
      (smallToposMorphismTypeU B S hS
        (IsThickening.inclusion B S hS hH)).pushforward.IsEquivalence ∧
      (smallEtaleRingedToposHom B S hS f').IsLocallyRinged ∧
      Nonempty (SmallEtaleTwoIso B S hS
        (smallEtaleComp B S hS (smallEtaleRingedToposHom B S hS f')
          (smallEtaleRingedToposHom B S hS (IsThickening.inclusion B S hS hG)))
        (smallEtaleRingedToposHom B S hS (f ≫ IsThickening.inclusion B S hS hH))) ∧
      Nonempty (SmallEtaleTwoIso B S hS
        (smallEtaleComp B S hS (smallEtaleRingedToposHom B S hS pY')
          (smallEtaleRingedToposHom B S hS f'))
        (smallEtaleRingedToposHom B S hS pX'))

AlgebraicGeometry.Space.exists_idealPow_firstOrderThickening_filtration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/OrderFiltration.lean, line 201. The attribute's comment: “the paragraph after Lemma 05ZP: for an nth order thickening X ⊂ X' with ideal I, the filtration 0 = I^{n+1} ⊂ I^n ⊂ ... ⊂ I ⊂ O_{X'} gives closed subspaces X = X_0 ⊂ X_1 ⊂ ... ⊂ X_n = X', X_k cut out by I^{k+1}, with each X_k ⊂ X_{k+1} a first order thickening (the source's X_{n+1} = X' is a misprint for X_n = X')”.

Section 05ZJ: an nth order thickening is filtered by first order thickenings. Let X ⊂ X' be an nth order thickening of algebraic spaces over S, with quasi-coherent ideal sheaf 𝓘 ⊆ 𝒪_{X'}. There are closed subspaces X_0, X_1, … of X', the kth one cut out by 𝓘^{k+1} (so the filtration 0 = 𝓘^{n+1} ⊂ 𝓘^n ⊂ ⋯ ⊂ 𝓘 ⊂ 𝒪_{X'} is that of their ideal sheaves), with X = X_0 ⊂ X_1 ⊂ ⋯ ⊂ X_n = X', such that every X_k ⊂ X_{k+1} is a first order thickening.

theorem exists_idealPow_firstOrderThickening_filtration {n : ℕ} {G : Subfunctor X.1}
    (hG : IsNthOrderThickening B S hS n X G) :
    ∃ Xs : ℕ → ClosedSubspaces B S hS X.1,
      (Xs 0).1 = G ∧ (Xs n).1 = ⊤ ∧ Monotone (fun k => (Xs k).1) ∧
      (∀ k, definingIdealSheaf B S hS X (Xs k) =
        idealPowSubmodule (definingIdealSheaf B S hS X ⟨G, hG.1.1⟩) (k + 1)
          (SheafOfModules.unit (structureRingSheaf B S hS X))) ∧
      ∀ k, IsFirstOrderThickening B S hS ⟨(Xs (k + 1)).1.toFunctor, (Xs (k + 1)).2.1⟩
        ((Xs k).1.preimage (Xs (k + 1)).1.ι)

Declarations registered for the tag:

• AlgebraicGeometry.Space.isLocallySurjective_structureSharpInverseImage, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LocallyNilpotentIdeal.lean, line 96 (StacksFrontier): “the sentence after Equation 05ZM: the closed immersion i_X : X -> X' corresponds to the surjective map i_X^# : O_{X'} -> O_X, read on the small etale site of X as i_X^{-1}O_{X'} -> O_X (stated for every closed immersion)”.
• AlgebraicGeometry.Space.isIntegralHom_universallyInjective_isSurjective_ι_of_isThickening, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismStructureSquare.lean, line 121 (StacksFrontier): “the sentence opening 'The fundamental equivalence': if X ⊂ X' is a thickening, then X -> X' is integral and universally bijective (universally injective and surjective)”.

Tag 05ZK, a definition

Tag 05ZK in the Stacks Project.

AlgebraicGeometry.Space.IsThickening, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings.lean, line 95. The attribute's comment: “part (1): thickening”.

Stacks 05ZK, part (1). A closed subspace G of an algebraic space X over S is a thickening of X when the two have the same associated topological space, i.e. when the map on points induced by the closed immersion G.ι is surjective.

abbrev IsThickening (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X : AlgebraicSpaces B S hS) (G : Subfunctor X.1) : Prop

AlgebraicGeometry.Space.IsMorphismOfThickenings, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings.lean, line 126. The attribute's comment: “part (5): morphism of thickenings”.

Stacks 05ZK, part (5). Given two thickenings G ⊂ X' and H ⊂ Y' of algebraic spaces over S, a morphism of thickenings is a morphism f' : X' ⟶ Y' with f'(G) ⊂ H, i.e. one whose restriction to G factors through the closed subspace H.

The restriction f = f'|_G : G ⟶ H is AlgebraicGeometry.Space.IsMorphismOfThickenings.restrict, and the pair (f, f') is what the source calls the morphism of thickenings (G ⊂ X') → (H ⊂ Y').

abbrev IsMorphismOfThickenings {X' Y' : AlgebraicSpaces B S hS} (G : Subfunctor X'.1)
    (H : Subfunctor Y'.1) (f' : X' ⟶ Y') : Prop

AlgebraicGeometry.Space.IsThickeningOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings.lean, line 190. The attribute's comment: “part (6): thickening over a base”.

Stacks 05ZK, part (6). A thickening over an algebraic space Z: a thickening G ⊂ X' of algebraic spaces over S together with structure morphisms a' : X' ⟶ Z of the ambient space and a : G ⟶ Z of the subspace, such that the closed immersion G ⟶ X' is a morphism over Z.

abbrev IsThickeningOver (Z : AlgebraicSpaces B S hS) {X' : AlgebraicSpaces B S hS}
    (G : Subfunctor X'.1) (a : G.toFunctor ⟶ Z.1) (a' : X' ⟶ Z) : Prop

AlgebraicGeometry.Space.IsMorphismOfThickeningsOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings.lean, line 198. The attribute's comment: “part (6): morphism of thickenings over a base”.

Stacks 05ZK, part (6). A morphism of thickenings over an algebraic space Z: two thickenings over Z and a morphism of thickenings between them which is a morphism over Z.

abbrev IsMorphismOfThickeningsOver (Z : AlgebraicSpaces B S hS)
    {X' Y' : AlgebraicSpaces B S hS} (G : Subfunctor X'.1) (H : Subfunctor Y'.1)
    (a : G.toFunctor ⟶ Z.1) (a' : X' ⟶ Z) (b : H.toFunctor ⟶ Z.1) (b' : Y' ⟶ Z)
    (f' : X' ⟶ Y') : Prop

AlgebraicGeometry.Space.isThickening_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftDifferenceUndeformedTarget.lean, line 71. The attribute's comment: “part (1): an algebraic space is a thickening of itself”.

An algebraic space is a thickening of itself: its top closed subspace.

theorem isThickening_top (Y : AlgebraicSpaces B S hS) : IsThickening B S hS Y ⊤

AlgebraicGeometry.Space.IsNthOrderThickening, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/Order.lean, line 127. The attribute's comment: “part (4): nth-order thickening”.

Stacks 05ZK, part (4). A closed subspace G of an algebraic space X over S is an nth-order thickening when the (n+1)st power of its defining ideal vanishes on every object of the small étale site of X.

abbrev IsNthOrderThickening (n : ℕ) (X : AlgebraicSpaces B S hS) (G : Subfunctor X.1) : Prop

AlgebraicGeometry.Space.IsFirstOrderThickening, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/Order.lean, line 135. The attribute's comment: “part (2): first-order thickening”.

Stacks 05ZK, part (2). A closed subspace G of an algebraic space X over S is a first-order thickening when its defining ideal has square zero on every object of the small étale site of X.

abbrev IsFirstOrderThickening (X : AlgebraicSpaces B S hS) (G : Subfunctor X.1) : Prop

AlgebraicGeometry.Space.IsFiniteOrderThickening, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/Order.lean, line 142. The attribute's comment: “part (3): finite-order thickening”.

Stacks 05ZK, part (3). A closed subspace G of an algebraic space X over S is a finite-order thickening when its defining ideal is nilpotent, with one exponent valid on every object of the small étale site of X.

abbrev IsFiniteOrderThickening (X : AlgebraicSpaces B S hS) (G : Subfunctor X.1) : Prop

Declarations registered for the tag:

• CategoryTheory.Arrow.Hom registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings.lean, line 100 (StacksFrontier): “parts (5) and (6): morphisms of thickenings, also over a base”.

Tag 05ZL, an equation

Tag 05ZL in the Stacks Project.

AlgebraicGeometry.Space.isIntegralHom_universallyInjective_isSurjective_ι_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/EtaleSite.lean, line 127. The attribute's comment: “the inclusion of a thickening is integral, universally injective and surjective”.

Stacks 05ZL. The inclusion of a thickening of an algebraic space over S is integral, universally injective and surjective.

theorem isIntegralHom_universallyInjective_isSurjective_ι_of_isThickening
    (hG : IsThickening B S hS X G) :
    IsIntegralHom B S hS G.ι ∧ UniversallyInjective B S hS G.ι ∧ IsSurjective B S hS G.ι

AlgebraicGeometry.Space.spacesEtaleAbelianSheafEquiv_of_isThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/EtaleToposAbelian.lean, line 101. The attribute's comment: “the identification of the two spaces-etale topoi, at sheaves of abelian groups”.

Equation [Stacks Project, Tag 05ZL] for sheaves of abelian groups. For a thickening G ⊂ X of algebraic spaces over S, the sheaves of abelian groups on the spaces-étale site of X and those on the spaces-étale site of G are canonically equivalent.

The equivalence is the chart form AlgebraicGeometry.Space.smallEtaleAbelianSheafEquiv_of_isThickening conjugated by the two comparison equivalences of [Stacks Project, Tag 03G1], exactly as the set-valued AlgebraicGeometry.Space.spacesEtaleSheafEquiv_of_isThickening is.

noncomputable def spacesEtaleAbelianSheafEquiv_of_isThickening (hG : IsThickening B S hS X G) :
    Sheaf (SpacesEtale.topology B S hS X) AddCommGrpCat.{u + 1} ≌
      Sheaf (SpacesEtale.topology B S hS (IsThickening.space B S hS hG))
        AddCommGrpCat.{u + 1}

AlgebraicGeometry.Space.mem_spacesEtaleTopology_iff_functorPushforward_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleCovering.lean, line 121. The attribute's comment: “identification of the covering sieves of the two spaces-étale sites”.

Stacks 05ZL. Base change along the inclusion of a thickening G ⊂ X identifies the covering sieves of the spaces-étale site of X with those of the spaces-étale site of G: a sieve of an object U is covering exactly when the sieve it generates on the base change of U is covering.

theorem mem_spacesEtaleTopology_iff_functorPushforward_of_isThickening
    {X : AlgebraicSpaces B S hS} {G : Subfunctor X.1} (hG : IsThickening B S hS X G)
    (U : SpacesEtale B S hS X) (R : Sieve U) :
    R ∈ SpacesEtale.topology B S hS X U ↔
      R.functorPushforward
          (spacesBaseChange B S hS (IsThickening.inclusion B S hS hG)).functor ∈
        SpacesEtale.topology B S hS (IsThickening.space B S hS hG)
          ((spacesBaseChange B S hS (IsThickening.inclusion B S hS hG)).functor.obj U)

AlgebraicGeometry.Space.spacesEtaleEquivalenceOfIsThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleEquivalence.lean, line 152. The attribute's comment: “the identification of the two spaces-étale sites of Stacks 03G0, as an equivalence of categories, for a thickening of arbitrary order”.

Let G ⊂ X be a thickening of algebraic spaces over S, of arbitrary order. Base change along the inclusion, V ↦ G ×_X V, is an equivalence of categories from the spaces-étale site of the ambient space X to the spaces-étale site of the closed subspace G.

noncomputable def spacesEtaleEquivalenceOfIsThickening (hG : IsThickening B S hS X G) :
    SpacesEtale B S hS X ≌ SpacesEtale B S hS (IsThickening.space B S hS hG)

AlgebraicGeometry.Space.isEquivalence_spacesBaseChange_of_isClosedImmersion_of_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleEssSurj/LiftedEtalePresentation.lean, line 576. The attribute's comment: “the identification of the two spaces-étale sites: base change along the inclusion of a thickening of arbitrary order is an equivalence of categories”.

Base change V ↦ X ×_Y V is an equivalence from the spaces-étale site of Y to that of X, for a surjective closed immersion f.

theorem isEquivalence_spacesBaseChange_of_isClosedImmersion_of_isSurjective (f : X ⟶ Y)
    (hci : IsClosedImmersion B S hS f.hom) (hsurj : IsSurjective B S hS f.hom) :
    (spacesBaseChange B S hS f).functor.IsEquivalence

Tag 05ZM, an equation

Tag 05ZM in the Stacks Project.

AlgebraicGeometry.Space.spacesEtaleRingSheafEquiv_of_isThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/EtaleRingedTopos.lean, line 227. The attribute's comment: “the equivalence of the two spaces-étale topoi at sheaves of commutative rings, which is what carries the structure sheaf of the ambient space to the right hand side of the equation; neither pair is claimed to be a locally ringed topos”.

The fundamental equivalence of a thickening, at sheaves of rings. For a thickening G ⊂ X of algebraic spaces the sheaves of commutative rings on the spaces-étale site of X and those on the spaces-étale site of G are canonically equivalent.

def spacesEtaleRingSheafEquiv_of_isThickening (hG : IsThickening B S hS X G) :
    Sheaf (SpacesEtale.topology B S hS X) CommRingCat.{u + 1} ≌
      Sheaf (SpacesEtale.topology B S hS (IsThickening.space B S hS hG))
        CommRingCat.{u + 1}

AlgebraicGeometry.Space.thickeningStructureSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/EtaleRingedTopos.lean, line 246. The attribute's comment: “the sheaf of rings O_{X'} of the right hand side of the equation, the structure sheaf of the ambient space read on the spaces-étale site of the thickening”.

The structure sheaf of the ambient space, on the site of the thickening. For a thickening G ⊂ X this is 𝒪_X carried through the equivalence of the two spaces-étale topoi, the sheaf of rings of the right hand side of the fundamental equivalence.

def thickeningStructureSheaf (hG : IsThickening B S hS X G) :
    Sheaf (SpacesEtale.topology B S hS (IsThickening.space B S hS hG)) CommRingCat.{u + 1}

AlgebraicGeometry.Space.thickeningInverseImageRingedTopos, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/EtaleRingedTopos.lean, line 323. The attribute's comment: “the right hand pair of the equation, in the presentation of scheme charts and with the structure sheaf of the ambient space read on the smaller site as its inverse image”.

The right hand side (Sh(G_étale), 𝒪_X) of the fundamental equivalence of a thickening. The small étale site of scheme charts of the closed subspace G of a thickening G ⊂ X, equipped with the structure sheaf of the ambient space X read on it as the inverse image i^{-1}𝒪_X along the inclusion.

This is the inverse-image ringed topos of Stacks 04KR at the morphism of small étale topoi of the inclusion. Its structure sheaf is not 𝒪_G: the two are related by the surjection i^♯ : i^{-1}𝒪_X ⟶ 𝒪_G, whose kernel is the conormal module of the thickening when the thickening is of first order.

abbrev thickeningInverseImageRingedTopos (hG : IsThickening B S hS X G) :
    RingedTopos.{u, u + 1, u}

AlgebraicGeometry.Space.thickeningFundamentalHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/EtaleRingedTopos.lean, line 345. The attribute's comment: “the canonical morphism between the two pairs of the equation, in the presentation of scheme charts: its geometric morphism is the direct image along the inclusion, and its structure map is the unit of the adjunction at the ambient structure sheaf”.

The canonical morphism of the fundamental equivalence of a thickening. Its underlying geometric morphism is the direct image along the inclusion i : G ⟶ X, and its structure map is the unit 𝒪_X ⟶ i_*i^{-1}𝒪_X of the adjunction i^{-1} ⊣ i_* on sheaves of commutative rings.

Both of the equation's claims about it are below: AlgebraicGeometry.Space.isIso_thickeningFundamentalHom_fSharp is that the structure map is an isomorphism, and AlgebraicGeometry.Space.isEquivalence_smallEtalePushforward_of_isThickening is that the geometric morphism is an equivalence — the latter is stated at the geometric morphism itself, which is this morphism's toToposHom by AlgebraicGeometry.inverseImageRingedToposHom_toToposHom, so it supplies that instance after an ascription at this spelling, as in AlgebraicGeometry.Space.thickeningFundamentalHomInverse below.

def thickeningFundamentalHom (hG : IsThickening B S hS X G) :
    RingedToposHom (thickeningInverseImageRingedTopos B S hS hG)
      (smallEtaleRingedTopos B S hS X)

AlgebraicGeometry.Space.isIso_thickeningFundamentalHom_fSharp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/EtaleRingedTopos.lean, line 365. The attribute's comment: “the structure-sheaf half: the structure map of the canonical morphism between the two pairs is an isomorphism, so both pairs carry the structure sheaf of the ambient space”.

The structure-sheaf half of Stacks 05ZM. The structure map of the canonical morphism — the unit 𝒪_X ⟶ i_*i^{-1}𝒪_X at the structure sheaf of the ambient space of a thickening — is an isomorphism of sheaves of commutative rings. So the two pairs of the equation carry one and the same structure sheaf, and not merely equivalent topoi.

The direct image of sheaves of sets along the inclusion is fully faithful and essentially surjective, so the set-level unit is invertible at every sheaf; forgetting the ring operations carries the unit of the adjunction on sheaves of commutative rings to the set-level unit, and reflects isomorphisms. The same statement for sheaves of not necessarily commutative rings is AlgebraicGeometry.Space.isIso_ringUnit_of_isThickening.

theorem isIso_thickeningFundamentalHom_fSharp (hG : IsThickening B S hS X G) :
    IsIso (thickeningFundamentalHom B S hS hG).fSharp

AlgebraicGeometry.Space.thickeningFundamentalHom_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/EtaleRingedTopos.lean, line 404. The attribute's comment: “that the canonical morphism between the two pairs is a morphism of LOCALLY ringed topoi, which is the clause the equation adds to the equivalence of the two topoi; that either pair is a locally ringed SITE is not claimed”.

The canonical morphism of the fundamental equivalence is a morphism of locally ringed topoi. This is the clause that makes the equation of Stacks 05ZM an equivalence of locally ringed topoi and not only of ringed topoi.

It needs no hypothesis on the thickening: the inverse-image form of the structure map of the canonical morphism out of an inverse-image ringed topos is the identity, and a morphism of ringed topoi whose inverse-image structure map is invertible is locally ringed, which is the step Stacks 04H9 settles with the words "as it is an isomorphism this is clear". The thickening hypothesis is what makes the morphism invertible, through AlgebraicGeometry.Space.isIso_thickeningFundamentalHom_fSharp and AlgebraicGeometry.Space.isEquivalence_smallEtalePushforward_of_isThickening.

That the two ringed topoi are locally ringed sites is a different assertion, and is not claimed; see the implementation notes.

theorem thickeningFundamentalHom_isLocallyRinged (hG : IsThickening B S hS X G) :
    (thickeningFundamentalHom B S hS hG).IsLocallyRinged

AlgebraicGeometry.Space.thickeningFundamentalHomInverse, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/EtaleRingedTopos.lean, line 420. The attribute's comment: “that the canonical morphism between the two pairs is invertible as a morphism of ringed topoi, which is the word equivalence in the equation”.

The inverse of the canonical morphism of the fundamental equivalence of a thickening. The geometric morphism is i^{-1} read as a direct image, and the structure map is the inverse of the inverse-image form i^{-1}𝒪_X ⟶ i^{-1}𝒪_X of the structure map of AlgebraicGeometry.Space.thickeningFundamentalHom.

Its existence is the content of the word equivalence in the equation of Stacks 05ZM: the canonical morphism is invertible because its geometric morphism is an equivalence of topoi and its structure map is an isomorphism of sheaves of rings.

def thickeningFundamentalHomInverse (hG : IsThickening B S hS X G) :
    RingedToposHom (smallEtaleRingedTopos B S hS X)
      (thickeningInverseImageRingedTopos B S hS hG)

AlgebraicGeometry.Space.thickeningFundamentalHomInverse_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/EtaleRingedTopos.lean, line 439. The attribute's comment: “that the inverse of the canonical morphism is again a morphism of LOCALLY ringed topoi, so that the equation is an equivalence of locally ringed topoi in both directions”.

The inverse of the canonical morphism is again a morphism of locally ringed topoi. Together with AlgebraicGeometry.Space.thickeningFundamentalHom_isLocallyRinged this is the equation of Stacks 05ZM in full: an invertible morphism of locally ringed topoi between the two pairs, in both directions.

The inverse is an isomorphism of ringed topoi — its geometric morphism is the inverse image of an equivalence and its structure map is the inverse of an isomorphism — and an isomorphism of ringed topoi is locally ringed by Stacks 04H9.

theorem thickeningFundamentalHomInverse_isLocallyRinged (hG : IsThickening B S hS X G) :
    (thickeningFundamentalHomInverse B S hS hG).IsLocallyRinged

AlgebraicGeometry.Space.spacesEtaleSheafEquiv_of_isThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/EtaleTopos.lean, line 303. The attribute's comment: “equivalence of the spaces-étale sheaf topoi”.

The equivalence of the spaces-étale sheaf topoi of a thickening. For a thickening G ⊂ X of algebraic spaces over S, the sheaves of sets on the spaces-étale site of X and the sheaves of sets on the spaces-étale site of G are canonically equivalent.

The equivalence is the chart form AlgebraicGeometry.Space.smallEtaleSheafEquiv_of_isThickening conjugated by the two comparison equivalences of Stacks 03G1, AlgebraicGeometry.Space.comparisonFunctor_sheafEquivalence, which identify the sheaves on the spaces-étale site of an algebraic space with the sheaves on its small étale site of scheme charts.

noncomputable def spacesEtaleSheafEquiv_of_isThickening (hG : IsThickening B S hS X G) :
    Sheaf (SpacesEtale.topology B S hS X) (Type (u + 1)) ≌
      Sheaf (SpacesEtale.topology B S hS (IsThickening.space B S hS hG)) (Type (u + 1))

AlgebraicGeometry.Space.fundamentalEquivalence_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FundamentalEquivalence.lean, line 221.

Stacks 05ZM, equation 76.9.1.2. Let G ⊂ X be a thickening of algebraic spaces over a scheme S; in the notation of the source G is X and X is X'. Then

(Sh(X'_{spaces,étale}), 𝒪_{X'}) ≅ (Sh(X_{spaces,étale}), 𝒪_{X'})

as locally ringed topoi, the right-hand structure sheaf being 𝒪_{X'} transported along the equivalence of spaces-étale topoi. The isomorphism is the canonical morphism AlgebraicGeometry.Space.spacesEtaleRingedToposHom_of_isThickening, and the four conjuncts below are what make it one: its geometric morphism is an equivalence in both directions, its structure map is invertible, and it is a morphism of locally ringed topoi.

theorem fundamentalEquivalence_of_isThickening (hG : IsThickening B S hS X G) :
    Functor.IsEquivalence
        (spacesEtaleRingedToposHom_of_isThickening B S hS hG).toToposHom.pushforward ∧
      Functor.IsEquivalence
        (spacesEtaleRingedToposHom_of_isThickening B S hS hG).toToposHom.inverseImage ∧
      IsIso (spacesEtaleRingedToposHom_of_isThickening B S hS hG).fSharp ∧
      RingedToposHom.IsLocallyRinged
        (spacesEtaleRingedToposHom_of_isThickening B S hS hG)

AlgebraicGeometry.Space.structureRingSheafDirectImageIsoOfRestrictEq, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/StructureSheafEquivalence.lean, line 325. The attribute's comment: “the structure sheaf transported across the equivalence of étale topoi of a thickening: the direct image of the structure sheaf of the ambient space depends only on the restriction of the morphism to the closed subspace”.

The structure-sheaf half of [Stacks Project, Tag 05ZM]. Let G ⊂ X' be a thickening of algebraic spaces over S, with inclusion i : X ⟶ X', and let a', b' : X' ⟶ Y' be two morphisms which agree on X. Then the two direct images (a')_*𝒪_{X'} and (b')_*𝒪_{X'} of the structure sheaf of X' are canonically isomorphic as sheaves of rings on the small étale site of Y'.

This is the sense in which the structure sheaf of X' is carried across the equivalence of étale topoi of the thickening: the direct image of 𝒪_{X'} depends only on the restriction of the morphism to the closed subspace, because the direct image of sheaves of sets does and the ring operations are transported along it.

It is what lets the structure maps (a')^♯ and (b')^♯ be compared, and so what [Stacks Project, Tag 0618] needs in order to speak of the difference of two lifts; see AlgebraicGeometry.Space.structureSharpOfRestrictEq.

noncomputable def structureRingSheafDirectImageIsoOfRestrictEq :
    structureRingSheafDirectImage B S hS a' ≅ structureRingSheafDirectImage B S hS b'

AlgebraicGeometry.Space.pushforwardCommRingFunctorIsoOfRestrictEq, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/StructureSheafEquivalence.lean, line 337. The attribute's comment: “the structure sheaf transported across the equivalence of étale topoi of a thickening, for sheaves of commutative rings: the direct image functor of sheaves of commutative rings depends only on the restriction of the morphism to the closed subspace”.

The structure-sheaf half of [Stacks Project, Tag 05ZM] for sheaves of commutative rings. This is the spelling in which the structure map fSharp of AlgebraicGeometry.Space.smallEtaleRingedToposHom takes its values.

noncomputable def pushforwardCommRingFunctorIsoOfRestrictEq :
    pushforwardCommRingFunctor.{u, u, u, u + 1, u, u + 1}
        (smallToposMorphismTypeU B S hS a') ≅
      pushforwardCommRingFunctor.{u, u, u, u + 1, u, u + 1}
        (smallToposMorphismTypeU B S hS b')

AlgebraicGeometry.Space.isIso_ringUnit_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/StructureSheafRingUnit.lean, line 187. The attribute's comment: “the structure-sheaf half, at the small étale sites: every sheaf of rings on the site of the ambient space — its structure sheaf in particular — is canonically the direct image along the inclusion of a sheaf of rings on the site of the thickening, which is the identification under which the two topoi carry one and the same structure sheaf”.

The unit O ⟶ i_*i^{-1}O of i^{-1} ⊣ i_* at a sheaf of rings is an isomorphism for the inclusion i : Z ⟶ X of a thickening. The direct image of sheaves of sets along i is fully faithful because i is a closed immersion and essentially surjective because Z ⊂ X is a thickening, so the set-level unit is invertible at every sheaf; and CategoryTheory.sheafCompose _ (CategoryTheory.forget RingCat) reflects isomorphisms.

So every sheaf of rings on the small étale site of X is canonically the direct image of one on the small étale site of Z. This is what lets the comorphisms of two morphisms agreeing on a thickening be read in one and the same sheaf of rings; see the module documentation.

theorem isIso_ringUnit_of_isThickening (hZ : IsThickening B S hS X Z.1)
    (O : Sheaf (SmallEtale.topology B S hS X.1) RingCat.{u}) :
    IsIso (ringUnit (smallToposMorphismTypeU B S hS (subspaceInclusion B S hS X Z)) O)

AlgebraicGeometry.Space.isIso_commRingUnit_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/StructureSheafRingUnit.lean, line 226. The attribute's comment: “the structure-sheaf half at the coefficient category of a morphism of ringed topoi: the direct image along the inclusion identifies the sheaves of commutative rings on the site of the thickening with those on the site of the ambient space, carrying the inverse image of the structure sheaf of the ambient space to that structure sheaf”.

The unit of the adjunction of [Stacks Project, Tag 00YV] at a sheaf of commutative rings is an isomorphism for the inclusion i : Z ⟶ X of a thickening.

This is AlgebraicGeometry.Space.isIso_ringUnit_of_isThickening at the coefficient category in which AlgebraicGeometry.RingedToposHom.fSharp takes its values, and the proof is the same: the direct image of sheaves of sets along a thickening is fully faithful and essentially surjective, Stacks.Sheaves.ToposPushforward.pushforwardCommRingFunctor_isEquivalence carries that to the direct image of sheaves of commutative rings, and the unit of an adjunction whose right adjoint is an equivalence is an isomorphism.

Stated at CommRingCat the identification applies to a morphism of ringed topoi: the invertibility of a structure map is the hypothesis [IsIso f.fSharp] of AlgebraicGeometry.RingedToposHom.inverse, and AlgebraicGeometry.RingedToposHom.ofInverseImageIso builds a morphism of ringed topoi out of a morphism of topoi together with an isomorphism of inverse-image structure sheaves.

theorem isIso_commRingUnit_of_isThickening (hZ : IsThickening B S hS X Z.1)
    (O : Sheaf (SmallEtale.topology B S hS X.1) CommRingCat.{u}) :
    IsIso ((commRingImageAdjunction
      (smallToposMorphismTypeU B S hS (subspaceInclusion B S hS X Z))).unit.app O)

AlgebraicGeometry.Space.smallEtaleCommRingSheafEquiv_of_isThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/StructureSheafTransport.lean, line 106. The attribute's comment: “equivalence of the small étale sheaves of commutative rings”.

Stacks 05ZM for sheaves of commutative rings. For a thickening G ⊂ X of algebraic spaces over S, the sheaves of commutative rings on the small étale site of X and on the small étale site of G are equivalent, by restriction along base change of étale scheme charts.

This is the comparison lemma for the dense subsite inclusion AlgebraicGeometry.Space.thickeningChartBaseChange_isDenseSubsite, instantiated at CommRingCat.{u} rather than at sheaves of sets; see the implementation notes for why that instantiation needs the essential smallness of the site.

noncomputable def smallEtaleCommRingSheafEquiv_of_isThickening (hG : IsThickening B S hS X G) :
    Sheaf (SmallEtale.topology B S hS X.1) CommRingCat.{u} ≌
      Sheaf (SmallEtale.topology B S hS (IsThickening.space B S hS hG).1) CommRingCat.{u}

Tag 05ZN, a lemma

Tag 05ZN in the Stacks Project.

AlgebraicGeometry.Space.eq_of_inducesCommonSmallEtaleRingedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismFromStructureMap/RecoveryAndThickeningHom.lean, line 270. The attribute's comment: “the uniqueness clause of the tag, unconditionally and in the generality in which it is true: at most one morphism X' ⟶ Y' of the ambient algebraic spaces over the base is 2-isomorphic to a given morphism of their small étale ringed topoi, so there is at most one morphism of thickenings (f, f') with alpha = (f')^sharp. This is the faithfulness half of 04KL over a base and it is PROVED, by 04M6; no thickening hypothesis and no 2-compatibility with the base is used”.

A morphism of algebraic spaces is determined by the morphism of small étale ringed topoi it induces. At most one morphism P ⟶ Q over S is 2-isomorphic to a given morphism ψ of the small étale ringed topoi.

This is the faithfulness half of Stacks 04KL over a base, and it is not carried: it holds unconditionally, by Stacks 04M6, AlgebraicGeometry.Space.eq_of_smallEtaleRingedToposHom_twoIso, which says exactly that two morphisms of algebraic spaces over S with 2-isomorphic morphisms of small étale ringed topoi are equal. The existence half of Stacks 04KL over a base is AlgebraicGeometry.Space.IsRecoveredFromSmallEtale, which is proved for every base scheme by AlgebraicGeometry.Space.isRecoveredFromSmallEtale_holds.

Note that the 2-compatibility with structure morphisms to a base, which AlgebraicGeometry.Space.IsRecoveredFromSmallEtale cannot do without, and the hypothesis on the base scheme, which its proof cannot do without, are not needed here: the counterexample recorded in that definition's docstring is a ψ induced by no morphism over S, not by two.

theorem eq_of_inducesCommonSmallEtaleRingedToposHom {P Q : AlgebraicSpaces B S hS}
    {ψ : RingedToposHom (smallEtaleRingedTopos B S hS P) (smallEtaleRingedTopos B S hS Q)}
    (k₁ k₂ : P ⟶ Q) (h₁ : InducesSmallEtaleRingedToposHom B S hS k₁ ψ)
    (h₂ : InducesSmallEtaleRingedToposHom B S hS k₂ ψ) :
    k₁ = k₂

AlgebraicGeometry.Space.existsUnique_thickeningHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismFromStructureMap/RecoveryAndThickeningHom.lean, line 538. The attribute's comment: “over a base SCHEME whose canonical morphism to the spectrum of its global functions is a monomorphism -- an affine base, a quasi-affine base, any base which embeds in an affine scheme: that the recovered morphism is a morphism of thickenings over the base and that the pair is unique. The source states the tag over an arbitrary base and ends we omit the verification that f-prime is a morphism over B; the existence of the morphism recovering a locally ringed morphism of the small etale ringed topoi over the base -- 04KL over a base -- is what that verification amounts to, and it is PROVED here for such a base scheme, by isRecoveredFromSmallEtale_of_mono_toSpecGamma. That hypothesis is the exact reach of the route, being equivalent to the assertion that a morphism of schemes into the base is determined by its ring map on global functions, which is all the chart construction of 04KL produces. So this clause is unconditional for those base schemes only, and is NOT the tag in the generality the source states it in. The locally ringed condition on (f_spaces,etale, alpha) is derived from the commuting square, not assumed, and the uniqueness of the pair and the two equations are derived from the faithfulness half of 04KL over a base, which is PROVED for every base -- see eq_of_inducesCommonSmallEtaleRingedToposHom, from 04M6”.

Stacks 05ZN over a base scheme determined by its global functions. Let G ⊂ X' and H ⊂ Y' be thickenings of algebraic spaces over T, let f : X ⟶ Y be a morphism of the two closed subspaces, and let Φ = (f_{spaces,étale}, α) be a morphism of the small étale ringed topoi of X' and Y' which is compatible with the two inclusions and with the two structure morphisms to T. Then there is exactly one morphism f' : X' ⟶ Y' inducing Φ, and it makes (f, f') a morphism of thickenings over T.

The two compatibilities are the source's commuting square for α, f^♯, i_X^♯ and i_Y^♯, and the hypothesis that α is a map of 𝒪_T-algebras. That Φ is locally ringed is not assumed: it is derived from the square by AlgebraicGeometry.Space.isLocallyRinged_of_thickeningSquare, as in the source. Neither is the recovery of morphisms from their small étale ringed topoi assumed: it is AlgebraicGeometry.Space.isRecoveredFromSmallEtale_of_mono_toSpecΓ, which is where the hypothesis on the base scheme is used and the only place it is used. That hypothesis holds for an affine base scheme and for a quasi-affine one.

theorem existsUnique_thickeningHom (hSmono : Mono S.toSpecΓ)
    (hG : IsThickening B S hS X' G) (hH : IsThickening B S hS Y' H)
    (pX' : X' ⟶ T) (pY' : Y' ⟶ T)
    (f : IsThickening.space B S hS hG ⟶ IsThickening.space B S hS hH)
    (Φ : RingedToposHom (smallEtaleRingedTopos B S hS X') (smallEtaleRingedTopos B S hS Y'))
    (hsquare : Nonempty (SmallEtaleTwoIso B S hS
      (smallEtaleComp B S hS Φ
        (smallEtaleRingedToposHom B S hS (IsThickening.inclusion B S hS hG)))
      (smallEtaleRingedToposHom B S hS (f ≫ IsThickening.inclusion B S hS hH))))
    (halgebra : Nonempty (SmallEtaleTwoIso B S hS
      (smallEtaleComp B S hS (smallEtaleRingedToposHom B S hS pY') Φ)
      (smallEtaleRingedToposHom B S hS pX'))) :
    ∃! f' : X' ⟶ Y', InducesSmallEtaleRingedToposHom B S hS f' Φ ∧
      IsThickening.inclusion B S hS hG ≫ f' = f ≫ IsThickening.inclusion B S hS hH ∧
      f' ≫ pY' = pX'

AlgebraicGeometry.Space.existsUnique_thickeningHom_of_isLocallyRinged, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismFromStructureMap/RecoveryAndThickeningHom.lean, line 574. The attribute's comment: “that the recovered morphism is a morphism of thickenings over the base and that the pair is unique, with the recovery of morphisms over the base taken as an argument (IsRecoveredFromSmallEtale, which is Stacks 04KL over a base) and with the locally ringed condition on (f_spaces,etale, alpha) taken as an argument, since the latter needs the structure-sheaf half of 05ZM”.

Stacks 05ZN with the recovery of morphisms over the base and the local ringedness of Φ taken as arguments.

This is the shape in which the statement was first written. Both arguments are now available without being assumed — hlocal from the commuting square by AlgebraicGeometry.Space.isLocallyRinged_of_thickeningSquare, and hKL for a base scheme whose canonical morphism to the spectrum of its global functions is a monomorphism by AlgebraicGeometry.Space.isRecoveredFromSmallEtale_of_mono_toSpecΓ — so the tag is registered on AlgebraicGeometry.Space.existsUnique_thickeningHom above rather than here. This form is kept because the declarations below are stated in terms of it.

theorem existsUnique_thickeningHom_of_isLocallyRinged (hKL : IsRecoveredFromSmallEtale B S hS)
    (hG : IsThickening B S hS X' G) (hH : IsThickening B S hS Y' H)
    (pX' : X' ⟶ T) (pY' : Y' ⟶ T)
    (f : IsThickening.space B S hS hG ⟶ IsThickening.space B S hS hH)
    (Φ : RingedToposHom (smallEtaleRingedTopos B S hS X') (smallEtaleRingedTopos B S hS Y'))
    (hlocal : Φ.IsLocallyRinged)
    (hsquare : Nonempty (SmallEtaleTwoIso B S hS
      (smallEtaleComp B S hS Φ
        (smallEtaleRingedToposHom B S hS (IsThickening.inclusion B S hS hG)))
      (smallEtaleRingedToposHom B S hS (f ≫ IsThickening.inclusion B S hS hH))))
    (halgebra : Nonempty (SmallEtaleTwoIso B S hS
      (smallEtaleComp B S hS (smallEtaleRingedToposHom B S hS pY') Φ)
      (smallEtaleRingedToposHom B S hS pX'))) :
    ∃! f' : X' ⟶ Y', InducesSmallEtaleRingedToposHom B S hS f' Φ ∧
      IsThickening.inclusion B S hS hG ≫ f' = f ≫ IsThickening.inclusion B S hS hH ∧
      f' ≫ pY' = pX'

AlgebraicGeometry.Space.existsUnique_thickeningHom_of_ringedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismFromStructureMap/RecoveryAndThickeningHom.lean, line 616. The attribute's comment: “the whole lemma, over an arbitrary base scheme: the morphism (f_spaces,etale, alpha) of the small etale ringed topoi of the ambient spaces, compatible with the inclusions and with the structure morphisms to the base space, is induced by exactly one f', and (f, f') is a morphism of thickenings over the base space”.

Stacks 05ZN. Let B be a big fppf site, S a scheme in it and T an algebraic space over S. Let G ⊂ X' and H ⊂ Y' be thickenings of algebraic spaces over T, with structure morphisms p_{X'} : X' ⟶ T and p_{Y'} : Y' ⟶ T, and let f : X ⟶ Y be a morphism of the two closed subspaces. Let Φ = (f_{spaces,étale}, α) be a morphism of the small étale ringed topoi of X' and Y' which is compatible with the two inclusions (the source's commuting square for α, f^♯, i_X^♯ and i_Y^♯) and with the two structure morphisms to T (the source's hypothesis that α is a map of 𝒪_T-algebras). Then there is exactly one morphism f' : X' ⟶ Y' inducing Φ, that is with α = (f')^♯, and (f, f') is a morphism of thickenings over T: f' ∘ i_X = i_Y ∘ f and p_{Y'} ∘ f' = p_{X'}.

Nothing is assumed of the base scheme: the recovery of morphisms over the base is AlgebraicGeometry.Space.isRecoveredFromSmallEtale_holds, Stacks 04KL over an arbitrary base, the locality of Φ is derived from the square by AlgebraicGeometry.Space.isLocallyRinged_of_thickeningSquare, and the two equations and the uniqueness come from the faithfulness half of Tag 04KL, AlgebraicGeometry.Space.eq_of_inducesCommonSmallEtaleRingedToposHom. This supersedes AlgebraicGeometry.Space.existsUnique_thickeningHom, which carries a hypothesis on the base.

theorem existsUnique_thickeningHom_of_ringedToposHom
    (hG : IsThickening B S hS X' G) (hH : IsThickening B S hS Y' H)
    (pX' : X' ⟶ T) (pY' : Y' ⟶ T)
    (f : IsThickening.space B S hS hG ⟶ IsThickening.space B S hS hH)
    (Φ : RingedToposHom (smallEtaleRingedTopos B S hS X') (smallEtaleRingedTopos B S hS Y'))
    (hsquare : Nonempty (SmallEtaleTwoIso B S hS
      (smallEtaleComp B S hS Φ
        (smallEtaleRingedToposHom B S hS (IsThickening.inclusion B S hS hG)))
      (smallEtaleRingedToposHom B S hS (f ≫ IsThickening.inclusion B S hS hH))))
    (halgebra : Nonempty (SmallEtaleTwoIso B S hS
      (smallEtaleComp B S hS (smallEtaleRingedToposHom B S hS pY') Φ)
      (smallEtaleRingedToposHom B S hS pX'))) :
    ∃! f' : X' ⟶ Y', InducesSmallEtaleRingedToposHom B S hS f' Φ ∧
      IsThickening.inclusion B S hS hG ≫ f' = f ≫ IsThickening.inclusion B S hS hH ∧
      f' ≫ pY' = pX'

Tag 05ZP, a lemma

Tag 05ZP in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_isOpenSubspace_preimage_eq_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/OpenSubspaces.lean, line 117.

Stacks 05ZP. Let G ⊂ X be a thickening of algebraic spaces over S. Every open subspace U ⊂ G is the inverse image of a unique open subspace U' ⊂ X, in other words U = G ×_X U'; the inverse image is CategoryTheory.Subfunctor.preimage, identified with the fibre product by Stacks 083Q.

In the notation of the source, G is X and X is X'.

The open subspace is the one cut out by the image of the point set of U under the inclusion of the thickening, which is a homeomorphism on point spaces.

theorem existsUnique_isOpenSubspace_preimage_eq_of_isThickening
    (hG : IsThickening B S hS X G) (U : Subfunctor G.toFunctor)
    (hU : IsOpenSubspace B S hS U) :
    ∃! U' : Subfunctor X.1, IsOpenSubspace B S hS U' ∧ U'.preimage G.ι = U

Tag 05ZQ, a lemma

Tag 05ZQ in the Stacks Project.

AlgebraicGeometry.Space.surjective_globalFunctionsMap_projection_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/AffineSections.lean, line 314. The attribute's comment: “surjectivity of the restriction of regular functions, stated at the level of the spaces-étale sites: the affine object of the thickening's site is the base change G ×_X U of an object U of the ambient space's site, and the map is pullback along the cartesian projection G ×_X U ⟶ U, which is the closed immersion the source proof uses. The transport of the ambient structure sheaf through Stacks 05ZM is not used and no part of Stacks 05ZM is claimed: in this library 05ZM is formalized as an equivalence of topoi only, so the sheaf 𝒪_{X'} on the thickening's site does not exist and Γ(U, 𝒪_{X'}) is Γ(U, 𝒪_U) by construction. Granted h07VR, h07SQ and hFinitePresentation, which are passed unchanged to Stacks 07VS, AlgebraicGeometry.Space.isAffineSpace_of_isSurjective_of_isFinite, and are the conclusions of Stacks 07VR and Stacks 07SQ about inverse systems together with the finite-presentation special case of Stacks 07VS; none is the universally quantified form of this conclusion”.

Stacks 05ZQ. Let G ⊂ X be a thickening of algebraic spaces over S and let U be an object of the spaces-étale site of X whose base change G ×_X U along the inclusion is affine. Then restriction of global regular functions along the cartesian projection G ×_X U ⟶ U, that is Γ(U, 𝒪_U) → Γ(G ×_X U, 𝒪_{G ×_X U}), is surjective.

The ambient object U is affine by AlgebraicGeometry.Space.isAffineSpace_of_isThickening_of_isAffineSpace_baseChange, which is Stacks 07VS, and the projection is a closed immersion, so AlgebraicGeometry.Space.surjective_globalFunctionsMap_of_isClosedImmersion applies.

theorem surjective_globalFunctionsMap_projection_of_isThickening
    (hG : IsThickening B S hS X G) (U : SpacesEtale B S hS X)
    (hU : IsAffineSpace B S hS
      ((SpacesEtale.toSpaces B S hS (IsThickening.space B S hS hG)).obj
        ((spacesBaseChange B S hS (IsThickening.inclusion B S hS hG)).functor.obj U)).obj)
    (h07VR : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsFinite B S hS g →
      IsQuasiCompactSpace B S hS Y' →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y' →
      IntegralFiniteSystem B S hS g)
    (h07SQ : ∀ {I : Type u} [Preorder I] [IsDirected I (· ≤ ·)]
      (D : DescentSituation B S hS B.contains_terminal I),
      IsAffineSpace B S hS D.limitCone.pt →
      ∃ i : I, D.base ≤ i ∧ IsAffineSpace B S hS (D.system.obj (Opposite.op i)))
    (hFinitePresentation : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsFinite B S hS g →
      IsFinitePresentation B S hS g → IsSurjective B S hS g → IsAffineSpace B S hS X' →
      IsAffineSpace B S hS Y') :
    Function.Surjective (globalFunctionsMap B S hS
      ((spacesBaseChange B S hS (IsThickening.inclusion B S hS hG)).projection.app U))

AlgebraicGeometry.Space.surjective_globalFunctionsMap_of_isFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/AffineSections.lean, line 381. The attribute's comment: “the FIRST-ORDER thickening case only, with the source's own quantifier: V is an arbitrary object of the spaces-étale site of the closed subspace G whose underlying algebraic space is affine, and the map is pullback of global regular functions along the composite V ≅ G ×_X U ⟶ U of the isomorphism supplied by essential surjectivity of base change with the cartesian projection, U being the object of the ambient space's site that essential surjectivity produces. The source states 05ZQ for a thickening of arbitrary order; essential surjectivity, AlgebraicGeometry.Space.essSurj_spacesBaseChange_of_isFirstOrderThickening, is proved only at a first-order thickening, so the general case stays with the weaker parametrisation of AlgebraicGeometry.Space.surjective_globalFunctionsMap_projection_of_isThickening. The source's own second proof, for finite order thickenings, likewise reduces to the first-order case. As for the general statement, the transport of the ambient structure sheaf through Stacks 05ZM is not used and no part of Stacks 05ZM is claimed: Γ(V, 𝒪_{X'}) is Γ(U, 𝒪_U) by construction. Granted h07VR, h07SQ and hFinitePresentation, passed unchanged to the theorem of Stacks 07VS, AlgebraicGeometry.Space.isAffineSpace_of_isSurjective_of_isFinite, and are the conclusions of Stacks 07VR and Stacks 07SQ about inverse systems together with the finite-presentation special case of Stacks 07VS; none is the universally quantified form of this conclusion”.

Stacks 05ZQ at a first-order thickening, with the source's own quantifier. Let G ⊂ X be a first-order thickening of algebraic spaces over S and let V be an arbitrary object of the spaces-étale site of G whose underlying algebraic space is affine. Then restriction of global regular functions Γ(U, 𝒪_U) → Γ(V, 𝒪_V) is surjective, where U is the object of the spaces-étale site of X whose base change along the inclusion is isomorphic to V, and the map is pullback along the composite V ≅ G ×_X U ⟶ U of that isomorphism with the cartesian projection.

Base change along the inclusion of a first-order thickening is essentially surjective by AlgebraicGeometry.Space.essSurj_spacesBaseChange_of_isFirstOrderThickening, which is Stacks 05ZH in the only generality the library has it; the instance is discharged in the statement, so no part of Stacks 05ZH is granted. The object U and the isomorphism are the CategoryTheory.Functor.objPreimage and CategoryTheory.Functor.objObjPreimageIso of that essential surjectivity. Transporting affineness of V across the isomorphism makes AlgebraicGeometry.Space.surjective_globalFunctionsMap_projection_of_isThickening apply at U, and pullback along an isomorphism is bijective on global regular functions, so the composite is surjective.

Only the first-order case: Stacks 05ZQ is stated in the source for a thickening of arbitrary order, and for such a thickening the weaker parametrisation of AlgebraicGeometry.Space.surjective_globalFunctionsMap_projection_of_isThickening remains all that is available. The three hypotheses are threaded unchanged into that theorem.

theorem surjective_globalFunctionsMap_of_isFirstOrderThickening
    (hG : IsFirstOrderThickening B S hS X G)
    (V : SpacesEtale B S hS (IsThickening.space B S hS (hG.isThickening B S hS)))
    (hV : IsAffineSpace B S hS
      ((SpacesEtale.toSpaces B S hS
        (IsThickening.space B S hS (hG.isThickening B S hS))).obj V).obj)
    (h07VR : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsFinite B S hS g →
      IsQuasiCompactSpace B S hS Y' →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y' →
      IntegralFiniteSystem B S hS g)
    (h07SQ : ∀ {I : Type u} [Preorder I] [IsDirected I (· ≤ ·)]
      (D : DescentSituation B S hS B.contains_terminal I),
      IsAffineSpace B S hS D.limitCone.pt →
      ∃ i : I, D.base ≤ i ∧ IsAffineSpace B S hS (D.system.obj (Opposite.op i)))
    (hFinitePresentation : ∀ {X' Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : X' ⟶ Y'),
      IsAlgebraicSpace B S hS X' → IsAlgebraicSpace B S hS Y' → IsFinite B S hS g →
      IsFinitePresentation B S hS g → IsSurjective B S hS g → IsAffineSpace B S hS X' →
      IsAffineSpace B S hS Y') :
    letI : (spacesBaseChange B S hS
        (IsThickening.inclusion B S hS (hG.isThickening B S hS))).functor.EssSurj :=
      @essSurj_spacesBaseChange_of_isFirstOrderThickening B S hS _ X
        (IsThickening.inclusion B S hS (hG.isThickening B S hS)) (inferInstanceAs (Mono G.ι))
        (Eq.mpr (congrArg (IsFirstOrderThickening B S hS X) (Subfunctor.range_ι G)) hG)
    Function.Surjective (globalFunctionsMap B S hS
      ((SpacesEtale.toSpaces B S hS
            (IsThickening.space B S hS (hG.isThickening B S hS))).map
          ((spacesBaseChange B S hS (IsThickening.inclusion B S hS
            (hG.isThickening B S hS))).functor.objObjPreimageIso V).inv ≫
        (spacesBaseChange B S hS (IsThickening.inclusion B S hS
            (hG.isThickening B S hS))).projection.app
          ((spacesBaseChange B S hS (IsThickening.inclusion B S hS
            (hG.isThickening B S hS))).functor.objPreimage V)))

AlgebraicGeometry.Space.surjective_globalFunctionsMap_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/AffineSectionsSpacesEtale.lean, line 122. The attribute's comment: “for a thickening of arbitrary order and an arbitrary affine object V of the spaces-étale site of the closed subspace. The source's Γ(U, 𝒪_{X'}), the sections of 𝒪_{X'} read on the site of the closed subspace through Stacks 05ZM, is stated as Γ(U', 𝒪_{U'}) for the object U' of the ambient space's site with V ≅ X ×_{X'} U' given by essential surjectivity of base change, and the map is pullback along V ≅ X ×_{X'} U' ⟶ U'”.

Stacks 05ZQ. Let S be a scheme and let G ⊂ X be a thickening of algebraic spaces over S, of arbitrary order. Let V be an object of the spaces-étale site of G whose underlying algebraic space is affine. Then restriction of global regular functions Γ(U, 𝒪_U) → Γ(V, 𝒪_V) is surjective, where U is the object of the spaces-étale site of X whose base change along the inclusion is isomorphic to V, and the map is pullback along the composite V ≅ G ×_X U ⟶ U of that isomorphism with the cartesian projection.

In the notation of the source, G is X, X is X', and V is the source's U: the object U here is the source's U' with U = X ×_{X'} U', and Γ(U, 𝒪_U) is the source's Γ(U, 𝒪_{X'}), the sections of 𝒪_{X'} read on X_{spaces,étale} through Stacks 05ZM.

Base change along the inclusion is essentially surjective at a thickening of arbitrary order, AlgebraicGeometry.Space.essSurj_spacesBaseChange_of_isThickening; the instance is discharged in the statement, so no part of Stacks 05ZH is granted. The object U and the isomorphism are the CategoryTheory.Functor.objPreimage and CategoryTheory.Functor.objObjPreimageIso of that essential surjectivity. Affineness of V transported across the isomorphism makes AlgebraicGeometry.Space.surjective_globalFunctionsMap_spacesBaseChange_projection_of_isThickening apply at U, and pullback along an isomorphism is bijective on global regular functions.

theorem surjective_globalFunctionsMap_of_isThickening
    (hG : IsThickening B S hS X G)
    (V : SpacesEtale B S hS (IsThickening.space B S hS hG))
    (hV : IsAffineSpace B S hS
      ((SpacesEtale.toSpaces B S hS (IsThickening.space B S hS hG)).obj V).obj) :
    letI : (spacesBaseChange B S hS (IsThickening.inclusion B S hS hG)).functor.EssSurj :=
      essSurj_spacesBaseChange_of_isThickening B S hS hG
    Function.Surjective (globalFunctionsMap B S hS
      ((SpacesEtale.toSpaces B S hS (IsThickening.space B S hS hG)).map
          ((spacesBaseChange B S hS (IsThickening.inclusion B S hS hG)).functor.objObjPreimageIso
            V).inv ≫
        (spacesBaseChange B S hS (IsThickening.inclusion B S hS hG)).projection.app
          ((spacesBaseChange B S hS (IsThickening.inclusion B S hS hG)).functor.objPreimage
            V)))

Tag 05ZR, a lemma

Tag 05ZR in the Stacks Project.

AlgebraicGeometry.Space.isRepresentable_of_isRepresentable_thickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ThickeningSchemeRepresentable.lean, line 96. The attribute's comment: “granted the three hypotheses of Stacks 07VT, carried verbatim from Stacks 07VV and used for nothing else: h09YA, the conclusion of Stacks 09YA that an integral morphism over a quasi-compact quasi-separated algebraic space is a directed limit of finite morphisms of finite presentation; h07SQ, the conclusion of Stacks 07SQ that a directed system with affine transition morphisms whose limit is affine has an affine stage; and hFinitePresentation, the case of Stacks 07VT in which the morphism is finite and of finite presentation. None is the universally quantified form of this conclusion: the first two conclude about inverse systems and the third about affineness of a target, while this concludes representability of a presheaf”.

Stacks 05ZR. Let S be a scheme and let G ⊂ X' be a thickening of algebraic spaces over S, in the subspace form of Stacks 05ZK, part (1). If G is (representable by) a scheme, then so is X'.

The inclusion G.ι is integral by Stacks 081Y, injective on points because it is a monomorphism, and surjective on points by the definition of a thickening, so Stacks 07VV applies in the direction that goes from the source.

theorem isRepresentable_of_isRepresentable_thickening {X' : AlgebraicSpaces B S hS}
    {G : Subfunctor X'.1} (hG : IsThickening B S hS X' G)
    (hGrep : G.toFunctor.IsRepresentable)
    (h09YA : ∀ {Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : Y ⟶ Z),
      IsAlgebraicSpace B S hS Y → IsAlgebraicSpace B S hS Z → IsIntegralHom B S hS g →
      IsQuasiCompactSpace B S hS Z →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Z →
      IntegralFiniteSystem B S hS g)
    (h07SQ : ∀ {I : Type u} [Preorder I] [IsDirected I (· ≤ ·)]
      (D : DescentSituation B S hS B.contains_terminal I),
      IsAffineSpace B S hS D.limitCone.pt →
      ∃ i : I, D.base ≤ i ∧ IsAffineSpace B S hS (D.system.obj (Opposite.op i)))
    (hFinitePresentation : ∀ {Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : Y ⟶ Z),
      IsAlgebraicSpace B S hS Y → IsAlgebraicSpace B S hS Z → IsFinite B S hS g →
      IsFinitePresentation B S hS g → IsSurjective B S hS g → IsAffineSpace B S hS Y →
      IsAffineSpace B S hS Z) :
    X'.1.IsRepresentable

AlgebraicGeometry.Space.isRepresentable_of_isThickeningHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ThickeningSchemeRepresentable.lean, line 134. The attribute's comment: “the morphism form, granted the three hypotheses of Stacks 07VT, carried verbatim from Stacks 07VV and used for nothing else: h09YA, the conclusion of Stacks 09YA that an integral morphism over a quasi-compact quasi-separated algebraic space is a directed limit of finite morphisms of finite presentation; h07SQ, the conclusion of Stacks 07SQ that a directed system with affine transition morphisms whose limit is affine has an affine stage; and hFinitePresentation, the case of Stacks 07VT in which the morphism is finite and of finite presentation. None is the universally quantified form of this conclusion: the first two conclude about inverse systems and the third about affineness of a target, while this concludes representability of a presheaf”.

Stacks 05ZR, morphism form. Let S be a scheme and let i : X ⟶ X' be a thickening of algebraic spaces over S, in the morphism form of AlgebraicGeometry.Space.IsThickeningHom. If X is (representable by) a scheme, then so is X'.

A thickening is a closed immersion, hence integral by Stacks 081Y, it is a monomorphism and therefore injective on points, and it is surjective on points, so Stacks 07VV applies in the direction that goes from the source.

theorem isRepresentable_of_isThickeningHom {X X' : AlgebraicSpaces B S hS} (i : X ⟶ X')
    (hi : IsThickeningHom B S hS i) (hXrep : X.1.IsRepresentable)
    (h09YA : ∀ {Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : Y ⟶ Z),
      IsAlgebraicSpace B S hS Y → IsAlgebraicSpace B S hS Z → IsIntegralHom B S hS g →
      IsQuasiCompactSpace B S hS Z →
      IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Z →
      IntegralFiniteSystem B S hS g)
    (h07SQ : ∀ {I : Type u} [Preorder I] [IsDirected I (· ≤ ·)]
      (D : DescentSituation B S hS B.contains_terminal I),
      IsAffineSpace B S hS D.limitCone.pt →
      ∃ j : I, D.base ≤ j ∧ IsAffineSpace B S hS (D.system.obj (Opposite.op j)))
    (hFinitePresentation : ∀ {Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (g : Y ⟶ Z),
      IsAlgebraicSpace B S hS Y → IsAlgebraicSpace B S hS Z → IsFinite B S hS g →
      IsFinitePresentation B S hS g → IsSurjective B S hS g → IsAffineSpace B S hS Y →
      IsAffineSpace B S hS Z) :
    X'.1.IsRepresentable

Declarations registered for the tag:

• AlgebraicGeometry.Space.isRepresentable_of_isThickening_of_isRepresentable, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SchemeOfThickening.lean, line 71 (StacksFrontier).
• AlgebraicGeometry.Space.isRepresentable_of_isThickeningHom_of_isRepresentable, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SchemeOfThickening.lean, line 78 (StacksFrontier): “the morphism form”.
• AlgebraicGeometry.Space.isRepresentable_of_isThickening_of_isRepresentable, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/ThickeningSchemeRepresentableTag.lean, line 21 (StacksFrontier).
• AlgebraicGeometry.Space.isRepresentable_of_isThickeningHom_of_isRepresentable, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/ThickeningSchemeRepresentableTag.lean, line 23 (StacksFrontier): “the morphism form”.

Tag 05ZS, a lemma

Tag 05ZS in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_smallBaseChange_of_isThickeningHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SmallEtaleThickeningEquivalence.lean, line 58.

Stacks 05ZS. Let i : X ⟶ X' be a thickening of algebraic spaces over S. Base change V' ↦ X ×_{X'} V' is an equivalence from the small étale site of X' to that of X.

theorem isEquivalence_smallBaseChange_of_isThickeningHom {X X' : AlgebraicSpaces B S hS}
    (i : X ⟶ X') (hi : IsThickeningHom B S hS i) :
    (smallBaseChange B S hS i hi.isClosedImmersion.rep).IsEquivalence

AlgebraicGeometry.Space.spacesEtaleEquivalenceOfIsFirstOrderThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleEquivalence.lean, line 180. The attribute's comment: “the FIRST-ORDER thickening case, on the spaces-étale site of Stacks 03G0. The source states the tag for a thickening of arbitrary order and as an equivalence of the small étale sites of scheme charts; on the spaces-étale site the arbitrary-order equivalence is AlgebraicGeometry.Space.spacesEtaleEquivalenceOfIsThickening, and on the small étale sites of scheme charts this module covers the full faithfulness of the functor, by AlgebraicGeometry.Space.fullyFaithfulThickeningChartBaseChangeOfIsFirstOrderThickening. The module's What is not covered section sets out the differences from the source”.

Stacks 05ZS at a first-order thickening, on the spaces-étale site. Let G ⊂ X be a first-order thickening of algebraic spaces over S. Base change along the inclusion, V ↦ G ×_X V, is an equivalence of categories from the spaces-étale site of X to the spaces-étale site of G.

In the notation of the source, G is X and X is X': the functor is V' ↦ X ×_{X'} V' and the equivalence runs X'_étale → X_étale.

The functor is the one of the Stacks 03G2 base-change datum AlgebraicGeometry.Space.spacesBaseChange, and it is an equivalence because a first-order thickening is in particular a thickening: this is AlgebraicGeometry.Space.spacesEtaleEquivalenceOfIsThickening, the arbitrary-order equivalence of Stacks 05ZL, read at first order.

noncomputable def spacesEtaleEquivalenceOfIsFirstOrderThickening
    (hG : IsFirstOrderThickening B S hS X G) :
    SpacesEtale B S hS X ≌
      SpacesEtale B S hS (IsThickening.space B S hS (hG.isThickening B S hS))

AlgebraicGeometry.Space.fullyFaithfulThickeningChartBaseChangeOfIsFirstOrderThickening, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleEquivalence.lean, line 244. The attribute's comment: “FULL FAITHFULNESS ONLY, at a FIRST-ORDER thickening, of the source's own functor X'_étale → X_étale on the small étale sites of SCHEME charts, Stacks 03ED. The source asserts an equivalence, so essential surjectivity on those sites is a separate statement, Stacks 07VW. The restriction to first order is inherited from the library's Stacks 05ZH, AlgebraicGeometry.Space.full_spacesBaseChange_of_isFirstOrderThickening and AlgebraicGeometry.Space.faithful_spacesBaseChange_of_isFirstOrderThickening. The companion statement on the spaces-étale site of Stacks 03G0, where the full equivalence IS available at first order, is AlgebraicGeometry.Space.spacesEtaleEquivalenceOfIsFirstOrderThickening; the module's What is not covered section sets out the differences from the source”.

Stacks 05ZS, full faithfulness of the functor X'_étale → X_étale, at a first-order thickening. Let G ⊂ X be a first-order thickening of algebraic spaces over S. Base change of étale scheme charts along the inclusion, AlgebraicGeometry.Space.thickeningChartBaseChange, is fully faithful.

This is on the source's own site: the objects are the schemes étale over the two spaces. Only full faithfulness is reached. Essential surjectivity is Stacks 07VW, which rests on Stacks 05ZR; these are AlgebraicGeometry.Space.smallEtalePullback_isEquivalence and AlgebraicGeometry.Space.isRepresentable_of_isRepresentable_thickening, and they do not apply here, for two separate reasons, as the module's What is not covered section sets out: each carries three inputs of Stacks 07VT that this library does not prove, and the 07VW equivalence is for AlgebraicGeometry.Space.smallEtalePullback, which nothing in this library relates as a functor to AlgebraicGeometry.Space.thickeningChartBaseChange.

Chart base change becomes spaces-étale base change after the Stacks 03G1 comparison, by AlgebraicGeometry.Space.smallBaseChange_comparison. The comparison is fully faithful and spaces-étale base change at a first-order thickening is fully faithful, so the composite of chart base change with the comparison at G is isomorphic to a fully faithful functor, hence fully faithful; cancelling the faithful comparison at G leaves chart base change fully faithful.

noncomputable def fullyFaithfulThickeningChartBaseChangeOfIsFirstOrderThickening
    (hG : IsFirstOrderThickening B S hS X G) :
    (thickeningChartBaseChange B S hS (hG.isThickening B S hS)).FullyFaithful

AlgebraicGeometry.Space.isEquivalence_thickeningChartBaseChange_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SpacesEtaleEquivalenceArbitraryOrder.lean, line 335. The attribute's comment: “the functor is AlgebraicGeometry.Space.thickeningChartBaseChange, base change V' ↦ X ×_{X'} V' of schemes étale over X' along the inclusion of the thickening, between the small étale sites of Stacks 03ED; the packaged CategoryTheory.Equivalence is AlgebraicGeometry.Space.smallEtaleEquivalenceOfIsThickening”.

Stacks 05ZS. Let S be a scheme and let G ⊂ X be a thickening of algebraic spaces over S, of arbitrary order. Base change of étale scheme charts along the inclusion, V' ↦ G ×_X V', is an equivalence of categories from the small étale site of X to the small étale site of G.

In the notation of the source, G is X and X is X': the functor is V' ↦ V = X ×_{X'} V' and the equivalence runs X'_étale → X_étale, on the sites of Stacks 03ED whose objects are the schemes étale over the two spaces, which are the sites the source's statement is about. The cartesian square identifying the value of the functor at a chart with the fibre product is AlgebraicGeometry.Space.smallBaseChange_isPullback.

Full faithfulness is AlgebraicGeometry.Space.thickeningChartBaseChange_full and AlgebraicGeometry.Space.thickeningChartBaseChange_faithful; essential surjectivity is AlgebraicGeometry.Space.essSurj_thickeningChartBaseChange_of_isThickening, which uses the source's Lemma 05ZR in its closed-immersion form. Nothing is granted and neither half bounds the order of the thickening.

theorem isEquivalence_thickeningChartBaseChange_of_isThickening
    (hG : IsThickening B S hS X G) :
    (thickeningChartBaseChange B S hS hG).IsEquivalence

Tag 05ZT, a lemma

Tag 05ZT in the Stacks Project.

AlgebraicGeometry.Space.SquareZeroExtension.nonempty_enlargedRealization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SquareZeroExtensionEnlargedRealization.lean, line 98. The attribute's comment: “corrected: realized after enlarging the big fppf site, since on a fixed cutoff site a free kernel of rank the cutoff cannot be realized”.

Stacks 05ZT, corrected: a square-zero extension of the étale structure sheaf by a quasi-coherent module is realized by a first-order thickening after enlarging the big fppf site.

Why the enlargement. On a big fppf site B of a fixed cutoff κ the statement is false. Take X = Y = S = Spec k for a field k of size below κ and 𝒜 = 𝒪_X ⊕ ℐ the trivial square-zero extension by the free module ℐ = 𝒪_X^{(κ)} of rank κ, which is quasi-coherent. A first-order thickening X ⊂ X' realizing it is a thickening of an affine scheme, hence an affine scheme (Stacks 07VT), X' = Spec R with R ⟶ k surjective with kernel ℐ(X) = k^{(κ)}, so #R ≥ κ. But X' is an algebraic space for B, so it has an étale chart from an object of B; a nonempty affine open U of it is an object of B, of size below κ, and it maps onto the one-point space X'. So R ⟶ Γ(U, 𝒪_U) is faithfully flat, hence injective, and #R ≤ #Γ(U, 𝒪_U) < κ: a contradiction.

What is proved. There is a big fppf site B' containing B (the realization uses a site containing the thickenings of the two presenting charts of a charted presentation of f), with the transport of X, Y, f and E to B' (AlgebraicGeometry.Space.siteTransport), and a realization of the transported extension on B'. This is the Stacks statement read with the universe of schemes allowed to grow, which is how the Stacks project uses it.

theorem nonempty_enlargedRealization (E : SquareZeroExtension B S hS f) :
    Nonempty (EnlargedRealization B S hS E)

Tag 09ZX, a lemma

Tag 09ZX in the Stacks Project.

AlgebraicGeometry.Space.thickeningBaseChangeHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/BaseChange.lean, line 144. The attribute's comment: “morphism of thickenings”.

Stacks 09ZX. The commutative square expressing that the inclusion of the inverse image of a subfunctor Y of Y' along f : X' ⟶ Y' lies over the inclusion of Y: a morphism in the arrow category from (Y ×_{Y'} X' ⟶ X') to (Y ⟶ Y').

def thickeningBaseChangeHom {Y' X' : AlgebraicSpaces B S hS} (Y : Subfunctor Y'.1)
    (f : X' ⟶ Y') :
    Arrow.mk (Y.preimage f.hom).ι ⟶ Arrow.mk Y.ι

AlgebraicGeometry.Space.isThickening_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/BaseChange.lean, line 152. The attribute's comment: “base change of a thickening”.

Stacks 09ZX. The inverse image of a thickening Y ⊂ Y' along a morphism of algebraic spaces f : X' ⟶ Y' is a thickening of X'.

theorem isThickening_preimage {Y' X' : AlgebraicSpaces B S hS} (Y : Subfunctor Y'.1)
    (f : X' ⟶ Y') (hY : IsThickening B S hS Y' Y) :
    IsThickening B S hS X' (Y.preimage f.hom)

AlgebraicGeometry.Space.isThickening_range_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/BaseChangeFibreProduct.lean, line 79. The attribute's comment: “base change of a thickening, at a chosen fibre product”.

Stacks 09ZX, at a chosen fibre product. Let G ⊂ X be a thickening of algebraic spaces over S with inclusion i : G ⟶ X, let φ : U ⟶ X be any morphism, and let

P --q--> U
|        |
p        φ
v        v
G --i--> X

be a cartesian square. Then the range of q is a thickening of U.

This is the reading of the base change of a thickening that a chosen fibre product supplies, and in particular the one that the isPullback field of AlgebraicGeometry.Space.spacesBaseChange supplies for an object of the spaces-étale site of X. The range of q is the inverse image of G along φ, so this is AlgebraicGeometry.Space.isThickening_preimage read through that identification; see the implementation notes.

theorem isThickening_range_of_isPullback {X U P : AlgebraicSpaces B S hS}
    {G : Subfunctor X.1} (hG : IsThickening B S hS X G) {φ : U ⟶ X} {q : P ⟶ U}
    {p : P ⟶ IsThickening.space B S hS hG}
    (sq : IsPullback q p φ (IsThickening.inclusion B S hS hG)) :
    IsThickening B S hS U (Subfunctor.range q.hom)

AlgebraicGeometry.Space.isNthOrderThickening_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/BaseChangeOrder.lean, line 130. The attribute's comment: “base change of an nth-order thickening”.

Stacks 09ZX. The inverse image of an nth-order thickening Y ⊂ Y' along an arbitrary morphism f : X' ⟶ Y' of algebraic spaces is an nth-order thickening of X'.

It is a thickening by the order-free part of the tag. Its defining ideal on an affine chart of X' lying over an affine chart of Y' is the extension of the defining ideal of Y there, so its (n+1)st power is the extension of the (n+1)st power and vanishes; the affine chart diagrams are cofinal by Stacks 03G2, and the vanishing descends from a covering family.

theorem isNthOrderThickening_preimage {n : ℕ} {Y' X' : AlgebraicSpaces B S hS}
    (Y : Subfunctor Y'.1) (f : X' ⟶ Y') (hY : IsNthOrderThickening B S hS n Y' Y) :
    IsNthOrderThickening B S hS n X' (Y.preimage f.hom)

AlgebraicGeometry.Space.isFirstOrderThickening_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/BaseChangeOrder.lean, line 152. The attribute's comment: “base change of a first-order thickening”.

Stacks 09ZX. The inverse image of a first-order thickening along an arbitrary morphism of algebraic spaces is a first-order thickening: the case n = 1 of AlgebraicGeometry.Space.isNthOrderThickening_preimage.

theorem isFirstOrderThickening_preimage {Y' X' : AlgebraicSpaces B S hS}
    (Y : Subfunctor Y'.1) (f : X' ⟶ Y') (hY : IsFirstOrderThickening B S hS Y' Y) :
    IsFirstOrderThickening B S hS X' (Y.preimage f.hom)

AlgebraicGeometry.Space.isFiniteOrderThickening_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/BaseChangeOrder.lean, line 160. The attribute's comment: “base change of a finite-order thickening”.

Stacks 09ZX. The inverse image of a finite-order thickening along an arbitrary morphism of algebraic spaces is a finite-order thickening, with the same bound on the order.

theorem isFiniteOrderThickening_preimage {Y' X' : AlgebraicSpaces B S hS}
    (Y : Subfunctor Y'.1) (f : X' ⟶ Y') (hY : IsFiniteOrderThickening B S hS Y' Y) :
    IsFiniteOrderThickening B S hS X' (Y.preimage f.hom)

Declarations registered for the tag:

• CategoryTheory.Subfunctor.isPullback_preimage, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/BaseChange.lean, line 168 (StacksFrontier): “cartesian square”.

Tag 0BPH, a lemma

Tag 0BPH in the Stacks Project.

AlgebraicGeometry.Space.isThickening_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/Comp.lean, line 50.

Stacks 0BPH. A thickening X ⊂ X' of a closed subspace X' ⊂ X'' of an algebraic space X'' which is itself a thickening of X'' presents X as a thickening of X'', the composite closed subspace being the image of X under the inclusion of X'.

theorem isThickening_image (X'' : AlgebraicSpaces B S hS) (X' : Subfunctor X''.1)
    (hX' : IsThickening B S hS X'' X') (X : Subfunctor X'.toFunctor)
    (hX : IsThickening B S hS ⟨X'.toFunctor, hX'.1.1⟩ X) :
    IsThickening B S hS X'' (X.image X'.ι)

Tag 0BPI, a lemma

Tag 0BPI in the Stacks Project.

AlgebraicGeometry.Space.thickening_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FpqcLocal.lean, line 111. The attribute's comment: “thickenings”.

Being a thickening is fpqc local on the base for morphisms of algebraic spaces over S: a morphism whose base change to every member of some fpqc covering of its target is a thickening is itself a thickening.

instance thickening_isLocalAtTarget_fpqc :
    (thickeningMorphismProperty B S hS).IsLocalAtTarget
      (Topology.precoverage.{u, v} .fpqc B S hS)

AlgebraicGeometry.Space.isFirstOrderThickeningHom_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FpqcLocalFirstOrder.lean, line 353. The attribute's comment: “first-order clause, for an arbitrary fpqc covering”.

Let f : X ⟶ X' be a morphism of algebraic spaces over S and let {gᵢ : X'ᵢ ⟶ X'} be an fpqc covering of X' by algebraic spaces. If every base change fᵢ : Xᵢ ⟶ X'ᵢ of f is a first-order thickening then f is a first-order thickening.

theorem isFirstOrderThickeningHom_of_isFpqcCovering {I : Type v}
    {X X' : AlgebraicSpaces B S hS} (f : X ⟶ X')
    {Xi X'i : I → AlgebraicSpaces B S hS} (g : ∀ i, X'i i ⟶ X')
    (fi : ∀ i, Xi i ⟶ X'i i) (p : ∀ i, Xi i ⟶ X)
    (hsq : ∀ i, IsPullback (p i).hom (fi i).hom f.hom (g i).hom)
    (hg : IsFpqcCovering B S hS fun i ↦ (g i).hom)
    (h : ∀ i, IsFirstOrderThickeningHom B S hS (fi i)) :
    IsFirstOrderThickeningHom B S hS f

AlgebraicGeometry.Space.firstOrderThickening_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FpqcLocalFirstOrder.lean, line 393. The attribute's comment: “first order thickenings”.

Being a first-order thickening is fpqc local on the base for morphisms of algebraic spaces over S: a morphism whose base change to every member of some fpqc covering of its target is a first-order thickening is itself one, and conversely.

instance firstOrderThickening_isLocalAtTarget_fpqc :
    (firstOrderThickeningMorphismProperty B S hS).IsLocalAtTarget
      (Topology.precoverage.{u, v} .fpqc B S hS)

AlgebraicGeometry.Space.isThickeningHom_and_isFirstOrderThickeningHom_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FpqcLocalFirstOrder.lean, line 415.

Being a thickening is fpqc local, and similarly for first order thickenings. Let f : X ⟶ X' be a morphism of algebraic spaces over S and let {gᵢ : X'ᵢ ⟶ X'} be an fpqc covering of X' by algebraic spaces, with fᵢ : Xᵢ ⟶ X'ᵢ the base change of f along gᵢ. Then: if every fᵢ is a thickening so is f, and if every fᵢ is a first-order thickening so is f.

theorem isThickeningHom_and_isFirstOrderThickeningHom_of_isFpqcCovering {I : Type v}
    {X X' : AlgebraicSpaces B S hS} (f : X ⟶ X')
    {Xi X'i : I → AlgebraicSpaces B S hS} (g : ∀ i, X'i i ⟶ X')
    (fi : ∀ i, Xi i ⟶ X'i i) (p : ∀ i, Xi i ⟶ X)
    (hsq : ∀ i, IsPullback (p i).hom (fi i).hom f.hom (g i).hom)
    (hg : IsFpqcCovering B S hS fun i ↦ (g i).hom) :
    ((∀ i, IsThickeningHom B S hS (fi i)) → IsThickeningHom B S hS f) ∧
      ((∀ i, IsFirstOrderThickeningHom B S hS (fi i)) →
        IsFirstOrderThickeningHom B S hS f)

AlgebraicGeometry.Space.isThickeningHom_iff_forall_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FpqcLocalFirstOrder.lean, line 431. The attribute's comment: “thickenings, as an equivalence along an fpqc covering”.

A morphism f : X ⟶ X' of algebraic spaces over S is a thickening if and only if its base change along every member of an fpqc covering {gᵢ : X'ᵢ ⟶ X'} is a thickening.

theorem isThickeningHom_iff_forall_of_isFpqcCovering {I : Type v}
    {X X' : AlgebraicSpaces B S hS} (f : X ⟶ X')
    {Xi X'i : I → AlgebraicSpaces B S hS} (g : ∀ i, X'i i ⟶ X')
    (fi : ∀ i, Xi i ⟶ X'i i) (p : ∀ i, Xi i ⟶ X)
    (hsq : ∀ i, IsPullback (p i).hom (fi i).hom f.hom (g i).hom)
    (hg : IsFpqcCovering B S hS fun i ↦ (g i).hom) :
    IsThickeningHom B S hS f ↔ ∀ i, IsThickeningHom B S hS (fi i)

AlgebraicGeometry.Space.isFirstOrderThickeningHom_iff_forall_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FpqcLocalFirstOrder.lean, line 445. The attribute's comment: “first-order clause, as an equivalence along an fpqc covering”.

A morphism f : X ⟶ X' of algebraic spaces over S is a first-order thickening if and only if its base change along every member of an fpqc covering {gᵢ : X'ᵢ ⟶ X'} is a first-order thickening.

theorem isFirstOrderThickeningHom_iff_forall_of_isFpqcCovering {I : Type v}
    {X X' : AlgebraicSpaces B S hS} (f : X ⟶ X')
    {Xi X'i : I → AlgebraicSpaces B S hS} (g : ∀ i, X'i i ⟶ X')
    (fi : ∀ i, Xi i ⟶ X'i i) (p : ∀ i, Xi i ⟶ X)
    (hsq : ∀ i, IsPullback (p i).hom (fi i).hom f.hom (g i).hom)
    (hg : IsFpqcCovering B S hS fun i ↦ (g i).hom) :
    IsFirstOrderThickeningHom B S hS f ↔
      ∀ i, IsFirstOrderThickeningHom B S hS (fi i)

Stacks.Spaces.UniversalThickening.isClosedSubspace_and_isFirstOrderThickening_of_surjectiveEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/UniversalExistence/FirstOrderClauseAndAffineSize.lean, line 279. The attribute's comment: “first-order clause, along a surjective etale chart”.

Stacks 0BPI, the first-order clause, along a surjective étale chart. Let Y be a subfunctor of an algebraic space Q over S which is a sheaf for the big fppf topology, and let q : V ⟶ Q be a surjective étale chart of Q by an object of the site. If the base change of the inclusion of Y along q is a closed immersion whose range is a first-order thickening of V, then Y is a closed subspace of Q and a first-order thickening of it.

The source states the clause for an arbitrary fpqc covering of the target; this is the case of a one-member covering by a surjective étale scheme chart, which is the case the construction below consumes, together with the sheaf condition on Y that the fpqc statement does not ask for. Algebraicity of Y and closedness of its inclusion are Stacks 03I2 at the closed immersions, whose effective-descent input is discharged outright by AlgebraicGeometry.Space.isEffectiveDescentAlongSurjectiveEtale_isClosedImmersion; surjectivity on points follows from surjectivity of q and of the base change; and the order clause is Stacks.Spaces.UniversalThickening.definingIdealAt_pow_eq_bot_of_surjectiveEtaleChart, which descends the vanishing of the square of the defining ideal from the charts of V to the charts of Q.

theorem isClosedSubspace_and_isFirstOrderThickening_of_surjectiveEtaleChart
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {Q : AlgebraicGeometry.AlgebraicSpaces B S hS} (Y : Subfunctor Q.1)
    (hYsheaf : Presheaf.IsSheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) Y.toFunctor)
    {V : AlgebraicGeometry.BigFppfOver B S hS} (q : yoneda.obj V ⟶ Q.1)
    (hqsurj : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
      (AlgebraicGeometry.BigFppfOver.toScheme B S hS)).presheaf q)
    (hqetale : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (AlgebraicGeometry.BigFppfOver.toScheme B S hS)).presheaf q)
    (hclosed : AlgebraicGeometry.Space.IsClosedImmersion B S hS
      (Limits.pullback.snd Y.ι q))
    (hfirst : AlgebraicGeometry.Space.IsFirstOrderThickening B S hS
      (AlgebraicGeometry.schemeSpace V)
      (Subfunctor.range (Limits.pullback.snd Y.ι q))) :
    AlgebraicGeometry.Space.IsClosedSubspace B S hS Y ∧
      AlgebraicGeometry.Space.IsFirstOrderThickening B S hS Q Y

Sources

• Section 76.9, Tag 05ZJ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.exists_sieve_isNilpotent_of_mem_definingIdealAt · AlgebraicGeometry.Space.thickeningHom_structureSharp_compatible · AlgebraicGeometry.Space.exists_idealPow_firstOrderThickening_filtration · AlgebraicGeometry.Space.isLocallySurjective_structureSharpInverseImage · AlgebraicGeometry.Space.isIntegralHom_universallyInjective_isSurjective_ι_of_isThickening · AlgebraicGeometry.Space.IsThickening · AlgebraicGeometry.Space.IsMorphismOfThickenings · AlgebraicGeometry.Space.IsThickeningOver

Section76.10 Morphisms of thickenings#

Section 76.10 of the Stacks Project, Tag 0CG4. 3 tags here are carried by 44 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09ZY, a lemma

Tag 09ZY in the Stacks Project.

AlgebraicGeometry.Space.isAffineHom_iff_isAffineHom_of_isThickening_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismProperties.lean, line 309. The attribute's comment: “part (1): affine”.

Stacks 09ZY, part (1). In a morphism of thickenings of algebraic spaces over S the morphism on the closed subspaces is affine if and only if the morphism on the ambient spaces is.

theorem isAffineHom_iff_isAffineHom_of_isThickening_unconditional
    (hG : IsThickening B S hS X G) (hH : IsThickening B S hS Y H)
    (f : Arrow.mk G.ι ⟶ Arrow.mk H.ι) :
    IsAffineHom B S hS f.left ↔ IsAffineHom B S hS f.right

AlgebraicGeometry.Space.isIntegralHom_iff_isIntegralHom_of_isThickening_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismProperties.lean, line 320. The attribute's comment: “part (5): integral”.

Stacks 09ZY, part (5). In a morphism of thickenings of algebraic spaces over S the morphism on the closed subspaces is integral if and only if the morphism on the ambient spaces is.

theorem isIntegralHom_iff_isIntegralHom_of_isThickening_unconditional
    (hG : IsThickening B S hS X G) (hH : IsThickening B S hS Y H)
    (f : Arrow.mk G.ι ⟶ Arrow.mk H.ι) :
    IsIntegralHom B S hS f.left ↔ IsIntegralHom B S hS f.right

AlgebraicGeometry.Space.isSeparated_iff_and_isQuasiSeparated_iff_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismProperties.lean, line 331. The attribute's comment: “part (6): separated, and quasi-separated”.

Stacks 09ZY, part (6). In a morphism of thickenings of algebraic spaces over S the morphism on the closed subspaces is separated if and only if the morphism on the ambient spaces is, and it is quasi-separated if and only if the morphism on the ambient spaces is.

theorem isSeparated_iff_and_isQuasiSeparated_iff_of_isThickening
    (hG : IsThickening B S hS X G) (hH : IsThickening B S hS Y H)
    (f : Arrow.mk G.ι ⟶ Arrow.mk H.ι) :
    (IsSeparated B S hS f.left ↔ IsSeparated B S hS f.right) ∧
      (IsQuasiSeparated B S hS f.left ↔ IsQuasiSeparated B S hS f.right)

AlgebraicGeometry.Space.universallyInjective_iff_universallyInjective_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismProperties.lean, line 344. The attribute's comment: “part (7): universally injective”.

Stacks 09ZY, part (7). In a morphism of thickenings of algebraic spaces over S the morphism on the closed subspaces is universally injective if and only if the morphism on the ambient spaces is.

theorem universallyInjective_iff_universallyInjective_of_isThickening
    (hG : IsThickening B S hS X G) (hH : IsThickening B S hS Y H)
    (f : Arrow.mk G.ι ⟶ Arrow.mk H.ι) :
    UniversallyInjective B S hS f.left ↔ UniversallyInjective B S hS f.right

AlgebraicGeometry.Space.universallyOpen_iff_universallyOpen_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismProperties.lean, line 355. The attribute's comment: “part (8): universally open”.

Stacks 09ZY, part (8). In a morphism of thickenings of algebraic spaces over S the morphism on the closed subspaces is universally open if and only if the morphism on the ambient spaces is.

theorem universallyOpen_iff_universallyOpen_of_isThickening
    (hG : IsThickening B S hS X G) (hH : IsThickening B S hS Y H)
    (f : Arrow.mk G.ι ⟶ Arrow.mk H.ι) :
    UniversallyOpen B S hS f.left ↔ UniversallyOpen B S hS f.right

AlgebraicGeometry.Space.relativelyRepresentable_iff_relativelyRepresentable_of_isThickening_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/MorphismProperties.lean, line 366. The attribute's comment: “part (9): representable”.

Stacks 09ZY, part (9). In a morphism of thickenings of algebraic spaces over S the morphism on the closed subspaces is representable if and only if the morphism on the ambient spaces is.

theorem relativelyRepresentable_iff_relativelyRepresentable_of_isThickening_unconditional
    (hG : IsThickening B S hS X G) (hH : IsThickening B S hS Y H)
    (f : Arrow.mk G.ι ⟶ Arrow.mk H.ι) :
    yoneda.relativelyRepresentable f.left ↔ yoneda.relativelyRepresentable f.right

AlgebraicGeometry.Space.isSurjective_iff_isSurjective_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/Morphisms.lean, line 53. The attribute's comment: “surjective”.

In a morphism of thickenings of algebraic spaces over S the map on the closed subspaces is surjective if and only if the map on the ambient spaces is.

theorem isSurjective_iff_isSurjective_of_isThickening
    {X Y : AlgebraicSpaces B S hS} {G : Subfunctor X.1} {H : Subfunctor Y.1}
    (hG : IsThickening B S hS X G) (hH : IsThickening B S hS Y H)
    (f : Arrow.mk G.ι ⟶ Arrow.mk H.ι) :
    IsSurjective B S hS f.left ↔ IsSurjective B S hS f.right

AlgebraicGeometry.Space.isQuasiSeparated_iff_isQuasiSeparated_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/QuasiSeparatedTransfer.lean, line 152. The attribute's comment: “part (6): the quasi-separated half”.

Stacks 09ZY, the quasi-separated half of part (6). In a morphism of thickenings of algebraic spaces over S the morphism on the closed subspaces is quasi-separated if and only if the morphism on the ambient spaces is.

The separated half of the same part is AlgebraicGeometry.Space.isSeparated_iff_isSeparated_of_isThickening; together they are the whole of part (6).

theorem isQuasiSeparated_iff_isQuasiSeparated_of_isThickening
    (hG : IsThickening B S hS X G) (hH : IsThickening B S hS Y H)
    (f : Arrow.mk G.ι ⟶ Arrow.mk H.ι) :
    IsQuasiSeparated B S hS f.left ↔ IsQuasiSeparated B S hS f.right

AlgebraicGeometry.Space.universallyClosed_iff_universallyClosed_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SeparatedAndClosed.lean, line 223. The attribute's comment: “part (4): universally closed”.

In a morphism of thickenings of algebraic spaces over S the morphism on the closed subspaces is universally closed if and only if the morphism on the ambient spaces is.

theorem universallyClosed_iff_universallyClosed_of_isThickening
    (hG : IsThickening B S hS X G) (hH : IsThickening B S hS Y H)
    (f : Arrow.mk G.ι ⟶ Arrow.mk H.ι) :
    UniversallyClosed B S hS f.left ↔ UniversallyClosed B S hS f.right

AlgebraicGeometry.Space.isQuasiCompact_iff_isQuasiCompact_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SeparatedAndClosed.lean, line 234. The attribute's comment: “part (3): quasi-compact”.

In a morphism of thickenings of algebraic spaces over S the morphism on the closed subspaces is quasi-compact if and only if the morphism on the ambient spaces is.

theorem isQuasiCompact_iff_isQuasiCompact_of_isThickening
    (hG : IsThickening B S hS X G) (hH : IsThickening B S hS Y H)
    (f : Arrow.mk G.ι ⟶ Arrow.mk H.ι) :
    IsQuasiCompact B S hS f.left ↔ IsQuasiCompact B S hS f.right

AlgebraicGeometry.Space.isSeparated_iff_isSeparated_of_isThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SeparatedAndClosed.lean, line 244. The attribute's comment: “part (6): the separated half only, not quasi-separated”.

In a morphism of thickenings of algebraic spaces over S the morphism on the closed subspaces is separated if and only if the morphism on the ambient spaces is.

theorem isSeparated_iff_isSeparated_of_isThickening
    (hG : IsThickening B S hS X G) (hH : IsThickening B S hS Y H)
    (f : Arrow.mk G.ι ⟶ Arrow.mk H.ι) :
    IsSeparated B S hS f.left ↔ IsSeparated B S hS f.right

Tag 09ZZ, a lemma

Tag 09ZZ in the Stacks Project.

AlgebraicGeometry.Space.CartesianFiniteOrderMorphismOfThickenings.isLocallyOfFiniteType_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/CartesianFiniteOrderMorphism.lean, line 281. The attribute's comment: “part (2), locally of finite type; the finite-order hypothesis is on the TARGET thickening Y ⊆ Y', which is strictly stronger than the source hypothesis X ⊆ X' in the tag's text, so this is a weaker theorem than the tag announces. It is the hypothesis the tag's own proof uses: it reduces to Tag 09ZW, which puts finite order on the target, and says 'by induction on the order of the thickening we may assume that Y ⊆ Y' is a first order thickening'. Cartesianness plus target finite order gives source finite order by Tag 09ZX, but not conversely”.

Stacks 09ZZ, part (2). Local finite type is invariant under a cartesian morphism of thickenings of algebraic spaces whose target thickening is of finite order: the map between the smaller spaces is locally of finite type exactly when the map between the ambient spaces is.

The hypothesis is the finite order of the target thickening Y ⊂ Y', which is stronger than the finite order of the source thickening X ⊂ X' that the tag's text states; see the implementation notes of this file.

theorem isLocallyOfFiniteType_iff (M : CartesianFiniteOrderMorphismOfThickenings B S hS) :
    IsLocallyOfFiniteType B S hS M.f ↔ IsLocallyOfFiniteType B S hS M.f'

AlgebraicGeometry.Space.CartesianFiniteOrderMorphismOfThickenings.isLocallyQuasiFinite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FiniteOrderMorphismEtaleLocal.lean, line 146. The attribute's comment: “part (3), locally quasi-finite; the finite-order hypothesis is on the TARGET thickening Y ⊆ Y', which is strictly stronger than the source hypothesis X ⊆ X' in the tag's text, so this is a weaker theorem than the tag announces. It is the hypothesis the tag's own proof uses: it reduces to Tag 09ZW, which puts finite order on the target, and says 'by induction on the order of the thickening we may assume that Y ⊆ Y' is a first order thickening'. Cartesianness plus target finite order gives source finite order by Tag 09ZX, but not conversely”.

Stacks 09ZZ, part (3). Local quasi-finiteness is invariant under a cartesian morphism of thickenings of algebraic spaces whose target thickening is of finite order: the map between the smaller spaces is locally quasi-finite exactly when the map between the ambient spaces is.

The hypothesis is the finite order of the target thickening Y ⊂ Y', which is stronger than the finite order of the source thickening X ⊂ X' that the tag's text states; see the implementation notes of this file.

theorem isLocallyQuasiFinite_iff (M : CartesianFiniteOrderMorphismOfThickenings B S hS) :
    IsLocallyQuasiFinite B S hS M.f ↔ IsLocallyQuasiFinite B S hS M.f'

AlgebraicGeometry.Space.CartesianFiniteOrderMorphismOfThickenings.isUnramified_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FiniteOrderMorphismEtaleLocal.lean, line 168. The attribute's comment: “part (6), unramified; the finite-order hypothesis is on the TARGET thickening Y ⊆ Y', which is strictly stronger than the source hypothesis X ⊆ X' in the tag's text, so this is a weaker theorem than the tag announces. It is the hypothesis the tag's own proof uses: it reduces to Tag 09ZW, which puts finite order on the target, and says 'by induction on the order of the thickening we may assume that Y ⊆ Y' is a first order thickening'. Cartesianness plus target finite order gives source finite order by Tag 09ZX, but not conversely”.

Stacks 09ZZ, part (6). Unramifiedness is invariant under a cartesian morphism of thickenings of algebraic spaces whose target thickening is of finite order: the map between the smaller spaces is unramified exactly when the map between the ambient spaces is.

The hypothesis is the finite order of the target thickening Y ⊂ Y', which is stronger than the finite order of the source thickening X ⊂ X' that the tag's text states; see the implementation notes of this file.

theorem isUnramified_iff (M : CartesianFiniteOrderMorphismOfThickenings B S hS) :
    IsUnramified B S hS M.f ↔ IsUnramified B S hS M.f'

AlgebraicGeometry.Space.CartesianFiniteOrderMorphismOfThickenings.isProper_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FiniteOrderMorphismImmersions.lean, line 248. The attribute's comment: “part (7), proper; the finite-order hypothesis is on the TARGET thickening Y ⊆ Y', which is strictly stronger than the source hypothesis X ⊆ X' in the tag's text, so this is a weaker theorem than the tag announces. It is the hypothesis the tag's own proof uses: it reduces to Tag 09ZW, which puts finite order on the target, and says 'by induction on the order of the thickening we may assume that Y ⊆ Y' is a first order thickening'. Cartesianness plus target finite order gives source finite order by Tag 09ZX, but not conversely”.

Stacks 09ZZ, part (7). Properness is invariant under a cartesian morphism of thickenings of algebraic spaces whose target thickening is of finite order.

Properness is the conjunction of separatedness, local finite type, quasi-compactness and universal closedness. The first, third and fourth are invariant under an arbitrary morphism of thickenings, by parts (6), (3) and (4) of Stacks 09ZY, and the second is part (2) of this tag.

theorem isProper_iff : IsProper B S hS M.f ↔ IsProper B S hS M.f'

AlgebraicGeometry.Space.CartesianFiniteOrderMorphismOfThickenings.isFinite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FiniteOrderMorphismImmersions.lean, line 272. The attribute's comment: “part (8), finite; the finite-order hypothesis is on the TARGET thickening Y ⊆ Y', which is strictly stronger than the source hypothesis X ⊆ X' in the tag's text, so this is a weaker theorem than the tag announces. It is the hypothesis the tag's own proof uses: it reduces to Tag 09ZW, which puts finite order on the target, and says 'by induction on the order of the thickening we may assume that Y ⊆ Y' is a first order thickening'. Cartesianness plus target finite order gives source finite order by Tag 09ZX, but not conversely”.

Stacks 09ZZ, part (8). Finiteness is invariant under a cartesian morphism of thickenings of algebraic spaces whose target thickening is of finite order.

By Stacks 0A4X a morphism of algebraic spaces is finite exactly when it is proper and locally quasi-finite, and both of those are invariant: properness by part (7) of this tag and local quasi-finiteness by part (3).

theorem isFinite_iff : IsFinite B S hS M.f ↔ IsFinite B S hS M.f'

AlgebraicGeometry.Space.CartesianFiniteOrderMorphismOfThickenings.isClosedImmersion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FiniteOrderMorphismImmersions.lean, line 313. The attribute's comment: “part (1), closed immersion; the finite-order hypothesis is on the TARGET thickening Y ⊆ Y', which is strictly stronger than the source hypothesis X ⊆ X' in the tag's text, so this is a weaker theorem than the tag announces. It is the hypothesis the tag's own proof uses: it reduces to Tag 09ZW, which puts finite order on the target, and says 'by induction on the order of the thickening we may assume that Y ⊆ Y' is a first order thickening'. Cartesianness plus target finite order gives source finite order by Tag 09ZX, but not conversely”.

Stacks 09ZZ, part (1). Being a closed immersion is invariant under a cartesian morphism of thickenings of algebraic spaces whose target thickening is of finite order.

The implication from the ambient morphism to the morphism of smaller spaces is base change along the cartesian square. In the other direction, Stacks 05W8 characterises closed immersions of algebraic spaces as the universally closed, unramified, universally injective morphisms, and each of those three conditions is invariant: universal closedness by part (4) of Stacks 09ZY, unramifiedness by part (6) of this tag, and universal injectivity because X ⟶ Y ⟶ Y' equals X ⟶ X' ⟶ Y', the inclusions of the two thickenings are universally injective closed immersions and the source inclusion is surjective.

theorem isClosedImmersion_iff :
    IsClosedImmersion B S hS M.f ↔ IsClosedImmersion B S hS M.f'

AlgebraicGeometry.Space.CartesianFiniteOrderMorphismOfThickenings.isImmersion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FiniteOrderMorphismImmersions.lean, line 419. The attribute's comment: “part (10), immersion; the finite-order hypothesis is on the TARGET thickening Y ⊆ Y', which is strictly stronger than the source hypothesis X ⊆ X' in the tag's text, so this is a weaker theorem than the tag announces. It is the hypothesis the tag's own proof uses: it reduces to Tag 09ZW, which puts finite order on the target, and says 'by induction on the order of the thickening we may assume that Y ⊆ Y' is a first order thickening'. Cartesianness plus target finite order gives source finite order by Tag 09ZX, but not conversely”.

Stacks 09ZZ, part (10). Being an immersion is invariant under a cartesian morphism of thickenings of algebraic spaces whose target thickening is of finite order.

The implication from the ambient morphism to the morphism of smaller spaces is base change along the cartesian square. In the other direction, Stacks 04CE factors the immersion f as a closed immersion into the open subspace of Y complementary to the boundary of the image of f, and isImmersion_right_of_isClosedImmersion_into_openSubspace above turns that factorisation into an immersion factorisation of f' using part (1).

theorem isImmersion_iff : IsImmersion B S hS M.f ↔ IsImmersion B S hS M.f'

AlgebraicGeometry.Space.CartesianFiniteOrderMorphismOfThickenings.mono_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FiniteOrderMorphismMonomorphism.lean, line 299. The attribute's comment: “part (9), monomorphism; the finite-order hypothesis is on the TARGET thickening Y ⊆ Y', which is strictly stronger than the source hypothesis X ⊆ X' in the tag's text, so this is a weaker theorem than the tag announces. It is the hypothesis the tag's own proof uses: it reduces to Tag 09ZW, which puts finite order on the target, and says 'by induction on the order of the thickening we may assume that Y ⊆ Y' is a first order thickening'. Cartesianness plus target finite order gives source finite order by Tag 09ZX, but not conversely”.

Stacks 09ZZ, part (9). Being a monomorphism is invariant under a cartesian morphism of thickenings of algebraic spaces whose target thickening is of finite order: the map between the smaller spaces is a monomorphism exactly when the map between the ambient spaces is.

The implication from the ambient morphism to the morphism of smaller spaces is base change along the cartesian square. In the other direction, the first projection of X' ×_{Y'} X' is a monomorphism by mono_pullback_fst and a split epimorphism retracted by the diagonal of f', hence an isomorphism, and a morphism whose kernel pair has invertible first projection is a monomorphism.

theorem mono_iff : Mono M.f ↔ Mono M.f'

AlgebraicGeometry.Space.CartesianFiniteOrderMorphismOfThickenings.isLocallyOfFiniteType_and_hasRelativeDimension_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/FiniteOrderMorphismRelativeDimension.lean, line 139. The attribute's comment: “part (4), locally of finite type of relative dimension d, stated as the conjunction of local finite type and relative dimension d which is what that property means; the finite-order hypothesis is on the TARGET thickening Y ⊆ Y', which is strictly stronger than the source hypothesis X ⊆ X' in the tag's text, so this is a weaker theorem than the tag announces. It is the hypothesis the tag's own proof uses: it reduces to Tag 09ZW, which puts finite order on the target, and says 'by induction on the order of the thickening we may assume that Y ⊆ Y' is a first order thickening'. Cartesianness plus target finite order gives source finite order by Tag 09ZX, but not conversely”.

Stacks 09ZZ, part (4). Being locally of finite type of relative dimension d is invariant under a cartesian morphism of thickenings of algebraic spaces whose target thickening is of finite order: the map between the smaller spaces is locally of finite type of relative dimension d exactly when the map between the ambient spaces is.

The property is the conjunction of local finite type and relative dimension d, and the statement is that conjunction. Its first half is part (2) of the same tag.

The hypothesis is the finite order of the target thickening Y ⊂ Y', which is stronger than the finite order of the source thickening X ⊂ X' that the tag's text states; see the implementation notes of this file.

theorem isLocallyOfFiniteType_and_hasRelativeDimension_iff
    (M : CartesianFiniteOrderMorphismOfThickenings B S hS) (d : ℕ) :
    (IsLocallyOfFiniteType B S hS M.f ∧ HasRelativeDimension d B S hS M.f) ↔
      (IsLocallyOfFiniteType B S hS M.f' ∧ HasRelativeDimension d B S hS M.f')

AlgebraicGeometry.Space.CartesianSourceFiniteOrderMorphismOfThickenings.isLocallyOfFiniteType_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SourceFiniteOrderMorphism.lean, line 324. The attribute's comment: “part (2): f is locally of finite type iff f' is”.

Stacks 09ZZ, part (2). In a cartesian morphism of thickenings of algebraic spaces whose source thickening is of finite order, the map between the smaller spaces is locally of finite type exactly when the map between the ambient spaces is.

theorem isLocallyOfFiniteType_iff (M : CartesianSourceFiniteOrderMorphismOfThickenings B S hS) :
    IsLocallyOfFiniteType B S hS M.f ↔ IsLocallyOfFiniteType B S hS M.f'

AlgebraicGeometry.Space.CartesianSourceFiniteOrderMorphismOfThickenings.isLocallyQuasiFinite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SourceFiniteOrderMorphism.lean, line 335. The attribute's comment: “part (3): f is locally quasi-finite iff f' is”.

Stacks 09ZZ, part (3). In a cartesian morphism of thickenings of algebraic spaces whose source thickening is of finite order, the map between the smaller spaces is locally quasi-finite exactly when the map between the ambient spaces is.

theorem isLocallyQuasiFinite_iff (M : CartesianSourceFiniteOrderMorphismOfThickenings B S hS) :
    IsLocallyQuasiFinite B S hS M.f ↔ IsLocallyQuasiFinite B S hS M.f'

AlgebraicGeometry.Space.CartesianSourceFiniteOrderMorphismOfThickenings.isUnramified_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SourceFiniteOrderMorphism.lean, line 346. The attribute's comment: “part (6): f is unramified iff f' is”.

Stacks 09ZZ, part (6). In a cartesian morphism of thickenings of algebraic spaces whose source thickening is of finite order, the map between the smaller spaces is unramified exactly when the map between the ambient spaces is.

theorem isUnramified_iff (M : CartesianSourceFiniteOrderMorphismOfThickenings B S hS) :
    IsUnramified B S hS M.f ↔ IsUnramified B S hS M.f'

AlgebraicGeometry.Space.CartesianSourceFiniteOrderMorphismOfThickenings.isLocallyOfFiniteType_and_hasRelativeDimension_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SourceFiniteOrderMorphism.lean, line 376. The attribute's comment: “part (4): f is locally of finite type of relative dimension d iff f' is, the property being the conjunction of local finite type and relative dimension d”.

Stacks 09ZZ, part (4). In a cartesian morphism of thickenings of algebraic spaces whose source thickening is of finite order, the map between the smaller spaces is locally of finite type of relative dimension d exactly when the map between the ambient spaces is.

theorem isLocallyOfFiniteType_and_hasRelativeDimension_iff
    (M : CartesianSourceFiniteOrderMorphismOfThickenings B S hS) (d : ℕ) :
    (IsLocallyOfFiniteType B S hS M.f ∧ HasRelativeDimension d B S hS M.f) ↔
      (IsLocallyOfFiniteType B S hS M.f' ∧ HasRelativeDimension d B S hS M.f')

AlgebraicGeometry.Space.CartesianSourceFiniteOrderMorphismOfThickenings.isZero_sheafOfDifferentials_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SourceFiniteOrderMorphism.lean, line 413. The attribute's comment: “part (5): Ω_{X/Y} = 0 iff Ω_{X'/Y'} = 0, for the sheaves of differentials of Tag 04CT”.

Stacks 09ZZ, part (5). In a cartesian morphism of thickenings of algebraic spaces whose source thickening is of finite order, the sheaf of differentials Ω_{X/Y} of the map between the smaller spaces vanishes exactly when the sheaf of differentials Ω_{X'/Y'} of the map between the ambient spaces does.

By Stacks 04G9 each vanishing is formal unramifiedness of the corresponding morphism, and formallyUnramified_iff compares those.

theorem isZero_sheafOfDifferentials_iff
    (M : CartesianSourceFiniteOrderMorphismOfThickenings B S hS) :
    IsZero (sheafOfDifferentials B S hS M.smallHom) ↔
      IsZero (sheafOfDifferentials B S hS M.ambientHom)

AlgebraicGeometry.Space.CartesianSourceFiniteOrderMorphismOfThickenings.isProper_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SourceFiniteOrderMorphismImmersions.lean, line 98. The attribute's comment: “part (7): f is proper iff f' is”.

Stacks 09ZZ, part (7). In a cartesian morphism of thickenings of algebraic spaces whose source thickening is of finite order, the map between the smaller spaces is proper exactly when the map between the ambient spaces is.

theorem isProper_iff (M : CartesianSourceFiniteOrderMorphismOfThickenings B S hS) :
    IsProper B S hS M.f ↔ IsProper B S hS M.f'

AlgebraicGeometry.Space.CartesianSourceFiniteOrderMorphismOfThickenings.isFinite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SourceFiniteOrderMorphismImmersions.lean, line 114. The attribute's comment: “part (8): f is finite iff f' is”.

Stacks 09ZZ, part (8). In a cartesian morphism of thickenings of algebraic spaces whose source thickening is of finite order, the map between the smaller spaces is finite exactly when the map between the ambient spaces is.

theorem isFinite_iff (M : CartesianSourceFiniteOrderMorphismOfThickenings B S hS) :
    IsFinite B S hS M.f ↔ IsFinite B S hS M.f'

AlgebraicGeometry.Space.CartesianSourceFiniteOrderMorphismOfThickenings.isClosedImmersion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SourceFiniteOrderMorphismImmersions.lean, line 140. The attribute's comment: “part (1): f is a closed immersion iff f' is”.

Stacks 09ZZ, part (1). In a cartesian morphism of thickenings of algebraic spaces whose source thickening is of finite order, the map between the smaller spaces is a closed immersion exactly when the map between the ambient spaces is.

By Stacks 05W8 a closed immersion is a universally closed, unramified, universally injective morphism. Universal closedness transfers by Stacks 09ZY and unramifiedness by part (6); the composite X ⟶ Y ⟶ Y' is universally injective, it equals X ⟶ X' ⟶ Y', and X ⟶ X' is surjective, so f' is universally injective.

theorem isClosedImmersion_iff (M : CartesianSourceFiniteOrderMorphismOfThickenings B S hS) :
    IsClosedImmersion B S hS M.f ↔ IsClosedImmersion B S hS M.f'

AlgebraicGeometry.Space.CartesianSourceFiniteOrderMorphismOfThickenings.isImmersion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SourceFiniteOrderMorphismImmersions.lean, line 226. The attribute's comment: “part (10): f is an immersion iff f' is”.

Stacks 09ZZ, part (10). In a cartesian morphism of thickenings of algebraic spaces whose source thickening is of finite order, the map between the smaller spaces is an immersion exactly when the map between the ambient spaces is.

Stacks 04CE factors the immersion f as a closed immersion into an open subspace of Y, and isImmersion_right_of_isClosedImmersion_into_openSubspace turns that into an immersion factorisation of f'.

theorem isImmersion_iff (M : CartesianSourceFiniteOrderMorphismOfThickenings B S hS) :
    IsImmersion B S hS M.f ↔ IsImmersion B S hS M.f'

AlgebraicGeometry.Space.CartesianSourceFiniteOrderMorphismOfThickenings.mono_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/SourceFiniteOrderMorphismImmersions.lean, line 304. The attribute's comment: “part (9): f is a monomorphism iff f' is”.

Stacks 09ZZ, part (9). In a cartesian morphism of thickenings of algebraic spaces whose source thickening is of finite order, the map between the smaller spaces is a monomorphism exactly when the map between the ambient spaces is.

If f is a monomorphism, the first projection of X' ×_{Y'} X' is a monomorphism by mono_pullback_fst_of_mono and a split epimorphism retracted by the diagonal, hence an isomorphism, so f' is a monomorphism. The converse is base change.

theorem mono_iff (M : CartesianSourceFiniteOrderMorphismOfThickenings B S hS) :
    Mono M.f ↔ Mono M.f'

Tag 0BPJ, a lemma

Tag 0BPJ in the Stacks Project.

AlgebraicGeometry.Space.isLocallyQuasiFinite_iff_of_cartesianMorphismOfThickenings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/EtaleLocalProperties.lean, line 110. The attribute's comment: “locally_quasi_finite”.

Stacks 0BPJ, part (1). Being locally quasi-finite is invariant under a cartesian morphism of thickenings of algebraic spaces whose two component maps are locally of finite type.

theorem isLocallyQuasiFinite_iff_of_cartesianMorphismOfThickenings
    (T : CartesianLocallyFiniteTypeMorphismOfThickenings B S hS) :
    IsLocallyQuasiFinite B S hS T.f ↔ IsLocallyQuasiFinite B S hS T.f'

AlgebraicGeometry.Space.formallyUnramifiedCharts_iff_of_cartesianMorphismOfThickenings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/EtaleLocalProperties.lean, line 125. The attribute's comment: “vanishing_differentials”.

Stacks 0BPJ, part (4). In a cartesian morphism of thickenings of algebraic spaces whose two component maps are locally of finite type, the module of relative differentials of f vanishes exactly when the module of relative differentials of f' does.

The vanishing of Ω_{X/Y} is expressed by the condition that the morphism of schemes in every commuting square of étale charts of f is formally unramified, which on an affine chart is the vanishing of the Kähler differentials of the corresponding ring map.

theorem formallyUnramifiedCharts_iff_of_cartesianMorphismOfThickenings
    (T : CartesianLocallyFiniteTypeMorphismOfThickenings B S hS) :
    HoldsOnEveryEtaleChart B S hS
        (@_root_.AlgebraicGeometry.FormallyUnramified.{u} : MorphismProperty Scheme.{u}) T.f ↔
      HoldsOnEveryEtaleChart B S hS
        (@_root_.AlgebraicGeometry.FormallyUnramified.{u} : MorphismProperty Scheme.{u}) T.f'

AlgebraicGeometry.Space.locallyQuasiFiniteProperty_iff_of_cartesianSquareOfThickeningHoms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/EtaleLocalPropertiesPointTest.lean, line 66. The attribute's comment: “part (1): locally quasi-finite, at the Section 04XB point test”.

Stacks 0BPJ, part (1), at the point test of Section 04XB. Let (f, f') : (X ⊂ X') → (Y ⊂ Y') be a morphism of thickenings of algebraic spaces over S with f and f' locally of finite type and X = Y ×_{Y'} X'. Then f is locally quasi-finite if and only if f' is locally quasi-finite.

The square is given by morphisms of the category of algebraic spaces over S and the three properties by morphism properties of that category.

theorem locallyQuasiFiniteProperty_iff_of_cartesianSquareOfThickeningHoms
    {X X' Y Y' : AlgebraicSpaces B S hS} {i : X ⟶ X'} {j : Y ⟶ Y'} {f : X ⟶ Y} {f' : X' ⟶ Y'}
    (hi : IsThickeningHom B S hS i) (hj : IsThickeningHom B S hS j) (hsq : IsPullback f i j f')
    (hft : locallyOfFiniteTypeProperty B S hS f)
    (hft' : locallyOfFiniteTypeProperty B S hS f') :
    locallyQuasiFiniteProperty B S hS f ↔ locallyQuasiFiniteProperty B S hS f'

AlgebraicGeometry.Space.formallyUnramifiedCharts_iff_of_cartesianSquareOfThickeningHoms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/EtaleLocalPropertiesPointTest.lean, line 85. The attribute's comment: “part (4): vanishing relative differentials, at the Section 04XB point test”.

Stacks 0BPJ, part (4), at the point test of Section 04XB. Let (f, f') : (X ⊂ X') → (Y ⊂ Y') be a morphism of thickenings of algebraic spaces over S with f and f' locally of finite type and X = Y ×_{Y'} X'. Then Ω_{X/Y} = 0 if and only if Ω_{X'/Y'} = 0, the vanishing of the relative differentials being expressed, as in AlgebraicGeometry.Space.formallyUnramifiedCharts_iff_of_cartesianMorphismOfThickenings, by formal unramifiedness of the morphism of schemes in every commuting square of étale charts.

The square is given by morphisms of the category of algebraic spaces over S.

theorem formallyUnramifiedCharts_iff_of_cartesianSquareOfThickeningHoms
    {X X' Y Y' : AlgebraicSpaces B S hS} {i : X ⟶ X'} {j : Y ⟶ Y'} {f : X ⟶ Y} {f' : X' ⟶ Y'}
    (hi : IsThickeningHom B S hS i) (hj : IsThickeningHom B S hS j) (hsq : IsPullback f i j f')
    (hft : locallyOfFiniteTypeProperty B S hS f)
    (hft' : locallyOfFiniteTypeProperty B S hS f') :
    HoldsOnEveryEtaleChart B S hS
        (@_root_.AlgebraicGeometry.FormallyUnramified.{u} : MorphismProperty Scheme.{u}) f.hom ↔
      HoldsOnEveryEtaleChart B S hS
        (@_root_.AlgebraicGeometry.FormallyUnramified.{u} :
          MorphismProperty Scheme.{u}) f'.hom

AlgebraicGeometry.Space.properProperty_iff_of_cartesianSquareOfThickeningHoms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/ProperFinite.lean, line 60. The attribute's comment: “part (8): proper, at the Section 04XB point test”.

Let (f, f') : (X ⊂ X') → (Y ⊂ Y') be a morphism of thickenings of algebraic spaces over S with f and f' locally of finite type and X = Y ×_{Y'} X'. Then f is proper if and only if f' is proper.

theorem properProperty_iff_of_cartesianSquareOfThickeningHoms
    (hi : IsThickeningHom B S hS i) (hj : IsThickeningHom B S hS j) (hsq : IsPullback f i j f')
    (hft : locallyOfFiniteTypeProperty B S hS f)
    (hft' : locallyOfFiniteTypeProperty B S hS f') :
    properProperty B S hS f ↔ properProperty B S hS f'

AlgebraicGeometry.Space.finiteMorphismProperty_iff_of_cartesianSquareOfThickeningHoms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/ProperFinite.lean, line 81. The attribute's comment: “part (2): finite, at the Section 04XB point test”.

Let (f, f') : (X ⊂ X') → (Y ⊂ Y') be a morphism of thickenings of algebraic spaces over S with f and f' locally of finite type and X = Y ×_{Y'} X'. Then f is finite if and only if f' is finite.

theorem finiteMorphismProperty_iff_of_cartesianSquareOfThickeningHoms
    (hi : IsThickeningHom B S hS i) (hj : IsThickeningHom B S hS j) (hsq : IsPullback f i j f')
    (hft : locallyOfFiniteTypeProperty B S hS f)
    (hft' : locallyOfFiniteTypeProperty B S hS f') :
    finiteMorphismProperty B S hS f ↔ finiteMorphismProperty B S hS f'

AlgebraicGeometry.Space.CartesianLocallyFiniteTypeMorphismOfThickenings.isProper_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/SpacesFiniteProperMono.lean, line 102. The attribute's comment: “part (8): f is proper iff f' is”.

Stacks 0BPJ, part (8). In a cartesian morphism of thickenings of algebraic spaces whose two component maps are locally of finite type, the map between the smaller spaces is proper exactly when the map between the ambient spaces is.

theorem isProper_iff (T : CartesianLocallyFiniteTypeMorphismOfThickenings B S hS) :
    IsProper B S hS T.f ↔ IsProper B S hS T.f'

AlgebraicGeometry.Space.CartesianLocallyFiniteTypeMorphismOfThickenings.isFinite_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/SpacesFiniteProperMono.lean, line 118. The attribute's comment: “part (2): f is finite iff f' is”.

Stacks 0BPJ, part (2). In a cartesian morphism of thickenings of algebraic spaces whose two component maps are locally of finite type, the map between the smaller spaces is finite exactly when the map between the ambient spaces is.

theorem isFinite_iff (T : CartesianLocallyFiniteTypeMorphismOfThickenings B S hS) :
    IsFinite B S hS T.f ↔ IsFinite B S hS T.f'

AlgebraicGeometry.Space.CartesianLocallyFiniteTypeMorphismOfThickenings.mono_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/SpacesFiniteProperMono.lean, line 209. The attribute's comment: “part (6): f is a monomorphism iff f' is”.

Stacks 0BPJ, part (6). In a cartesian morphism of thickenings of algebraic spaces whose two component maps are locally of finite type, the map between the smaller spaces is a monomorphism exactly when the map between the ambient spaces is.

If f is a monomorphism, the first projection of X' ×_{Y'} X' is a monomorphism by mono_pullback_fst_of_mono and a split epimorphism retracted by the diagonal, hence an isomorphism, so f' is a monomorphism. The converse is base change.

theorem mono_iff (T : CartesianLocallyFiniteTypeMorphismOfThickenings B S hS) :
    Mono T.f ↔ Mono T.f'

AlgebraicGeometry.Space.closedImmersionProperty_iff_of_cartesianSquareOfThickeningHoms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/SpacesImmersions.lean, line 141. The attribute's comment: “part (3): closed immersion, at the Section 04XB point test”.

Stacks 0BPJ, part (3), at the point test of Section 04XB. Let (f, f') : (X ⊂ X') → (Y ⊂ Y') be a morphism of thickenings of algebraic spaces over S with f and f' locally of finite type and X = Y ×_{Y'} X'. Then f is a closed immersion if and only if f' is a closed immersion.

theorem closedImmersionProperty_iff_of_cartesianSquareOfThickeningHoms
    (hi : IsThickeningHom B S hS i) (hj : IsThickeningHom B S hS j) (hsq : IsPullback f i j f')
    (hft : locallyOfFiniteTypeProperty B S hS f)
    (hft' : locallyOfFiniteTypeProperty B S hS f') :
    closedImmersionProperty B S hS f ↔ closedImmersionProperty B S hS f'

AlgebraicGeometry.Space.immersionProperty_iff_of_cartesianSquareOfThickeningHoms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/SpacesImmersions.lean, line 287. The attribute's comment: “part (7): immersion, at the Section 04XB point test”.

Stacks 0BPJ, part (7), at the point test of Section 04XB. Let (f, f') : (X ⊂ X') → (Y ⊂ Y') be a morphism of thickenings of algebraic spaces over S with f and f' locally of finite type and X = Y ×_{Y'} X'. Then f is an immersion if and only if f' is an immersion.

theorem immersionProperty_iff_of_cartesianSquareOfThickeningHoms
    (hi : IsThickeningHom B S hS i) (hj : IsThickeningHom B S hS j) (hsq : IsPullback f i j f')
    (hft : locallyOfFiniteTypeProperty B S hS f)
    (hft' : locallyOfFiniteTypeProperty B S hS f') :
    immersionProperty B S hS f ↔ immersionProperty B S hS f'

AlgebraicGeometry.Space.mono_iff_of_cartesianSquareOfThickeningHoms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/SpacesImmersions.lean, line 344. The attribute's comment: “part (6): monomorphism, at the Section 04XB point test”.

Stacks 0BPJ, part (6), at the point test of Section 04XB. Let (f, f') : (X ⊂ X') → (Y ⊂ Y') be a morphism of thickenings of algebraic spaces over S with f and f' locally of finite type and X = Y ×_{Y'} X'. Then f is a monomorphism if and only if f' is a monomorphism.

The direction from f' to f is base change. In the other direction, f' is a monomorphism as soon as the first projection of X' ×_{Y'} X' is an isomorphism, and that projection is obtained as follows. Pull the thickening i : X ⟶ X' back along the first projection; the resulting square

X ×_{X'} (X' ×_{Y'} X') --→ X
|                           |
↓                           ↓
X' ×_{Y'} X' ------fst-----→ X'

is again a cartesian morphism of thickenings with both horizontal maps locally of finite type, and its upper map is an isomorphism: a section of the upper left corner is a pair (a, b) of sections of X' with f'(a) = f'(b) and a a section of X, the cartesian square of the given morphism of thickenings exhibits b as a second factorisation of that pair through X with the same image under f, and monomorphy of f identifies the two. An isomorphism is a closed immersion, so part (3) above makes fst a closed immersion, hence a monomorphism; it is also split by the diagonal of f', and a monomorphism which is a split epimorphism is an isomorphism.

This is the argument of AlgebraicGeometry.Space.CartesianFiniteOrderMorphismOfThickenings.mono_iff for part (9) of Stacks 09ZZ, with part (3) above in place of part (1) of that tag; the source's own proof of this case instead compares the conormal sheaf of the diagonal of f with that of f', which needs the algebraic-space form of Stacks 08S2 and so is not available here.

theorem mono_iff_of_cartesianSquareOfThickeningHoms
    (hi : IsThickeningHom B S hS i) (_hj : IsThickeningHom B S hS j) (hsq : IsPullback f i j f')
    (_hft : locallyOfFiniteTypeProperty B S hS f)
    (hft' : locallyOfFiniteTypeProperty B S hS f') :
    Mono f ↔ Mono f'

AlgebraicGeometry.Space.isUnramified_iff_of_cartesianMorphismOfThickenings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/Unramified.lean, line 118. The attribute's comment: “unramified”.

Being unramified is invariant under a cartesian morphism of thickenings of algebraic spaces whose two component maps are locally of finite type.

theorem isUnramified_iff_of_cartesianMorphismOfThickenings
    (T : CartesianLocallyFiniteTypeMorphismOfThickenings B S hS) :
    IsUnramified B S hS T.f ↔ IsUnramified B S hS T.f'

AlgebraicGeometry.Space.unramifiedMorphismProperty_iff_of_cartesianSquareOfThickeningHoms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/UnramifiedPointTest.lean, line 60. The attribute's comment: “part (5): unramified, at the Section 04XB point test”.

Stacks 0BPJ, part (5), at the point test of Section 04XB. Let (f, f') : (X ⊂ X') → (Y ⊂ Y') be a morphism of thickenings of algebraic spaces over S with f and f' locally of finite type and X = Y ×_{Y'} X'. Then f is unramified if and only if f' is unramified.

The two thickenings are given as morphisms i : X ⟶ X' and j : Y ⟶ Y' of the category of algebraic spaces over S (AlgebraicGeometry.Space.IsThickeningHom) and the three properties as morphism properties of that category, which is the shape the point test of Stacks 03YK reads a property of morphisms of algebraic spaces in; see AlgebraicGeometry.Stack.HasRelativeProperty. The equivalence itself is AlgebraicGeometry.Space.isUnramified_iff_of_cartesianMorphismOfThickenings, the same statement with the two smaller spaces presented as subfunctors of the two ambient ones.

theorem unramifiedMorphismProperty_iff_of_cartesianSquareOfThickeningHoms
    {X X' Y Y' : AlgebraicSpaces B S hS} {i : X ⟶ X'} {j : Y ⟶ Y'} {f : X ⟶ Y} {f' : X' ⟶ Y'}
    (hi : IsThickeningHom B S hS i) (hj : IsThickeningHom B S hS j) (hsq : IsPullback f i j f')
    (hft : locallyOfFiniteTypeProperty B S hS f)
    (hft' : locallyOfFiniteTypeProperty B S hS f') :
    unramifiedMorphismProperty B S hS f ↔ unramifiedMorphismProperty B S hS f'

Declarations registered for the tag:

• AlgebraicGeometry.Space.isClosedImmersion_iff_of_cartesianMorphismOfThickenings, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/SpacesFiniteProperMono.lean, line 222 (StacksFrontier): “part (3): f is a closed immersion iff f' is”.
• AlgebraicGeometry.Space.isImmersion_iff_of_cartesianMorphismOfThickenings, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/SpacesFiniteProperMono.lean, line 225 (StacksFrontier): “part (7): f is an immersion iff f' is”.

Sources

• Section 76.10, Tag 0CG4
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.isAffineHom_iff_isAffineHom_of_isThickening_unconditional · AlgebraicGeometry.Space.isIntegralHom_iff_isIntegralHom_of_isThickening_unconditional · AlgebraicGeometry.Space.isSeparated_iff_and_isQuasiSeparated_iff_of_isThickening · AlgebraicGeometry.Space.universallyInjective_iff_universallyInjective_of_isThickening · AlgebraicGeometry.Space.universallyOpen_iff_universallyOpen_of_isThickening · AlgebraicGeometry.Space.relativelyRepresentable_iff_relativelyRepresentable_of_isThickening_unconditional · AlgebraicGeometry.Space.isSurjective_iff_isSurjective_of_isThickening · AlgebraicGeometry.Space.isQuasiSeparated_iff_isQuasiSeparated_of_isThickening

Section76.11 Picard groups of thickenings#

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

Tag 0DNM, a lemma

Tag 0DNM in the Stacks Project.

AlgebraicGeometry.Space.picardFirstOrderSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/PicardSequence.lean, line 317. References: EGA IV (21.13.9), “The exact segment H¹(U”.

Stacks Project, Tag 0DNM. Let S be a scheme and let X ⊂ X' be a first-order thickening of algebraic spaces over S with ideal sheaf 𝓘. Then there is a canonical exact sequence

0 → H⁰(X,𝓘) → H⁰(X',𝒪*_{X'}) → H⁰(X,𝒪*_X) → H¹(X,𝓘) → Pic(X') → Pic(X) → H²(X,𝓘) → ⋯

which continues in every degree.

It is the long exact cohomology sequence of 0 → 𝓘 → 𝒪*_{X'} → 𝒪*_X → 0 on the common small étale site, with the two degree-one unit cohomology groups read as Picard groups by Tag 040E.

def picardFirstOrderSequence : PicardFirstOrderSequence B S hS hG

Sources

• Section 76.11, Tag 0DNL
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.picardFirstOrderSequence

Section76.12 Infinitesimal neighbourhoods#

Section 76.12 of the Stacks Project, Tag 05ZU. 3 tags here are carried by 13 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05ZV, a definition

Tag 05ZV in the Stacks Project.

Stacks.IdealSheaf.isNthOrderThickening_inclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/InfinitesimalNeighbourhood.lean, line 113. The attribute's comment: “the order asserted by the definition, read on an étale chart”.

The subscheme of a sheaf of ideals is an nth order thickening inside the subscheme of its (n + 1)st power.

theorem isNthOrderThickening_inclusion (I : X.IdealSheafData) (n : ℕ) :
    _root_.Stacks.Thickenings.IsNthOrderThickening n
      (Scheme.IdealSheafData.inclusion (pow_succ_le_self I n))

AlgebraicGeometry.Space.nthOrderInfinitesimalNeighbourhood, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/InfinitesimalNeighbourhood.lean, line 172. The attribute's comment: “part (2); the ideal of Z is given on an étale chart, 03MB being unavailable”.

The nth order infinitesimal neighbourhood of the closed subspace cut out by a sheaf of ideals J on a chart φ : U ⟶ X: the subspace of X cut out on that chart by J ^ (n + 1).

def nthOrderInfinitesimalNeighbourhood (φ : yoneda.obj U ⟶ X.1)
    (J : ((BigFppfOver.toScheme B S hS).obj U).IdealSheafData) (n : ℕ) : Subfunctor X.1

AlgebraicGeometry.Space.firstOrderInfinitesimalNeighbourhood, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/InfinitesimalNeighbourhood.lean, line 179. The attribute's comment: “part (1); the ideal of Z is given on an étale chart, 03MB being unavailable”.

The first order infinitesimal neighbourhood of the closed subspace cut out by a sheaf of ideals on a chart: the subspace cut out there by the square of that sheaf of ideals.

abbrev firstOrderInfinitesimalNeighbourhood (φ : yoneda.obj U ⟶ X.1)
    (J : ((BigFppfOver.toScheme B S hS).obj U).IdealSheafData) : Subfunctor X.1

AlgebraicGeometry.Space.immersionClosedLift_comp_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/InfinitesimalNeighbourhoodImmersion.lean, line 583. The attribute's comment: “over X: the immersion is the closed immersion of Z into the open U ⊆ X followed by the inclusion of U, which is what puts Z ⊆ Z_n over X”.

The factorisation of an immersion through the complement of the boundary of its image recovers the immersion. This is what puts the pair Z ⊆ Z_n ⊆ U of Stacks 05ZV over X: the open subspace U sits in X, and i is the composite of the closed immersion of Z into U with that inclusion.

theorem immersionClosedLift_comp_ι (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (i : Y ⟶ X) (hi : IsImmersion B S hS i) :
    immersionClosedLift B S hS hX hY i hi ≫
        (boundaryComplement B S hS X (Set.range (pointsMap B S hS Y i))).ι = i

AlgebraicGeometry.Space.nthOrderInfinitesimalNeighbourhoodOfImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/InfinitesimalNeighbourhoodImmersion.lean, line 605. The attribute's comment: “the construction of Z_n: the closed subspace of the open U = X ∖ ∂Z cut out by 𝓘 ^ (n + 1)”. References: EGA II (8.10.1), “more general”.

Stacks 05ZV. The nth order infinitesimal neighbourhood Z_n of an immersion i : Z ⟶ X of algebraic spaces over S: the closed subspace of the open subspace U ⊆ X in which Z is closed which is cut out by the (n + 1)st power of the quasi-coherent sheaf of ideals of Z in U.

def nthOrderInfinitesimalNeighbourhoodOfImmersion (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (i : Y ⟶ X) (hi : IsImmersion B S hS i) (n : ℕ) :
    ClosedSubspaces B S hS (immersionAmbientOpen B S hS hX i hi).1

AlgebraicGeometry.Space.firstOrderInfinitesimalNeighbourhoodOfImmersion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/InfinitesimalNeighbourhoodImmersion.lean, line 614. The attribute's comment: “part (1): the first order infinitesimal neighbourhood”.

Stacks 05ZV, part (1). The first order infinitesimal neighbourhood of an immersion: the closed subspace cut out by the square of the sheaf of ideals of its source.

abbrev firstOrderInfinitesimalNeighbourhoodOfImmersion (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (i : Y ⟶ X) (hi : IsImmersion B S hS i) :
    ClosedSubspaces B S hS (immersionAmbientOpen B S hS hX i hi).1

AlgebraicGeometry.Space.le_nthOrderInfinitesimalNeighbourhoodOfImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/InfinitesimalNeighbourhoodImmersion.lean, line 636. The attribute's comment: “the inclusion Z ⊆ Z_n inside the ambient open U”.

The source of an immersion is contained in each of its infinitesimal neighbourhoods. This is the inclusion Z ⊆ Z_n of Stacks 05ZV.

theorem le_nthOrderInfinitesimalNeighbourhoodOfImmersion (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (i : Y ⟶ X) (hi : IsImmersion B S hS i) (n : ℕ) :
    (immersionSourceSubspace B S hS hX hY i hi).1 ≤
      (nthOrderInfinitesimalNeighbourhoodOfImmersion B S hS hX hY i hi n).1

AlgebraicGeometry.Space.isNthOrderThickening_nthOrderInfinitesimalNeighbourhoodOfImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/InfinitesimalNeighbourhoodImmersion.lean, line 653. The attribute's comment: “the order: Z ⊆ Z_n is an nth order thickening, as the definition asserts”.

Stacks 05ZV, the order. The source of an immersion sits inside its nth order infinitesimal neighbourhood as an nth order thickening: on the small étale site of Z_n the (n + 1)st power of the defining ideal of Z vanishes. Together with AlgebraicGeometry.Space.le_nthOrderInfinitesimalNeighbourhoodOfImmersion and AlgebraicGeometry.Space.immersionClosedLift_comp_ι this is the assertion of the definition that Z ⊆ Z_n is the nth order thickening of Z over X.

The subspace of Z_n is the image of Z under the inclusion Z ⟶ Z_n of AlgebraicGeometry.Space.le_nthOrderInfinitesimalNeighbourhoodOfImmersion, that is, Z itself read inside Z_n.

theorem isNthOrderThickening_nthOrderInfinitesimalNeighbourhoodOfImmersion
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (i : Y ⟶ X)
    (hi : IsImmersion B S hS i) (n : ℕ) :
    IsNthOrderThickening B S hS n
        (closedSubspaceSpace B S hS (immersionAmbientOpen B S hS hX i hi)
          (nthOrderInfinitesimalNeighbourhoodOfImmersion B S hS hX hY i hi n))
      (Subfunctor.range (Subfunctor.homOfLe
        (le_nthOrderInfinitesimalNeighbourhoodOfImmersion B S hS hX hY i hi n)))

Tag 05ZW, a lemma

Tag 05ZW in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_lift_of_isNthOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/Infinitesimal.lean, line 240. The attribute's comment: “part (2): nth-order universal property”.

Stacks 05ZW, part (2). The universal property of the nth-order infinitesimal neighbourhood of an immersion. Let Z be a closed subspace of an open subspace U of X and let N be the closed subspace of U cut out by the (n+1)st power of the ideal sheaf of Z. Then every nth-order thickening G ⊆ T' over X compatible with Z admits a unique morphism to N over X extending the given map of its closed part.

theorem existsUnique_lift_of_isNthOrderThickening {n : ℕ} {X T' : AlgebraicSpaces B S hS}
    {U : Subfunctor X.1} (hU : IsOpenSubspace B S hS U)
    (Z N : ClosedSubspaces B S hS U.toFunctor)
    (hN : ∀ V : SmallEtale B S hS U.toFunctor,
      ((BigFppfOver.toScheme B S hS).map (N.2.2.rep.snd V.1.hom)).ker =
        ((BigFppfOver.toScheme B S hS).map (Z.2.2.rep.snd V.1.hom)).ker ^ (n + 1))
    {G : Subfunctor T'.1} (hG : IsNthOrderThickening B S hS n T' G)
    (a : G.toFunctor ⟶ Z.1.toFunctor) (b : T'.1 ⟶ X.1)
    (hab : G.ι ≫ b = a ≫ Z.1.ι ≫ U.ι) :
    ∃! a' : T'.1 ⟶ N.1.toFunctor,
      G.ι ≫ a' ≫ N.1.ι = a ≫ Z.1.ι ∧ a' ≫ N.1.ι ≫ U.ι = b

AlgebraicGeometry.Space.existsUnique_lift_of_isFirstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/Infinitesimal.lean, line 283. The attribute's comment: “part (1): first-order universal property”.

Stacks 05ZW, part (1). The universal property of the first-order infinitesimal neighbourhood of an immersion: the case n = 1 of AlgebraicGeometry.Space.existsUnique_lift_of_isNthOrderThickening.

theorem existsUnique_lift_of_isFirstOrderThickening {X T' : AlgebraicSpaces B S hS}
    {U : Subfunctor X.1} (hU : IsOpenSubspace B S hS U)
    (Z N : ClosedSubspaces B S hS U.toFunctor)
    (hN : ∀ V : SmallEtale B S hS U.toFunctor,
      ((BigFppfOver.toScheme B S hS).map (N.2.2.rep.snd V.1.hom)).ker =
        ((BigFppfOver.toScheme B S hS).map (Z.2.2.rep.snd V.1.hom)).ker ^ 2)
    {G : Subfunctor T'.1} (hG : IsFirstOrderThickening B S hS T' G)
    (a : G.toFunctor ⟶ Z.1.toFunctor) (b : T'.1 ⟶ X.1)
    (hab : G.ι ≫ b = a ≫ Z.1.ι ≫ U.ι) :
    ∃! a' : T'.1 ⟶ N.1.toFunctor,
      G.ι ≫ a' ≫ N.1.ι = a ≫ Z.1.ι ∧ a' ≫ N.1.ι ≫ U.ι = b

Tag 05ZX, a lemma

Tag 05ZX in the Stacks Project.

AlgebraicGeometry.Space.epi_conormalMap_firstOrderNeighbourhood, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleFirstOrderNeighbourhood.lean, line 89. The attribute's comment: “surjectivity of the comparison map of conormal modules”.

Let Z be a closed subspace of an algebraic space X and let Z' be the first order infinitesimal neighbourhood of Z in X. The map of conormal modules 𝒞_{Z/X} ⟶ 𝒞_{Z/Z'} induced by the fibre product square formed by Z ⊆ Z' and the inclusion Z' ⟶ X is an epimorphism.

theorem epi_conormalMap_firstOrderNeighbourhood (X : AlgebraicSpaces B S hS)
    (Z Z' : ClosedSubspaces B S hS X.1) (h : IsFirstOrderNeighbourhood B S hS X Z Z') :
    Epi (conormalMap B S hS
      (preimageSubspace B S hS (subspaceInclusion B S hS X Z') Z) Z
      (subspaceInclusion B S hS X Z')
      (preimageProjection B S hS (subspaceInclusion B S hS X Z') Z)
      (conormalEtaleRestrictionSquare B S hS (subspaceInclusion B S hS X Z') Z))

AlgebraicGeometry.Space.isIso_immersionLiftConormalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleFirstOrderNeighbourhoodImmersion.lean, line 387. The attribute's comment: “the map of conormal modules of 04CP from an immersion to its first order infinitesimal neighbourhood is an isomorphism”.

[Stacks Project, Tag 05ZX]. Let i : Z ⟶ X be an immersion of algebraic spaces and let Z ⊆ Z' be the first order infinitesimal neighbourhood of Z in X: the closed subspace of the complement X ∖ ∂Z of the boundary of the image, through which i factors as a closed immersion, cut out by the square of the defining ideal sheaf of Z there. Then the map 𝒞_{Z/X} ⟶ 𝒞_{Z/Z'} of [Stacks Project, Tag 04CP] induced by the square with 𝟙 Z on the left and Z' ⟶ X on the right, AlgebraicGeometry.Space.immersionLiftConormalMap, is an isomorphism of 𝒪_Z-modules.

The two conormal modules are AlgebraicGeometry.Space.conormalModuleOfImmersion of [Stacks Project, Tag 04CN], for i and for the immersion Z ⟶ Z'. The containment of the image of Z in Z', which the map is built from, is derived from the neighbourhood hypothesis by AlgebraicGeometry.Space.le_of_isFirstOrderNeighbourhood.

theorem isIso_immersionLiftConormalMap
    (h : IsFirstOrderNeighbourhood B S hS (immersionAmbient B S hS hX hZ i hi)
      (immersionRangeSubspace B S hS hX hZ i hi) Z') :
    IsIso (immersionLiftConormalMap B S hS hX hZ i hi Z'
      (le_of_isFirstOrderNeighbourhood B S hS _ _ Z' h))

AlgebraicGeometry.Space.isIso_conormalMap_of_ker_eq_ker_sq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ConormalModuleFirstOrderNeighbourhoodIso.lean, line 353. The attribute's comment: “the isomorphism, for a closed subspace”.

Let Z be a closed subspace of an algebraic space X and let N ⊆ X be its first order infinitesimal neighbourhood, the closed subspace whose ideal sheaf is on every étale chart of X the square of that of Z. The map 𝒞_{Z/X} ⟶ 𝒞_{Z_N/N} of conormal modules of [Stacks Project, Tag 04CP] attached to the fibre product square of Z_N = Z ×_X N ⊆ N over Z ⊆ X is an isomorphism.

theorem isIso_conormalMap_of_ker_eq_ker_sq :
    IsIso (conormalMap B S hS (preimageSubspace B S hS (subspaceInclusion B S hS X N) Z) Z
      (subspaceInclusion B S hS X N)
      (preimageProjection B S hS (subspaceInclusion B S hS X N) Z)
      (conormalEtaleRestrictionSquare B S hS (subspaceInclusion B S hS X N) Z))

Sources

• Section 76.12, Tag 05ZU
• AxiomMath/Stacks at 5ed82d14

LeanStacks.IdealSheaf.isNthOrderThickening_inclusion · AlgebraicGeometry.Space.nthOrderInfinitesimalNeighbourhood · AlgebraicGeometry.Space.firstOrderInfinitesimalNeighbourhood · AlgebraicGeometry.Space.immersionClosedLift_comp_ι · AlgebraicGeometry.Space.nthOrderInfinitesimalNeighbourhoodOfImmersion · AlgebraicGeometry.Space.firstOrderInfinitesimalNeighbourhoodOfImmersion · AlgebraicGeometry.Space.le_nthOrderInfinitesimalNeighbourhoodOfImmersion · AlgebraicGeometry.Space.isNthOrderThickening_nthOrderInfinitesimalNeighbourhoodOfImmersion

Section76.13 Formally smooth, étale, unramified transformations#

Section 76.13 of the Stacks Project, Tag 04G3. 7 tags here are carried by 29 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 049S, a definition

Tag 049S in the Stacks Project.

AlgebraicGeometry.Space.FormallySmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Defs.lean, line 68. The attribute's comment: “part (1)”. References: SGA 3 XI (1.6), “formally smooth”.

Stacks 049S, part (1). Every commutative affine square against a square-zero closed immersion admits a lift.

public abbrev FormallySmooth {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v} (a : F ⟶ G) : Prop

AlgebraicGeometry.Space.FormallyEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Defs.lean, line 79. The attribute's comment: “part (2)”. References: SGA 3 XI (1.6), “formally étale”.

Stacks 049S, part (2). Every commutative affine square against a square-zero closed immersion admits exactly one lift.

public abbrev FormallyEtale {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v} (a : F ⟶ G) : Prop

AlgebraicGeometry.Space.FormallyUnramified, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Defs.lean, line 90. The attribute's comment: “part (3)”. References: SGA 3 XI (1.6), “formally unramified”.

Stacks 049S, part (3). Every commutative affine square against a square-zero closed immersion admits at most one lift.

public abbrev FormallyUnramified {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v} (a : F ⟶ G) :
    Prop

Tag 04G4, a lemma

Tag 04G4 in the Stacks Project.

AlgebraicGeometry.Space.formallyEtale_iff_formallySmooth_and_formallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/EtaleIffSmoothUnramified.lean, line 49. References: EGA IV (17.1.1), “étale ⟺ smooth+unram”.

Stacks 04G4. A transformation of set-valued functors on the big fppf site is formally étale if and only if it is both formally smooth and formally unramified.

public theorem formallyEtale_iff_formallySmooth_and_formallyUnramified (a : F ⟶ G) :
    FormallyEtale a ↔ (FormallySmooth a ∧ FormallyUnramified a)

Tag 049T, a lemma

Tag 049T in the Stacks Project.

AlgebraicGeometry.Space.FormallySmooth.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Comp.lean, line 48. The attribute's comment: “formally_smooth_comp”. References: EGA IV (17.1.3), “(ii) smooth”; EGA IV (17.1.5), “sufficiency, smooth”.

Stacks 049T, formal smoothness under composition.

public theorem FormallySmooth.comp (a : F ⟶ G) (b : G ⟶ H)
    (ha : FormallySmooth a) (hb : FormallySmooth b) :
    FormallySmooth (a ≫ b)

AlgebraicGeometry.Space.formallyEtale_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Comp.lean, line 60. The attribute's comment: “formally_etale_comp”. References: EGA IV (17.1.3), “(ii) étale”; EGA IV (17.1.5), “sufficiency, étale”.

The composite of two formally étale transformations is formally étale.

public theorem formallyEtale_comp {a : F ⟶ G} {b : G ⟶ H}
    (ha : FormallyEtale a) (hb : FormallyEtale b) :
    FormallyEtale (a ≫ b)

AlgebraicGeometry.Space.formallyUnramified_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Comp.lean, line 74. The attribute's comment: “formally_unramified_comp”. References: EGA IV (17.1.3), “(ii) unramified”; EGA IV (17.1.5), “sufficiency, unramified”.

Stacks 049T, composition part. A composite of formally unramified transformations is formally unramified.

public theorem formallyUnramified_comp (a : F ⟶ G) (b : G ⟶ H)
    (ha : FormallyUnramified a) (hb : FormallyUnramified b) :
    FormallyUnramified (a ≫ b)

Tag 049U, a lemma

Tag 049U in the Stacks Project.

AlgebraicGeometry.Space.FormallySmooth.baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/BaseChange.lean, line 227. The attribute's comment: “formally_smooth_base_change”. References: EGA IV (17.1.3), “(iii) smooth”.

Stacks 049U, formal smoothness under base change.

public theorem FormallySmooth.baseChange
    (D : FppfFunctorPullbackSituation.{u, v})
    (ha : FormallySmooth D.a) :
    FormallySmooth D.toH

AlgebraicGeometry.Space.formallyEtale_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/BaseChange.lean, line 240. The attribute's comment: “formally_etale_base_change”. References: EGA IV (17.1.3), “(iii) étale”.

A base change of a formally étale transformation is formally étale.

public theorem formallyEtale_baseChange
    (D : FppfFunctorPullbackSituation.{u, v})
    (ha : FormallyEtale D.a) :
    FormallyEtale D.toH

AlgebraicGeometry.Space.formallyUnramified_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/BaseChange.lean, line 252. The attribute's comment: “formally_unramified_base_change”. References: EGA IV (17.1.3), “(iii) unramified”.

The base change of a formally unramified transformation is formally unramified.

public theorem formallyUnramified_baseChange
    (D : FppfFunctorPullbackSituation.{u, v})
    (ha : FormallyUnramified D.a) :
    FormallyUnramified D.toH

Tag 04AL, a lemma

Tag 04AL in the Stacks Project.

AlgebraicGeometry.Space.formallyEtale_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Etale.lean, line 46. The attribute's comment: “etale_implies_formally_etale”. References: EGA IV (17.1.3), “(i) open immersion”.

An étale representable transformation on the big fppf site is formally étale.

public theorem formallyEtale_of_etale
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (a : F ⟶ G)
    (ha : (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf a) :
    FormallyEtale a

AlgebraicGeometry.Space.formallySmooth_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Etale.lean, line 121. The attribute's comment: “etale_implies_formally_smooth”. References: EGA IV (17.1.3), “(i) open immersion”.

An étale representable transformation on the big fppf site is formally smooth.

public theorem formallySmooth_of_etale
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (a : F ⟶ G)
    (ha : (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf a) :
    FormallySmooth a

AlgebraicGeometry.Space.formallySmooth_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Smooth.lean, line 70. The attribute's comment: “part (1)”.

Stacks 04AL, part (1). A smooth representable transformation on the big fppf site is formally smooth.

public theorem formallySmooth_of_smooth
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (a : F ⟶ G)
    (ha : (MorphismProperty.inverseImage
      (@Smooth.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf a) :
    FormallySmooth a

AlgebraicGeometry.Space.formallySmooth_formallyEtale_formallyUnramified_of_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/SmoothEtaleUnramified.lean, line 70. References: EGA 0 (19.0.1), “partial”; SGA 3 XI (1.6), “necessity direction”.

Stacks 04AL. Let S be a scheme, let F and G be set-valued functors on the big fppf site over S, and let a : F ⟶ G be a representable transformation of functors. Then

1. if a is smooth it is formally smooth;
2. if a is étale it is formally étale;
3. if a is unramified it is formally unramified.

Each part is proved by turning the lifting problem into one for the scheme representing the base change of a along a point of the target, where the corresponding implication for morphisms of schemes applies; see AlgebraicGeometry.Space.formallySmooth_of_smooth, AlgebraicGeometry.Space.formallyEtale_of_etale and AlgebraicGeometry.Space.formallyUnramified_of_unramified, which this statement assembles.

public theorem formallySmooth_formallyEtale_formallyUnramified_of_representable
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) :
    ((MorphismProperty.inverseImage (@Smooth.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf a → FormallySmooth a) ∧
      ((MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf a → FormallyEtale a) ∧
      ((MorphismProperty.inverseImage (@Unramified.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf a → FormallyUnramified a)

AlgebraicGeometry.Space.formallyUnramified_of_unramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Unramified.lean, line 189. The attribute's comment: “unramified_implies_formally_unramified”.

Stacks Project, Tag 04AL. An unramified representable transformation is formally unramified.

public theorem formallyUnramified_of_unramified
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G)
    (ha : (MorphismProperty.inverseImage
      (@Unramified.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf a) :
    FormallyUnramified a

Tag 04CY, a lemma

Tag 04CY in the Stacks Project.

AlgebraicGeometry.Space.formallyEtale_comp_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Etale.lean, line 108. The attribute's comment: “compose_formally_etale”.

An étale transformation followed by a formally étale transformation is formally étale.

public theorem formallyEtale_comp_of_etale
    {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {a : F ⟶ G} {b : G ⟶ H}
    (ha : (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf a)
    (hb : FormallyEtale b) :
    FormallyEtale (a ≫ b)

AlgebraicGeometry.Space.formallySmooth_comp_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Etale.lean, line 133. The attribute's comment: “compose_formally_smooth”.

An étale transformation followed by a formally smooth transformation is formally smooth.

public theorem formallySmooth_comp_of_etale
    {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {a : F ⟶ G} {b : G ⟶ H}
    (ha : (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf a)
    (hb : FormallySmooth b) :
    FormallySmooth (a ≫ b)

AlgebraicGeometry.Space.exists_etale_affine_local_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/EtaleLocalLift.lean, line 210. The attribute's comment: “local_formal_smooth_lift”.

Stacks 04CY, the local form of the descent half. In a representable, surjective, étale situation F ⟶ G ⟶ H over an affine square-zero thickening i : T ⟶ T', a formally smooth composite admits, over every point of T, an affine étale neighbourhood U' ⟶ T' of its image and a section of G over U' which lifts the given section of H and agrees with the given section of G over T after restriction to every common refinement.

public theorem exists_etale_affine_local_lift
    (D : RepresentableSurjectiveEtaleSituation.{u})
    (T T' : BigFppfOver D.B D.S D.hS) (i : T ⟶ T')
    (_hT' : IsAffine ((BigFppfOver.toScheme D.B D.S D.hS).obj T'))
    (hi : IsSquareZeroClosedImmersion D.B D.S D.hS i)
    (x : D.G.obj (op T)) (y : D.H.obj (op T'))
    (hxy : D.b.app (op T) x = D.H.map i.op y)
    (hsmooth : FormallySmooth (D.a ≫ D.b))
    (t : (BigFppfOver.toScheme D.B D.S D.hS).obj T) :
    ∃ (U' : BigFppfOver D.B D.S D.hS) (j : U' ⟶ T') (z : D.G.obj (op U')),
      IsAffine ((BigFppfOver.toScheme D.B D.S D.hS).obj U') ∧
      Etale ((BigFppfOver.toScheme D.B D.S D.hS).map j) ∧
      (∃ u : (BigFppfOver.toScheme D.B D.S D.hS).obj U',
        ((BigFppfOver.toScheme D.B D.S D.hS).map j).base u =
          ((BigFppfOver.toScheme D.B D.S D.hS).map i).base t) ∧
      D.b.app (op U') z = D.H.map j.op y ∧
      ∀ (V : BigFppfOver D.B D.S D.hS) (f : V ⟶ T) (g : V ⟶ U'),
        f ≫ i = g ≫ j → D.G.map f.op x = D.G.map g.op z

AlgebraicGeometry.Space.formallyUnramified_comp_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Unramified.lean, line 219. The attribute's comment: “compose_formally_unramified”.

A formally unramified transformation remains formally unramified after precomposition with an étale transformation.

public theorem formallyUnramified_comp_of_etale
    {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (a : F ⟶ G) (b : G ⟶ H)
    (ha : (MorphismProperty.inverseImage (@Etale :
      MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS)).presheaf a)
    (hb : FormallyUnramified b) :
    FormallyUnramified (a ≫ b)

AlgebraicGeometry.Space.formallyUnramified_of_comp_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/UnramifiedEtaleDescent.lean, line 181. The attribute's comment: “part (5), corrected form: G separated for the étale topology; false as written, see DoubledSection.Rational.not_forall_descend”.

Stacks 04CY, the corrected part (5) of the tag. In a representable, surjective, étale situation, a formally unramified composite forces the second transformation to be formally unramified as soon as the intermediate presheaf is separated for the étale topology.

Separatedness is the whole of what is used, and it is exactly the step the tag's own proof takes: having identified two sections of G after pullback along an étale covering, that proof concludes "hence f = g as W' → T' is an étale covering".

It cannot be dropped: the tag states this part for arbitrary set-valued functors, and in that generality it is false. The counterexample is AlgebraicGeometry.Space.DoubledSection.exists_not_formallyUnramified_of_comp, which doubles the sections of the functor of points of the thickening that factor through neither the étale cover nor the thickened object. This is an erratum to the source statement.

An intermediate presheaf which is an algebraic space over S is separated for the étale topology, so AlgebraicGeometry.Space.formallyUnramified_of_formallyUnramified_comp is the special case of this result at such a presheaf, as is AlgebraicGeometry.Space.formallyUnramified_of_comp, which asks the full sheaf condition.

public theorem formallyUnramified_of_comp_of_isSeparated
    (s : RepresentableSurjectiveEtaleSituation.{u})
    (hG : Presieve.IsSeparated ((etaleTopology s.B).over (s.B.obj s.hS)) s.G)
    (hba : FormallyUnramified (s.a ≫ s.b)) :
    FormallyUnramified s.b

AlgebraicGeometry.Space.formallyUnramified_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/UnramifiedEtaleDescent.lean, line 277. The attribute's comment: “descend_formally_unramified”.

In a representable, surjective, étale situation, a formally unramified composite forces the second transformation to be formally unramified as soon as the intermediate presheaf is a sheaf for the étale topology.

This is the special case of AlgebraicGeometry.Space.formallyUnramified_of_comp_of_isSeparated at a presheaf which satisfies the full sheaf condition rather than merely separatedness, so it is a weaker statement than the corrected part (5) of Stacks 04CY, whose registration as that part sits on that result.

public theorem formallyUnramified_of_comp
    (s : RepresentableSurjectiveEtaleSituation.{u})
    (hG : Presheaf.IsSheaf ((etaleTopology s.B).over (s.B.obj s.hS)) s.G)
    (hba : FormallyUnramified (s.a ≫ s.b)) :
    FormallyUnramified s.b

AlgebraicGeometry.Space.formallyEtale_of_comp_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/UnramifiedEtaleDescent.lean, line 303. The attribute's comment: “part (6), corrected form: G a sheaf and H separated for the étale topology; false as written, see DoubledSection.Rational.not_forall_descend”.

Stacks 04CY, the corrected part (6) of the tag. In a representable, surjective, étale situation, a formally étale composite forces the second transformation to be formally étale as soon as the intermediate presheaf is a sheaf for the étale topology and the target presheaf is separated for it.

Separatedness is all that the target presheaf contributes, and it is all the tag's own proof asks of it: H enters only to compare two sections of H that already agree over an étale covering. The intermediate presheaf genuinely needs the full sheaf condition, since the proof glues the étale-local solutions produced by part (4) — "hence we may glue the local solutions to get assertion (6)" in the tag.

The tag states this part for arbitrary set-valued functors, and in that generality it is false: the situation of AlgebraicGeometry.Space.DoubledSection.exists_not_formallyUnramified_of_comp has a formally étale composite and a second transformation that is not formally étale. This is an erratum to the source statement.

public theorem formallyEtale_of_comp_of_isSeparated
    (s : RepresentableSurjectiveEtaleSituation.{u})
    (hG : Presheaf.IsSheaf ((etaleTopology s.B).over (s.B.obj s.hS)) s.G)
    (hH : Presieve.IsSeparated ((etaleTopology s.B).over (s.B.obj s.hS)) s.H)
    (hba : FormallyEtale (s.a ≫ s.b)) :
    FormallyEtale s.b

AlgebraicGeometry.Space.formallyEtale_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/UnramifiedEtaleDescent.lean, line 450. The attribute's comment: “descend_formally_etale”.

In a representable, surjective, étale situation, a formally étale composite forces the second transformation to be formally étale as soon as the intermediate and target presheaves are sheaves for the étale topology.

This is the corollary of AlgebraicGeometry.Space.formallyEtale_of_comp_of_isSeparated obtained by strengthening separatedness of the target presheaf to the full sheaf condition, so it states a special case of the corrected part (6) of Stacks 04CY, whose registration as that part sits on that result.

public theorem formallyEtale_of_comp
    (s : RepresentableSurjectiveEtaleSituation.{u})
    (hG : Presheaf.IsSheaf ((etaleTopology s.B).over (s.B.obj s.hS)) s.G)
    (hH : Presheaf.IsSheaf ((etaleTopology s.B).over (s.B.obj s.hS)) s.H)
    (hba : FormallyEtale (s.a ≫ s.b)) :
    FormallyEtale s.b

AlgebraicGeometry.Space.formallyUnramified_of_formallyUnramified_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallyUnramifiedEtaleDescent.lean, line 462. The attribute's comment: “part (5), for a middle functor which is an algebraic space”.

Let p : F ⟶ G be a representable, surjective and étale transformation of set-valued functors on the big fppf site of S, let q : G ⟶ H and let G be an algebraic space over S. If p ≫ q is formally unramified in the sense of [Stacks Project, Tag 049S], then so is q.

The corrected part (5) asks G to be separated for the étale topology, and an algebraic space is (see the implementation notes of this file), so this is a special case of AlgebraicGeometry.Space.formallyUnramified_of_comp_of_isSeparated, which carries the corrected part (5). This proof uses a hypothesis of a different kind — separatedness for the fpqc topology, which follows from the representable diagonal alone. The composition direction is AlgebraicGeometry.Space.formallyUnramified_comp_of_etale.

theorem formallyUnramified_of_formallyUnramified_comp (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (p : F ⟶ G) (q : G ⟶ H)
    (hG : IsAlgebraicSpace B S hS G)
    (hps : (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf p)
    (hpe : (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf p)
    (hpq : FormallyUnramified (p ≫ q)) :
    FormallyUnramified q

AlgebraicGeometry.Space.DoubledSection.Rational.not_forall_descend_formallyEtale_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DescentFormallyEtaleNeedsSeparatedTarget.lean, line 269. The attribute's comment: “counterexample to part (6) with G an étale sheaf and H arbitrary: the condition on H in the corrected form cannot be dropped”.

Part (6) of Stacks 04CY is false when only the intermediate functor is asked to be an étale sheaf. The universal statement "for every representable, surjective, étale a : F ⟶ G and every b : G ⟶ H with F and G étale sheaves, b is formally étale when b ∘ a is" fails, already over Spec ℚ.

So the corrected part (6), AlgebraicGeometry.Space.formallyEtale_of_comp_of_isSeparated, needs its hypothesis on the target functor H as well as its hypothesis on G; the latter is shown necessary by AlgebraicGeometry.Space.DoubledSection.Rational.not_forall_descend.

public theorem not_forall_descend_formallyEtale_of_isSheaf :
    ¬ (∀ s : RepresentableSurjectiveEtaleSituation.{0},
        Presheaf.IsSheaf ((etaleTopology s.B).over (s.B.obj s.hS)) s.F →
        Presheaf.IsSheaf ((etaleTopology s.B).over (s.B.obj s.hS)) s.G →
        FormallyEtale (s.a ≫ s.b) → FormallyEtale s.b)

AlgebraicGeometry.Space.DoubledSection.Rational.not_forall_descend, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Examples/Spaces/DescentFormallyUnramifiedNeedsSeparatedRational.lean, line 268. The attribute's comment: “counterexample to parts (5),(6) as written”.

Parts (5) and (6) of Stacks 04CY are false as written. The source states, for an arbitrary representable, surjective, étale a : F ⟶ G and any b : G ⟶ H of set-valued functors on a big fppf site, that b is formally unramified when b ∘ a is (part (5)) and formally étale when b ∘ a is (part (6)). Both universal statements fail, already over Spec ℚ.

The corrected forms are AlgebraicGeometry.Space.formallyUnramified_of_comp_of_isSeparated and AlgebraicGeometry.Space.formallyEtale_of_comp_of_isSeparated.

theorem not_forall_descend :
    ¬ (∀ s : RepresentableSurjectiveEtaleSituation.{0},
        FormallyUnramified (s.a ≫ s.b) → FormallyUnramified s.b) ∧
      ¬ (∀ s : RepresentableSurjectiveEtaleSituation.{0},
        FormallyEtale (s.a ≫ s.b) → FormallyEtale s.b)

Declarations registered for the tag:

• AlgebraicGeometry.hasPullbacks_bigAffineFppf, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/UnramifiedEtaleDescent.lean, line 93 (StacksFrontier): “fibre products in the big affine fppf site”.
• AlgebraicGeometry.preservesPullbacks_bigAffineFppfToScheme, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/UnramifiedEtaleDescent.lean, line 96 (StacksFrontier): “preservation by the big affine fppf functor to schemes”.
• AlgebraicGeometry.hasPullbacks_bigAffineFppf, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/UnramifiedEtaleDescentSupplement.lean, line 27 (StacksFrontier): “fibre products in the big affine fppf site”.
• AlgebraicGeometry.preservesPullbacks_bigAffineFppfToScheme, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/UnramifiedEtaleDescentSupplement.lean, line 30 (StacksFrontier): “preservation by the big affine fppf functor to schemes”.

Tag 04G5, a lemma

Tag 04G5 in the Stacks Project.

AlgebraicGeometry.Space.formallySmooth_of_comp_of_formallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Factor.lean, line 75. The attribute's comment: “smooth”. References: EGA IV (17.1.4), “formally smooth case”; EGA IV (17.1.5), “necessity, smooth”.

Stacks 04G5, smooth. Formal smoothness of a composite descends to its first factor when the second factor is formally unramified.

public theorem formallySmooth_of_comp_of_formallyUnramified (a : F ⟶ G) (b : G ⟶ H)
    (hb : FormallyUnramified b)
    (hba : FormallySmooth (a ≫ b)) :
    FormallySmooth a

AlgebraicGeometry.Space.formallyEtale_of_comp_of_formallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Factor.lean, line 87. The attribute's comment: “etale”. References: EGA IV (17.1.4), “formally étale case”; EGA IV (17.1.5), “necessity, étale”.

Stacks 04G5, étale case. A first factor of a formally étale transformation is formally étale if the second factor is formally unramified.

public theorem formallyEtale_of_comp_of_formallyUnramified (a : F ⟶ G) (b : G ⟶ H)
    (hb : FormallyUnramified b)
    (hba : FormallyEtale (a ≫ b)) :
    FormallyEtale a

AlgebraicGeometry.Space.formallyUnramified_left_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Factor.lean, line 101. The attribute's comment: “unramified”. References: EGA IV (17.1.3), “(v), b fmly unramified”; EGA IV (17.1.5), “necessity, unramified”.

Stacks Project, Tag 04G5, unramified case. If a transformation and a composite ending in it are formally unramified, so is the first factor.

public theorem formallyUnramified_left_of_comp (a : F ⟶ G) (b : G ⟶ H)
    (_hb : FormallyUnramified b)
    (hba : FormallyUnramified (a ≫ b)) :
    FormallyUnramified a

Sources

• Section 76.13, Tag 04G3
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.FormallySmooth · AlgebraicGeometry.Space.FormallyEtale · AlgebraicGeometry.Space.FormallyUnramified · AlgebraicGeometry.Space.formallyEtale_iff_formallySmooth_and_formallyUnramified · AlgebraicGeometry.Space.FormallySmooth.comp · AlgebraicGeometry.Space.formallyEtale_comp · AlgebraicGeometry.Space.formallyUnramified_comp · AlgebraicGeometry.Space.FormallySmooth.baseChange

Section76.14 Formally unramified morphisms#

Section 76.14 of the Stacks Project, Tag 04G6. 9 tags here are carried by 16 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04G7, a definition

Tag 04G7 in the Stacks Project.

AlgebraicGeometry.Space.FormallyUnramified, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Defs.lean, line 90. The attribute's comment: “formally unramified morphism of algebraic spaces”. References: SGA 3 XI (1.6), “formally unramified”.

Stacks 049S, part (3). Every commutative affine square against a square-zero closed immersion admits at most one lift.

public abbrev FormallyUnramified {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type v} (a : F ⟶ G) :
    Prop

Tag 04G8, a lemma

Tag 04G8 in the Stacks Project.

AlgebraicGeometry.Space.formallyUnramified_iff_etaleCharts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/UnramifiedChartCriterion.lean, line 102. The attribute's comment: “equivalence of (1) and (2)”.

Stacks 04G8, the equivalence of (1) and (2). A morphism of algebraic spaces over S is formally unramified exactly when the morphism of schemes underlying every commuting square of étale scheme charts is formally unramified.

public theorem formallyUnramified_iff_etaleCharts
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    FormallyUnramified f ↔
      HoldsOnEveryEtaleChart B S hS
        (@_root_.AlgebraicGeometry.FormallyUnramified.{u} : MorphismProperty Scheme.{u}) f

AlgebraicGeometry.Space.formallyUnramified_iff_surjectiveEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/UnramifiedChartCriterion.lean, line 119. The attribute's comment: “equivalence of (1) and (3)”.

Stacks 04G8, the equivalence of (1) and (3). A morphism of algebraic spaces over S is formally unramified exactly when there is one commuting square of étale scheme charts, both chart maps surjective, whose underlying morphism of schemes is formally unramified.

public theorem formallyUnramified_iff_surjectiveEtaleChart
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    FormallyUnramified f ↔
      ∃ (U V : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X) (b : yoneda.obj V ⟶ Y) (ψ : U ⟶ V),
        (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf a ∧
        (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf b ∧
        (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf a ∧
        (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf b ∧
        yoneda.map ψ ≫ b = a ≫ f ∧
        _root_.AlgebraicGeometry.FormallyUnramified
          ((BigFppfOver.toScheme B S hS).map ψ)

AlgebraicGeometry.Space.holdsOnEveryEtaleChart_of_formallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallyUnramifiedEtaleCharts.lean, line 561. The attribute's comment: “condition (1) implies condition (2)”.

Stacks 04G8, condition (1) implies condition (2). A formally unramified morphism of presheaves on the big fppf site of S is formally unramified on every commuting square of étale scheme charts.

No algebraicity hypothesis on the source or target is needed, and none is imposed.

theorem holdsOnEveryEtaleChart_of_formallyUnramified (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X ⟶ Y)
    (hf : FormallyUnramified f) :
    HoldsOnEveryEtaleChart B S hS
      (@_root_.AlgebraicGeometry.FormallyUnramified.{u} : MorphismProperty Scheme.{u}) f

AlgebraicGeometry.Space.exists_surjectiveEtaleChart_of_holdsOnEveryEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallyUnramifiedEtaleCharts.lean, line 578. The attribute's comment: “condition (2) implies condition (3)”.

Stacks 04G8, condition (2) implies condition (3). If a morphism of algebraic spaces over S is formally unramified on every commuting square of étale scheme charts, then there is one such square whose two chart morphisms are in addition surjective.

The square is produced from a surjective étale chart of the target, which exists by AlgebraicGeometry.IsAlgebraicSpace.exists_atlas, and its lift to the source, which is [Stacks Project, Tag 02X1].

theorem exists_surjectiveEtaleChart_of_holdsOnEveryEtaleChart (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hall : HoldsOnEveryEtaleChart B S hS
      (@_root_.AlgebraicGeometry.FormallyUnramified.{u} : MorphismProperty Scheme.{u}) f) :
    ∃ (U V : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X) (b : yoneda.obj V ⟶ Y) (h : U ⟶ V),
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf a ∧
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf b ∧
      (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf a ∧
      (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf b ∧
      yoneda.map h ≫ b = a ≫ f ∧
      _root_.AlgebraicGeometry.FormallyUnramified
        ((BigFppfOver.toScheme B S hS).map h)

AlgebraicGeometry.Space.formallyUnramified_of_surjectiveEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallyUnramifiedEtaleDescent.lean, line 491. The attribute's comment: “condition (3) implies condition (1)”.

Stacks 04G8, condition (3) implies condition (1). If a morphism f out of an algebraic space over S has one commuting square of surjective étale scheme charts whose chart morphism is formally unramified as a morphism of schemes, then f is formally unramified in the sense of [Stacks Project, Tag 049S].

The composite of the chart of the source with f is formally unramified by AlgebraicGeometry.Space.formallyUnramified_chart_comp, and AlgebraicGeometry.Space.formallyUnramified_of_formallyUnramified_comp descends that along the chart. Together with AlgebraicGeometry.Space.holdsOnEveryEtaleChart_of_formallyUnramified and AlgebraicGeometry.Space.exists_surjectiveEtaleChart_of_holdsOnEveryEtaleChart it makes all three conditions of the tag equivalent.

theorem formallyUnramified_of_surjectiveEtaleChart (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (f : X ⟶ Y)
    (hex : ∃ (U V : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X) (b : yoneda.obj V ⟶ Y)
      (h : U ⟶ V),
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf a ∧
      (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf b ∧
      (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf a ∧
      (MorphismProperty.inverseImage (@Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf b ∧
      yoneda.map h ≫ b = a ≫ f ∧
      _root_.AlgebraicGeometry.FormallyUnramified
        ((BigFppfOver.toScheme B S hS).map h)) :
    FormallyUnramified f

Tag 05ZY, a lemma

Tag 05ZY in the Stacks Project.

AlgebraicGeometry.Space.FormallyUnramified.lifts_unique_of_firstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/UnramifiedThickenings.lean, line 132.

Stacks 05ZY. A formally unramified morphism f : X ⟶ Y of algebraic spaces over S admits at most one dotted arrow in a solid square over a first-order thickening T ⊂ T' of algebraic spaces over S. In other words the affineness of the test objects in the definition of formal unramifiedness, Stacks 049S part (3), may be dropped.

theorem FormallyUnramified.lifts_unique_of_firstOrderThickening
    {X Y T' : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : FormallyUnramified f.hom)
    (T : Subfunctor T'.obj) (hT : IsFirstOrderThickening B S hS T' T)
    (a : T.toFunctor ⟶ X.obj) (b : T'.obj ⟶ Y.obj) (hsq : a ≫ f.hom = T.ι ≫ b)
    (z₁ z₂ : T'.obj ⟶ X.obj)
    (hz₁a : T.ι ≫ z₁ = a) (hz₁b : z₁ ≫ f.hom = b)
    (hz₂a : T.ι ≫ z₂ = a) (hz₂b : z₂ ≫ f.hom = b) :
    z₁ = z₂

Tag 05ZZ, a lemma

Tag 05ZZ in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.Space.formallyUnramified_comp, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Spaces.lean, line 64 (StacksFrontier).

Tag 0600, a lemma

Tag 0600 in the Stacks Project.

AlgebraicGeometry.Space.formallyUnramified_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/UnramifiedBaseChange.lean, line 53. References: EGA IV (17.1.3), “more general”.

Stacks 0600. A base change of a formally unramified morphism of algebraic spaces is formally unramified: in a cartesian square with f formally unramified, the opposite side p of the square is formally unramified.

This is also the first assertion of Stacks 060B: in a fibre product diagram Z = X ×_Y W of algebraic spaces over S with h' : W ⟶ Y formally unramified (here f), the morphism h : Z ⟶ X (here p) is formally unramified.

theorem formallyUnramified_of_isPullback
    {F G H P : AlgebraicSpaces B S hS}
    (f : F ⟶ G) (g : H ⟶ G) (p : P ⟶ H) (q : P ⟶ F)
    (sq : IsPullback p q g f)
    (unramified : FormallyUnramified f.hom) :
    FormallyUnramified p.hom

Tag 04G9, a lemma

Tag 04G9 in the Stacks Project.

AlgebraicGeometry.Space.formallyUnramified_iff_isZero_sheafOfDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallyUnramifiedSheafOfDifferentials.lean, line 268. References: EGA IV (17.2.1), “more general”.

Stacks 04G9. A morphism f : X ⟶ Y of algebraic spaces over S is formally unramified exactly when its sheaf of differentials Ω_{X/Y} is a zero object.

The invertibility clause of Stacks 04CS, read at zero objects for an arbitrary morphism of schemes of the site, is AlgebraicGeometry.Space.sheafOfDifferentialsSchemeVanishing; Stacks 04CU turns it into the chart-square comparison that the proof consumes, AlgebraicGeometry.Space.sheafOfDifferentialsChartComparison, and AlgebraicGeometry.Space.formallyUnramified_iff_isZero_sheafOfDifferentials_of_chart is the proof proper; see there.

theorem formallyUnramified_iff_isZero_sheafOfDifferentials {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) :
    FormallyUnramified f.hom ↔ IsZero (sheafOfDifferentials B S hS f)

Tag 04GA, a lemma

Tag 04GA in the Stacks Project.

AlgebraicGeometry.Space.isUnramified_tfae_sheafOfDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedSheafOfDifferentials.lean, line 111.

Stacks 04GA. For a morphism f : X ⟶ Y of algebraic spaces over a scheme S the following are equivalent:

1. f is unramified,
2. f is locally of finite type and Ω_{X/Y} = 0,
3. f is locally of finite type and formally unramified.

(1) ⟺ (3) is AlgebraicGeometry.Space.isUnramified_iff_isLocallyOfFiniteType_and_formallyUnramified, and (1) ⟺ (2) is AlgebraicGeometry.Space.isUnramified_iff_isLocallyOfFiniteType_and_isZero_sheafOfDifferentials.

theorem isUnramified_tfae_sheafOfDifferentials (f : X ⟶ Y) :
    List.TFAE [IsUnramified B S hS f.hom,
      IsLocallyOfFiniteType B S hS f.hom ∧ IsZero (sheafOfDifferentials B S hS f),
      IsLocallyOfFiniteType B S hS f.hom ∧ FormallyUnramified f.hom]

Tag 05W6, a lemma

Tag 05W6 in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_isLocallyQuasiFinite_of_isLocallyOfFiniteType_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedMonoCriteria.lean, line 243. The attribute's comment: “separated and locally quasi-finite, from condition (3)”.

Stacks 0463. A monomorphism of algebraic spaces over S which is locally of finite type is separated and locally quasi-finite.

Separatedness is [Stacks Project, Tag 042N], already available as AlgebraicGeometry.Space.isSeparated_of_mono; local quasi-finiteness goes through unramifiedness, which a monomorphism locally of finite type has by AlgebraicGeometry.Space.isUnramified_of_isLocallyOfFiniteType_of_mono.

These are two of the three assertions of the "moreover" clause of [Stacks Project, Tag 05W6], reached from its condition (3); the equivalence of conditions (1) and (3) carries them over to condition (1), and the two unconditional equivalences below carry them over to conditions (2) and (4).

theorem isSeparated_isLocallyQuasiFinite_of_isLocallyOfFiniteType_mono (f : X ⟶ Y)
    (h : IsLocallyOfFiniteType B S hS f ∧ Mono f) :
    IsSeparated B S hS f ∧ IsLocallyQuasiFinite B S hS f

AlgebraicGeometry.Space.isUnramified_mono_iff_isUnramified_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedMonoCriteria.lean, line 261. The attribute's comment: “conditions (1) and (2)”. References: EGA IV (17.2.6), “(b) => (a)”.

Stacks 05W6, conditions (1) and (2). A morphism of algebraic spaces over S is unramified and a monomorphism if and only if it is unramified and universally injective.

The forward implication is AlgebraicGeometry.Space.isUnramified_universallyInjective_of_isUnramified_mono. The converse is AlgebraicGeometry.Space.mono_of_isOpenImmersion_diagonal_of_universallyInjective, whose open-immersion input is part (1) of [Stacks Project, Tag 05W1], specialised to f; that is AlgebraicGeometry.Space.isOpenImmersion_diagonal_of_isUnramified.

theorem isUnramified_mono_iff_isUnramified_universallyInjective
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    (IsUnramified B S hS f ∧ Mono f) ↔
      (IsUnramified B S hS f ∧ UniversallyInjective B S hS f)

AlgebraicGeometry.Space.isUnramified_mono_iff_universallyInjective_locallyOfFiniteType_formallyUnramified, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedMonoCriteria.lean, line 287. The attribute's comment: “conditions (1) and (4)”.

Stacks 05W6, conditions (1) and (4). A morphism of algebraic spaces over S is unramified and a monomorphism if and only if it is universally injective, locally of finite type and formally unramified.

The forward implication is, in this namespace, universallyInjective_isLocallyOfFiniteType_formallyUnramified_of_isUnramified_mono. For the converse, local finite type together with formal unramifiedness on étale charts is unramifiedness, which is the available half of [Stacks Project, Tag 04GA]; passing from AlgebraicGeometry.Space.FormallyUnramified to the chart condition is condition (1) implies condition (2) of [Stacks Project, Tag 04G8], supplied by AlgebraicGeometry.Space.holdsOnEveryEtaleChart_of_formallyUnramified of StacksFrontier.AlgebraicGeometry.Spaces.FormallyUnramifiedEtaleCharts. The monomorphism is then obtained as in AlgebraicGeometry.Space.isUnramified_mono_iff_isUnramified_universallyInjective, from part (1) of [Stacks Project, Tag 05W1]. Both inputs being available, this equivalence is unconditional and carries the tag.

theorem isUnramified_mono_iff_universallyInjective_locallyOfFiniteType_formallyUnramified
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    (IsUnramified B S hS f ∧ Mono f) ↔
      (UniversallyInjective B S hS f ∧ IsLocallyOfFiniteType B S hS f ∧
        FormallyUnramified (B := B) (S := S) (hS := hS) f)

AlgebraicGeometry.Space.isUnramified_mono_iff_isLocallyOfFiniteType_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedMonomorphism.lean, line 202. The attribute's comment: “conditions (1) and (3)”.

Stacks 05W6, conditions (1) and (3). A morphism of algebraic spaces over S is unramified and a monomorphism if and only if it is locally of finite type and a monomorphism.

theorem isUnramified_mono_iff_isLocallyOfFiniteType_mono
    (_hX : IsAlgebraicSpace B S hS X) (_hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    (IsUnramified B S hS f ∧ Mono f) ↔ (IsLocallyOfFiniteType B S hS f ∧ Mono f)

AlgebraicGeometry.Space.isUnramified_mono_tfae_and_relativelyRepresentable_isSeparated_isLocallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedMonoRepresentable.lean, line 89.

Stacks 05W6. Let f : X ⟶ Y be a morphism of algebraic spaces over a scheme S. The following are equivalent:

1. f is unramified and a monomorphism,
2. f is unramified and universally injective,
3. f is locally of finite type and a monomorphism,
4. f is universally injective, locally of finite type and formally unramified.

Moreover, in that case f is representable, separated and locally quasi-finite.

The equivalences run through condition (1). The "moreover" clause is taken at condition (3): separatedness and local quasi-finiteness are [Stacks Project, Tag 0463], and representability follows from them by [Stacks Project, Tag 0418].

theorem isUnramified_mono_tfae_and_relativelyRepresentable_isSeparated_isLocallyQuasiFinite
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    List.TFAE
      [IsUnramified B S hS f ∧ Mono f,
        IsUnramified B S hS f ∧ UniversallyInjective B S hS f,
        IsLocallyOfFiniteType B S hS f ∧ Mono f,
        UniversallyInjective B S hS f ∧ IsLocallyOfFiniteType B S hS f ∧
          FormallyUnramified (B := B) (S := S) (hS := hS) f] ∧
      ((IsUnramified B S hS f ∧ Mono f) →
        yoneda.relativelyRepresentable f ∧ IsSeparated B S hS f ∧
          IsLocallyQuasiFinite B S hS f)

Tag 05W8, a lemma

Tag 05W8 in the Stacks Project.

AlgebraicGeometry.Space.closedImmersion_conditions_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionCriteria.lean, line 153. References: SGA 3 V (4.1.3).

The five equivalent conditions characterizing closed immersions of algebraic spaces.

public theorem closedImmersion_conditions_tfae
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE
      [IsClosedImmersion B S hS f,
       UniversallyClosed B S hS f ∧
         (IsUnramified B S hS f ∧ Mono f),
       UniversallyClosed B S hS f ∧
         (IsUnramified B S hS f ∧
           UniversallyInjective B S hS f),
       UniversallyClosed B S hS f ∧
         (IsLocallyOfFiniteType B S hS f ∧ Mono f),
       UniversallyClosed B S hS f ∧
         (UniversallyInjective B S hS f ∧
           (IsLocallyOfFiniteType B S hS f ∧
             FormallyUnramified f))]

Sources

• Section 76.14, Tag 04G6
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Space.FormallyUnramified · AlgebraicGeometry.Space.formallyUnramified_iff_etaleCharts · AlgebraicGeometry.Space.formallyUnramified_iff_surjectiveEtaleChart · AlgebraicGeometry.Space.holdsOnEveryEtaleChart_of_formallyUnramified · AlgebraicGeometry.Space.exists_surjectiveEtaleChart_of_holdsOnEveryEtaleChart · AlgebraicGeometry.Space.formallyUnramified_of_surjectiveEtaleChart · AlgebraicGeometry.Space.FormallyUnramified.lifts_unique_of_firstOrderThickening · AlgebraicGeometry.Space.formallyUnramified_comp

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.