74.3 Descent data for… to 74.22 Descent data for spaces…

Section74.3 Descent data for quasi-coherent sheaves #

Section 74.3 of the Stacks Project, Tag 04W2. 4 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04W3, a definition

Tag 04W3 in the Stacks Project.

AlgebraicGeometry.Space.QuasiCoherentDescent.DescentDatum, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/QuasiCoherent/DescentData.lean, line 109. The attribute's comment: “part (1)”.

Stacks 04W3, part (1). A descent datum for quasi-coherent modules relative to a family (f i : Y i ⟶ X) of algebraic spaces over X: a quasi-coherent module on each Y i, an isomorphism of the two inverse images on each pairwise fibre product, and the cocycle condition.

structure DescentDatum (Y : I → AlgebraicSpaces B S hS) (f : ∀ i, Y i ⟶ X)

AlgebraicGeometry.Space.QuasiCoherentDescent.DescentDatum.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/QuasiCoherent/DescentData.lean, line 136. The attribute's comment: “part (2)”.

Stacks 04W3, part (2). A morphism of descent data: a family of morphisms of the component modules commuting with every pairwise isomorphism.

structure DescentDatum.Hom {Y : I → AlgebraicSpaces B S hS} {f : ∀ i, Y i ⟶ X}
    (D E : DescentDatum B S hS Y f)

Tag 04W4, a lemma

Tag 04W4 in the Stacks Project.

AlgebraicGeometry.Space.QuasiCoherentDescent.pullbackDatum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/QuasiCoherent/FamilyPullback.lean, line 331. The attribute's comment: “part (1)”.

Stacks 04W4, part (1). The pullback of a descent datum for quasi-coherent modules along a morphism of families of morphisms with fixed target: the inverse images (h₀ i)^*F (s₀ i), with the pairwise isomorphisms of the given datum pulled back to the pairwise fibre products of the source family.

def pullbackDatum (Φ : 𝒰.HomOver 𝒱 g)
    (D : DescentDatum B S hS 𝒱.X 𝒱.f) : DescentDatum B S hS 𝒰.X 𝒰.f

AlgebraicGeometry.Space.QuasiCoherentDescent.pullbackFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/QuasiCoherent/FamilyPullback.lean, line 369. The attribute's comment: “part (2)”.

Stacks 04W4, part (2). Pullback of descent data along a morphism of families of morphisms with fixed target is a functor on the categories of descent data of Stacks 04W3.

def pullbackFunctor (Φ : 𝒰.HomOver 𝒱 g) :
    DescentDatum B S hS 𝒱.X 𝒱.f ⥤ DescentDatum B S hS 𝒰.X 𝒰.f

AlgebraicGeometry.Space.QuasiCoherentDescent.pullbackCompare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/QuasiCoherent/FamilyPullback.lean, line 382. The attribute's comment: “part (3), the comparison isomorphism”.

Stacks 04W4, part (3). For two morphisms of families with the same morphism of targets, the pairwise isomorphism of the given datum read on U i along h₀ i and h₀' i is an isomorphism of the i-th components of the two pulled-back data.

def pullbackCompare (Φ Ψ : 𝒰.HomOver 𝒱 g) (D : DescentDatum B S hS 𝒱.X 𝒱.f) (i : 𝒰.I₀) :
    (modulePullback B S hS (Φ.h₀ i)).obj (D.F (Φ.s₀ i)) ≅
      (modulePullback B S hS (Ψ.h₀ i)).obj (D.F (Ψ.s₀ i))

AlgebraicGeometry.Space.QuasiCoherentDescent.pullbackCompare_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/QuasiCoherent/FamilyPullback.lean, line 394. The attribute's comment: “part (3), compatibility of the comparison with the pairwise isomorphisms”.

Stacks 04W4, part (3). The components of pullbackCompare commute with the pairwise isomorphisms of the two pulled-back data, so that they constitute a morphism of descent data: two applications of the cocycle condition of the given datum on the test space U i ×_U U j, which carries four morphisms to members of 𝒱.

theorem pullbackCompare_naturality
    (Φ Ψ : 𝒰.HomOver 𝒱 g) (D : DescentDatum B S hS 𝒱.X 𝒱.f) (i j : 𝒰.I₀) :
    (modulePullback B S hS (pairFst B S hS 𝒰.X 𝒰.f i j)).mapIso
          (pullbackCompare B S hS Φ Ψ D i) ≪≫ pullbackTransition B S hS Ψ D i j =
      pullbackTransition B S hS Φ D i j ≪≫
        (modulePullback B S hS (pairSnd B S hS 𝒰.X 𝒰.f i j)).mapIso
          (pullbackCompare B S hS Φ Ψ D j)

AlgebraicGeometry.Space.QuasiCoherentDescent.pullbackCompare_datum_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/QuasiCoherent/FamilyPullback.lean, line 454. The attribute's comment: “part (3), naturality of the comparison in the descent datum”.

Stacks 04W4, part (3). The comparison is natural in the descent datum: it commutes with the components of the pulled-back morphisms, which are the components of AlgebraicGeometry.Space.QuasiCoherentDescent.pullbackHom.

theorem pullbackCompare_datum_naturality (Φ Ψ : 𝒰.HomOver 𝒱 g)
    {D E : DescentDatum B S hS 𝒱.X 𝒱.f} (a : D ⟶ E) (i : 𝒰.I₀) :
    (modulePullback B S hS (Φ.h₀ i)).map (a.app (Φ.s₀ i)) ≫
        (pullbackCompare B S hS Φ Ψ E i).hom =
      (pullbackCompare B S hS Φ Ψ D i).hom ≫
        (modulePullback B S hS (Ψ.h₀ i)).map (a.app (Ψ.s₀ i))

Tag 04W5, a definition

Tag 04W5 in the Stacks Project.

AlgebraicGeometry.Space.QuasiCoherentDescent.canonicalDescentDatum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/QuasiCoherent/CanonicalDatum.lean, line 77. The attribute's comment: “the canonical descent datum”.

Stacks 04W5. The canonical descent datum (M|_{Y i}, can) of a quasi-coherent 𝒪_X-module M relative to a family (f i : Y i ⟶ X): the inverse images (f i)^*M, with the canonical comparison of the two inverse images of M on each pairwise fibre product.

def canonicalDescentDatum
    (Y : I → AlgebraicSpaces B S hS) (f : ∀ i, Y i ⟶ X)
    (M : Modules.{u, u} B S hS X.1 X.2) (hM : M.IsQuasicoherentOnSite) :
    DescentDatum B S hS Y f

AlgebraicGeometry.Space.QuasiCoherentDescent.trivialDescentDatum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/QuasiCoherent/CanonicalDatum.lean, line 116. The attribute's comment: “the trivial descent datum”.

Stacks 04W5. The trivial descent datum of a quasi-coherent 𝒪_X-module: its canonical descent datum relative to the one-member family {𝟙 X}.

def trivialDescentDatum
    (M : Modules.{u, u} B S hS X.1 X.2) (hM : M.IsQuasicoherentOnSite) :
    DescentDatum B S hS (fun _ : PUnit.{v + 1} => X) (fun _ => 𝟙 X)

AlgebraicGeometry.Space.QuasiCoherentDescent.IsEffective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/QuasiCoherent/CanonicalDatum.lean, line 124. The attribute's comment: “effective descent datum”.

Stacks 04W5. A descent datum for quasi-coherent modules is effective when it is isomorphic to the canonical descent datum of a quasi-coherent module on the target.

def IsEffective
    (Y : I → AlgebraicSpaces B S hS) (f : ∀ i, Y i ⟶ X)
    (D : DescentDatum B S hS Y f) : Prop

Tag 04W6, a lemma

Tag 04W6 in the Stacks Project.

AlgebraicGeometry.Space.QuasiCoherentDescent.isEtaleEffective_and_fullyFaithful_of_isZariskiCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/QuasiCoherent/MemberPerMemberIsoDirect.lean, line 167.

For a Zariski covering of an algebraic space, every descent datum for quasi-coherent modules is effective, and the canonical descent functor is fully faithful.

theorem isEtaleEffective_and_fullyFaithful_of_isZariskiCovering
    (hcov : IsZariskiCovering B S hS I (fun i => (Yi i).1) (fun i => (f i).hom)) :
    (∀ D : DescentDatum B S hS Yi f, IsEtaleEffective B S hS Yi f hf D) ∧
      (etaleCanonicalDescentFunctor B S hS Yi f hf).Full ∧
        (etaleCanonicalDescentFunctor B S hS Yi f hf).Faithful

Sources

Section74.4 Fpqc descent of quasi-coherent sheaves #

Section 74.4 of the Stacks Project, Tag 04W7. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04W8, a proposition

Tag 04W8 in the Stacks Project.

AlgebraicGeometry.Space.QuasiCoherentDescent.faithful_canonicalDescentFunctor_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/QuasiCoherent/FpqcChartLocalization.lean, line 537. The attribute's comment: “the faithfulness half of the full-faithfulness clause, for an fpqc covering of algebraic spaces: the members of an fpqc covering are flat and the covering is jointly surjective on points, so a morphism of quasi-coherent modules is determined by its inverse images along it and the canonical descent functor of Stacks 04W5 is faithful. The fullness half of that clause and the effectivity clause are separate assertions of the tag and are not proved here”.

The faithfulness half of the full-faithfulness clause of Stacks 04W8. The canonical descent functor of Stacks 04W5, from the quasi-coherent 𝒪_X-modules of Stacks 03G9 to the descent data of Stacks 04W3 relative to an fpqc covering (f i : X i ⟶ X) of algebraic spaces in the sense of Stacks 03MQ, is faithful.

The covering is the only input. Its members are flat and it is jointly surjective on points, so AlgebraicGeometry.Space.QuasiCoherentDescent.reprFpqcHomInjective supplies the represented case of the reduction above. The two data needed to form the functor are supplied, not assumed: the associativity coherence of the comparison of inverse images of Stacks 03LU is AlgebraicGeometry.Space.modulePullbackCompIsoAssoc, and quasi-coherence of the inverse images is Stacks 03GA for an arbitrary morphism of algebraic spaces.

This is the faithfulness half only. The fullness half of the full-faithfulness clause, and the effectivity clause of the same tag, are not proved here.

theorem faithful_canonicalDescentFunctor_of_isFpqcCovering
    (hf : IsFpqcCovering B S hS fun i => (f i).hom) :
    (canonicalDescentFunctor' B S hS Xi f).Faithful

AlgebraicGeometry.Space.QuasiCoherentDescent.isEquivalence_canonicalDescentFunctor'_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/QuasiCoherent/FpqcDescentTransitivity.lean, line 613.

Stacks 04W8: for an fpqc covering (f i : X i ⟶ X) of algebraic spaces, the canonical descent functor from the quasi-coherent 𝒪_X-modules to the descent data relative to the covering is an equivalence.

This is the tag, both of whose clauses the equivalence carries: the functor is fully faithful, and every descent datum on quasi-coherent sheaves for the family is effective — which is essential surjectivity by …essSurj_canonicalDescentFunctor'_iff_forall_isEffective. The full-faithfulness clause is …nonempty_fullyFaithful_canonicalDescentFunctor_of_isFpqcCovering and the effectivity clause is …forall_isEffective_of_isFpqcCovering; both are proved, and nothing is assumed beyond the covering.

theorem isEquivalence_canonicalDescentFunctor'_of_isFpqcCovering
    (Xi : I → AlgebraicSpaces B S hS) (f : ∀ i, Xi i ⟶ X)
    (hf : IsFpqcCovering B S hS fun i => (f i).hom) :
    (canonicalDescentFunctor' B S hS Xi f).IsEquivalence

Sources

LeanAlgebraicGeometry.Space.QuasiCoherentDescent.faithful_canonicalDescentFunctor_of_isFpqcCovering · AlgebraicGeometry.Space.QuasiCoherentDescent.isEquivalence_canonicalDescentFunctor'_of_isFpqcCovering

Section74.5 Quasi-coherent modules and affines #

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

Tag 0H03, an equation

Tag 0H03 in the Stacks Project.

AlgebraicGeometry.Space.affineEtaleRestriction_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineEtaleRingedTopos.lean, line 130. The attribute's comment: “equivalence of topoi”.

Restriction from the small étale site of an algebraic space to its affine étale charts is an equivalence on sheaves of sets, at the universe of the objects of the site.

theorem affineEtaleRestriction_isEquivalence :
    (affineEtaleRestriction B S hS F hF (Type (u + 1))).IsEquivalence

AlgebraicGeometry.Space.affineEtaleToSmallEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineEtaleRingedTopos.lean, line 145. The attribute's comment: “canonical morphism of ringed topoi”.

The canonical morphism from the affine étale ringed topos of an algebraic space to its small étale ringed topos.

Its inverse image is restriction to affine charts and is an equivalence, and its structure map is an isomorphism which, after forgetting the ring operations, is the identity of the restricted structure sheaf.

noncomputable def affineEtaleToSmallEtale :
    { f : RingedToposHom
        (affineEtaleRingedTopos B S hS F hF)
        (liftedSmallEtaleRingedTopos B S hS F) //
      f.toToposHom.inverseImage =
        affineEtaleRestriction B S hS F hF (Type (u + 1)) ∧
      f.toToposHom.inverseImage.IsEquivalence ∧
      IsIso f.fSharpInverseImage ∧
      HEq ((affineEtaleRingedTopos B S hS F hF).forgetRing.map
        f.fSharpInverseImage)
        (𝟙 ((affineEtaleRingedTopos B S hS F hF).forgetRing.obj
          (affineEtaleRingedTopos B S hS F hF).O)) }

Tag 0H04, a lemma

Tag 0H04 in the Stacks Project.

AlgebraicGeometry.Space.isIso_restrictionBaseChange_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineEtaleCartesianModules.lean, line 241. The attribute's comment: “quasi-coherent implies cartesian”.

A quasi-coherent sheaf of modules on the affine étale site of an algebraic space is cartesian: each restriction map exhibits its target as a base change of its source.

theorem isIso_restrictionBaseChange_of_isQuasicoherentOnSite
    (M : SheafOfModules.{max m (u + 1)} (affineEtaleRingSheaf B S hS F hF))
    (hM : M.IsQuasicoherentOnSite)
    {U V : AffineEtale B S hS F} (f : U ⟶ V) :
    IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u + 1, m} M.val f.op)

AlgebraicGeometry.Space.affineEtale_quasicoherent_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineEtaleQuasicoherentModules.lean, line 270. The attribute's comment: “the equivalence of (1), (2) and (3)”.

Stacks 0H04. Let F be an algebraic space over a scheme S and let 𝓕 be a presheaf of 𝒪_F-modules on the affine étale site of F. The following are equivalent:

for every morphism U ⟶ U' of F_{affine, étale} the base-change map 𝓕(U') ⊗_{𝒪_F(U')} 𝒪_F(U) ⟶ 𝓕(U) is an isomorphism;

𝓕 is a sheaf and is quasi-coherent on the ringed site (F_{affine, étale}, 𝒪_F) in the sense of Modules on Sites, Definition 03DL (6);

𝓕 is a sheaf and corresponds, under the equivalence of Stacks 0H03, to a quasi-coherent 𝒪_F-module on the small étale site of F.

Conditions (2) and (3) carry the sheaf condition as a conjunct, because quasi-coherence is a condition on a sheaf of modules; the source's proof of (1) ⇒ (2) likewise begins by proving the sheaf condition.

(1) ⇒ (2) is AlgebraicGeometry.Space.isQuasicoherentOnSite_of_isIso_restrictionBaseChange, (2) ⇒ (1) is AlgebraicGeometry.Space.isIso_restrictionBaseChange_of_isQuasicoherentOnSite, and (2) ⇔ (3) is AlgebraicGeometry.Space.isQuasicoherentOnSite_affineEtaleLiftedModuleRestriction_iff together with the essential surjectivity of restriction to the affine charts.

theorem affineEtale_quasicoherent_tfae
    (M : PresheafOfModules.{u + 1}
      ((affineEtaleStructureSheaf B S hS F hF).obj ⋙ forget₂ CommRingCat RingCat)) :
    List.TFAE
      [∀ (U V : AffineEtale B S hS F) (f : U ⟶ V),
          IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u + 1, u + 1} M f.op),
        ∃ h : Presheaf.IsSheaf (AffineEtale.topology B S hS F) M.presheaf,
          (⟨M, h⟩ : SheafOfModules.{u + 1}
            (affineEtaleRingSheaf B S hS F hF)).IsQuasicoherentOnSite,
        ∃ h : Presheaf.IsSheaf (AffineEtale.topology B S hS F) M.presheaf,
          ∃ G : SheafOfModules.{u + 1} (liftedSmallEtaleRingSheaf B S hS F),
            G.IsQuasicoherentOnSite ∧
              Nonempty ((affineEtaleLiftedModuleRestriction B S hS F hF).obj G ≅ ⟨M, h⟩)]

Sources

LeanAlgebraicGeometry.Space.affineEtaleRestriction_isEquivalence · AlgebraicGeometry.Space.affineEtaleToSmallEtale · AlgebraicGeometry.Space.isIso_restrictionBaseChange_of_isQuasicoherentOnSite · AlgebraicGeometry.Space.affineEtale_quasicoherent_tfae

Section74.6 Descent of finiteness properties of modules #

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

Tag 060U, a lemma

Tag 060U in the Stacks Project.

AlgebraicGeometry.Space.isFiniteType_of_pullback_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/ModuleFiniteness.lean, line 344. The attribute's comment: “finite type read on the restriction to every etale scheme chart; at the module universe of the structure rings”.

Stacks 060U. A quasi-coherent module on an algebraic space whose inverse image along every member of an fpqc covering is of finite type is itself of finite type, finite type being read on the restriction to every étale scheme chart.

theorem isFiniteType_of_pullback_fpqc
    {I : Type v} {X : AlgebraicSpaces B S hS} (Xᵢ : I → AlgebraicSpaces B S hS)
    (f : ∀ i, Xᵢ i ⟶ X) (F : Modules.{u, u} B S hS X.obj X.property)
    (hF : F.IsQuasicoherentOnSite)
    (hf : IsFpqcCovering B S hS fun i ↦ (f i).hom)
    (hft : ∀ (i : I) (W : SmallEtale B S hS (Xᵢ i).obj),
      (restrictToChart B S hS (Xᵢ i).property
        ((modulePullback B S hS (f i)).obj F) W).IsFiniteType) :
    ∀ V : SmallEtale B S hS X.obj,
      (restrictToChart B S hS X.property F V).IsFiniteType

Tag 060V, a lemma

Tag 060V in the Stacks Project.

AlgebraicGeometry.Space.isFinitePresentation_of_pullback_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/ModuleFinitePresentation.lean, line 42.

Let F be a quasi-coherent 𝒪_X-module on an algebraic space X and let {f_i : X_i → X} be an fpqc covering such that each f_i^* F is an 𝒪_{X_i}-module of finite presentation. Then F is an 𝒪_X-module of finite presentation.

