65.3 Representable morphisms of… to 65.13 Separation conditions on…

Section65.3 Representable morphisms of presheaves #

Section 65.3 of the Stacks Project, Tag 025U. 6 tags here are carried by 3 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02W9, a lemma

Tag 02W9 in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.Functor.relativelyRepresentable.map registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable.lean, line 59 (StacksFrontier): “for the Yoneda embedding of a category with fibre products, h_f is representable”.

Tag 02WA, a lemma

Tag 02WA in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.Functor.relativelyRepresentable.isMultiplicative registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable.lean, line 63 (StacksFrontier): “representable transformations are stable under composition”.

Tag 02WB, a lemma

Tag 02WB in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.Functor.relativelyRepresentable.isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable.lean, line 66 (StacksFrontier): “representable transformations are stable under base change”.

Tag 02WC, a lemma

Tag 02WC in the Stacks Project.

AlgebraicGeometry.Space.relativelyRepresentable_prod_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Products.lean, line 44.

Stacks Project, Tag 02WC. The product of two representable transformations of presheaves on the big fppf site over S is representable.

public theorem relativelyRepresentable_prod_map
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F₁ G₁ F₂ G₂ : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (a₁ : F₁ ⟶ G₁) (a₂ : F₂ ⟶ G₂)
    (h₁ : yoneda.relativelyRepresentable a₁) (h₂ : yoneda.relativelyRepresentable a₂) :
    yoneda.relativelyRepresentable (prod.map a₁ a₂)

Tag 02WD, a lemma

Tag 02WD in the Stacks Project.

AlgebraicGeometry.Space.isSheaf_of_relativelyRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Sheaf.lean, line 39.

A representable transformation into a sheaf on the big fppf site over S has a sheaf as its source.

public theorem isSheaf_of_relativelyRepresentable
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (a : F ⟶ G) (ha : yoneda.relativelyRepresentable a)
    (hG : Presheaf.IsSheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) G) :
    Presheaf.IsSheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) F

Tag 05L9, a lemma

Tag 05L9 in the Stacks Project.

AlgebraicGeometry.Space.relativelyRepresentable_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Diagonal.lean, line 36.

The diagonal of a representable transformation of presheaves on the big fppf site over S is representable.

public theorem relativelyRepresentable_diagonal
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (a : F ⟶ G) (ha : yoneda.relativelyRepresentable a) :
    yoneda.relativelyRepresentable (pullback.diagonal a)

Sources

LeanCategoryTheory.Functor.relativelyRepresentable.map · CategoryTheory.Functor.relativelyRepresentable.isMultiplicative · CategoryTheory.Functor.relativelyRepresentable.isStableUnderBaseChange · AlgebraicGeometry.Space.relativelyRepresentable_prod_map · AlgebraicGeometry.Space.isSheaf_of_relativelyRepresentable · AlgebraicGeometry.Space.relativelyRepresentable_diagonal

Section65.4 Lists of useful properties of morphisms of schemes #

Section 65.4 of the Stacks Project, Tag 02WE. 3 tags here are carried by 49 declarations of the repository (all in StacksFrontier) and 67 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02WF, a remark

Tag 02WF in the Stacks Project.

AlgebraicGeometry.Space.finitePresentation_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 200. The attribute's comment: “finite_presentation”.

Morphisms of schemes of finite presentation remain of finite presentation after arbitrary base change.

public instance finitePresentation_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (@AlgebraicGeometry.FinitePresentation.{u})

AlgebraicGeometry.Space.finiteType_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeFiniteType.lean, line 43. The attribute's comment: “of_finite_type”.

Morphisms of schemes of finite type remain of finite type after arbitrary base change.

public instance finiteType_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      ((@LocallyOfFiniteType : MorphismProperty Scheme.{u}) ⊓ @QuasiCompact)

AlgebraicGeometry.Space.quasiFinite_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeQuasiFinite.lean, line 42. The attribute's comment: “quasi_finite”. References: EGA II (6.2.4).

Quasi-finite morphisms of schemes remain quasi-finite after arbitrary base change.

public instance quasiFinite_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange
      (((@LocallyOfFiniteType : MorphismProperty Scheme.{u}) ⊓ @QuasiCompact) ⊓
        @LocallyQuasiFinite)

Declarations registered for the tag:

AlgebraicGeometry.isAffineHom_isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 82 (StacksFrontier): “affine”. References: EGA II (1.5.1); EGA II (1.5.5), “more general”; EGA II (1.6.2); EGA IV (14.5.11), “Necessity direction”; EGA IV (2.7.1), “(xiii)”; SGA 1 VIII (2.1), “partial”; SGA 1 VIII (5.6), “necessity”; SGA 3 I (4.6.4.1), “partial”; SGA 3 III (0.1.7), “(a)”; SGA 3 III (0.17), “partial”; SGA 3 VIB (10.1), “partial”; SGA 3 XIX (2.1), “more general”; SGA 4 VIII (5.1), “partial”.
AlgebraicGeometry.Etale.etale_isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 97 (StacksFrontier): “etale”. References: EGA IV (17.3.3), “(iii), étale case”; EGA IV (17.7.3), “(ii)”; SGA 1 I (4.6); SGA 1 IX (1.3); SGA 1 IX (4.2), “Étaleness of X₁' → S₁'”; SGA 3 VIB (10.1), “partial”; SGA 3 VIB (2.1.2), “partial”; SGA 3 VIIB (1.6.C), “special case”; SGA 4 VII (1.4), “partial”; SGA 4½ Arcata (2.1.3).
AlgebraicGeometry.IsFinite.instIsStableUnderBaseChangeScheme registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 99 (StacksFrontier): “finite”. References: EGA I (6.4.12), “more general”; EGA I (6.4.6), “more general”; EGA II (6.1.5), “(iii), finite branch”; EGA III (2.6.2.1), “more general”; EGA IV (2.7.1), “implication”; EGA IV (21.10.16), “f₁ is finite”; SGA 1 VIII (5.7), “preservation (finite)”; SGA 1 VIII (6.6); SGA 3 VIB (10.1), “partial”; SGA 4 VIII (5.4), “more general”.
AlgebraicGeometry.locallyOfFiniteType_isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 113 (StacksFrontier): “finite_type”. References: EGA I (10.13.5), “(ii)”; EGA I (6.3.4), “clause (iv)”; EGA I (6.6.6); EGA II (3.5.5), “partial”; EGA IV (1.3.4); EGA IV (2.7.1), “(iii)”; SGA 3 VIB (2.1.2), “partial”.
AlgebraicGeometry.Flat.isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 115 (StacksFrontier): “flat”. References: EGA III (7.7.2), “special case”; EGA III (7.9.7), “special case”; EGA IV (11.5.4), “necessity”; EGA IV (2.1.4); EGA IV (2.2.13), “(i)”; EGA IV (2.5.1), “special case”; EGA IV (20.6.9), “flatness of X' over S'”; EGA IV (21.15.9), “partial”; EGA IV (7.3.5), “partial”; SGA 3 III (0.13), “partial”; SGA 3 VIB (10.1), “partial”; SGA 3 VIB (11.1); SGA 3 VIB (2.1.2), “partial”; SGA 3 VIB (3.11), “fiber-flatness”; SGA 3 VIIB (1.3.3), “(iii), special case”; SGA 3 XIX (2.1); SGA 4 Vbis (3.3), “special case”; SGA 6 0 (2.9), “special case”; SGA 6 XII (2.3), “(a)”; SGA 6 XII (4.1), “(1)”; SGA 7 VII (1.3.8), “partial”.
AlgebraicGeometry.gUnramified_isStableUnderBaseChange, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 117 (StacksFrontier): “g_unramified”.
AlgebraicGeometry.IsIntegralHom.instIsStableUnderBaseChangeScheme registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 119 (StacksFrontier): “integral”. References: EGA II (6.1.5), “(iii), integral branch”; EGA IV (2.7.1), “implication”; SGA 1 VIII (5.7), “preservation (integral)”.
AlgebraicGeometry.locallyOfFinitePresentation_isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 127 (StacksFrontier): “locally_finite_presentation”. References: EGA IV (1.4.3); EGA IV (2.7.1), “(iv)”; EGA IV (20.6.9), “partial”; EGA IV (21.15.9), “partial”; EGA IV (8.6.2), “partial”; SGA 3 VIB (5.6.1.0), “partial”.
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.monomorphisms registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 130 (StacksFrontier): “monomorphism”. References: EGA I (3.3.12), “more general”; EGA IV (2.7.1), “(ix)”; SGA 3 IV (4.5.7), “more general”; SGA 3 VIB (10.1), “monomorphisms”.
AlgebraicGeometry.IsProper.isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 133 (StacksFrontier): “proper”. References: EGA II (5.4.2), “more general”; EGA III (4.3.4), “more general”; EGA IV (2.7.1), “implication”; SGA 1 IX (2.4), “partial”; SGA 1 VIII (4.8), “partial”; SGA 3 VIB (10.1), “partial”; SGA 6 X (7.5), “partial”.
AlgebraicGeometry.quasiSeparated_isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 135 (StacksFrontier): “quasi_separated”. References: EGA IV (1.2.2); EGA IV (2.7.1), “(ii)”; SGA 4 VI (1.8), “(ii), special case”; SGA 4 VI (1.9.1), “(ii), special case”; SGA 4 VIII (5.1), “partial”; SGA 7 VII (1.3.8), “partial”.
AlgebraicGeometry.IsSeparated.isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 137 (StacksFrontier): “separated”. References: EGA I (10.15.3), “(iii), special case”; EGA I (5.5.1); EGA I (5.5.3), “more general”; EGA III (6.9.1), “separatedness of f′_i”; EGA III (7.7.2), “separatedness of f'”; EGA IV (2.7.1), “implication”; SGA 1 IX (2.4), “partial”; SGA 1 IX (4.2), “partial”; SGA 1 VIII (4.8), “partial”; SGA 3 VIB (10.1), “separatedness”.
AlgebraicGeometry.smooth_isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 149 (StacksFrontier): “smooth”. References: EGA IV (17.3.3), “smooth branch of (iii)”; EGA IV (17.7.3), “(ii)”; EGA IV (6.8.2), “globally smooth f”; EGA IV (6.8.3), “more general”; SGA 1 II (1.3), “more general”; SGA 1 II (4.13), “global ascent”; SGA 3 VIB (10.1), “smooth morphisms”; SGA 3 VIB (2.1.2), “partial”; SGA 3 XIX (2.1), “(i)”; SGA 6 VIII (1.6), “partial”; SGA 6 VIII (1.8), “partial”; SGA 6 X (7.13.3), “partial”.
AlgebraicGeometry.Surjective.instIsStableUnderBaseChangeScheme registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 151 (StacksFrontier): “surjective”. References: EGA I (3.5.2); SGA 1 VIII (3.1), “Surjectivity clause”; SGA 3 VIB (10.1), “partial, sufficiency”; SGA 3 VIIB (2.4.1), “special case”.
CategoryTheory.MorphismProperty.universally_isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 160 (StacksFrontier): “universal_homeomorphism”. References: EGA IV (14.3.4), “(ii), special case”; EGA IV (2.4.3), “more general”; EGA IV (2.6.4), “partial”; SGA 1 IX (4.2), “partial”; SGA 1 VIII (4.7), “more general”; SGA 3 IV (1.11), “partial”; SGA 4 VI (1.9.1), “more general”.
AlgebraicGeometry.universallyClosed_isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 174 (StacksFrontier): “universally_closed”. References: EGA II (5.4.9), “5.4.2(iii)”; EGA IV (2.4.3), “(iii)”; EGA IV (2.6.4), “(ii)”; SGA 1 IX (2.4), “partial”; SGA 1 VIII (4.7), “necessity”; SGA 3 V (6.1), “partial”.
AlgebraicGeometry.UniversallyInjective.isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 176 (StacksFrontier): “universally_injective”. References: SGA 3 VIB (10.1), “partial, sufficiency”; SGA 3 VIB (2.6), “more general”.
AlgebraicGeometry.UniversallyOpen.instIsStableUnderBaseChangeScheme registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 179 (StacksFrontier): “universally_open”. References: EGA IV (14.3.4), “(ii), global form”; EGA IV (2.4.3), “(iii), universally open”; EGA IV (2.6.4), “necessity in (i)”; SGA 1 IX (2.4), “partial”; SGA 1 VIII (4.7), “necessity”; SGA 3 V (6.1), “special case”; SGA 3 VIB (2.1.2), “partial”.
AlgebraicGeometry.unramified_isStableUnderBaseChange, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChange.lean, line 195 (StacksFrontier): “unramified”.
AlgebraicGeometry.quasiCompact_isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeClauses.lean, line 30 (StacksFrontier): “quasi_compact”. References: EGA I (6.3.4), “clause (iv)”; EGA I (6.6.4); EGA III (6.9.1), “partial”; EGA III (6.9.4), “more general”; EGA III (7.7.2), “quasi-compactness of f'”; EGA IV (1.1.2); EGA IV (2.3.7), “(i)”; EGA IV (2.6.4), “necessity in (v)”; SGA 1 VIII (3.3), “quasi-compact clause”; SGA 4 VI (1.8), “(ii), special case”; SGA 4 VI (1.9.1), “(ii), special case”; SGA 4 VIII (5.1), “partial”; SGA 7 VII (1.3.8), “partial”.
CategoryTheory.MorphismProperty.universally_isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeClauses.lean, line 32 (StacksFrontier): “universally_submersive”. References: EGA IV (14.3.4), “(ii), special case”; EGA IV (2.4.3), “more general”; EGA IV (2.6.4), “partial”; SGA 1 IX (4.2), “partial”; SGA 1 VIII (4.7), “more general”; SGA 3 IV (1.11), “partial”; SGA 4 VI (1.9.1), “more general”.
AlgebraicGeometry.instIsStableUnderBaseChangeSchemeLocallyQuasiFinite registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeLocallyQuasiFinite.lean, line 24 (StacksFrontier): “locally_quasi_finite”. References: EGA II (6.2.4), “(iii)”; SGA 3 V (7.4), “special case”; SGA 3 VIB (10.1), “sufficiency”; SGA 3 VIB (2.8), “(i) ⇒ (ii), partial”.
AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeRemainingClauses.lean, line 67 (StacksFrontier): “closed immersion”. References: EGA I (10.14.5), “(ii), ordinary schemes”; EGA I (4.3.1), “special case”; EGA I (4.3.2); EGA I (4.5.5), “(iii), special case”; EGA II (8.10.2), “j′ is a closed immersion”; EGA IV (17.13.1), “closed immersions”; EGA IV (2.7.1), “implication”; EGA IV (8.6.2), “more general”; SGA 1 VIII (5.5), “closed-immersion clause”; SGA 3 VIB (10.1), “partial”; SGA 4 XII (4.3), “Parenthetical clause”.
AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeRemainingClauses.lean, line 70 (StacksFrontier): “open immersion”. References: EGA I (4.3.1), “special case”; EGA I (4.3.2); EGA I (4.5.5), “(iii), special case”; EGA IV (11.9.5), “Geometric clause”; EGA IV (2.7.1), “(x)”; SGA 1 VIII (5.5), “open-immersion clause”; SGA 3 VIB (10.1), “open immersions”; SGA 6 VIII (1.6), “partial”.
AlgebraicGeometry.IsImmersion.isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeRemainingClauses.lean, line 73 (StacksFrontier): “locally closed immersion”. References: EGA I (4.3.1), “special case”; EGA I (4.3.2); EGA I (4.5.5), “(iii), special case”; EGA II (3.8.1), “Immersion clause”; EGA IV (17.13.1); SGA 3 VIB (10.1), “partial”.
AlgebraicGeometry.isQuasiAffineHom_isStableUnderBaseChange, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeRemainingClauses.lean, line 76 (StacksFrontier): “quasi_affine”.
AlgebraicGeometry.syntomic_isStableUnderBaseChange, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeRemainingClauses.lean, line 78 (StacksFrontier): “syntomic”.
Stacks.Morphisms.isFiniteLocallyFree_isStableUnderBaseChange, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeRemainingClauses.lean, line 80 (StacksFrontier): “finite_locally_free”.
AlgebraicGeometry.IsProjectiveMorphism.baseChange, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeRemainingClauses.lean, line 83 (StacksFrontier): “h_projective”.
AlgebraicGeometry.isStableUnderBaseChange_isProjective, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeRemainingClauses.lean, line 85 (StacksFrontier): “projective”.
AlgebraicGeometry.IsLocallyProjective.pullback_fst, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeRemainingClauses.lean, line 87 (StacksFrontier): “locally_projective”.
AlgebraicGeometry.RelativeDimension.of_isPullback, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/BaseChangeRemainingClauses.lean, line 89 (StacksFrontier): “relative_dimension_d”.

Tag 02WG, a remark

Tag 02WG in the Stacks Project.

AlgebraicGeometry.Space.universalHomeomorphism_isStableUnderComposition, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 180. The attribute's comment: “universal_homeomorphism”.