theorem isFinitePresentation_of_pullback_fpqc {I : Type v} {X : AlgebraicSpaces B S hS}
    (Xᵢ : I → AlgebraicSpaces B S hS) (f : ∀ i, Xᵢ i ⟶ X)
    (F : Modules.{u, u} B S hS X.obj X.property) (hF : F.IsQuasicoherentOnSite)
    (hf : IsFpqcCovering B S hS fun i ↦ (f i).hom)
    (hfp : ∀ i, ((modulePullback B S hS (f i)).obj F).IsFinitePresentation) :
    F.IsFinitePresentation

Tag 060W, a lemma

Tag 060W in the Stacks Project.

AlgebraicGeometry.Space.isFlat_of_pullback_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/ModuleFiniteness.lean, line 371. The attribute's comment: “flatness read on the restriction to every etale scheme chart; at the module universe of the structure rings”.

Stacks 060W. A quasi-coherent module on an algebraic space whose inverse image along every member of an fpqc covering is flat is itself flat, flatness being read on the restriction to every étale scheme chart.

theorem isFlat_of_pullback_fpqc
    {I : Type v} {X : AlgebraicSpaces B S hS} (Xᵢ : I → AlgebraicSpaces B S hS)
    (f : ∀ i, Xᵢ i ⟶ X) (F : Modules.{u, u} B S hS X.obj X.property)
    (hF : F.IsQuasicoherentOnSite)
    (hf : IsFpqcCovering B S hS fun i ↦ (f i).hom)
    (hflat : ∀ (i : I) (W : SmallEtale B S hS (Xᵢ i).obj),
      SheafOfModules.IsFlat.{u, u, u, u} (O := (etaleChartScheme B S hS W).toRingedSpace.sheaf)
        (restrictToChart B S hS (Xᵢ i).property
          ((modulePullback B S hS (f i)).obj F) W)) :
    ∀ V : SmallEtale B S hS X.obj,
      SheafOfModules.IsFlat.{u, u, u, u} (O := (etaleChartScheme B S hS V).toRingedSpace.sheaf)
        (restrictToChart B S hS X.property F V)

Tag 060X, a lemma

Tag 060X in the Stacks Project.

AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_of_pullback_isFpqcCovering_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeFpqcDescentQuasicoherent.lean, line 47.

Let X be an algebraic space over S, let 𝓕 be a quasi-coherent 𝒪_X-module and let {f i : X i ⟶ X} be an fpqc covering of X such that every pullback (f i)^*𝓕 is finite locally free. Then 𝓕 is finite locally free.

theorem isFiniteLocallyFreeOnSite_of_pullback_isFpqcCovering_of_isQuasicoherentOnSite
    {I : Type v} {X : AlgebraicSpaces B S hS} {Xi : I → AlgebraicSpaces B S hS}
    (f : ∀ i, Xi i ⟶ X) (hf : IsFpqcCovering B S hS fun i ↦ (f i).hom)
    (F : Modules.{u, u} B S hS X.obj X.property) (hF : F.IsQuasicoherentOnSite)
    (hFlf : ∀ i, SheafOfModules.IsFiniteLocallyFreeOnSite
      ((modulePullback B S hS (f i)).obj F)) :
    SheafOfModules.IsFiniteLocallyFreeOnSite F

Tag 060Y, a lemma

Tag 060Y in the Stacks Project.

AlgebraicGeometry.Space.isLocallyProjective_of_pullback_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/ModuleFiniteness.lean, line 399. The attribute's comment: “local projectivity in the chartwise sense of Tag 060R; at the module universe of the structure rings”.

Stacks 060Y. A quasi-coherent module on an algebraic space whose inverse image along every member of an fpqc covering is locally projective is itself locally projective, in the chartwise sense of Stacks 060R.

theorem isLocallyProjective_of_pullback_fpqc
    {I : Type v} {X : AlgebraicSpaces B S hS} (Xᵢ : I → AlgebraicSpaces B S hS)
    (f : ∀ i, Xᵢ i ⟶ X) (F : QuasicoherentSheaves.{u, u} B S hS X.obj X.property)
    (hf : IsFpqcCovering B S hS fun i ↦ (f i).hom)
    (hproj : ∀ i, IsLocallyProjective B S hS (Xᵢ i).property
      ⟨(modulePullback B S hS (f i)).obj F.obj,
        isQuasicoherentOnSite_modulePullback_of_isQuasicoherentOnSite B S hS (f i)
          F.obj F.property⟩) :
    IsLocallyProjective B S hS X.property F

Tag 060Z, a lemma

Tag 060Z in the Stacks Project.

AlgebraicGeometry.Space.isFiniteType_iff_smallBaseChangePushforward_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePushforwardFiniteType.lean, line 302.

For a finite morphism f : X ⟶ Y of algebraic spaces a quasi-coherent 𝒪_X-module F is of finite type if and only if its direct image f_*F is.

theorem isFiniteType_iff_smallBaseChangePushforward_of_isQuasicoherentOnSite
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsFinite B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hqc : F.IsQuasicoherentOnSite) :
    F.IsFiniteType ↔
      ((smallBaseChangeModulePushforward B S hS f
        (relativelyRepresentable_hom_of_isFinite B S hS f hf)).obj F).IsFiniteType

Tag 0610, a lemma

Tag 0610 in the Stacks Project.

AlgebraicGeometry.Space.isFinitePresentation_iff_smallBaseChangePushforward_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartSchemeFinitePresentationDescent.lean, line 166.

For a finite morphism f : X ⟶ Y of finite presentation of algebraic spaces a quasi-coherent 𝒪_X-module F is of finite presentation if and only if its direct image f_*F is.

theorem isFinitePresentation_iff_smallBaseChangePushforward_of_isQuasicoherentOnSite
    (f : X ⟶ Y) (hf : IsFinite B S hS f.hom) (hfp : IsFinitePresentation B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hqc : F.IsQuasicoherentOnSite) :
    F.IsFinitePresentation ↔
      ((smallBaseChangeModulePushforward B S hS f
        (relativelyRepresentable_hom_of_isFinite B S hS f hf)).obj F).IsFinitePresentation

Sources

LeanAlgebraicGeometry.Space.isFiniteType_of_pullback_fpqc · AlgebraicGeometry.Space.isFinitePresentation_of_pullback_fpqc · AlgebraicGeometry.Space.isFlat_of_pullback_fpqc · AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_of_pullback_isFpqcCovering_of_isQuasicoherentOnSite · AlgebraicGeometry.Space.isLocallyProjective_of_pullback_fpqc · AlgebraicGeometry.Space.isFiniteType_iff_smallBaseChangePushforward_of_isQuasicoherentOnSite · AlgebraicGeometry.Space.isFinitePresentation_iff_smallBaseChangePushforward_of_isQuasicoherentOnSite

Section74.7 Fpqc coverings #

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

Tag 04P1, a lemma

Tag 04P1 in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_openSubspace_of_fpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FpqcOpenSubspaceDescent.lean, line 420.

A family of open subspaces Wᵢ i of the members of an fpqc covering f i : Tᵢ i ⟶ T whose two pullbacks to each Tᵢ i ×_T Tᵢ j agree is the family of preimages of a unique open subspace of T.

public theorem existsUnique_openSubspace_of_fpqcCovering
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type v} {T : AlgebraicSpaces B S hS}
    {Tᵢ : I → AlgebraicSpaces B S hS}
    (f : ∀ i, Tᵢ i ⟶ T)
    (hf : IsFpqcCovering B S hS (fun i => (f i).hom))
    (Wᵢ : ∀ i, {W : Subfunctor (Tᵢ i).1 // IsOpenSubspace B S hS W})
    (hW : ∀ i j,
      (Wᵢ i).1.preimage (pullback.fst (f i).hom (f j).hom) =
        (Wᵢ j).1.preimage (pullback.snd (f i).hom (f j).hom)) :
    ∃! W : {W : Subfunctor T.1 // IsOpenSubspace B S hS W},
      ∀ i, W.1.preimage (f i).hom = (Wᵢ i).1

Tag 04P2, a lemma

Tag 04P2 in the Stacks Project.

AlgebraicGeometry.Space.existsUnique_desc_of_fpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FpqcMorphismDescent.lean, line 485.

Stacks 04P2. For an fpqc covering {X i ⟶ Y} of algebraic spaces over S and an algebraic space Z over S, the diagram Mor(Y, Z) ⟶ ∏ i, Mor(X i, Z) ⇉ ∏ (i, j), Mor(X i ×_Y X j, Z) is an equalizer: a family of morphisms X i ⟶ Z agreeing on the fibre products X i ×_Y X j descends uniquely to Y ⟶ Z.

The input is Stacks 0APL, that an algebraic space is a sheaf for the fpqc topology; the rest is formal.

public theorem existsUnique_desc_of_fpqcCovering
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type v} {X : I → AlgebraicSpaces B S hS}
    {Y : AlgebraicSpaces B S hS}
    (f : ∀ i, X i ⟶ Y)
    (hf : IsFpqcCovering B S hS (fun i => (f i).hom))
    (Z : AlgebraicSpaces B S hS)
    (g : ∀ i, X i ⟶ Z)
    (hg : ∀ i j,
      (ObjectProperty.homMk (pullback.fst (f i).hom (f j).hom) :
        AlgebraicSpaces.fiberProduct B S hS (f i) (f j) ⟶ X i) ≫ g i =
      (ObjectProperty.homMk (pullback.snd (f i).hom (f j).hom) :
        AlgebraicSpaces.fiberProduct B S hS (f i) (f j) ⟶ X j) ≫ g j) :
    ∃! h : Y ⟶ Z, ∀ i, f i ≫ h = g i

Sources

LeanAlgebraicGeometry.Space.existsUnique_openSubspace_of_fpqcCovering · AlgebraicGeometry.Space.existsUnique_desc_of_fpqcCovering

Section74.8 Descent of finiteness and smoothness properties of morphisms #

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

Tag 06NR, a lemma

Tag 06NR in the Stacks Project.

AlgebraicGeometry.Space.isFlat_of_comp_of_locallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/MorphismFiniteness.lean, line 184. The attribute's comment: “flatness”.

Stacks 06NR. Flatness of a composite of morphisms of algebraic spaces descends to the second factor when the first factor is surjective as a morphism of fppf sheaves.

theorem isFlat_of_comp_of_locallySurjective
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (_hZ : IsAlgebraicSpace B S hS Z)
    (f : X ⟶ Y) (g : Y ⟶ Z)
    (hfg : IsFlat B S hS (f ≫ g))
    (hf : Presheaf.IsLocallySurjective (BigFppfOver.topology B S hS) f) :
    IsFlat B S hS g

AlgebraicGeometry.Space.isLocallyOfFiniteType_of_comp_of_locallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/MorphismFiniteness.lean, line 204. The attribute's comment: “locally finite type”.

Stacks 06NR. Local finite type of a composite of morphisms of algebraic spaces descends to the second factor when the first factor is surjective as a morphism of fppf sheaves.

theorem isLocallyOfFiniteType_of_comp_of_locallySurjective
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (_hZ : IsAlgebraicSpace B S hS Z)
    (f : X ⟶ Y) (g : Y ⟶ Z)
    (hfg : IsLocallyOfFiniteType B S hS (f ≫ g))
    (hf : Presheaf.IsLocallySurjective (BigFppfOver.topology B S hS) f) :
    IsLocallyOfFiniteType B S hS g

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_comp_of_locallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/MorphismFiniteness.lean, line 224. The attribute's comment: “locally finite presentation”.

Stacks 06NR. Local finite presentation of a composite of morphisms of algebraic spaces descends to the second factor when the first factor is surjective as a morphism of fppf sheaves.

theorem isLocallyOfFinitePresentation_of_comp_of_locallySurjective
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (_hZ : IsAlgebraicSpace B S hS Z)
    (f : X ⟶ Y) (g : Y ⟶ Z)
    (hfg : IsLocallyOfFinitePresentation B S hS (f ≫ g))
    (hf : Presheaf.IsLocallySurjective (BigFppfOver.topology B S hS) f) :
    IsLocallyOfFinitePresentation B S hS g

Tag 0AHC, a lemma

Tag 0AHC in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFiniteType_of_commonFppfDescentSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/MorphismFiniteness.lean, line 244. The attribute's comment: “the case of local finite type”. References: EGA IV (11.3.16), “locally of finite type”.

Stacks 0AHC, the case of local finite type. In a commutative triangle X ⟶ Y ⟶ B of algebraic spaces whose first morphism is surjective, flat and locally of finite presentation, if X ⟶ B is locally of finite type then so is Y ⟶ B.

theorem isLocallyOfFiniteType_of_commonFppfDescentSituation
    (T : CommonFppfDescentSituation.{u}) (hp : IsLocallyOfFiniteType T.site T.S T.hS T.p) :
    IsLocallyOfFiniteType T.site T.S T.hS T.q

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_of_commonFppfDescentSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/MorphismFiniteness.lean, line 260. The attribute's comment: “the case of local finite presentation”. References: EGA IV (11.3.16), “loc. fin. presentation”; SGA 4 IV (8.5.5), “partial”.

Stacks 0AHC, the case of local finite presentation. In a commutative triangle X ⟶ Y ⟶ B of algebraic spaces whose first morphism is surjective, flat and locally of finite presentation, if X ⟶ B is locally of finite presentation then so is Y ⟶ B.

theorem isLocallyOfFinitePresentation_of_commonFppfDescentSituation
    (T : CommonFppfDescentSituation.{u})
    (hp : IsLocallyOfFinitePresentation T.site T.S T.hS T.p) :
    IsLocallyOfFinitePresentation T.site T.S T.hS T.q

Tag 0AHD, a lemma

Tag 0AHD in the Stacks Project.

AlgebraicGeometry.Space.isSmooth_of_comp_surjective_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/Permanence.lean, line 115. The attribute's comment: “smooth case”.

Stacks 0AHD, smooth case. In a commuting triangle p = f ≫ q of morphisms of algebraic spaces over S with f surjective and smooth, smoothness of p implies smoothness of q.

theorem isSmooth_of_comp_surjective_isSmooth
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (_hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z)
    (hcomm : p = f ≫ q) (hfs : IsSurjective B S hS f)
    (hf : IsSmooth B S hS f) (hp : IsSmooth B S hS p) :
    IsSmooth B S hS q

AlgebraicGeometry.Space.isEtale_of_comp_surjective_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/Permanence.lean, line 132. The attribute's comment: “étale case”.

Stacks 0AHD, étale case. In a commuting triangle p = f ≫ q of morphisms of algebraic spaces over S with f surjective and étale, étaleness of p implies étaleness of q.

theorem isEtale_of_comp_surjective_isEtale
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z)
    (hcomm : p = f ≫ q) (hfs : IsSurjective B S hS f)
    (hf : IsEtale B S hS f) (hp : IsEtale B S hS p) :
    IsEtale B S hS q

AlgebraicGeometry.Space.isSyntomic_of_comp_surjective_isSyntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/SyntomicPermanence.lean, line 51. The attribute's comment: “syntomic case”.

Stacks 0AHD, syntomic case. In a commuting triangle p = f ≫ q of morphisms of algebraic spaces over S with f surjective and syntomic, syntomicity of p implies syntomicity of q.

theorem isSyntomic_of_comp_surjective_isSyntomic
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (_hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z)
    (hcomm : p = f ≫ q) (hfs : IsSurjective B S hS f)
    (hf : IsSyntomic B S hS f) (hp : IsSyntomic B S hS p) :
    IsSyntomic B S hS q

Tag 0AHE, a lemma

Tag 0AHE in the Stacks Project.

AlgebraicGeometry.Space.isSmooth_of_comp_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/FppfPermanence.lean, line 151. The attribute's comment: “smooth case”.

Stacks 0AHE, smooth case. In a commuting triangle p = f ≫ q of morphisms of algebraic spaces over S with f surjective, flat and locally of finite presentation, smoothness of p implies smoothness of q.

theorem isSmooth_of_comp_of_fppf
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (_hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z)
    (hcomm : p = f ≫ q) (hfs : IsSurjective B S hS f) (hff : IsFlat B S hS f)
    (hfp : IsLocallyOfFinitePresentation B S hS f) (hp : IsSmooth B S hS p) :
    IsSmooth B S hS q

AlgebraicGeometry.Space.isEtale_of_comp_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/FppfPermanence.lean, line 167. The attribute's comment: “étale case”.

Stacks 0AHE, étale case. In a commuting triangle p = f ≫ q of morphisms of algebraic spaces over S with f surjective, flat and locally of finite presentation, étaleness of p implies étaleness of q.

theorem isEtale_of_comp_of_fppf
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (p : X ⟶ Z) (q : Y ⟶ Z)
    (hcomm : p = f ≫ q) (hfs : IsSurjective B S hS f) (hff : IsFlat B S hS f)
    (hfp : IsLocallyOfFinitePresentation B S hS f) (hp : IsEtale B S hS p) :
    IsEtale B S hS q

Tag 0AHF, a lemma

Tag 0AHF in the Stacks Project.

AlgebraicGeometry.Space.isSyntomic_of_comp_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SyntomicFactor.lean, line 102. The attribute's comment: “syntomicity of q”.

Stacks 0AHF. Syntomicity descends from a composite of morphisms of algebraic spaces over S along a surjective, flat morphism which is locally of finite presentation: if f : X ⟶ Y is surjective, flat and locally of finite presentation and f ≫ q is syntomic, then q : Y ⟶ Z is syntomic.

theorem isSyntomic_of_comp_of_fppf
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (q : Y ⟶ Z)
    (hfs : IsSurjective B S hS f) (hff : IsFlat B S hS f)
    (hflfp : IsLocallyOfFinitePresentation B S hS f)
    (hp : IsSyntomic B S hS (f ≫ q)) :
    IsSyntomic B S hS q

AlgebraicGeometry.Space.isSyntomic_of_isSyntomic_comp_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Morphisms/SyntomicFactor.lean, line 117. The attribute's comment: “syntomicity of f”.

Stacks 0AHF. A flat morphism of algebraic spaces over S which is locally of finite presentation is syntomic as soon as its composite with another morphism is syntomic. The source states this alongside the conclusion about the other factor, under the extra hypothesis that f be surjective; surjectivity is not needed here.

theorem isSyntomic_of_isSyntomic_comp_of_fppf
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z) (f : X ⟶ Y) (q : Y ⟶ Z)
    (hff : IsFlat B S hS f) (hflfp : IsLocallyOfFinitePresentation B S hS f)
    (hp : IsSyntomic B S hS (f ≫ q)) :
    IsSyntomic B S hS f

Sources

Section74.9 Descending properties of spaces #

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

Tag 06DQ, a lemma

Tag 06DQ in the Stacks Project.

AlgebraicGeometry.Space.isGeometricallyUnibranchAt_of_isFlatAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DescendingProperties/GeometricallyUnibranch.lean, line 108.

Stacks 06DQ. Let f : F ⟶ G be a morphism of algebraic spaces over a scheme S and let x be a point of |F|. If f is flat at x and F is geometrically unibranch at x, then G is geometrically unibranch at f(x).

theorem isGeometricallyUnibranchAt_of_isFlatAt (hF : IsAlgebraicSpace B S hS F)
    (hG : IsAlgebraicSpace B S hS G) (f : F ⟶ G) (x : points B S hS F)
    (hf : IsFlatAt B S hS f x) (hx : IsGeometricallyUnibranchAt B S hS F x) :
    IsGeometricallyUnibranchAt B S hS G (pointsMap B S hS F f x)

Tag 06MI, a lemma

Tag 06MI in the Stacks Project.

AlgebraicGeometry.Space.isReduced_of_flat_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/Reduced.lean, line 41.

A flat surjective morphism of algebraic spaces over S whose source is reduced has reduced target.

theorem isReduced_of_flat_of_surjective
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hflat : IsFlat B S hS f)
    (hsurj : IsSurjective B S hS f)
    (hred : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsReduced T)) :
    HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsReduced T)

Tag 06MJ, a lemma

Tag 06MJ in the Stacks Project.

AlgebraicGeometry.Space.isLocallyNoetherian_of_isSurjective_of_isFlat_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/Noetherian.lean, line 85.

Stacks 06MJ. Local Noetherianity passes from the source of a surjective, flat morphism of algebraic spaces over S locally of finite presentation to its target.

This is the case P = AlgebraicGeometry.IsLocallyNoetherian of hasEtaleLocalProperty_of_isSurjective_of_isFlat_of_isLocallyOfFinitePresentation, whose two locality hypotheses hold for local Noetherianity of schemes.

theorem isLocallyNoetherian_of_isSurjective_of_isFlat_of_isLocallyOfFinitePresentation
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hfp : IsLocallyOfFinitePresentation B S hS f)
    (hflat : IsFlat B S hS f)
    (hsurj : IsSurjective B S hS f)
    (hnoeth : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsLocallyNoetherian T)) :
    HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsLocallyNoetherian T)

Tag 06MK, a lemma

Tag 06MK in the Stacks Project.

AlgebraicGeometry.Space.hasEtaleLocalProperty_isRegular_of_isSurjective_of_isFlat_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/Regular.lean, line 109. References: SGA 1 I (9.2), “converse (X reg ⇒ Y reg)”.

Stacks 06MK. Regularity passes from the source of a surjective, flat morphism of algebraic spaces over S locally of finite presentation to its target.

A regular scheme is locally Noetherian, so a regular étale chart of the source witnesses local Noetherianity of the source; Stacks 06MJ carries that to the target, and hasEtaleLocalProperty_isRegular_of_isSurjective_of_isFlat then applies.

theorem hasEtaleLocalProperty_isRegular_of_isSurjective_of_isFlat_of_isLocallyOfFinitePresentation
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hfp : IsLocallyOfFinitePresentation B S hS f)
    (hflat : IsFlat B S hS f)
    (hsurj : IsSurjective B S hS f)
    (hreg : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsRegular T)) :
    HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsRegular T)

Tag 0GB3, a lemma

Tag 0GB3 in the Stacks Project.

AlgebraicGeometry.Space.hasEtaleLocalPropertyULift_isReduced_of_isSmoothULift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalSpace/ReductionSmoothBaseChange.lean, line 143. The attribute's comment: “reducedness of the source, in an arbitrary value universe”.

Stacks 0GB3, reducedness of the source, for presheaves with values in a universe max w u independent of the universe u of the schemes: a smooth morphism of algebraic spaces over S whose target is reduced has reduced source.

A reduced surjective étale atlas V of the target and an atlas W of the base change of the morphism along it form a commuting square of étale charts, so the scheme morphism W ⟶ V is smooth and W is reduced by Stacks 033B; it is a reduced surjective étale atlas of the source.

theorem hasEtaleLocalPropertyULift_isReduced_of_isSmoothULift
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (max w u)}
    (hF : IsAlgebraicSpaceULift.{w} B S hS F) (hG : IsAlgebraicSpaceULift.{w} B S hS G)
    (f : F ⟶ G) (hf : IsSmoothULift.{w} B S hS f)
    (hred : HasEtaleLocalPropertyULift.{w} B S hS G (fun T : Scheme.{u} ↦ IsReduced T)) :
    HasEtaleLocalPropertyULift.{w} B S hS F (fun T : Scheme.{u} ↦ IsReduced T)

AlgebraicGeometry.Space.isReduced_of_flat_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/Reduced.lean, line 41. The attribute's comment: “reducedness of the target under surjectivity”.

A flat surjective morphism of algebraic spaces over S whose source is reduced has reduced target.

theorem isReduced_of_flat_of_surjective
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y)
    (hflat : IsFlat B S hS f)
    (hsurj : IsSurjective B S hS f)
    (hred : HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsReduced T)) :
    HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsReduced T)

AlgebraicGeometry.Space.isReduced_source_of_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/Reduced.lean, line 64. The attribute's comment: “reducedness of the source”. References: SGA 1 II (3.1), “reduced, Y ⇒ X”.

A smooth morphism of algebraic spaces over S whose target is reduced has reduced source.

theorem isReduced_source_of_isSmooth
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) (hf : IsSmooth B S hS f)
    (hred : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} => IsReduced T)) :
    HasEtaleLocalProperty B S hS X (fun T : Scheme.{u} => IsReduced T)

Sources

LeanAlgebraicGeometry.Space.isGeometricallyUnibranchAt_of_isFlatAt · AlgebraicGeometry.Space.isReduced_of_flat_of_surjective · AlgebraicGeometry.Space.isLocallyNoetherian_of_isSurjective_of_isFlat_of_isLocallyOfFinitePresentation · AlgebraicGeometry.Space.hasEtaleLocalProperty_isRegular_of_isSurjective_of_isFlat_of_isLocallyOfFinitePresentation · AlgebraicGeometry.Space.hasEtaleLocalPropertyULift_isReduced_of_isSmoothULift · AlgebraicGeometry.Space.isReduced_source_of_isSmooth

Section74.10 Descending properties of morphisms #

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

Tag 03YH, a definition

Tag 03YH in the Stacks Project.

AlgebraicGeometry.Space.Topology, an inductive in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Coverings.lean, line 375. The attribute's comment: “the five topologies”.

Stacks 03YH. The topologies for which locality on the base of a property of morphisms of algebraic spaces is considered.

inductive Topology

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

Stacks 03YH. A family of morphisms of algebraic spaces over S with common target is a covering family for the topology τ when its source and target presheaves are algebraic spaces and it satisfies the covering condition of τ.

abbrev Topology.IsCovering (τ : Topology)
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type v} {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (Yi : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (g : ∀ i, Yi i ⟶ Y) : Prop

AlgebraicGeometry.Space.Topology.precoverage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Coverings.lean, line 410. The attribute's comment: “the precoverage”.

Stacks 03YH. The precoverage on the category of algebraic spaces over S presented by the τ-covering families. A property P of morphisms of algebraic spaces is local on the base for τ exactly when CategoryTheory.MorphismProperty.IsLocalAtTarget P (τ.precoverage B S hS).

def Topology.precoverage (τ : Topology)
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    Precoverage (AlgebraicSpaces B S hS)

Declarations registered for the tag:

CategoryTheory.MorphismProperty.IsLocalAtTarget registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Coverings.lean, line 418 (StacksFrontier): “locality on the base”. References: SGA 3 IV (4.6.3), “(e_T)”; SGA 3 VIB (2.0), “b)”.

Tag 06EM, a lemma

Tag 06EM in the Stacks Project.

AlgebraicGeometry.Space.prop_fiberProduct_fst_of_isLocalAtTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/LocalAtTarget.lean, line 121.

A property of morphisms of algebraic spaces over S which is local on the base for τ is inherited by the base change along any morphism of the kind belonging to τ.

theorem prop_fiberProduct_fst_of_isLocalAtTarget
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (τ : Topology) (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsLocalAtTarget (τ.precoverage.{u, v} B S hS)]
    {X Y Y' : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : P f)
    (hg : match τ with
      | .fpqc => IsFlat B S hS g.hom
      | .fppf => IsFlat B S hS g.hom ∧ IsLocallyOfFinitePresentation B S hS g.hom
      | .syntomic => IsSyntomic B S hS g.hom
      | .smooth => IsSmooth B S hS g.hom
      | .etale => IsEtale B S hS g.hom) :
    P (ObjectProperty.homMk (pullback.fst g.hom f.hom) :
      AlgebraicSpaces.fiberProduct B S hS g f ⟶ Y')

Tag 06R2, a lemma

Tag 06R2 in the Stacks Project.

AlgebraicGeometry.Space.largestOpenSubspace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargestOpenLocus.lean, line 471. The attribute's comment: “existence and maximality”.

Stacks 06R2, existence and maximality. For a property P of morphisms of algebraic spaces over S which is local on the target for a topology τ other than the fpqc topology, every morphism f : X ⟶ Y has a largest open subspace of Y over which its restriction has P.

noncomputable def largestOpenSubspace (τ : Topology) (hτ : τ ≠ .fpqc)
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsLocalAtTarget (Topology.precoverage.{u, u + 1} τ B S hS)]
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    {W : {W : Subfunctor Y.obj // IsOpenSubspace B S hS W} //
      HasPropertyOnOpen B S hS P f W ∧
        ∀ V : {V : Subfunctor Y.obj // IsOpenSubspace B S hS V},
          HasPropertyOnOpen B S hS P f V → V.1 ≤ W.1}

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

Stacks 06R2, part (1). A morphism g : Y' ⟶ Y which τ admits as a member of a covering family and along which the base change of f has P factors through the largest open locus of f.

theorem factorsThrough_largestOpenSubspace (τ : Topology) (hτ : τ ≠ .fpqc)
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsLocalAtTarget (Topology.precoverage.{u, u + 1} τ B S hS)]
    {X Y Y' : AlgebraicSpaces B S hS} (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hg : τ.IsMember B S hS g.hom) (hP : P (pullback.snd f g)) :
    ∃ h : Y' ⟶ openObject B S hS (largestOpenSubspace B S hS τ hτ P f).1,
      h ≫ openInclusion B S hS (largestOpenSubspace B S hS τ hτ P f).1 = g

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

Stacks 06R2, part (2). The largest open locus of a base change of f along a morphism g which τ admits as a member of a covering family is the inverse image of the largest open locus of f.

theorem largestOpenSubspace_baseChange (τ : Topology) (hτ : τ ≠ .fpqc)
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsLocalAtTarget (Topology.precoverage.{u, u + 1} τ B S hS)]
    {X Y Y' : AlgebraicSpaces B S hS} (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hg : τ.IsMember B S hS g.hom) :
    (largestOpenSubspace B S hS τ hτ P (pullback.snd f g)).1.1 =
      ((largestOpenSubspace B S hS τ hτ P f).1.1).preimage g.hom

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

Stacks 06R2, part (3). The largest open locus of the base change of f along a member of a τ-covering of its target is the inverse image of the largest open locus of f.

theorem largestOpenSubspace_covering (τ : Topology) (hτ : τ ≠ .fpqc)
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsLocalAtTarget (Topology.precoverage.{u, u + 1} τ B S hS)]
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) {I : Type v}
    (Yi : I → AlgebraicSpaces B S hS) (g : ∀ i, Yi i ⟶ Y)
    (hg : τ.IsCovering B S hS (fun i ↦ (Yi i).obj) (fun i ↦ (g i).hom)) (i : I) :
    (largestOpenSubspace B S hS τ hτ P (pullback.snd f (g i))).1.1 =
      ((largestOpenSubspace B S hS τ hτ P f).1.1).preimage (g i).hom

Tag 041J, a lemma

Tag 041J in the Stacks Project.

AlgebraicGeometry.Space.isLocalAtTarget_fpqc_of_affineDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FpqcLocalAtTarget.lean, line 641.

An affine-local morphism property which descends along surjective flat maps of affine schemes and respects finite coproducts is fpqc local on the target.

public theorem isLocalAtTarget_fpqc_of_affineDescent
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    (hcoprod : ∀ (n : ℕ)
      (X Y : Fin n → AlgebraicSpaces B S hS)
      (f : ∀ i, X i ⟶ Y i)
      (X₀ Y₀ : AlgebraicSpaces B S hS)
      (ιX : ∀ i, X i ⟶ X₀) (ιY : ∀ i, Y i ⟶ Y₀)
      (g : X₀ ⟶ Y₀),
      IsColimit (Cofan.mk X₀ ιX) →
      IsColimit (Cofan.mk Y₀ ιY) →
      (∀ i, f i ≫ ιY i = ιX i ≫ g) →
      (∀ i, P (f i)) → P g)
    (haffine : ∀ {X Y : AlgebraicSpaces B S hS}
      (f : X ⟶ Y),
      P f ↔ ∀ (T : BigAffineFppf B S hS)
        (g : schemeSpace
          ((BigAffineFppf.inclusion B S hS).obj T) ⟶ Y),
        P (pullback.snd f g))
    (hdescent : ∀ (T T' : BigAffineFppf B S hS)
      (g : T' ⟶ T),
      Flat ((BigAffineFppf.toScheme B S hS).map g) →
      Surjective ((BigAffineFppf.toScheme B S hS).map g) →
      ∀ (X : AlgebraicSpaces B S hS)
        (f : X ⟶ schemeSpace
          ((BigAffineFppf.inclusion B S hS).obj T)),
        P (pullback.snd f
          (schemeSpaceMap
            ((BigAffineFppf.inclusion B S hS).map g))) → P f) :
    P.IsLocalAtTarget (Space.Topology.precoverage.{u, v}
      .fpqc B S hS)

Sources

LeanAlgebraicGeometry.Space.Topology · AlgebraicGeometry.Space.Topology.IsCovering · AlgebraicGeometry.Space.Topology.precoverage · CategoryTheory.MorphismProperty.IsLocalAtTarget · AlgebraicGeometry.Space.prop_fiberProduct_fst_of_isLocalAtTarget · AlgebraicGeometry.Space.largestOpenSubspace · AlgebraicGeometry.Space.factorsThrough_largestOpenSubspace · AlgebraicGeometry.Space.largestOpenSubspace_baseChange

Section74.11 Descending properties of morphisms in the fpqc topology #

Section 74.11 of the Stacks Project, Tag 041K. 30 tags here are carried by 39 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 041L, a lemma

Tag 041L in the Stacks Project.

AlgebraicGeometry.Space.quasiCompact_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactFpqcLocalAtTarget.lean, line 218. References: SGA 4 IV (8.5.5), “more general”.

Quasi-compactness of morphisms of algebraic spaces over S is local on the base for the fpqc topology.

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

Tag 041N, a lemma

Tag 041N in the Stacks Project.

AlgebraicGeometry.Space.isQuasiSeparated_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiSeparatedFpqcLocalAtTarget.lean, line 147. References: EGA IV (2.7.1), “more general”; SGA 4 IV (8.5.5), “more general”.

Stacks 041N. Quasi-separatedness of a morphism of algebraic spaces over S is local on the target for the fpqc topology.

One direction is stability under base change (Stacks 03KL). In the other, quasi-separatedness of f : X ⟶ Y is quasi-compactness of Δ_f : X ⟶ X ×_Y X; the given fpqc covering of Y pulls back to one of X ×_Y X by part (3) of Stacks 03MR, the base change of Δ_f along each member of it is the relative diagonal of the corresponding base change of f, and so quasi-compactness of Δ_f follows from Stacks 041L.

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

Tag 041O, a lemma

Tag 041O in the Stacks Project.

AlgebraicGeometry.Space.universallyClosed_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Fpqc/UniversallyClosed.lean, line 221.

Stacks 041O. Universal closedness of morphisms of algebraic spaces over S is local on the base for the fpqc topology.

Universal closedness is being universally a closed morphism, so the ascent half is formal. For the descent half, condition (3) of Stacks 03IT reduces the assertion to closedness of the base changes along morphisms from the affine objects of the site; over such an affine T the fpqc condition of Stacks 03MQ supplies a finite affine family covering T and refining the given covering, and closedness of a morphism to a representable algebraic space descends along it.

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

Tag 041P, a lemma

Tag 041P in the Stacks Project.

AlgebraicGeometry.Space.universallyOpen_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Fpqc/UniversallyOpen.lean, line 228. References: SGA 4 IV (8.5.5), “more general”.

Stacks 041P. Universal openness of morphisms of algebraic spaces over S is local on the base for the fpqc topology.

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

Tag 0CFW, a lemma

Tag 0CFW in the Stacks Project.

AlgebraicGeometry.Space.universallySubmersive_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Fpqc/UniversallySubmersive.lean, line 152.

Universal submersiveness of morphisms of algebraic spaces over S is local on the base for the fpqc topology.

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

Tag 041Q, a lemma

Tag 041Q in the Stacks Project.

AlgebraicGeometry.Space.surjective_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SurjectiveFpqcLocalAtTarget.lean, line 223. References: SGA 4 IV (8.5.5), “more general”.

Surjectivity of morphisms of algebraic spaces over S is local on the base for the fpqc topology.

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

AlgebraicGeometry.Space.surjective_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SurjectiveFpqcLocalAtTarget.lean, line 252. The attribute's comment: “the fppf precoverage”.

Stacks 041Q at the fppf precoverage: surjectivity of morphisms of algebraic spaces over S is local at the target for the fppf topology. This is the form in which the relative properties of Stacks 03YK ask for it; the comparison of precoverages is Stacks 0DFQ, AlgebraicGeometry.Space.fppfPrecoverage_le_fpqcPrecoverage.

instance surjective_isLocalAtTarget_fppf :
    (surjectiveMorphismProperty B S hS).IsLocalAtTarget
      (Topology.fppf.precoverage.{u, v} B S hS)

Tag 041R, a lemma

Tag 041R in the Stacks Project.

AlgebraicGeometry.Space.universallyInjective_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversallyInjectiveFpqcLocalAtTarget.lean, line 145.

Stacks 041R. Universal injectivity of morphisms of algebraic spaces over S is local on the base for the fpqc topology.

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

Tag 0CFX, a lemma

Tag 0CFX in the Stacks Project.

AlgebraicGeometry.Space.universalHomeomorphism_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UniversalHomeomorphismFpqcLocalAtTarget.lean, line 264. References: SGA 4 IV (8.5.5), “more general”.

Stacks 0CFX. Being a universal homeomorphism is, for morphisms of algebraic spaces over S, local on the base for the fpqc topology of Stacks 03YH: such a morphism is a universal homeomorphism exactly when its base change to every member of some fpqc covering family of its target is a universal homeomorphism.

A morphism is a universal homeomorphism exactly when it is surjective, universally injective and universally open, surjectivity is fpqc local on the base by Stacks 041Q, universal injectivity by Stacks 041R and universal openness by Stacks 041P, so their conjunction is.

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

Tag 041S, a lemma

Tag 041S in the Stacks Project.

AlgebraicGeometry.Space.locallyOfFiniteType_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/FinitenessFpqcLocality.lean, line 54.

Being locally of finite type is, for morphisms of algebraic spaces over S, local on the base for the fpqc topology.

instance locallyOfFiniteType_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) => IsLocallyOfFiniteType B S hS f.hom)
      (Topology.precoverage.{u, v} .fpqc B S hS)

Tag 041T, a lemma

Tag 041T in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePresentationFpqcLocalAtTarget.lean, line 355. References: EGA IV (2.7.1), “more general”; SGA 3 VIB (10.8), “(i)⇒(ii)”; SGA 4 IV (8.5.5), “more general”.

Stacks Project, Tag 041T (Lemma 74.11.10 of Chapter 74, Descent and Algebraic Spaces). The property 𝒫(f) = "f is locally of finite presentation" of morphisms of algebraic spaces over S is fpqc local on the base.

The setting is the source's own. By the conventions of that chapter (Stacks 041I, Section 74.2) every scheme lies in a big fppf site Sch_fppf, here B, and S is one of its objects; algebraic spaces over S are the objects of AlgebraicSpaces B S S_mem, and local finite presentation of a morphism of algebraic spaces is that of Stacks 03XP, part (1). "Fpqc local on the base" is Definition 74.10.1 (Stacks 03YH) at the fpqc topology: for every fpqc covering {Yᵢ → Y} of algebraic spaces in the sense of Stacks 03MQ, indexed by a type in any universe v, and every morphism f : X ⟶ Y, the morphism f is locally of finite presentation if and only if every base change Yᵢ ×_Y X → Yᵢ is. That is the class CategoryTheory.MorphismProperty.IsLocalAtTarget at Topology.fpqc.precoverage, whose coverings are exactly the families Presieve.ofArrows Yᵢ gᵢ with gᵢ an fpqc covering of Y.

The scheme-level statement, for morphisms of schemes, is Descent, Lemma 35.23.13 (Stacks 02KY), Stacks.Descent.locallyOfFinitePresentation_isLocalAtTarget_fpqc; the proof of the source reduces to it, and so does this one.

instance isLocallyOfFinitePresentation_isLocalAtTarget_fpqc
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (S_mem : B.Contains S) :
    MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S S_mem⦄ (f : X ⟶ Y) =>
        IsLocallyOfFinitePresentation B S S_mem f.hom)
      (Topology.fpqc.precoverage.{u, v} B S S_mem)

Tag 041U, a lemma

Tag 041U in the Stacks Project.

AlgebraicGeometry.Space.isFiniteType_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteTypeFpqcLocalAtTarget.lean, line 81.

Stacks 041U. Being of finite type, as a property of morphisms of algebraic spaces over S, is local on the target for the fpqc topology.

Being of finite type is being locally of finite type and quasi-compact (Stacks 03XF, part (3)); the first conjunct is local on the target for the fpqc topology by Stacks 041S and the second by Stacks 041L, so their conjunction is.

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

AlgebraicGeometry.Space.finiteType_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/FinitenessFpqcLocality.lean, line 66.

Being of finite type is, for morphisms of algebraic spaces over S, local on the base for the fpqc topology.

instance finiteType_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) => IsFiniteType B S hS f.hom)
      (Topology.precoverage.{u, v} .fpqc B S hS)