Universal homeomorphisms of schemes are stable under composition.

public instance universalHomeomorphism_isStableUnderComposition :
    MorphismProperty.IsStableUnderComposition
      (@AlgebraicGeometry.UniversalHomeomorphism.{u} : MorphismProperty Scheme.{u})

AlgebraicGeometry.Space.universallySubmersive_isStableUnderComposition, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 191. The attribute's comment: “universally_submersive”.

The composite of universally submersive morphisms of schemes is universally submersive.

public instance universallySubmersive_isStableUnderComposition :
    (topologically @Topology.IsQuotientMap :
      MorphismProperty Scheme.{u}).universally.IsStableUnderComposition

Declarations registered for the tag:

AlgebraicGeometry.instIsAffineHomCompScheme registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 83 (StacksFrontier): “affine”. References: EGA II (1.3.5); EGA II (1.3.6), “partial”; EGA II (1.6.2).
AlgebraicGeometry.Etale.etale_comp registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 88 (StacksFrontier): “etale”. References: EGA IV (17.3.3), “(ii), étale case”; EGA IV (17.3.5), “étale clause”; SGA 1 I (4.6); SGA 1 V (3.3), “special case”.
AlgebraicGeometry.IsFinite.instIsStableUnderCompositionScheme registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 90 (StacksFrontier): “finite_integral”. References: EGA II (6.1.5), “(ii), finite branch”; EGA IV (21.10.15), “Condition a)”.
AlgebraicGeometry.IsIntegralHom.instIsStableUnderCompositionScheme registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 96 (StacksFrontier): “finite_integral”. References: EGA II (6.1.5), “(ii), integral branch”.
AlgebraicGeometry.locallyOfFinitePresentation_comp registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 101 (StacksFrontier): “finite_presentation”. References: EGA IV (1.4.3); SGA 6 III (1.14), “special case”.
AlgebraicGeometry.quasiCompact_comp registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 103 (StacksFrontier): “finite_presentation”. References: EGA I (6.6.4); EGA IV (1.1.2); SGA 4 VI (1.8), “(i), special case”; SGA 4 VI (1.9.1), “(i), special case”.
AlgebraicGeometry.quasiSeparated_comp registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 109 (StacksFrontier): “finite_presentation”. References: EGA IV (1.2.2); SGA 4 VI (1.8), “(i), special case”; SGA 4 VI (1.9.1), “(i), special case”.
AlgebraicGeometry.Flat.comp registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 114 (StacksFrontier): “flat”. References: EGA 0 (6.7.5), “Schemes (EGA preschemes)”; EGA IV (2.1.5), “global case Y' = Y”; EGA IV (2.1.6); EGA IV (2.2.11), “(iii), special case”; EGA IV (2.2.13), “(iii)”; EGA IV (6.6.1), “(i): flatness of h = g∘f”; EGA IV (7.3.5), “partial”; SGA 3 VIIB (1.3.3), “(i), special case”.
AlgebraicGeometry.IsClosedImmersion.comp registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 116 (StacksFrontier): “immersions”. References: EGA I (10.14.5), “(i), ordinary schemes”; EGA I (4.1.6); EGA I (4.2.5); EGA I (4.5.5), “(i), special case”.
AlgebraicGeometry.IsOpenImmersion.comp registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 122 (StacksFrontier): “immersions”. References: EGA I (4.2.5); EGA I (4.5.5), “(i), special case”.
AlgebraicGeometry.IsImmersion.comp registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 126 (StacksFrontier): “immersions”. References: EGA I (4.1.6); EGA I (4.2.5); EGA I (4.5.5), “(i), special case”.
CategoryTheory.mono_comp registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 131 (StacksFrontier): “monomorphisms”.
AlgebraicGeometry.IsProper.stableUnderComposition registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 133 (StacksFrontier): “proper”. References: EGA II (5.4.2).
AlgebraicGeometry.quasiCompact_isStableUnderComposition registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 135 (StacksFrontier): “quasi_compact”. References: EGA I (6.6.4); EGA IV (1.1.2); SGA 4 VI (1.8), “(i), special case”; SGA 4 VI (1.9.1), “(i), special case”.
AlgebraicGeometry.quasiSeparated_isStableUnderComposition registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 141 (StacksFrontier): “quasi_separated”. References: EGA IV (1.2.2); SGA 4 VI (1.8), “(i), special case”; SGA 4 VI (1.9.1), “(i), special case”.
AlgebraicGeometry.IsSeparated.stableUnderComposition registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 148 (StacksFrontier): “separated”. References: EGA I (10.15.3), “(i), ordinary preschemes”; EGA I (5.5.1).
AlgebraicGeometry.smooth_comp registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 153 (StacksFrontier): “smooth”. References: EGA IV (17.3.3), “smooth branch of (ii)”; EGA IV (6.8.3), “more general”; SGA 1 II (1.3), “more general”.
AlgebraicGeometry.instSurjectiveCompScheme registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 158 (StacksFrontier): “surjective”. References: EGA I (2.2.7).
AlgebraicGeometry.universallyClosed_isStableUnderComposition registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 161 (StacksFrontier): “universally_closed”. References: EGA II (5.4.9), “5.4.2(ii)”; EGA IV (2.4.3), “(ii)”.
AlgebraicGeometry.universallyInjective_isStableUnderComposition registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 164 (StacksFrontier): “universally_injective”. References: EGA I (3.5.6); EGA IV (6.15.3.1), “(i), special case”.
AlgebraicGeometry.UniversallyOpen.instCompScheme registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 170 (StacksFrontier): “universally_open”. References: EGA IV (14.3.4), “(i), special case”; EGA IV (2.4.3), “(ii), universally open”.
AlgebraicGeometry.unramified_isStableUnderComposition, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 174 (StacksFrontier): “unramified”.
AlgebraicGeometry.gUnramified_isStableUnderComposition, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Composition.lean, line 176 (StacksFrontier): “unramified”.
Stacks.Morphisms.isFiniteLocallyFree_comp, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/CompositionClauses.lean, line 40 (StacksFrontier): “finite_locally_free”.
AlgebraicGeometry.IsProjectiveMorphism.comp, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/CompositionClauses.lean, line 42 (StacksFrontier): “h_projective”.
AlgebraicGeometry.isQuasiAffineHom_isStableUnderComposition, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/CompositionClauses.lean, line 44 (StacksFrontier): “quasi_affine”.
AlgebraicGeometry.locallyQuasiFinite_conditions_comp, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/CompositionClauses.lean, line 47 (StacksFrontier): “quasi_finite”.
AlgebraicGeometry.quasiFinite_conditions_comp, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/CompositionClauses.lean, line 49 (StacksFrontier): “quasi_finite”.
AlgebraicGeometry.syntomic_isStableUnderComposition, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/CompositionClauses.lean, line 51 (StacksFrontier): “syntomic”.
AlgebraicGeometry.locallyOfFiniteType_comp registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/CompositionFiniteType.lean, line 23 (StacksFrontier): “finite_type”. References: EGA I (10.13.5), “(i), special case”; EGA I (6.3.4), “clause (ii)”; EGA I (6.6.6); EGA IV (1.3.4).
AlgebraicGeometry.quasiCompact_comp registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/CompositionFiniteType.lean, line 29 (StacksFrontier): “finite_type”. References: EGA I (6.6.4); EGA IV (1.1.2); SGA 4 VI (1.8), “(i), special case”; SGA 4 VI (1.9.1), “(i), special case”.

Tag 02WH, a remark

Tag 02WH in the Stacks Project.

AlgebraicGeometry.etale_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleFpqcLocalAtTarget.lean, line 73. The attribute's comment: “etale”. References: SGA 3 VIB (2.1.2), “partial”.

Étaleness of morphisms of schemes is fpqc local on the base.

instance etale_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@Etale : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

AlgebraicGeometry.etale_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleFpqcLocalAtTarget.lean, line 84. The attribute's comment: “etale”.

Étaleness of morphisms of schemes is fppf local on the base.

instance etale_isLocalAtTarget_fppf :
    MorphismProperty.IsLocalAtTarget (@Etale : MorphismProperty Scheme.{u})
      Scheme.fppfPrecoverage

Stacks.Descent.isClosedImmersion_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 95. The attribute's comment: “entry (1)(a): closed immersions”. References: SGA 1 VIII (5.5), “more general”; SGA 3 VIB (12.1), “more general”; SGA 4 IV (8.5.5).

Stacks 02WH, entry (1)(a): being a closed immersion is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem isClosedImmersion_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@IsClosedImmersion : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@IsClosedImmersion : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@IsClosedImmersion : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.isOpenImmersion_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 111. The attribute's comment: “entry (1)(b): open immersions”. References: EGA IV (2.7.1), “more general”; SGA 1 VIII (5.5), “more general”; SGA 4 IV (8.5.5).

Stacks 02WH, entry (1)(b): being an open immersion is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem isOpenImmersion_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@IsOpenImmersion : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@IsOpenImmersion : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@IsOpenImmersion : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.isImmersion_inf_quasiCompact_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 126. The attribute's comment: “entry (1)(c): quasi-compact immersions”. References: EGA IV (2.7.1), “more general”; SGA 4 IV (8.5.5).