Tag 041V, a lemma

Tag 041V in the Stacks Project.

AlgebraicGeometry.Space.finitePresentation_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/FinitePresentationFpqcLocality.lean, line 71. References: SGA 4 IV (8.5.5), “more general”.

Stacks 041V. Being of finite presentation is, for morphisms of algebraic spaces over S, local on the base for the fpqc topology of Stacks 03YH.

Being of finite presentation is being locally of finite presentation (Stacks 041T) together with quasi-compactness (Stacks 041L) and quasi-separatedness (Stacks 041N).

instance finitePresentation_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) => IsFinitePresentation B S hS f.hom)
      (Topology.precoverage.{u, v} .fpqc B S hS)

Tag 041W, a lemma

Tag 041W in the Stacks Project.

AlgebraicGeometry.Space.isFlat_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFpqcLocality.lean, line 111.

Stacks 041W. Flatness of a morphism of algebraic spaces over S is local on the target for the fpqc topology.

instance isFlat_isLocalAtTarget_fpqc
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    MorphismProperty.IsLocalAtTarget
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) => IsFlat B S hS f.hom)
      (Topology.fpqc.precoverage.{u, v} B S hS)

AlgebraicGeometry.Space.isFlat_isLocalAtTarget_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/SelfIntersectionFlatProjections.lean, line 87. The attribute's comment: “the fppf precoverage”.

Stacks 041W at the fppf precoverage: flatness of morphisms of algebraic spaces over S is local at the target for the fppf topology. It follows from the fpqc form AlgebraicGeometry.Space.isFlat_isLocalAtTarget_fpqc through AlgebraicGeometry.Space.fppfPrecoverage_le_fpqcPrecoverage, and it is the form in which the relative properties of Stacks 03YK ask for it; it is the exact analogue of AlgebraicGeometry.Space.isLocallyOfFinitePresentation_isLocalAtTarget_fppf and of AlgebraicGeometry.Space.smooth_isLocalAtTarget_fppf.

theorem isFlat_isLocalAtTarget_fppf (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (g : X ⟶ Y) => IsFlat B S hS g.hom)
      (Topology.fppf.precoverage.{u, v} B S hS)

Tag 041X, a lemma

Tag 041X in the Stacks Project.

AlgebraicGeometry.Space.openImmersion_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OpenImmersionFpqcLocalAtTarget.lean, line 371.

Stacks 041X. Being an open immersion of algebraic spaces over S is local on the base for the fpqc topology.

instance openImmersion_isLocalAtTarget_fpqc
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    (openImmersionProperty B S hS).IsLocalAtTarget
      (Topology.precoverage.{u, v} .fpqc B S hS)

Tag 041Y, a lemma

Tag 041Y in the Stacks Project.

AlgebraicGeometry.Space.isomorphisms_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IsomorphismFpqcLocalAtTarget.lean, line 122. References: SGA 4 IV (8.5.5), “more general”.

Stacks 041Y. Being an isomorphism is, for morphisms of algebraic spaces over S, local on the base for the fpqc topology of Stacks 03YH: such a morphism is an isomorphism exactly when its base change to every member of some fpqc covering family of its target is an isomorphism.

A morphism is an isomorphism exactly when it is a surjective open immersion, surjectivity is fpqc local on the base by Stacks 041Q and being an open immersion by Stacks 041X, so their conjunction is.

instance isomorphisms_isLocalAtTarget_fpqc :
    (MorphismProperty.isomorphisms (AlgebraicSpaces B S hS)).IsLocalAtTarget
      (Topology.precoverage.{u, v} .fpqc B S hS)

Tag 041Z, a lemma

Tag 041Z in the Stacks Project.

AlgebraicGeometry.Space.isLocalAtTarget_isAffineHom_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/IndQuasiAffineFpqcSheaf.lean, line 86.

Affineness of morphisms of algebraic spaces is fpqc local on the base, which is Stacks, Tag 041Z.

theorem isLocalAtTarget_isAffineHom_fpqc (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    MorphismProperty.IsLocalAtTarget
      (fun {X Y} (f : X ⟶ Y) => IsAffineHom B S hS f.hom :
        MorphismProperty (AlgebraicSpaces B S hS))
      (Topology.fpqc.precoverage.{u, v} B S hS)

Tag 0420, a lemma

Tag 0420 in the Stacks Project.

AlgebraicGeometry.Space.isClosedImmersion_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionFppfLocalAtTarget.lean, line 72. The attribute's comment: “the fppf precoverage”.

Stacks 0420 at the fppf precoverage: being a closed immersion is local on the base for the fppf topology for morphisms of algebraic spaces over S, so such a morphism is a closed immersion exactly when its base change to every member of some fppf covering of its target is one.

The fpqc form is AlgebraicGeometry.Space.isClosedImmersion_isLocalAtTarget_fpqc, and the two are compared by AlgebraicGeometry.Space.fppfPrecoverage_le_fpqcPrecoverage (Stacks 0DFQ). This is the form in which the relative properties of Stacks 03YK ask for it.

instance isClosedImmersion_isLocalAtTarget_fppf :
    (closedImmersionProperty B S hS).IsLocalAtTarget
      (Topology.precoverage.{u, v} .fppf B S hS)

AlgebraicGeometry.Space.isClosedImmersion_isLocalAtTarget_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionFpqcLocalAtTarget.lean, line 758. References: SGA 3 IV (6.4.1), “(N')”.

Stacks 0420. Being a closed immersion is fpqc local on the base for morphisms of algebraic spaces over S: such a morphism is a closed immersion exactly when its base change to every member of some fpqc covering of its target is one.

theorem isClosedImmersion_isLocalAtTarget_fpqc
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) => IsClosedImmersion B S hS f.hom)
      (Topology.precoverage.{u, v} .fpqc B S hS)

Tag 0421, a lemma

Tag 0421 in the Stacks Project.

AlgebraicGeometry.Space.separated_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedFpqcLocalAtTarget.lean, line 78. References: SGA 4 IV (8.5.5), “more general”.

Stacks 0421. Separatedness of morphisms of algebraic spaces over S is local on the base for the fpqc topology: a morphism is separated exactly when its base change to every member of some fpqc covering of its target is separated.

Separatedness of f : X ⟶ Y is the relative diagonal Δ_f : X ⟶ X ×_Y X being a closed immersion. Pulling a covering {Y i ⟶ Y} back along X ×_Y X ⟶ Y gives a covering of X ×_Y X whose base changes of Δ_f are the relative diagonals of the base changes of f, so Stacks 0420 for closed immersions applies.

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

Tag 0422, a lemma

Tag 0422 in the Stacks Project.

AlgebraicGeometry.Space.isProperULift_of_isPullback_uliftYoneda_family, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeValuedProperEtaleDescent.lean, line 87. The attribute's comment: “for a family of morphisms of the site, in the value universe of a formal algebraic space”. References: SGA 1 VIII (4.8), “partial”.

Stacks 0422 for a family of morphisms of the site, in the value universe Type (u + 1). Let p : F ⟶ U be a morphism of presheaves on the big fppf site of S with values in Type (u + 1) whose source is an algebraic space over S and whose target is the universe-lifted representable sheaf of an object U of the site, and let {qᵢ : Vᵢ ⟶ U} be a family of morphisms of the site whose Yoneda images form an fppf covering family of U in the sense of Stacks 03Y8. If some base change of p along each qᵢ is proper, then p is proper.

The source and the base changes are algebraic spaces, hence universe lifts of presheaves in the value universe of the site; there properness of a lift is properness of the presheaf (AlgebraicGeometry.Space.isProperULift_whiskerRight_iff) and the covering family generates a covering family of the fpqc precoverage of Stacks 03YH, at which properness is local on the base by Stacks 0422.

theorem isProperULift_of_isPullback_uliftYoneda_family
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (u + 1)} {U : BigFppfOver B S hS}
    {p : F ⟶ (uliftYoneda.{u + 1}).obj U} {Idx : Type (u + 1)}
    {V : Idx → BigFppfOver B S hS} {q : ∀ i, V i ⟶ U}
    {F' : Idx → ((BigFppfOver B S hS)ᵒᵖ ⥤ Type (u + 1))}
    {p' : ∀ i, F' i ⟶ (uliftYoneda.{u + 1}).obj (V i)} {k : ∀ i, F' i ⟶ F}
    (sq : ∀ i, IsPullback (k i) (p' i) p ((uliftYoneda.{u + 1}).map (q i)))
    (hF : IsAlgebraicSpaceULift.{u + 1} B S hS F)
    (hcov : IsFppfCovering B S hS (fun i => yoneda.obj (V i)) (fun i => yoneda.map (q i)))
    (hp' : ∀ i, IsProperULift.{u + 1} B S hS (p' i)) :
    IsProperULift.{u + 1} B S hS p

AlgebraicGeometry.Space.isProperULift_of_isPullback_uliftYoneda_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LargeValuedProperEtaleDescent.lean, line 195. The attribute's comment: “for one surjective étale morphism of the site, in the value universe of a formal algebraic space”.

Stacks 0422 for a single surjective étale morphism of the site, in the value universe Type (u + 1). Let p : F ⟶ U be a morphism of presheaves on the big fppf site of S with values in Type (u + 1) whose source is an algebraic space over S and whose target is the universe-lifted representable sheaf of an object U of the site, and let q : U' ⟶ U be a morphism of the site which is surjective and étale on underlying schemes. If some base change of p along q is proper, then p is proper.

The one-member family consisting of the Yoneda image of q is an fppf covering family of its target by AlgebraicGeometry.Space.isFppfCovering_atlas, so this is the family statement at that family.

theorem isProperULift_of_isPullback_uliftYoneda_map
    {F F' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type (u + 1)} {U U' : BigFppfOver B S hS}
    {p : F ⟶ (uliftYoneda.{u + 1}).obj U} {p' : F' ⟶ (uliftYoneda.{u + 1}).obj U'}
    {k : F' ⟶ F} (q : U' ⟶ U)
    (sq : IsPullback k p' p ((uliftYoneda.{u + 1}).map q))
    (hF : IsAlgebraicSpaceULift.{u + 1} B S hS F)
    (hqs : Surjective ((BigFppfOver.toScheme B S hS).map q))
    (hqe : Etale ((BigFppfOver.toScheme B S hS).map q))
    (hp' : IsProperULift.{u + 1} B S hS p') :
    IsProperULift.{u + 1} B S hS p

AlgebraicGeometry.Space.proper_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperFpqcLocalAtTarget.lean, line 65. References: SGA 1 VIII (4.8), “more general”; SGA 4 IV (8.5.5), “more general”.

Stacks 0422. Properness of morphisms of algebraic spaces over S is local on the base for the fpqc topology: a morphism is proper exactly when its base change to every member of some fpqc covering family of its target is proper.

Being proper is being separated, of finite type and universally closed (Stacks 03ZM); the three conjuncts are local on the base for the fpqc topology by Stacks 0421, Stacks 041U and Stacks 041O, so their conjunction is.

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

Tag 0423, a lemma

Tag 0423 in the Stacks Project.

AlgebraicGeometry.Space.isLocalAtTarget_isQuasiAffineHom_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiAffineFpqcChartDescent.lean, line 647. References: EGA IV (2.7.1), “more general”; SGA 4 IV (8.5.5), “more general”.

Stacks 0423 (Lemma 74.11.20 of Chapter 74, Descent and Algebraic Spaces). The property "f is quasi-affine" of morphisms of algebraic spaces over S is fpqc local on the base, in the sense of Definition 74.10.1 (Stacks 03YH): for every fpqc covering {Yᵢ ⟶ Y} of algebraic spaces over S (Stacks 03MQ) and every morphism of algebraic spaces f : X ⟶ Y, the morphism f is quasi-affine if and only if each base change Yᵢ ×_Y X ⟶ Yᵢ is quasi-affine.

The setting is that of the conventions of Chapter 74 (Stacks 041I): S is a scheme of the big fppf site B, algebraic spaces over S are sheaves on the big fppf site of S, and quasi-affineness is the notion of Stacks 03WL, AlgebraicGeometry.Space.IsQuasiAffineHom: every base change to an affine scheme is represented by a quasi-affine scheme. Locality on the base is CategoryTheory.MorphismProperty.IsLocalAtTarget for the fpqc precoverage AlgebraicGeometry.Space.Topology.precoverage .fpqc of the category of algebraic spaces over S, whose covering presieves are those generated by the fpqc coverings, with index sets in any universe.

theorem isLocalAtTarget_isQuasiAffineHom_fpqc (B : BigFppfSite.{u}) (S : Scheme.{u})
    (contains : B.Contains S) :
    MorphismProperty.IsLocalAtTarget
      (fun {X Y : AlgebraicSpaces B S contains} (g : X ⟶ Y) ↦
          IsQuasiAffineHom B S contains g.hom :
        MorphismProperty (AlgebraicSpaces B S contains))
      (Topology.fpqc.precoverage.{u, v} B S contains)

Tag 0424, a lemma

Tag 0424 in the Stacks Project.

AlgebraicGeometry.Space.immersion_inf_quasiCompact_isLocalAtTarget_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiCompactImmersionFpqcLocalAtTarget.lean, line 235. References: SGA 4 IV (8.5.5), “more general”.

Stacks 0424. Being a quasi-compact immersion is fpqc local on the base for morphisms of algebraic spaces over S: such a morphism is a quasi-compact immersion exactly when its base change to every member of some fpqc covering of its target is a quasi-compact immersion.

theorem immersion_inf_quasiCompact_isLocalAtTarget_fpqc :
    (immersionProperty B S hS ⊓ quasiCompactProperty B S hS).IsLocalAtTarget
      (Topology.precoverage.{u, v} .fpqc B S hS)

Tag 0425, a lemma

Tag 0425 in the Stacks Project.

AlgebraicGeometry.Space.integralMorphismProperty_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Fpqc/Integral.lean, line 162. References: SGA 4 IV (8.5.5), “more general”.

Stacks 0425. Integrality of morphisms of algebraic spaces over S is local on the base for the fpqc topology of Stacks 03YH.

An integral morphism is an affine universally closed one (Stacks 0415), affineness is fpqc local on the base (Stacks 041Z) and so is universal closedness (Stacks 041O), and locality on the base passes to an infimum of morphism properties.

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

Tag 0426, a lemma

Tag 0426 in the Stacks Project.

AlgebraicGeometry.Space.isFinite_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteFpqcLocalAtTarget.lean, line 97. References: SGA 4 IV (8.5.5), “more general”.

Stacks 0426. Finiteness of morphisms of algebraic spaces over S is local on the base for the fpqc topology of Stacks 03YH: a morphism is finite exactly when its base change to every member of some fpqc covering family of its target is finite.

A morphism is finite exactly when it is proper and locally quasi-finite (Stacks 0A4X), properness is fpqc local on the base by Stacks 0422 and local quasi-finiteness by Stacks 0427, so their conjunction is.

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

Tag 0427, a lemma

Tag 0427 in the Stacks Project.

AlgebraicGeometry.Space.isLocallyQuasiFinite_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteFpqcLocalAtTarget.lean, line 59. The attribute's comment: “locally quasi-finite case”.

Stacks 0427, the locally quasi-finite case. Local quasi-finiteness of a morphism of algebraic spaces over S is local on the base for the fpqc topology of Stacks 03YH.

instance isLocallyQuasiFinite_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) => IsLocallyQuasiFinite B S hS f.hom)
      (Topology.precoverage.{u, v} .fpqc B S hS)

AlgebraicGeometry.Space.isQuasiFinite_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/QuasiFiniteFpqcLocalAtTarget.lean, line 79. The attribute's comment: “quasi-finite case”. References: SGA 4 IV (8.5.5), “more general”.

Stacks 0427, the quasi-finite case. Quasi-finiteness of a morphism of algebraic spaces over S is local on the base for the fpqc topology of Stacks 03YH.

Quasi-finiteness is local quasi-finiteness together with quasi-compactness, and quasi-compactness is fpqc local on the base by Stacks 041L.

instance isQuasiFinite_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) => IsQuasiFinite B S hS f.hom)
      (Topology.precoverage.{u, v} .fpqc B S hS)

Tag 0428, a lemma

Tag 0428 in the Stacks Project.

AlgebraicGeometry.Space.syntomic_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SyntomicFpqcLocalAtTarget.lean, line 49.

Stacks 0428. Syntomicity of a morphism of algebraic spaces over S is local on the base for the fpqc topology of Stacks 03YH.

instance syntomic_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) => IsSyntomic B S hS f.hom)
      (Topology.precoverage.{u, v} .fpqc B S hS)

Tag 0429, a lemma

Tag 0429 in the Stacks Project.

AlgebraicGeometry.Space.smooth_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoveringComparison.lean, line 474. The attribute's comment: “the fppf precoverage”.

Stacks 0429 at the fppf precoverage: smoothness of morphisms of algebraic spaces over S is local at the target for the fppf topology. The fpqc form is AlgebraicGeometry.Space.smooth_isLocalAtTarget_fpqc, and the two are compared by AlgebraicGeometry.Space.fppfPrecoverage_le_fpqcPrecoverage. This is the form in which Stacks 03YK's relative properties ask for it.

instance smooth_isLocalAtTarget_fppf (B : BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    (smoothMorphismProperty B S hS).IsLocalAtTarget
      (Topology.fppf.precoverage.{u, v} B S hS)

AlgebraicGeometry.Space.smooth_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothFpqcLocalAtTarget.lean, line 791.

Smoothness of algebraic-space morphisms is fpqc local on the base.

instance smooth_isLocalAtTarget_fpqc (B : BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) :
    (smoothMorphismProperty B S hS).IsLocalAtTarget
      (Topology.precoverage.{u, v} .fpqc B S hS)

Tag 042A, a lemma

Tag 042A in the Stacks Project.

AlgebraicGeometry.Space.isUnramified_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedFpqcLocalAtTarget.lean, line 243.

Unramifiedness of a morphism of algebraic spaces over S is local on the target for the fpqc topology.

public instance isUnramified_isLocalAtTarget_fpqc
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) =>
        IsUnramified B S hS f.hom)
      (Topology.fpqc.precoverage.{u, v} B S hS)

AlgebraicGeometry.Space.isUnramified_iff_forall_pullbackSnd_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/UnramifiedFpqcLocalAtTarget.lean, line 285. The attribute's comment: “Definition 03YH unfolded: f unramified iff every Yᵢ ×_Y X → Yᵢ is”.

Let {gᵢ : Yᵢ ⟶ Y} be an fpqc covering of algebraic spaces over S, indexed by a type I in any universe, and f : X ⟶ Y a morphism of algebraic spaces over S. Then f is unramified if and only if every base change pullback.snd f (g i) : Yᵢ ×_Y X ⟶ Yᵢ of f is unramified.

theorem isUnramified_iff_forall_pullbackSnd_of_isFpqcCovering
    {B : BigFppfSite.{u}} {S : Scheme.{u}} {hS : B.Contains S}
    {I : Type v} {X Y : AlgebraicSpaces B S hS} {Yi : I → AlgebraicSpaces B S hS}
    (g : ∀ i, Yi i ⟶ Y) (hg : IsFpqcCovering B S hS (fun i => (g i).hom)) (f : X ⟶ Y) :
    IsUnramified B S hS f.hom ↔ ∀ i, IsUnramified B S hS (pullback.snd f (g i)).hom

Tag 042B, a lemma

Tag 042B in the Stacks Project.

AlgebraicGeometry.Space.isEtale_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleFpqcLocalAtTarget.lean, line 54.

Stacks 042B. Étaleness of a morphism of algebraic spaces over S is local on the base for the fpqc topology of Stacks 03YH.

instance isEtale_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) => IsEtale B S hS f.hom)
      (Topology.precoverage.{u, v} .fpqc B S hS)

Tag 042C, a lemma

Tag 042C in the Stacks Project.

AlgebraicGeometry.Space.isFiniteLocallyFree_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeFpqcLocalAtTarget.lean, line 116.

Stacks 042C. Being finite locally free is, for morphisms of algebraic spaces over S, local on the base for the fpqc topology of Stacks 03YH: such a morphism is finite locally free exactly when its base change to every member of some fpqc covering family of its target is finite locally free.

A morphism is finite locally free exactly when it is finite, flat and locally of finite presentation (Stacks 0416), finiteness is fpqc local on the base by Stacks 0426, flatness by Stacks 041W and local finite presentation by Stacks 041T, so their conjunction is.

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

Tag 042D, a lemma

Tag 042D in the Stacks Project.

AlgebraicGeometry.Space.mono_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/MonomorphismFpqcLocalAtTarget.lean, line 133. References: SGA 3 IV (4.5.8), “special case”; SGA 4 IV (8.5.5), “more general”.

Stacks 042D. Monomorphy of morphisms of algebraic spaces over S is local on the base for the fpqc topology: a morphism is a monomorphism exactly when its base change to every member of some fpqc covering of its target is a monomorphism.

Stacks 042Q reduces monomorphy to monomorphy of the base changes along the morphisms out of the affine objects of the site, over such an object the covering is refined by a finite family of affine objects factoring through its members, and monomorphy descends along the fpqc covering sieve that family generates because the fibre product is an fpqc sheaf by Stacks 0APL.

instance mono_isLocalAtTarget_fpqc :
    (MorphismProperty.monomorphisms (AlgebraicSpaces B S hS)).IsLocalAtTarget
      (Topology.precoverage.{u, v} .fpqc B S hS)

Sources

Section74.12 Descending properties of morphisms in the fppf topology #

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

Tag 042U, a lemma

Tag 042U in the Stacks Project.

AlgebraicGeometry.Space.isImmersion_isLocalAtTarget_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ImmersionFppfLocalAtTarget.lean, line 120.

Being an immersion is fppf local on the base for morphisms of algebraic spaces over S: such a morphism is an immersion exactly when its base change to every member of some fppf covering of its target is an immersion.

theorem isImmersion_isLocalAtTarget_fppf
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    (immersionProperty B S hS).IsLocalAtTarget
      (Topology.precoverage.{u, v} .fppf B S hS)

Tag 042F, a lemma

Tag 042F in the Stacks Project.

AlgebraicGeometry.Space.locallySeparated_isLocalAtTarget_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/LocallySeparatedFppfLocalAtTarget.lean, line 116.

Stacks 042F. Local separatedness of morphisms of algebraic spaces over S is local on the base for the fppf topology: a morphism is locally separated exactly when its base change to every member of some fppf covering of its target is locally separated.

Local separatedness of f : X ⟶ Y is the relative diagonal Δ_f : X ⟶ X ×_Y X being an immersion. Pulling a covering {Y i ⟶ Y} back along X ×_Y X ⟶ Y gives a covering of X ×_Y X whose base changes of Δ_f are the relative diagonals of the base changes of f, so Stacks 042U for immersions applies.

theorem locallySeparated_isLocalAtTarget_fppf :
    (locallySeparatedMorphismProperty B S hS).IsLocalAtTarget
      (Topology.precoverage.{u, v} .fppf B S hS)

Sources

LeanAlgebraicGeometry.Space.isImmersion_isLocalAtTarget_fppf · AlgebraicGeometry.Space.locallySeparated_isLocalAtTarget_fppf

Section74.13 Application of descent of properties of morphisms #

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

Tag 0D3C, a lemma

Tag 0D3C in the Stacks Project.

AlgebraicGeometry.Space.isRelativelyAmple_iff_forall_isRelativelyAmple_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeAmpleFpqcLocal.lean, line 57.

Stacks 0D3C. Let f : X ⟶ Y be a morphism of algebraic spaces over S, 𝓛 an invertible 𝒪_X-module and {gᵢ : Yᵢ ⟶ Y} an fpqc covering, with base changes fᵢ : Xᵢ ⟶ Yᵢ of f and pullbacks 𝓛ᵢ of 𝓛 to Xᵢ. Then 𝓛 is ample on X/Y if and only if 𝓛ᵢ is ample on Xᵢ/Yᵢ for every i.

theorem isRelativelyAmple_iff_forall_isRelativelyAmple_of_isFpqcCovering
    {X Y : AlgebraicSpaces B S hS} {f : X ⟶ Y} {I : Type v}
    {Yᵢ Xᵢ : I → AlgebraicSpaces B S hS} {gᵢ : ∀ i, Yᵢ i ⟶ Y} {fᵢ : ∀ i, Xᵢ i ⟶ Yᵢ i}
    {pᵢ : ∀ i, Xᵢ i ⟶ X} (hsq : ∀ i, IsPullback (pᵢ i) (fᵢ i) f (gᵢ i))
    (L : Modules.{u, u} B S hS X.1 X.2)
    (hL : Stacks.SheafOfModules.IsInvertible (structurePresheaf B S hS X.1)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS X.1 X.2).O)).property L)
    (hfpqc : IsFpqcCovering B S hS fun i => (gᵢ i).hom) :
    IsRelativelyAmple B S hS f L ↔
      ∀ i, IsRelativelyAmple B S hS (fᵢ i) ((modulePullback B S hS (pᵢ i)).obj L)

AlgebraicGeometry.Space.forall_isRelativelyAmple_baseChange_of_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeAmpleFpqcLocalAtTarget.lean, line 145. The attribute's comment: “(1) implies (2), unconditionally; the fpqc hypothesis on the family is not needed for this direction”.

Stacks 0D3C, (1) implies (2). If L is ample on X/Y then the pullback of L to the base change of f along any member of the family is ample on that base change: this is the base-change stability of Stacks 0D33, and nothing is asked of the family.

theorem forall_isRelativelyAmple_baseChange_of_isRelativelyAmple
    (hL : IsRelativelyAmple B S hS f L) (i : I) :
    IsRelativelyAmple B S hS (fᵢ i) ((modulePullback B S hS (pᵢ i)).obj L)

AlgebraicGeometry.Space.exists_affineFpqcRefinement_isAmpleOnBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeAmpleFpqcLocalAtTarget.lean, line 162. The attribute's comment: “the unconditional half of (2) implies (1): the clause of Tag 0D36 on a finite affine fpqc covering of each affine scheme over Y. Descending it to the scheme itself is carried by isRelativelyAmple_iff_forall_isRelativelyAmple_baseChange”.

The reduction of Stacks 0D3C, (2) implies (1), to the scheme level. Assume the pullback of L to each base change Xᵢ is ample on Xᵢ/Yᵢ. Then every affine scheme T over Y admits a finite family of affine schemes over T which covers T in the fpqc topology of schemes and on each of whose members the base-change clause of Stacks 0D36 for (f, L) holds.

The fpqc condition of Stacks 03MQ supplies the family together with a factorisation of each member through some Yᵢ, and AlgebraicGeometry.Space.isAmpleOnBaseChange_of_isPullback turns the clause for (fᵢ, Lᵢ) at that factorisation into the clause for (f, L).

theorem exists_affineFpqcRefinement_isAmpleOnBaseChange
    (hfpqc : IsFpqcCovering B S hS fun i => (gᵢ i).hom)
    (h : ∀ i, IsRelativelyAmple B S hS (fᵢ i) ((modulePullback B S hS (pᵢ i)).obj L))
    (T : BigAffineFppf B S hS)
    (g : yoneda.obj ((BigAffineFppf.inclusion B S hS).obj T) ⟶ Y.1) :
    ∃ U : PreZeroHypercover.{u + 1} T, Finite U.I₀ ∧
      Presieve.map (BigAffineFppf.toScheme B S hS) U.presieve₀ ∈
        Scheme.fpqcPrecoverage ((BigAffineFppf.toScheme B S hS).obj T) ∧
      ∀ j : U.I₀, IsAmpleOnBaseChange B S hS f L
        ((BigAffineFppf.inclusion B S hS).obj (U.X j))
        (yoneda.map ((BigAffineFppf.inclusion B S hS).map (U.f j)) ≫ g)

AlgebraicGeometry.Space.isRelativelyAmple_iff_forall_isRelativelyAmple_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/RelativeAmpleFpqcLocalAtTarget.lean, line 192. The attribute's comment: “full equivalence, with the hypotheses of the source: L invertible and the family an fpqc covering”.

Stacks 0D3C. Let L be an invertible 𝒪_X-module, let {gᵢ : Yᵢ ⟶ Y} be an fpqc covering, let fᵢ : Xᵢ ⟶ Yᵢ be the base change of f : X ⟶ Y and Lᵢ the pullback of L. Then L is ample on X/Y if and only if Lᵢ is ample on Xᵢ/Yᵢ for every i.

The forward direction is base change. For the converse, f is quasi-compact and separated (Stacks 0D34, 041L, 0421), the clause of Stacks 0D36 may be tested at the affine schemes over Y, and at such a scheme it is AlgebraicGeometry.Space.exists_affineFpqcRefinement_isAmpleOnBaseChange followed by AlgebraicGeometry.Space.exists_isPullback_of_affineFpqcFamily and AlgebraicGeometry.Space.exists_isRelativelyAmple_of_fpqcFamily.

theorem isRelativelyAmple_iff_forall_isRelativelyAmple_baseChange
    (hL : Stacks.SheafOfModules.IsInvertible (structurePresheaf B S hS X.1)
      ((Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS X.1 X.2).O)).property L)
    (hfpqc : IsFpqcCovering B S hS fun i => (gᵢ i).hom) :
    IsRelativelyAmple B S hS f L ↔
      ∀ i, IsRelativelyAmple B S hS (fᵢ i) ((modulePullback B S hS (pᵢ i)).obj L)

Tag 0D3D, a lemma

Tag 0D3D in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_factors_iff_isRelativelyAmple_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Limits/ProperLimitOfFinitePresentationEmbedding.lean, line 236.

Let S be a scheme, f : X ⟶ Y a proper morphism of algebraic spaces over S and L an invertible 𝒪_X-module. There is an open subspace V ⊆ Y such that a morphism g : Y' ⟶ Y of algebraic spaces factors through V if and only if the pullback of L to X' = Y' ×_Y X is ample on X'/Y' (Stacks 0D31).

theorem exists_isOpenSubspace_factors_iff_isRelativelyAmple_of_isProper
    {X Y : AlgebraicSpaces B S hS} {f : X ⟶ Y} (hf : IsProper B S hS f.hom)
    {L : Modules.{u, u} B S hS X.1 X.2}
    (hL : Stacks.SheafOfModules.IsInvertible (structurePresheaf B S hS X.1)
      ((Stacks.SheafOfModules.Tensor.ringSheaf
        (smallEtaleRingedSite B S hS X.1 X.2).O)).property L) :
    ∃ V : Subfunctor Y.1, IsOpenSubspace B S hS V ∧
      ∀ ⦃X' Y' : AlgebraicSpaces B S hS⦄ (g : Y' ⟶ Y) (p : X' ⟶ X) (f' : X' ⟶ Y'),
        IsPullback p f' f g →
          ((∃ l : Y'.1 ⟶ V.toFunctor, l ≫ V.ι = g.hom) ↔
            IsRelativelyAmple B S hS f' ((modulePullback B S hS p).obj L))

Sources

LeanAlgebraicGeometry.Space.isRelativelyAmple_iff_forall_isRelativelyAmple_of_isFpqcCovering · AlgebraicGeometry.Space.forall_isRelativelyAmple_baseChange_of_isRelativelyAmple · AlgebraicGeometry.Space.exists_affineFpqcRefinement_isAmpleOnBaseChange · AlgebraicGeometry.Space.isRelativelyAmple_iff_forall_isRelativelyAmple_baseChange · AlgebraicGeometry.Space.exists_isOpenSubspace_factors_iff_isRelativelyAmple_of_isProper

Section74.14 Properties of morphisms local on the source #

Section 74.14 of the Stacks Project, Tag 06EN. 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 06EP, a definition

Tag 06EP in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.MorphismProperty.IsLocalAtSource registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Coverings.lean, line 420 (StacksFrontier). References: SGA 4 IV (8.5.4).

Tag 06EQ, a lemma

Tag 06EQ in the Stacks Project.

AlgebraicGeometry.Space.comp_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSource/Precomposition.lean, line 164. The attribute's comment: “fpqc”.

Stacks 06EQ, the fpqc case. A property fpqc local on the source is stable under precomposition with a flat morphism.

theorem comp_isFlat [P.IsLocalAtSource (Topology.precoverage.{u, v} .fpqc B S hS)]
    {X Y Z : AlgebraicSpaces B S hS} (a : X ⟶ Y) (f : Y ⟶ Z)
    (ha : IsFlat B S hS a.hom) (hf : P f) : P (a ≫ f)

AlgebraicGeometry.Space.comp_isFlat_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSource/Precomposition.lean, line 172. The attribute's comment: “fppf”.

Stacks 06EQ, the fppf case. A property fppf local on the source is stable under precomposition with a flat morphism which is locally of finite presentation.

theorem comp_isFlat_isLocallyOfFinitePresentation
    [P.IsLocalAtSource (Topology.precoverage.{u, v} .fppf B S hS)]
    {X Y Z : AlgebraicSpaces B S hS} (a : X ⟶ Y) (f : Y ⟶ Z)
    (hflat : IsFlat B S hS a.hom)
    (hlfp : IsLocallyOfFinitePresentation B S hS a.hom) (hf : P f) : P (a ≫ f)

AlgebraicGeometry.Space.comp_isSyntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSource/Precomposition.lean, line 182. The attribute's comment: “syntomic”.

Stacks 06EQ, the syntomic case. A property syntomic local on the source is stable under precomposition with a syntomic morphism.

theorem comp_isSyntomic [P.IsLocalAtSource (Topology.precoverage.{u, v} .syntomic B S hS)]
    {X Y Z : AlgebraicSpaces B S hS} (a : X ⟶ Y) (f : Y ⟶ Z)
    (ha : IsSyntomic B S hS a.hom) (hf : P f) : P (a ≫ f)

AlgebraicGeometry.Space.comp_isSmooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSource/Precomposition.lean, line 190. The attribute's comment: “smooth”.

Stacks 06EQ, the smooth case. A property smooth local on the source is stable under precomposition with a smooth morphism.

theorem comp_isSmooth [P.IsLocalAtSource (Topology.precoverage.{u, v} .smooth B S hS)]
    {X Y Z : AlgebraicSpaces B S hS} (a : X ⟶ Y) (f : Y ⟶ Z)
    (ha : IsSmooth B S hS a.hom) (hf : P f) : P (a ≫ f)

AlgebraicGeometry.Space.comp_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSource/Precomposition.lean, line 198. The attribute's comment: “étale”.

Stacks 06EQ, the étale case. A property étale local on the source is stable under precomposition with an étale morphism.

theorem comp_isEtale [P.IsLocalAtSource (Topology.precoverage.{u, v} .etale B S hS)]
    {X Y Z : AlgebraicSpaces B S hS} (a : X ⟶ Y) (f : Y ⟶ Z)
    (ha : IsEtale B S hS a.hom) (hf : P f) : P (a ≫ f)

Tag 06ER, a lemma

Tag 06ER in the Stacks Project.

AlgebraicGeometry.Space.Topology.isLocalAtSource_holdsOnEveryEtaleChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSource/PropertyLocalOnSource.lean, line 126.

Stacks 06ER. Let P be a property of morphisms of schemes over S which is étale local on the source and target, and let τ be one of the five topologies of Stacks 03YH. If P is local on the source for the counterpart of τ on schemes, then the associated property of morphisms of algebraic spaces over S of Stacks 03MJ is local on the source for τ.

theorem Topology.isLocalAtSource_holdsOnEveryEtaleChart (τ : Topology)
    (P : MorphismProperty Scheme.{u}) (hP : IsEtaleLocalOnSourceAndTarget P)
    (hlocal : P.IsLocalAtSource τ.schemePrecoverage) :
    MorphismProperty.IsLocalAtSource
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) =>
        HoldsOnEveryEtaleChart B S hS P f.hom)
      (Topology.precoverage.{u, v} τ B S hS)

Sources

LeanCategoryTheory.MorphismProperty.IsLocalAtSource · AlgebraicGeometry.Space.comp_isFlat · AlgebraicGeometry.Space.comp_isFlat_isLocallyOfFinitePresentation · AlgebraicGeometry.Space.comp_isSyntomic · AlgebraicGeometry.Space.comp_isSmooth · AlgebraicGeometry.Space.comp_isEtale · AlgebraicGeometry.Space.Topology.isLocalAtSource_holdsOnEveryEtaleChart

Section74.15 Properties of morphisms local in the fpqc topology on the source #

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

Tag 06ET, a lemma

Tag 06ET in the Stacks Project.

AlgebraicGeometry.Space.isFlat_isLocalAtSource_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FlatFpqcLocality.lean, line 62.

Stacks 06ET. Flatness of morphisms of algebraic spaces over S is local on the source for the fpqc topology.

instance isFlat_isLocalAtSource_fpqc
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    MorphismProperty.IsLocalAtSource
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) => IsFlat B S hS f.hom)
      (Topology.fpqc.precoverage.{u, v} B S hS)