Stacks 02WH, entry (1)(c): being a quasi-compact immersion is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem
    isImmersion_inf_quasiCompact_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange
        (@IsImmersion ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@IsImmersion ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@IsImmersion ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.quasiCompact_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 143. The attribute's comment: “entry (2): quasi-compact”.

Stacks 02WH, entry (2): being quasi-compact is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem quasiCompact_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@QuasiCompact : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@QuasiCompact : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@QuasiCompact : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.universallyClosed_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 158. The attribute's comment: “entry (3): universally closed”. References: EGA IV (2.6.4), “more general”.

Stacks 02WH, entry (3): being universally closed is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem universallyClosed_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@UniversallyClosed : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@UniversallyClosed : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@UniversallyClosed : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.isSeparated_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 173. The attribute's comment: “entry (4): separated”.

Stacks 02WH, entry (4), separated case: being separated is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem isSeparated_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@IsSeparated : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@IsSeparated : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@IsSeparated : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.quasiSeparated_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 186. The attribute's comment: “entry (4): quasi-separated”.

Stacks 02WH, entry (4), quasi-separated case: being quasi-separated is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem quasiSeparated_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@QuasiSeparated : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@QuasiSeparated : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@QuasiSeparated : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.monomorphisms_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 201. The attribute's comment: “entry (5): monomorphism”. References: SGA 4 IV (8.5.5).

Stacks 02WH, entry (5): being a monomorphism is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem monomorphisms_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (MorphismProperty.monomorphisms Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (MorphismProperty.monomorphisms Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (MorphismProperty.monomorphisms Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.surjective_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 216. The attribute's comment: “entry (6): surjective”. References: SGA 4 IV (8.5.5).

Stacks 02WH, entry (6): being surjective is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem surjective_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@Surjective : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@Surjective : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@Surjective : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.universallyInjective_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 231. The attribute's comment: “entry (7): universally injective”.

Stacks 02WH, entry (7): being universally injective is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem universallyInjective_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@UniversallyInjective : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@UniversallyInjective : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@UniversallyInjective : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.isAffineHom_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 246. The attribute's comment: “entry (8): affine”.

Stacks 02WH, entry (8): being affine is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem isAffineHom_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@IsAffineHom : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@IsAffineHom : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@IsAffineHom : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.isQuasiAffineHom_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 261. The attribute's comment: “entry (9): quasi-affine”.

Stacks 02WH, entry (9): being quasi-affine is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem isQuasiAffineHom_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@IsQuasiAffineHom : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@IsQuasiAffineHom : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@IsQuasiAffineHom : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.locallyOfFiniteType_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 276. The attribute's comment: “entry (10): locally of finite type”.

Stacks 02WH, entry (10), locally of finite type case: being locally of finite type is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem locallyOfFiniteType_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@LocallyOfFiniteType : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@LocallyOfFiniteType : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@LocallyOfFiniteType : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.finiteType_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 289. The attribute's comment: “entry (10): of finite type”.

Stacks 02WH, entry (10), finite type case: being of finite type is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem finiteType_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange
        (@LocallyOfFiniteType ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@LocallyOfFiniteType ⊓ @QuasiCompact : MorphismProperty Scheme.{u})
          Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@LocallyOfFiniteType ⊓ @QuasiCompact : MorphismProperty Scheme.{u})
          Scheme.fppfPrecoverage

Stacks.Descent.locallyOfFiniteType_inf_locallyQuasiFinite_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 307. The attribute's comment: “entry (11): locally quasi-finite”.

Stacks 02WH, entry (11), locally quasi-finite case: being locally quasi-finite is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem
  locallyOfFiniteType_inf_locallyQuasiFinite_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange
        (@LocallyOfFiniteType ⊓ @LocallyQuasiFinite : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@LocallyOfFiniteType ⊓ @LocallyQuasiFinite : MorphismProperty Scheme.{u})
          Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@LocallyOfFiniteType ⊓ @LocallyQuasiFinite : MorphismProperty Scheme.{u})
          Scheme.fppfPrecoverage

Stacks.Descent.finiteType_inf_locallyQuasiFinite_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 324. The attribute's comment: “entry (11): quasi-finite”.

Stacks 02WH, entry (11), quasi-finite case: being quasi-finite is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem
    finiteType_inf_locallyQuasiFinite_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange
        ((@LocallyOfFiniteType ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) ⊓
          @LocallyQuasiFinite) ∧
      MorphismProperty.IsLocalAtTarget
          ((@LocallyOfFiniteType ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) ⊓
            @LocallyQuasiFinite) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          ((@LocallyOfFiniteType ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) ⊓
            @LocallyQuasiFinite) Scheme.fppfPrecoverage

Stacks.Descent.locallyOfFinitePresentation_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 345. The attribute's comment: “entry (12): locally of finite presentation”. References: SGA 4 IV (8.5.5), “partial”.

Stacks 02WH, entry (12), locally of finite presentation case: being locally of finite presentation is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem locallyOfFinitePresentation_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange
        (@LocallyOfFinitePresentation : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@LocallyOfFinitePresentation : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@LocallyOfFinitePresentation : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.finitePresentation_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 359. The attribute's comment: “entry (12): of finite presentation”. References: SGA 4 IV (8.5.5).

Stacks 02WH, entry (12), finite presentation case: being of finite presentation is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem finitePresentation_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@FinitePresentation : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@FinitePresentation : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@FinitePresentation : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.locallyOfFiniteTypeRelativeDimension_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 374. The attribute's comment: “entry (13): locally of finite type of relative dimension d”.

Stacks 02WH, entry (13): being locally of finite type of relative dimension d is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem
    locallyOfFiniteTypeRelativeDimension_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf
    (d : ℕ) :
    MorphismProperty.IsStableUnderBaseChange (locallyOfFiniteTypeRelativeDimension.{u} d) ∧
      MorphismProperty.IsLocalAtTarget
          (locallyOfFiniteTypeRelativeDimension.{u} d) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (locallyOfFiniteTypeRelativeDimension.{u} d) Scheme.fppfPrecoverage

Stacks.Descent.universallyOpen_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 391. The attribute's comment: “entry (14): universally open”. References: EGA IV (2.6.4), “more general”; SGA 4 IV (8.5.5).

Stacks 02WH, entry (14): being universally open is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem universallyOpen_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@UniversallyOpen : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@UniversallyOpen : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@UniversallyOpen : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.flat_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 406. The attribute's comment: “entry (15): flat”.

Stacks 02WH, entry (15): being flat is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem flat_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@Flat : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@Flat : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@Flat : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.syntomic_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 421. The attribute's comment: “entry (16): syntomic”.

Stacks 02WH, entry (16): being syntomic is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem syntomic_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@Syntomic : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@Syntomic : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@Syntomic : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.smooth_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 436. The attribute's comment: “entry (17): smooth”. References: SGA 3 VIB (2.1.2); SGA 3 VIIA (8.3.1), “partial”.

Stacks 02WH, entry (17): being smooth is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem smooth_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@Smooth : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@Smooth : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@Smooth : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.unramified_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 451. The attribute's comment: “entry (18): unramified”.

Stacks 02WH, entry (18), unramified case: being unramified is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem unramified_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@Unramified : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@Unramified : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@Unramified : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.gUnramified_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 464. The attribute's comment: “entry (18): G-unramified”.

Stacks 02WH, entry (18), G-unramified case: being G-unramified is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem gUnramified_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@GUnramified : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@GUnramified : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@GUnramified : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.etale_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 479. The attribute's comment: “entry (19): etale”.

Stacks 02WH, entry (19): being étale is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem etale_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@Etale : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@Etale : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@Etale : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.isProper_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 495. The attribute's comment: “entry (20): proper”. References: SGA 4 IV (8.5.5).

Stacks 02WH, entry (20) of the list: proper, Descent, Lemma 02L1. The source's "proper" is AlgebraicGeometry.IsProper in Lean. Being proper is stable under arbitrary base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem isProper_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@IsProper : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@IsProper : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@IsProper : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.isFinite_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 510. The attribute's comment: “entry (21): finite”.

Stacks 02WH, entry (21), finite case: being finite is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem isFinite_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@IsFinite : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@IsFinite : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@IsFinite : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.isIntegralHom_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 523. The attribute's comment: “entry (21): integral”.

Stacks 02WH, entry (21), integral case: being integral is stable under base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem isIntegralHom_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange (@IsIntegralHom : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@IsIntegralHom : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@IsIntegralHom : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.isFiniteLocallyFree_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 540. The attribute's comment: “entry (22): finite locally free”. References: SGA 1 VIII (5.7), “more general”.

Stacks 02WH, entry (22) of the list: finite locally free, Descent, Lemma 02VO, with the rank left unconstrained. The source's "finite locally free" is Stacks.Morphisms.IsFiniteLocallyFree in Lean. Being finite locally free is stable under arbitrary base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem isFiniteLocallyFree_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange
        (@Stacks.Morphisms.IsFiniteLocallyFree : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@Stacks.Morphisms.IsFiniteLocallyFree : MorphismProperty Scheme.{u})
          Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@Stacks.Morphisms.IsFiniteLocallyFree : MorphismProperty Scheme.{u})
          Scheme.fppfPrecoverage

Stacks.Descent.isFiniteLocallyFreeOfRank_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 559. The attribute's comment: “entry (22): finite locally free of rank d”. References: SGA 1 VIII (5.7), “special case”.

Stacks 02WH, entry (22) of the list: finite locally free, Descent, Lemma 02VO, for a fixed rank d. The source's "finite locally free" of rank d is Stacks.Morphisms.IsFiniteLocallyFreeOfRank.property d in Lean. Being finite locally free of rank d is stable under arbitrary base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem
    isFiniteLocallyFreeOfRank_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf
    (d : ℕ) :
    MorphismProperty.IsStableUnderBaseChange
        (Stacks.Morphisms.IsFiniteLocallyFreeOfRank.property.{u} d) ∧
      MorphismProperty.IsLocalAtTarget
          (Stacks.Morphisms.IsFiniteLocallyFreeOfRank.property.{u} d) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (Stacks.Morphisms.IsFiniteLocallyFreeOfRank.property.{u} d) Scheme.fppfPrecoverage

Stacks.Descent.universallyQuotientMap_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 583. The attribute's comment: “entry (23): universally submersive”. References: EGA IV (15.7.11.1), “fpqc-locality conjunct”; SGA 1 IX (4.2), “partial”.

Stacks 02WH, entry (23) of the list: universally submersive, Descent, Lemma 0CEW. A submersive morphism is one whose underlying map of topological spaces is a quotient map, so the source's "universally submersive" is in Lean (topologically Topology.IsQuotientMap).universally — the Lean name universallyQuotientMap denotes exactly the source's "universally submersive". That property is stable under arbitrary base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem universallyQuotientMap_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange
        ((topologically @Topology.IsQuotientMap : MorphismProperty Scheme.{u}).universally) ∧
      MorphismProperty.IsLocalAtTarget
          ((topologically @Topology.IsQuotientMap : MorphismProperty Scheme.{u}).universally)
          Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          ((topologically @Topology.IsQuotientMap : MorphismProperty Scheme.{u}).universally)
          Scheme.fppfPrecoverage

Stacks.Descent.universalHomeomorphism_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 605. The attribute's comment: “entry (24): universal homeomorphism”. References: EGA IV (2.6.2), “(iv), special case”; EGA IV (2.6.4), “more general”; SGA 1 VIII (4.7), “more general”; SGA 4 IV (8.5.5).

Stacks 02WH, entry (24) of the list: universal homeomorphism, Descent, Lemma 0CEX. The source's "universal homeomorphism" is AlgebraicGeometry.UniversalHomeomorphism in Lean. Being a universal homeomorphism is stable under arbitrary base change, fpqc local on the base, and a fortiori fppf local on the base.

public theorem universalHomeomorphism_isStableUnderBaseChange_and_isLocalAtTarget_fpqc_fppf :
    MorphismProperty.IsStableUnderBaseChange
        (@UniversalHomeomorphism : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget
          (@UniversalHomeomorphism : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (@UniversalHomeomorphism : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.isImmersion_isStableUnderBaseChange_and_isLocalAtTarget_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Entries.lean, line 630. The attribute's comment: “last sentence (02YM): immersions are fppf local on the base”. References: EGA II (3.8.1), “more general”.

Stacks 02WH, the closing sentence of the remark: immersions are fppf local on the base, Descent, Lemma 02YM. Being an immersion is stable under base change, and it is fppf local on the base — that fppf locality is exactly the content of 02YM, which the remark's last sentence cites. The remark records explicitly that being an immersion may not be fpqc local on the base, so no fpqc conjunct is asserted here; only the three cases of entry (1) — closed, open and quasi-compact immersions — are claimed fpqc local.

public theorem isImmersion_isStableUnderBaseChange_and_isLocalAtTarget_fppf :
    MorphismProperty.IsStableUnderBaseChange (@IsImmersion : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget (@IsImmersion : MorphismProperty Scheme.{u})
        Scheme.fppfPrecoverage

Stacks.Descent.fpqcAndFppfLocalOnBase_allEntries_and_isImmersion_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FppfLocalOnBase/Remark.lean, line 111. The attribute's comment: “The remark in full, as one conjunction in the source's order: entry (n) is the n-th conjunct, and each conjunct states that the property that entry names is stable under arbitrary base change, local on the base for the fpqc precoverage, and a fortiori local on the base for the fppf precoverage. Entry (1) is the conjunction of its three cases, (a) closed, (b) open and (c) quasi-compact immersions; each entry with two readings, namely (4), (10), (11), (12), (18), (21) and (22), is the conjunction of both readings; and entries (13) and (22) are quantified over their numerical parameter. The twenty-fifth and last conjunct is the remark's closing sentence: being an immersion is stable under arbitrary base change and local on the base for the fppf precoverage, which is Descent, Lemma 02YM.”. References: EGA IV (17.3.3), “(iii)”; EGA IV (2.6.4), “more general”; EGA IV (2.7.1), “more general”; SGA 1 IX (2.4), “special case”; SGA 1 IX (4.2), “Étaleness”; SGA 1 VIII (5.5), “more general”; SGA 3 IV (4.7), “(a)”; SGA 3 IV (6.4.1); SGA 3 VIB (2.1.2); SGA 3 VIIA (8.3.1), “Smoothness entry (17)”; SGA 3 XI (6.8), “partial”.

Stacks Project, Remark 02WH, in full. Of the properties of morphisms of schemes which are stable under base change, the following twenty-four are also fpqc local on the base, and a fortiori fppf local on the base:

immersions, in the three cases (a) closed immersions (Descent, Lemma 02L6), (b) open immersions (Descent, Lemma 02L3), and (c) quasi-compact immersions (Descent, Lemma 02L8);

quasi-compact (Descent, Lemma 02KQ);

universally closed (Descent, Lemma 02KS);

(quasi-)separated (Descent, Lemmas 02KR and 02KU);

monomorphism (Descent, Lemma 02YK);

surjective (Descent, Lemma 02KV);

universally injective (Descent, Lemma 02KW);

affine (Descent, Lemma 02L5);

quasi-affine (Descent, Lemma 02L7);

(locally) of finite type (Descent, Lemmas 02KX and 02KZ);

(locally) quasi-finite (Descent, Lemma 02VI);

(locally) of finite presentation (Descent, Lemmas 02KY and 02L0);

locally of finite type of relative dimension d (Descent, Lemma 02VJ);

universally open (Descent, Lemma 02KT);

flat (Descent, Lemma 02L2);

syntomic (Descent, Lemma 02VK);

smooth (Descent, Lemma 02VL);

unramified, resp. G-unramified (Descent, Lemma 02VM);

étale (Descent, Lemma 02VN);

proper (Descent, Lemma 02L1);

finite or integral (Descent, Lemma 02LA);

finite locally free (Descent, Lemma 02VO), with the rank unconstrained or fixed;

universally submersive (Descent, Lemma 0CEW);

universal homeomorphism (Descent, Lemma 0CEX).

The final conjunct is the remark's last sentence: the property of being an immersion may not be fpqc local on the base, but it is stable under base change and fppf local on the base, by Descent, Lemma 02YM. No fpqc locality is asserted of immersions in general.

public theorem fpqcAndFppfLocalOnBase_allEntries_and_isImmersion_fppf :
    -- entry (1)(a), (b), (c): closed, open and quasi-compact immersions
    ((MorphismProperty.IsStableUnderBaseChange (@IsClosedImmersion : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@IsClosedImmersion : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@IsClosedImmersion : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
      (MorphismProperty.IsStableUnderBaseChange (@IsOpenImmersion : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@IsOpenImmersion : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@IsOpenImmersion : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
      (MorphismProperty.IsStableUnderBaseChange
           (@IsImmersion ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@IsImmersion ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@IsImmersion ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage)) ∧
    -- entry (2): quasi-compact
    (MorphismProperty.IsStableUnderBaseChange (@QuasiCompact : MorphismProperty Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (@QuasiCompact : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (@QuasiCompact : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- entry (3): universally closed
    (MorphismProperty.IsStableUnderBaseChange (@UniversallyClosed : MorphismProperty Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (@UniversallyClosed : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (@UniversallyClosed : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- entry (4): separated, and quasi-separated
    ((MorphismProperty.IsStableUnderBaseChange (@IsSeparated : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@IsSeparated : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@IsSeparated : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
      (MorphismProperty.IsStableUnderBaseChange (@QuasiSeparated : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@QuasiSeparated : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@QuasiSeparated : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage)) ∧
    -- entry (5): monomorphism
    (MorphismProperty.IsStableUnderBaseChange (MorphismProperty.monomorphisms Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (MorphismProperty.monomorphisms Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (MorphismProperty.monomorphisms Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- entry (6): surjective
    (MorphismProperty.IsStableUnderBaseChange (@Surjective : MorphismProperty Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (@Surjective : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (@Surjective : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- entry (7): universally injective
    (MorphismProperty.IsStableUnderBaseChange
         (@UniversallyInjective : MorphismProperty Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (@UniversallyInjective : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (@UniversallyInjective : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- entry (8): affine
    (MorphismProperty.IsStableUnderBaseChange (@IsAffineHom : MorphismProperty Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (@IsAffineHom : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (@IsAffineHom : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- entry (9): quasi-affine
    (MorphismProperty.IsStableUnderBaseChange (@IsQuasiAffineHom : MorphismProperty Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (@IsQuasiAffineHom : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (@IsQuasiAffineHom : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- entry (10): locally of finite type, and of finite type
    ((MorphismProperty.IsStableUnderBaseChange
           (@LocallyOfFiniteType : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@LocallyOfFiniteType : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@LocallyOfFiniteType : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
      (MorphismProperty.IsStableUnderBaseChange
           (@LocallyOfFiniteType ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@LocallyOfFiniteType ⊓ @QuasiCompact : MorphismProperty Scheme.{u})
           Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@LocallyOfFiniteType ⊓ @QuasiCompact : MorphismProperty Scheme.{u})
           Scheme.fppfPrecoverage)) ∧
    -- entry (11): locally quasi-finite, and quasi-finite
    ((MorphismProperty.IsStableUnderBaseChange
           (@LocallyOfFiniteType ⊓ @LocallyQuasiFinite : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@LocallyOfFiniteType ⊓ @LocallyQuasiFinite : MorphismProperty Scheme.{u})
           Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@LocallyOfFiniteType ⊓ @LocallyQuasiFinite : MorphismProperty Scheme.{u})
           Scheme.fppfPrecoverage) ∧
      (MorphismProperty.IsStableUnderBaseChange
           ((@LocallyOfFiniteType ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) ⊓
             @LocallyQuasiFinite) ∧
       MorphismProperty.IsLocalAtTarget
           ((@LocallyOfFiniteType ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) ⊓
             @LocallyQuasiFinite) Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           ((@LocallyOfFiniteType ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) ⊓
             @LocallyQuasiFinite) Scheme.fppfPrecoverage)) ∧
    -- entry (12): locally of finite presentation, and of finite presentation
    ((MorphismProperty.IsStableUnderBaseChange
           (@LocallyOfFinitePresentation : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@LocallyOfFinitePresentation : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@LocallyOfFinitePresentation : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
      (MorphismProperty.IsStableUnderBaseChange
           (@FinitePresentation : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@FinitePresentation : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@FinitePresentation : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage)) ∧
    -- entry (13): locally of finite type of relative dimension `d`
    (∀ d : ℕ,
      MorphismProperty.IsStableUnderBaseChange (locallyOfFiniteTypeRelativeDimension.{u} d) ∧
      MorphismProperty.IsLocalAtTarget
          (locallyOfFiniteTypeRelativeDimension.{u} d) Scheme.fpqcPrecoverage ∧
      MorphismProperty.IsLocalAtTarget
          (locallyOfFiniteTypeRelativeDimension.{u} d) Scheme.fppfPrecoverage) ∧
    -- entry (14): universally open
    (MorphismProperty.IsStableUnderBaseChange (@UniversallyOpen : MorphismProperty Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (@UniversallyOpen : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (@UniversallyOpen : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- entry (15): flat
    (MorphismProperty.IsStableUnderBaseChange (@Flat : MorphismProperty Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (@Flat : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (@Flat : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- entry (16): syntomic
    (MorphismProperty.IsStableUnderBaseChange (@Syntomic : MorphismProperty Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (@Syntomic : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (@Syntomic : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- entry (17): smooth
    (MorphismProperty.IsStableUnderBaseChange (@Smooth : MorphismProperty Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (@Smooth : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (@Smooth : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- entry (18): unramified, and G-unramified
    ((MorphismProperty.IsStableUnderBaseChange (@Unramified : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@Unramified : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@Unramified : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
      (MorphismProperty.IsStableUnderBaseChange (@GUnramified : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@GUnramified : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@GUnramified : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage)) ∧
    -- entry (19): étale
    (MorphismProperty.IsStableUnderBaseChange (@Etale : MorphismProperty Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (@Etale : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (@Etale : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- entry (20): proper
    (MorphismProperty.IsStableUnderBaseChange (@IsProper : MorphismProperty Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (@IsProper : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (@IsProper : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- entry (21): finite, and integral
    ((MorphismProperty.IsStableUnderBaseChange (@IsFinite : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@IsFinite : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@IsFinite : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
      (MorphismProperty.IsStableUnderBaseChange (@IsIntegralHom : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@IsIntegralHom : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@IsIntegralHom : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage)) ∧
    -- entry (22): finite locally free, of unconstrained and of fixed rank
    ((MorphismProperty.IsStableUnderBaseChange
           (@Stacks.Morphisms.IsFiniteLocallyFree : MorphismProperty Scheme.{u}) ∧
       MorphismProperty.IsLocalAtTarget
           (@Stacks.Morphisms.IsFiniteLocallyFree : MorphismProperty Scheme.{u})
           Scheme.fpqcPrecoverage ∧
       MorphismProperty.IsLocalAtTarget
           (@Stacks.Morphisms.IsFiniteLocallyFree : MorphismProperty Scheme.{u})
           Scheme.fppfPrecoverage) ∧
      (∀ d : ℕ,
        MorphismProperty.IsStableUnderBaseChange
            (Stacks.Morphisms.IsFiniteLocallyFreeOfRank.property.{u} d) ∧
        MorphismProperty.IsLocalAtTarget
            (Stacks.Morphisms.IsFiniteLocallyFreeOfRank.property.{u} d) Scheme.fpqcPrecoverage ∧
        MorphismProperty.IsLocalAtTarget
            (Stacks.Morphisms.IsFiniteLocallyFreeOfRank.property.{u} d) Scheme.fppfPrecoverage)) ∧
    -- entry (23): universally submersive
    (MorphismProperty.IsStableUnderBaseChange
         ((topologically @Topology.IsQuotientMap : MorphismProperty Scheme.{u}).universally) ∧
     MorphismProperty.IsLocalAtTarget
         ((topologically @Topology.IsQuotientMap : MorphismProperty Scheme.{u}).universally)
         Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         ((topologically @Topology.IsQuotientMap : MorphismProperty Scheme.{u}).universally)
         Scheme.fppfPrecoverage) ∧
    -- entry (24): universal homeomorphism
    (MorphismProperty.IsStableUnderBaseChange
         (@UniversalHomeomorphism : MorphismProperty Scheme.{u}) ∧
     MorphismProperty.IsLocalAtTarget
         (@UniversalHomeomorphism : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage ∧
     MorphismProperty.IsLocalAtTarget
         (@UniversalHomeomorphism : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage) ∧
    -- the last sentence (02YM): immersions in general are fppf local on the base, and no fpqc
    -- locality is claimed of them
    (MorphismProperty.IsStableUnderBaseChange (@IsImmersion : MorphismProperty Scheme.{u}) ∧
      MorphismProperty.IsLocalAtTarget (@IsImmersion : MorphismProperty Scheme.{u})
        Scheme.fppfPrecoverage)

Stacks.Descent.locallyOfFiniteType_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Diagonal.lean, line 238. The attribute's comment: “locally_finite_type”.

Stacks 02WH. Being locally of finite type is fppf local on the base.

instance locallyOfFiniteType_isLocalAtTarget_fppf :
    MorphismProperty.IsLocalAtTarget
      (@AlgebraicGeometry.LocallyOfFiniteType : MorphismProperty AlgebraicGeometry.Scheme.{u})
      AlgebraicGeometry.Scheme.fppfPrecoverage

AlgebraicGeometry.instIsLocalAtTargetFppfMonomorphisms, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/FpqcLocal.lean, line 81. The attribute's comment: “monomorphism”. References: SGA 4 IV (8.5.5), “special case”.

Monomorphisms of schemes are local on the target for the fppf precoverage.

instance instIsLocalAtTargetFppfMonomorphisms :
    (MorphismProperty.monomorphisms Scheme).IsLocalAtTarget Scheme.fppfPrecoverage

AlgebraicGeometry.surjective_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/FpqcLocal.lean, line 92. The attribute's comment: “surjective”. References: SGA 4 IV (8.5.5).

Stacks Project, Tag 02WH (surjective). Surjectivity of scheme morphisms is local on the target for the fpqc precoverage.

public instance surjective_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@Surjective.{u}) Scheme.fpqcPrecoverage

AlgebraicGeometry.surjective_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/FpqcLocal.lean, line 119. The attribute's comment: “surjective”.

Stacks Project, Tag 02WH (surjective). Surjectivity of scheme morphisms is local on the target for the fppf precoverage.

public instance surjective_isLocalAtTarget_fppf :
    MorphismProperty.IsLocalAtTarget (@Surjective.{u}) Scheme.fppfPrecoverage

AlgebraicGeometry.universallyInjective_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/FpqcLocal.lean, line 224. The attribute's comment: “universally_injective”.

Universal injectivity of morphisms of schemes is fpqc local on the target.

public instance universallyInjective_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (@UniversallyInjective : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage

AlgebraicGeometry.universallyInjective_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/FpqcLocal.lean, line 253. The attribute's comment: “universally_injective”.

Universal injectivity of morphisms of schemes is fppf local on the target.

public instance universallyInjective_isLocalAtTarget_fppf :
    MorphismProperty.IsLocalAtTarget
      (@UniversallyInjective : MorphismProperty Scheme.{u}) Scheme.fppfPrecoverage

Stacks.Descent.quasiCompact_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/QuasiCompactLocal.lean, line 66. The attribute's comment: “quasi_compact”.

Stacks 02WH. Quasi-compactness of a morphism of schemes is fppf local on the base.

public instance quasiCompact_isLocalAtTarget_fppf :
    MorphismProperty.IsLocalAtTarget (@QuasiCompact : MorphismProperty Scheme.{u})
      Scheme.fppfPrecoverage

Declarations registered for the tag:

MorphismProperty.IsStableUnderBaseChange.monomorphisms registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/FpqcLocal.lean, line 75 (StacksFrontier): “monomorphism”.
AlgebraicGeometry.isLocalAtTarget_monomorphisms_fpqc, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/FpqcLocal.lean, line 77 (StacksFrontier): “monomorphism”.
AlgebraicGeometry.Surjective.instIsStableUnderBaseChangeScheme registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/FpqcLocal.lean, line 87 (StacksFrontier): “surjective”. References: EGA I (3.5.2); SGA 1 VIII (3.1), “Surjectivity clause”; SGA 3 VIB (10.1), “partial, sufficiency”; SGA 3 VIIB (2.4.1), “special case”.
AlgebraicGeometry.UniversallyInjective.isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/FpqcLocal.lean, line 219 (StacksFrontier): “universally_injective”. References: SGA 3 VIB (10.1), “partial, sufficiency”; SGA 3 VIB (2.6), “more general”.

Sources

LeanAlgebraicGeometry.Space.finitePresentation_isStableUnderBaseChange · AlgebraicGeometry.Space.finiteType_isStableUnderBaseChange · AlgebraicGeometry.Space.quasiFinite_isStableUnderBaseChange · AlgebraicGeometry.isAffineHom_isStableUnderBaseChange · AlgebraicGeometry.Etale.etale_isStableUnderBaseChange · AlgebraicGeometry.IsFinite.instIsStableUnderBaseChangeScheme · AlgebraicGeometry.locallyOfFiniteType_isStableUnderBaseChange · AlgebraicGeometry.Flat.isStableUnderBaseChange

Section65.5 Properties of representable morphisms of presheaves #

Section 65.5 of the Stacks Project, Tag 02WI. 11 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 9 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 025V, a definition

Tag 025V in the Stacks Project.

AlgebraicGeometry.Space.HasSchemeProperty, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RepresentableProperty.lean, line 107.

Stacks 025V. A representable map of presheaves a : F ⟶ G on the big fppf site of S has property P, for P a property of morphisms of schemes, when for every object U of the site and every ξ : h_U ⟶ G the resulting morphism of schemes V_ξ ⟶ U has P.

abbrev Space.HasSchemeProperty (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty Scheme.{u}) {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) :
    Prop

Declarations registered for the tag:

CategoryTheory.MorphismProperty.presheaf registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/RepresentableProperty.lean, line 93 (StacksFrontier): “a representable map of presheaves has a property of morphisms of schemes when every represented base change of it has that property”.

Tag 02YN, a remark

Tag 02YN in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.MorphismProperty.presheaf registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Presentation/Surjective.lean, line 63 (StacksFrontier): “surjectivity after representable base change, the default for morphisms of algebraic spaces”.
CategoryTheory.Presheaf.isLocallySurjective_bot, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Presentation/Surjective.lean, line 65 (StacksFrontier): “objectwise surjectivity of a map of presheaves”.
CategoryTheory.Sheaf.IsLocallySurjective registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Presentation/Surjective.lean, line 67 (StacksFrontier): “local surjectivity of a map of sheaves”.

Tag 02WJ, a lemma

Tag 02WJ in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.MorphismProperty.relative_map_iff registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch65.lean, line 31 (StacksFrontier): “h_f has the relative property P if and only if f has P, for P stable under base change; stated for any fully faithful functor preserving fibre products”.

Tag 02WK, a lemma

Tag 02WK in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.MorphismProperty.relative_isStableUnderComposition registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch65.lean, line 35 (StacksFrontier): “the relative property attached to P is stable under composition when P is; stated for any fully faithful functor”.

Tag 02WL, a lemma

Tag 02WL in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.MorphismProperty.relative_isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch65.lean, line 27 (StacksFrontier). References: SGA 4 VI (1.9.1), “more general”.

Tag 03KD, a lemma

Tag 03KD in the Stacks Project.

AlgebraicGeometry.Space.presheaf_of_isLocallySurjective_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Presentation/Descent.lean, line 46.

A morphism property of a representable transformation descends along a transformation which becomes surjective after fppf sheafification.

theorem presheaf_of_isLocallySurjective_pullback (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (P : MorphismProperty Scheme.{u})
    [P.IsStableUnderBaseChange] [P.IsLocalAtTarget Scheme.fppfPrecoverage]
    {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (a : F ⟶ G) (b : H ⟶ G)
    (ha : yoneda.relativelyRepresentable a)
    (hb : Presheaf.IsLocallySurjective (BigFppfOver.topology B S hS) b)
    (hbase : (P.inverseImage (BigFppfOver.toScheme B S hS)).presheaf (pullback.snd a b)) :
    (P.inverseImage (BigFppfOver.toScheme B S hS)).presheaf a

Tag 02WM, a lemma

Tag 02WM in the Stacks Project.

AlgebraicGeometry.Space.hasSchemeProperty_prod_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable/Product.lean, line 55.

Stacks 02WM. Let P be a property of morphisms of schemes which is stable under composition. If two representable morphisms of presheaves a₁ : F₁ ⟶ G₁ and a₂ : F₂ ⟶ G₂ on the big fppf site of S both have P in the sense of Stacks 025V, then so does their product a₁ × a₂ : F₁ × F₂ ⟶ G₁ × G₂.

theorem hasSchemeProperty_prod_map (P : MorphismProperty Scheme.{u})
    [P.IsStableUnderComposition] {F₁ F₂ G₁ G₂ : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (a₁ : F₁ ⟶ G₁) (a₂ : F₂ ⟶ G₂)
    (h₁ : HasSchemeProperty B S hS P a₁) (h₂ : HasSchemeProperty B S hS P a₂) :
    HasSchemeProperty B S hS P (prod.map a₁ a₂)

Tag 02YO, a lemma

Tag 02YO in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.MorphismProperty.relative_monotone registered with add_to_stacks in StacksFrontier/MathlibRegistrations/Ch65.lean, line 29 (StacksFrontier).

Tag 05VM, a lemma

Tag 05VM in the Stacks Project.

AlgebraicGeometry.Space.isLocallySurjective_of_representable_flat_locallyOfFinitePresentation_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Presentation/Surjective.lean, line 74.

Stacks Project, Tag 05VM. A representable map of sheaves whose scheme-valued base changes are surjective, flat, and locally of finite presentation is locally surjective for the fppf topology.

theorem isLocallySurjective_of_representable_flat_locallyOfFinitePresentation_surjective
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : Sheaf (BigFppfOver.topology B S hS) (Type u)} (a : F ⟶ G)
    (ha : (MorphismProperty.presheaf
      (MorphismProperty.inverseImage
        ((fun _ _ f => Flat f ∧ LocallyOfFinitePresentation f ∧ Surjective f) :
          MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) a.hom) :
    Sheaf.IsLocallySurjective a

Tag 025W, a lemma

Tag 025W in the Stacks Project.

AlgebraicGeometry.yoneda_relativelyRepresentable_diag_tfae_bigFppfOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RepresentableProperty.lean, line 116.

Stacks 025W. For a presheaf F on the big fppf site of S, representability of the diagonal of F, representability of every scheme-valued point of F, and representability of the fibre product of every pair of scheme-valued points of F are equivalent.

theorem yoneda_relativelyRepresentable_diag_tfae_bigFppfOver
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) :
    List.TFAE
      [yoneda.relativelyRepresentable (Limits.diag F),
        ∀ (U : BigFppfOver B S hS) (ξ : F.obj (Opposite.op U)),
          yoneda.relativelyRepresentable (yonedaEquiv.symm ξ),
        ∀ (U V : BigFppfOver B S hS) (ξ : F.obj (Opposite.op U))
          (ξ' : F.obj (Opposite.op V)),
          (Limits.pullback (yonedaEquiv.symm ξ) (yonedaEquiv.symm ξ')).IsRepresentable]

Declarations registered for the tag:

CategoryTheory.yoneda_relativelyRepresentable_diag_tfae, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/RepresentableProperty.lean, line 98 (StacksFrontier): “stated for the Yoneda embedding of an arbitrary category with binary products and fibre products”.

Tag 0CB7, a lemma

Tag 0CB7 in the Stacks Project.

AlgebraicGeometry.Space.presheaf_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Presentation/Diagonal.lean, line 81.

A property of all pairwise fibre products of representables over a presheaf passes to its diagonal.

theorem presheaf_diagonal (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty Scheme.{u}) [P.IsStableUnderBaseChange]
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (h : ∀ (U V : BigFppfOver B S hS) (a : F.obj (op U)) (b : F.obj (op V)),
      ∃ (W : BigFppfOver B S hS)
        (i : yoneda.obj W ≅ pullback (yonedaEquiv.symm a) (yonedaEquiv.symm b))
        (f : W ⟶ U ⨯ V),
        yoneda.map (f ≫ prod.fst) =
          i.hom ≫ pullback.fst (yonedaEquiv.symm a) (yonedaEquiv.symm b) ∧
        yoneda.map (f ≫ prod.snd) =
          i.hom ≫ pullback.snd (yonedaEquiv.symm a) (yonedaEquiv.symm b) ∧
        P ((BigFppfOver.toScheme B S hS).map f)) :
    (P.inverseImage (BigFppfOver.toScheme B S hS)).presheaf (diag F)

AlgebraicGeometry.Space.sheaf_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Presentation/DiagonalFunctor.lean, line 449. The attribute's comment: “for the sheafified Yoneda embedding, which is the one the diagonal of a formal algebraic space is tested against”.

Stacks 0CB7 for the sheafified Yoneda embedding of the big fppf site over S: if every pair of scheme-valued points of an fppf sheaf X of Type (u + 1) has a fibre product represented by an object W of the site whose canonical morphism to the product of the two sources has Q, then the diagonal of X has Q relative to the sheafified Yoneda embedding.

theorem sheaf_diagonal (Q : MorphismProperty (BigFppfOver B S hS))
    [Q.IsStableUnderBaseChange]
    (X : Sheaf (BigFppfOver.topology B S hS) (Type (u + 1)))
    (h : ∀ (U V : BigFppfOver B S hS)
      (α : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj U ⟶ X)
      (β : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj V ⟶ X),
      ∃ (W : BigFppfOver B S hS)
        (i : (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).obj W ≅ pullback α β)
        (f : W ⟶ U ⨯ V),
        (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).map (f ≫ Limits.prod.fst) =
          i.hom ≫ pullback.fst α β ∧
        (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)).map (f ≫ Limits.prod.snd) =
          i.hom ≫ pullback.snd α β ∧
        Q f) :
    Q.relative (Sheaf.sheafifiedYoneda (BigFppfOver.topology B S hS)) (diag X)

Sources

LeanAlgebraicGeometry.Space.HasSchemeProperty · CategoryTheory.MorphismProperty.presheaf · CategoryTheory.Presheaf.isLocallySurjective_bot · CategoryTheory.Sheaf.IsLocallySurjective · CategoryTheory.MorphismProperty.relative_map_iff · CategoryTheory.MorphismProperty.relative_isStableUnderComposition · CategoryTheory.MorphismProperty.relative_isStableUnderBaseChange · AlgebraicGeometry.Space.presheaf_of_isLocallySurjective_pullback

Section65.6 Algebraic spaces #

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

Tag 025Y, a definition

Tag 025Y in the Stacks Project.

AlgebraicGeometry.IsAlgebraicSpace, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Basic.lean, line 96.

Stacks 025Y. A presheaf of sets on the big fppf site of S is an algebraic space over S when it is an fppf sheaf, has representable diagonal, and admits a surjective étale morphism from a representable presheaf.

structure IsAlgebraicSpace (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

Tag 025Z, a lemma

Tag 025Z in the Stacks Project.

AlgebraicGeometry.isAlgebraicSpace_yoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Category.lean, line 236.

Stacks 025Z. The representable presheaf of a scheme over S is an algebraic space over S.

theorem isAlgebraicSpace_yoneda (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (T : BigFppfOver B S hS) : IsAlgebraicSpace B S hS (yoneda.obj T)

Tag 0260, a definition

Tag 0260 in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.NatTrans registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 298 (StacksFrontier). References: EGA 0 (3.1.4); EGA 0 (3.2.3), “more general”; EGA 0 (8.1.3); EGA 0 (8.2.1); SGA 3 I (1.1); SGA 3 I (2.1.1), “more general”; SGA 3 VIIB (2.3.2), “definition of Hom_k-Gr(G”; SGA 4 I (1.1.1); SGA 4 I (4.3).
CategoryTheory.Functor.category registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 308 (StacksFrontier). References: SGA 4 I (1.1.1).

Sources

LeanAlgebraicGeometry.IsAlgebraicSpace · AlgebraicGeometry.isAlgebraicSpace_yoneda · CategoryTheory.NatTrans · CategoryTheory.Functor.category

Section65.7 Fibre products of algebraic spaces #

Section 65.7 of the Stacks Project, Tag 04T8. 3 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02X0, a lemma

Tag 02X0 in the Stacks Project.

AlgebraicGeometry.isAlgebraicSpace_prod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits.lean, line 111. The attribute's comment: “the product is an algebraic space”.

The presheaf product of two algebraic spaces over S is an algebraic space over S.

theorem isAlgebraicSpace_prod (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G) :
    IsAlgebraicSpace B S hS (F ⨯ G)

AlgebraicGeometry.AlgebraicSpaces.isLimitBinaryFanProduct, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits.lean, line 143. The attribute's comment: “the universal property”.

The presheaf product of two algebraic spaces over S, with the two presheaf projections, is a product in the category of algebraic spaces over S.

noncomputable def isLimitBinaryFanProduct (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) (F G : AlgebraicSpaces B S hS) :
    IsLimit (BinaryFan.mk
      (ObjectProperty.homMk (prod.fst : F.obj ⨯ G.obj ⟶ F.obj) : product B S hS F G ⟶ F)
      (ObjectProperty.homMk (prod.snd : F.obj ⨯ G.obj ⟶ G.obj) :
        product B S hS F G ⟶ G))

Tag 04T9, a lemma

Tag 04T9 in the Stacks Project.

AlgebraicGeometry.isAlgebraicSpace_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreProduct.lean, line 129.

Let F and G be algebraic spaces over S, let H be an fppf sheaf on the big fppf site of S whose diagonal is representable, and let f : F ⟶ H and g : G ⟶ H. Then a fibre product Z of f and g is an algebraic space over S.

theorem isAlgebraicSpace_of_isPullback
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (hHsheaf : Presheaf.IsSheaf (BigFppfOver.topology B S hS) H)
    (hHdiag : yoneda.relativelyRepresentable (diag H))
    {f : F ⟶ H} {g : G ⟶ H} {p : Z ⟶ F} {q : Z ⟶ G} (hZ : IsPullback p q f g) :
    IsAlgebraicSpace B S hS Z

AlgebraicGeometry.isAlgebraicSpace_pullback_of_representable_diagonal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FibreProduct.lean, line 165. The attribute's comment: “the chosen presheaf fibre product”.

The chosen presheaf fibre product of two algebraic spaces over an fppf sheaf with representable diagonal is an algebraic space.

theorem isAlgebraicSpace_pullback_of_representable_diagonal
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ H) (g : G ⟶ H)
    (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (hH : Presheaf.IsSheaf (BigFppfOver.topology B S hS) H)
    (hdiag : yoneda.relativelyRepresentable (diag H)) :
    IsAlgebraicSpace B S hS (pullback f g)

Tag 02X2, a lemma

Tag 02X2 in the Stacks Project.

AlgebraicGeometry.AlgebraicSpaces, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Category.lean, line 265. The attribute's comment: “the category of algebraic spaces over the base”.

Stacks 02X2. The category of algebraic spaces over a scheme S of a big fppf site: the full subcategory of presheaves on the big fppf site of S whose objects are algebraic spaces over S.

abbrev AlgebraicSpaces (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)

AlgebraicGeometry.isAlgebraicSpace_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Category.lean, line 350. The attribute's comment: “algebraicity of the fibre product”.

Stacks 02X2. The presheaf fibre product of two algebraic spaces over an algebraic space is an algebraic space.

theorem isAlgebraicSpace_pullback {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : F ⟶ H) (g : G ⟶ H) (hF : IsAlgebraicSpace B S hS F) (hG : IsAlgebraicSpace B S hS G)
    (hH : IsAlgebraicSpace B S hS H) :
    IsAlgebraicSpace B S hS (pullback f g)

AlgebraicGeometry.AlgebraicSpaces.isPullback_fiberProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Category.lean, line 403. The attribute's comment: “universal property among algebraic spaces”.

Stacks 02X2. The presheaf fibre product of two algebraic spaces is a fibre product in the category of algebraic spaces over the base.

theorem isPullback_fiberProduct {F G H : AlgebraicSpaces B S hS} (f : F ⟶ H) (g : G ⟶ H) :
    IsPullback (ObjectProperty.homMk (pullback.fst f.hom g.hom) : fiberProduct B S hS f g ⟶ F)
      (ObjectProperty.homMk (pullback.snd f.hom g.hom) : fiberProduct B S hS f g ⟶ G) f g

Sources

LeanAlgebraicGeometry.isAlgebraicSpace_prod · AlgebraicGeometry.AlgebraicSpaces.isLimitBinaryFanProduct · AlgebraicGeometry.isAlgebraicSpace_of_isPullback · AlgebraicGeometry.isAlgebraicSpace_pullback_of_representable_diagonal · AlgebraicGeometry.AlgebraicSpaces · AlgebraicGeometry.isAlgebraicSpace_pullback · AlgebraicGeometry.AlgebraicSpaces.isPullback_fiberProduct

Section65.8 Glueing algebraic spaces #

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

Tag 0F15, a lemma

Tag 0F15 in the Stacks Project.

AlgebraicGeometry.coproductInl_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoproductInclusion.lean, line 449. The attribute's comment: “open immersion”.

Stacks 0F15. The first inclusion into a binary coproduct of sheaves on the big fppf site of S is representable by open immersions. By symmetry the same holds for the second inclusion.

theorem coproductInl_isOpenImmersion (hc : IsColimit (BinaryCofan.mk iF iG)) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@IsOpenImmersion.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) iF.hom

AlgebraicGeometry.coproductInl_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoproductInclusion.lean, line 467. The attribute's comment: “closed immersion”.

Stacks 0F15. The first inclusion into a binary coproduct of sheaves on the big fppf site of S is representable by closed immersions. By symmetry the same holds for the second inclusion.

theorem coproductInl_isClosedImmersion (hc : IsColimit (BinaryCofan.mk iF iG)) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@IsClosedImmersion.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) iF.hom

AlgebraicGeometry.Sheaf.exists_clopen_decomposition_of_isColimit_cofan_ulift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeValuedCoproductDecomposition.lean, line 86. The attribute's comment: “in an arbitrary value universe”.

Stacks 02WO and Stacks 0F15 for sheaves with values in a universe max w u independent of the universe u of the schemes. A section x of a coproduct P = ∐ᵢ Fᵢ of pointwise u-small sheaves over an object W of the big fppf site of S, the index type being u-small, decomposes W into a family of pairwise disjoint open subobjects W' i, covering W, such that x restricted to W' i comes from Fᵢ; and each W' i is universal with that property.

This is AlgebraicGeometry.Sheaf.exists_clopen_decomposition_of_isColimit_cofan with the value universe of the sheaves decoupled from the universe of the morphisms of the site. The decomposition machinery is not rebuilt: the sheaves are universe lifts of sheaves of Type u, the coproduct cocone descends to those by AlgebraicGeometry.Space.exists_shrink_isColimit_cofan_of_small, and the conclusion, which speaks of objects of the site and of sections, transports back along the lift.

theorem Sheaf.exists_clopen_decomposition_of_isColimit_cofan_ulift {I : Type v} [Small.{u} I]
    {F : I → Sheaf (BigFppfOver.topology B S hS) (Type (max w u))}
    (hF : ∀ i, FunctorToTypes.Small.{u} (F i).obj)
    {P : Sheaf (BigFppfOver.topology B S hS) (Type (max w u))} (ι : ∀ i, F i ⟶ P)
    (hP : IsColimit (Cofan.mk P ι)) (W : BigFppfOver B S hS) (x : P.obj.obj (op W)) :
    ∃ (W' : I → BigFppfOver B S hS) (p : ∀ i, W' i ⟶ W),
      (∀ i, IsOpenImmersion ((BigFppfOver.toScheme B S hS).map (p i))) ∧
      (∀ i, ∃ z : (F i).obj.obj (op (W' i)),
        (ι i).hom.app (op (W' i)) z = P.obj.map (p i).op x) ∧
      (∀ i i', i ≠ i' → ∀ (y : (BigFppfOver.toScheme B S hS).obj (W' i))
        (y' : (BigFppfOver.toScheme B S hS).obj (W' i')),
        (BigFppfOver.toScheme B S hS).map (p i) y ≠
          (BigFppfOver.toScheme B S hS).map (p i') y') ∧
      (∀ w : (BigFppfOver.toScheme B S hS).obj W,
        ∃ i, w ∈ Set.range ((BigFppfOver.toScheme B S hS).map (p i))) ∧
      (∀ (i : I) (T : BigFppfOver B S hS) (t : T ⟶ W),
        (∃ z : (F i).obj.obj (op T), (ι i).hom.app (op T) z = P.obj.map t.op x) →
        ∃ t' : T ⟶ W' i, t' ≫ p i = t)

Tag 02WO, a lemma

Tag 02WO in the Stacks Project.

AlgebraicGeometry.Space.exists_clopen_scheme_coproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Glueing/RepresentableCoproduct.lean, line 53.

A sheaf coproduct represented by a scheme comes from an open-and-closed coproduct decomposition of that scheme.

theorem exists_clopen_scheme_coproduct
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (I : Type v)
    (Fᵢ : I → Sheaf (BigFppfOver.topology B S hS) (Type u))
    (F : Sheaf (BigFppfOver.topology B S hS) (Type u))
    (ι : ∀ i, Fᵢ i ⟶ F)
    (hcoprod : IsColimit (Cofan.mk F ι))
    (U : BigFppfOver B S hS)
    (e : F.obj ≅ yoneda.obj U) :
    ∃ (Uᵢ : I → BigFppfOver B S hS)
      (j : ∀ i, Uᵢ i ⟶ U)
      (eᵢ : ∀ i, (Fᵢ i).obj ≅ yoneda.obj (Uᵢ i)),
      (∀ i, AlgebraicGeometry.IsOpenImmersion
        ((BigFppfOver.toScheme B S hS).map (j i))) ∧
      (∀ i, AlgebraicGeometry.IsClosedImmersion
        ((BigFppfOver.toScheme B S hS).map (j i))) ∧
      (∀ i, (eᵢ i).hom ≫ yoneda.map (j i) = (ι i).hom ≫ e.hom) ∧
      Nonempty (IsColimit (Cofan.mk ((BigFppfOver.toScheme B S hS).obj U)
        (fun i => (BigFppfOver.toScheme B S hS).map (j i))))

AlgebraicGeometry.Sheaf.exists_clopen_decomposition_of_isColimit_cofan_ulift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeValuedCoproductDecomposition.lean, line 86. The attribute's comment: “in an arbitrary value universe, for pointwise u-small sheaves and a u-small index type; the smallness hypotheses are absent from AlgebraicGeometry.Sheaf.exists_clopen_decomposition_of_isColimit_cofan, which is the same statement in the value universe of the site”.

Stacks 02WO and Stacks 0F15 for sheaves with values in a universe max w u independent of the universe u of the schemes. A section x of a coproduct P = ∐ᵢ Fᵢ of pointwise u-small sheaves over an object W of the big fppf site of S, the index type being u-small, decomposes W into a family of pairwise disjoint open subobjects W' i, covering W, such that x restricted to W' i comes from Fᵢ; and each W' i is universal with that property.

This is AlgebraicGeometry.Sheaf.exists_clopen_decomposition_of_isColimit_cofan with the value universe of the sheaves decoupled from the universe of the morphisms of the site. The decomposition machinery is not rebuilt: the sheaves are universe lifts of sheaves of Type u, the coproduct cocone descends to those by AlgebraicGeometry.Space.exists_shrink_isColimit_cofan_of_small, and the conclusion, which speaks of objects of the site and of sections, transports back along the lift.

theorem Sheaf.exists_clopen_decomposition_of_isColimit_cofan_ulift {I : Type v} [Small.{u} I]
    {F : I → Sheaf (BigFppfOver.topology B S hS) (Type (max w u))}
    (hF : ∀ i, FunctorToTypes.Small.{u} (F i).obj)
    {P : Sheaf (BigFppfOver.topology B S hS) (Type (max w u))} (ι : ∀ i, F i ⟶ P)
    (hP : IsColimit (Cofan.mk P ι)) (W : BigFppfOver B S hS) (x : P.obj.obj (op W)) :
    ∃ (W' : I → BigFppfOver B S hS) (p : ∀ i, W' i ⟶ W),
      (∀ i, IsOpenImmersion ((BigFppfOver.toScheme B S hS).map (p i))) ∧
      (∀ i, ∃ z : (F i).obj.obj (op (W' i)),
        (ι i).hom.app (op (W' i)) z = P.obj.map (p i).op x) ∧
      (∀ i i', i ≠ i' → ∀ (y : (BigFppfOver.toScheme B S hS).obj (W' i))
        (y' : (BigFppfOver.toScheme B S hS).obj (W' i')),
        (BigFppfOver.toScheme B S hS).map (p i) y ≠
          (BigFppfOver.toScheme B S hS).map (p i') y') ∧
      (∀ w : (BigFppfOver.toScheme B S hS).obj W,
        ∃ i, w ∈ Set.range ((BigFppfOver.toScheme B S hS).map (p i))) ∧
      (∀ (i : I) (T : BigFppfOver B S hS) (t : T ⟶ W),
        (∃ z : (F i).obj.obj (op T), (ι i).hom.app (op T) z = P.obj.map t.op x) →
        ∃ t' : T ⟶ W' i, t' ≫ p i = t)

AlgebraicGeometry.Sheaf.isEmpty_toScheme_of_eq_of_ne_ulift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeValuedCoproductDecomposition.lean, line 197. The attribute's comment: “disjointness of the legs, in an arbitrary value universe”.

Distinct legs of a coproduct cocone of pointwise u-small sheaves on the big fppf site of S have disjoint images, for a value universe independent of the universe of the objects of the site: an object of the site carrying sections of two different members of the family with the same image in the coproduct has no points.

This is AlgebraicGeometry.Sheaf.isEmpty_toScheme_of_eq_of_ne with the value universe of the sheaves decoupled from the universe of the morphisms of the site, and is the disjointness half of Stacks 02WO there.

theorem Sheaf.isEmpty_toScheme_of_eq_of_ne_ulift {I : Type v} [Small.{u} I]
    {F : I → Sheaf (BigFppfOver.topology B S hS) (Type (max w u))}
    (hF : ∀ i, FunctorToTypes.Small.{u} (F i).obj)
    {P : Sheaf (BigFppfOver.topology B S hS) (Type (max w u))} (ι : ∀ i, F i ⟶ P)
    (hP : IsColimit (Cofan.mk P ι)) {i j : I} (hij : i ≠ j) {W : BigFppfOver B S hS}
    (x : (F i).obj.obj (op W)) (y : (F j).obj.obj (op W))
    (h : (ι i).hom.app (op W) x = (ι j).hom.app (op W) y) :
    IsEmpty ((BigFppfOver.toScheme B S hS).obj W)

Tag 02WP, a lemma

Tag 02WP in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_of_coproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoproductSummand.lean, line 233.

Stacks 02WP. Every summand of a sheaf coproduct that is an algebraic space is an algebraic space.

theorem isAlgebraicSpace_of_coproduct
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (I : Type v)
    (Fᵢ : I → Sheaf (BigFppfOver.topology B S hS) (Type u))
    (F : Sheaf (BigFppfOver.topology B S hS) (Type u))
    (ι : ∀ i, Fᵢ i ⟶ F)
    (hcoprod : IsColimit (Cofan.mk F ι))
    (hF : IsAlgebraicSpace B S hS F.obj)
    (i : I) : IsAlgebraicSpace B S hS (Fᵢ i).obj

Tag 02WQ, a lemma

Tag 02WQ in the Stacks Project.

AlgebraicGeometry.isAlgebraicSpace_coproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoproductAlgebraic.lean, line 808.

Stacks 02WQ. A coproduct of algebraic spaces over S is an algebraic space over S, provided the chosen surjective étale scheme atlases of the members have a coproduct inside the big fppf site over S.

The sheaf condition is part of the data. The diagonal is representable by AlgebraicGeometry.relativelyRepresentable_diag_of_isColimit_cofan, and the coproduct V of the atlases, with the morphism to the coproduct sheaf glued by AlgebraicGeometry.exists_hom_yoneda_of_isColimit_cofan, is a surjective étale atlas by AlgebraicGeometry.presheaf_inverseImage_of_isColimit_cofan.

theorem isAlgebraicSpace_coproduct
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type v}
    (F : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : ∀ i, IsAlgebraicSpace B S hS (F i))
    (G : Sheaf (BigFppfOver.topology B S hS) (Type u))
    (ι : ∀ i, (⟨F i, (hF i).isSheaf⟩ :
      Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ G)
    (hG : IsColimit (Cofan.mk G ι))
    (U : I → BigFppfOver B S hS)
    (f : ∀ i, yoneda.obj (U i) ⟶ F i)
    (hsurj : ∀ i, (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) (f i))
    (hetale : ∀ i, (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) (f i))
    (V : BigFppfOver B S hS)
    (j : ∀ i, U i ⟶ V)
    (hV : IsColimit (Cofan.mk V j)) :
    IsAlgebraicSpace B S hS G.obj

AlgebraicGeometry.Space.isAlgebraicSpaceULift_coproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeValuedCoproduct.lean, line 306. The attribute's comment: “in an arbitrary value universe, for a u-small index type; the index is unrestricted in AlgebraicGeometry.isAlgebraicSpace_coproduct, which is the same statement in the value universe of the site”.

Stacks 02WQ for presheaves with values in a universe max w u independent of the universe u of the schemes. A coproduct of algebraic spaces over S, indexed by a u-small type and with values in Type (max w u), is an algebraic space over S, provided the chosen surjective étale scheme atlases of the members have a coproduct inside the big fppf site over S.

The presheaves involved are pointwise u-small, so they are universe lifts of presheaves of Type u and the algebraic-space condition transports along the lift; the universal property of the coproduct transports along it too, by fullness, so no coproduct of sheaves of Type u is formed.

theorem isAlgebraicSpaceULift_coproduct {I : Type v} [Small.{u} I]
    {Fᵢ : I → Sheaf (BigFppfOver.topology B S hS) (Type (max w u))}
    (hFᵢ : ∀ i, IsAlgebraicSpaceULift.{w} B S hS (Fᵢ i).obj)
    {G : Sheaf (BigFppfOver.topology B S hS) (Type (max w u))} (ι : ∀ i, Fᵢ i ⟶ G)
    (hG : IsColimit (Cofan.mk G ι))
    (U : I → BigFppfOver B S hS)
    (a : ∀ i, (uliftYoneda.{w}).obj (U i) ⟶ (Fᵢ i).obj)
    (hsurj : ∀ i, (surjectiveOnSite B S hS).relative (uliftYoneda.{w}) (a i))
    (hetale : ∀ i, (etaleOnSite B S hS).relative (uliftYoneda.{w}) (a i))
    {V : BigFppfOver B S hS} {j : ∀ i, U i ⟶ V} (hV : IsColimit (Cofan.mk V j)) :
    IsAlgebraicSpaceULift.{w} B S hS G.obj

Tag 02WR, a lemma

Tag 02WR in the Stacks Project.

AlgebraicGeometry.isAlgebraicSpace_of_open_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OpenCoverAlgebraic.lean, line 308.

Stacks 02WR. An fppf sheaf with a jointly surjective family of representable open algebraic-space subfunctors is an algebraic space, when the coproduct of the family is itself an algebraic space.

theorem isAlgebraicSpace_of_open_cover
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F)
    (I : Type v)
    (Fᵢ : I → Sheaf (BigFppfOver.topology B S hS) (Type u))
    (hFᵢ : ∀ i, IsAlgebraicSpace B S hS (Fᵢ i).obj)
    (G : Sheaf (BigFppfOver.topology B S hS) (Type u))
    (ι : ∀ i, Fᵢ i ⟶ G)
    (hcoprod : IsColimit (Cofan.mk G ι))
    (g : G.obj ⟶ F)
    (hopen : ∀ i, (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@IsOpenImmersion.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) ((ι i).hom ≫ g))
    (hsurj : Presheaf.IsLocallySurjective
      (BigFppfOver.topology B S hS) g)
    (hG : IsAlgebraicSpace B S hS G.obj) :
    IsAlgebraicSpace B S hS F

Sources

LeanAlgebraicGeometry.coproductInl_isOpenImmersion · AlgebraicGeometry.coproductInl_isClosedImmersion · AlgebraicGeometry.Sheaf.exists_clopen_decomposition_of_isColimit_cofan_ulift · AlgebraicGeometry.Space.exists_clopen_scheme_coproduct · AlgebraicGeometry.Sheaf.isEmpty_toScheme_of_eq_of_ne_ulift · AlgebraicGeometry.Space.isAlgebraicSpace_of_coproduct · AlgebraicGeometry.isAlgebraicSpace_coproduct · AlgebraicGeometry.Space.isAlgebraicSpaceULift_coproduct

Section65.9 Presentations of algebraic spaces #

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

Tag 0262, a lemma

Tag 0262 in the Stacks Project.

AlgebraicGeometry.Space.isCoequalizer_of_surjective_flat_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatChartCoequalizer.lean, line 140. The attribute's comment: “part (3), with the étale chart of the source replaced by a surjective flat chart locally of finite presentation”.

Stacks 0262, part (3), with the étale hypothesis on the chart weakened to flatness together with local finite presentation. A surjective flat chart locally of finite presentation of an algebraic space is the coequalizer, in fppf sheaves of sets, of its kernel pair.

The three conditions are the relative properties of Tag 02YN: they are asked of every represented base change of the chart.

theorem isCoequalizer_of_surjective_flat_locallyOfFinitePresentation
    (f : yoneda.obj U ⟶ F) (s t : R ⟶ U)
    (hR : IsPullback (yoneda.map s) (yoneda.map t) f f)
    (hF : IsAlgebraicSpace B S hS F)
    (hsurj : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f)
    (hflat : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Flat.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f)
    (hlfp : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.LocallyOfFinitePresentation.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f) :
    let J := BigFppfOver.topology B S hS
    ∃ (hRsh : Presheaf.IsSheaf J (yoneda.obj R))
      (hUsh : Presheaf.IsSheaf J (yoneda.obj U)),
      let RF : Sheaf J (Type u) := ⟨yoneda.obj R, hRsh⟩
      let UF : Sheaf J (Type u) := ⟨yoneda.obj U, hUsh⟩
      let FF : Sheaf J (Type u) := ⟨F, hF.isSheaf⟩
      let sf : RF ⟶ UF := ⟨yoneda.map s⟩
      let tf : RF ⟶ UF := ⟨yoneda.map t⟩
      let ff : UF ⟶ FF := ⟨f⟩
    let w : sf ≫ ff = tf ≫ ff := by
        apply Sheaf.hom_ext
        exact hR.w
      Nonempty (IsColimit (Cofork.ofπ ff w))

AlgebraicGeometry.Space.isCoequalizer_of_surjectiveFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatChartCoequalizer.lean, line 187. The attribute's comment: “part (3), for a surjective finite locally free chart of the source in place of a surjective étale one”.

Stacks 0262, part (3), for a surjective finite locally free chart in place of a surjective étale one. Such a chart of an algebraic space is the coequalizer, in fppf sheaves of sets, of its kernel pair.

Finite local freeness is read in the representable sense, condition (1) of Stacks 03ZW, and gives flatness and local finite presentation of every represented base change by the scheme-level equivalence Tag 02KB.

theorem isCoequalizer_of_surjectiveFiniteLocallyFree
    (f : yoneda.obj U ⟶ F) (s t : R ⟶ U)
    (hR : IsPullback (yoneda.map s) (yoneda.map t) f f)
    (hF : IsAlgebraicSpace B S hS F)
    (hsurj : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f)
    (hflf : (MorphismProperty.inverseImage
      (@Stacks.Morphisms.IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f) :
    let J := BigFppfOver.topology B S hS
    ∃ (hRsh : Presheaf.IsSheaf J (yoneda.obj R))
      (hUsh : Presheaf.IsSheaf J (yoneda.obj U)),
      let RF : Sheaf J (Type u) := ⟨yoneda.obj R, hRsh⟩
      let UF : Sheaf J (Type u) := ⟨yoneda.obj U, hUsh⟩
      let FF : Sheaf J (Type u) := ⟨F, hF.isSheaf⟩
      let sf : RF ⟶ UF := ⟨yoneda.map s⟩
      let tf : RF ⟶ UF := ⟨yoneda.map t⟩
      let ff : UF ⟶ FF := ⟨f⟩
    let w : sf ≫ ff = tf ≫ ff := by
        apply Sheaf.hom_ext
        exact hR.w
      Nonempty (IsColimit (Cofork.ofπ ff w))

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

The kernel pair of a map from a representable presheaf defines an equivalence relation over the base scheme. This includes monicity of R ⟶ U ×_S U.

theorem isEquivalenceRelation_of_isPullback
    (hR : IsPullback (yoneda.map s) (yoneda.map t) f f) :
    IsEquivalenceRelation ((Over.post B.inclusion).map s)
      ((Over.post B.inclusion).map t)

AlgebraicGeometry.Space.isCoequalizer_of_surjectiveEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/KernelPairRelation.lean, line 179. The attribute's comment: “part (3)”.

Stacks 0262, part (3). A surjective étale atlas of an algebraic space is the coequalizer, in fppf sheaves of sets, of its kernel pair: every map to a sheaf which identifies the two projections descends uniquely.

theorem isCoequalizer_of_surjectiveEtale
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {R U : BigFppfOver B S hS}
    (f : yoneda.obj U ⟶ F) (s t : R ⟶ U)
    (hR : IsPullback (yoneda.map s) (yoneda.map t) f f)
    (hF : IsAlgebraicSpace B S hS F)
    (hsurj : (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) f)
    (hetale : (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) f) :
    let J := BigFppfOver.topology B S hS
    ∃ (hRsh : Presheaf.IsSheaf J (yoneda.obj R))
      (hUsh : Presheaf.IsSheaf J (yoneda.obj U)),
      let RF : Sheaf J (Type u) := ⟨yoneda.obj R, hRsh⟩
      let UF : Sheaf J (Type u) := ⟨yoneda.obj U, hUsh⟩
      let FF : Sheaf J (Type u) := ⟨F, hF.isSheaf⟩
      let sf : RF ⟶ UF := ⟨yoneda.map s⟩
      let tf : RF ⟶ UF := ⟨yoneda.map t⟩
      let ff : UF ⟶ FF := ⟨f⟩
    let w : sf ≫ ff = tf ≫ ff := by
        apply Sheaf.hom_ext
        exact hR.w
      Nonempty (IsColimit (Cofork.ofπ ff w))

Declarations registered for the tag:

CategoryTheory.MorphismProperty.relative.property registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/KernelPairRelation.lean, line 173 (StacksFrontier): “part (2), étale projections”.

Tag 02WS, a definition

Tag 02WS in the Stacks Project.

Stacks.Groupoids.IsEtaleEquivalenceRelation, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EquivalenceRelations.lean, line 103.

Stacks 02WS. An equivalence relation over S is étale when its source and target maps are étale morphisms of schemes.

class IsEtaleEquivalenceRelation {R U : Over S} (j : PreRelation R U) : Prop

Tag 0263, a definition

Tag 0263 in the Stacks Project.

AlgebraicGeometry.Space.Presentation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtalePresentation.lean, line 50.

Stacks 0263. An étale presentation of an algebraic space by a scheme over S together with an étale equivalence relation on it.

structure Presentation (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (_hF : IsAlgebraicSpace B S hS F)

Sources

LeanAlgebraicGeometry.Space.isCoequalizer_of_surjective_flat_locallyOfFinitePresentation · AlgebraicGeometry.Space.isCoequalizer_of_surjectiveFiniteLocallyFree · AlgebraicGeometry.Space.isEquivalenceRelation_of_isPullback · AlgebraicGeometry.Space.isCoequalizer_of_surjectiveEtale · CategoryTheory.MorphismProperty.relative.property · Stacks.Groupoids.IsEtaleEquivalenceRelation · AlgebraicGeometry.Space.Presentation

Section65.10 Algebraic spaces and equivalence relations #

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

Tag 02WT, a lemma

Tag 02WT in the Stacks Project.

AlgebraicGeometry.Space.isEtaleEquivalenceRelation_restrict, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Presentation/Restriction.lean, line 93.

Restricting an étale equivalence relation along an étale morphism again gives an étale equivalence relation.

instance isEtaleEquivalenceRelation_restrict (j : Stacks.Groupoids.PreRelation R U)
    (g : U' ⟶ U) [Stacks.Groupoids.IsEtaleEquivalenceRelation j] [Etale g.left] :
    Stacks.Groupoids.IsEtaleEquivalenceRelation (AlgebraicGeometry.PreRelation.restrict j g)

Tag 02WU, a lemma

Tag 02WU in the Stacks Project.

AlgebraicGeometry.GroupoidScheme.isOpenImmersion_restrictionQuotientMap_of_isInvariantSet, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/QuotientSheaf/OpenSaturation.lean, line 906.

Stacks 02WU. Let (U, R, s, t, c) be a groupoid scheme over S and let i : V ⟶ U be an open immersion of schemes over S whose range is invariant under the arrows of the groupoid. Then the map of fppf quotient sheaves V/R|_V ⟶ U/R induced by the restriction of the groupoid along i is representable, and is an open immersion; so V/R|_V is an open subspace of U/R.

The Stacks Project states this for a pre-relation j = (s, t) : R → U ×_S U which is an equivalence relation with s, t surjective, flat and locally of finite presentation, and an arbitrary flat, locally finitely presented g : U' → U. Those hypotheses enter only to make the saturation t(s^{-1}(g(U'))) an open subscheme of U over which g is an fppf covering. Here the saturation is the given invariant open itself and the covering is split by the identity arrow of the groupoid, so no flatness is needed of anything.

theorem isOpenImmersion_restrictionQuotientMap_of_isInvariantSet
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    (G : GroupoidScheme S) {W : Over S} (i : W ⟶ G.objects) [IsOpenImmersion i.left]
    (hi : IsInvariantSet G (Set.range i.left.base)) :
    Space.IsOpenImmersion B S hS
      (restrictionQuotientMap (BigFppfOver.topology B S hS) (Over.post B.inclusion) G i
        (restrict G i)).1

AlgebraicGeometry.isOpenImmersion_restrictedQuotientMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuotientSheafFppfOpenImmersion.lean, line 194.

Stacks 02WU. Let j = (t, s) : R ⟶ U ×_S U be an equivalence relation of schemes over S whose source and target maps are surjective, flat and locally of finite presentation, and let g : U' ⟶ U be flat and locally of finite presentation. The induced map U'/R' ⟶ U/R of quotient sheaves on the big fppf site over S is representable and an open immersion.

theorem isOpenImmersion_restrictedQuotientMap (B : BigFppfSite.{u}) (hS : B.Contains S)
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    (j : PreRelation R U) (g : U' ⟶ U) [IsEquivalenceRelation j.target j.source]
    (hs_surj : Surjective j.source.left) (ht_surj : Surjective j.target.left)
    (hs_flat : Flat j.source.left) (ht_flat : Flat j.target.left)
    (hs_lfp : LocallyOfFinitePresentation j.source.left)
    (ht_lfp : LocallyOfFinitePresentation j.target.left)
    (hg_flat : Flat g.left) (hg_lfp : LocallyOfFinitePresentation g.left) :
    Space.IsOpenImmersion B S hS
      (restrictQuotientSheafMap (BigFppfOver.topology B S hS)
        (CategoryTheory.Over.post (X := B.obj hS) B.inclusion) j g).hom

AlgebraicGeometry.Space.isOpenImmersion_restrictedQuotientMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RestrictedQuotientOpenImmersion.lean, line 292.

Stacks 02WU. Let j be an equivalence relation on U over S whose source and target maps are surjective, flat and locally of finite presentation, and let g : U' ⟶ U be flat and locally of finite presentation. Then the induced map of fppf quotient sheaves U'/R' ⟶ U/R is representable by open immersions.

theorem isOpenImmersion_restrictedQuotientMap
    (B : BigFppfSite.{u}) (hS : B.Contains S)
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)]
    (j : PreRelation R U) (g : U' ⟶ U)
    [IsEquivalenceRelation j.target j.source]
    (hs_surj : Surjective j.source.left)
    (ht_surj : Surjective j.target.left)
    (hs_flat : Flat j.source.left)
    (ht_flat : Flat j.target.left)
    (hs_lfp : LocallyOfFinitePresentation j.source.left)
    (ht_lfp : LocallyOfFinitePresentation j.target.left)
    (hg_flat : Flat g.left)
    (hg_lfp : LocallyOfFinitePresentation g.left) :
    IsOpenImmersion B S hS
      (restrictQuotientSheafMap (BigFppfOver.topology B S hS)
        (Over.post (X := B.obj hS) B.inclusion) j g).hom

Tag 02WV, a lemma

Tag 02WV in the Stacks Project.

AlgebraicGeometry.Space.quotientMap_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PresentationFromQuotient.lean, line 272. The attribute's comment: “kernel pair”.

The relation is the fibre product U ×_{U/R} U. Nothing is assumed about the quotient.

theorem quotientMap_isPullback
    [IsEtaleEquivalenceRelation (relation B S hS s t)] :
    IsPullback (yoneda.map t) (yoneda.map s)
      (quotientMap B S hS s t) (quotientMap B S hS s t)

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

The quotient map of an étale equivalence relation is surjective after every representable base change, as soon as it is representable.

theorem quotientMap_surjective
    [IsEtaleEquivalenceRelation (relation B S hS s t)]
    (hrep : yoneda.relativelyRepresentable (quotientMap B S hS s t)) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)))
      (quotientMap B S hS s t)

AlgebraicGeometry.Space.quotientMap_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PresentationFromQuotient.lean, line 462. The attribute's comment: “étale”.

The quotient map of an étale equivalence relation is étale after every representable base change, as soon as it is representable.

theorem quotientMap_etale
    [IsEtaleEquivalenceRelation (relation B S hS s t)]
    (hrep : yoneda.relativelyRepresentable (quotientMap B S hS s t)) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)))
      (quotientMap B S hS s t)

AlgebraicGeometry.Space.quotientPresentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PresentationFromQuotient.lean, line 479. The attribute's comment: “presentation”.

An étale equivalence relation whose quotient sheaf is an algebraic space presents that algebraic space.

noncomputable def quotientPresentation
    [IsEtaleEquivalenceRelation (relation B S hS s t)]
    (hQ : IsAlgebraicSpace B S hS
      (quotientSheaf (BigFppfOver.topology B S hS)
        (Over.post B.inclusion) (relation B S hS s t)).obj) :
    Presentation B S hS _ hQ

Tag 0265, a lemma

Tag 0265 in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_quotientSheaf_of_affineBase_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiAffineFlatChartDescent.lean, line 533. The attribute's comment: “the quotient sheaf is an algebraic space”.

Stacks 0265, the algebraic-space property. The quotient sheaf of an étale equivalence relation on an object of the big fppf site of S is an algebraic space over S. Stacks 0265 assumes the underlying scheme of U affine; the proof does not use it.

This is AlgebraicGeometry.Space.isAlgebraicSpace_quotientSheaf_of_quasiAffineDescent with its hypothesis h0247 discharged.

theorem isAlgebraicSpace_quotientSheaf_of_affineBase_unconditional :
    IsAlgebraicSpace B S hS
      (quotientSheaf (BigFppfOver.topology B S hS) (Over.post B.inclusion) j).obj

AlgebraicGeometry.Space.surjective_toQuotientSheaf_of_affineBase_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiAffineFlatChartDescent.lean, line 544. The attribute's comment: “the quotient map is surjective”.

Stacks 0265, surjectivity of the quotient map. This is AlgebraicGeometry.Space.surjective_toQuotientSheaf_of_quasiAffineDescent with its hypothesis h0247 discharged.

theorem surjective_toQuotientSheaf_of_affineBase_unconditional :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)))
      (yonedaEquiv.symm
        ((toQuotientSheaf (BigFppfOver.topology B S hS)
          (Over.post B.inclusion) j).app (Opposite.op U)
          (𝟙 ((Over.post B.inclusion).obj U))))

AlgebraicGeometry.Space.etale_toQuotientSheaf_of_affineBase_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiAffineFlatChartDescent.lean, line 560. The attribute's comment: “the quotient map is étale”.

Stacks 0265, étaleness of the quotient map. This is AlgebraicGeometry.Space.etale_toQuotientSheaf_of_quasiAffineDescent with its hypothesis h0247 discharged.

theorem etale_toQuotientSheaf_of_affineBase_unconditional :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)))
      (yonedaEquiv.symm
        ((toQuotientSheaf (BigFppfOver.topology B S hS)
          (Over.post B.inclusion) j).app (Opposite.op U)
          (𝟙 ((Over.post B.inclusion).obj U))))

Tag 02WW, a theorem

Tag 02WW in the Stacks Project.

AlgebraicGeometry.Space.uliftQuotientMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleQuotientPresentation.lean, line 157. The attribute's comment: “canonical quotient map”.

The canonical map from the lifted functor of points of the presenting scheme to the lifted quotient sheaf of its relation.

def uliftQuotientMap [HasSheafify (BigFppfOver.topology B S hS) (Type (max u v))] :
    uliftYoneda.{v}.obj U ⟶ (uliftQuotientSheaf.{u, v} B S hS s t).obj

AlgebraicGeometry.Space.quotientMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/PresentationFromQuotient.lean, line 147. The attribute's comment: “canonical quotient map”.

The canonical map from the presenting scheme to the quotient sheaf of its relation.

public noncomputable def quotientMap :
    yoneda.obj U ⟶
      (quotientSheaf (BigFppfOver.topology B S hS)
        (Over.post B.inclusion) (relation B S hS s t)).obj

AlgebraicGeometry.Space.isAlgebraicSpace_quotient_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuotientSheafPresentationUnconditional.lean, line 115. The attribute's comment: “the quotient sheaf is an algebraic space”.

Stacks 02WW, the algebraic-space property. The quotient sheaf of an étale equivalence relation on an object of the big fppf site of S is an algebraic space over S.

This is AlgebraicGeometry.Space.isAlgebraicSpace_quotientSheaf_relation_of_diagDescent with its descent hypothesis discharged by AlgebraicGeometry.Space.isEffectiveDescentAlongCoveringSieve_monomorphisms_inf_lft.

theorem isAlgebraicSpace_quotient_unconditional
    [IsEtaleEquivalenceRelation (relation B S hS s t)] :
    IsAlgebraicSpace B S hS
      (quotientSheaf (BigFppfOver.topology B S hS)
        (Over.post B.inclusion) (relation B S hS s t)).obj

AlgebraicGeometry.Space.quotientMap_surjective_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuotientSheafPresentationUnconditional.lean, line 126. The attribute's comment: “the quotient map is surjective”.

Stacks 02WW, surjectivity of the quotient map. The canonical map U ⟶ U/R is surjective after every representable base change.

theorem quotientMap_surjective_unconditional
    [IsEtaleEquivalenceRelation (relation B S hS s t)] :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)))
      (quotientMap B S hS s t)

AlgebraicGeometry.Space.quotientMap_etale_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuotientSheafPresentationUnconditional.lean, line 138. The attribute's comment: “the quotient map is étale”.

Stacks 02WW, étaleness of the quotient map. The canonical map U ⟶ U/R is étale after every representable base change.

theorem quotientMap_etale_unconditional
    [IsEtaleEquivalenceRelation (relation B S hS s t)] :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)))
      (quotientMap B S hS s t)

AlgebraicGeometry.Space.quotientPresentation_unconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuotientSheafPresentationUnconditional.lean, line 150. The attribute's comment: “the presentation”.

Stacks 02WW, the presentation. An étale equivalence relation presents its quotient sheaf: (U, R, U ⟶ U/R) is a presentation of the algebraic space U/R.

noncomputable def quotientPresentation_unconditional
    [IsEtaleEquivalenceRelation (relation B S hS s t)] :
    Presentation B S hS _ (isAlgebraicSpace_quotient_unconditional B S hS s t)

Sources

LeanAlgebraicGeometry.Space.isEtaleEquivalenceRelation_restrict · AlgebraicGeometry.GroupoidScheme.isOpenImmersion_restrictionQuotientMap_of_isInvariantSet · AlgebraicGeometry.isOpenImmersion_restrictedQuotientMap · AlgebraicGeometry.Space.isOpenImmersion_restrictedQuotientMap · AlgebraicGeometry.Space.quotientMap_isPullback · AlgebraicGeometry.Space.quotientMap_surjective · AlgebraicGeometry.Space.quotientMap_etale · AlgebraicGeometry.Space.quotientPresentation

Section65.11 Algebraic spaces, retrofitted #

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

Tag 0BGQ, a lemma

Tag 0BGQ in the Stacks Project.

AlgebraicGeometry.isAlgebraicSpace_of_surjective_etale_atlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleAtlasCriterionUnconditional.lean, line 84.

Stacks 0BGQ. A sheaf F on the big fppf site over S admitting a representable, surjective, étale morphism f : h_U ⟶ F from an object U of the site is an algebraic space over S.

The kernel pair R = U ×_F U of f is an object of the site with étale projections forming an étale equivalence relation, so the quotient sheaf U/R is an algebraic space by Stacks 02WW; both F and U/R are the coequalizer of the two projections in fppf sheaves of sets, hence isomorphic.

theorem isAlgebraicSpace_of_surjective_etale_atlas
    (hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F)
    (U : BigFppfOver B S hS) (f : yoneda.obj U ⟶ F)
    (hsurj : MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Surjective.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS)) f)
    (hetale : MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS)) f) :
    IsAlgebraicSpace B S hS F

Tag 0BGR, a lemma

Tag 0BGR in the Stacks Project.

AlgebraicGeometry.isAlgebraicSpace_of_relativelyRepresentable_surjective_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleAtlasCriterionUnconditional.lean, line 102.

Stacks 0BGR. A sheaf F on the big fppf site over S admitting a representable, surjective, étale morphism a : G ⟶ F from an algebraic space G over S is an algebraic space over S.

A surjective étale atlas h_U ⟶ G of G by an object of the site is representable because G has representable diagonal, and composing it with a gives an atlas of the same kind for F.

theorem isAlgebraicSpace_of_relativelyRepresentable_surjective_etale
    {G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hG : IsAlgebraicSpace B S hS G)
    (hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F) (a : G ⟶ F)
    (hs : MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Surjective.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS)) a)
    (he : MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u}) (BigFppfOver.toScheme B S hS)) a) :
    IsAlgebraicSpace B S hS F

AlgebraicGeometry.Space.isAlgebraicSpaceULift_of_relative_surjective_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeValuedEtaleAtlas.lean, line 96. The attribute's comment: “in an arbitrary value universe”.

Stacks 0BGR for presheaves with values in a universe max w u independent of the universe u of the schemes. A sheaf F on the big fppf site of S admitting a morphism a : G ⟶ F from an algebraic space G over S which is representable by objects of the site, surjective and étale is an algebraic space over S.

Both presheaves are pointwise u-small — the source because it is an algebraic space, the target because its sections lift along a after a surjective étale base change — so they are universe lifts of presheaves of Type u and the statement is the one in the value universe of the site transported along the lift.

theorem isAlgebraicSpaceULift_of_relative_surjective_etale
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (max w u)}
    (hF : Presheaf.IsSheaf (BigFppfOver.topology B S hS) F)
    (hG : IsAlgebraicSpaceULift.{w} B S hS G) (a : G ⟶ F)
    (hs : (surjectiveOnSite B S hS).relative (uliftYoneda.{w}) a)
    (he : (etaleOnSite B S hS).relative (uliftYoneda.{w}) a) :
    IsAlgebraicSpaceULift.{w} B S hS F

Tag 02WY, a lemma

Tag 02WY in the Stacks Project.

AlgebraicGeometry.isAlgebraicSpace_of_relativelyRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Representable.lean, line 212.

A representable transformation to an algebraic space over S has an algebraic space over S as its source.

theorem isAlgebraicSpace_of_relativelyRepresentable
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (a : G ⟶ F) (ha : yoneda.relativelyRepresentable a)
    (hF : IsAlgebraicSpace B S hS F) :
    IsAlgebraicSpace B S hS G

Tag 02WZ, a lemma

Tag 02WZ in the Stacks Project.

AlgebraicGeometry.presheaf_inverseImage_iff_atlas_snd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RepresentableAtlasTest.lean, line 75.

Stacks 02WZ. A representable transformation of presheaves on the big fppf site of S has a base-change stable, fppf local relative property exactly when its base change along one surjective étale representable transformation to the target has it. The presheaves are arbitrary: no algebraic space condition on F or G enters the argument.

theorem presheaf_inverseImage_iff_atlas_snd
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty Scheme.{u})
    [P.IsStableUnderBaseChange] [P.IsLocalAtTarget Scheme.fppfPrecoverage]
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : G ⟶ F) (hf : yoneda.relativelyRepresentable f)
    (U : BigFppfOver B S hS) (q : yoneda.obj U ⟶ F)
    (hq_surj : (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) q)
    (hq_etale : (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) q) :
    (MorphismProperty.presheaf
      (P.inverseImage (BigFppfOver.toScheme B S hS))) f ↔
      P ((BigFppfOver.toScheme B S hS).map (hf.snd q))

Tag 03I2, a lemma

Tag 03I2 in the Stacks Project.

AlgebraicGeometry.Space.isAlgebraicSpace_and_presheaf_of_surjectiveEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleDescentFromFppfDescent.lean, line 411.

Stacks 03I2. Let S be a scheme contained in a big fppf site and let P be a property of morphisms of schemes which is preserved by arbitrary base change, is fppf local on the base, and is such that morphisms with P satisfy descent for fppf coverings. Let f : X ⟶ Y be a morphism of presheaves on the big fppf site of S with X a sheaf and Y an algebraic space over S, and suppose some surjective étale chart g : yoneda.obj U ⟶ Y of Y makes the base change of f representable with P. Then X is an algebraic space over S, and f is representable and has P.

The three conclusions of the source are the two conjuncts: the second, (P.inverseImage _).presheaf f, is representability of f together with P for every represented base change of it.

theorem isAlgebraicSpace_and_presheaf_of_surjectiveEtaleChart
    {P : MorphismProperty Scheme.{u}} [P.IsStableUnderBaseChange]
    [P.IsLocalAtTarget Scheme.fppfPrecoverage]
    (hP : SatisfiesDescent.{u, 0} P Scheme.fppfPrecoverage)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : Presheaf.IsSheaf (BigFppfOver.topology B S hS) X)
    (hY : IsAlgebraicSpace B S hS Y) {f : X ⟶ Y}
    {U : BigFppfOver B S hS} {g : yoneda.obj U ⟶ Y}
    (hs : (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) g)
    (he : (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) g)
    (hV : (P.inverseImage (BigFppfOver.toScheme B S hS)).presheaf (pullback.snd f g)) :
    IsAlgebraicSpace B S hS X ∧
      (P.inverseImage (BigFppfOver.toScheme B S hS)).presheaf f

Tag 02X1, a lemma

Tag 02X1 in the Stacks Project.

AlgebraicGeometry.Space.exists_surjective_etale_chart_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleLocal.lean, line 77.

Let a : F ⟶ G be a morphism of presheaves on the big fppf site of S with F an algebraic space over S. Every surjective étale scheme chart q : yoneda.obj V ⟶ G is dominated by a surjective étale scheme chart of F: there are an object U of the site, a surjective étale chart p : yoneda.obj U ⟶ F and a morphism α : U ⟶ V making the square commute.

theorem exists_surjective_etale_chart_lift {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hF : IsAlgebraicSpace B S hS F) (a : F ⟶ G) (V : BigFppfOver B S hS)
    (q : yoneda.obj V ⟶ G)
    (hq_surjective : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf q)
    (hq_etale : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS)).presheaf q) :
    ∃ (U : BigFppfOver B S hS) (p : yoneda.obj U ⟶ F) (α : U ⟶ V),
      p ≫ a = yoneda.map α ≫ q ∧
      (MorphismProperty.inverseImage
        (@AlgebraicGeometry.Surjective.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf p ∧
      (MorphismProperty.inverseImage
        (@AlgebraicGeometry.Etale.{u} : MorphismProperty Scheme.{u})
        (BigFppfOver.toScheme B S hS)).presheaf p

Sources

LeanAlgebraicGeometry.isAlgebraicSpace_of_surjective_etale_atlas · AlgebraicGeometry.isAlgebraicSpace_of_relativelyRepresentable_surjective_etale · AlgebraicGeometry.Space.isAlgebraicSpaceULift_of_relative_surjective_etale · AlgebraicGeometry.isAlgebraicSpace_of_relativelyRepresentable · AlgebraicGeometry.presheaf_inverseImage_iff_atlas_snd · AlgebraicGeometry.Space.isAlgebraicSpace_and_presheaf_of_surjectiveEtaleChart · AlgebraicGeometry.Space.exists_surjective_etale_chart_lift

Section65.12 Immersions and Zariski coverings of algebraic spaces #

Section 65.12 of the Stacks Project, Tag 02YT. 6 tags here are carried by 19 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02YU, a definition

Tag 02YU in the Stacks Project.

AlgebraicGeometry.Space.IsOpenImmersion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 104. The attribute's comment: “part (1): open immersions”.

Stacks 02YU, part (1). A morphism of algebraic spaces over S is an open immersion when it is representable and every represented base change of it is an open immersion of schemes.

abbrev IsOpenImmersion {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G) : Prop

AlgebraicGeometry.Space.IsOpenSubspace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 125. The attribute's comment: “part (2): open subspaces”.

Stacks 02YU, part (2). A subfunctor of a presheaf on the big fppf site of S is an open subspace when it is an algebraic space over S and its inclusion is an open immersion.

abbrev IsOpenSubspace {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (G : Subfunctor F) : Prop

AlgebraicGeometry.Space.IsClosedImmersion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 132. The attribute's comment: “part (3): closed immersions”.

Stacks 02YU, part (3). A morphism of algebraic spaces over S is a closed immersion when it is representable and every represented base change of it is a closed immersion of schemes.

abbrev IsClosedImmersion {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G) : Prop

AlgebraicGeometry.Space.IsClosedSubspace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 150. The attribute's comment: “part (4): closed subspaces”.

Stacks 02YU, part (4). A subfunctor of a presheaf on the big fppf site of S is a closed subspace when it is an algebraic space over S and its inclusion is a closed immersion.

abbrev IsClosedSubspace {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (G : Subfunctor F) : Prop

AlgebraicGeometry.Space.IsImmersion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 157. The attribute's comment: “part (5): immersions”.

Stacks 02YU, part (5). A morphism of algebraic spaces over S is an immersion when it is representable and every represented base change of it is an immersion of schemes.

abbrev IsImmersion {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G) : Prop

AlgebraicGeometry.Space.IsLocallyClosedSubspace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms.lean, line 175. The attribute's comment: “part (6): locally closed subspaces”.

Stacks 02YU, part (6). A subfunctor of a presheaf on the big fppf site of S is a locally closed subspace when it is an algebraic space over S and its inclusion is an immersion.

abbrev IsLocallyClosedSubspace {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (G : Subfunctor F) : Prop

Tag 02YV, a lemma

Tag 02YV in the Stacks Project.

AlgebraicGeometry.Space.isOpenImmersion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ImmersionBaseChange.lean, line 167. The attribute's comment: “part (1): open immersions”. References: EGA I (4.2.5), “open immersions”.

Stacks 02YV, part (1): a composite of open immersions of algebraic spaces over S is an open immersion.

theorem isOpenImmersion_comp {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : F ⟶ G) (g : G ⟶ H)
    (hf : IsOpenImmersion B S hS f) (hg : IsOpenImmersion B S hS g) :
    IsOpenImmersion B S hS (f ≫ g)

AlgebraicGeometry.Space.isClosedImmersion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ImmersionBaseChange.lean, line 178. The attribute's comment: “part (2): closed immersions”. References: EGA I (4.2.5), “closed immersions”; EGA I (4.1.6), “closed subprescheme”.

Stacks 02YV, part (2): a composite of closed immersions of algebraic spaces over S is a closed immersion.

theorem isClosedImmersion_comp {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : F ⟶ G) (g : G ⟶ H)
    (hf : IsClosedImmersion B S hS f) (hg : IsClosedImmersion B S hS g) :
    IsClosedImmersion B S hS (f ≫ g)

AlgebraicGeometry.Space.isImmersion_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ImmersionBaseChange.lean, line 187. The attribute's comment: “part (3): immersions”. References: EGA I (4.2.5), “immersions”; EGA I (4.1.6), “subprescheme case”.

Stacks 02YV, part (3): a composite of immersions of algebraic spaces over S is an immersion.

theorem isImmersion_comp {F G H : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (f : F ⟶ G) (g : G ⟶ H)
    (hf : IsImmersion B S hS f) (hg : IsImmersion B S hS g) :
    IsImmersion B S hS (f ≫ g)

Declarations registered for the tag:

CategoryTheory.MorphismProperty.relative_isStableUnderComposition registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Immersions.lean, line 233 (StacksFrontier): “parts (1)-(3), in the generality of a relatively representable morphism property: the relative property of a property stable under composition is again stable under composition”.
CategoryTheory.MorphismProperty.comp_mem registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Immersions.lean, line 236 (StacksFrontier): “parts (1)-(3), the conclusion read off from that stability: a composite of two morphisms with a property stable under composition again has it”.

Tag 02YW, a lemma

Tag 02YW in the Stacks Project.

AlgebraicGeometry.Space.isClosedImmersion_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ImmersionBaseChange.lean, line 113. The attribute's comment: “closed immersions”. References: EGA I (4.3.2), “closed immersion”.

Stacks 02YW for closed immersions: a base change of a closed immersion of algebraic spaces over S is a closed immersion.

theorem isClosedImmersion_of_isPullback {F G H P : AlgebraicSpaces B S hS}
    {f : F ⟶ H} {g : G ⟶ H} {fst : P ⟶ F} {snd : P ⟶ G} (sq : IsPullback fst snd f g)
    (hf : IsClosedImmersion B S hS f.hom) :
    IsClosedImmersion B S hS snd.hom

AlgebraicGeometry.Space.isOpenImmersion_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ImmersionBaseChange.lean, line 122. The attribute's comment: “open immersions”. References: EGA I (4.3.2), “open immersion”.

Stacks 02YW for open immersions: a base change of an open immersion of algebraic spaces over S is an open immersion.

theorem isOpenImmersion_of_isPullback {F G H P : AlgebraicSpaces B S hS}
    {f : F ⟶ H} {g : G ⟶ H} {fst : P ⟶ F} {snd : P ⟶ G} (sq : IsPullback fst snd f g)
    (hf : IsOpenImmersion B S hS f.hom) :
    IsOpenImmersion B S hS snd.hom

AlgebraicGeometry.Space.isImmersion_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ImmersionBaseChange.lean, line 131. The attribute's comment: “immersions”. References: EGA I (4.3.2), “immersion”.

Stacks 02YW for immersions: a base change of an immersion of algebraic spaces over S is an immersion.

theorem isImmersion_of_isPullback {F G H P : AlgebraicSpaces B S hS}
    {f : F ⟶ H} {g : G ⟶ H} {fst : P ⟶ F} {snd : P ⟶ G} (sq : IsPullback fst snd f g)
    (hf : IsImmersion B S hS f.hom) :
    IsImmersion B S hS snd.hom

Tag 02YX, a lemma

Tag 02YX in the Stacks Project.

AlgebraicGeometry.Space.isOpenSubspace_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OpenImmersionCriteria.lean, line 107. The attribute's comment: “open subspaces”.

An open subspace of an algebraic space over S which is contained in a second subfunctor is an open subspace of that subfunctor.

theorem isOpenSubspace_of_le (F₁ F₂ : Subfunctor F) (hF₁ : IsOpenSubspace B S hS F₁)
    (h : F₁ ≤ F₂) :
    IsOpenSubspace B S hS (Subfunctor.range (Subfunctor.homOfLe h))

AlgebraicGeometry.Space.isClosedSubspace_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OpenImmersionCriteria.lean, line 117. The attribute's comment: “closed subspaces”.

A closed subspace of an algebraic space over S which is contained in a second subfunctor is a closed subspace of that subfunctor.

theorem isClosedSubspace_of_le (F₁ F₂ : Subfunctor F) (hF₁ : IsClosedSubspace B S hS F₁)
    (h : F₁ ≤ F₂) :
    IsClosedSubspace B S hS (Subfunctor.range (Subfunctor.homOfLe h))

AlgebraicGeometry.Space.isLocallyClosedSubspace_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OpenImmersionCriteria.lean, line 127. The attribute's comment: “locally closed subspaces”.

A locally closed subspace of an algebraic space over S which is contained in a second subfunctor is a locally closed subspace of that subfunctor.

theorem isLocallyClosedSubspace_of_le (F₁ F₂ : Subfunctor F)
    (hF₁ : IsLocallyClosedSubspace B S hS F₁) (h : F₁ ≤ F₂) :
    IsLocallyClosedSubspace B S hS (Subfunctor.range (Subfunctor.homOfLe h))

Tag 02YY, a definition

Tag 02YY in the Stacks Project.

AlgebraicGeometry.Space.IsZariskiCover, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiCover.lean, line 35.

A family U of subfunctors of a presheaf F on the big fppf site of S is a Zariski covering of F when every member is an open subspace and the map from the coproduct of the members to F is locally surjective for the fppf topology.

abbrev IsZariskiCover (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (I : Type u) (U : I → Subfunctor F) : Prop

Tag 02YZ, a definition

Tag 02YZ in the Stacks Project.

AlgebraicGeometry.Space.OpenSubspaces, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallZariskiSite.lean, line 223. The attribute's comment: “underlying category”.

The category of open subspaces of an algebraic space, with inclusions as morphisms.

public abbrev OpenSubspaces

AlgebraicGeometry.Space.OpenSubspaces.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallZariskiSite.lean, line 231. The attribute's comment: “covering families”.

A family of open subspaces covers an open subspace if it is a Zariski cover of that subspace in the sense of Stacks 02YY.

public abbrev IsCovering
    (E : Covering.{u + 1, u + 1, u} (OpenSubspaces B S hS F)) : Prop

AlgebraicGeometry.Space.OpenSubspaces.isSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallZariskiSite.lean, line 294. The attribute's comment: “site axioms”.

Zariski covering families satisfy the axioms of a site.

public theorem isSite : IsSite (IsCovering B S hS F)

Sources

LeanAlgebraicGeometry.Space.IsOpenImmersion · AlgebraicGeometry.Space.IsOpenSubspace · AlgebraicGeometry.Space.IsClosedImmersion · AlgebraicGeometry.Space.IsClosedSubspace · AlgebraicGeometry.Space.IsImmersion · AlgebraicGeometry.Space.IsLocallyClosedSubspace · AlgebraicGeometry.Space.isOpenImmersion_comp · AlgebraicGeometry.Space.isClosedImmersion_comp

Section65.13 Separation conditions on algebraic spaces #

Section 65.13 of the Stacks Project, Tag 02X3. 3 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02X3, the section

Tag 02X3 in the Stacks Project.

AlgebraicGeometry.Space.isQuasiSeparatedOver_of_isSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactDiagonalQuasiAffine.lean, line 82. The attribute's comment: “separated gives a quasi-compact diagonal”.

Stacks 02X3. An algebraic space separated over S is quasi-separated over S: a diagonal which is a closed immersion is in particular quasi-compact. Together with the definition of quasi-separatedness this is the parenthetical remark of Section 65.13, that the diagonal is quasi-compact as soon as F is separated or quasi-separated over S.

theorem isQuasiSeparatedOver_of_isSeparatedOver (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsSeparatedOver B S hS F) : IsQuasiSeparatedOver B S hS F

AlgebraicGeometry.Space.presheaf_isSeparated_inf_quasiFinite_diag_of_isQuasiSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactDiagonalQuasiAffine.lean, line 98. The attribute's comment: “a quasi-compact diagonal is quasi-finite and separated”.

Stacks 02X3. Let F be an algebraic space over S whose diagonal is quasi-compact, that is, which is quasi-separated over S. Then the diagonal is separated and quasi-finite: every represented base change of it is a separated, locally quasi-finite, locally of finite type and quasi-compact morphism of schemes.

Separatedness is Stacks 02X4, part (3); locally quasi-finite and locally of finite type are Stacks 02X4, part (4); quasi-compactness is the hypothesis.

theorem presheaf_isSeparated_inf_quasiFinite_diag_of_isQuasiSeparatedOver
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hΔ : IsQuasiSeparatedOver B S hS F) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@AlgebraicGeometry.IsSeparated.{u} ⊓ @AlgebraicGeometry.LocallyQuasiFinite.{u} ⊓
          @AlgebraicGeometry.LocallyOfFiniteType.{u} ⊓ @AlgebraicGeometry.QuasiCompact.{u} :
        MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) (diag F)

AlgebraicGeometry.Space.presheaf_isQuasiAffineHom_diag_of_isQuasiSeparatedOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactDiagonalQuasiAffine.lean, line 120. The attribute's comment: “a quasi-compact diagonal is quasi-affine”.

Stacks 02X3. Let F be an algebraic space over S whose diagonal is quasi-compact, that is, which is quasi-separated over S. Then the diagonal is quasi-affine: every represented base change of it is a quasi-affine morphism of schemes.

The diagonal is separated and quasi-finite, and a separated quasi-finite morphism of schemes is quasi-affine by Stacks 02LR.

theorem presheaf_isQuasiAffineHom_diag_of_isQuasiSeparatedOver
    (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hF : IsAlgebraicSpace B S hS F)
    (hΔ : IsQuasiSeparatedOver B S hS F) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@AlgebraicGeometry.IsQuasiAffineHom.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) (diag F)

Tag 02X4, a lemma

Tag 02X4 in the Stacks Project.

AlgebraicGeometry.presheaf_locallyOfFiniteType_diag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DiagonalProperties.lean, line 332. The attribute's comment: “part (1)”.

Stacks 02X4, part (1). The diagonal of an algebraic space over S is locally of finite type: every represented base change of it is a morphism of schemes locally of finite type.

theorem presheaf_locallyOfFiniteType_diag (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) (diag F)

AlgebraicGeometry.presheaf_monomorphisms_diag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DiagonalProperties.lean, line 346. The attribute's comment: “part (2)”.

Stacks 02X4, part (2). The diagonal of an algebraic space over S is a monomorphism: every represented base change of it is a monomorphism of schemes.

theorem presheaf_monomorphisms_diag (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (MorphismProperty.monomorphisms Scheme.{u})
      (BigFppfOver.toScheme B S hS))) (diag F)

AlgebraicGeometry.presheaf_isSeparated_diag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DiagonalProperties.lean, line 360. The attribute's comment: “part (3)”.

Stacks 02X4, part (3). The diagonal of an algebraic space over S is separated: every represented base change of it is a separated morphism of schemes. This follows from part (2), a monomorphism of schemes being separated.

theorem presheaf_isSeparated_diag (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      (@IsSeparated.{u} : MorphismProperty Scheme.{u})
      (BigFppfOver.toScheme B S hS))) (diag F)

AlgebraicGeometry.presheaf_locallyQuasiFinite_diag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DiagonalProperties.lean, line 374. The attribute's comment: “part (4)”.

Stacks 02X4, part (4). The diagonal of an algebraic space over S is locally quasi-finite: every represented base change of it is a morphism of schemes which is locally of finite type and has discrete fibres.

theorem presheaf_locallyQuasiFinite_diag (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hF : IsAlgebraicSpace B S hS F) :
    (MorphismProperty.presheaf (MorphismProperty.inverseImage
      ((@LocallyOfFiniteType.{u} : MorphismProperty Scheme.{u}) ⊓
        (@LocallyQuasiFinite.{u} : MorphismProperty Scheme.{u}))
      (BigFppfOver.toScheme B S hS))) (diag F)

Tag 02X5, a definition

Tag 02X5 in the Stacks Project.

AlgebraicGeometry.Space.IsSeparatedOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Separated.lean, line 57. The attribute's comment: “separated”.

An algebraic space over S is separated over S when its diagonal is a closed immersion of algebraic spaces.

abbrev IsSeparatedOver (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

AlgebraicGeometry.Space.IsLocallySeparatedOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Separated.lean, line 63. The attribute's comment: “locally_separated”.

An algebraic space over S is locally separated over S when its diagonal is an immersion of algebraic spaces.

abbrev IsLocallySeparatedOver (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

AlgebraicGeometry.Space.IsQuasiSeparatedOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Separated.lean, line 69. The attribute's comment: “quasi_separated”.

An algebraic space over S is quasi-separated over S when its diagonal is quasi-compact after every representable base change.

abbrev IsQuasiSeparatedOver (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

AlgebraicGeometry.Space.IsZariskiLocallyQuasiSeparatedOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Separated.lean, line 77. The attribute's comment: “zariski_locally_quasi_separated”.

An algebraic space over S is Zariski locally quasi-separated over S when it admits a Zariski covering by open subspaces which are quasi-separated over S.

abbrev IsZariskiLocallyQuasiSeparatedOver (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) : Prop

Sources

LeanAlgebraicGeometry.Space.isQuasiSeparatedOver_of_isSeparatedOver · AlgebraicGeometry.Space.presheaf_isSeparated_inf_quasiFinite_diag_of_isQuasiSeparatedOver · AlgebraicGeometry.Space.presheaf_isQuasiAffineHom_diag_of_isQuasiSeparatedOver · AlgebraicGeometry.presheaf_locallyOfFiniteType_diag · AlgebraicGeometry.presheaf_monomorphisms_diag · AlgebraicGeometry.presheaf_isSeparated_diag · AlgebraicGeometry.presheaf_locallyQuasiFinite_diag · AlgebraicGeometry.Space.IsSeparatedOver

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

65.3 Representable morphisms of… to 65.13 Separation conditions on…

Section65.3 Representable morphisms of presheaves#

Tag 02W9, a lemma

Tag 02WA, a lemma

Tag 02WB, a lemma

Tag 02WC, a lemma

Tag 02WD, a lemma

Tag 05L9, a lemma

Sources

Section65.4 Lists of useful properties of morphisms of schemes#

Tag 02WF, a remark

Tag 02WG, a remark

Tag 02WH, a remark

Sources

Section65.5 Properties of representable morphisms of presheaves#

Tag 025V, a definition

Tag 02YN, a remark

Tag 02WJ, a lemma

Tag 02WK, a lemma

Tag 02WL, a lemma

Tag 03KD, a lemma

Tag 02WM, a lemma

Tag 02YO, a lemma

Tag 05VM, a lemma

Tag 025W, a lemma

Tag 0CB7, a lemma

Sources

Section65.6 Algebraic spaces#

Tag 025Y, a definition

Tag 025Z, a lemma

Tag 0260, a definition

Sources

Section65.7 Fibre products of algebraic spaces#

Tag 02X0, a lemma

Tag 04T9, a lemma

Tag 02X2, a lemma

Sources

Section65.8 Glueing algebraic spaces#

Tag 0F15, a lemma

Tag 02WO, a lemma

Tag 02WP, a lemma

Tag 02WQ, a lemma

Tag 02WR, a lemma

Sources

Section65.9 Presentations of algebraic spaces#

Tag 0262, a lemma

Tag 02WS, a definition

Tag 0263, a definition

Sources

Section65.10 Algebraic spaces and equivalence relations#

Tag 02WT, a lemma

Tag 02WU, a lemma

Tag 02WV, a lemma

Tag 0265, a lemma

Tag 02WW, a theorem

Sources

Section65.11 Algebraic spaces, retrofitted#

Tag 0BGQ, a lemma

Tag 0BGR, a lemma

Tag 02WY, a lemma

Tag 02WZ, a lemma

Tag 03I2, a lemma

Tag 02X1, a lemma

Sources

Section65.12 Immersions and Zariski coverings of algebraic spaces#

Tag 02YU, a definition

Tag 02YV, a lemma

Tag 02YW, a lemma

Tag 02YX, a lemma

Tag 02YY, a definition

Tag 02YZ, a definition

Sources

Section65.13 Separation conditions on algebraic spaces#

Tag 02X3, the section

Tag 02X4, a lemma

Tag 02X5, a definition

Sources

Section65.3 Representable morphisms of presheaves #

Section65.4 Lists of useful properties of morphisms of schemes #

Section65.5 Properties of representable morphisms of presheaves #

Section65.6 Algebraic spaces #

Section65.7 Fibre products of algebraic spaces #

Section65.8 Glueing algebraic spaces #

Section65.9 Presentations of algebraic spaces #

Section65.10 Algebraic spaces and equivalence relations #

Section65.11 Algebraic spaces, retrofitted #

Section65.12 Immersions and Zariski coverings of algebraic spaces #

Section65.13 Separation conditions on algebraic spaces #