Sources

LeanAlgebraicGeometry.Space.isFlat_isLocalAtSource_fpqc

Section74.16 Properties of morphisms local in the fppf topology on the source #

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

Tag 06EV, a lemma

Tag 06EV in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFinitePresentation_isLocalAtSource_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSource/Fppf.lean, line 63.

Stacks 06EV. Being locally of finite presentation, for a morphism of algebraic spaces over S, is local on the source for the fppf topology.

instance isLocallyOfFinitePresentation_isLocalAtSource_fppf :
    MorphismProperty.IsLocalAtSource
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) =>
        IsLocallyOfFinitePresentation B S hS f.hom)
      (Topology.fppf.precoverage.{u, v} B S hS)

Tag 06EW, a lemma

Tag 06EW in the Stacks Project.

AlgebraicGeometry.Space.isLocallyOfFiniteType_isLocalAtSource_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FppfSourceLocalityFiniteType.lean, line 58.

Stacks 06EW. Being locally of finite type, as a property of morphisms of algebraic spaces over S, is local on the source for the fppf topology.

instance isLocallyOfFiniteType_isLocalAtSource_fppf :
    MorphismProperty.IsLocalAtSource
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) =>
        IsLocallyOfFiniteType B S hS f.hom)
      (Topology.precoverage.{u, v} .fppf B S hS)

Tag 06EX, a lemma

Tag 06EX in the Stacks Project.

AlgebraicGeometry.Space.isOpenMorphism_isLocalAtSource_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OpenSourceLocality.lean, line 113.

Stacks 06EX. Being open, for a morphism of algebraic spaces over S, is local on the source for the fppf topology.

instance isOpenMorphism_isLocalAtSource_fppf :
    MorphismProperty.IsLocalAtSource
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) ↦ IsOpenMorphism B S hS f.hom)
      (Topology.fppf.precoverage.{u, v} B S hS)

Tag 06EY, a lemma

Tag 06EY in the Stacks Project.

AlgebraicGeometry.Space.universallyOpen_isLocalAtSource_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/OpenSourceLocality.lean, line 135.

Stacks 06EY. Being universally open, for a morphism of algebraic spaces over S, is local on the source for the fppf topology.

instance universallyOpen_isLocalAtSource_fppf :
    MorphismProperty.IsLocalAtSource
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) ↦ UniversallyOpen B S hS f.hom)
      (Topology.fppf.precoverage.{u, v} B S hS)

Sources

LeanAlgebraicGeometry.Space.isLocallyOfFinitePresentation_isLocalAtSource_fppf · AlgebraicGeometry.Space.isLocallyOfFiniteType_isLocalAtSource_fppf · AlgebraicGeometry.Space.isOpenMorphism_isLocalAtSource_fppf · AlgebraicGeometry.Space.universallyOpen_isLocalAtSource_fppf

Section74.17 Properties of morphisms local in the syntomic topology on the source #

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

Tag 06F0, a lemma

Tag 06F0 in the Stacks Project.

AlgebraicGeometry.Space.syntomic_isLocalAtSource_syntomic, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SyntomicSourceLocalityTransfer.lean, line 351.

Stacks 06F0. Syntomicity of a morphism of algebraic spaces over S is local on the source for the syntomic topology of Stacks 03YH.

Syntomicity of morphisms of schemes is étale local on the source and target ([Stacks Project, Tag 04R3]) and local on the source for the syntomic topology of schemes ([Stacks Project, Tag 036S]), so this is the instance of AlgebraicGeometry.Space.isLocalAtSource_syntomic_of_schemes at that property.

instance syntomic_isLocalAtSource_syntomic :
    MorphismProperty.IsLocalAtSource
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) => IsSyntomic B S hS f.hom)
      (Topology.precoverage.{u, v} .syntomic B S hS)

Sources

LeanAlgebraicGeometry.Space.syntomic_isLocalAtSource_syntomic

Section74.18 Properties of morphisms local in the smooth topology on the source #

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

Tag 06F2, a lemma

Tag 06F2 in the Stacks Project.

AlgebraicGeometry.Space.isSmooth_isLocalAtSource_smooth, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothSourceLocalityTransfer.lean, line 432.

Stacks 06F2. Smoothness of morphisms of algebraic spaces over S is local on the source for the smooth topology.

One application of the smooth case of Stacks 06ER to smoothness of morphisms of schemes, which is étale local on the source and target (Stacks 04R3, smooth case) and smooth local on the source (Stacks 036U). Registered as an instance, which is the form the criterion of Stacks 06FB takes it in.

instance isSmooth_isLocalAtSource_smooth :
    MorphismProperty.IsLocalAtSource
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) => IsSmooth B S hS f.hom)
      (Topology.precoverage.{u, v} .smooth B S hS)

Sources

LeanAlgebraicGeometry.Space.isSmooth_isLocalAtSource_smooth

Section74.19 Properties of morphisms local in the étale topology on the source #

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

Tag 06F4, a lemma

Tag 06F4 in the Stacks Project.

AlgebraicGeometry.Space.isEtale_isLocalAtSource_etale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSource/Etale.lean, line 73.

Stacks 06F4. Étaleness of a morphism of algebraic spaces over S is local on the source for the étale topology.

instance isEtale_isLocalAtSource_etale :
    MorphismProperty.IsLocalAtSource
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) => IsEtale B S hS f.hom)
      (Topology.etale.precoverage.{u, v} B S hS)

Tag 06F5, a lemma

Tag 06F5 in the Stacks Project.

AlgebraicGeometry.Space.isLocallyQuasiFinite_isLocalAtSource_etale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSource/Etale.lean, line 92.

Stacks 06F5. Local quasi-finiteness of a morphism of algebraic spaces over S is local on the source for the étale topology.

instance isLocallyQuasiFinite_isLocalAtSource_etale :
    MorphismProperty.IsLocalAtSource
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) => IsLocallyQuasiFinite B S hS f.hom)
      (Topology.etale.precoverage.{u, v} B S hS)

Tag 06F6, a lemma

Tag 06F6 in the Stacks Project.

AlgebraicGeometry.Space.unramified_isLocalAtSource_etale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleSourceLocalityTransfer.lean, line 153.

Stacks 06F6. Unramifiedness of a morphism of algebraic spaces over S is local on the source for the étale topology of Stacks 03YH.

Unramifiedness of morphisms of schemes is étale local on the source and target ([Stacks Project, Tag 04R3]) and local on the source for the étale topology of schemes ([Stacks Project, Tag 03YV]), so this is the instance of AlgebraicGeometry.Space.isLocalAtSource_etale_of_schemes at that property.

instance unramified_isLocalAtSource_etale :
    MorphismProperty.IsLocalAtSource
      (fun ⦃F G : AlgebraicSpaces B S hS⦄ (f : F ⟶ G) => IsUnramified B S hS f.hom)
      (Topology.precoverage.{u, v} .etale B S hS)

Sources

LeanAlgebraicGeometry.Space.isEtale_isLocalAtSource_etale · AlgebraicGeometry.Space.isLocallyQuasiFinite_isLocalAtSource_etale · AlgebraicGeometry.Space.unramified_isLocalAtSource_etale

Section74.20 Properties of morphisms smooth local on source-and-target #

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

Tag 06F8, a definition

Tag 06F8 in the Stacks Project.

AlgebraicGeometry.Space.IsSmoothLocalOnSourceAndTarget, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothLocalOnSourceAndTarget.lean, line 55.

Stacks 06F8. A property of morphisms of algebraic spaces over S is smooth local on the source-and-target when it is stable under smooth precomposition and smooth base change, and can be checked in smooth neighbourhoods of every point of the source.

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

Tag 06F9, a lemma

Tag 06F9 in the Stacks Project.

AlgebraicGeometry.Space.isSmoothLocalAtSource, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothLocalProperties.lean, line 163. The attribute's comment: “smooth_local_source”.

Stacks 06F9, smooth locality on the source. A property of morphisms of algebraic spaces over S which is smooth local on the source-and-target is local at the source for the smooth precoverage.

theorem isSmoothLocalAtSource
    (P : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    (hP : IsSmoothLocalOnSourceAndTarget B S hS P) :
    (P.inverseImage (ObjectProperty.ι
      (fun F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u =>
        IsAlgebraicSpace B S hS F))).IsLocalAtSource
      (Topology.precoverage.{u, v} .smooth B S hS)

AlgebraicGeometry.Space.isSmoothLocalAtTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothLocalProperties.lean, line 212. The attribute's comment: “smooth_local_target”.

Stacks 06F9, smooth locality on the target. A property of morphisms of algebraic spaces over S which is smooth local on the source-and-target is local at the target for the smooth precoverage.

theorem isSmoothLocalAtTarget
    (P : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    (hP : IsSmoothLocalOnSourceAndTarget B S hS P) :
    (P.inverseImage (ObjectProperty.ι
      (fun F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u =>
        IsAlgebraicSpace B S hS F))).IsLocalAtTarget
      (Topology.precoverage.{u, v} .smooth B S hS)

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

Stacks 06F9, smooth postcomposition. A property of morphisms of algebraic spaces over S which is smooth local on the source-and-target is preserved by postcomposition with a smooth morphism.

theorem comp_smooth
    (P : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    (hP : IsSmoothLocalOnSourceAndTarget B S hS P)
    {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (hZ : IsAlgebraicSpace B S hS Z)
    (f : X ⟶ Y) (g : Y ⟶ Z)
    (hf : P f) (hg : IsSmooth B S hS g) : P (f ≫ g)

Tag 06FA, a lemma

Tag 06FA in the Stacks Project.

AlgebraicGeometry.Space.smoothLocalOnSourceAndTarget_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothLocalProperties.lean, line 337.

Stacks 06FA. Seven equivalent criteria for a morphism of algebraic spaces over S to have a property which is smooth local on the source-and-target: the property itself; a smooth neighbourhood of every point of the source on which it holds; one smooth diagram surjective on the source; every smooth comparison into a fibre product over a smooth base change; a smooth covering of the target over which the base changes have it; a smooth covering of the source whose composites have it; and a smooth covering of the target refined by smooth coverings of the corresponding fibre products.

theorem smoothLocalOnSourceAndTarget_tfae
    (P : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    (hP : IsSmoothLocalOnSourceAndTarget B S hS P)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y)
    (f : X ⟶ Y) :
    List.TFAE [
      P f,
      (∀ x : points B S hS X,
        ∃ (U V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
          (_hU : IsAlgebraicSpace B S hS U)
          (_hV : IsAlgebraicSpace B S hS V)
          (a : U ⟶ X) (b : V ⟶ Y) (h : U ⟶ V)
          (u : points B S hS U),
          IsSmooth B S hS a ∧
            IsSmooth B S hS b ∧
            pointsMap B S hS U a u = x ∧
            h ≫ b = a ≫ f ∧ P h),
      (∃ (U V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
          (_hU : IsAlgebraicSpace B S hS U)
          (_hV : IsAlgebraicSpace B S hS V)
          (a : U ⟶ X) (b : V ⟶ Y) (h : U ⟶ V),
          IsSmooth B S hS a ∧
            IsSurjective B S hS a ∧
            IsSmooth B S hS b ∧
            h ≫ b = a ≫ f ∧ P h),
      (∀ (U V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
          (_hU : IsAlgebraicSpace B S hS U)
          (_hV : IsAlgebraicSpace B S hS V)
          (b : V ⟶ Y) (k : U ⟶ pullback f b),
          IsSmooth B S hS b →
          IsSmooth B S hS k →
          P (k ≫ pullback.snd f b)),
      (∃ (I : Type v)
          (V : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
          (b : ∀ i, V i ⟶ Y),
          IsSmoothCovering B S hS V b ∧
          ∀ i, P (pullback.snd f (b i))),
      (∃ (I : Type v)
          (U : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
          (a : ∀ i, U i ⟶ X),
          IsSmoothCovering B S hS U a ∧
          ∀ i, P (a i ≫ f)),
      (∃ (I : Type v)
          (V : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
          (b : ∀ i, V i ⟶ Y)
          (J : I → Type w)
          (U : ∀ i, J i → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
          (a : ∀ i j, U i j ⟶ pullback f (b i)),
          IsSmoothCovering B S hS V b ∧
          (∀ i, IsSmoothCovering B S hS (U i) (a i)) ∧
          (∀ i j, P (a i j ≫ pullback.snd f (b i))))
    ]

Tag 06FB, a lemma

Tag 06FB in the Stacks Project.

AlgebraicGeometry.Space.isSmoothLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSourceAndTarget/SmoothCriterion.lean, line 75.

Stacks 06FB. A property of morphisms of algebraic spaces over S which is local at the source and at the target for the smooth topology, and is preserved by postcomposition with a smooth morphism, is smooth local on the source-and-target.

theorem isSmoothLocalOnSourceAndTarget
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty ((BigFppfOver B S hS)ᵒᵖ ⥤ Type u))
    [hSource : (P.inverseImage (ObjectProperty.ι
      (fun F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u =>
        IsAlgebraicSpace B S hS F))).IsLocalAtSource
      (Topology.precoverage.{u, u + 1} .smooth B S hS)]
    [hTarget : (P.inverseImage (ObjectProperty.ι
      (fun F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u =>
        IsAlgebraicSpace B S hS F))).IsLocalAtTarget
      (Topology.precoverage.{u, u + 1} .smooth B S hS)]
    (hcomp : ∀ {X Y Z : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
      (_hX : IsAlgebraicSpace B S hS X)
      (_hY : IsAlgebraicSpace B S hS Y)
      (_hZ : IsAlgebraicSpace B S hS Z)
      (f : X ⟶ Y) (g : Y ⟶ Z),
      P f → IsSmooth B S hS g → P (f ≫ g)) :
    IsSmoothLocalOnSourceAndTarget B S hS P

Tag 06FC, a remark

Tag 06FC in the Stacks Project.

AlgebraicGeometry.Space.isSyntomic_isSmoothLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSourceAndTarget/Syntomic.lean, line 66. The attribute's comment: “syntomic”.

Stacks 06FC, the syntomic case. Syntomicity of morphisms of algebraic spaces over S is smooth local on the source-and-target.

The source locality hypothesis of Stacks 06FB comes from the syntomic one, Stacks 06F0, along AlgebraicGeometry.Space.Topology.precoverage_smooth_le_syntomic; the target locality one comes from the fpqc one, Stacks 0428, along AlgebraicGeometry.Space.Topology.precoverage_smooth_le_fpqc; and the postcomposition hypothesis is composition of syntomic morphisms (Stacks 03Z8) applied to the fact that a smooth morphism is syntomic.

theorem isSyntomic_isSmoothLocalOnSourceAndTarget :
    IsSmoothLocalOnSourceAndTarget B S hS (fun _ _ f => IsSyntomic B S hS f)

AlgebraicGeometry.Space.universallyOpen_isSmoothLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSourceAndTarget/UniversallyOpen.lean, line 77. The attribute's comment: “universally open”.

Stacks 06FC, the universally-open case. Being universally open is, for morphisms of algebraic spaces over S, smooth local on the source-and-target.

The source locality hypothesis of Stacks 06FB comes from the fppf one, Stacks 06EY, along AlgebraicGeometry.Space.Topology.precoverage_smooth_le_fppf; the target locality one comes from the fpqc one, Stacks 041P, along AlgebraicGeometry.Space.Topology.precoverage_smooth_le_fpqc; and the postcomposition hypothesis is composition of universally open morphisms (Stacks 03Z4) applied to AlgebraicGeometry.Space.universallyOpen_of_isSmooth.

theorem universallyOpen_isSmoothLocalOnSourceAndTarget :
    IsSmoothLocalOnSourceAndTarget B S hS
      (fun _ _ f => UniversallyOpen B S hS f)

AlgebraicGeometry.Space.isSmoothLocalOnSourceAndTarget_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothLocalityCriterion.lean, line 187. The attribute's comment: “flat”.

Stacks 06FC, the flat case. Flatness of morphisms of algebraic spaces over S is smooth local on the source-and-target.

The two locality hypotheses of Stacks 06FB come from the fpqc ones (Stacks 06ET and 041W) along AlgebraicGeometry.Space.smooth_precoverage_le_fpqc, and the postcomposition hypothesis is composition of flat morphisms (Stacks 03MN) applied to the flatness of a smooth morphism (Stacks 04TA).

theorem isSmoothLocalOnSourceAndTarget_flat :
    IsSmoothLocalOnSourceAndTarget B S hS (fun _ _ f => IsFlat B S hS f)

AlgebraicGeometry.Space.isSmoothLocalOnSourceAndTarget_locallyOfFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothLocalityFiniteness.lean, line 150. The attribute's comment: “locally_of_finite_type”.

Stacks 06FC, the locally-of-finite-type case. Being locally of finite type for morphisms of algebraic spaces over S is smooth local on the source-and-target.

The source locality hypothesis of Stacks 06FB is AlgebraicGeometry.Space.isLocallyOfFiniteType_isLocalAtSource_smooth; the target locality one comes from the fpqc statement of Stacks 041S along AlgebraicGeometry.Space.smooth_precoverage_le_fpqc, and the postcomposition hypothesis is composition of morphisms locally of finite type (Stacks 03XG) applied to the fact that a smooth morphism is locally of finite type (Stacks 06MH).

theorem isSmoothLocalOnSourceAndTarget_locallyOfFiniteType :
    IsSmoothLocalOnSourceAndTarget B S hS
      (fun _ _ f => IsLocallyOfFiniteType B S hS f)

AlgebraicGeometry.Space.isSmoothLocalOnSourceAndTarget_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothLocalityFiniteness.lean, line 178. The attribute's comment: “locally_of_finite_presentation”.

Stacks 06FC, the locally-of-finite-presentation case. Being locally of finite presentation for morphisms of algebraic spaces over S is smooth local on the source-and-target.

The source locality hypothesis of Stacks 06FB is AlgebraicGeometry.Space.isLocallyOfFinitePresentation_isLocalAtSource_smooth; the target locality one comes from the fpqc statement of Stacks 041T along AlgebraicGeometry.Space.smooth_precoverage_le_fpqc, and the postcomposition hypothesis is composition of morphisms locally of finite presentation (Stacks 03XQ) applied to the fact that a smooth morphism is locally of finite presentation (Stacks 04AJ).

theorem isSmoothLocalOnSourceAndTarget_locallyOfFinitePresentation :
    IsSmoothLocalOnSourceAndTarget B S hS
      (fun _ _ f => IsLocallyOfFinitePresentation B S hS f)

AlgebraicGeometry.Space.isSmoothLocalOnSourceAndTarget_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmoothSourceLocalityTransfer.lean, line 446. The attribute's comment: “smooth”.

Stacks 06FC, the smooth case. Smoothness of morphisms of algebraic spaces over S is smooth local on the source-and-target.

The source locality hypothesis of Stacks 06FB is Stacks 06F2; the target locality one comes from the fpqc one (Stacks 0429) along AlgebraicGeometry.Space.smooth_precoverage_le_fpqc, and the postcomposition hypothesis is composition of smooth morphisms (Stacks 03ZD).

theorem isSmoothLocalOnSourceAndTarget_smooth :
    IsSmoothLocalOnSourceAndTarget B S hS (fun _ _ f => IsSmooth B S hS f)

Sources

LeanAlgebraicGeometry.Space.IsSmoothLocalOnSourceAndTarget · AlgebraicGeometry.Space.isSmoothLocalAtSource · AlgebraicGeometry.Space.isSmoothLocalAtTarget · AlgebraicGeometry.Space.comp_smooth · AlgebraicGeometry.Space.smoothLocalOnSourceAndTarget_tfae · AlgebraicGeometry.Space.isSmoothLocalOnSourceAndTarget · AlgebraicGeometry.Space.isSyntomic_isSmoothLocalOnSourceAndTarget · AlgebraicGeometry.Space.universallyOpen_isSmoothLocalOnSourceAndTarget

Section74.21 Properties of morphisms étale-smooth local on source-and-target #

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

Tag 0CFZ, a definition

Tag 0CFZ in the Stacks Project.

AlgebraicGeometry.Space.IsEtaleSmoothLocalOnSourceAndTarget, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleSmoothLocalOnSourceAndTarget.lean, line 59.

Stacks 0CFZ. A property of morphisms of algebraic spaces over S is étale-smooth local on the source-and-target when it is stable under étale precomposition and under smooth base change, and holds exactly when it holds on an étale neighbourhood over a smooth target neighbourhood of every point of the source.

structure IsEtaleSmoothLocalOnSourceAndTarget
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty (AlgebraicSpaces B S hS)) : Prop

Tag 0CG0, a lemma

Tag 0CG0 in the Stacks Project.

AlgebraicGeometry.Space.postcomp_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSourceAndTarget/EtaleSmoothProperties.lean, line 111. The attribute's comment: “etale_postcomposition”.

Stacks 0CG0, étale postcomposition. A property of morphisms of algebraic spaces over S which is étale-smooth local on the source-and-target is preserved by postcomposition with an étale morphism.

theorem postcomp_of_etale
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    (hP : IsEtaleSmoothLocalOnSourceAndTarget B S hS P)
    {X Y Z : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : P f) (g : Y ⟶ Z)
    (hg : IsEtale B S hS g.hom) : P (f ≫ g)

AlgebraicGeometry.Space.of_comp_etale, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSourceAndTarget/EtaleSmoothProperties.lean, line 142. The attribute's comment: “etale_postcomposition_permanence”.

Stacks 0CG0, cancelling an étale postcomposition. If a property of morphisms of algebraic spaces over S is étale-smooth local on the source-and-target and holds for f ≫ g with g étale, then it holds for f.

lemma of_comp_etale
    {P : MorphismProperty (AlgebraicSpaces B S hS)}
    (hP : IsEtaleSmoothLocalOnSourceAndTarget B S hS P)
    {X Y Z : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (g : Y ⟶ Z)
    (hg : IsEtale B S hS g.hom)
    (hfg : P (f ≫ g)) : P f

AlgebraicGeometry.Space.isLocalAtSource_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSourceAndTarget/EtaleSmoothProperties.lean, line 159. The attribute's comment: “etale_local_source”.

Stacks 0CG0, étale locality on the source. A property of morphisms of algebraic spaces over S which is étale-smooth local on the source-and-target is local at the source for the étale topology.

theorem isLocalAtSource_etale
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    (hP : IsEtaleSmoothLocalOnSourceAndTarget B S hS P) :
    P.IsLocalAtSource (Topology.precoverage.{u, v} .etale B S hS)

AlgebraicGeometry.Space.isLocalAtTarget_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSourceAndTarget/EtaleSmoothProperties.lean, line 207. The attribute's comment: “smooth_local_target”.

Stacks 0CG0, smooth locality on the target. A property of morphisms of algebraic spaces over S which is étale-smooth local on the source-and-target is local at the target for the smooth topology.

theorem isLocalAtTarget_smooth
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    (hP : IsEtaleSmoothLocalOnSourceAndTarget B S hS P) :
    P.IsLocalAtTarget (Topology.precoverage.{u, v} .smooth B S hS)

Tag 0CG1, a lemma

Tag 0CG1 in the Stacks Project.

AlgebraicGeometry.Space.etaleSmoothLocalOnSourceAndTarget_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSourceAndTarget/EtaleSmoothTfae.lean, line 114.

Stacks 0CG1. Seven equivalent criteria for a morphism f : X ⟶ Y of algebraic spaces over S to have a property which is étale-smooth local on the source-and-target: the property itself; an étale neighbourhood over a smooth target neighbourhood on which it holds above every point of the source; one such neighbourhood surjective onto the source; every such neighbourhood; a smooth covering of the target whose base changes have it; an étale covering of the source whose composites have it; and a smooth covering of the target together with étale coverings of the corresponding fibre products.

theorem etaleSmoothLocalOnSourceAndTarget_tfae
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    (hP : IsEtaleSmoothLocalOnSourceAndTarget B S hS P)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) :
    List.TFAE [
      P f,
      (∀ x : points B S hS X.1,
        ∃ (V U : AlgebraicSpaces B S hS)
          (b : V ⟶ Y)
          (e : U ⟶ AlgebraicSpaces.fiberProduct B S hS f b)
          (v : points B S hS U.1),
          IsSmooth B S hS b.hom ∧
          IsEtale B S hS e.hom ∧
          pointsMap B S hS U.1
            (e ≫ (ObjectProperty.homMk (pullback.fst f.hom b.hom) :
              AlgebraicSpaces.fiberProduct B S hS f b ⟶ X)).hom v = x ∧
          P (e ≫ (ObjectProperty.homMk (pullback.snd f.hom b.hom) :
            AlgebraicSpaces.fiberProduct B S hS f b ⟶ V))),
      (∃ (V U : AlgebraicSpaces B S hS)
        (b : V ⟶ Y)
        (e : U ⟶ AlgebraicSpaces.fiberProduct B S hS f b),
        IsSmooth B S hS b.hom ∧
        IsEtale B S hS e.hom ∧
        IsSurjective B S hS
          (e ≫ (ObjectProperty.homMk (pullback.fst f.hom b.hom) :
            AlgebraicSpaces.fiberProduct B S hS f b ⟶ X)).hom ∧
        P (e ≫ (ObjectProperty.homMk (pullback.snd f.hom b.hom) :
          AlgebraicSpaces.fiberProduct B S hS f b ⟶ V))),
      (∀ (V U : AlgebraicSpaces B S hS)
        (b : V ⟶ Y)
        (e : U ⟶ AlgebraicSpaces.fiberProduct B S hS f b),
        IsSmooth B S hS b.hom →
        IsEtale B S hS e.hom →
        P (e ≫ (ObjectProperty.homMk (pullback.snd f.hom b.hom) :
          AlgebraicSpaces.fiberProduct B S hS f b ⟶ V))),
      (∃ (I : Type (u + 1))
        (V : I → AlgebraicSpaces B S hS)
        (b : ∀ i, V i ⟶ Y),
        IsSmoothCovering B S hS (fun i => (V i).1) (fun i => (b i).hom) ∧
        ∀ i, P (ObjectProperty.homMk (pullback.snd f.hom (b i).hom) :
          AlgebraicSpaces.fiberProduct B S hS f (b i) ⟶ V i)),
      (∃ (I : Type (u + 1))
        (U : I → AlgebraicSpaces B S hS)
        (a : ∀ i, U i ⟶ X),
        IsEtaleCovering B S hS (fun i => (U i).1) (fun i => (a i).hom) ∧
        ∀ i, P ((a i) ≫ f)),
      (∃ (I : Type (u + 1))
        (V : I → AlgebraicSpaces B S hS)
        (b : ∀ i, V i ⟶ Y)
        (J : I → Type (u + 1))
        (U : ∀ i, J i → AlgebraicSpaces B S hS)
        (e : ∀ i j, U i j ⟶ AlgebraicSpaces.fiberProduct B S hS f (b i)),
        IsSmoothCovering B S hS (fun i => (V i).1) (fun i => (b i).hom) ∧
        ∀ i, IsEtaleCovering B S hS (fun j => (U i j).1) (fun j => (e i j).hom) ∧
          ∀ j, P (e i j ≫
            (ObjectProperty.homMk (pullback.snd f.hom (b i).hom) :
              AlgebraicSpaces.fiberProduct B S hS f (b i) ⟶ V i)))]

Tag 0CG2, a lemma

Tag 0CG2 in the Stacks Project.

AlgebraicGeometry.Space.isEtaleSmoothLocalOnSourceAndTarget_of_local, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSourceAndTarget/EtaleSmoothFromLocality/SchemeSquareDescent.lean, line 307.

Stacks 0CG2. A property of morphisms of algebraic spaces over S which is étale local on the source, smooth local on the target and stable under postcomposition with open immersions is étale-smooth local on the source-and-target.

theorem isEtaleSmoothLocalOnSourceAndTarget_of_local
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (P : MorphismProperty (AlgebraicSpaces B S hS))
    [P.IsLocalAtSource (Space.Topology.precoverage.{u, u + 1} .etale B S hS)]
    [P.IsLocalAtTarget (Space.Topology.precoverage.{u, u + 1} .smooth B S hS)]
    [P.RespectsRight (fun ⦃X Y : AlgebraicSpaces B S hS⦄
      (f : X ⟶ Y) => Space.IsOpenImmersion B S hS f.hom)] :
    Space.IsEtaleSmoothLocalOnSourceAndTarget B S hS P

Tag 0CG3, a remark

Tag 0CG3 in the Stacks Project.

AlgebraicGeometry.Space.isEtale_isEtaleSmoothLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSourceAndTarget/EtaleSmoothExamples.lean, line 69. The attribute's comment: “étale”.

Étaleness of morphisms of algebraic spaces over S is étale-smooth local on the source-and-target.

theorem isEtale_isEtaleSmoothLocalOnSourceAndTarget :
    IsEtaleSmoothLocalOnSourceAndTarget B S hS
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) => IsEtale B S hS f.hom)

AlgebraicGeometry.Space.isLocallyQuasiFinite_isEtaleSmoothLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSourceAndTarget/EtaleSmoothExamples.lean, line 90. The attribute's comment: “locally quasi-finite”.

Local quasi-finiteness of morphisms of algebraic spaces over S is étale-smooth local on the source-and-target.

theorem isLocallyQuasiFinite_isEtaleSmoothLocalOnSourceAndTarget :
    IsEtaleSmoothLocalOnSourceAndTarget B S hS
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) => IsLocallyQuasiFinite B S hS f.hom)

AlgebraicGeometry.Space.isUnramified_isEtaleSmoothLocalOnSourceAndTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/LocalOnSourceAndTarget/EtaleSmoothExamples.lean, line 112. The attribute's comment: “unramified”.

Unramifiedness of morphisms of algebraic spaces over S is étale-smooth local on the source-and-target.

theorem isUnramified_isEtaleSmoothLocalOnSourceAndTarget :
    IsEtaleSmoothLocalOnSourceAndTarget B S hS
      (fun ⦃X Y : AlgebraicSpaces B S hS⦄ (f : X ⟶ Y) => IsUnramified B S hS f.hom)

Sources

LeanAlgebraicGeometry.Space.IsEtaleSmoothLocalOnSourceAndTarget · AlgebraicGeometry.Space.postcomp_of_etale · AlgebraicGeometry.Space.of_comp_etale · AlgebraicGeometry.Space.isLocalAtSource_etale · AlgebraicGeometry.Space.isLocalAtTarget_smooth · AlgebraicGeometry.Space.etaleSmoothLocalOnSourceAndTarget_tfae · AlgebraicGeometry.Space.isEtaleSmoothLocalOnSourceAndTarget_of_local · AlgebraicGeometry.Space.isEtale_isEtaleSmoothLocalOnSourceAndTarget

Section74.22 Descent data for spaces over spaces #

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

Tag 0ADG, a definition

Tag 0ADG in the Stacks Project.

AlgebraicGeometry.Space.Descent.DescentData, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Descent.lean, line 58. The attribute's comment: “parts (1) and (2): a descent datum relative to one morphism Y → X”. References: SGA 3 IV (2.1), “descent datum”.

A descent datum relative to a family of morphisms of algebraic spaces over a scheme.

public structure DescentData
    (hT : IsAlgebraicSpace B S hS T)
    (hX : ∀ i, IsAlgebraicSpace B S hS (X i))

AlgebraicGeometry.Space.Descent.DescentData.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Descent.lean, line 84. The attribute's comment: “parts (1) and (2): a descent datum relative to one morphism Y → X”.

A morphism of descent data is a compatible family of maps over the family members.

public structure Hom (D E : DescentData f hT hX)

Tag 0ADH, a remark

Tag 0ADH in the Stacks Project.

AlgebraicGeometry.Space.Descent.gluingProjEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/ProjectionBaseChange.lean, line 217. The attribute's comment: “the two presentations of the gluing isomorphism of a descent datum”.

Over the pairwise fibre product X i ×_T X j, an isomorphism V_i ×_T X_j ≅ X_i ×_T V_j is the same thing as an isomorphism pr₀^* V_i ≅ pr₁^* V_j of the two base changes along the projections.

def gluingProjEquiv (i j : ι) (Vi : Over (X i)) (Vj : Over (X j)) :
    (Over.mk (prod.map (structureMap (f i) Vi) (𝟙 (Over.mk (f j)))) ≅
        Over.mk (prod.map (𝟙 (Over.mk (f i))) (structureMap (f j) Vj))) ≃
      (projFstObj f i j Vi ≅ projSndObj f i j Vj)

AlgebraicGeometry.Space.Descent.DescentData.projGluing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/ProjectionBaseChange.lean, line 251. The attribute's comment: “the gluing isomorphism read as a map pr₀^ V ⟶ pr₁^ V”.

The gluing isomorphism of a descent datum, read as an isomorphism pr₀^* V_i ≅ pr₁^* V_j of algebraic spaces over the pairwise fibre product X i ×_T X j.

def projGluing (D : DescentData f hT hX) (i j : ι) :
    projFstObj f i j (D.obj i) ≅ projSndObj f i j (D.obj j)

AlgebraicGeometry.Space.Descent.DescentData.projGluing01_comp_projGluing12, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/ProjectionBaseChange.lean, line 379. The attribute's comment: “the cocycle condition in the form pr₀₂^ φ = pr₁₂^ φ ∘ pr₀₁^* φ”.

The cocycle condition of a descent datum, read on base changes along the projections of the triple fibre product: pr₀₂^* φ_ik = pr₁₂^* φ_jk ∘ pr₀₁^* φ_ij.

theorem projGluing01_comp_projGluing12 (D : DescentData f hT hX) (i j k : ι) :
    D.projGluing01 i j k ≫ D.projGluing12 i j k = D.projGluing02 i j k

Tag 0ADI, a definition

Tag 0ADI in the Stacks Project.

AlgebraicGeometry.Space.Descent.DescentData, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Descent.lean, line 58. The attribute's comment: “part (1), descent data”. References: SGA 3 IV (2.1), “descent datum”.

A descent datum relative to a family of morphisms of algebraic spaces over a scheme.

public structure DescentData
    (hT : IsAlgebraicSpace B S hS T)
    (hX : ∀ i, IsAlgebraicSpace B S hS (X i))

AlgebraicGeometry.Space.Descent.DescentData.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Descent.lean, line 84. The attribute's comment: “part (2), morphisms of descent data”.

A morphism of descent data is a compatible family of maps over the family members.

public structure Hom (D E : DescentData f hT hX)

Tag 0ADJ, a remark

Tag 0ADJ in the Stacks Project.

AlgebraicGeometry.Space.Descent.DescentData, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/Descent.lean, line 58. The attribute's comment: “the gluing isomorphisms and the cocycle condition in pullback form”. References: SGA 3 IV (2.1), “descent datum”.

A descent datum relative to a family of morphisms of algebraic spaces over a scheme.

public structure DescentData
    (hT : IsAlgebraicSpace B S hS T)
    (hX : ∀ i, IsAlgebraicSpace B S hS (X i))

Tag 0ADK, a lemma

Tag 0ADK in the Stacks Project.

AlgebraicGeometry.Space.Descent.familyCoproductEquivalenceOfAdmitsCoproductIndex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/CoproductAlgebraicityFull.lean, line 188.

Let {f i : X i → T} be a family of morphisms of algebraic spaces over S with fixed target, and let Y = ∐ X i be the coproduct of the sources in sheaves on the big fppf site, an algebraic space over S by AlgebraicGeometry.Space.Descent.sigmaAlgebraicSheafCoproduct. There is a canonical equivalence from the category of descent data relative to the family to the category of descent data relative to Y → T, which sends (V i, φ i j) to (V, φ) with V = ∐ V i and φ restricting to φ i j on each pair of summands, and a morphism (ψ i) to ∐ ψ i.

The index type is u-small and of cardinality below the cofinality of the site's size cutoff, as is every countable index type.

public def familyCoproductEquivalenceOfAdmitsCoproductIndex :
    FullFamilyCoproductEquivalence.{u, v, w} f hT hX (sigmaAlgebraicSheafCoproduct X hX)

Tag 0ADL, a lemma

Tag 0ADL in the Stacks Project.

AlgebraicGeometry.Space.Descent.pullbackDescentDataFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/HomDescent.lean, line 157. The attribute's comment: “part (1), pullback functor”.

The pullback functor on descent data, with the canonical natural comparison of its underlying space over Y' with ordinary pullback along f.

public def pullbackDescentDataFunctor
    {X X' Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (a : Y ⟶ X) (a' : Y' ⟶ X') (h : X' ⟶ X) (f : Y' ⟶ Y)
    (ha : f ≫ a = a' ≫ h)
    (hX : IsAlgebraicSpace B S hS X)
    (hX' : IsAlgebraicSpace B S hS X')
    (hY : IsAlgebraicSpace B S hS Y)
    (hY' : IsAlgebraicSpace B S hS Y') :
    { F : HomDescentData.{u, v} a hX hY ⥤ HomDescentData.{u, w} a' hX' hY' //
      ∃ α : ∀ D : HomDescentData.{u, v} a hX hY,
          (F.obj D).obj PUnit.unit ≅ (Over.pullback f).obj (D.obj PUnit.unit),
        (∀ {D E : HomDescentData.{u, v} a hX hY} (φ : D ⟶ E),
          (F.map φ).hom PUnit.unit ≫ (α E).hom =
            (α D).hom ≫ (Over.pullback f).map (φ.hom PUnit.unit)) ∧
        (∀ D : HomDescentData.{u, v} a hX hY,
          let A' := (Over.map a').obj ((F.obj D).obj PUnit.unit)
          let B' := Over.mk a'
          let A := (Over.map a).obj (D.obj PUnit.unit)
          let B := Over.mk a
          ∃ (q : (Over.map h).obj A' ⟶ A)
            (r : (Over.map h).obj B' ⟶ B),
            q.left = (α D).hom.left ≫ pullback.fst (D.obj PUnit.unit).hom f ∧
            r.left = f ∧
            (let s : (Over.map h).obj (A' ⨯ B') ⟶ A ⨯ B :=
                prod.lift ((Over.map h).map (prod.fst : A' ⨯ B' ⟶ A') ≫ q)
                  ((Over.map h).map (prod.snd : A' ⨯ B' ⟶ B') ≫ r)
             let t : (Over.map h).obj (B' ⨯ A') ⟶ B ⨯ A :=
                prod.lift ((Over.map h).map (prod.fst : B' ⨯ A' ⟶ B') ≫ r)
                  ((Over.map h).map (prod.snd : B' ⨯ A' ⟶ A') ≫ q)
             (Over.map h).map ((F.obj D).gluing PUnit.unit PUnit.unit).hom.left ≫ t =
               s ≫ (D.gluing PUnit.unit PUnit.unit).hom.left)) }

AlgebraicGeometry.Space.Descent.pullbackDescentDataFunctor_canonicalIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/HomDescent.lean, line 445. The attribute's comment: “part (2), canonical isomorphism”.

Pullback along two maps completing the same square is canonically and naturally isomorphic, by the gluing isomorphism of the descent datum.

public def pullbackDescentDataFunctor_canonicalIso :
    let F₀ := pullbackDescentDataFunctor.{u, v, w} a a' h f₀ ha₀ hX hX' hY hY'
    let F₁ := pullbackDescentDataFunctor.{u, v, w} a a' h f₁ ha₁ hX hX' hY hY'
    let α₀ := Classical.choose F₀.property
    let α₁ := Classical.choose F₁.property
    { η : F₀.val ≅ F₁.val //
      ∀ D : HomDescentData.{u, v} a hX hY,
        let V₀ := (F₀.val.obj D).obj PUnit.unit
        let V₁ := (F₁.val.obj D).obj PUnit.unit
        let A := (Over.map a).obj (D.obj PUnit.unit)
        let B₀ := Over.mk a
        ∃ (q₀ : (Over.map (a' ≫ h)).obj V₀ ⟶ A)
          (q₁ : (Over.map (a' ≫ h)).obj V₁ ⟶ A)
          (y₁ : (Over.map (a' ≫ h)).obj V₀ ⟶ B₀)
          (y₀ : (Over.map (a' ≫ h)).obj V₁ ⟶ B₀),
          q₀.left = (α₀ D).hom.left ≫ pullback.fst (D.obj PUnit.unit).hom f₀ ∧
          q₁.left = (α₁ D).hom.left ≫ pullback.fst (D.obj PUnit.unit).hom f₁ ∧
          y₁.left = V₀.hom ≫ f₁ ∧ y₀.left = V₁.hom ≫ f₀ ∧
          prod.lift q₀ y₁ ≫ (D.gluing PUnit.unit PUnit.unit).hom.left =
            (Over.map (a' ≫ h)).map ((η.hom.app D).hom PUnit.unit) ≫
              prod.lift y₀ q₁ }

Tag 0ADM, a definition

Tag 0ADM in the Stacks Project.

AlgebraicGeometry.Space.Descent.pullbackDescentDataFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/HomDescent.lean, line 157. The attribute's comment: “the functor so constructed is the pullback functor on descent data”.

The pullback functor on descent data, with the canonical natural comparison of its underlying space over Y' with ordinary pullback along f.

public def pullbackDescentDataFunctor
    {X X' Y Y' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (a : Y ⟶ X) (a' : Y' ⟶ X') (h : X' ⟶ X) (f : Y' ⟶ Y)
    (ha : f ≫ a = a' ≫ h)
    (hX : IsAlgebraicSpace B S hS X)
    (hX' : IsAlgebraicSpace B S hS X')
    (hY : IsAlgebraicSpace B S hS Y)
    (hY' : IsAlgebraicSpace B S hS Y') :
    { F : HomDescentData.{u, v} a hX hY ⥤ HomDescentData.{u, w} a' hX' hY' //
      ∃ α : ∀ D : HomDescentData.{u, v} a hX hY,
          (F.obj D).obj PUnit.unit ≅ (Over.pullback f).obj (D.obj PUnit.unit),
        (∀ {D E : HomDescentData.{u, v} a hX hY} (φ : D ⟶ E),
          (F.map φ).hom PUnit.unit ≫ (α E).hom =
            (α D).hom ≫ (Over.pullback f).map (φ.hom PUnit.unit)) ∧
        (∀ D : HomDescentData.{u, v} a hX hY,
          let A' := (Over.map a').obj ((F.obj D).obj PUnit.unit)
          let B' := Over.mk a'
          let A := (Over.map a).obj (D.obj PUnit.unit)
          let B := Over.mk a
          ∃ (q : (Over.map h).obj A' ⟶ A)
            (r : (Over.map h).obj B' ⟶ B),
            q.left = (α D).hom.left ≫ pullback.fst (D.obj PUnit.unit).hom f ∧
            r.left = f ∧
            (let s : (Over.map h).obj (A' ⨯ B') ⟶ A ⨯ B :=
                prod.lift ((Over.map h).map (prod.fst : A' ⨯ B' ⟶ A') ≫ q)
                  ((Over.map h).map (prod.snd : A' ⨯ B' ⟶ B') ≫ r)
             let t : (Over.map h).obj (B' ⨯ A') ⟶ B ⨯ A :=
                prod.lift ((Over.map h).map (prod.fst : B' ⨯ A' ⟶ B') ≫ r)
                  ((Over.map h).map (prod.snd : B' ⨯ A' ⟶ A') ≫ q)
             (Over.map h).map ((F.obj D).gluing PUnit.unit PUnit.unit).hom.left ≫ t =
               s ≫ (D.gluing PUnit.unit PUnit.unit).hom.left)) }

Tag 0ADN, a lemma

Tag 0ADN in the Stacks Project.

AlgebraicGeometry.Space.Descent.pullbackDatum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/FamilyPullback.lean, line 224. The attribute's comment: “family_pullback_datum”.

Pullback of a descent datum along a morphism of families of algebraic spaces.

public def pullbackDatum (g : T' ⟶ T) (comm : ∀ i, gᵢ i ≫ f (α i) = f' i ≫ g) :
    PulledBackDatum f f' hT hX hT' hX' α gᵢ D

AlgebraicGeometry.Space.Descent.pullbackFunctorCoproductComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/FamilyPullbackCoproduct.lean, line 1086. The attribute's comment: “part (4), agreement with the pullback functors of 0ADL through 0ADK”.

Stacks Project, Tag 0ADN part (4). Let U = {X j → T} and U' = {X' i → T'} be families of morphisms of algebraic spaces over S with fixed target, and let α : I' → I, g : T' → T, gᵢ : X' i → X (α i) be a morphism of families with fixed target. The pullback functor on descent data along that morphism of families, Tag 0ADN part (2), agrees — through the canonical equivalences of Tag 0ADK between descent data for a family and descent data for the coproduct of its sources — with the pullback functor of Tag 0ADL for the induced commutative square ∐ X' i → ∐ X j, T' → T of single morphisms.

The isomorphism is pinned on each summand: on the i-th summand of the coproduct of the pulled-back components it is the projection of X' i ×_{X (α i)} V (α i) onto V (α i), followed by the inclusion of the α i-th summand of the coproduct of the original components.

The index types are u-small and of cardinality below the cofinality of the site's size cutoff, as is every countable index type. This is the same size condition that AlgebraicGeometry.Space.Descent.familyCoproductEquivalenceOfAdmitsCoproductIndex carries, and it is what makes the coproducts exist at all.

public def pullbackFunctorCoproductComparison :
    let Ycop := sigmaAlgebraicSheafCoproduct X hX
    let Y'cop := sigmaAlgebraicSheafCoproduct X' hX'
    let E := familyCoproductEquivalenceOfAdmitsCoproductIndex.{u, v, w} f hT hX
    let E' := familyCoproductEquivalenceOfAdmitsCoproductIndex.{u, v', w} f' hT' hX'
    let P := pullbackFunctor f f' hT hX hT' hX' α g gᵢ comm
    let F := pullbackDescentDataFunctor.{u, w, w} (Ycop.desc (spaceSheaf T hT) f)
      (Y'cop.desc (spaceSheaf T' hT') f') g (coproductMap hX hX' α gᵢ Ycop Y'cop)
      (coproductMap_comm f f' hT hX hT' hX' α g gᵢ comm Ycop Y'cop) hT hT'
      Ycop.isAlgebraicSpace Y'cop.isAlgebraicSpace
    let αF := Classical.choose F.property
    { η : P.functor ⋙ E'.equivalence.functor ≅ E.equivalence.functor ⋙ F.val //
      ∀ (D : DescentData f hT hX) (i : ι'),
        ((fullTotalCoproduct f' hT' hX' (P.functor.obj D)).ι i).hom ≫
            (E'.objIso (P.functor.obj D)).inv.left ≫
            ((η.hom.app D).hom PUnit.unit).left ≫
            (αF (E.equivalence.functor.obj D)).hom.left ≫
            pullback.fst ((E.equivalence.functor.obj D).obj PUnit.unit).hom
              (coproductMap hX hX' α gᵢ Ycop Y'cop) =
          ((eqToHom (P.obj_eq D)).hom i).left ≫
            (pullbackDatum f f' hT hX hT' hX' α gᵢ D g comm).objMap i ≫
            ((fullTotalCoproduct f hT hX D).ι (α i)).hom ≫ (E.objIso D).inv.left }

AlgebraicGeometry.Space.Descent.pullbackFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/FamilyPullbackFunctor.lean, line 81. The attribute's comment: “family_pullback_functor”.

Pullback along a morphism of families is functorial on descent data. This is the pullback functor named by Tag 0ADP.

public noncomputable def pullbackFunctor :
    PullbackFunctor f f' hT hX hT' hX' α g gᵢ comm

AlgebraicGeometry.Space.Descent.pullbackFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/FamilyPullbackIndependence.lean, line 306. The attribute's comment: “family_map_independence”.

The canonical natural isomorphism between the pullback functors induced by two morphisms of families with the same map of targets.

public def pullbackFunctorIso :
    PullbackFunctorIso f f' hT hX hT' hX' α β g gᵢ hᵢ commα commβ
      (pullbackFunctor f f' hT hX hT' hX' α g gᵢ commα)
      (pullbackFunctor f f' hT hX hT' hX' β g hᵢ commβ)

Tag 0ADP, a definition

Tag 0ADP in the Stacks Project.

AlgebraicGeometry.Space.Descent.pullbackFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/FamilyPullbackFunctor.lean, line 81.

Pullback along a morphism of families is functorial on descent data. This is the pullback functor named by Tag 0ADP.

public noncomputable def pullbackFunctor :
    PullbackFunctor f f' hT hX hT' hX' α g gᵢ comm

Tag 0ADQ, a definition

Tag 0ADQ in the Stacks Project.

AlgebraicGeometry.Space.Descent.trivialDescentFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/Effective.lean, line 57. The attribute's comment: “part (1), trivial descent datum”.

An algebraic space over X carries its trivial descent datum for the identity of X.

public def trivialDescentFunctor (X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B S hS X) :
    AlgebraicSpacesOver (B := B) (S := S) (hS := hS) X ⥤
      HomDescentData.{u, v} (𝟙 X) hX hX

AlgebraicGeometry.Space.Descent.canonicalDescentFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/Effective.lean, line 78. The attribute's comment: “part (2), canonical descent datum”.

Pulling the trivial descent datum back along a morphism gives the canonical descent datum of an algebraic space over the target.

public def canonicalDescentFunctor {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : Y ⟶ X)
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) :
    AlgebraicSpacesOver (B := B) (S := S) (hS := hS) X ⥤ HomDescentData.{u, v} f hX hY

AlgebraicGeometry.Space.Descent.HomDescentData.IsEffective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/Effective.lean, line 87. The attribute's comment: “part (3), effectivity”.

A descent datum for one morphism is effective if it is isomorphic to the canonical descent datum of an algebraic space over the target.

public abbrev HomDescentData.IsEffective {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : Y ⟶ X}
    {hX : IsAlgebraicSpace B S hS X} {hY : IsAlgebraicSpace B S hS Y}
    (D : HomDescentData.{u, v} f hX hY) : Prop

Tag 0ADR, a definition

Tag 0ADR in the Stacks Project.

AlgebraicGeometry.Space.Descent.familyCanonicalDescentFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/Effective.lean, line 98. The attribute's comment: “part (1), canonical descent datum”.

Pulling the trivial descent datum over T back to each member of a family gives the canonical descent datum of an algebraic space over T.

public def familyCanonicalDescentFunctor (f : ∀ i, X i ⟶ T)
    (hT : IsAlgebraicSpace B S hS T) (hX : ∀ i, IsAlgebraicSpace B S hS (X i)) :
    AlgebraicSpacesOver (B := B) (S := S) (hS := hS) T ⥤ DescentData f hT hX

AlgebraicGeometry.Space.Descent.DescentData.IsEffective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/Effective.lean, line 108. The attribute's comment: “part (2), effectivity”.

A descent datum for a family is effective if it is isomorphic to the canonical descent datum of an algebraic space over the target.

public abbrev DescentData.IsEffective {f : ∀ i, X i ⟶ T} {hT : IsAlgebraicSpace B S hS T}
    {hX : ∀ i, IsAlgebraicSpace B S hS (X i)} (D : DescentData f hT hX) : Prop

Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

74.3 Descent data for… to 74.22 Descent data for spaces…

Section74.3 Descent data for quasi-coherent sheaves#

Tag 04W3, a definition

Tag 04W4, a lemma

Tag 04W5, a definition

Tag 04W6, a lemma

Sources

Section74.4 Fpqc descent of quasi-coherent sheaves#

Tag 04W8, a proposition

Sources

Section74.5 Quasi-coherent modules and affines#

Tag 0H03, an equation

Tag 0H04, a lemma

Sources

Section74.6 Descent of finiteness properties of modules#

Tag 060U, a lemma

Tag 060V, a lemma

Tag 060W, a lemma

Tag 060X, a lemma

Tag 060Y, a lemma

Tag 060Z, a lemma

Tag 0610, a lemma

Sources

Section74.7 Fpqc coverings#

Tag 04P1, a lemma

Tag 04P2, a lemma

Sources

Section74.8 Descent of finiteness and smoothness properties of morphisms#

Tag 06NR, a lemma

Tag 0AHC, a lemma

Tag 0AHD, a lemma

Tag 0AHE, a lemma

Tag 0AHF, a lemma

Sources

Section74.9 Descending properties of spaces#

Tag 06DQ, a lemma

Tag 06MI, a lemma

Tag 06MJ, a lemma

Tag 06MK, a lemma

Tag 0GB3, a lemma

Sources

Section74.10 Descending properties of morphisms#

Tag 03YH, a definition

Tag 06EM, a lemma

Tag 06R2, a lemma

Tag 041J, a lemma

Sources

Section74.11 Descending properties of morphisms in the fpqc topology#

Tag 041L, a lemma

Tag 041N, a lemma

Tag 041O, a lemma

Tag 041P, a lemma

Tag 0CFW, a lemma

Tag 041Q, a lemma

Tag 041R, a lemma

Tag 0CFX, a lemma

Tag 041S, a lemma

Tag 041T, a lemma

Tag 041U, a lemma

Tag 041V, a lemma

Tag 041W, a lemma

Tag 041X, a lemma

Tag 041Y, a lemma

Tag 041Z, a lemma

Tag 0420, a lemma

Tag 0421, a lemma

Tag 0422, a lemma

Tag 0423, a lemma

Tag 0424, a lemma

Tag 0425, a lemma

Tag 0426, a lemma

Tag 0427, a lemma

Tag 0428, a lemma

Tag 0429, a lemma

Tag 042A, a lemma

Tag 042B, a lemma

Tag 042C, a lemma

Tag 042D, a lemma

Sources

Section74.12 Descending properties of morphisms in the fppf topology#

Section74.3 Descent data for quasi-coherent sheaves #

Section74.4 Fpqc descent of quasi-coherent sheaves #

Section74.5 Quasi-coherent modules and affines #

Section74.6 Descent of finiteness properties of modules #

Section74.7 Fpqc coverings #

Section74.8 Descent of finiteness and smoothness properties of morphisms #

Section74.9 Descending properties of spaces #

Section74.10 Descending properties of morphisms #

Section74.11 Descending properties of morphisms in the fpqc topology #

Section74.12 Descending properties of morphisms in the fppf topology #

Section74.13 Application of descent of properties of morphisms #

Section74.14 Properties of morphisms local on the source #

Section74.15 Properties of morphisms local in the fpqc topology on the source #

Section74.16 Properties of morphisms local in the fppf topology on the source #

Section74.17 Properties of morphisms local in the syntomic topology on the source #

Section74.18 Properties of morphisms local in the smooth topology on the source #

Section74.19 Properties of morphisms local in the étale topology on the source #

Section74.20 Properties of morphisms smooth local on source-and-target #

Section74.21 Properties of morphisms étale-smooth local on source-and-target #

Section74.22 Descent data for spaces over spaces #