81 Pushouts of Algebraic Spaces

Chapter 81 of the Stacks Project, Pushouts of Algebraic Spaces, Tag 0AHT: the 12 sections of its 14 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 65 tags are carried by 129 declarations of the repository (all in StacksFrontier) and 1 registered declaration.

Section81.3 Colimits of algebraic spaces #

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

Tag 07SX, a lemma

Tag 07SX in the Stacks Project.

AlgebraicGeometry.Space.isColimit_algebraicSpaces_of_scheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/Colimits.lean, line 415.

Under descent of separated étale families and preservation of the scheme colimit by étale base change, the colimit is also a colimit of algebraic spaces.

public theorem isColimit_algebraicSpaces_of_scheme
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type u} [Category.{u} I]
    (D : I ⥤ BigFppfOver B S hS) (c : Cocone D)
    (_hColimit : IsColimit ((BigFppfOver.toScheme B S hS).mapCocone c))
    (hCover : ∀ x : (BigFppfOver.toScheme B S hS).obj c.pt,
      ∃ (i : I) (y : (BigFppfOver.toScheme B S hS).obj (D.obj i)),
        (BigFppfOver.toScheme B S hS).map (c.ι.app i) y = x)
    (hEtaleColimit :
      ∀ (U : BigFppfOver B S hS) (v : U ⟶ c.pt),
        Etale ((BigFppfOver.toScheme B S hS).map v) →
        ∀ (E : I ⥤ BigFppfOver B S hS) (p : E ⟶ D)
          (q : E ⟶ (Functor.const I).obj U),
          (∀ i, IsPullback (p.app i) (q.app i) (c.ι.app i) v) →
          IsColimit ((BigFppfOver.toScheme B S hS).mapCocone
            ({ pt := U, ι := q } : Cocone E)))
    (hEtaleDescent :
      ∀ (E : I ⥤ BigFppfOver B S hS) (p : E ⟶ D),
        (∀ i, Etale ((BigFppfOver.toScheme B S hS).map (p.app i))) →
        (∀ i, _root_.AlgebraicGeometry.IsSeparated
          ((BigFppfOver.toScheme B S hS).map (p.app i))) →
        (∀ {i j : I} (f : i ⟶ j),
          IsPullback (E.map f) (p.app i) (p.app j) (D.map f)) →
        ∃ (U : BigFppfOver B S hS) (v : U ⟶ c.pt)
          (q : E ⟶ (Functor.const I).obj U),
          Etale ((BigFppfOver.toScheme B S hS).map v) ∧
          (∀ i, IsPullback (p.app i) (q.app i) (c.ι.app i) v)) :
    ∀ (F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u),
      IsAlgebraicSpace B S hS F →
      ∀ (a : ∀ i : I, yoneda.obj (D.obj i) ⟶ F),
        (∀ {i j : I} (f : i ⟶ j), yoneda.map (D.map f) ≫ a j = a i) →
        ∃! b : yoneda.obj c.pt ⟶ F,
          ∀ i, yoneda.map (c.ι.app i) ≫ b = a i

Tag 0GFQ, a lemma

Tag 0GFQ in the Stacks Project.

AlgebraicGeometry.Space.isColimit_of_fpqc_local, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ColimitsFpqcLocal.lean, line 92.

[Stacks, Tag 0GFQ]. Let T be an algebraic space over a scheme S of a big fppf site and let D be a diagram of algebraic spaces over T with a cocone c. Suppose given an fpqc covering f a : (d a).pt ⟶ c.pt of the vertex such that

every d a is a cocone on a diagram E a whose squares over D are cartesian, and d a is a colimit; and

every pairwise overlap d₂ a b of the covering is likewise a cocone on a cartesian diagram E₂ a b over D and is a colimit.

Then c is a colimit of D in the category of algebraic spaces over T.

The base algebraic space is the source's B; it is called T here because B names the big fppf site throughout this library.

theorem isColimit_of_fpqc_local
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {T : AlgebraicSpaces B S hS}
    {I : Type v} [Category.{w} I] (D : I ⥤ Over T) (c : Cocone D)
    {A : Type t}
    (E : A → I ⥤ Over T) (d : ∀ a, Cocone (E a))
    (p : ∀ a, E a ⟶ D)
    (f : ∀ a, (d a).pt ⟶ c.pt)
    (hcover : IsFpqcCovering B S hS fun a => ((f a).left).hom)
    (hbase : ∀ (a : A) (i : I),
      IsPullback ((p a).app i).left ((d a).ι.app i).left (c.ι.app i).left (f a).left)
    (hlocal : ∀ a, Nonempty (IsColimit (d a)))
    (E₂ : A → A → I ⥤ Over T)
    (d₂ : ∀ a b, Cocone (E₂ a b))
    (p₂ : ∀ a b, E₂ a b ⟶ D)
    (toFirst : ∀ a b, (d₂ a b).pt ⟶ (d a).pt)
    (toSecond : ∀ a b, (d₂ a b).pt ⟶ (d b).pt)
    (hoverlap : ∀ a b, IsPullback (toFirst a b).left (toSecond a b).left (f a).left (f b).left)
    (hbaseOverlap : ∀ (a b : A) (i : I),
      IsPullback ((p₂ a b).app i).left ((d₂ a b).ι.app i).left
        (c.ι.app i).left (toFirst a b ≫ f a).left)
    (hoverlapColimit : ∀ a b, Nonempty (IsColimit (d₂ a b))) :
    Nonempty (IsColimit c)

Tag 0GHL, a lemma

Tag 0GHL in the Stacks Project.

AlgebraicGeometry.Space.isColimit_of_etale_local_affine_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/EtaleLocalAffineColimit.lean, line 1200.

Stacks 0GHL. Let B be an algebraic space over S, let D be a diagram of algebraic spaces over B and let c be a cocone on D. If base change along the cocone legs is an equivalence from the small étale site of the vertex onto the limit of the small étale sites of the members, and if every cocone of morphisms from the base changes of an affine étale realization to an affine space over an affine étale base descends uniquely, then c is a colimit of D in the category of algebraic spaces over B.

theorem isColimit_of_etale_local_affine_descent
    {I : Type v} [Category.{w} I]
    {B : AlgebraicSpaces site S hS} {D : I ⥤ Over B}
    (c : Cocone D)
    (h₁ : EtaleComparisonIsEquivalence site S hS c)
    (h₂ : ∀ (B' : AlgebraicSpaces site S hS) (b : B' ⟶ B),
      IsAffineSpace site S hS B'.1 →
      IsEtale site S hS b.hom →
      ∀ (Z : AlgebraicSpaces site S hS) (z : Z ⟶ B'),
        IsAffineSpace site S hS Z.1 →
        ∀ (E : CompatibleEtaleDiagram site S hS D)
          (r : EtaleRealization site S hS c E),
          IsAffineSpace site S hS r.U.1 →
          ∀ (u : r.U ⟶ B'),
            r.toX ≫ c.pt.hom = u ≫ b →
            ∀ (fᵢ : E.U ⟶ (Functor.const I).obj Z),
              (∀ i, fᵢ.app i ≫ z = r.baseChange.app i ≫ u) →
              ∃! f : r.U ⟶ Z,
                (f ≫ z = u) ∧
                  (∀ i, r.baseChange.app i ≫ f = fᵢ.app i)) :
    Nonempty (IsColimit c)

Tag 0GFP, a lemma

Tag 0GFP in the Stacks Project.

AlgebraicGeometry.Space.isColimit_of_separated_etale_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/SeparatedColimitCriterion.lean, line 500. The attribute's comment: “all five hypotheses; (1) carried by the diagram landing in the separated spaces over B, (2) by IsColimit of the cocone there, (3) stated as joint surjectivity on points, (4) and (5) stated with cartesian comparison squares”.

Stacks 0GFP. Let B be an algebraic space over S and let D be a diagram of algebraic spaces separated over B, with a colimit c in the category of algebraic spaces separated over B. Assume that the members of the diagram jointly cover the vertex on points, that every separated étale algebraic space over the vertex is the colimit of its base changes to the members of the diagram, and that every compatible family of separated étale algebraic spaces over the members of the diagram arises as the family of base changes of a separated étale algebraic space over the vertex. Then c is a colimit of the diagram in the category of all algebraic spaces over B.

theorem isColimit_of_separated_etale_descent
    (D : I ⥤ SeparatedOver site S hS B) (c : Cocone D) (hc : IsColimit c)
    (hcover : ∀ x : points site S hS c.pt.obj.left.obj,
      ∃ i : I, ∃ y : points site S hS (D.obj i).obj.left.obj,
        pointsMap site S hS (D.obj i).obj.left.obj (c.ι.app i).hom.left.hom y = x)
    (hbase : ∀ (E : I ⥤ SeparatedOver site S hS B) (p : E ⟶ D) (d : Cocone E)
      (q : d.pt ⟶ c.pt), IsEtaleSeparated site S hS q →
      (∀ i : I, IsPullback (p.app i).hom.left (d.ι.app i).hom.left
        (c.ι.app i).hom.left q.hom.left) → IsColimit d)
    (hdesc : ∀ (E : I ⥤ SeparatedOver site S hS B) (p : E ⟶ D),
      (∀ i : I, IsEtaleSeparated site S hS (p.app i)) →
      (∀ {i j : I} (f : i ⟶ j), IsPullback (E.map f).hom.left (p.app i).hom.left
        (p.app j).hom.left (D.map f).hom.left) →
      ∃ (d : Cocone E) (q : d.pt ⟶ c.pt), IsEtaleSeparated site S hS q ∧
        ∀ i : I, IsPullback (p.app i).hom.left (d.ι.app i).hom.left
          (c.ι.app i).hom.left q.hom.left) :
    Nonempty (IsColimit ((separatedOverInclusion site S hS B).mapCocone c))

Sources

LeanAlgebraicGeometry.Space.isColimit_algebraicSpaces_of_scheme · AlgebraicGeometry.Space.isColimit_of_fpqc_local · AlgebraicGeometry.Space.isColimit_of_etale_local_affine_descent · AlgebraicGeometry.Space.isColimit_of_separated_etale_descent

Section81.4 Descending étale sheaves #

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

Tag 0GFS, a lemma

Tag 0GFS in the Stacks Project.

AlgebraicGeometry.Space.SpacesEtale.isEquivalence_toDescentData_smallEtaleSheafSystem_of_isEtaleCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallEtaleSheafDescent.lean, line 196.

Stacks 0GFS. Let X be an algebraic space over a scheme S and let {g i : Y i ⟶ X} be an étale covering of algebraic spaces. Then sheaves of sets on the small étale site of X are equivalent, via the functor taking a sheaf to its canonical descent datum, to descent data for étale sheaves with respect to that covering: a sheaf on the small étale site of each Y i, together with transition isomorphisms over the overlaps satisfying the cocycle condition.

theorem isEquivalence_toDescentData_smallEtaleSheafSystem_of_isEtaleCovering
    [∀ (U : SpacesEtale B S hS X) (Z : _),
      HasLimitsOfShape
        (StructuredArrow Z (Space.comparisonFunctor B S hS U.obj.left).op) (Type (u + 1))]
    {I : Type t} (Y : I → AlgebraicSpaces B S hS) (g : ∀ i, Y i ⟶ X)
    (hg : IsEtaleCovering B S hS (fun i => (Y i).1) (fun i => (g i).hom)) :
    ((smallEtaleSheafSystem B S hS (X := X)).toDescentData
      (fun i => toFinal B S hS (etaleObject B S hS (g i) (hg.etale i)))).IsEquivalence

AlgebraicGeometry.Space.SpacesEtale.isEquivalence_toDescentData_spacesEtalePseudofunctor_of_isEtaleCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleGlobalDescent.lean, line 555. The attribute's comment: “for the pseudofunctor of spaces-étale inverse images”.

Stacks 0GFS for the pseudofunctor of spaces-étale inverse images. Let X be an algebraic space over a scheme S and let {g i : Y i ⟶ X} be an étale covering of algebraic spaces. Then sheaves of sets on the spaces-étale site of X are equivalent, via the functor taking a sheaf to its canonical descent datum, to descent data for that covering: a spaces-étale sheaf on each Y i, together with transition isomorphisms over the overlaps satisfying the cocycle condition.

theorem isEquivalence_toDescentData_spacesEtalePseudofunctor_of_isEtaleCovering
    {I : Type t} (Y : I → AlgebraicSpaces B S hS) (g : ∀ i, Y i ⟶ X)
    (hg : IsEtaleCovering B S hS (fun i => (Y i).1) (fun i => (g i).hom)) :
    ((spacesEtalePseudofunctor B S hS).toDescentData g).IsEquivalence

Tag 0GFT, a lemma

Tag 0GFT in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_toDescentData_singleton_of_isEtaleCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleDescentEtaleLocal.lean, line 374. The attribute's comment: “for the pseudofunctor of spaces-étale inverse images”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S and let {g i : Y i ⟶ Y} be an étale covering. If spaces-étale sheaves on Y i are equivalent, via the canonical descent datum, to descent data for the base change X ×_Y Y i ⟶ Y i of f, and likewise over each pairwise overlap Y i ×_Y Y j, then spaces-étale sheaves on Y are equivalent to descent data for f itself.

theorem isEquivalence_toDescentData_singleton_of_isEtaleCovering
    (hY : ∀ i, ((spacesEtalePseudofunctor B S hS).toDescentData
      (fun _ : Unit => (spacesChosenPullback B S hS f (g i)).p₂)).IsEquivalence)
    (hYY : ∀ i j, ((spacesEtalePseudofunctor B S hS).toDescentData
      (fun _ : Unit => (spacesChosenPullback B S hS f
        (spacesChosenPullback B S hS (g i) (g j)).p).p₂)).IsEquivalence) :
    ((spacesEtalePseudofunctor B S hS).toDescentData
      (fun _ : Unit => f)).IsEquivalence

Tag 0GFU, a lemma

Tag 0GFU in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_toDescentData_singleton_of_surjective_integral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleDescentRepresentableCover.lean, line 193. The attribute's comment: “the surjective integral case, for the pseudofunctor of spaces-étale inverse images, granted the case of a representable target as the hypothesis hsch. Proved here: the étale-local reduction of the source, that is, that the conclusion for an arbitrary algebraic space Y follows from the case in which the target is a scheme -- a scheme atlas of Y is a one-member étale covering (Tag 025Y), the two base changes of f named by Tag 0GFT have representable target, and the representable surjective integral morphisms are stable under base change (Tag 02WE). NOT proved, and carried by hsch: the case of a scheme target, which the source deduces from Etale Cohomology Tag 0GEZ; that lemma is not in this library and rests in turn on the devissage of Tag 0GF1 and on the base-change theorem of Tag 0EYP. The other two cases of the source statement are separate declarations with their own hypothesis.”.

Stacks 0GFU, the surjective integral case. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is representable by schemes, surjective and integral. Then spaces-étale sheaves on Y are equivalent, via the canonical descent datum, to descent data for the covering {X ⟶ Y}, granted the same assertion for a morphism with representable target.

theorem isEquivalence_toDescentData_singleton_of_surjective_integral
    (hsch : SpacesEtaleDescentOverRepresentable B S hS
      (MorphismProperty.inverseImage
        (@AlgebraicGeometry.Surjective.{u} ⊓ @AlgebraicGeometry.IsIntegralHom.{u})
        (BigFppfOver.toScheme B S hS)).presheaf)
    (f : X ⟶ Y)
    (hsurj : (MorphismProperty.inverseImage (@AlgebraicGeometry.Surjective.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f.hom)
    (hint : (MorphismProperty.inverseImage (@AlgebraicGeometry.IsIntegralHom.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f.hom) :
    ((spacesEtalePseudofunctor B S hS).toDescentData (fun _ : Unit => f)).IsEquivalence

AlgebraicGeometry.Space.isEquivalence_toDescentData_singleton_of_surjective_proper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleDescentRepresentableCover.lean, line 221. The attribute's comment: “the surjective proper case, for the pseudofunctor of spaces-étale inverse images, granted the case of a representable target as the hypothesis hsch. Proved here: the étale-local reduction of the source, that is, that the conclusion for an arbitrary algebraic space Y follows from the case in which the target is a scheme -- a scheme atlas of Y is a one-member étale covering (Tag 025Y), the two base changes of f named by Tag 0GFT have representable target, and the representable surjective proper morphisms are stable under base change (Tag 02WE). NOT proved, and carried by hsch: the case of a scheme target, which the source deduces from Etale Cohomology Tag 0GF0; that lemma is not in this library and rests in turn on the devissage of Tag 0GF1 and on the proper base-change theorem of Tag 0A3U. The other two cases of the source statement are separate declarations with their own hypothesis.”.

Stacks 0GFU, the surjective proper case. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is representable by schemes, surjective and proper. Then spaces-étale sheaves on Y are equivalent, via the canonical descent datum, to descent data for the covering {X ⟶ Y}, granted the same assertion for a morphism with representable target.

theorem isEquivalence_toDescentData_singleton_of_surjective_proper
    (hsch : SpacesEtaleDescentOverRepresentable B S hS
      (MorphismProperty.inverseImage
        (@AlgebraicGeometry.Surjective.{u} ⊓ @AlgebraicGeometry.IsProper.{u})
        (BigFppfOver.toScheme B S hS)).presheaf)
    (f : X ⟶ Y)
    (hsurj : (MorphismProperty.inverseImage (@AlgebraicGeometry.Surjective.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f.hom)
    (hproper : (MorphismProperty.inverseImage (@AlgebraicGeometry.IsProper.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f.hom) :
    ((spacesEtalePseudofunctor B S hS).toDescentData (fun _ : Unit => f)).IsEquivalence

AlgebraicGeometry.Space.isEquivalence_toDescentData_singleton_of_surjective_flat_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleDescentRepresentableCover.lean, line 251. The attribute's comment: “the surjective flat locally-of-finite-presentation case, for the pseudofunctor of spaces-étale inverse images, granted the case of a representable target as the hypothesis hsch. Proved here: the étale-local reduction of the source, that is, that the conclusion for an arbitrary algebraic space Y follows from the case in which the target is a scheme -- a scheme atlas of Y is a one-member étale covering (Tag 025Y), the two base changes of f named by Tag 0GFT have representable target, and the representable surjective flat morphisms locally of finite presentation are stable under base change (Tag 02WE). NOT proved, and carried by hsch: the case of a scheme target, which the source deduces from Etale Cohomology Tag 0GF2; that lemma is not in this library and rests in turn on the devissage of Tag 0GF1 and on the finite domination of an fppf covering of Tag 0CP0. The other two cases of the source statement are separate declarations with their own hypothesis.”.

Stacks 0GFU, the surjective flat locally finitely presented case. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is representable by schemes, surjective, flat and locally of finite presentation. Then spaces-étale sheaves on Y are equivalent, via the canonical descent datum, to descent data for the covering {X ⟶ Y}, granted the same assertion for a morphism with representable target.

theorem isEquivalence_toDescentData_singleton_of_surjective_flat_locallyOfFinitePresentation
    (hsch : SpacesEtaleDescentOverRepresentable B S hS
      (MorphismProperty.inverseImage
        (@AlgebraicGeometry.Surjective.{u} ⊓ @AlgebraicGeometry.Flat.{u} ⊓
          @AlgebraicGeometry.LocallyOfFinitePresentation.{u})
        (BigFppfOver.toScheme B S hS)).presheaf)
    (f : X ⟶ Y)
    (hsurj : (MorphismProperty.inverseImage (@AlgebraicGeometry.Surjective.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f.hom)
    (hflat : (MorphismProperty.inverseImage (@AlgebraicGeometry.Flat.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f.hom)
    (hlfp : (MorphismProperty.inverseImage
      (@AlgebraicGeometry.LocallyOfFinitePresentation.{u})
      (BigFppfOver.toScheme B S hS)).presheaf f.hom) :
    ((spacesEtalePseudofunctor B S hS).toDescentData (fun _ : Unit => f)).IsEquivalence

AlgebraicGeometry.Space.isEquivalence_toDescentData_singleton_of_relativelyRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleDescentSchemeTarget.lean, line 187.

Let f : X ⟶ Y be a morphism of algebraic spaces over S which is representable (by schemes) and is surjective and integral, or surjective and proper, or surjective, flat and locally of finite presentation. Then the functor from sheaves on the spaces-étale site of Y (that is, Sh(Y_étale), Stacks 03G1) to descent data for étale sheaves with respect to {X ⟶ Y} is an equivalence of categories.

theorem isEquivalence_toDescentData_singleton_of_relativelyRepresentable
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hrep : yoneda.relativelyRepresentable f.hom)
    (hf : IsSurjectiveIntegralProperOrFlatLfp B S hS f) :
    ((spacesEtalePseudofunctor B S hS).toDescentData (fun _ : Unit => f)).IsEquivalence

Tag 0GFV, a lemma

Tag 0GFV in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_toDescentData_singleton_of_representable_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleDescentRepresentableRefinement.lean, line 235. The attribute's comment: “granted h0GFU, the conclusion of Stacks 0GFU: that for EVERY morphism of algebraic spaces over S which is representable by schemes and is surjective and integral, surjective and proper, or surjective and flat and locally of finite presentation, spaces-étale sheaves on its target are equivalent to descent data for the singleton family it generates. That is the special case π = 𝟙 X of this statement, in which the morphism carrying the hypotheses is the morphism of the descent problem itself, so it is NOT the universally quantified form of this conclusion: this conclusion asks for descent along f while the hypotheses are carried by π ≫ f, and f itself is neither representable nor surjective in any instance of the grant. The implication runs one way only — the grant is an instance of this conclusion, and getting this conclusion back out of the grant is exactly the refinement step. That step, Stacks 0GEA, is proved and not granted: CategoryTheory.Pseudofunctor.isEquivalence_toDescentData_of_homOver of this file restates the library's CategoryTheory.Functor.isEquivalence_toFamilyDescentDatum_of_homOver at an arbitrary pseudofunctor, and its fibre-product and base-change obligations are discharged here”.

Stacks 0GFV for the pseudofunctor of spaces-étale inverse images. Let f : X ⟶ Y be a morphism of algebraic spaces over S and let π : X' ⟶ X be a morphism of algebraic spaces. If the composite π ≫ f is representable by schemes and is surjective and integral, surjective and proper, or surjective and flat and locally of finite presentation, then spaces-étale sheaves on Y are equivalent, via the canonical descent datum, to descent data for the singleton family {X ⟶ Y}. No hypothesis is placed on f itself.

The conclusion of Stacks 0GFU is granted as h0GFU; see the implementation notes of the file.

theorem isEquivalence_toDescentData_singleton_of_representable_comp
    (h0GFU : ∀ {X₀ Y₀ : AlgebraicSpaces B S hS} (f₀ : X₀ ⟶ Y₀),
      yoneda.relativelyRepresentable f₀.hom →
      IsSurjectiveIntegralProperOrFlatLfp B S hS f₀ →
      ((spacesEtalePseudofunctor B S hS).toDescentData
        (fun _ : Unit => f₀)).IsEquivalence)
    {X' X Y : AlgebraicSpaces B S hS} (π : X' ⟶ X) (f : X ⟶ Y)
    (hrep : yoneda.relativelyRepresentable (π ≫ f).hom)
    (hcov : IsSurjectiveIntegralProperOrFlatLfp B S hS (π ≫ f)) :
    ((spacesEtalePseudofunctor B S hS).toDescentData
      (fun _ : Unit => f)).IsEquivalence

AlgebraicGeometry.Space.isEquivalence_toDescentData_singleton_of_relativelyRepresentable_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleDescentSchemeTarget.lean, line 218.

Let f : X ⟶ Y be a morphism of algebraic spaces over S and let π : X' ⟶ X be a morphism of algebraic spaces. Assume that π ≫ f is representable (by schemes) and is surjective and integral, or surjective and proper, or surjective, flat and locally of finite presentation. Then the functor from sheaves on the spaces-étale site of Y to descent data for étale sheaves with respect to {X ⟶ Y} is an equivalence of categories.

theorem isEquivalence_toDescentData_singleton_of_relativelyRepresentable_comp
    {X' X Y : AlgebraicSpaces B S hS} (π : X' ⟶ X) (f : X ⟶ Y)
    (hrep : yoneda.relativelyRepresentable (π ≫ f).hom)
    (hcov : IsSurjectiveIntegralProperOrFlatLfp B S hS (π ≫ f)) :
    ((spacesEtalePseudofunctor B S hS).toDescentData (fun _ : Unit => f)).IsEquivalence

Tag 0GFW, a lemma

Tag 0GFW in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_toDescentData_singleton_of_isSurjectiveIntegralProperOrFlatLfp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleDescentProperSurjective.lean, line 201.

Let f : X ⟶ Y be a morphism of algebraic spaces over S which is surjective and integral, or surjective and proper, or surjective, flat and locally of finite presentation. Then the functor from sheaves on the spaces-étale site of Y to descent data for étale sheaves with respect to {X ⟶ Y} is an equivalence of categories.

theorem isEquivalence_toDescentData_singleton_of_isSurjectiveIntegralProperOrFlatLfp
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : IsSurjectiveIntegralProperOrFlatLfp B S hS f) :
    ((spacesEtalePseudofunctor B S hS).toDescentData (fun _ : Unit => f)).IsEquivalence

AlgebraicGeometry.Space.isEquivalence_toDescentData_singleton_of_isSurjectiveDescentMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleDescentSurjective.lean, line 197. The attribute's comment: “all three cases stated; the integral and flat cases are proved from Stacks 0GFV, carried as a hypothesis, and the proper case is carried whole as a hypothesis”.

Stacks 0GFW for the pseudofunctor of spaces-étale inverse images. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is surjective and integral, or surjective and proper, or surjective and flat and locally of finite presentation. Then sheaves on the spaces-étale site of Y are equivalent, through the canonical descent datum, to descent data for the one-member family {f}.

All three cases are stated. The integral and the flat case are proved from hGFV, which is Stacks 0GFV; the proper case is the hypothesis hproper, carried whole.

theorem isEquivalence_toDescentData_singleton_of_isSurjectiveDescentMorphism
    (hGFV : DescentEffectiveAlongRepresentablePrecomposition B S hS)
    (hproper : DescentEffectiveAlongProperSurjective B S hS)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : IsSurjectiveDescentMorphism B S hS f.hom) :
    ((spacesEtalePseudofunctor B S hS).toDescentData (fun _ : Unit => f)).IsEquivalence

Tag 0GFX, a lemma

Tag 0GFX in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_toDescentData_of_isFppfCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleDescentFppfCovering.lean, line 112.

Let S be a scheme and let {f i : X i ⟶ Y} be an fppf covering of algebraic spaces over S. Then the functor from sheaves on the spaces-étale site of Y (that is, Sh(Y_étale)) to descent data for étale sheaves with respect to {f i : X i ⟶ Y} is an equivalence of categories.

theorem isEquivalence_toDescentData_of_isFppfCovering {I : Type v}
    {X : I → AlgebraicSpaces B S hS} {Y : AlgebraicSpaces B S hS} (f : ∀ i, X i ⟶ Y)
    (hf : IsFppfCovering B S hS (fun i => (X i).1) (fun i => (f i).hom)) :
    ((spacesEtalePseudofunctor B S hS).toDescentData f).IsEquivalence

Tag 0GFY, a lemma

Tag 0GFY in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_spacesModificationRestriction_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleModificationProper.lean, line 68.

[Stacks, Tag 0GFY]. Let S be a scheme, let f : Y ⟶ X be a proper morphism of algebraic spaces over S, let i : Z ⟶ X be a closed immersion, and let E = Z ×_X Y with projections j : E ⟶ Y and g : E ⟶ Z. Suppose f is an isomorphism over the open complement u : X ∖ Z ⟶ X of Z: the projection fU : V ⟶ X ∖ Z of a fibre product V = (X ∖ Z) ×_X Y is an isomorphism. Then the functor Sh(X_étale) ⥤ Sh(Y_étale) ×_{Sh(E_étale)} Sh(Z_étale), F ↦ (f⁻¹F, i⁻¹F), is an equivalence of categories.

theorem isEquivalence_spacesModificationRestriction_of_isProper
    (hf : IsProper B S hS f.hom) (hi : IsClosedImmersion B S hS i.hom)
    (sq : IsPullback j g f i)
    {V : AlgebraicSpaces B S hS} (w' : V ⟶ Y)
    (fU : V ⟶ closedImmersionComplement B S hS i hi) [IsIso fU]
    (sqU : IsPullback w' fU f (closedImmersionComplementHom B S hS i hi)) :
    (spacesModificationRestriction B S hS f i j g sq.w).IsEquivalence

Sources

Section81.5 Descending étale morphisms of algebraic spaces #

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

Tag 0GG0, a lemma

Tag 0GG0 in the Stacks Project.

AlgebraicGeometry.Space.isEffective_homDescentData_of_isEtale_of_isProper_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/EtaleEffectiveAlongProper.lean, line 96. The attribute's comment: “both the effectivity and the sharper form naming an étale V ⟶ Y, stated in the library's vocabulary for descent data of spaces; the translation between descent data of spaces and of étale sheaves and the proper case of Stacks 0GFW are carried as hypotheses”.

Stacks 0GG0. Let f : X ⟶ Y be a proper surjective morphism of algebraic spaces over S. A descent datum relative to f whose underlying space is étale over X is effective; more precisely, it is isomorphic to the canonical descent datum of an algebraic space over Y which is étale over Y.

Two statements of the source are carried as hypotheses rather than proved: hproperCase is the proper case of Stacks 0GFW, which is the case Stacks 0GG0 appeals to, and hbridge is the translation between descent data of spaces and descent data of spaces-étale sheaves.

theorem isEffective_homDescentData_of_isEtale_of_isProper_isSurjective
    (hproperCase : DescentEffectiveAlongProperSurjective B S hS)
    (hbridge : EtaleSpaceDescentEffectiveOfSheafDescent B S hS)
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hsurj : IsSurjective B S hS f.hom) (hproper : IsProper B S hS f.hom)
    (D : Descent.HomDescentData.{u, 0} f.hom Y.property X.property)
    (hD : IsEtale B S hS (D.obj PUnit.unit).hom) :
    Descent.HomDescentData.IsEffective.{u, 0} D ∧
      ∃ V : Descent.AlgebraicSpacesOver (B := B) (S := S) (hS := hS) Y.1,
        IsEtale B S hS V.obj.hom ∧
          Nonempty ((Descent.canonicalDescentFunctor.{u, 0} f.hom Y.property
            X.property).obj V ≅ D)

AlgebraicGeometry.Space.isEffective_and_exists_isEtale_iso_of_isProper_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/SpacesOverSpaces/EtaleEffectiveAlongProperUnconditional.lean, line 55. The attribute's comment: “both the effectivity and the sharper form naming an étale V ⟶ Y”.

Stacks 0GG0. Let f : X ⟶ Y be a proper surjective morphism of algebraic spaces over S. Any descent datum (U/X, φ) relative to f (Stacks 0ADG) with U étale over X is effective (Stacks 0ADQ). More precisely, there exists an algebraic space V over Y, étale over Y, whose canonical descent datum is isomorphic to (U/X, φ).

theorem isEffective_and_exists_isEtale_iso_of_isProper_isSurjective
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hsurj : IsSurjective B S hS f.hom) (hproper : IsProper B S hS f.hom)
    (D : Descent.HomDescentData.{u, 0} f.hom Y.property X.property)
    (hD : IsEtale B S hS (D.obj PUnit.unit).hom) :
    Descent.HomDescentData.IsEffective.{u, 0} D ∧
      ∃ V : Descent.AlgebraicSpacesOver (B := B) (S := S) (hS := hS) Y.1,
        IsEtale B S hS V.obj.hom ∧
          Nonempty ((Descent.canonicalDescentFunctor.{u, 0} f.hom Y.property
            X.property).obj V ≅ D)

Tag 0GG1, a lemma

Tag 0GG1 in the Stacks Project.

AlgebraicGeometry.Space.isEquivalence_spacesEtaleModificationRestriction_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleModificationProper.lean, line 86.

[Stacks, Tag 0GG1]. Let S be a scheme, let f : Y ⟶ X be a proper morphism of algebraic spaces over S, let i : Z ⟶ X be a closed immersion, and let E = Z ×_X Y with projections j : E ⟶ Y and g : E ⟶ Z. Suppose f is an isomorphism over the open complement u : X ∖ Z ⟶ X of Z: the projection fU : V ⟶ X ∖ Z of a fibre product V = (X ∖ Z) ×_X Y is an isomorphism. Then the functor X_{spaces,étale} ⥤ Y_{spaces,étale} ×_{E_{spaces,étale}} Z_{spaces,étale}, V ↦ (V ×_X Y, V ×_X Z), is an equivalence of categories.

theorem isEquivalence_spacesEtaleModificationRestriction_of_isProper
    (hf : IsProper B S hS f.hom) (hi : IsClosedImmersion B S hS i.hom)
    (sq : IsPullback j g f i)
    {V : AlgebraicSpaces B S hS} (w' : V ⟶ Y)
    (fU : V ⟶ closedImmersionComplement B S hS i hi) [IsIso fU]
    (sqU : IsPullback w' fU f (closedImmersionComplementHom B S hS i hi)) :
    (spacesEtaleModificationRestriction B S hS f i j g sq.w).IsEquivalence

Sources

LeanAlgebraicGeometry.Space.isEffective_homDescentData_of_isEtale_of_isProper_isSurjective · AlgebraicGeometry.Space.isEffective_and_exists_isEtale_iso_of_isProper_isSurjective · AlgebraicGeometry.Space.isEquivalence_spacesEtaleModificationRestriction_of_isProper

Section81.6 Pushouts along thickenings and affine morphisms #

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

Tag 07SY, a lemma

Tag 07SY in the Stacks Project.

AlgebraicGeometry.Space.isPushout_algebraicSpaces_of_isThickening_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningAffine.lean, line 1085. The attribute's comment: “granted the étale clause of Tag 07RX, carried as a hypothesis; Tag 06AD is discharged from Stacks.Thickenings.forall_isAffine_of_isThickening”.

Stacks 07SY. The pushout Y' = Y ⨿_X X' of a thickening X ⟶ X' and an affine morphism X ⟶ Y of schemes over S is also a pushout in the category of algebraic spaces over S.

public theorem isPushout_algebraicSpaces_of_isThickening_of_isAffineHom
    (h07RX : ∀ {Z Z' W : Scheme.{u}} (k : Z ⟶ Z') (g : Z ⟶ W) (hk : IsThickening k)
      [IsAffineHom g] [HasPushout k g] (T : Stacks.Pushout.gluingData k g),
      Etale ((Stacks.Pushout.gluingFunctor k g hk).obj T).hom ↔
        (Etale T.obj.left.hom ∧ Etale T.obj.right.hom))
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X X' Y Y' : BigFppfOver B S hS}
    (i : X ⟶ X') (f : X ⟶ Y) (a : X' ⟶ Y') (b : Y ⟶ Y')
    (hi : IsThickening ((BigFppfOver.toScheme B S hS).map i))
    [IsAffineHom ((BigFppfOver.toScheme B S hS).map f)]
    (hPushout : IsPushout ((BigFppfOver.toScheme B S hS).map i)
      ((BigFppfOver.toScheme B S hS).map f)
      ((BigFppfOver.toScheme B S hS).map a)
      ((BigFppfOver.toScheme B S hS).map b)) :
    IsPushout
      (ObjectProperty.homMk (yoneda.map i) :
        (⟨yoneda.obj X, isAlgebraicSpace_yoneda B S hS X⟩ : AlgebraicSpaces B S hS) ⟶
        (⟨yoneda.obj X', isAlgebraicSpace_yoneda B S hS X'⟩ : AlgebraicSpaces B S hS))
      (ObjectProperty.homMk (yoneda.map f) :
        (⟨yoneda.obj X, isAlgebraicSpace_yoneda B S hS X⟩ : AlgebraicSpaces B S hS) ⟶
        (⟨yoneda.obj Y, isAlgebraicSpace_yoneda B S hS Y⟩ : AlgebraicSpaces B S hS))
      (ObjectProperty.homMk (yoneda.map a) :
        (⟨yoneda.obj X', isAlgebraicSpace_yoneda B S hS X'⟩ : AlgebraicSpaces B S hS) ⟶
        (⟨yoneda.obj Y', isAlgebraicSpace_yoneda B S hS Y'⟩ : AlgebraicSpaces B S hS))
      (ObjectProperty.homMk (yoneda.map b) :
        (⟨yoneda.obj Y, isAlgebraicSpace_yoneda B S hS Y⟩ : AlgebraicSpaces B S hS) ⟶
        (⟨yoneda.obj Y', isAlgebraicSpace_yoneda B S hS Y'⟩ : AlgebraicSpaces B S hS))

AlgebraicGeometry.Space.isPushout_algebraicSpaces_of_isThickening_of_isAffineHom', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningAffineUnconditional.lean, line 36.

Stacks 07SY. For a thickening X ⟶ X' and an affine morphism X ⟶ Y of schemes over S, a pushout square of schemes is also a pushout square in the algebraic spaces over S.

theorem isPushout_algebraicSpaces_of_isThickening_of_isAffineHom'
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X X' Y Y' : BigFppfOver B S hS}
    (i : X ⟶ X') (f : X ⟶ Y) (a : X' ⟶ Y') (b : Y ⟶ Y')
    (hi : Stacks.Thickenings.IsThickening ((BigFppfOver.toScheme B S hS).map i))
    [IsAffineHom ((BigFppfOver.toScheme B S hS).map f)]
    (hPushout : IsPushout ((BigFppfOver.toScheme B S hS).map i)
      ((BigFppfOver.toScheme B S hS).map f)
      ((BigFppfOver.toScheme B S hS).map a)
      ((BigFppfOver.toScheme B S hS).map b)) :
    IsPushout
      (ObjectProperty.homMk (yoneda.map i) :
        (⟨yoneda.obj X, isAlgebraicSpace_yoneda B S hS X⟩ : AlgebraicSpaces B S hS) ⟶
        (⟨yoneda.obj X', isAlgebraicSpace_yoneda B S hS X'⟩ : AlgebraicSpaces B S hS))
      (ObjectProperty.homMk (yoneda.map f) :
        (⟨yoneda.obj X, isAlgebraicSpace_yoneda B S hS X⟩ : AlgebraicSpaces B S hS) ⟶
        (⟨yoneda.obj Y, isAlgebraicSpace_yoneda B S hS Y⟩ : AlgebraicSpaces B S hS))
      (ObjectProperty.homMk (yoneda.map a) :
        (⟨yoneda.obj X', isAlgebraicSpace_yoneda B S hS X'⟩ : AlgebraicSpaces B S hS) ⟶
        (⟨yoneda.obj Y', isAlgebraicSpace_yoneda B S hS Y'⟩ : AlgebraicSpaces B S hS))
      (ObjectProperty.homMk (yoneda.map b) :
        (⟨yoneda.obj Y, isAlgebraicSpace_yoneda B S hS Y⟩ : AlgebraicSpaces B S hS) ⟶
        (⟨yoneda.obj Y', isAlgebraicSpace_yoneda B S hS Y'⟩ : AlgebraicSpaces B S hS))

Tag 07VX, a lemma

Tag 07VX in the Stacks Project.

AlgebraicGeometry.Space.exists_hasPushout_isThickeningHom_inr_isPullback_appTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningAffinePushoutTag.lean, line 59.

Stacks 07VX. Let i : X ⟶ X' be a thickening and f : X ⟶ Y an affine morphism of algebraic spaces over S. Then

there is a pushout Y' = Y ⨿_X X' in the category of algebraic spaces over S;

Y ⟶ Y' is a thickening, so Y' is a thickening of Y;

𝒪_{Y'} = 𝒪_Y ×_{f_*𝒪_X} f'_*𝒪_{X'} as sheaves on Y_étale = (Y')_étale, evaluated on each of its objects: for a scheme W étale over Y' with base changes W₁ to X', W₂ to Y and W₀ to X, the ring Γ(W, 𝒪) is the fibre product of Γ(W₂, 𝒪) and Γ(W₁, 𝒪) over Γ(W₀, 𝒪).

The objects of the small étale site of Y' are the schemes étale over Y', and the sections over W of 𝒪_Y, f_*𝒪_X and f'_*𝒪_{X'} are the rings of functions on W₂, W₀ and W₁. Limits of sheaves are computed objectwise, so the objectwise statement (3) is the equality of sheaves of the source.

theorem exists_hasPushout_isThickeningHom_inr_isPullback_appTop
    {X X' Y : AlgebraicSpaces B S hS} (i : X ⟶ X') (f : X ⟶ Y)
    (hi : IsThickeningHom B S hS i) (hf : IsAffineHom B S hS f.hom) :
    ∃ _ : HasPushout i f,
      IsThickeningHom B S hS (pushout.inr i f) ∧
      ∀ {W W₁ W₂ W₀ : BigFppfOver B S hS} (w : yoneda.obj W ⟶ (pushout i f).1)
        (_hwE : IsEtale B S hS w)
        {u₁ : W₁ ⟶ W} {p₁ : yoneda.obj W₁ ⟶ X'.1}
        (_h₁ : IsPullback (yoneda.map u₁) p₁ w (pushout.inl i f).hom)
        {u₂ : W₂ ⟶ W} {p₂ : yoneda.obj W₂ ⟶ Y.1}
        (_h₂ : IsPullback (yoneda.map u₂) p₂ w (pushout.inr i f).hom)
        {iW : W₀ ⟶ W₁} {fW : W₀ ⟶ W₂} {p₀ : yoneda.obj W₀ ⟶ X.1}
        (_h₀₁ : IsPullback (yoneda.map iW) p₀ p₁ i.hom)
        (_h₀₂ : IsPullback (yoneda.map fW) p₀ p₂ f.hom)
        (hw₀ : iW ≫ u₁ = fW ≫ u₂),
        let Φ := BigFppfOver.toScheme B S hS
        IsPullback ((Φ.map u₂).app ⊤) ((Φ.map u₁).app ⊤) ((Φ.map fW).app ((Φ.map u₂) ⁻¹ᵁ ⊤))
          ((Φ.map iW).app ((Φ.map u₁) ⁻¹ᵁ ⊤) ≫ eqToHom (congrArg (fun O ↦ Γ(Φ.obj W₀, O))
            (congrArg (fun k : Φ.obj W₀ ⟶ Φ.obj W ↦ k ⁻¹ᵁ ⊤)
              (show Φ.map iW ≫ Φ.map u₁ = Φ.map fW ≫ Φ.map u₂ by
                rw [← Φ.map_comp, ← Φ.map_comp, hw₀]))))

AlgebraicGeometry.Space.pushout_spec_of_isThickeningHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningAffinePushoutTags.lean, line 66.

[Stacks Project, Tag 07VX]. Let i : X ⟶ X' be a thickening of algebraic spaces over S and f : X ⟶ Y an affine morphism. The pushout Y' = Y ⨿_X X' exists in the category of algebraic spaces over S, the morphism Y ⟶ Y' is a thickening, and 𝒪_{Y'} = 𝒪_Y ×_{f_*𝒪_X} f'_*𝒪_{X'} as sheaves on the small étale site of Y': over every object W ⟶ Y' of that site — indeed over every scheme W flat over Y' — the ring of functions on W is the fibre product of the rings of functions on W ×_{Y'} Y and on W ×_{Y'} X' over the ring of functions on W ×_{Y'} X.

theorem pushout_spec_of_isThickeningHom :
    let hatlas : HasThickeningAffineAtlases B S hS :=
      hasThickeningAffineAtlases_of_chartLift B S hS (hasEtaleChartLifts B S hS)
    HasPushout i f ∧
      (letI := hasPushout_of_isThickening_of_isAffineHom B S hS hatlas i f hi hf
      IsThickeningHom B S hS (pushout.inr i f) ∧
      ∀ {W WX' WY WX : BigFppfOver B S hS} {cX' : WX' ⟶ W} {cY : WY ⟶ W} {jX' : WX ⟶ WX'}
        {jY : WX ⟶ WY} {w : schemeSpace W ⟶ pushout i f} {pX' : schemeSpace WX' ⟶ X'}
        {pY : schemeSpace WY ⟶ Y} {pX : schemeSpace WX ⟶ X}, IsFlat B S hS w.hom →
        IsPullback (schemeSpaceMap cX') pX' w (pushout.inl i f) →
        IsPullback (schemeSpaceMap cY) pY w (pushout.inr i f) →
        IsPullback (schemeSpaceMap jY) pX pY f → schemeSpaceMap jX' ≫ pX' = pX ≫ i →
        jY ≫ cY = jX' ≫ cX' →
        IsPullback (Scheme.Γ.map ((BigFppfOver.toScheme B S hS).map cY).op)
          (Scheme.Γ.map ((BigFppfOver.toScheme B S hS).map cX').op)
          (Scheme.Γ.map ((BigFppfOver.toScheme B S hS).map jY).op)
          (Scheme.Γ.map ((BigFppfOver.toScheme B S hS).map jX').op))

AlgebraicGeometry.Space.hasPushout_of_isThickeningHom_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningAffinePushoutTheorem.lean, line 119. The attribute's comment: “existence of the pushout”.

Stacks 07VX, existence. A thickening i : X ⟶ X' and an affine morphism f : X ⟶ Y of algebraic spaces over S have a pushout Y' = Y ⨿_X X' in the category of algebraic spaces over S.

theorem hasPushout_of_isThickeningHom_of_isAffineHom
    {X X' Y : AlgebraicSpaces B S hS} (i : X ⟶ X') (f : X ⟶ Y)
    (hi : IsThickeningHom B S hS i) (hf : IsAffineHom B S hS f.hom) : HasPushout i f

AlgebraicGeometry.Space.pushout_inr_isThickeningHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningAffinePushoutTheorem.lean, line 126. The attribute's comment: “the pushout is a thickening of Y”.

Stacks 07VX, Y' = Y ⨿_X X' is a thickening of Y.

theorem pushout_inr_isThickeningHom
    {X X' Y : AlgebraicSpaces B S hS} (i : X ⟶ X') (f : X ⟶ Y)
    (hi : IsThickeningHom B S hS i) (hf : IsAffineHom B S hS f.hom) [HasPushout i f] :
    IsThickeningHom B S hS (pushout.inr i f)

AlgebraicGeometry.Space.pushout_isPullback_appTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningAffinePushoutTheorem.lean, line 142. The attribute's comment: “the structure sheaf”.

Stacks 07VX, the structure sheaf. 𝒪_{Y'} = 𝒪_Y ×_{f_*𝒪_X} f'_*𝒪_{X'} as sheaves on the small étale site of Y', evaluated on each of its objects: for a scheme W étale over Y' with base changes W₁ to X', W₂ to Y and W₀ to X, the ring Γ(W, 𝒪) is the fibre product of Γ(W₂, 𝒪) and Γ(W₁, 𝒪) over Γ(W₀, 𝒪).

The objects of the small étale site of Y' are the schemes étale over Y', and the sections over W of 𝒪_Y, f_*𝒪_X and f'_*𝒪_{X'} are the rings of functions on W₂, W₀ and W₁. Limits of sheaves are computed objectwise, so this objectwise statement is the same as the equality of sheaves of the source.

theorem pushout_isPullback_appTop
    {X X' Y : AlgebraicSpaces B S hS} (i : X ⟶ X') (f : X ⟶ Y)
    (hi : IsThickeningHom B S hS i) (hf : IsAffineHom B S hS f.hom) [HasPushout i f]
    {W W₁ W₂ W₀ : BigFppfOver B S hS} (w : yoneda.obj W ⟶ (pushout i f).1)
    (hwE : IsEtale B S hS w)
    {u₁ : W₁ ⟶ W} {p₁ : yoneda.obj W₁ ⟶ X'.1}
    (h₁ : IsPullback (yoneda.map u₁) p₁ w (pushout.inl i f).hom)
    {u₂ : W₂ ⟶ W} {p₂ : yoneda.obj W₂ ⟶ Y.1}
    (h₂ : IsPullback (yoneda.map u₂) p₂ w (pushout.inr i f).hom)
    {iW : W₀ ⟶ W₁} {fW : W₀ ⟶ W₂} {p₀ : yoneda.obj W₀ ⟶ X.1}
    (h₀₁ : IsPullback (yoneda.map iW) p₀ p₁ i.hom) (h₀₂ : IsPullback (yoneda.map fW) p₀ p₂ f.hom)
    (hw₀ : iW ≫ u₁ = fW ≫ u₂) :
    let Φ := BigFppfOver.toScheme B S hS
    IsPullback ((Φ.map u₂).app ⊤) ((Φ.map u₁).app ⊤) ((Φ.map fW).app ((Φ.map u₂) ⁻¹ᵁ ⊤))
      ((Φ.map iW).app ((Φ.map u₁) ⁻¹ᵁ ⊤) ≫ eqToHom (congrArg (fun O ↦ Γ(Φ.obj W₀, O))
        (congrArg (fun k : Φ.obj W₀ ⟶ Φ.obj W ↦ k ⁻¹ᵁ ⊤)
          (show Φ.map iW ≫ Φ.map u₁ = Φ.map fW ≫ Φ.map u₂ by
            rw [← Φ.map_comp, ← Φ.map_comp, hw₀]))))

Tag 07VY, a lemma

Tag 07VY in the Stacks Project.

AlgebraicGeometry.Space.pushoutGluing_spec_of_isThickeningHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningAffinePushoutTags.lean, line 91.

[Stacks Project, Tag 07VY]. Let i : X ⟶ X' be a thickening of algebraic spaces over S, f : X ⟶ Y an affine morphism and Y' = Y ⨿_X X'. The base-change functor F : V' ↦ (V' ×_{Y'} Y, V' ×_{Y'} X', 1) sends schemes over Y' to pairs of schemes; it has the left adjoint G, which sends a triple (V, U', φ) to the pushout V ⨿_{V ×_Y X} U' with its structure morphism to Y'; and G sends pairs of schemes to schemes.

theorem pushoutGluing_spec_of_isThickeningHom :
    let hatlas : HasThickeningAffineAtlases B S hS :=
      hasThickeningAffineAtlases_of_chartLift B S hS (hasEtaleChartLifts B S hS)
    letI := hasPushout_of_isThickening_of_isAffineHom B S hS hatlas i f hi hf
    (∀ Z : Over (pushout i f), Z.left.1.IsRepresentable →
        ((pushoutBaseChangeFunctor B S hS hatlas i f hi hf).obj Z).obj.left.left.1.IsRepresentable ∧
        ((pushoutBaseChangeFunctor B S hS hatlas i f hi hf).obj
          Z).obj.right.left.1.IsRepresentable) ∧
      Nonempty (pushoutGluingFunctor B S hS hatlas i f hi hf ⊣
        pushoutBaseChangeFunctor B S hS hatlas i f hi hf) ∧
      (∀ T : pushoutGluingData B S hS i f,
        ∃ (v : T.obj.left.left ⟶ ((pushoutGluingFunctor B S hS hatlas i f hi hf).obj T).left)
          (u' : T.obj.right.left ⟶ ((pushoutGluingFunctor B S hS hatlas i f hi hf).obj T).left),
          IsPushout (CategoryTheory.PushoutGluing.sourceMap i f T)
              (pullback.fst T.obj.right.hom i) v u' ∧
            v ≫ ((pushoutGluingFunctor B S hS hatlas i f hi hf).obj T).hom =
              T.obj.left.hom ≫ pushout.inr i f ∧
            u' ≫ ((pushoutGluingFunctor B S hS hatlas i f hi hf).obj T).hom =
              T.obj.right.hom ≫ pushout.inl i f) ∧
      (∀ T : pushoutGluingData B S hS i f, T.obj.left.left.1.IsRepresentable →
        T.obj.right.left.1.IsRepresentable →
        ((pushoutGluingFunctor B S hS hatlas i f hi hf).obj T).left.1.IsRepresentable)

Tag 07VZ, a lemma

Tag 07VZ in the Stacks Project.

AlgebraicGeometry.Space.isPullback_right_of_isPullback_of_surjective_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/CartesianSquareDescent.lean, line 157.

Stacks 07VZ. Let S be a scheme and let A, B, C, D, E, F be algebraic spaces over S sitting in a commutative diagram with rows A ⟶ C ⟶ E and B ⟶ D ⟶ F and vertical maps A ⟶ B, C ⟶ D, E ⟶ F. If the square A, B, C, D and the outer rectangle A, B, E, F are cartesian and B ⟶ D is surjective and étale, then the square C, D, E, F is cartesian.

theorem isPullback_right_of_isPullback_of_surjective_etale
    (_hA : IsAlgebraicSpace B₀ S hS A) (hB : IsAlgebraicSpace B₀ S hS B)
    (hC : IsAlgebraicSpace B₀ S hS C) (hD : IsAlgebraicSpace B₀ S hS D)
    (hE : IsAlgebraicSpace B₀ S hS E) (_hF : IsAlgebraicSpace B₀ S hS F)
    (hcomm : cE ≫ eF = cD ≫ dF)
    (hleft : IsPullback aC aB cD bD)
    (houter : IsPullback (aC ≫ cE) aB eF (bD ≫ dF))
    (hsurj : IsSurjective B₀ S hS bD) (hetale : IsEtale B₀ S hS bD) :
    IsPullback cE cD eF dF

Tag 07W0, a lemma

Tag 07W0 in the Stacks Project.

AlgebraicGeometry.Space.isIso_pushoutGluingAdjunction_unit_of_isThickeningHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningAffinePushoutTags.lean, line 165.

[Stacks Project, Tag 07W0]. Let i : X ⟶ X' be a thickening of algebraic spaces over S, f : X ⟶ Y an affine morphism, Y' = Y ⨿_X X', and let G ⊣ F be the gluing adjunction of [Stacks Project, Tag 07VY], with F : V' ↦ (V' ×_{Y'} Y, V' ×_{Y'} X', 1) and G sending a triple (V, U', φ) to V ⨿_{V ×_Y X} U'. Then F ∘ G is isomorphic to the identity functor of the category of triples; indeed the unit 𝟭 ⟶ G ⋙ F of the adjunction is an isomorphism.

theorem isIso_pushoutGluingAdjunction_unit_of_isThickeningHom :
    let hatlas : HasThickeningAffineAtlases B S hS :=
      hasThickeningAffineAtlases_of_chartLift B S hS (hasEtaleChartLifts B S hS)
    letI := hasPushout_of_isThickening_of_isAffineHom B S hS hatlas i f hi hf
    IsIso (pushoutGluingAdjunction B S hS hatlas i f hi hf).unit ∧
      Nonempty (pushoutGluingFunctor B S hS hatlas i f hi hf ⋙
          pushoutBaseChangeFunctor B S hS hatlas i f hi hf ≅
        𝟭 (pushoutGluingData B S hS i f))

Tag 07W1, an equation

Tag 07W1 in the Stacks Project.

AlgebraicGeometry.Space.exists_etaleChartCube, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningAffinePushoutTags.lean, line 190.

[Stacks Project, Tag 07W1], equation 81.6.5.1 of the proof of Stacks 07W0. Let i : X ⟶ X' be a thickening of algebraic spaces over S and f : X ⟶ Y an affine morphism. There is a cube whose back square is the pushout Y' = Y ⨿_X X' of algebraic spaces and whose front square is the pushout P = V ⨿_U U' of étale scheme charts, with U ⟶ U' a thickening and U ⟶ V affine, whose four lateral squares are cartesian and whose four northeast arrows are surjective and étale.

theorem exists_etaleChartCube
    {X X' Y : AlgebraicSpaces B S hS} (i : X ⟶ X') (f : X ⟶ Y)
    (hi : IsThickeningHom B S hS i) (hf : IsAffineHom B S hS f.hom) :
    ∃ (U U' V P : BigFppfOver B S hS) (Y' : AlgebraicSpaces B S hS)
      (aY : X' ⟶ Y') (bY : Y ⟶ Y') (k : U ⟶ U') (g : U ⟶ V) (aP : U' ⟶ P) (bP : V ⟶ P)
      (p : yoneda.obj U ⟶ X.1) (p' : yoneda.obj U' ⟶ X'.1) (q : yoneda.obj V ⟶ Y.1)
      (r : yoneda.obj P ⟶ Y'.1),
      IsPushout i f aY bY ∧
      IsPushout ((BigFppfOver.toScheme B S hS).map k) ((BigFppfOver.toScheme B S hS).map g)
        ((BigFppfOver.toScheme B S hS).map aP) ((BigFppfOver.toScheme B S hS).map bP) ∧
      Stacks.Thickenings.IsThickening ((BigFppfOver.toScheme B S hS).map k) ∧
      _root_.AlgebraicGeometry.IsAffineHom ((BigFppfOver.toScheme B S hS).map g) ∧
      IsPullback (yoneda.map k) p p' i.hom ∧
      IsPullback p (yoneda.map g) f.hom q ∧
      IsPullback (yoneda.map aP) p' r aY.hom ∧
      IsPullback (yoneda.map bP) q r bY.hom ∧
      IsSurjective B S hS p ∧ IsEtale B S hS p ∧
      IsSurjective B S hS p' ∧ IsEtale B S hS p' ∧
      IsSurjective B S hS q ∧ IsEtale B S hS q ∧
      IsSurjective B S hS r ∧ IsEtale B S hS r

Tag 07W2, an equation

Tag 07W2 in the Stacks Project.

AlgebraicGeometry.Space.exists_etaleChartCube_gluingData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningAffinePushoutTags.lean, line 221.

[Stacks Project, Tag 07W2], equation 81.6.5.2 of the proof of Stacks 07W0. Let i : X ⟶ X' be a thickening of algebraic spaces over S, f : X ⟶ Y an affine morphism and (V, U', φ) a triple over the span. There is a cube over the span U' ⟵ U ⟶ V of the triple whose back square is the pushout G(V, U', φ) = V ⨿_U U' of algebraic spaces and whose front square is the pushout G₁ = V₁ ⨿_{U₁} U₁' of étale scheme charts, whose four lateral squares are cartesian and whose four northeast arrows are surjective and étale; in particular G₁ ⟶ G(V, U', φ) is surjective étale.

theorem exists_etaleChartCube_gluingData
    {X X' Y : AlgebraicSpaces B S hS} (i : X ⟶ X') (f : X ⟶ Y)
    (hi : IsThickeningHom B S hS i) (hf : IsAffineHom B S hS f.hom)
    (T : pushoutGluingData B S hS i f) :
    ∃ (U₁ U₁' V₁ G₁ : BigFppfOver B S hS) (G : AlgebraicSpaces B S hS)
      (aG : T.obj.right.left ⟶ G) (bG : T.obj.left.left ⟶ G) (k : U₁ ⟶ U₁') (g : U₁ ⟶ V₁)
      (aG₁ : U₁' ⟶ G₁) (bG₁ : V₁ ⟶ G₁)
      (p : yoneda.obj U₁ ⟶ (pullback T.obj.right.hom i).1)
      (p' : yoneda.obj U₁' ⟶ T.obj.right.left.1)
      (q : yoneda.obj V₁ ⟶ T.obj.left.left.1) (r : yoneda.obj G₁ ⟶ G.1),
      IsPushout (pullback.fst T.obj.right.hom i)
        (CategoryTheory.PushoutGluing.sourceMap i f T) aG bG ∧
      IsPushout ((BigFppfOver.toScheme B S hS).map k) ((BigFppfOver.toScheme B S hS).map g)
        ((BigFppfOver.toScheme B S hS).map aG₁) ((BigFppfOver.toScheme B S hS).map bG₁) ∧
      Stacks.Thickenings.IsThickening ((BigFppfOver.toScheme B S hS).map k) ∧
      _root_.AlgebraicGeometry.IsAffineHom ((BigFppfOver.toScheme B S hS).map g) ∧
      IsPullback (yoneda.map k) p p' (pullback.fst T.obj.right.hom i).hom ∧
      IsPullback p (yoneda.map g)
        (CategoryTheory.PushoutGluing.sourceMap i f T).hom q ∧
      IsPullback (yoneda.map aG₁) p' r aG.hom ∧
      IsPullback (yoneda.map bG₁) q r bG.hom ∧
      IsSurjective B S hS p ∧ IsEtale B S hS p ∧
      IsSurjective B S hS p' ∧ IsEtale B S hS p' ∧
      IsSurjective B S hS q ∧ IsEtale B S hS q ∧
      IsSurjective B S hS r ∧ IsEtale B S hS r

Tag 08KV, a lemma

Tag 08KV in the Stacks Project.

AlgebraicGeometry.Space.PushoutModules.isFiniteType_iff_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningPushoutFiniteModules.lean, line 179. The attribute's comment: “(a)”.

Stacks Project, Tag 08KV (a). Let i : X ⟶ X' be a thickening and f : X ⟶ Y an affine morphism of algebraic spaces over S, let Y' = Y ⨿_X X' be their pushout (Stacks 07VX) and g : V' ⟶ Y' a morphism, with V = Y ×_{Y'} V' and U' = X' ×_{Y'} V'. If a quasi-coherent 𝒪_{V'}-module 𝒢' flat over Y' corresponds to the triple (𝒢, ℱ', φ) under the equivalence AlgebraicGeometry.Space.PushoutModules.isEquivalence_flatRestrictionFunctor, so that 𝒢 = (V ⟶ V')^*𝒢' and ℱ' = (U' ⟶ V')^*𝒢', then 𝒢' is of finite type if and only if 𝒢 and ℱ' are of finite type.

theorem isFiniteType_iff_restrict :
    letI := hasPushout_of_isThickeningHom_of_isAffineHom B S hS i f hi hf
    ∀ {V' : AlgebraicSpaces B S hS} (g : V' ⟶ pushout i f)
      (M : (FlatQuasicoherentOver g).FullSubcategory),
      M.obj.IsFiniteType ↔
        (((FlatQuasicoherentTriple i f g).lift ((FlatQuasicoherentOver g).ι ⋙
          (TripleGluing.restrictFunctor (squareOverlap (commonToTarget i f g)
            (targetRestriction i f g) (commonToAmbient i f g) (ambientRestriction i f g)
            (commonToAmbient_comp_eq i f g))))
          fun M => flatQuasicoherentTriple_restrict i f g M.obj
            M.property).obj M).obj.target.IsFiniteType ∧
        (((FlatQuasicoherentTriple i f g).lift ((FlatQuasicoherentOver g).ι ⋙
          (TripleGluing.restrictFunctor (squareOverlap (commonToTarget i f g)
            (targetRestriction i f g) (commonToAmbient i f g) (ambientRestriction i f g)
            (commonToAmbient_comp_eq i f g))))
          fun M => flatQuasicoherentTriple_restrict i f g M.obj
            M.property).obj M).obj.ambient.IsFiniteType

AlgebraicGeometry.Space.PushoutModules.isFinitePresentationOnSite_iff_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningPushoutFiniteModules.lean, line 309. The attribute's comment: “(b)”.

Stacks Project, Tag 08KV (b). Let i : X ⟶ X' be a thickening and f : X ⟶ Y an affine morphism of algebraic spaces over S, let Y' = Y ⨿_X X' be their pushout (Stacks 07VX) and g : V' ⟶ Y' a morphism locally of finite presentation, with V = Y ×_{Y'} V' and U' = X' ×_{Y'} V'. If a quasi-coherent 𝒪_{V'}-module 𝒢' flat over Y' corresponds to the triple (𝒢, ℱ', φ) under the equivalence AlgebraicGeometry.Space.PushoutModules.isEquivalence_flatRestrictionFunctor, so that 𝒢 = (V ⟶ V')^*𝒢' and ℱ' = (U' ⟶ V')^*𝒢', then 𝒢' is of finite presentation if and only if 𝒢 and ℱ' are of finite presentation (Stacks 03DL (7), SheafOfModules.IsFinitePresentationOnSite).

theorem isFinitePresentationOnSite_iff_restrict :
    letI := hasPushout_of_isThickeningHom_of_isAffineHom B S hS i f hi hf
    ∀ {V' : AlgebraicSpaces B S hS} (g : V' ⟶ pushout i f),
      IsLocallyOfFinitePresentation B S hS g.hom →
      ∀ M : (FlatQuasicoherentOver g).FullSubcategory,
      (SheafOfModules.IsFinitePresentationOnSite M.obj ↔
        SheafOfModules.IsFinitePresentationOnSite
          (((FlatQuasicoherentTriple i f g).lift ((FlatQuasicoherentOver g).ι ⋙
            (TripleGluing.restrictFunctor (squareOverlap (commonToTarget i f g)
              (targetRestriction i f g) (commonToAmbient i f g) (ambientRestriction i f g)
              (commonToAmbient_comp_eq i f g))))
            fun M => flatQuasicoherentTriple_restrict i f g M.obj M.property).obj M).obj.target ∧
        SheafOfModules.IsFinitePresentationOnSite
          (((FlatQuasicoherentTriple i f g).lift ((FlatQuasicoherentOver g).ι ⋙
            (TripleGluing.restrictFunctor (squareOverlap (commonToTarget i f g)
              (targetRestriction i f g) (commonToAmbient i f g) (ambientRestriction i f g)
              (commonToAmbient_comp_eq i f g))))
            fun M => flatQuasicoherentTriple_restrict i f g M.obj
              M.property).obj M).obj.ambient)

AlgebraicGeometry.Space.PushoutModules.isEquivalence_flatRestrictionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningPushoutFlatModules.lean, line 357. The attribute's comment: “the equivalence”.

Stacks Project, Tag 08KV, the equivalence. Let i : X ⟶ X' be a thickening and f : X ⟶ Y an affine morphism of algebraic spaces over S, let Y' = Y ⨿_X X' be their pushout (Stacks 07VX) and let g : V' ⟶ Y' be a morphism, with V = Y ×_{Y'} V', U' = X' ×_{Y'} V' and U = X ×_{Y'} V'. The functor 𝒢' ↦ ((V ⟶ V')^*𝒢', (U' ⟶ V')^*𝒢', can) is an equivalence of categories from the quasi-coherent 𝒪_{V'}-modules flat over Y' onto the triples (𝒢, ℱ', φ) of a quasi-coherent 𝒪_V-module 𝒢 flat over Y, a quasi-coherent 𝒪_{U'}-module ℱ' flat over X' and an isomorphism φ : (U ⟶ V)^*𝒢 ≅ (U ⟶ U')^*ℱ'.

The source writes "ℱ' … flat over X": ℱ' lives on U' = X' ×_{Y'} V', which lies over X', so the condition is flatness over X', as in the scheme case Stacks 08KU. The pushout is not assumed: it exists by Stacks 07VX (AlgebraicGeometry.Space.hasPushout_of_isThickeningHom_of_isAffineHom), which is the instance the statement binds. The functor is written out as the lift to the two full subcategories of CategoryTheory.TripleGluing.restrictFunctor at the canonical comparison AlgebraicGeometry.Space.PushoutModules.squareOverlap; a quasi-inverse is the gluing functor (𝒢, ℱ', φ) ↦ (V ⟶ V')_*𝒢 ×_{(U ⟶ V')_*ℱ} (U' ⟶ V')_*ℱ' (isEquivalence_flatRestrictionFunctor_of_hasPushout).

theorem isEquivalence_flatRestrictionFunctor :
    letI := hasPushout_of_isThickeningHom_of_isAffineHom B S hS i f hi hf
    ∀ {V' : AlgebraicSpaces B S hS} (g : V' ⟶ pushout i f),
      ((((FlatQuasicoherentTriple i f g).lift ((FlatQuasicoherentOver g).ι ⋙
      (TripleGluing.restrictFunctor (squareOverlap (commonToTarget i f g) (targetRestriction i f g)
      (commonToAmbient i f g) (ambientRestriction i f g) (commonToAmbient_comp_eq i f g))))
        fun M => flatQuasicoherentTriple_restrict i f g M.obj M.property) :
        (FlatQuasicoherentOver g).FullSubcategory ⥤
        (FlatQuasicoherentTriple i f g).FullSubcategory)).IsEquivalence

AlgebraicGeometry.Space.PushoutModules.isEquivalence_flatRestrictionFunctor_and_finiteness_iff_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningPushoutModulesTag.lean, line 77.

Let i : X ⟶ X' be a thickening and f : X ⟶ Y an affine morphism of algebraic spaces over S, let Y' = Y ⨿_X X' be their pushout (Stacks 07VX) and let g : V' ⟶ Y' be a morphism, with V = Y ×_{Y'} V', U' = X' ×_{Y'} V' and U = X ×_{Y'} V'.

The functor 𝒢' ↦ ((V ⟶ V')^*𝒢', (U' ⟶ V')^*𝒢', can) is an equivalence of categories from the quasi-coherent 𝒪_{V'}-modules flat over Y' onto the triples (𝒢, ℱ', φ) of a quasi-coherent 𝒪_V-module 𝒢 flat over Y, a quasi-coherent 𝒪_{U'}-module ℱ' flat over X' and an isomorphism φ : (U ⟶ V)^*𝒢 ≅ (U ⟶ U')^*ℱ'.

Suppose 𝒢' corresponds to the triple (𝒢, ℱ', φ), so that 𝒢 = (V ⟶ V')^*𝒢' and ℱ' = (U' ⟶ V')^*𝒢'. Then (a) 𝒢' is of finite type if and only if 𝒢 and ℱ' are of finite type; (b) if g is locally of finite presentation, then 𝒢' is of finite presentation if and only if 𝒢 and ℱ' are of finite presentation (Stacks 03DL (7), SheafOfModules.IsFinitePresentationOnSite).

The source writes "ℱ' … flat over X": ℱ' lives on U' = X' ×_{Y'} V', which lies over X', so the condition is flatness over X', as in the scheme case Stacks 08KU. The pushout is not assumed: it exists by Stacks 07VX (AlgebraicGeometry.Space.hasPushout_of_isThickeningHom_of_isAffineHom), which is the instance the statement binds. The functor is written out as the lift to the two full subcategories of CategoryTheory.TripleGluing.restrictFunctor at the canonical comparison AlgebraicGeometry.Space.PushoutModules.squareOverlap; a quasi-inverse is the gluing functor (𝒢, ℱ', φ) ↦ (V ⟶ V')_*𝒢 ×_{(U ⟶ V')_*ℱ} (U' ⟶ V')_*ℱ' (isEquivalence_flatRestrictionFunctor_of_hasPushout).

theorem isEquivalence_flatRestrictionFunctor_and_finiteness_iff_restrict :
    letI := hasPushout_of_isThickeningHom_of_isAffineHom B S hS i f hi hf
    ∀ {V' : AlgebraicSpaces B S hS} (g : V' ⟶ pushout i f),
      ((((FlatQuasicoherentTriple i f g).lift ((FlatQuasicoherentOver g).ι ⋙
          (TripleGluing.restrictFunctor (squareOverlap (commonToTarget i f g)
            (targetRestriction i f g) (commonToAmbient i f g) (ambientRestriction i f g)
            (commonToAmbient_comp_eq i f g))))
        fun M => flatQuasicoherentTriple_restrict i f g M.obj M.property) :
        (FlatQuasicoherentOver g).FullSubcategory ⥤
          (FlatQuasicoherentTriple i f g).FullSubcategory)).IsEquivalence ∧
      (∀ (M : (FlatQuasicoherentOver g).FullSubcategory),
        M.obj.IsFiniteType ↔
          (((FlatQuasicoherentTriple i f g).lift ((FlatQuasicoherentOver g).ι ⋙
            (TripleGluing.restrictFunctor (squareOverlap (commonToTarget i f g)
              (targetRestriction i f g) (commonToAmbient i f g) (ambientRestriction i f g)
              (commonToAmbient_comp_eq i f g))))
            fun M => flatQuasicoherentTriple_restrict i f g M.obj
              M.property).obj M).obj.target.IsFiniteType ∧
          (((FlatQuasicoherentTriple i f g).lift ((FlatQuasicoherentOver g).ι ⋙
            (TripleGluing.restrictFunctor (squareOverlap (commonToTarget i f g)
              (targetRestriction i f g) (commonToAmbient i f g) (ambientRestriction i f g)
              (commonToAmbient_comp_eq i f g))))
            fun M => flatQuasicoherentTriple_restrict i f g M.obj
              M.property).obj M).obj.ambient.IsFiniteType) ∧
      (IsLocallyOfFinitePresentation B S hS g.hom →
        ∀ M : (FlatQuasicoherentOver g).FullSubcategory,
        (SheafOfModules.IsFinitePresentationOnSite M.obj ↔
          SheafOfModules.IsFinitePresentationOnSite
            (((FlatQuasicoherentTriple i f g).lift ((FlatQuasicoherentOver g).ι ⋙
              (TripleGluing.restrictFunctor (squareOverlap (commonToTarget i f g)
                (targetRestriction i f g) (commonToAmbient i f g) (ambientRestriction i f g)
                (commonToAmbient_comp_eq i f g))))
              fun M => flatQuasicoherentTriple_restrict i f g M.obj M.property).obj M).obj.target ∧
          SheafOfModules.IsFinitePresentationOnSite
            (((FlatQuasicoherentTriple i f g).lift ((FlatQuasicoherentOver g).ι ⋙
              (TripleGluing.restrictFunctor (squareOverlap (commonToTarget i f g)
                (targetRestriction i f g) (commonToAmbient i f g) (ambientRestriction i f g)
                (commonToAmbient_comp_eq i f g))))
              fun M => flatQuasicoherentTriple_restrict i f g M.obj
                M.property).obj M).obj.ambient))

Tag 07W3, a lemma

Tag 07W3 in the Stacks Project.

AlgebraicGeometry.Space.pushoutGluing_flat_of_isThickeningHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ThickeningAffinePushoutTags.lean, line 125.

[Stacks Project, Tag 07W3]. Let i : X ⟶ X' be a thickening of algebraic spaces over S, f : X ⟶ Y an affine morphism, Y' = Y ⨿_X X' and G ⊣ F the gluing adjunction of [Stacks Project, Tag 07VY]. For a triple (V, U', φ), the glued space G(V, U', φ) ⟶ Y' is (1) locally of finite type, (2) flat, (3) flat and locally of finite presentation, (4) smooth, (5) étale, if and only if both V ⟶ Y and U' ⟶ X' are. If W' is flat over Y' the counit G(F(W')) ⟶ W' is an isomorphism; the unit is an isomorphism; F sends spaces flat over Y' to flat triples and G sends flat triples to spaces flat over Y'; so F and G are mutually quasi-inverse between the spaces flat over Y' and the triples with V ⟶ Y and U' ⟶ X' flat.

theorem pushoutGluing_flat_of_isThickeningHom :
    let hatlas : HasThickeningAffineAtlases B S hS :=
      hasThickeningAffineAtlases_of_chartLift B S hS (hasEtaleChartLifts B S hS)
    letI := hasPushout_of_isThickening_of_isAffineHom B S hS hatlas i f hi hf
    (∀ T : pushoutGluingData B S hS i f,
      (IsLocallyOfFiniteType B S hS
          ((pushoutGluingFunctor B S hS hatlas i f hi hf).obj T).hom.hom ↔
        IsLocallyOfFiniteType B S hS T.obj.left.hom.hom ∧
          IsLocallyOfFiniteType B S hS T.obj.right.hom.hom) ∧
      (IsFlat B S hS ((pushoutGluingFunctor B S hS hatlas i f hi hf).obj T).hom.hom ↔
        IsFlat B S hS T.obj.left.hom.hom ∧ IsFlat B S hS T.obj.right.hom.hom) ∧
      ((IsFlat B S hS ((pushoutGluingFunctor B S hS hatlas i f hi hf).obj T).hom.hom ∧
          IsLocallyOfFinitePresentation B S hS
            ((pushoutGluingFunctor B S hS hatlas i f hi hf).obj T).hom.hom) ↔
        ((IsFlat B S hS T.obj.left.hom.hom ∧
            IsLocallyOfFinitePresentation B S hS T.obj.left.hom.hom) ∧
          (IsFlat B S hS T.obj.right.hom.hom ∧
            IsLocallyOfFinitePresentation B S hS T.obj.right.hom.hom))) ∧
      (IsSmooth B S hS ((pushoutGluingFunctor B S hS hatlas i f hi hf).obj T).hom.hom ↔
        IsSmooth B S hS T.obj.left.hom.hom ∧ IsSmooth B S hS T.obj.right.hom.hom) ∧
      (IsEtale B S hS ((pushoutGluingFunctor B S hS hatlas i f hi hf).obj T).hom.hom ↔
        IsEtale B S hS T.obj.left.hom.hom ∧ IsEtale B S hS T.obj.right.hom.hom)) ∧
    (∀ Z : Over (pushout i f), IsFlat B S hS Z.hom.hom →
      IsIso ((pushoutGluingAdjunction B S hS hatlas i f hi hf).counit.app Z)) ∧
    IsIso (pushoutGluingAdjunction B S hS hatlas i f hi hf).unit ∧
    (∀ Z : Over (pushout i f), IsFlat B S hS Z.hom.hom →
      IsFlat B S hS ((pushoutBaseChangeFunctor B S hS hatlas i f hi hf).obj Z).obj.left.hom.hom ∧
        IsFlat B S hS
          ((pushoutBaseChangeFunctor B S hS hatlas i f hi hf).obj Z).obj.right.hom.hom) ∧
    (∀ T : pushoutGluingData B S hS i f,
      IsFlat B S hS T.obj.left.hom.hom → IsFlat B S hS T.obj.right.hom.hom →
        IsFlat B S hS ((pushoutGluingFunctor B S hS hatlas i f hi hf).obj T).hom.hom)

Sources

Section81.7 Pushouts along closed immersions and integral morphisms #

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

Tag 0EDP, a lemma

Tag 0EDP in the Stacks Project.

AlgebraicGeometry.Space.pushout_isPushout_algebraicSpaces, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/Schemes.lean, line 651.

Stacks 0EDP. In the standing situation of [Stacks Project, Tag 0ECI], the scheme pushout Y ⨿_Z X of [Stacks Project, Tag 0E25] is also a pushout in the category of algebraic spaces over S: the square formed by the four schemes and the four canonical morphisms, regarded through the Yoneda embedding as a square of algebraic spaces over S, is a pushout square.

theorem pushout_isPushout_algebraicSpaces :
    IsPushout
      (ObjectProperty.homMk (yoneda.map (fppfOverI s B hS hX hZ)) :
        (⟨yoneda.obj (fppfOverZ s B hS hZ),
          isAlgebraicSpace_yoneda B s.S hS (fppfOverZ s B hS hZ)⟩ :
          AlgebraicSpaces B s.S hS) ⟶
        (⟨yoneda.obj (fppfOverX s B hS hX),
          isAlgebraicSpace_yoneda B s.S hS (fppfOverX s B hS hX)⟩ :
          AlgebraicSpaces B s.S hS))
      (ObjectProperty.homMk (yoneda.map (fppfOverJ s B hS hY hZ)) :
        (⟨yoneda.obj (fppfOverZ s B hS hZ),
          isAlgebraicSpace_yoneda B s.S hS (fppfOverZ s B hS hZ)⟩ :
          AlgebraicSpaces B s.S hS) ⟶
        (⟨yoneda.obj (fppfOverY s B hS hY),
          isAlgebraicSpace_yoneda B s.S hS (fppfOverY s B hS hY)⟩ :
          AlgebraicSpaces B s.S hS))
      (ObjectProperty.homMk (yoneda.map (fppfOverInl s B hS hX hP)) :
        (⟨yoneda.obj (fppfOverX s B hS hX),
          isAlgebraicSpace_yoneda B s.S hS (fppfOverX s B hS hX)⟩ :
          AlgebraicSpaces B s.S hS) ⟶
        (⟨yoneda.obj (fppfOverPushout s B hS hP),
          isAlgebraicSpace_yoneda B s.S hS (fppfOverPushout s B hS hP)⟩ :
          AlgebraicSpaces B s.S hS))
      (ObjectProperty.homMk (yoneda.map (fppfOverInr s B hS hY hP)) :
        (⟨yoneda.obj (fppfOverY s B hS hY),
          isAlgebraicSpace_yoneda B s.S hS (fppfOverY s B hS hY)⟩ :
          AlgebraicSpaces B s.S hS) ⟶
        (⟨yoneda.obj (fppfOverPushout s B hS hP),
          isAlgebraicSpace_yoneda B s.S hS (fppfOverPushout s B hS hP)⟩ :
          AlgebraicSpaces B s.S hS))

Sources

LeanAlgebraicGeometry.Space.pushout_isPushout_algebraicSpaces

Section81.8 Pushouts and derived categories #

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

Tag 0DL7, a lemma

Tag 0DL7 in the Stacks Project.

AlgebraicGeometry.Space.derivedPushoutEssentialImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/DerivedPushoutGlueingRepresentedAffine.lean, line 567.

Stacks 0DL7. Let S be a scheme and let
X  --i-->  X'
|          |
f          f'
v          v
Y  --j-->  Y'
be a pushout in the category of algebraic spaces over S as in Stacks 07VX, with i a thickening and f affine. Then the essential image of the functor D(𝒪_{Y'}) ⥤ D(𝒪_Y) ×_{D(𝒪_X)} D(𝒪_{X'}), M' ↦ (Lj^* M', L(f')^* M', can), given by derived pullback, contains every triple (M, K', α) with M ∈ D(𝒪_Y) and K' ∈ D(𝒪_{X'}) pseudo-coherent: for every isomorphism α : Lf^* M ≅ Li^* K' there are M' ∈ D(𝒪_{Y'}) and isomorphisms a : Lj^* M' ≅ M and b : L(f')^* M' ≅ K' with Li^* b equal to α ∘ Lf^* a through the 2-cell Lf^* Lj^* ≅ Li^* L(f')^* (Stacks 0D6D). This holds at any models of the four derived categories; the statement is AlgebraicGeometry.Space.DerivedPushoutEssentialImage.

The proof is the source's: the fibre M' of the glueing map Rj_* M ⊕ Rf'_* K' ⟶ Rj_* Rf_* Li^* K' (AlgebraicGeometry.Space.derivedPushoutEssentialImage_of_derivedPushoutGlueingIsIso), the isomorphism step checked on the affine étale charts of Y' (AlgebraicGeometry.Space.derivedPushoutGlueingIsIso_of_onAffineChart), where the base change of the square is a represented affine square whose rings form a fibre product along a surjection with nil kernel (AlgebraicGeometry.Space.derivedPushoutEssentialImage_of_representedAffine), and on which the step is the ring-level statement (MilnorPatching.isIso_homEquiv_symm_of_isPullback_of_distinguished_glueingMap_derivedExtension) carried to the algebraic spaces along the derived associated-module functors (AlgebraicGeometry.Space.pushoutGlueingIsIsoStepOnRepresentedAffine).

theorem derivedPushoutEssentialImage :
    DerivedPushoutEssentialImage.{w₁, w₂, w₃, w₄, u} B S hS

Sources

LeanAlgebraicGeometry.Space.derivedPushoutEssentialImage

Section81.9 Constructing elementary distinguished squares #

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

Tag 0DVI, a lemma

Tag 0DVI in the Stacks Project.

AlgebraicGeometry.Space.isPushout_elementaryDistinguishedSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ElementaryDistinguishedSquarePushout.lean, line 340.

Stacks 0DVI. An elementary distinguished square is a pushout square in the category of algebraic spaces over the base scheme: the target is glued from the open subspace and the étale morphism along their fibre product.

theorem isPushout_elementaryDistinguishedSquare
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {W V : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hW : IsAlgebraicSpace B S hS W) (U : Subfunctor W) (f : V ⟶ W)
    (h : IsElementaryDistinguishedSquare B S hS hW U f) :
    IsPushout
      (ObjectProperty.homMk (pullback.snd U.ι f) :
        AlgebraicSpaces.fiberProduct B S hS
            (ObjectProperty.homMk U.ι :
              (⟨U.toFunctor, h.isOpenSubspace.1⟩ : AlgebraicSpaces B S hS) ⟶ ⟨W, hW⟩)
            (ObjectProperty.homMk f :
              (⟨V, h.isAlgebraicSpace⟩ : AlgebraicSpaces B S hS) ⟶ ⟨W, hW⟩) ⟶
          ⟨V, h.isAlgebraicSpace⟩)
      (ObjectProperty.homMk (pullback.fst U.ι f) :
        _ ⟶ (⟨U.toFunctor, h.isOpenSubspace.1⟩ : AlgebraicSpaces B S hS))
      (ObjectProperty.homMk f :
        (⟨V, h.isAlgebraicSpace⟩ : AlgebraicSpaces B S hS) ⟶ ⟨W, hW⟩)
      (ObjectProperty.homMk U.ι :
        (⟨U.toFunctor, h.isOpenSubspace.1⟩ : AlgebraicSpaces B S hS) ⟶ ⟨W, hW⟩)

Tag 0DVJ, a lemma

Tag 0DVJ in the Stacks Project.

AlgebraicGeometry.Space.exists_pushout_isElementaryDistinguishedSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ElementaryDistinguishedSquareGluing.lean, line 1158.

Stacks 0DVJ. Let V and U be algebraic spaces over S, let V' be an open subspace of V and let f' : V' ⟶ U be a separated étale morphism. Then there is an algebraic space W over S together with an open subspace of W isomorphic to U and a morphism V ⟶ W forming an elementary distinguished square, and the resulting square is a pushout of V ← V' → U in the category of algebraic spaces over S.

theorem exists_pushout_isElementaryDistinguishedSquare
    (U V : AlgebraicSpaces B S hS) (V' : Subfunctor V.obj)
    (hV' : IsOpenSubspace B S hS V') (f' : V'.toFunctor ⟶ U.obj)
    (hf' : IsEtale B S hS f') (hf'sep : IsSeparated B S hS f') :
    ∃ (W : AlgebraicSpaces B S hS) (Uw : Subfunctor W.obj) (e : U.obj ≅ Uw.toFunctor)
      (f : V ⟶ W),
      IsElementaryDistinguishedSquare B S hS W.property Uw f.hom ∧
        IsPushout
          (ObjectProperty.homMk V'.ι :
            (⟨V'.toFunctor, hV'.1⟩ : AlgebraicSpaces B S hS) ⟶ V)
          (ObjectProperty.homMk f' :
            (⟨V'.toFunctor, hV'.1⟩ : AlgebraicSpaces B S hS) ⟶ U)
          f (ObjectProperty.homMk (e.hom ≫ Uw.ι) : U ⟶ W)

Sources

LeanAlgebraicGeometry.Space.isPushout_elementaryDistinguishedSquare · AlgebraicGeometry.Space.exists_pushout_isElementaryDistinguishedSquare

Section81.10 Formal glueing of quasi-coherent modules #

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

Tag 0AEQ, a lemma

Tag 0AEQ in the Stacks Project.

AlgebraicGeometry.Space.stalkDerivedPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedComplexDerivedStalk.lean, line 293. The attribute's comment: “the comparison isomorphism, for a commutative (not necessarily cartesian) square and a geometric point of Y lifted to the closed subspace, on the two carried inputs 0AEH part (1) and 015N bundled as DerivedPushforwardSquareData”.

Stacks 0AEQ. Let f : Y ⟶ X be a morphism of algebraic spaces over a scheme S, let i : Z ⟶ X and i' : W ⟶ Y be closed immersions and let f' : W ⟶ Z be an integral universally injective morphism making the square commute — in the source W = f^{-1}Z and f' is the base change of f. Let ȳ be a geometric point of Y lying on W and let x̄ = f(ȳ). For an object Q of D(Y_étale) all of whose cohomology sheaves are supported on |W|, the stalk at x̄ of Rf_*Q is the stalk at ȳ of Q.

def stalkDerivedPushforwardIso
    [RF.IsRightDerivedFunctor unit
      (HomotopyCategory.quasiIso (abelianSheaves.{u + 1} B S hS Y) (ComplexShape.up ℤ))]
    (d : DerivedPushforwardSquareData B S hS i hi i' hi' f' hf' hf'int hf'inj RF)
    (y : GeometricPoint B S hS Y.1) (w : GeometricPoint B S hS W.1)
    (hw : geometricPointMap i'.hom w = y) (Q : smallEtaleDerivedCategory.{u + 1} B S hS Y)
    (hQ : cohomologySupportedOn.{u + 1} B S hS Y
      (Set.range (pointsMap B S hS W.1 i'.hom)) Q) :
    (smallEtaleDerivedAbelianStalk B S hS (geometricPointMap f.hom y)).obj (RF.obj Q) ≅
      (smallEtaleDerivedAbelianStalk B S hS y).obj Q

AlgebraicGeometry.Space.stalkDerivedPushforwardIso_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedComplexDerivedStalk.lean, line 309. The attribute's comment: “naturality of the comparison isomorphism in the supported complex”.

Stacks 0AEQ: the comparison is natural. The identification (Rf_*Q)_{x̄} ≅ Q_ȳ is natural in the complex Q supported on |W|.

theorem stalkDerivedPushforwardIso_naturality
    [RF.IsRightDerivedFunctor unit
      (HomotopyCategory.quasiIso (abelianSheaves.{u + 1} B S hS Y) (ComplexShape.up ℤ))]
    (d : DerivedPushforwardSquareData B S hS i hi i' hi' f' hf' hf'int hf'inj RF)
    (y : GeometricPoint B S hS Y.1) (w : GeometricPoint B S hS W.1)
    (hw : geometricPointMap i'.hom w = y)
    {Q Q' : smallEtaleDerivedCategory.{u + 1} B S hS Y}
    (hQ : cohomologySupportedOn.{u + 1} B S hS Y
      (Set.range (pointsMap B S hS W.1 i'.hom)) Q)
    (hQ' : cohomologySupportedOn.{u + 1} B S hS Y
      (Set.range (pointsMap B S hS W.1 i'.hom)) Q') (g : Q ⟶ Q') :
    (smallEtaleDerivedAbelianStalk B S hS (geometricPointMap f.hom y)).map (RF.map g) ≫
        (stalkDerivedPushforwardIso B S hS f hfr i hi i' hi' f' hf' hf'int hf'inj hsq RF unit d
          y w hw Q' hQ').hom =
      (stalkDerivedPushforwardIso B S hS f hfr i hi i' hi' f' hf' hf'int hf'inj hsq RF unit d
          y w hw Q hQ).hom ≫
        (smallEtaleDerivedAbelianStalk B S hS y).map g

AlgebraicGeometry.Space.stalkRightDerivedDirectImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedComplexRightDerivedStalk.lean, line 358.

Stacks 0AEQ. Let f : Y ⟶ X be a morphism of algebraic spaces over a scheme S, let i : Z ⟶ X be a closed immersion and let f^{-1}Z be its inverse image, a cartesian square sq with f' : f^{-1}Z ⟶ Z and i' : f^{-1}Z ⟶ Y, such that f' is integral and universally injective. Let ȳ be a geometric point of Y and x̄ = f(ȳ). Then for every object Q of D(Y_étale) supported on |f^{-1}Z| there is an isomorphism (Rf_*Q)_{x̄} ≅ Q_ȳ in D(Ab), where Rf_* is any total right derived functor of the direct image of abelian sheaves along f and the derived categories are arbitrary models.

def stalkRightDerivedDirectImageIso (f : Y ⟶ X) (i : Z ⟶ X) (hi : IsClosedImmersion B S hS i.hom)
    (i' : W ⟶ Y) (f' : W ⟶ Z) (sq : IsPullback f' i' i f) (hf'int : IsIntegralHom B S hS f'.hom)
    (hf'inj : UniversallyInjective B S hS f'.hom)
    (RF : DerivedCategory (abelianSheaves.{u + 1} B S hS Y) ⥤
      DerivedCategory (abelianSheaves.{u + 1} B S hS X))
    (α : (smallEtaleAbelianDirectImage B S hS f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ RF)
    [RF.IsRightDerivedFunctor α
      (HomotopyCategory.quasiIso (abelianSheaves.{u + 1} B S hS Y) (ComplexShape.up ℤ))]
    (y : GeometricPoint B S hS Y.1)
    (Q : DerivedCategory (abelianSheaves.{u + 1} B S hS Y))
    (hQ : ∀ n : ℤ, supportOfSheaf B S hS Y.1
      ((DerivedCategory.homologyFunctor (abelianSheaves.{u + 1} B S hS Y) n).obj Q) ⊆
        Set.range (pointsMap B S hS W.1 i'.hom)) :
    (smallEtaleAbelianStalk B S hS (geometricPointMap f.hom y)).mapDerivedCategory.obj
        (RF.obj Q) ≅
      (smallEtaleAbelianStalk B S hS y).mapDerivedCategory.obj Q

AlgebraicGeometry.Space.stalkRightDerivedDirectImageIso_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SupportedComplexRightDerivedStalk.lean, line 381. The attribute's comment: “naturality of the comparison in the supported complex”.

Stacks 0AEQ: the comparison is natural in the complex Q supported on |f^{-1}Z|, being the value at Q of an isomorphism of functors.

theorem stalkRightDerivedDirectImageIso_naturality (f : Y ⟶ X) (i : Z ⟶ X)
    (hi : IsClosedImmersion B S hS i.hom)
    (i' : W ⟶ Y) (f' : W ⟶ Z) (sq : IsPullback f' i' i f) (hf'int : IsIntegralHom B S hS f'.hom)
    (hf'inj : UniversallyInjective B S hS f'.hom)
    (RF : DerivedCategory (abelianSheaves.{u + 1} B S hS Y) ⥤
      DerivedCategory (abelianSheaves.{u + 1} B S hS X))
    (α : (smallEtaleAbelianDirectImage B S hS f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ RF)
    [RF.IsRightDerivedFunctor α
      (HomotopyCategory.quasiIso (abelianSheaves.{u + 1} B S hS Y) (ComplexShape.up ℤ))]
    (y : GeometricPoint B S hS Y.1)
    {Q Q' : DerivedCategory (abelianSheaves.{u + 1} B S hS Y)}
    (hQ : ∀ n : ℤ, supportOfSheaf B S hS Y.1
      ((DerivedCategory.homologyFunctor (abelianSheaves.{u + 1} B S hS Y) n).obj Q) ⊆
        Set.range (pointsMap B S hS W.1 i'.hom))
    (hQ' : ∀ n : ℤ, supportOfSheaf B S hS Y.1
      ((DerivedCategory.homologyFunctor (abelianSheaves.{u + 1} B S hS Y) n).obj Q') ⊆
        Set.range (pointsMap B S hS W.1 i'.hom)) (g : Q ⟶ Q') :
    (smallEtaleAbelianStalk B S hS (geometricPointMap f.hom y)).mapDerivedCategory.map
        (RF.map g) ≫
        (stalkRightDerivedDirectImageIso B S hS f i hi i' f' sq hf'int hf'inj RF α y Q' hQ').hom =
      (stalkRightDerivedDirectImageIso B S hS f i hi i' f' sq hf'int hf'inj RF α y Q hQ).hom ≫
        (smallEtaleAbelianStalk B S hS y).mapDerivedCategory.map g

Tag 0AER, a lemma

Tag 0AER in the Stacks Project.

AlgebraicGeometry.Space.isIso_kernelMap_and_mono_cokernelMap_pushforwardStalkMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalGlueingTwoTermStalkComplex.lean, line 425. The attribute's comment: “isomorphism on kernels and injection on cokernels of the two-term stalk complexes”.

Stacks 0AER. Let f : Y ⟶ X be a morphism of algebraic spaces over a scheme S and let Z ⊆ X be a closed subspace such that f^{-1}Z ⟶ Z is integral and universally injective. Let ȳ be a geometric point of Y, let x̄ = f(ȳ) and let G be an abelian sheaf on the small étale site of Y. Writing V = Y ∖ f^{-1}Z and j' : V ⟶ Y for the inclusion, the map of two-term complexes
((f_*G)_x̄ ⟶ (f_*(j'_*(G|_V)))_x̄) ⟶ (G_ȳ ⟶ (j'_*(G|_V))_ȳ)
given by the canonical comparison of AlgebraicGeometry.Space.smallEtaleAbelianPushforwardStalkMap induces an isomorphism on kernels and an injection on cokernels.

theorem isIso_kernelMap_and_mono_cokernelMap_pushforwardStalkMap (f : Y ⟶ X)
    (hfr : yoneda.relativelyRepresentable f.hom) (Z : ClosedSubspaces B S hS X.1)
    (hint : IsIntegralHom B S hS (Z.1.fromPreimage f.hom))
    (hinj : UniversallyInjective B S hS (Z.1.fromPreimage f.hom))
    (y : GeometricPoint B S hS Y.1) (G : abelianSheaves.{u + 1} B S hS Y) :
    IsIso (kernel.map
        ((smallEtaleAbelianPushforward.{u + 1} B S hS f hfr ⋙
            smallEtaleAbelianStalk B S hS (geometricPointMap f.hom y)).map
          (smallEtaleAbelianRestrictionUnit B S hS f Z G))
        ((smallEtaleAbelianStalk B S hS y).map
          (smallEtaleAbelianRestrictionUnit B S hS f Z G))
        ((smallEtaleAbelianPushforwardStalkMap B S hS f hfr y).app G)
        ((smallEtaleAbelianPushforwardStalkMap B S hS f hfr y).app
          (smallEtaleAbelianRestrictionPushforward B S hS f Z G))
        ((smallEtaleAbelianPushforwardStalkMap B S hS f hfr y).naturality
          (smallEtaleAbelianRestrictionUnit B S hS f Z G))) ∧
      Mono (cokernel.map
        ((smallEtaleAbelianPushforward.{u + 1} B S hS f hfr ⋙
            smallEtaleAbelianStalk B S hS (geometricPointMap f.hom y)).map
          (smallEtaleAbelianRestrictionUnit B S hS f Z G))
        ((smallEtaleAbelianStalk B S hS y).map
          (smallEtaleAbelianRestrictionUnit B S hS f Z G))
        ((smallEtaleAbelianPushforwardStalkMap B S hS f hfr y).app G)
        ((smallEtaleAbelianPushforwardStalkMap B S hS f hfr y).app
          (smallEtaleAbelianRestrictionPushforward B S hS f Z G))
        ((smallEtaleAbelianPushforwardStalkMap B S hS f hfr y).naturality
          (smallEtaleAbelianRestrictionUnit B S hS f Z G)))

AlgebraicGeometry.Space.isIso_kernelMap_and_mono_cokernelMap_directImageStalkMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalGlueingTwoTermStalkComplexGeneral.lean, line 199. The attribute's comment: “isomorphism on kernels and injection on cokernels of the two-term stalk complexes, for an arbitrary morphism of algebraic spaces”.

Stacks 0AER. Let f : Y ⟶ X be a morphism of algebraic spaces over a scheme S and let Z ⊆ X be a closed subspace such that f^{-1}Z ⟶ Z is integral and universally injective. Let ȳ be a geometric point of Y, let x̄ = f(ȳ) and let G be an abelian sheaf on the small étale site of Y. Writing V = Y ∖ f^{-1}Z and j' : V ⟶ Y for the inclusion, the map of two-term complexes
((f_*G)_x̄ ⟶ (f_*(j'_*(G|_V)))_x̄) ⟶ (G_ȳ ⟶ (j'_*(G|_V))_ȳ)
given by the canonical comparison of AlgebraicGeometry.Space.smallEtaleAbelianPushforwardStalkMap induces an isomorphism on kernels and an injection on cokernels.

theorem isIso_kernelMap_and_mono_cokernelMap_directImageStalkMap (f : Y ⟶ X)
    (Z : ClosedSubspaces B S hS X.1)
    (hint : IsIntegralHom B S hS (Z.1.fromPreimage f.hom))
    (hinj : UniversallyInjective B S hS (Z.1.fromPreimage f.hom))
    (y : GeometricPoint B S hS Y.1) (G : abelianSheaves.{u + 1} B S hS Y) :
    IsIso (kernel.map
        ((smallEtaleAbelianDirectImage B S hS f ⋙
            smallEtaleAbelianStalk B S hS (geometricPointMap f.hom y)).map
          (smallEtaleAbelianRestrictionUnit B S hS f Z G))
        ((smallEtaleAbelianStalk B S hS y).map
          (smallEtaleAbelianRestrictionUnit B S hS f Z G))
        ((smallEtaleAbelianDirectImageStalkMap B S hS f y).app G)
        ((smallEtaleAbelianDirectImageStalkMap B S hS f y).app
          (smallEtaleAbelianRestrictionPushforward B S hS f Z G))
        ((smallEtaleAbelianDirectImageStalkMap B S hS f y).naturality
          (smallEtaleAbelianRestrictionUnit B S hS f Z G))) ∧
      Mono (cokernel.map
        ((smallEtaleAbelianDirectImage B S hS f ⋙
            smallEtaleAbelianStalk B S hS (geometricPointMap f.hom y)).map
          (smallEtaleAbelianRestrictionUnit B S hS f Z G))
        ((smallEtaleAbelianStalk B S hS y).map
          (smallEtaleAbelianRestrictionUnit B S hS f Z G))
        ((smallEtaleAbelianDirectImageStalkMap B S hS f y).app G)
        ((smallEtaleAbelianDirectImageStalkMap B S hS f y).app
          (smallEtaleAbelianRestrictionPushforward B S hS f Z G))
        ((smallEtaleAbelianDirectImageStalkMap B S hS f y).naturality
          (smallEtaleAbelianRestrictionUnit B S hS f Z G)))

Tag 0AES, a lemma

Tag 0AES in the Stacks Project.

AlgebraicGeometry.Space.exists_geometricModuleStalkGerm_modulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DirectImageGeometricStalk.lean, line 232. The attribute's comment: “generation half, for the geometric point stalk expressed as the filtered colimit over the etale neighbourhoods of x-bar, with the sections on Y times_X V read chartwise; the canonical morphism Spec(O_{X, x-bar}) -> X is not constructed, since the etale local ring lives one universe up and its spectrum is not an object of the site, so neither the source's formula nor its quasi-compact, quasi-separated and quasi-coherent hypotheses appear”.

Stacks 0AES, the generation half of the colimit form. Every element of the geometric stalk (f_*G)_{x̄} is the germ at x̄ of a section of p_V^*G on Y ×_X V, for some small étale neighbourhood V of x̄: that section is a compatible family of sections of G over the étale scheme charts of Y above Y ×_X V.

theorem exists_geometricModuleStalkGerm_modulePushforward (f : Y ⟶ X)
    (z : geometricModuleStalk B S hS X x ((modulePushforward B S hS f).obj G)) :
    ∃ (N : SmallEtaleNeighborhood x) (a : (directImageChartDiagram B S hS f G N.chart).sections),
      geometricModuleStalkGerm B S hS X x ((modulePushforward B S hS f).obj G) N
        ((directImageChartSectionsEquiv B S hS f G N.chart).symm a) = z

AlgebraicGeometry.Space.geometricModuleStalkGerm_modulePushforward_eq_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DirectImageGeometricStalk.lean, line 253. The attribute's comment: “separation half, for the geometric point stalk expressed as the filtered colimit over the etale neighbourhoods of x-bar, with the sections on Y times_X V read chartwise; the canonical morphism Spec(O_{X, x-bar}) -> X is not constructed, since the etale local ring lives one universe up and its spectrum is not an object of the site, so neither the source's formula nor its quasi-compact, quasi-separated and quasi-coherent hypotheses appear”.

Stacks 0AES, the separation half of the colimit form. Two sections of the direct image f_*G over the chart of a small étale neighbourhood N of x̄ have the same germ in the geometric stalk (f_*G)_{x̄} exactly when, for some smaller neighbourhood V, their chartwise sections of G over the étale scheme charts of Y above Y ×_X V agree — that is, exactly when they agree in Γ(Y ×_X V, p_V^*G).

theorem geometricModuleStalkGerm_modulePushforward_eq_iff (f : Y ⟶ X)
    (N : SmallEtaleNeighborhood x)
    (s t : ((modulePushforward B S hS f).obj G).val.obj (op N.chart)) :
    geometricModuleStalkGerm B S hS X x ((modulePushforward B S hS f).obj G) N s =
        geometricModuleStalkGerm B S hS X x ((modulePushforward B S hS f).obj G) N t ↔
      ∃ (M : SmallEtaleNeighborhood x) (g : M ⟶ N), ∀ j,
        directImageChartSection B S hS f G M.chart j
            (((modulePushforward B S hS f).obj G).val.map g.hom.op s) =
          directImageChartSection B S hS f G M.chart j
            (((modulePushforward B S hS f).obj G).val.map g.hom.op t)

AlgebraicGeometry.Space.directImageGeometricStalkAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/DirectImageStalkStrictHenselization.lean, line 162. The attribute's comment: “(f_G)_xbar = Γ(Y ×_X Spec(O_{X,xbar}), p^G) for f quasi-compact and quasi-separated and G quasi-coherent, as an isomorphism of abelian groups; the source's p^F is a misprint for p^G”.

The stalk of a direct image at a geometric point, over the strict henselization. Let X be an algebraic space over S, f : Y ⟶ X a quasi-compact and quasi-separated morphism, x̄ a geometric point of X and h : Spec(𝒪_{X, x̄}) ⟶ X the canonical morphism (AlgebraicGeometry.Space.strictHenselizationSpaceHom). For a quasi-coherent 𝒪_Y-module 𝒢,

(f_*𝒢)_{x̄} = Γ(Y ×_X Spec(𝒪_{X, x̄}), p^*𝒢),

where p : Y ×_X Spec(𝒪_{X, x̄}) ⟶ Y is the projection: the geometric stalk of the direct image is identified, as an abelian group, with the global sections of the pullback of 𝒢 to the base change of Y to the strict henselization. (The source prints p^*𝓕 for p^*𝒢.)

The identification is the composite of: the stalk of f_*𝒢 at x̄ = h ∘ t̄ with the stalk of h^*f_*𝒢 at the closed point t̄ (Stacks 05VQ and the bijectivity of 𝒪_{X, x̄} ⟶ 𝒪_{T, t̄}), that stalk with the global sections of h^*f_*𝒢 (the closed point has an initial neighbourhood), the flat base change h^*f_*𝒢 ≅ f'_*p^*𝒢 of Stacks 073K, and Γ(T, f'_* -) = Γ(Y ×_X T, -).

def directImageGeometricStalkAddEquiv :
    geometricModuleStalk B S hS X x ((modulePushforward B S hS f).obj G) ≃+
      ((modulePullback B S hS (pullback.fst f (strictHenselizationSpaceHom X x))).obj
        G).sections

Tag 0AET, a lemma

Tag 0AET in the Stacks Project.

AlgebraicGeometry.Space.closedSubspaceStalkIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/StalkTorsionOfSupportedComplex.lean, line 355. The attribute's comment: “the stalk I_x̄ of the ideal sheaf of Z”.

Stacks 0AET. The stalk I_x̄ ⊆ 𝒪_{X, x̄} at a geometric point of the ideal sheaf of a closed subspace: the ideal of the étale local ring generated by the germs of the local sections of the defining ideal.

noncomputable def closedSubspaceStalkIdeal (X : AlgebraicSpaces B S hS)
    (Z : ClosedSubspaces B S hS X.1) (x : GeometricPoint B S hS X.1) :
    Ideal (etaleLocalRing B S hS X.1 x)

AlgebraicGeometry.Space.isIPowerTorsion_geometricModuleStalk_homology_of_cohomologySupportedOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/StalkTorsionOfSupportedComplex.lean, line 423. The attribute's comment: “asserted for the stalk Hⁿ(Q)_x̄ of the cohomology sheaf rather than for the cohomology Hⁿ(Q_x̄) of the stalk of Q in D(Ab); the two agree by exactness of the stalk functor at a geometric point, which this development does not have. Stated at module universe m = u”.

Stacks 0AET. Let X be an algebraic space over S, let Z ⊆ X be a closed subspace whose inclusion is of finite presentation and let Q ∈ D_QCoh(𝒪_X) have all its cohomology sheaves supported on |Z|. Then at every geometric point x̄ the stalk of every cohomology sheaf of Q is power torsion for the stalk I_x̄ of the ideal sheaf of Z.

theorem isIPowerTorsion_geometricModuleStalk_homology_of_cohomologySupportedOn
    (X : AlgebraicSpaces B S hS)
    [HasSheafify (smallEtaleRingedSite B S hS X.1 X.2).J AddCommGrpCat.{u}]
    [(smallEtaleRingedSite B S hS X.1 X.2).J.WEqualsLocallyBijective AddCommGrpCat.{u}]
    (Z : ClosedSubspaces B S hS X.1) (hZ : IsFinitePresentation B S hS Z.1.ι)
    (Q : QuasicoherentDerivedCategory.{u, u} B S hS X.1 X.2)
    (hQ : CohomologySupportedOn B S hS X.1 X.2
      (Set.range (pointsMap B S hS Z.1.toFunctor Z.1.ι)) Q.1)
    (x : GeometricPoint B S hS X.1) (n : ℤ) :
    IsIPowerTorsion (etaleLocalRing B S hS X.1 x)
      (geometricModuleStalk B S hS X x
        ((DerivedCategory.homologyFunctor (Modules.{u, u} B S hS X.1 X.2) n).obj Q.1))
      (closedSubspaceStalkIdeal B S hS X Z x)

Tag 0AEU, a lemma

Tag 0AEU in the Stacks Project.

AlgebraicGeometry.Space.isIso_derivedAdjunction_counit_app_of_cohomologySupportedOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingDerivedEquivalence.lean, line 167. The attribute's comment: “with Z ⟶ X of finite presentation, which the source's proof uses and without which the statement fails”.

Stacks 0AEU. Let f : Y ⟶ X be a morphism of algebraic spaces over S and Z ⊆ X a closed subspace of finite presentation such that f⁻¹Z ⟶ Z is an isomorphism and f is flat at every point of f⁻¹Z. Then for every Q ∈ D_QCoh(𝒪_Y) supported on |f⁻¹Z| the counit Lf^*Rf_*Q ⟶ Q of the derived adjunction of the morphism of small étale ringed topoi is an isomorphism.

The finite presentation of Z ⟶ X is not in the source's statement, but the source's proof uses it (through Stacks 0AET and 05E9, which need the ideal of Z finitely generated), and the assertion is false without it. Let A be a valuation ring of rank one with divisible value group, X = Spec A and Z = V(m) for the maximal ideal m = m², which is not finitely generated. Choose g ∈ m of valuation 1 and c_n ∈ A whose valuations increase strictly to 1, and let Y = Spec B for B = A[t/c_1, t/c_2, …] ⊂ K[t]. Then B is flat over A, B/mB = A/m, so f⁻¹Z ⟶ Z is an isomorphism, and M = B/gB is supported on V(mB); but the counit M ⊗_A B ⟶ M is not an isomorphism, because t ∉ A + gB. In Stacks 0AFJ, the application the source makes of this lemma, Z ⟶ X is of finite presentation by Situation 0AEV.

theorem isIso_derivedAdjunction_counit_app_of_cohomologySupportedOn
    {Y X : AlgebraicSpaces B S hS} (f : Y ⟶ X) (Z : Subfunctor X.1)
    (hZ : IsClosedSubspace B S hS Z) (hZfp : IsFinitePresentation B S hS Z.ι)
    (hfZ : IsIso (Z.fromPreimage f.hom))
    (hflat : ∀ y : points B S hS (Z.preimage f.hom).toFunctor,
      IsFlatAt B S hS f.hom
        (pointsMap B S hS (Z.preimage f.hom).toFunctor (Z.preimage f.hom).ι y))
    (Q : QuasicoherentDerivedCategory.{u, u} B S hS Y.1 Y.2)
    (hQ : CohomologySupportedOn B S hS Y.1 Y.2
      (Set.range (pointsMap B S hS (Z.preimage f.hom).toFunctor (Z.preimage f.hom).ι)) Q.1) :
    IsIso ((derivedAdjunction (smallEtaleRingedToposHom B S hS f)).counit.app Q.1)

Tag 0AEV, a situation

Tag 0AEV in the Stacks Project.

AlgebraicGeometry.Space.FormalGlueingSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModules.lean, line 59. The attribute's comment: “standing data and hypotheses”.

Stacks 0AEV. The standing situation for formal glueing of quasi-coherent modules: a quasi-compact, quasi-separated morphism f : Y ⟶ X of algebraic spaces over S, a finitely presented closed subspace Z of X over which f is an isomorphism, with f flat at every point of the inverse image of Z.

structure FormalGlueingSituation
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)

AlgebraicGeometry.Space.FormalGlueingSituation.V_eq_openComplement_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModules.lean, line 105. The attribute's comment: “V = Y minus the inverse image of Z”.

Stacks 0AEV. The inverse image of the open complement of Z is the open complement of the inverse image of Z.

theorem V_eq_openComplement_preimage (D : FormalGlueingSituation B S hS) :
    D.V = openComplement B S hS (D.Z.preimage D.f)

AlgebraicGeometry.Space.FormalGlueingSituation.isOpenSubspace_U, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModules.lean, line 115. The attribute's comment: “openness of U”.

Stacks 0AEV. The complement of Z is an open subspace of X.

theorem isOpenSubspace_U (D : FormalGlueingSituation B S hS) :
    IsOpenSubspace B S hS D.U

AlgebraicGeometry.Space.FormalGlueingSituation.isOpenSubspace_V, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModules.lean, line 121. The attribute's comment: “openness of V”.

Stacks 0AEV. The complement of the inverse image of Z is an open subspace of Y.

theorem isOpenSubspace_V (D : FormalGlueingSituation B S hS) :
    IsOpenSubspace B S hS D.V

Tag 0AEW, an equation

Tag 0AEW in the Stacks Project.

AlgebraicGeometry.Space.FormalGlueingSituation.overlapPullbackComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModulesFunctor.lean, line 244. The attribute's comment: “the comparison over the overlap”.

The canonical identification (f|_V)^* ∘ j^* ≅ (j')^* ∘ f^* of the two ways of transporting an 𝒪_X-module to the overlap V: both are the inverse image along the common composite V ⟶ X of the glueing square, by the inverse-image half of Stacks 03LU.

def overlapPullbackComparison :
    modulePullback B S hS D.openImmersion ⋙ modulePullback B S hS D.overlapRestriction ≅
      modulePullback B S hS D.ambientMorphism ⋙ modulePullback B S hS D.openImmersionOver

AlgebraicGeometry.Space.FormalGlueingSituation.moduleGlueingData, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModulesFunctor.lean, line 262. The attribute's comment: “the category of glueing data”.

The category QCoh(Y → X, Z) of formal glueing data for quasi-coherent modules: the triples (H, G, φ) of a quasi-coherent 𝒪_U-module H, a quasi-coherent 𝒪_Y-module G and an isomorphism φ : (f|_V)^*H ≅ G|_V, with the pairs of module maps commuting with the overlap isomorphisms as morphisms.

The category is introduced in the prose of the source immediately before equation (0AEX); it is the target of the functor of Stacks 0AEW and the source of the functor of Stacks 0AEX.

abbrev moduleGlueingData

AlgebraicGeometry.Space.FormalGlueingSituation.glueingModulesUnconditional, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModulesFunctorUnconditional.lean, line 67.

The functor QCoh(𝒪_X) ⥤ QCoh(Y → X, Z) of formal glueing: a quasi-coherent 𝒪_X-module goes to its restriction to the open complement U, its pullback to Y, and the canonical comparison of the two on the overlap V.

def glueingModulesUnconditional :
    QuasicoherentSheaves.{u, u} B S hS D.spaceX.1 D.spaceX.2 ⥤ D.moduleGlueingData

AlgebraicGeometry.Space.FormalGlueingSituation.glueingModulesFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModulesUnconditional.lean, line 55. The attribute's comment: “the functor, with no hypothesis”.

The functor QCoh(𝒪_X) ⥤ QCoh(Y → X, Z) of formal glueing: a quasi-coherent 𝒪_X-module F goes to (F|_U, f^*F, can).

def glueingModulesFunctor :
    QuasicoherentSheaves.{u, u} B S hS D.spaceX.1 D.spaceX.2 ⥤ D.moduleGlueingData

Tag 0AEX, an equation

Tag 0AEX in the Stacks Project.

AlgebraicGeometry.Space.FormalGlueingSituation.glueingKernelMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModulesKernel.lean, line 287. The attribute's comment: “the map out of the direct sum”.

The map j_*H ⊕ f_*G ⟶ (f ∘ j')_*(G|_V) of Stacks 0AEX: the difference of the two canonical maps to the direct image from the overlap, so that a pair of sections lies in its kernel exactly when the two sections agree on the overlap.

def glueingKernelMap :
    D.restrictionDirectImage ⊞ D.ambientDirectImage ⟶ D.overlapDirectImage

AlgebraicGeometry.Space.FormalGlueingSituation.glueingKernelDiagram, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModulesKernel.lean, line 301. The attribute's comment: “the kernel module, as a functor of the glueing triple”.

The 𝒪_X-module Ker(j_*H ⊕ f_*G ⟶ (f ∘ j')_*(G|_V)) of Stacks 0AEX, as a functor of the glueing triple. It is the kernel in the category of functors to the 𝒪_X-modules, so no quasi-coherence is assumed and the functoriality is that of a kernel.

def glueingKernelDiagram :
    D.moduleGlueingComma ⥤ Modules.{u, u} B S hS D.spaceX.1 D.spaceX.2

AlgebraicGeometry.Space.FormalGlueingSituation.glueingKernelFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModulesUnconditional.lean, line 97. The attribute's comment: “the functor, with no hypothesis”.

The functor QCoh(Y → X, Z) ⥤ QCoh(𝒪_X), (H, G, φ) ↦ Ker(j_*H ⊕ f_*G ⟶ (f ∘ j')_*(G|_V)).

def glueingKernelFunctor :
    D.moduleGlueingData ⥤ QuasicoherentSheaves.{u, u} B S hS D.spaceX.1 D.spaceX.2

Tag 0AEY, a lemma

Tag 0AEY in the Stacks Project.

AlgebraicGeometry.Space.FormalGlueingSituation.glueingAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModulesUnconditional.lean, line 118. The attribute's comment: “with no hypothesis”.

The functor glueingModulesFunctor is left adjoint to the functor glueingKernelFunctor.

def glueingAdjunction : D.glueingModulesFunctor ⊣ D.glueingKernelFunctor

Tag 0AEZ, a lemma

Tag 0AEZ in the Stacks Project.

AlgebraicGeometry.Space.FormalGlueingSituation.FlatBaseChange.glueingModulesFunctorPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModulesFlatBaseChangeUnconditional.lean, line 473. The attribute's comment: “compatibility with the functor of Tag 0AEW”.

Stacks 0AEZ, compatibility with the functor of Stacks 0AEW. For the base change of the formal glueing situation along a flat morphism g : X' ⟶ X, the pullback QCoh(𝒪_X) ⥤ QCoh(𝒪_{X'}) of Stacks 03GA and the pullback QCoh(Y → X, Z) ⥤ QCoh(Y' → X', Z') of glueing triples commute with the functors QCoh(𝒪_X) ⥤ QCoh(Y → X, Z) and QCoh(𝒪_{X'}) ⥤ QCoh(Y' → X', Z') of Stacks 0AEW.

def glueingModulesFunctorPullbackIso :
    D.glueingModulesFunctor ⋙ c.glueingDataPullback ≅
      quasicoherentPullbackFunctor B S hS c.g ⋙ D'.glueingModulesFunctor

AlgebraicGeometry.Space.FormalGlueingSituation.FlatBaseChange.glueingKernelFunctorPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModulesFlatBaseChangeUnconditional.lean, line 500. The attribute's comment: “compatibility with the functor of Tag 0AEX”.

Stacks 0AEZ, compatibility with the functor of Stacks 0AEX. For the base change of the formal glueing situation along a flat morphism g : X' ⟶ X, the pullback QCoh(𝒪_X) ⥤ QCoh(𝒪_{X'}) of Stacks 03GA and the pullback QCoh(Y → X, Z) ⥤ QCoh(Y' → X', Z') of glueing triples commute with the functors QCoh(Y → X, Z) ⥤ QCoh(𝒪_X) and QCoh(Y' → X', Z') ⥤ QCoh(𝒪_{X'}) of Stacks 0AEX.

The isomorphism is the one transported from AlgebraicGeometry.Space.FormalGlueingSituation.FlatBaseChange.glueingModulesFunctorPullbackIso along the two equivalences of Stacks 0AF0, whose quasi-inverses are the functors of Stacks 0AEX.

def glueingKernelFunctorPullbackIso :
    D.glueingKernelFunctor ⋙ quasicoherentPullbackFunctor B S hS c.g ≅
      c.glueingDataPullback ⋙ D'.glueingKernelFunctor

AlgebraicGeometry.Space.FormalGlueingSituation.glueingModulesFunctorBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModulesFlatBaseChangeUnconditional.lean, line 519. The attribute's comment: “compatibility with the functor of Tag 0AEW, for the constructed base change along a flat morphism”.

Stacks 0AEZ, compatibility with the functor of Stacks 0AEW, for the base change of the situation along a flat morphism k : X' ⟶ X, with Z' = X' ×_X Z and Y' = X' ×_X Y.

def glueingModulesFunctorBaseChangeIso :
    D.glueingModulesFunctor ⋙ (D.flatBaseChange k hk).glueingDataPullback ≅
      quasicoherentPullbackFunctor B S hS k ⋙ (D.baseChange k).glueingModulesFunctor

AlgebraicGeometry.Space.FormalGlueingSituation.glueingKernelFunctorBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModulesFlatBaseChangeUnconditional.lean, line 528. The attribute's comment: “compatibility with the functor of Tag 0AEX, for the constructed base change along a flat morphism”.

Stacks 0AEZ, compatibility with the functor of Stacks 0AEX, for the base change of the situation along a flat morphism k : X' ⟶ X, with Z' = X' ×_X Z and Y' = X' ×_X Y.

def glueingKernelFunctorBaseChangeIso :
    D.glueingKernelFunctor ⋙ quasicoherentPullbackFunctor B S hS k ≅
      (D.flatBaseChange k hk).glueingDataPullback ⋙ (D.baseChange k).glueingKernelFunctor

Tag 0AF0, a proposition

Tag 0AF0 in the Stacks Project.

AlgebraicGeometry.Space.FormalGlueingSituation.isIso_glueingAdjunction_unit_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingModulesQCohEquivalence.lean, line 83.

Stacks 0AF0. In Situation 0AEV the functor QCoh(𝒪_X) ⥤ QCoh(Y → X, Z) of Stacks 0AEW is an equivalence with quasi-inverse the functor of Stacks 0AEX: the unit and the counit of the adjunction of Stacks 0AEY between them are isomorphisms.

theorem isIso_glueingAdjunction_unit_counit :
    IsIso D.glueingAdjunction.unit ∧ IsIso D.glueingAdjunction.counit

Tag 0AFJ, a lemma

Tag 0AFJ in the Stacks Project.

AlgebraicGeometry.Space.FormalGlueingSituation.exists_supportedQuasicoherentDerived_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingDerivedEquivalence.lean, line 198.

Stacks 0AFJ. In Situation 0AEV (AlgebraicGeometry.Space.FormalGlueingSituation), the derived direct image Rf_* of the morphism of small étale ringed topoi of f induces an equivalence D_{QCoh,|f⁻¹Z|}(𝒪_Y) ≌ D_{QCoh,|Z|}(𝒪_X) with quasi-inverse given by the derived pullback Lf^*: there is an equivalence whose functor is the restriction of Rf_* and whose inverse is the restriction of Lf^*.

theorem FormalGlueingSituation.exists_supportedQuasicoherentDerived_equivalence
    (D : FormalGlueingSituation B S hS) :
    letI := HasDerivedCategory.standard (Modules.{u, u} B S hS D.spaceX.1 D.spaceX.2)
    letI := HasDerivedCategory.standard (Modules.{u, u} B S hS D.spaceY.1 D.spaceY.2)
    ∃ e : (supportedQuasicoherentDerived B S hS D.spaceY
        (subspacePointSet B S hS D.Y (D.Z.preimage D.f))).FullSubcategory ≌
      (supportedQuasicoherentDerived B S hS D.spaceX
        (subspacePointSet B S hS D.X D.Z)).FullSubcategory,
      e.functor ⋙ (supportedQuasicoherentDerived B S hS D.spaceX
          (subspacePointSet B S hS D.X D.Z)).ι =
        (supportedQuasicoherentDerived B S hS D.spaceY
          (subspacePointSet B S hS D.Y (D.Z.preimage D.f))).ι ⋙
          derivedPushforward (X := smallEtaleRingedTopos B S hS D.spaceY)
            (Y := smallEtaleRingedTopos B S hS D.spaceX)
            (smallEtaleRingedToposHom B S hS D.ambientMorphism) ∧
      e.inverse ⋙ (supportedQuasicoherentDerived B S hS D.spaceY
          (subspacePointSet B S hS D.Y (D.Z.preimage D.f))).ι =
        (supportedQuasicoherentDerived B S hS D.spaceX
          (subspacePointSet B S hS D.X D.Z)).ι ⋙
          smallEtaleDerivedModulePullback B S hS D.ambientMorphism

Tag 0AF1, a lemma

Tag 0AF1 in the Stacks Project.

AlgebraicGeometry.Space.exists_fpqcCovering_refining_openComplement_and_source, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingCovering.lean, line 950.

The open complement and the formal-glueing morphism admit an fpqc covering refinement.

theorem exists_fpqcCovering_refining_openComplement_and_source
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (D : FormalGlueingSituation B S hS) :
    ∃ (I : Type u)
      (Xi : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
      (g : ∀ i, Xi i ⟶ D.X),
      (∀ i, IsAlgebraicSpace B S hS (Xi i)) ∧
      IsFpqcCovering B S hS g ∧
      (∀ i, (∃ a : Xi i ⟶ D.U.toFunctor, a ≫ D.U.ι = g i) ∨
        (∃ b : Xi i ⟶ D.Y, b ≫ D.f = g i))

Sources

LeanAlgebraicGeometry.Space.stalkDerivedPushforwardIso · AlgebraicGeometry.Space.stalkDerivedPushforwardIso_naturality · AlgebraicGeometry.Space.stalkRightDerivedDirectImageIso · AlgebraicGeometry.Space.stalkRightDerivedDirectImageIso_naturality · AlgebraicGeometry.Space.isIso_kernelMap_and_mono_cokernelMap_pushforwardStalkMap · AlgebraicGeometry.Space.isIso_kernelMap_and_mono_cokernelMap_directImageStalkMap · AlgebraicGeometry.Space.exists_geometricModuleStalkGerm_modulePushforward · AlgebraicGeometry.Space.geometricModuleStalkGerm_modulePushforward_eq_iff

Section81.11 Formal glueing of algebraic spaces #

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

Tag 0AF3, an equation

Tag 0AF3 in the Stacks Project.

AlgebraicGeometry.Space.FormalGlueingSituation.formalGlueingFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingSpaces.lean, line 149.

Restriction from algebraic spaces over X to their cartesian formal-glueing diagrams. The comparison identifies it naturally with pullback on each component and the canonical associativity identification on the overlap.

noncomputable def formalGlueingFunctor (D : FormalGlueingSituation B S hS) :
    Σ F : spacesOverX D ⥤ glueingData D,
      F ⋙ (show ObjectProperty
          (Comma (Over.pullback (D.U.fromPreimage D.f))
            (Over.pullback D.V.ι)) from
          fun T ↦ IsIso T.hom ∧
            IsAlgebraicSpace B S hS T.left.left ∧
            IsAlgebraicSpace B S hS T.right.left).ι ≅
        (show ObjectProperty (Over D.X) from
          fun T ↦ IsAlgebraicSpace B S hS T.left).ι ⋙
          restrictionDiagram D

Tag 0AF4, a lemma

Tag 0AF4 in the Stacks Project.

AlgebraicGeometry.Space.FormalGlueingSituation.affineGlueingFunctor_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingSpacesRestrictedEquivalences.lean, line 55. The attribute's comment: “part (1)”.

Stacks 0AF4, part (1). The functor of Stacks 0AF3 is an equivalence from algebraic spaces affine over X onto glueing triples whose maps U' ⟶ U, V' ⟶ V and Y' ⟶ Y are affine.

theorem affineGlueingFunctor_isEquivalence (D : FormalGlueingSituation B S hS) :
    (affineGlueingFunctor D).IsEquivalence

AlgebraicGeometry.Space.FormalGlueingSituation.closedGlueingFunctor_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingSpacesRestrictedEquivalences.lean, line 62. The attribute's comment: “part (2)”.

Stacks 0AF4, part (2). The functor of Stacks 0AF3 is an equivalence from closed immersions into X onto glueing triples whose three maps are closed immersions.

theorem closedGlueingFunctor_isEquivalence (D : FormalGlueingSituation B S hS) :
    (closedGlueingFunctor D).IsEquivalence

AlgebraicGeometry.Space.FormalGlueingSituation.finiteGlueingFunctor_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingSpacesRestrictedEquivalences.lean, line 69. The attribute's comment: “part (3)”.

Stacks 0AF4, part (3). The functor of Stacks 0AF3 is an equivalence from algebraic spaces finite over X onto glueing triples whose three maps are finite.

theorem finiteGlueingFunctor_isEquivalence (D : FormalGlueingSituation B S hS) :
    (finiteGlueingFunctor D).IsEquivalence

Tag 0AF5, a lemma

Tag 0AF5 in the Stacks Project.

AlgebraicGeometry.Space.FormalGlueingSituation.reflectsIsomorphisms_formalGlueingFunctor, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingSpaces.lean, line 301.

Stacks 0AF5. The restriction functor from algebraic spaces over X to cartesian formal-glueing triples reflects isomorphisms: a morphism over X whose restrictions to U and to Y are invertible is itself invertible.

instance reflectsIsomorphisms_formalGlueingFunctor
    (D : FormalGlueingSituation B S hS) :
    (formalGlueingFunctor D).1.ReflectsIsomorphisms

Tag 0AF6, a lemma

Tag 0AF6 in the Stacks Project.

AlgebraicGeometry.Space.FormalGlueingSituation.bijective_formalGlueingFunctor_map_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/FormalGlueingSpacesSeparatedBijection.lean, line 59.

In a formal glueing situation, the functor of Stacks 0AF3 is bijective on morphisms X'₁ ⟶ X'₂ of algebraic spaces over X whenever X'₂ ⟶ X is separated.

theorem bijective_formalGlueingFunctor_map_of_isSeparated (D : FormalGlueingSituation B S hS)
    {X₁ X₂ : spacesOverX D} (hsep : IsSeparated B S hS X₂.obj.hom) :
    Function.Bijective fun a : X₁ ⟶ X₂ ↦ (formalGlueingFunctor D).1.map a

Sources

LeanAlgebraicGeometry.Space.FormalGlueingSituation.formalGlueingFunctor · AlgebraicGeometry.Space.FormalGlueingSituation.affineGlueingFunctor_isEquivalence · AlgebraicGeometry.Space.FormalGlueingSituation.closedGlueingFunctor_isEquivalence · AlgebraicGeometry.Space.FormalGlueingSituation.finiteGlueingFunctor_isEquivalence · AlgebraicGeometry.Space.FormalGlueingSituation.reflectsIsomorphisms_formalGlueingFunctor · AlgebraicGeometry.Space.FormalGlueingSituation.bijective_formalGlueingFunctor_map_of_isSeparated

Section81.12 Glueing and the Beauville-Laszlo theorem #

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

Tag 0F9N, an equation

Tag 0F9N in the Stacks Project.

BeauvilleLaszlo.Space.beauvilleLaszloGlueingSpaces, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueing.lean, line 303.

The canonical functor from spaces over X to cartesian gluing triples, including its natural comparison with all three base changes and the two induced arrows.

noncomputable def beauvilleLaszloGlueingSpaces
    (B : BigFppfSite.{u})
    (U' U X' X : Scheme.{u}) (hU' : B.Contains U')
    (hU : B.Contains U) (hX' : B.Contains X') (hX : B.Contains X)
    (gU : B.obj hU' ⟶ B.obj hU)
    (gX' : B.obj hU' ⟶ B.obj hX')
    (jU : B.obj hU ⟶ B.obj hX)
    (jX' : B.obj hX' ⟶ B.obj hX)
    (hcomm : gU ≫ jU = gX' ≫ jX') :
    GlueingFunctorSpec B U' U X' X hU' hU hX' hX gU gX' jU jX' hcomm

Tag 0F9P, a lemma

Tag 0F9P in the Stacks Project.

AlgebraicGeometry.Space.exists_etaleCovering_iff_isGlueable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/BeauvilleLaszlo.lean, line 804.

Glueability of an algebraic space can be checked on all affine schemes étale over it, or on one étale covering by affine schemes.

theorem exists_etaleCovering_iff_isGlueable
  {R : Type u} {R' : Type v} [CommRing R] [CommRing R']
  (g : R →+* R') (f : R)
  (_hglue : BeauvilleLaszlo.IsGlueingPair g f)
  (B : BigFppfSite.{u})
  (hX : B.Contains (Spec (.of R)))
  (Y : _root_.AlgebraicGeometry.AlgebraicSpaces B (Spec (.of R)) hX) :
  (∃ (I : Type (u + 1))
      (W : I → BigFppfOver B (Spec (.of R)) hX)
      (p : ∀ i, yoneda.obj (W i) ⟶ Y.1),
      IsEtaleCovering B (Spec (.of R)) hX
        (fun i ↦ yoneda.obj (W i)) p ∧
        ∀ i, IsAffine ((BigFppfOver.toScheme B (Spec (.of R)) hX).obj (W i)) ∧
          IsGlueableGlobalSections g f B hX (W i)) ↔
    IsGlueableAlgebraicSpace g f B hX Y

Tag 0F9Q, a lemma

Tag 0F9Q in the Stacks Project.

BeauvilleLaszlo.Space.isAffineSpace_components, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingAffine.lean, line 110. The attribute's comment: “the functor restricts to the affine subcategories”.

The gluing functor of Stacks 0F9N takes affine algebraic spaces to triples with affine components. All four schemes of the square are assumed affine, as they are in the Beauville--Laszlo situation, where they are the spectra of R, R_f, R' and R'_f.

theorem isAffineSpace_components
    (B : BigFppfSite.{u})
    (U' U X' X : Scheme.{u}) (hU' : B.Contains U')
    (hU : B.Contains U) (hX' : B.Contains X') (hX : B.Contains X)
    [IsAffine U'] [IsAffine U] [IsAffine X'] [IsAffine X]
    (gU : B.obj hU' ⟶ B.obj hU)
    (gX' : B.obj hU' ⟶ B.obj hX')
    (jU : B.obj hU ⟶ B.obj hX)
    (jX' : B.obj hX' ⟶ B.obj hX)
    (hcomm : gU ≫ jU = gX' ≫ jX')
    (G : GlueingFunctorSpec B U' U X' X hU' hU hX' hX gU gX' jU jX' hcomm)
    (Y : AlgebraicSpaces B X hX)
    (hY : AlgebraicGeometry.Space.IsAffineSpace B X hX Y.1) :
    affineComponents B U' U X' hU' hU hX' gU gX' (G.functor.obj Y)

BeauvilleLaszlo.Space.canonicalAffineGlueableRestriction_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingAffineCanonicalEquivalence.lean, line 63.

Stacks 0F9Q. For a Beauville--Laszlo glueing pair (g : R → R', f), the glueing functor of Stacks 0F9N restricts to an equivalence between the category of affine algebraic spaces over X = Spec R which are glueable for (g, f) and the full subcategory of those glueing triples (V, V', Y') over U ← U' → X' whose three components are affine.

The functor in question is BeauvilleLaszlo.Space.canonicalAffineGlueableRestriction, which is by definition the restriction of BeauvilleLaszlo.Space.beauvilleLaszloGlueingSpaces, the glueing functor of Stacks 0F9N, to those two full subcategories.

theorem canonicalAffineGlueableRestriction_isEquivalence {R R' : Type u} [CommRing R] [CommRing R']
    (g : R →+* R') (f : R) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R)))
    (hcomm : canGU g f B hU' hU ≫ canJU f B hU hX = canGX' g f B hU' hX' ≫ canJX' g B hX' hX)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) :
    (canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).IsEquivalence

BeauvilleLaszlo.Space.beauvilleLaszloAffineEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingAffineEquivalence.lean, line 1015.

Stacks 0F9Q. The glueing functor of Stacks 0F9N restricts to an equivalence between the affine algebraic spaces over X = Spec R which are glueable for the pair (R → R', f) and the cartesian glueing triples (V, V', Y') over U ← U' → X' whose three components are affine — together with the identification of the forward functor of that equivalence with the restriction of the glueing functor itself, which is what the statement of the tag asserts.

Faithfulness is Stacks 0F9S, fullness is BeauvilleLaszlo.Space.full_comp_glueingFunctor and essential surjectivity is BeauvilleLaszlo.Space.essSurj_affineGlueableRestriction; the equivalence is the one Mathlib builds out of the three, so its forward functor is the restricted glueing functor and the identification is BeauvilleLaszlo.Space.affineGlueableRestrictionCompIso.

noncomputable def beauvilleLaszloAffineEquivalence (f : R)
    (hpair : _root_.BeauvilleLaszlo.IsGlueingPair (algebraMap R R') f)
    (B : BigFppfSite.{u}) (hX : B.Contains (Spec (.of R)))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R')))
    (hU' : B.Contains (Spec (.of (Localization.Away ((algebraMap R R') f))))) :
    AffineGlueingEquivalenceSpec (algebraMap R R') f B
      (Spec (.of (Localization.Away ((algebraMap R R') f))))
      (Spec (.of (Localization.Away f))) (Spec (.of R')) hU' hU hX' hX
      (AlgebraicGeometry.Space.specSite B hU hU').hom
      (AlgebraicGeometry.Space.specSite B hX' hU').hom
      (beauvilleLaszloGlueingSpaces B (Spec (.of (Localization.Away ((algebraMap R R') f))))
        (Spec (.of (Localization.Away f))) (Spec (.of R')) (Spec (.of R)) hU' hU hX' hX
        (AlgebraicGeometry.Space.specSite B hU hU').hom
        (AlgebraicGeometry.Space.specSite B hX' hU').hom
        (AlgebraicGeometry.Space.specSite B hX hU).hom
        (AlgebraicGeometry.Space.specSite B hX hX').hom
        (specSite_square_comm f B hU' hU hX' hX)).functor

BeauvilleLaszlo.Space.essSurj_affineGlueableRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingAffineEssSurj.lean, line 276. The attribute's comment: “the restricted functor is essentially surjective”.

Stacks 0F9Q, the essential surjectivity clause. The restriction of a glueing functor of Stacks 0F9N to the affine algebraic spaces over Spec R which are glueable for the pair is essentially surjective onto the cartesian glueing triples with affine components.

theorem essSurj_affineGlueableRestriction {R R' : Type u} [CommRing R] [CommRing R']
    [Algebra R R'] (f : R)
    (hpair : _root_.BeauvilleLaszlo.IsGlueingPair (algebraMap R R') f)
    (B : BigFppfSite.{u})
    (hX : B.Contains (Spec (.of R)))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R')))
    (hU' : B.Contains (Spec (.of (Localization.Away ((algebraMap R R') f)))))
    (hcomm : (AlgebraicGeometry.Space.specSite B hU hU').hom ≫
          (AlgebraicGeometry.Space.specSite B hX hU).hom =
        (AlgebraicGeometry.Space.specSite B hX' hU').hom ≫
          (AlgebraicGeometry.Space.specSite B hX hX').hom)
    (G : GlueingFunctorSpec B (Spec (.of (Localization.Away ((algebraMap R R') f))))
      (Spec (.of (Localization.Away f))) (Spec (.of R')) (Spec (.of R)) hU' hU hX' hX
      (AlgebraicGeometry.Space.specSite B hU hU').hom
      (AlgebraicGeometry.Space.specSite B hX' hU').hom
      (AlgebraicGeometry.Space.specSite B hX hU).hom
      (AlgebraicGeometry.Space.specSite B hX hX').hom hcomm) :
    (affineGlueableRestriction (g := algebraMap R R') (f := f) G).EssSurj

Tag 0F9R, a lemma

Tag 0F9R in the Stacks Project.

BeauvilleLaszlo.Space.isFinite_iff_canonicalAffineGlueableRestriction_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingEquivalenceProperties.lean, line 503. The attribute's comment: “P = finite; morphisms of affine glueable spaces”.

Stacks 0F9R for P finite, on the glueing functor. Let (g : R → R', f) be a glueing pair and let F be the glueing functor of Stacks 0F9N restricted, as in Stacks 0F9Q, to the affine algebraic spaces over X = Spec R which are glueable for (g, f). A morphism φ of such spaces is finite if and only if the three components of the morphism of triples F.map φ, over U = Spec R_f, U' = Spec R'_{g f} and X' = Spec R', are finite.

theorem isFinite_iff_canonicalAffineGlueableRestriction_map
    {R R' : Type u} [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R)))
    (hcomm : canGU g f B hU' hU ≫ canJU f B hU hX = canGX' g f B hU' hX' ≫ canJX' g B hX' hX)
    {Y Z : (affineGlueableSpaces g f B hX).FullSubcategory} (φ : Y ⟶ Z) :
    AlgebraicGeometry.Space.IsFinite B (Spec (.of R)) hX φ.hom.hom ↔
      AlgebraicGeometry.Space.IsFinite B (Spec (.of (Localization.Away f))) hU
          ((overU B _ _ _ hU' hU hX' _ _).map
            ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
              φ).hom).hom ∧
        AlgebraicGeometry.Space.IsFinite B (Spec (.of (Localization.Away (g f)))) hU'
            ((overU' B _ _ _ hU' hU hX' _ _).map
              ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                φ).hom).hom ∧
          AlgebraicGeometry.Space.IsFinite B (Spec (.of R')) hX'
              ((overX' B _ _ _ hU' hU hX' _ _).map
                ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                  φ).hom).hom

BeauvilleLaszlo.Space.isFinite_affineGlueingEquivalence_inverse_map_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingEquivalenceProperties.lean, line 542. The attribute's comment: “P = finite; morphisms of triples with affine components”.

Stacks 0F9R for P finite, on the inverse equivalence. Let (g : R → R', f) be a glueing pair. For every morphism β of glueing triples over U ← U' → X' with affine components, the morphism of affine glueable algebraic spaces over X = Spec R corresponding to β under the equivalence of Stacks 0F9Q is finite if and only if the three components of β are finite.

theorem isFinite_affineGlueingEquivalence_inverse_map_iff
    {R R' : Type u} [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R)))
    (hcomm : canGU g f B hU' hU ≫ canJU f B hU hX = canGX' g f B hU' hX' ≫ canJX' g B hX' hX)
    {T₁ T₂ : (affineComponents B _ _ _ hU' hU hX' (canGU g f B hU' hU)
      (canGX' g f B hU' hX')).FullSubcategory} (β : T₁ ⟶ T₂) :
    AlgebraicGeometry.Space.IsFinite B (Spec (.of R)) hX
        ((affineGlueingEquivalence g f B hU' hU hX' hX hcomm hglue).equivalence.inverse.map
          β).hom.hom ↔
      AlgebraicGeometry.Space.IsFinite B (Spec (.of (Localization.Away f))) hU
          ((overU B _ _ _ hU' hU hX' _ _).map β.hom).hom ∧
        AlgebraicGeometry.Space.IsFinite B (Spec (.of (Localization.Away (g f)))) hU'
            ((overU' B _ _ _ hU' hU hX' _ _).map β.hom).hom ∧
          AlgebraicGeometry.Space.IsFinite B (Spec (.of R')) hX'
              ((overX' B _ _ _ hU' hU hX' _ _).map β.hom).hom

BeauvilleLaszlo.Space.isClosedImmersion_iff_canonicalAffineGlueableRestriction_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingEquivalenceProperties.lean, line 579. The attribute's comment: “P = closed immersion; morphisms of affine glueable spaces”.

Stacks 0F9R for P closed immersion, on the glueing functor. Let (g : R → R', f) be a glueing pair and let F be the glueing functor of Stacks 0F9N restricted, as in Stacks 0F9Q, to the affine algebraic spaces over X = Spec R which are glueable for (g, f). A morphism φ of such spaces is a closed immersion if and only if the three components of the morphism of triples F.map φ, over U = Spec R_f, U' = Spec R'_{g f} and X' = Spec R', are closed immersions.

theorem isClosedImmersion_iff_canonicalAffineGlueableRestriction_map
    {R R' : Type u} [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R)))
    (hcomm : canGU g f B hU' hU ≫ canJU f B hU hX = canGX' g f B hU' hX' ≫ canJX' g B hX' hX)
    {Y Z : (affineGlueableSpaces g f B hX).FullSubcategory} (φ : Y ⟶ Z) :
    AlgebraicGeometry.Space.IsClosedImmersion B (Spec (.of R)) hX φ.hom.hom ↔
      AlgebraicGeometry.Space.IsClosedImmersion B (Spec (.of (Localization.Away f))) hU
          ((overU B _ _ _ hU' hU hX' _ _).map
            ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
              φ).hom).hom ∧
        AlgebraicGeometry.Space.IsClosedImmersion B (Spec (.of (Localization.Away (g f)))) hU'
            ((overU' B _ _ _ hU' hU hX' _ _).map
              ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                φ).hom).hom ∧
          AlgebraicGeometry.Space.IsClosedImmersion B (Spec (.of R')) hX'
              ((overX' B _ _ _ hU' hU hX' _ _).map
                ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                  φ).hom).hom

BeauvilleLaszlo.Space.isClosedImmersion_affineGlueingEquivalence_inverse_map_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingEquivalenceProperties.lean, line 619. The attribute's comment: “P = closed immersion; morphisms of triples with affine components”.

Let (g : R → R', f) be a glueing pair. For every morphism β of glueing triples over U ← U' → X' with affine components, the morphism of affine glueable algebraic spaces over X = Spec R corresponding to β under the inverse of the glueing equivalence is a closed immersion if and only if the three components of β are closed immersions.

theorem isClosedImmersion_affineGlueingEquivalence_inverse_map_iff
    {R R' : Type u} [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R)))
    (hcomm : canGU g f B hU' hU ≫ canJU f B hU hX = canGX' g f B hU' hX' ≫ canJX' g B hX' hX)
    {T₁ T₂ : (affineComponents B _ _ _ hU' hU hX' (canGU g f B hU' hU)
      (canGX' g f B hU' hX')).FullSubcategory} (β : T₁ ⟶ T₂) :
    AlgebraicGeometry.Space.IsClosedImmersion B (Spec (.of R)) hX
        ((affineGlueingEquivalence g f B hU' hU hX' hX hcomm hglue).equivalence.inverse.map
          β).hom.hom ↔
      AlgebraicGeometry.Space.IsClosedImmersion B (Spec (.of (Localization.Away f))) hU
          ((overU B _ _ _ hU' hU hX' _ _).map β.hom).hom ∧
        AlgebraicGeometry.Space.IsClosedImmersion B (Spec (.of (Localization.Away (g f)))) hU'
            ((overU' B _ _ _ hU' hU hX' _ _).map β.hom).hom ∧
          AlgebraicGeometry.Space.IsClosedImmersion B (Spec (.of R')) hX'
              ((overX' B _ _ _ hU' hU hX' _ _).map β.hom).hom

BeauvilleLaszlo.Space.isFlat_iff_canonicalAffineGlueableRestriction_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingEquivalenceProperties.lean, line 657. The attribute's comment: “P = flat; morphisms of affine glueable spaces”.

Stacks 0F9R for P flat, on the glueing functor. Let (g : R → R', f) be a glueing pair and let F be the glueing functor of Stacks 0F9N restricted, as in Stacks 0F9Q, to the affine algebraic spaces over X = Spec R which are glueable for (g, f). A morphism φ of such spaces is flat if and only if the three components of the morphism of triples F.map φ, over U = Spec R_f, U' = Spec R'_{g f} and X' = Spec R', are flat.

theorem isFlat_iff_canonicalAffineGlueableRestriction_map
    {R R' : Type u} [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R)))
    (hcomm : canGU g f B hU' hU ≫ canJU f B hU hX = canGX' g f B hU' hX' ≫ canJX' g B hX' hX)
    {Y Z : (affineGlueableSpaces g f B hX).FullSubcategory} (φ : Y ⟶ Z) :
    AlgebraicGeometry.Space.IsFlat B (Spec (.of R)) hX φ.hom.hom ↔
      AlgebraicGeometry.Space.IsFlat B (Spec (.of (Localization.Away f))) hU
          ((overU B _ _ _ hU' hU hX' _ _).map
            ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
              φ).hom).hom ∧
        AlgebraicGeometry.Space.IsFlat B (Spec (.of (Localization.Away (g f)))) hU'
            ((overU' B _ _ _ hU' hU hX' _ _).map
              ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                φ).hom).hom ∧
          AlgebraicGeometry.Space.IsFlat B (Spec (.of R')) hX'
              ((overX' B _ _ _ hU' hU hX' _ _).map
                ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                  φ).hom).hom

BeauvilleLaszlo.Space.isFlat_affineGlueingEquivalence_inverse_map_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingEquivalenceProperties.lean, line 698. The attribute's comment: “P = flat; morphisms of triples with affine components”.

Stacks 0F9R for P flat, on the inverse equivalence. Let (g : R → R', f) be a glueing pair. For every morphism β of glueing triples over U ← U' → X' with affine components, the morphism of affine glueable algebraic spaces over X = Spec R corresponding to β under the equivalence of Stacks 0F9Q is flat if and only if the three components of β are flat.

theorem isFlat_affineGlueingEquivalence_inverse_map_iff
    {R R' : Type u} [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R)))
    (hcomm : canGU g f B hU' hU ≫ canJU f B hU hX = canGX' g f B hU' hX' ≫ canJX' g B hX' hX)
    {T₁ T₂ : (affineComponents B _ _ _ hU' hU hX' (canGU g f B hU' hU)
      (canGX' g f B hU' hX')).FullSubcategory} (β : T₁ ⟶ T₂) :
    AlgebraicGeometry.Space.IsFlat B (Spec (.of R)) hX
        ((affineGlueingEquivalence g f B hU' hU hX' hX hcomm hglue).equivalence.inverse.map
          β).hom.hom ↔
      AlgebraicGeometry.Space.IsFlat B (Spec (.of (Localization.Away f))) hU
          ((overU B _ _ _ hU' hU hX' _ _).map β.hom).hom ∧
        AlgebraicGeometry.Space.IsFlat B (Spec (.of (Localization.Away (g f)))) hU'
            ((overU' B _ _ _ hU' hU hX' _ _).map β.hom).hom ∧
          AlgebraicGeometry.Space.IsFlat B (Spec (.of R')) hX'
              ((overX' B _ _ _ hU' hU hX' _ _).map β.hom).hom

BeauvilleLaszlo.Space.isFiniteType_iff_canonicalAffineGlueableRestriction_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingEquivalenceProperties.lean, line 737. The attribute's comment: “P = finite type; morphisms of affine glueable spaces”.

Stacks 0F9R for P finite type, on the glueing functor. Let (g : R → R', f) be a glueing pair and let F be the glueing functor of Stacks 0F9N restricted, as in Stacks 0F9Q, to the affine algebraic spaces over X = Spec R which are glueable for (g, f). A morphism φ of such spaces is of finite type if and only if the three components of the morphism of triples F.map φ, over U = Spec R_f, U' = Spec R'_{g f} and X' = Spec R', are of finite type.

theorem isFiniteType_iff_canonicalAffineGlueableRestriction_map
    {R R' : Type u} [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R)))
    (hcomm : canGU g f B hU' hU ≫ canJU f B hU hX = canGX' g f B hU' hX' ≫ canJX' g B hX' hX)
    {Y Z : (affineGlueableSpaces g f B hX).FullSubcategory} (φ : Y ⟶ Z) :
    AlgebraicGeometry.Space.IsFiniteType B (Spec (.of R)) hX φ.hom.hom ↔
      AlgebraicGeometry.Space.IsFiniteType B (Spec (.of (Localization.Away f))) hU
          ((overU B _ _ _ hU' hU hX' _ _).map
            ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
              φ).hom).hom ∧
        AlgebraicGeometry.Space.IsFiniteType B (Spec (.of (Localization.Away (g f)))) hU'
            ((overU' B _ _ _ hU' hU hX' _ _).map
              ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                φ).hom).hom ∧
          AlgebraicGeometry.Space.IsFiniteType B (Spec (.of R')) hX'
              ((overX' B _ _ _ hU' hU hX' _ _).map
                ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                  φ).hom).hom

BeauvilleLaszlo.Space.isFiniteType_affineGlueingEquivalence_inverse_map_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingEquivalenceProperties.lean, line 777. The attribute's comment: “P = finite type; morphisms of triples with affine components”.

Stacks 0F9R for P finite type, on the inverse equivalence. Let (g : R → R', f) be a glueing pair. For every morphism β of glueing triples over U ← U' → X' with affine components, the morphism of affine glueable algebraic spaces over X = Spec R corresponding to β under the equivalence of Stacks 0F9Q is of finite type if and only if the three components of β are of finite type.

theorem isFiniteType_affineGlueingEquivalence_inverse_map_iff
    {R R' : Type u} [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R)))
    (hcomm : canGU g f B hU' hU ≫ canJU f B hU hX = canGX' g f B hU' hX' ≫ canJX' g B hX' hX)
    {T₁ T₂ : (affineComponents B _ _ _ hU' hU hX' (canGU g f B hU' hU)
      (canGX' g f B hU' hX')).FullSubcategory} (β : T₁ ⟶ T₂) :
    AlgebraicGeometry.Space.IsFiniteType B (Spec (.of R)) hX
        ((affineGlueingEquivalence g f B hU' hU hX' hX hcomm hglue).equivalence.inverse.map
          β).hom.hom ↔
      AlgebraicGeometry.Space.IsFiniteType B (Spec (.of (Localization.Away f))) hU
          ((overU B _ _ _ hU' hU hX' _ _).map β.hom).hom ∧
        AlgebraicGeometry.Space.IsFiniteType B (Spec (.of (Localization.Away (g f)))) hU'
            ((overU' B _ _ _ hU' hU hX' _ _).map β.hom).hom ∧
          AlgebraicGeometry.Space.IsFiniteType B (Spec (.of R')) hX'
              ((overX' B _ _ _ hU' hU hX' _ _).map β.hom).hom

BeauvilleLaszlo.Space.isFlat_and_isFinitePresentation_iff_canonicalAffineGlueableRestriction_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingEquivalenceProperties.lean, line 815. The attribute's comment: “P = flat and finite presentation; morphisms of affine glueable spaces”.

Stacks 0F9R for P flat and finite presentation, on the glueing functor. Let (g : R → R', f) be a glueing pair and let F be the glueing functor of Stacks 0F9N restricted, as in Stacks 0F9Q, to the affine algebraic spaces over X = Spec R which are glueable for (g, f). A morphism φ of such spaces is flat and of finite presentation if and only if the three components of the morphism of triples F.map φ, over U = Spec R_f, U' = Spec R'_{g f} and X' = Spec R', are flat and of finite presentation.

theorem isFlat_and_isFinitePresentation_iff_canonicalAffineGlueableRestriction_map
    {R R' : Type u} [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R)))
    (hcomm : canGU g f B hU' hU ≫ canJU f B hU hX = canGX' g f B hU' hX' ≫ canJX' g B hX' hX)
    {Y Z : (affineGlueableSpaces g f B hX).FullSubcategory} (φ : Y ⟶ Z) :
    (AlgebraicGeometry.Space.IsFlat B (Spec (.of R)) hX φ.hom.hom ∧
        AlgebraicGeometry.Space.IsFinitePresentation B (Spec (.of R)) hX φ.hom.hom) ↔
      (AlgebraicGeometry.Space.IsFlat B (Spec (.of (Localization.Away f))) hU
            ((overU B _ _ _ hU' hU hX' _ _).map
              ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                φ).hom).hom ∧
          AlgebraicGeometry.Space.IsFinitePresentation B (Spec (.of (Localization.Away f))) hU
            ((overU B _ _ _ hU' hU hX' _ _).map
              ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                φ).hom).hom) ∧
        (AlgebraicGeometry.Space.IsFlat B (Spec (.of (Localization.Away (g f)))) hU'
              ((overU' B _ _ _ hU' hU hX' _ _).map
                ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                  φ).hom).hom ∧
            AlgebraicGeometry.Space.IsFinitePresentation B
                (Spec (.of (Localization.Away (g f)))) hU'
              ((overU' B _ _ _ hU' hU hX' _ _).map
                ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                  φ).hom).hom) ∧
          (AlgebraicGeometry.Space.IsFlat B (Spec (.of R')) hX'
                ((overX' B _ _ _ hU' hU hX' _ _).map
                  ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                    φ).hom).hom ∧
              AlgebraicGeometry.Space.IsFinitePresentation B (Spec (.of R')) hX'
                ((overX' B _ _ _ hU' hU hX' _ _).map
                  ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                    φ).hom).hom)

BeauvilleLaszlo.Space.isFlat_and_isFinitePresentation_affineGlueingEquivalence_inverse_map_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingEquivalenceProperties.lean, line 877. The attribute's comment: “P = flat and finite presentation; morphisms of triples with affine components”.

Stacks 0F9R for P flat and finite presentation, on the inverse equivalence. Let (g : R → R', f) be a glueing pair. For every morphism β of glueing triples over U ← U' → X' with affine components, the morphism of affine glueable algebraic spaces over X = Spec R corresponding to β under the equivalence of Stacks 0F9Q is flat and of finite presentation if and only if the three components of β are flat and of finite presentation.

theorem isFlat_and_isFinitePresentation_affineGlueingEquivalence_inverse_map_iff
    {R R' : Type u} [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R)))
    (hcomm : canGU g f B hU' hU ≫ canJU f B hU hX = canGX' g f B hU' hX' ≫ canJX' g B hX' hX)
    {T₁ T₂ : (affineComponents B _ _ _ hU' hU hX' (canGU g f B hU' hU)
      (canGX' g f B hU' hX')).FullSubcategory} (β : T₁ ⟶ T₂) :
    (AlgebraicGeometry.Space.IsFlat B (Spec (.of R)) hX
        ((affineGlueingEquivalence g f B hU' hU hX' hX hcomm hglue).equivalence.inverse.map
          β).hom.hom ∧
      AlgebraicGeometry.Space.IsFinitePresentation B (Spec (.of R)) hX
        ((affineGlueingEquivalence g f B hU' hU hX' hX hcomm hglue).equivalence.inverse.map
          β).hom.hom) ↔
      (AlgebraicGeometry.Space.IsFlat B (Spec (.of (Localization.Away f))) hU
            ((overU B _ _ _ hU' hU hX' _ _).map β.hom).hom ∧
          AlgebraicGeometry.Space.IsFinitePresentation B (Spec (.of (Localization.Away f))) hU
            ((overU B _ _ _ hU' hU hX' _ _).map β.hom).hom) ∧
        (AlgebraicGeometry.Space.IsFlat B (Spec (.of (Localization.Away (g f)))) hU'
              ((overU' B _ _ _ hU' hU hX' _ _).map β.hom).hom ∧
            AlgebraicGeometry.Space.IsFinitePresentation B
                (Spec (.of (Localization.Away (g f)))) hU'
              ((overU' B _ _ _ hU' hU hX' _ _).map β.hom).hom) ∧
          (AlgebraicGeometry.Space.IsFlat B (Spec (.of R')) hX'
                ((overX' B _ _ _ hU' hU hX' _ _).map β.hom).hom ∧
              AlgebraicGeometry.Space.IsFinitePresentation B (Spec (.of R')) hX'
                ((overX' B _ _ _ hU' hU hX' _ _).map β.hom).hom)

BeauvilleLaszlo.Space.isEtale_iff_canonicalAffineGlueableRestriction_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingEquivalenceProperties.lean, line 932. The attribute's comment: “P = étale; morphisms of affine glueable spaces”.

Stacks 0F9R for P étale, on the glueing functor. Let (g : R → R', f) be a glueing pair and let F be the glueing functor of Stacks 0F9N restricted, as in Stacks 0F9Q, to the affine algebraic spaces over X = Spec R which are glueable for (g, f). A morphism φ of such spaces is étale if and only if the three components of the morphism of triples F.map φ, over U = Spec R_f, U' = Spec R'_{g f} and X' = Spec R', are étale.

theorem isEtale_iff_canonicalAffineGlueableRestriction_map
    {R R' : Type u} [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R)))
    (hcomm : canGU g f B hU' hU ≫ canJU f B hU hX = canGX' g f B hU' hX' ≫ canJX' g B hX' hX)
    {Y Z : (affineGlueableSpaces g f B hX).FullSubcategory} (φ : Y ⟶ Z) :
    AlgebraicGeometry.Space.IsEtale B (Spec (.of R)) hX φ.hom.hom ↔
      AlgebraicGeometry.Space.IsEtale B (Spec (.of (Localization.Away f))) hU
          ((overU B _ _ _ hU' hU hX' _ _).map
            ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
              φ).hom).hom ∧
        AlgebraicGeometry.Space.IsEtale B (Spec (.of (Localization.Away (g f)))) hU'
            ((overU' B _ _ _ hU' hU hX' _ _).map
              ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                φ).hom).hom ∧
          AlgebraicGeometry.Space.IsEtale B (Spec (.of R')) hX'
              ((overX' B _ _ _ hU' hU hX' _ _).map
                ((canonicalAffineGlueableRestriction g f B hU' hU hX' hX hcomm).map
                  φ).hom).hom

BeauvilleLaszlo.Space.isEtale_affineGlueingEquivalence_inverse_map_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingEquivalenceProperties.lean, line 973. The attribute's comment: “P = étale; morphisms of triples with affine components”.

Stacks 0F9R for P étale, on the inverse equivalence. Let (g : R → R', f) be a glueing pair. For every morphism β of glueing triples over U ← U' → X' with affine components, the morphism of affine glueable algebraic spaces over X = Spec R corresponding to β under the equivalence of Stacks 0F9Q is étale if and only if the three components of β are étale.

theorem isEtale_affineGlueingEquivalence_inverse_map_iff
    {R R' : Type u} [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R)))
    (hcomm : canGU g f B hU' hU ≫ canJU f B hU hX = canGX' g f B hU' hX' ≫ canJX' g B hX' hX)
    {T₁ T₂ : (affineComponents B _ _ _ hU' hU hX' (canGU g f B hU' hU)
      (canGX' g f B hU' hX')).FullSubcategory} (β : T₁ ⟶ T₂) :
    AlgebraicGeometry.Space.IsEtale B (Spec (.of R)) hX
        ((affineGlueingEquivalence g f B hU' hU hX' hX hcomm hglue).equivalence.inverse.map
          β).hom.hom ↔
      AlgebraicGeometry.Space.IsEtale B (Spec (.of (Localization.Away f))) hU
          ((overU B _ _ _ hU' hU hX' _ _).map β.hom).hom ∧
        AlgebraicGeometry.Space.IsEtale B (Spec (.of (Localization.Away (g f)))) hU'
            ((overU' B _ _ _ hU' hU hX' _ _).map β.hom).hom ∧
          AlgebraicGeometry.Space.IsEtale B (Spec (.of R')) hX'
              ((overX' B _ _ _ hU' hU hX' _ _).map β.hom).hom

BeauvilleLaszlo.isFinite_iff_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingProperties.lean, line 191. The attribute's comment: “P = finite”.

Let (R → R', f) be a glueing pair. A morphism h : Spec B → Spec A of schemes over X = Spec R is finite if and only if its base changes to U = Spec R_f, U' = Spec R'_f and X' = Spec R', the three components of its image under the glueing functor of Stacks 0F9N, are finite.

theorem isFinite_iff_baseChange (f : R) (hglue : IsGlueingPair (algebraMap R R') f)
    (h : Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R B))) ⟶
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A)))) :
    IsFinite h.left ↔
      IsFinite ((Over.pullback (Spec.map (CommRingCat.ofHom
          (algebraMap R (Localization.Away f))))).map h).left ∧
        IsFinite ((Over.pullback (Spec.map (CommRingCat.ofHom
            (algebraMap R (Localization.Away (algebraMap R R' f)))))).map h).left ∧
          IsFinite ((Over.pullback (Spec.map (CommRingCat.ofHom
            (algebraMap R R')))).map h).left

BeauvilleLaszlo.isClosedImmersion_iff_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingProperties.lean, line 220. The attribute's comment: “P = closed immersion”.

Let (R → R', f) be a glueing pair. A morphism h : Spec B → Spec A of schemes over X = Spec R is a closed immersion if and only if its base changes to U = Spec R_f, U' = Spec R'_f and X' = Spec R', the three components of its image under the glueing functor of Stacks 0F9N, are closed immersions.

theorem isClosedImmersion_iff_baseChange (f : R) (hglue : IsGlueingPair (algebraMap R R') f)
    (h : Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R B))) ⟶
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A)))) :
    IsClosedImmersion h.left ↔
      IsClosedImmersion ((Over.pullback (Spec.map (CommRingCat.ofHom
          (algebraMap R (Localization.Away f))))).map h).left ∧
        IsClosedImmersion ((Over.pullback (Spec.map (CommRingCat.ofHom
            (algebraMap R (Localization.Away (algebraMap R R' f)))))).map h).left ∧
          IsClosedImmersion ((Over.pullback (Spec.map (CommRingCat.ofHom
            (algebraMap R R')))).map h).left

BeauvilleLaszlo.flat_iff_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingProperties.lean, line 241. The attribute's comment: “P = flat”.

Let (R → R', f) be a glueing pair and let the R-algebra A be glueable for it. A morphism h : Spec B → Spec A of schemes over X = Spec R is flat if and only if its base changes to U = Spec R_f, U' = Spec R'_f and X' = Spec R', the three components of its image under the glueing functor of Stacks 0F9N, are flat.

theorem flat_iff_baseChange (f : R) (hglue : IsGlueingPair (algebraMap R R') f)
    (hA : (beauvilleLaszloModuleSequence (S := R') A f).ShortExact)
    (h : Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R B))) ⟶
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A)))) :
    Flat h.left ↔
      Flat ((Over.pullback (Spec.map (CommRingCat.ofHom
          (algebraMap R (Localization.Away f))))).map h).left ∧
        Flat ((Over.pullback (Spec.map (CommRingCat.ofHom
            (algebraMap R (Localization.Away (algebraMap R R' f)))))).map h).left ∧
          Flat ((Over.pullback (Spec.map (CommRingCat.ofHom
            (algebraMap R R')))).map h).left

BeauvilleLaszlo.locallyOfFiniteType_iff_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingProperties.lean, line 262. The attribute's comment: “P = finite type”.

Let (R → R', f) be a glueing pair. A morphism h : Spec B → Spec A of schemes over X = Spec R is locally of finite type if and only if its base changes to U = Spec R_f, U' = Spec R'_f and X' = Spec R', the three components of its image under the glueing functor of Stacks 0F9N, are. A morphism of affine schemes is of finite type exactly when it is locally of finite type, being quasi-compact.

theorem locallyOfFiniteType_iff_baseChange (f : R) (hglue : IsGlueingPair (algebraMap R R') f)
    (h : Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R B))) ⟶
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A)))) :
    LocallyOfFiniteType h.left ↔
      LocallyOfFiniteType ((Over.pullback (Spec.map (CommRingCat.ofHom
          (algebraMap R (Localization.Away f))))).map h).left ∧
        LocallyOfFiniteType ((Over.pullback (Spec.map (CommRingCat.ofHom
            (algebraMap R (Localization.Away (algebraMap R R' f)))))).map h).left ∧
          LocallyOfFiniteType ((Over.pullback (Spec.map (CommRingCat.ofHom
            (algebraMap R R')))).map h).left

BeauvilleLaszlo.flat_and_locallyOfFinitePresentation_iff_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingProperties.lean, line 284. The attribute's comment: “P = flat and finite presentation”.

Let (R → R', f) be a glueing pair and let the R-algebra A be glueable for it. A morphism h : Spec B → Spec A of schemes over X = Spec R is flat and locally of finite presentation if and only if its base changes to U = Spec R_f, U' = Spec R'_f and X' = Spec R', the three components of its image under the glueing functor of Stacks 0F9N, are. A morphism of affine schemes is of finite presentation exactly when it is locally of finite presentation, being quasi-compact and quasi-separated.

theorem flat_and_locallyOfFinitePresentation_iff_baseChange (f : R)
    (hglue : IsGlueingPair (algebraMap R R') f)
    (hA : (beauvilleLaszloModuleSequence (S := R') A f).ShortExact)
    (h : Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R B))) ⟶
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A)))) :
    (Flat h.left ∧ LocallyOfFinitePresentation h.left) ↔
      (Flat ((Over.pullback (Spec.map (CommRingCat.ofHom
          (algebraMap R (Localization.Away f))))).map h).left ∧
        LocallyOfFinitePresentation ((Over.pullback (Spec.map (CommRingCat.ofHom
          (algebraMap R (Localization.Away f))))).map h).left) ∧
      (Flat ((Over.pullback (Spec.map (CommRingCat.ofHom
          (algebraMap R (Localization.Away (algebraMap R R' f)))))).map h).left ∧
        LocallyOfFinitePresentation ((Over.pullback (Spec.map (CommRingCat.ofHom
          (algebraMap R (Localization.Away (algebraMap R R' f)))))).map h).left) ∧
      (Flat ((Over.pullback (Spec.map (CommRingCat.ofHom
          (algebraMap R R')))).map h).left ∧
        LocallyOfFinitePresentation ((Over.pullback (Spec.map (CommRingCat.ofHom
          (algebraMap R R')))).map h).left)

BeauvilleLaszlo.etale_iff_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingProperties.lean, line 318. The attribute's comment: “P = étale”.

Let (R → R', f) be a glueing pair and let the R-algebra A be glueable for it. A morphism h : Spec B → Spec A of schemes over X = Spec R is étale if and only if its base changes to U = Spec R_f, U' = Spec R'_f and X' = Spec R', the three components of its image under the glueing functor of Stacks 0F9N, are étale.

theorem etale_iff_baseChange (f : R) (hglue : IsGlueingPair (algebraMap R R') f)
    (hA : (beauvilleLaszloModuleSequence (S := R') A f).ShortExact)
    (h : Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R B))) ⟶
      Over.mk (Spec.map (CommRingCat.ofHom (algebraMap R A)))) :
    Etale h.left ↔
      Etale ((Over.pullback (Spec.map (CommRingCat.ofHom
          (algebraMap R (Localization.Away f))))).map h).left ∧
        Etale ((Over.pullback (Spec.map (CommRingCat.ofHom
            (algebraMap R (Localization.Away (algebraMap R R' f)))))).map h).left ∧
          Etale ((Over.pullback (Spec.map (CommRingCat.ofHom
            (algebraMap R R')))).map h).left

Tag 0F9S, a lemma

Tag 0F9S in the Stacks Project.

BeauvilleLaszlo.Space.beauvilleLaszloGlueingSpaces_map_injective_of_isGlueable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingFaithful.lean, line 669.

The Beauville--Laszlo gluing functor is faithful on glueable algebraic spaces over Spec R.

theorem beauvilleLaszloGlueingSpaces_map_injective_of_isGlueable
    (R R' : Type u) [CommRing R] [CommRing R']
    (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f)
    (B : AlgebraicGeometry.BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R')))
    (hX : B.Contains (Spec (.of R))) :
    let U' : Scheme.{u} := Spec (.of (Localization.Away (g f)))
    let U : Scheme.{u} := Spec (.of (Localization.Away f))
    let X' : Scheme.{u} := Spec (.of R')
    let X : Scheme.{u} := Spec (.of R)
    let gU : B.obj hU' ⟶ B.obj hU :=
      ⟨Spec.map (CommRingCat.ofHom (Localization.awayMap g f))⟩
    let gX' : B.obj hU' ⟶ B.obj hX' :=
      ⟨Spec.map (CommRingCat.ofHom (algebraMap R' (Localization.Away (g f))))⟩
    let jU : B.obj hU ⟶ B.obj hX :=
      ⟨Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f)))⟩
    let jX' : B.obj hX' ⟶ B.obj hX :=
      ⟨Spec.map (CommRingCat.ofHom g)⟩
    ∀ (hcomm : gU ≫ jU = gX' ≫ jX')
      (Y Z : _root_.AlgebraicGeometry.AlgebraicSpaces B X hX),
      _root_.AlgebraicGeometry.Space.IsGlueableAlgebraicSpace g f B hX Y →
      _root_.AlgebraicGeometry.Space.IsGlueableAlgebraicSpace g f B hX Z →
      Function.Injective (fun (φ : Y ⟶ Z) ↦
        (BeauvilleLaszlo.Space.beauvilleLaszloGlueingSpaces
          B U' U X' X hU' hU hX' hX gU gX' jU jX' hcomm).functor.map φ)

Tag 0F9T, a lemma

Tag 0F9T in the Stacks Project.

BeauvilleLaszlo.Space.beauvilleLaszloGlueingSpaces_map_surjective_of_isGlueable_of_isAffineHom_diag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingFullyFaithfulComplete.lean, line 316. The attribute's comment: “fullness”.

Stacks 0F9T, fullness. For a Beauville--Laszlo glueing pair (g : R → R', f), a morphism of glueing triples between the images of two algebraic spaces over Spec R which are glueable for (g, f) comes from a morphism of algebraic spaces, provided the target has affine diagonal.

Nothing beyond the glueing pair and these two conditions is assumed: the equivalence of the affine case is BeauvilleLaszlo.Space.affineGlueingEquivalence (Stacks 0F9Q) and étaleness of a morphism of affine glueable spaces in terms of its components is BeauvilleLaszlo.Space.isEtale_iff_isEtale_glueingComponents (Stacks 0F9R for the property "étale"); both are supplied to beauvilleLaszloGlueingSpaces_map_surjective_of_isGlueable_of_affineDiagonal.

theorem beauvilleLaszloGlueingSpaces_map_surjective_of_isGlueable_of_isAffineHom_diag
    (R R' : Type u) [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R))) :
    let U' : Scheme.{u} := Spec (.of (Localization.Away (g f)))
    let U : Scheme.{u} := Spec (.of (Localization.Away f))
    let X' : Scheme.{u} := Spec (.of R')
    let X : Scheme.{u} := Spec (.of R)
    let gU : B.obj hU' ⟶ B.obj hU :=
      ⟨Spec.map (CommRingCat.ofHom (Localization.awayMap g f))⟩
    let gX' : B.obj hU' ⟶ B.obj hX' :=
      ⟨Spec.map (CommRingCat.ofHom (algebraMap R' (Localization.Away (g f))))⟩
    let jU : B.obj hU ⟶ B.obj hX :=
      ⟨Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f)))⟩
    let jX' : B.obj hX' ⟶ B.obj hX := ⟨Spec.map (CommRingCat.ofHom g)⟩
    ∀ (hcomm : gU ≫ jU = gX' ≫ jX') (Y Z : AlgebraicSpaces B X hX),
      AlgebraicGeometry.Space.IsGlueableAlgebraicSpace g f B hX Y →
      AlgebraicGeometry.Space.IsGlueableAlgebraicSpace g f B hX Z →
      AlgebraicGeometry.Space.IsAffineHom B X hX (diag Z.1) →
      Function.Surjective (fun (φ : Y ⟶ Z) ↦
        (beauvilleLaszloGlueingSpaces
          B U' U X' X hU' hU hX' hX gU gX' jU jX' hcomm).functor.map φ)

BeauvilleLaszlo.Space.beauvilleLaszloGlueingSpaces_map_bijective_of_isGlueable_of_isAffineHom_diag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingFullyFaithfulComplete.lean, line 357.

Stacks 0F9T. For a Beauville--Laszlo glueing pair (g : R → R', f), the glueing functor of Stacks 0F9N is fully faithful on the full subcategory of algebraic spaces Y/X which are glueable for (g, f) and have affine diagonal Y → Y ×_X Y: the map it induces on each hom-set between two such objects is bijective.

Injectivity is Stacks 0F9S, which needs glueability alone; surjectivity needs affineness of the diagonal of the target alone, and is beauvilleLaszloGlueingSpaces_map_surjective_of_isGlueable_of_isAffineHom_diag.

theorem beauvilleLaszloGlueingSpaces_map_bijective_of_isGlueable_of_isAffineHom_diag
    (R R' : Type u) [CommRing R] [CommRing R'] (g : R →+* R') (f : R)
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f) (B : BigFppfSite.{u})
    (hU' : B.Contains (Spec (.of (Localization.Away (g f)))))
    (hU : B.Contains (Spec (.of (Localization.Away f))))
    (hX' : B.Contains (Spec (.of R'))) (hX : B.Contains (Spec (.of R))) :
    let U' : Scheme.{u} := Spec (.of (Localization.Away (g f)))
    let U : Scheme.{u} := Spec (.of (Localization.Away f))
    let X' : Scheme.{u} := Spec (.of R')
    let X : Scheme.{u} := Spec (.of R)
    let gU : B.obj hU' ⟶ B.obj hU :=
      ⟨Spec.map (CommRingCat.ofHom (Localization.awayMap g f))⟩
    let gX' : B.obj hU' ⟶ B.obj hX' :=
      ⟨Spec.map (CommRingCat.ofHom (algebraMap R' (Localization.Away (g f))))⟩
    let jU : B.obj hU ⟶ B.obj hX :=
      ⟨Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f)))⟩
    let jX' : B.obj hX' ⟶ B.obj hX := ⟨Spec.map (CommRingCat.ofHom g)⟩
    ∀ (hcomm : gU ≫ jU = gX' ≫ jX') (Y Z : AlgebraicSpaces B X hX),
      AlgebraicGeometry.Space.IsGlueableAlgebraicSpace g f B hX Y →
      AlgebraicGeometry.Space.IsGlueableAlgebraicSpace g f B hX Z →
      AlgebraicGeometry.Space.IsAffineHom B X hX (diag Y.1) →
      AlgebraicGeometry.Space.IsAffineHom B X hX (diag Z.1) →
      Function.Bijective (fun (φ : Y ⟶ Z) ↦
        (beauvilleLaszloGlueingSpaces
          B U' U X' X hU' hU hX' hX gU gX' jU jX' hcomm).functor.map φ)

Declarations registered for the tag:

BeauvilleLaszlo.Space.beauvilleLaszloGlueingSpaces_map_injective_of_isGlueable, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/BeauvilleLaszloGlueingFullyFaithful.lean, line 1131 (StacksFrontier): “faithfulness”.

Tag 0F9U, a lemma

Tag 0F9U in the Stacks Project.

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

Stacks 0F9U. Let (g : R → R', f) be a glueing pair, and let X = Spec R, U = Spec R_f, X' = Spec R' and U' = Spec R'_{g f} be the four corners of its square, all in the big fppf site B. Any cartesian triple (V, V', Y') of algebraic spaces over U ← U' → X' whose three components are quasi-affine is isomorphic to the image, under the gluing functor of Stacks 0F9N, of an algebraic space Y over X which is separated over X.

theorem exists_isSeparatedOver_iso_of_isQuasiAffineComponents
    (hglue : _root_.BeauvilleLaszlo.IsGlueingPair g f)
    (Z : GlueingData B (Spec (.of (Localization.Away (g f))))
      (Spec (.of (Localization.Away f))) (Spec (.of R')) hU' hU hX'
      (canGU g f B hU' hU) (canGX' g f B hU' hX'))
    (hZ : quasiAffineComponents B (Spec (.of (Localization.Away (g f))))
      (Spec (.of (Localization.Away f))) (Spec (.of R')) hU' hU hX'
      (canGU g f B hU' hU) (canGX' g f B hU' hX') Z) :
    ∃ Y : AlgebraicSpaces B (Spec (.of R)) hX,
      AlgebraicGeometry.Space.IsSeparatedOver B (Spec (.of R)) hX Y.obj ∧
        Nonempty ((beauvilleLaszloGlueingSpaces B _ _ _ _ hU' hU hX' hX
          (canGU g f B hU' hU) (canGX' g f B hU' hX') (canJU f B hU hX) (canJX' g B hX' hX)
          (canonical_comm g f B hU' hU hX' hX)).functor.obj Y ≅ Z)

Sources

LeanBeauvilleLaszlo.Space.beauvilleLaszloGlueingSpaces · AlgebraicGeometry.Space.exists_etaleCovering_iff_isGlueable · BeauvilleLaszlo.Space.isAffineSpace_components · BeauvilleLaszlo.Space.canonicalAffineGlueableRestriction_isEquivalence · BeauvilleLaszlo.Space.beauvilleLaszloAffineEquivalence · BeauvilleLaszlo.Space.essSurj_affineGlueableRestriction · BeauvilleLaszlo.Space.isFinite_iff_canonicalAffineGlueableRestriction_map · BeauvilleLaszlo.Space.isFinite_affineGlueingEquivalence_inverse_map_iff

Section81.13 Coequalizers and glueing #

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

Tag 0AGG, a lemma

Tag 0AGG in the Stacks Project.

AlgebraicGeometry.Space.properKernelPairCoequalizers_of_core, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ProperKernelPairCoequalizer.lean, line 122. The attribute's comment: “all six clauses; clause (5) is proved from the others, while existence of the coequalizer and clauses (1) to (4) are carried in the hypothesis”.

Let g : Y ⟶ X be a proper morphism of algebraic spaces over S with X locally Noetherian and let R = Y ×_X Y with its two projections s, t : R ⟶ Y. Then s and t have a coequalizer X' in the category of algebraic spaces over S, and: (1) the morphism X' ⟶ X is finite; (2) the morphism Y ⟶ X' is proper; (3) the morphism Y ⟶ X' is surjective; (4) the morphism X' ⟶ X is universally injective; (5) if g is surjective, the morphism X' ⟶ X is a universal homeomorphism. Existence of the coequalizer and clauses (1) to (4) are the hypothesis hcore.

theorem properKernelPairCoequalizers_of_core
    (hcore : ProperKernelPairCoequalizerCore B S hS) :
    ProperKernelPairCoequalizers B S hS

AlgebraicGeometry.Space.properKernelPairCoequalizers_holds, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/ProperKernelPairSheafDescent.lean, line 207.

Stacks 0AGG. Let S be a scheme and let g : Y ⟶ X be a morphism of algebraic spaces over S with X locally Noetherian and g proper. Let R = Y ×_X Y with projections s, t : R ⟶ Y. There exists a coequalizer X' of s, t : R ⟶ Y in the category of algebraic spaces over S. Moreover 1. the morphism X' ⟶ X is finite; 2. the morphism Y ⟶ X' is proper; 3. the morphism Y ⟶ X' is surjective; 4. the morphism X' ⟶ X is universally injective; 5. if g is surjective, the morphism X' ⟶ X is a universal homeomorphism.

The statement AlgebraicGeometry.Space.ProperKernelPairCoequalizers consists of exactly these six clauses: existence of the coequalizer as an AlgebraicGeometry.Space.KernelPairCoequalizer (a colimit cofork of the kernel pair in the category of algebraic spaces over S), and clauses (1) to (5) for every such coequalizer. Everything is proved here, unconditionally: nothing is carried as a hypothesis. The two inputs of the proof, the proper case of Stacks 0GFW and the translation step of Stacks 0GG0, are the theorems AlgebraicGeometry.Space.descentEffectiveAlongProperSurjective and AlgebraicGeometry.Space.etaleSpaceDescentEffectiveOfSheafDescent.

theorem properKernelPairCoequalizers_holds : ProperKernelPairCoequalizers B S hS

Tag 0AGH, a situation

Tag 0AGH in the Stacks Project.

AlgebraicGeometry.Space.CoequalizerGlueSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/Coequalizers.lean, line 49.

Stacks 0AGH. The standing situation for the coequalizer construction: a locally Noetherian algebraic space X over S, a closed immersion i : Z ⟶ X with complementary open subspace U, and a proper morphism f : X' ⟶ X which is an isomorphism over U.

structure CoequalizerGlueSituation

Tag 0AGI, a lemma

Tag 0AGI in the Stacks Project.

AlgebraicGeometry.Space.CoequalizerGlueSituation.nonempty_glueCoequalizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/CoequalizerGlueing.lean, line 286. The attribute's comment: “existence of the coequalizer; this clause is Stacks 0AGG, carried as the hypothesis hAGG because 0AGG rests on 08AR, which the library does not have”.

Stacks 0AGI, existence of the coequalizer X₁ of s, t : R ⟶ Y in the category of algebraic spaces over S, for Y = X' ⨿ Z and R = Y ×_X Y.

theorem nonempty_glueCoequalizer
    (hAGG : ProperKernelPairCoequalizers T.B T.S T.hS)
    (hproper : IsProper T.B T.S T.hS T.glueMap.hom) :
    Nonempty (KernelPairCoequalizer T.B T.S T.hS T.glueMap)

AlgebraicGeometry.Space.CoequalizerGlueSituation.isFinite_glueCoequalizer_toTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/CoequalizerGlueing.lean, line 295. The attribute's comment: “the morphism to X is finite; this clause is part (1) of Stacks 0AGG, carried as the hypothesis hAGG”.

Stacks 0AGI, finiteness of X₁ ⟶ X.

theorem isFinite_glueCoequalizer_toTarget
    (hAGG : ProperKernelPairCoequalizers T.B T.S T.hS)
    (hproper : IsProper T.B T.S T.hS T.glueMap.hom)
    (D : KernelPairCoequalizer T.B T.S T.hS T.glueMap) :
    IsFinite T.B T.S T.hS D.toTarget.hom

AlgebraicGeometry.Space.CoequalizerGlueSituation.universalHomeomorphism_glueCoequalizer_toTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/CoequalizerGlueing.lean, line 307. The attribute's comment: “the morphism to X is a universal homeomorphism; part (5) of Stacks 0AGG is carried as the hypothesis hAGG, and its surjectivity input is proved here”.

Stacks 0AGI, the morphism X₁ ⟶ X is a universal homeomorphism. The surjectivity of g which part (5) of Stacks 0AGG asks for is supplied by AlgebraicGeometry.Space.CoequalizerGlueSituation.isSurjective_glueMap.

theorem universalHomeomorphism_glueCoequalizer_toTarget
    (hAGG : ProperKernelPairCoequalizers T.B T.S T.hS)
    (hproper : IsProper T.B T.S T.hS T.glueMap.hom)
    (D : KernelPairCoequalizer T.B T.S T.hS T.glueMap) :
    UniversalHomeomorphism T.B T.S T.hS D.toTarget.hom

AlgebraicGeometry.Space.CoequalizerGlueSituation.glueCoequalizer_closedSubspace_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/CoequalizerGlueing.lean, line 319. The attribute's comment: “Z lifts to the coequalizer; proved here”.

Stacks 0AGI, the closed immersion Z ⟶ X lifts to the coequalizer: the composition of the coproduct inclusion of Z with the quotient morphism is a lift. This clause is proved outright: it needs only that Y ⟶ X₁ ⟶ X is g, which is g on the summand Z.

theorem glueCoequalizer_closedSubspace_lift
    (D : KernelPairCoequalizer T.B T.S T.hS T.glueMap) :
    (coprod.inr ≫ D.π) ≫ D.toTarget = (ObjectProperty.homMk T.i : _ ⟶ T.targetSpace)

AlgebraicGeometry.Space.CoequalizerGlueSituation.exists_glueCoequalizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/CoequalizerGlueingUnconditional.lean, line 56.

Stacks 0AGI. In Situation 0AGH (X locally Noetherian over S, Z ⟶ X a closed immersion with complementary open U, f : X' ⟶ X proper and an isomorphism over U), let Y = X' ⨿ Z and R = Y ×_X Y with projections s, t : R ⟶ Y. There exists a coequalizer X₁ of s, t in the category of algebraic spaces over S; the morphism X₁ ⟶ X is finite and a universal homeomorphism, it is an isomorphism over U (its base change along U ⟶ X is an isomorphism), and Z ⟶ X lifts to X₁. Everything is proved: Stacks 0AGG is AlgebraicGeometry.Space.properKernelPairCoequalizers_holds.

theorem exists_glueCoequalizer :
    ∃ D : KernelPairCoequalizer T.B T.S T.hS T.glueMap,
      IsFinite T.B T.S T.hS D.toTarget.hom ∧
      UniversalHomeomorphism T.B T.S T.hS D.toTarget.hom ∧
      IsIso (pullback.snd D.toTarget.hom T.U.ι) ∧
      ∃ l : T.closedSpace ⟶ D.space, l ≫ D.toTarget = ObjectProperty.homMk T.i

Tag 0AGJ, an equation

Tag 0AGJ in the Stacks Project.

AlgebraicGeometry.Space.CoequalizerGlueSituation.ClosedSubspaceSystem.towerMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/CoequalizerGlueing.lean, line 396. The attribute's comment: “the morphism of the tower”.

Stacks 0AGJ. The morphism X_n ⟶ X_{n+1} of the tower X_1 ⟶ X_2 ⟶ X_3 ⟶ … ⟶ X, induced by the morphisms Y_n ⟶ Y_{n+1} and R_n ⟶ R_{n+1}.

def towerMap (n : ℕ) : (D n).space ⟶ (D (n + 1)).space

AlgebraicGeometry.Space.CoequalizerGlueSituation.ClosedSubspaceSystem.towerMap_comp_toTarget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/CoequalizerGlueing.lean, line 411. The attribute's comment: “the tower is a tower over X”.

Stacks 0AGJ. Each morphism of the tower X_1 ⟶ X_2 ⟶ X_3 ⟶ … ⟶ X is a morphism over X: the triangle formed with the two morphisms to X commutes.

theorem towerMap_comp_toTarget (n : ℕ) :
    N.towerMap D n ≫ (D (n + 1)).toTarget = (D n).toTarget

Tag 0AGK, a lemma

Tag 0AGK in the Stacks Project.

AlgebraicGeometry.Space.CoequalizerGlueSituation.exists_factorsThroughSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/CoequalizerGlueingUnconditional.lean, line 73.

Stacks 0AGK. In Situation 0AGH assume X quasi-compact. Let Z_n be the infinitesimal neighbourhoods of Z in X and X_n the coequalizers of the kernel pairs of X' ⨿ Z_n ⟶ X, forming the tower X_1 ⟶ X_2 ⟶ X_3 ⟶ … ⟶ X of Stacks 0AGJ (for any choice D of these coequalizers, which exist by Stacks 0AGI). Then for all n large enough there is an m such that X_n ⟶ X_{n+m} factors through a closed immersion X ⟶ X_{n+m}; the closed immersion is moreover a section of X_{n+m} ⟶ X. Everything is proved: Stacks 0AGG is AlgebraicGeometry.Space.properKernelPairCoequalizers_holds.

theorem exists_factorsThroughSection (hqc : IsQuasiCompactSpace T.B T.S T.hS T.X)
    (D : ∀ n, KernelPairCoequalizer T.B T.S T.hS (T.neighbourhoodSystem.glueMapAt n)) :
    ∃ n₀, ∀ n, n₀ ≤ n → ∃ m, T.neighbourhoodSystem.FactorsThroughSection D n m

Tag 0AGL, a remark

Tag 0AGL in the Stacks Project.

AlgebraicGeometry.Space.CoequalizerGlueSituation.exists_isEssentiallyConstantWith, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Pushouts/CoequalizerGlueingUnconditional.lean, line 85.

Stacks 0AGL. In Situation 0AGH with X quasi-compact, the system X_1 ⟶ X_2 ⟶ X_3 ⟶ … of Stacks 0AGJ (for any choice D of the coequalizers) is essentially constant with value X in the sense of Stacks 05PU, with respect to the cocone of the morphisms X_n ⟶ X. Everything is proved: Stacks 0AGG is AlgebraicGeometry.Space.properKernelPairCoequalizers_holds.

theorem exists_isEssentiallyConstantWith (hqc : IsQuasiCompactSpace T.B T.S T.hS T.X)
    (D : ∀ n, KernelPairCoequalizer T.B T.S T.hS (T.neighbourhoodSystem.glueMapAt n)) :
    ∃ (i : ℕ) (r : T.targetSpace ⟶ (D i).space),
      CategoryTheory.EssentiallyConstantInd.IsEssentiallyConstantWith
        (T.neighbourhoodSystem.towerDiagram D)
        (T.neighbourhoodSystem.towerCocone D) i r

Sources

LeanAlgebraicGeometry.Space.properKernelPairCoequalizers_of_core · AlgebraicGeometry.Space.properKernelPairCoequalizers_holds · AlgebraicGeometry.Space.CoequalizerGlueSituation · AlgebraicGeometry.Space.CoequalizerGlueSituation.nonempty_glueCoequalizer · AlgebraicGeometry.Space.CoequalizerGlueSituation.isFinite_glueCoequalizer_toTarget · AlgebraicGeometry.Space.CoequalizerGlueSituation.universalHomeomorphism_glueCoequalizer_toTarget · AlgebraicGeometry.Space.CoequalizerGlueSituation.glueCoequalizer_closedSubspace_lift · AlgebraicGeometry.Space.CoequalizerGlueSituation.exists_glueCoequalizer

Section81.14 Compactifications #

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

Tag 0F45, a lemma

Tag 0F45 in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_of_elementaryDistinguishedSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/SeparatedFromElementarySquare.lean, line 1235. The attribute's comment: “with the additional hypothesis that V ×_X V ⟶ V ×_Y V is closed; the source's hypothesis list is insufficient, see the counterexample in the module docstring”.

Stacks 0F45. A morphism of algebraic spaces g : X ⟶ Y over S is separated once an elementary distinguished square (U ⊆ X, f : V ⟶ X) has U ⟶ Y and V ⟶ Y separated and has the comparison maps U ×_X V ⟶ U ×_Y V and V ×_X V ⟶ V ×_Y V closed.

The second comparison map is not among the source's hypotheses: Lemma 81.14.1 asks only for U ×_X V ⟶ U ×_Y V to be closed, and its proof asserts that (V ×_Y V) ×_{X ×_Y X, Δ} X = V, which is false — that base change is V ×_X V. The source's hypothesis list is insufficient, and the counterexample in this module's docstring shows the extra hypothesis cannot be dropped. This statement is therefore the repaired one.

public theorem isSeparated_of_elementaryDistinguishedSquare
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X V Y : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : AlgebraicGeometry.IsAlgebraicSpace B S hS X)
    (hY : AlgebraicGeometry.IsAlgebraicSpace B S hS Y)
    (g : X ⟶ Y) (U : Subfunctor X) (f : V ⟶ X)
    (hsq : AlgebraicGeometry.Space.IsElementaryDistinguishedSquare B S hS hX U f)
    (hU : AlgebraicGeometry.Space.IsSeparated B S hS (U.ι ≫ g))
    (hV : AlgebraicGeometry.Space.IsSeparated B S hS (f ≫ g))
    (hUV : IsClosedMorphism B S hS (pullback.mapDesc U.ι f g))
    (hVV : IsClosedMorphism B S hS (pullback.mapDesc f f g)) :
    AlgebraicGeometry.Space.IsSeparated B S hS g

AlgebraicGeometry.Space.not_forall_isSeparated_of_isElementaryDistinguishedSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Perfect/SeparatedFromElementarySquareCounterexample.lean, line 553. The attribute's comment: “counterexample: the statement as published is false; the corrected statement, with V ×_X V ⟶ V ×_Y V also closed, is isSeparated_of_elementaryDistinguishedSquare”.

Stacks 0F45 as published is false. It is not true that a morphism g : X ⟶ Y of algebraic spaces over S is separated as soon as an elementary distinguished square (U ⊆ X, f : V ⟶ X) has U ⟶ Y and V ⟶ Y separated and U ×_X V ⟶ U ×_Y V closed. The counterexample is AlgebraicGeometry.AffineLineInvolution.exists_isElementaryDistinguishedSquare_not_isSeparated, over the field ℚ. The statement with the further hypothesis that V ×_X V ⟶ V ×_Y V is closed is AlgebraicGeometry.Space.isSeparated_of_elementaryDistinguishedSquare.

theorem not_forall_isSeparated_of_isElementaryDistinguishedSquare :
    ¬ ∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
      {X V Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
      (_hY : IsAlgebraicSpace B S hS Y) (g : X ⟶ Y) (U : Subfunctor X) (f : V ⟶ X),
      IsElementaryDistinguishedSquare B S hS hX U f →
      IsSeparated B S hS (U.ι ≫ g) → IsSeparated B S hS (f ≫ g) →
      IsClosedMorphism B S hS (pullback.mapDesc U.ι f g) → IsSeparated B S hS g

Tag 0F46, a lemma

Tag 0F46 in the Stacks Project.

AlgebraicGeometry.Space.exists_isAdmissibleBlowup_separating_strictTransforms_and_closures, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AdmissibleBlowupStrictTransformSeparationQcqs.lean, line 62.

Stacks 0F46. Let S be a scheme, let X be a quasi-compact and quasi-separated algebraic space over S and let U ⊆ X be a quasi-compact open subspace.

If Z₁, Z₂ ⊆ X are closed subspaces of finite presentation with Z₁ ∩ Z₂ ∩ U = ∅, then there is a U-admissible blowup b : X' ⟶ X such that the strict transforms of Z₁ and Z₂ are disjoint. The blowup is recorded with its centre Y, a finitely presented closed subspace of X disjoint from U in which b is the blowup, and the strict transforms are taken relative to the exceptional divisor b⁻¹Y.

If T₁, T₂ ⊆ |U| are disjoint constructible closed subsets, then there is a U-admissible blowup b : X' ⟶ X such that the closures of T₁ and T₂ in |X'| are disjoint, Tᵢ being read in |X'| through b, which is an isomorphism over U.

theorem exists_isAdmissibleBlowup_separating_strictTransforms_and_closures
    (hZ : B.Contains (⊤_ Scheme.{u})) {X : AlgebraicSpaces B S hS}
    (hXqc : IsQuasiCompactSpace B S hS X.1) (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (U : OpenSubspaces B S hS X.1) (hUqc : IsQuasiCompactSpace B S hS U.1.toFunctor) :
    (∀ Z₁ Z₂ : ClosedSubspaces B S hS X.1,
      IsFinitePresentation B S hS Z₁.1.ι → IsFinitePresentation B S hS Z₂.1.ι →
        Disjoint (subspacePointSet B S hS X.1 U.1 ∩ subspacePointSet B S hS X.1 Z₁.1)
          (subspacePointSet B S hS X.1 Z₂.1) →
        ∃ (X' : AlgebraicSpaces B S hS) (b : X' ⟶ X) (Y : ClosedSubspaces B S hS X.1),
          IsAdmissibleBlowup B S hS U b ∧ IsFinitePresentation B S hS Y.1.ι ∧
            Disjoint (subspacePointSet B S hS X.1 U.1) (subspacePointSet B S hS X.1 Y.1) ∧
              IsBlowupAlong B S hS Y b ∧
                Disjoint (strictTransformPointSet (closedSubspaceSpaceι X Z₁) b
                    (preimageClosedSubspace b Y).1)
                  (strictTransformPointSet (closedSubspaceSpaceι X Z₂) b
                    (preimageClosedSubspace b Y).1)) ∧
      ∀ T₁ T₂ : Set (points B S hS U.1.toFunctor), IsClosed T₁ → IsClosed T₂ →
        Topology.IsConstructible T₁ → Topology.IsConstructible T₂ → Disjoint T₁ T₂ →
        ∃ (X' : AlgebraicSpaces B S hS) (b : X' ⟶ X), IsAdmissibleBlowup B S hS U b ∧
          Disjoint (closure (pointsMap B S hS _ b.hom ⁻¹' (pointsMap B S hS _ U.1.ι '' T₁)))
            (closure (pointsMap B S hS _ b.hom ⁻¹' (pointsMap B S hS _ U.1.ι '' T₂)))

Tag 0F47, a lemma

Tag 0F47 in the Stacks Project.

AlgebraicGeometry.Space.exists_isBlowupAlong_isIso_strictTransformSpaceToBlowUp_over_closure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AdmissibleBlowupIsoNearClosure.lean, line 84.

Stacks 0F47. Let S be a scheme, let f : X ⟶ Y be a proper morphism of algebraic spaces over S with Y quasi-compact and quasi-separated, let V ⊆ Y be a quasi-compact open subspace and let T ⊆ |V| be a closed subset such that f|_{f⁻¹(V)} : f⁻¹(V) ⟶ V is an isomorphism over an open neighbourhood W of T in V. Then there is a V-admissible blowup b : Y' ⟶ Y, the blowup of Y in a closed subspace Yc of finite presentation whose points avoid those of V, such that the strict transform f' : X' ⟶ Y' of f is an isomorphism over an open neighbourhood W' of the closure of T in |Y'|.

An open subspace of V is an open subspace W of Y with W ≤ V, and f|_{f⁻¹(V)} is an isomorphism over it exactly when f is, i.e. when f⁻¹(W) ⟶ W is an isomorphism. The centre Yc is recorded, since the strict transform is taken relative to it. The closure of T in |Y'| is the closure of the set of points of Y' mapping into the image of T in |Y|, as in Stacks 0F46 (AlgebraicGeometry.Space.exists_isAdmissibleBlowup_disjoint_closure). The source also asks X to be quasi-compact and quasi-separated; this follows from properness of f over the quasi-compact and quasi-separated Y, is not used, and is omitted.

theorem exists_isBlowupAlong_isIso_strictTransformSpaceToBlowUp_over_closure
    {X Y : AlgebraicSpaces B S hS}
    (hYqc : IsQuasiCompactSpace B S hS Y.1)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS B.contains_terminal Y.1)
    (f : X ⟶ Y) (hf : IsProper B S hS f.hom)
    (V : OpenSubspaces B S hS Y.1) (hVqc : IsQuasiCompactSpace B S hS V.1.toFunctor)
    (T : Set (points B S hS V.1.toFunctor)) (hT : IsClosed T)
    (W : OpenSubspaces B S hS Y.1) (hWV : W.1 ≤ V.1)
    (hTW : pointsMap B S hS _ V.1.ι '' T ⊆ subspacePointSet B S hS Y.1 W.1)
    (hWiso : IsIso (pullback.snd f.hom W.1.ι)) :
    ∃ (Y' : AlgebraicSpaces B S hS) (b : Y' ⟶ Y) (Yc : ClosedSubspaces B S hS Y.1),
      IsFinitePresentation B S hS Yc.1.ι ∧
        Disjoint (subspacePointSet B S hS Y.1 V.1) (subspacePointSet B S hS Y.1 Yc.1) ∧
          IsBlowupAlong B S hS Yc b ∧
            ∃ W' : OpenSubspaces B S hS Y'.1,
              closure (pointsMap B S hS _ b.hom ⁻¹' (pointsMap B S hS _ V.1.ι '' T)) ⊆
                  subspacePointSet B S hS Y'.1 W'.1 ∧
                IsIso (pullback.snd
                  (strictTransformSpaceToBlowUp B S hS f b (Yc.1.preimage b.hom)).hom
                  W'.1.ι)

Tag 0F48, a lemma

Tag 0F48 in the Stacks Project.

AlgebraicGeometry.Space.exists_isAdmissibleBlowup_surjective_finite_flat_etaleLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/StrictTransformFiniteFlatNearClosure.lean, line 781.

Stacks 0F48. Let S be a scheme, let f : X ⟶ Y be a proper morphism of quasi-compact and quasi-separated algebraic spaces over S, let V ⊆ Y be a quasi-compact open subspace with inverse image U = f⁻¹(V), let A ⊆ U and Bc ⊆ V be closed subspaces such that f restricts to an isomorphism e : A ≅ Bc, and assume f is étale at every point of A. Then there is a V-admissible blowup b : Y' ⟶ Y, with centre Yc, such that the strict transform f' : X' ⟶ Y' of f satisfies: for every geometric point ā of X' lying in the closure of the inverse image of |A| in |X'| there is a quotient φ : 𝒪_{X', ā} ⟶ 𝒪, a surjection onto a local ring, such that φ ∘ (𝒪_{Y', f'(ā)} ⟶ 𝒪_{X', ā}) is finite and flat.

The ring 𝒪 is the étale local ring of the strict transform E of a quasi-compact open X₁₀ of a U-admissible blowup of X, at a geometric point over ā (AlgebraicGeometry.Space.exists_isAdmissibleBlowup_isFlat_cover_closure), chosen so that the part of X₁₀ over Bc lies over A. As A is open in f⁻¹(Bc), being the image of a section of f⁻¹(Bc) ⟶ Bc near which that morphism is étale, E ×_{Y'} Bc ⟶ Bc is a monomorphism, and E ⟶ Y' is étale at every point over the closure of |Bc| (AlgebraicGeometry.Space.isEtaleAt_of_mono_pullback_snd), which contains f'(ā). So the map 𝒪_{Y', f'(ā)} ⟶ 𝒪 is bijective (AlgebraicGeometry.Space.bijective_etaleLocalRingMap_of_isEtaleAt) and φ is surjective.

theorem exists_isAdmissibleBlowup_surjective_finite_flat_etaleLocalRing
    (hZ : B.Contains (⊤_ Scheme.{u})) {X Y : AlgebraicSpaces B S hS}
    (hXqc : IsQuasiCompactSpace B S hS X.1) (hXqs : IsAbsolutelyQuasiSeparated B S hS hZ X.1)
    (hYqc : IsQuasiCompactSpace B S hS Y.1) (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y.1)
    (f : X ⟶ Y) (hf : IsProper B S hS f.hom)
    (V : OpenSubspaces B S hS Y.1) (hVqc : IsQuasiCompactSpace B S hS V.1.toFunctor)
    (A : ClosedSubspaces B S hS (V.1.preimage f.hom).toFunctor)
    (Bc : ClosedSubspaces B S hS V.1.toFunctor) (e : A.1.toFunctor ≅ Bc.1.toFunctor)
    (he : e.hom ≫ Bc.1.ι = A.1.ι ≫ V.1.fromPreimage f.hom)
    (het : ∀ a : points B S hS A.1.toFunctor,
      IsEtaleAt B S hS f.hom (pointsMap B S hS _ (A.1.ι ≫ (V.1.preimage f.hom).ι) a)) :
    ∃ (Y' : AlgebraicSpaces B S hS) (b : Y' ⟶ Y) (Yc : ClosedSubspaces B S hS Y.1),
      IsAdmissibleBlowup B S hS V b ∧ IsFinitePresentation B S hS Yc.1.ι ∧
        Disjoint (subspacePointSet B S hS Y.1 V.1) (subspacePointSet B S hS Y.1 Yc.1) ∧
          IsBlowupAlong B S hS Yc b ∧
            ∀ abar : GeometricPoint B S hS
                (strictTransformSpace B S hS f b (Yc.1.preimage b.hom)).1,
              abar.image ∈ closure (pointsMap B S hS _
                  (strictTransformSpaceι B S hS f b (Yc.1.preimage b.hom) ≫
                    strictTransformPullbackToSource B S hS f b).hom ⁻¹'
                  Set.range (pointsMap B S hS _ (A.1.ι ≫ (V.1.preimage f.hom).ι))) →
              ∃ (O : CommRingCat.{u + 1})
                (φ : etaleLocalRing B S hS
                  (strictTransformSpace B S hS f b (Yc.1.preimage b.hom)).1 abar →+* O),
                IsLocalRing O ∧ Function.Surjective φ ∧
                  (φ.comp (etaleLocalRingMap
                    (strictTransformSpace B S hS f b (Yc.1.preimage b.hom)).2
                    (strictTransformSpaceToBlowUp B S hS f b (Yc.1.preimage b.hom)).hom
                    abar)).Finite ∧
                  (φ.comp (etaleLocalRingMap
                    (strictTransformSpace B S hS f b (Yc.1.preimage b.hom)).2
                    (strictTransformSpaceToBlowUp B S hS f b (Yc.1.preimage b.hom)).hom
                    abar)).Flat

Tag 0F49, a lemma

Tag 0F49 in the Stacks Project.

AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_le_strictTransformInAmbient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupPropernessAndStrictTransformImage.lean, line 339. The attribute's comment: “the inclusion of the scheme-theoretic image in the strict transform”.

One inclusion of Stacks 0F49, with Stacks 085T and 0863 as explicit hypotheses. Let X ⟶ T and Y ⟶ T be morphisms of algebraic spaces over S, let U ⊆ X be an open subspace, let v : V ⟶ X ×_T Y be a morphism whose composite with the first projection factors through U, and let Z be the scheme-theoretic image of v. Let b : X' ⟶ X be the blowup of X in a closed subspace Zc of finite presentation whose points are disjoint from those of U — that is, a U-admissible blowup of Stacks 086B. Then the scheme-theoretic image of the lift v' : V ⟶ X' ×_T Y is contained in the strict transform of Z with respect to b.

Here X' ×_T Y is spelled (X ×_T Y) ×_X X', the strict transform of Stacks 0862 is taken of Z viewed as an algebraic space over X, and its image in the ambient space is AlgebraicGeometry.Space.strictTransformInAmbient.

Stacks 0F49 asserts that the two are equal. This is the inclusion of the scheme-theoretic image in the strict transform, and only that; it is not the tag's equality, and the clause string of the attribute says which inclusion it is. The reverse inclusion is the content the library cannot reach; see AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_eq_strictTransformInAmbient.

Two hypotheses stand for inputs the library does not have, and both are upstream of this conclusion — each is the conclusion of a tag that is missing, and neither mentions the scheme-theoretic image of the lift:

hfac is the source's morphism V ⟶ Z', which comes from Stacks 085T part (1): the blowup is an isomorphism away from its centre, and V lies over U, which is disjoint from the centre;

himm is step (1) of the source's proof, that the strict transform is a closed subspace of X' ×_X Z, which is Stacks 0863 part (2).

Given those, the inclusion is the minimality of the scheme-theoretic image, Stacks 082X in the form AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_le: the strict transform is a closed subspace through which the lift factors. Quasi-compactness of v is not needed for this half and so is not carried; the source uses it only in the reverse inclusion.

theorem schemeTheoreticImageSubfunctor_le_strictTransformInAmbient (p : X ⟶ T) (q : Y ⟶ T)
    (U : OpenSubspaces B S hS X.1) (Zc : ClosedSubspaces B S hS X.1) (b : X' ⟶ X)
    (hfp : IsFinitePresentation B S hS Zc.1.ι)
    (hdisj : Disjoint (subspacePointSet B S hS X.1 U.1)
      (subspacePointSet B S hS X.1 Zc.1))
    (hbl : IsBlowupAlong B S hS Zc b)
    (v : V ⟶ AlgebraicSpaces.fiberProduct B S hS p q)
    (v' : V.1 ⟶ (strictTransformPullback B S hS (fiberProductFirst B S hS p q) b).1)
    (hvU : Subfunctor.range (v.hom ≫ (fiberProductFirst B S hS p q).hom) ≤ U.1)
    (hfac : IsAdmissibleBlowup B S hS U b →
      Subfunctor.range (v.hom ≫ (fiberProductFirst B S hS p q).hom) ≤ U.1 →
      Subfunctor.range v' ≤ strictTransformInAmbient B S hS p q b Zc
        (schemeTheoreticImage B S hS v.hom
          (AlgebraicSpaces.fiberProduct B S hS p q).property))
    (himm : IsClosedSubspace B S hS (strictTransformInAmbient B S hS p q b Zc
      (schemeTheoreticImage B S hS v.hom
        (AlgebraicSpaces.fiberProduct B S hS p q).property))) :
    schemeTheoreticImageSubfunctor B S hS v' ≤
      strictTransformInAmbient B S hS p q b Zc
        (schemeTheoreticImage B S hS v.hom
          (AlgebraicSpaces.fiberProduct B S hS p q).property)

AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_eq_strictTransformInAmbient_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/BlowupPropernessAndStrictTransformImageUnconditional.lean, line 1029. The attribute's comment: “the equality of the scheme-theoretic image of the lift with the strict transform, at the source's hypotheses and with NO side condition and no part of the conclusion assumed. The properness of the admissible blowup, Stacks 085Z, is proved rather than assumed, by AlgebraicGeometry.Space.isProper_of_isBlowupAlong_of_isFinitePresentation, which itself carries no side condition”.

Stacks 0F49. Let X ⟶ T and Y ⟶ T be morphisms of algebraic spaces over S, let U ⊆ X be an open subspace, let v : V ⟶ X ×_T Y be a quasi-compact morphism whose composite with the first projection factors through U, and let Z be the scheme-theoretic image of v. Let b : X' ⟶ X be a U-admissible blowup, that is, the blowup of X in a closed subspace Zc of finite presentation whose points are disjoint from those of U. Then the scheme-theoretic image of the lift v' : V ⟶ X' ×_T Y equals the strict transform of Z with respect to b.

This is the assertion of Stacks 0F49. Both inclusions are proved:

AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_le_strictTransformInAmbient_of_lift is steps (1) and (2) of the source's proof — the strict transform is a closed subspace of X' ×_T Y through which the lift factors;

AlgebraicGeometry.Space.strictTransformInAmbient_le_schemeTheoreticImageSubfunctor is steps (4) and (5) — V is scheme-theoretically dense in the part of Z ×_X X' lying over the complement of the centre, by part (3) of Stacks 082Z, and the strict transform is cut out by the ideal of sections supported on the exceptional divisor, which is the ideal-theoretic form of "there are no nonzero sections of 𝒪_{Z'} supported on E".

Step (3) of the source's proof, the quasi-compactness of the lift, is supplied by AlgebraicGeometry.Space.isQuasiCompact_of_comp_fiberProductFirst_unconditional, which needs the properness of the admissible blowup, Stacks 085Z. That is now proved, in AlgebraicGeometry.Space.isProper_of_isBlowupAlong_of_isFinitePresentation, and carries no side condition, so nothing is assumed here beyond the source's own hypotheses. In particular the density statement, part of the tag's own conclusion, is the theorem AlgebraicGeometry.Space.strictTransformInAmbient_le_schemeTheoreticImageSubfunctor, and neither the existence of a proper blowup nor a surjective étale chart of X with the size conditions of Stacks 085Q is assumed.

theorem schemeTheoreticImageSubfunctor_eq_strictTransformInAmbient_unconditional
    [HasSheafify (BigFppfOver.topology B S hS) (Type u)] (p : X ⟶ T) (q : Y ⟶ T)
    (U : OpenSubspaces B S hS X.1) (Zc : ClosedSubspaces B S hS X.1) (b : X' ⟶ X)
    (hfp : IsFinitePresentation B S hS Zc.1.ι)
    (hdisj : Disjoint (subspacePointSet B S hS X.1 U.1)
      (subspacePointSet B S hS X.1 Zc.1))
    (hbl : IsBlowupAlong B S hS Zc b)
    (v : V ⟶ AlgebraicSpaces.fiberProduct B S hS p q)
    (hv : IsQuasiCompact B S hS v.hom)
    (v' : V.1 ⟶ (strictTransformPullback B S hS (fiberProductFirst B S hS p q) b).1)
    (hv' : v' ≫ pullback.fst (fiberProductFirst B S hS p q).hom b.hom = v.hom)
    (hvU : Subfunctor.range (v.hom ≫ (fiberProductFirst B S hS p q).hom) ≤ U.1) :
    schemeTheoreticImageSubfunctor B S hS v' =
      strictTransformInAmbient B S hS p q b Zc
        (schemeTheoreticImage B S hS v.hom
          (AlgebraicSpaces.fiberProduct B S hS p q).property)

Tag 0F4A, a lemma

Tag 0F4A in the Stacks Project.

AlgebraicGeometry.Space.exists_isAdmissibleBlowup_isProper_extension_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EtaleCompactificationProperExtension.lean, line 138.

Let T be a quasi-compact and quasi-separated algebraic space over S, let g : U ⟶ T be separated and of finite type, and let f : V ⟶ U be étale. Suppose V has a compactification over T: a quasi-compact open immersion j : V ⟶ Y into an algebraic space Y with p : Y ⟶ T proper and j ≫ p = f ≫ g. Then there are a V-admissible blowup b : Y' ⟶ Y and an open subspace V' ⊆ Y' containing V — a morphism e : V ⟶ V' lying over j whose image in Y' is the inverse image of V — such that f extends to a proper morphism q : V' ⟶ U over T.

theorem exists_isAdmissibleBlowup_isProper_extension_of_isEtale
    (hZ : B.Contains (⊤_ Scheme.{u})) {T U V Y : AlgebraicSpaces B S hS}
    (hTqc : IsQuasiCompactSpace B S hS T.1) (hTqs : IsAbsolutelyQuasiSeparated B S hS hZ T.1)
    (g : U.1 ⟶ T.1) (hgft : IsFiniteType B S hS g) (hgsep : IsSeparated B S hS g)
    (f : V.1 ⟶ U.1) (_hf : IsEtale B S hS f)
    (j : V.1 ⟶ Y.1) (p : Y.1 ⟶ T.1) (hj : IsOpenImmersion B S hS j)
    (hjqc : IsQuasiCompact B S hS j) (hp : IsProper B S hS p) (hcomm : j ≫ p = f ≫ g) :
    ∃ (Y' : AlgebraicSpaces B S hS) (b : Y' ⟶ Y),
      IsAdmissibleBlowup B S hS
        ⟨Subfunctor.range j, isOpenSubspace_subfunctorRange B S hS V.2 hj⟩ b ∧
      ∃ (V' : OpenSubspaces B S hS Y'.1) (e : V.1 ⟶ V'.1.toFunctor) (q : V'.1.toFunctor ⟶ U.1),
        Subfunctor.range (e ≫ V'.1.ι) = (Subfunctor.range j).preimage b.hom ∧
          e ≫ V'.1.ι ≫ b.hom = j ∧ IsProper B S hS q ∧ e ≫ q = f ∧
            q ≫ g = V'.1.ι ≫ b.hom ≫ p

Tag 0F4B, a lemma

Tag 0F4B in the Stacks Project.

AlgebraicGeometry.Space.hasCompactification_of_isElementaryDistinguishedSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NagataCompactification/EtaleSquareCompactification.lean, line 278. The attribute's comment: “proof corrected: the source's W₁ = U ⊔_{U₁} (X₁ ∖ (Z̄₁₂ ∪ T̄)) need not be separated; X₁ is modified by three more admissible blowups (0F46 twice, and a blowup in I + J^M from the Nullstellensatz on the closure of the off-diagonal of U₁ ×_U U₁), and W₁ is glued from the chart N = X₁ ∖ (closure (V₁ ∖ U₁) ∪ closure (∂ ∖ Q))”.

Compactifications glue across an elementary distinguished square (Stacks 0F4B). Over a quasi-compact, quasi-separated algebraic space Y of finite type over Spec ℤ, let U be separated and of finite type over Y and (U₂ ⊆ U, f : U₁ ⟶ U) an elementary distinguished square such that U₁ and U₂ have compactifications over Y and U₁ ×_U U₂ ⟶ U has dense image. Then U has a compactification over Y.

The proof is the repaired one of StacksFrontier.AlgebraicGeometry.Spaces.NagataCompactification.EtaleSquareGluing; the density of U₁ ×_U U₂ in U is not needed.

theorem hasCompactification_of_isElementaryDistinguishedSquare (hZ : B.Contains (⊤_ Scheme.{u})) :
    Stmt0F4B (B := B) (S := S) (hS := hS) hZ

Tag 0F4C, a lemma

Tag 0F4C in the Stacks Project.

AlgebraicGeometry.Space.exists_affine_etale_isElementaryDistinguishedSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffineEtaleEnlargementOfOpen/Enlargement.lean, line 464.

Stacks 0F4C. Let U be a dense open subspace of a Noetherian algebraic space X over S with U ≠ X. There is an affine scheme V and an étale morphism V ⟶ X such that the open subspace W whose points are those of U together with the image of V strictly contains U, the pair (U ⊆ W, V ⟶ W) is an elementary distinguished square, and U ×_X V ⟶ U has dense image.

theorem exists_affine_etale_isElementaryDistinguishedSquare
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (hZ : B.Contains (⊤_ Scheme.{u}))
    (X : (AlgebraicGeometry.BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (hX : AlgebraicGeometry.IsAlgebraicSpace B S hS X)
    (hXnoeth : AlgebraicGeometry.Space.IsNoetherian B S hS hZ X)
    (U : Subfunctor X) (hU : AlgebraicGeometry.Space.IsOpenSubspace B S hS U)
    (hUproper : U ≠ ⊤)
    (_hUdense : letI : TopologicalSpace (AlgebraicGeometry.Space.points B S hS X) :=
        AlgebraicGeometry.Space.pointTopology B S hS X
      DenseRange (AlgebraicGeometry.Space.pointsMap B S hS U.toFunctor U.ι)) :
    ∃ (V : AlgebraicGeometry.BigFppfOver B S hS)
      (W : Subfunctor X)
      (hW : AlgebraicGeometry.Space.IsOpenSubspace B S hS W)
      (hUW : U < W)
      (f : yoneda.obj V ⟶ W.toFunctor),
      IsAffine ((AlgebraicGeometry.BigFppfOver.toScheme B S hS).obj V) ∧
      AlgebraicGeometry.Space.IsEtale B S hS (f ≫ W.ι) ∧
      (Set.range (AlgebraicGeometry.Space.pointsMap B S hS W.toFunctor W.ι) =
        Set.range (AlgebraicGeometry.Space.pointsMap B S hS U.toFunctor U.ι) ∪
          Set.range (AlgebraicGeometry.Space.pointsMap B S hS (yoneda.obj V) (f ≫ W.ι))) ∧
      AlgebraicGeometry.Space.IsElementaryDistinguishedSquare B S hS hW.1
        (Subfunctor.range (Subfunctor.homOfLe hUW.le)) f ∧
      (letI : TopologicalSpace (AlgebraicGeometry.Space.points B S hS U.toFunctor) :=
        AlgebraicGeometry.Space.pointTopology B S hS U.toFunctor
       DenseRange (AlgebraicGeometry.Space.pointsMap B S hS (pullback U.ι (f ≫ W.ι))
         (pullback.fst U.ι (f ≫ W.ι))))

Tag 0F4D, a theorem

Tag 0F4D in the Stacks Project.

AlgebraicGeometry.Space.hasCompactification_of_isSeparated_of_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NagataCompactification/Nagata.lean, line 63.

Nagata's compactification theorem for algebraic spaces. Let Y be a quasi-compact and quasi-separated algebraic space over S, and let f : X ⟶ Y be a separated morphism of finite type. Then X has a compactification over Y.

theorem hasCompactification_of_isSeparated_of_isFiniteType (hZ : B.Contains (⊤_ Scheme.{u}))
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (hYqc : IsQuasiCompactSpace B S hS Y)
    (hYqs : IsAbsolutelyQuasiSeparated B S hS hZ Y) (f : X ⟶ Y) (hsep : IsSeparated B S hS f)
    (hft : IsFiniteType B S hS f) : HasCompactification B S hS f

Sources

LeanAlgebraicGeometry.Space.isSeparated_of_elementaryDistinguishedSquare · AlgebraicGeometry.Space.not_forall_isSeparated_of_isElementaryDistinguishedSquare · AlgebraicGeometry.Space.exists_isAdmissibleBlowup_separating_strictTransforms_and_closures · AlgebraicGeometry.Space.exists_isBlowupAlong_isIso_strictTransformSpaceToBlowUp_over_closure · AlgebraicGeometry.Space.exists_isAdmissibleBlowup_surjective_finite_flat_etaleLocalRing · AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_le_strictTransformInAmbient · AlgebraicGeometry.Space.schemeTheoreticImageSubfunctor_eq_strictTransformInAmbient_unconditional · AlgebraicGeometry.Space.exists_isAdmissibleBlowup_isProper_extension_of_isEtale

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

81 Pushouts of Algebraic Spaces

Section81.3 Colimits of algebraic spaces#

Tag 07SX, a lemma

Tag 0GFQ, a lemma

Tag 0GHL, a lemma

Tag 0GFP, a lemma

Sources

Section81.4 Descending étale sheaves#

Tag 0GFS, a lemma

Tag 0GFT, a lemma

Tag 0GFU, a lemma

Tag 0GFV, a lemma

Tag 0GFW, a lemma

Tag 0GFX, a lemma

Tag 0GFY, a lemma

Sources

Section81.5 Descending étale morphisms of algebraic spaces#

Tag 0GG0, a lemma

Tag 0GG1, a lemma

Sources

Section81.6 Pushouts along thickenings and affine morphisms#

Tag 07SY, a lemma

Tag 07VX, a lemma

Tag 07VY, a lemma

Tag 07VZ, a lemma

Tag 07W0, a lemma

Tag 07W1, an equation

Tag 07W2, an equation

Tag 08KV, a lemma

Tag 07W3, a lemma

Sources

Section81.7 Pushouts along closed immersions and integral morphisms#

Tag 0EDP, a lemma

Sources

Section81.8 Pushouts and derived categories#

Tag 0DL7, a lemma

Sources

Section81.9 Constructing elementary distinguished squares#

Tag 0DVI, a lemma

Tag 0DVJ, a lemma

Sources

Section81.10 Formal glueing of quasi-coherent modules#

Tag 0AEQ, a lemma

Tag 0AER, a lemma

Tag 0AES, a lemma

Tag 0AET, a lemma

Tag 0AEU, a lemma

Tag 0AEV, a situation

Tag 0AEW, an equation

Tag 0AEX, an equation

Tag 0AEY, a lemma

Tag 0AEZ, a lemma

Tag 0AF0, a proposition

Tag 0AFJ, a lemma

Tag 0AF1, a lemma

Sources

Section81.11 Formal glueing of algebraic spaces#

Tag 0AF3, an equation

Tag 0AF4, a lemma

Tag 0AF5, a lemma

Tag 0AF6, a lemma

Sources

Section81.12 Glueing and the Beauville-Laszlo theorem#

Tag 0F9N, an equation

Tag 0F9P, a lemma

Tag 0F9Q, a lemma

Tag 0F9R, a lemma

Tag 0F9S, a lemma

Tag 0F9T, a lemma

Tag 0F9U, a lemma

Sources

Section81.13 Coequalizers and glueing#

Tag 0AGG, a lemma

Tag 0AGH, a situation

Tag 0AGI, a lemma

Tag 0AGJ, an equation

Tag 0AGK, a lemma

Tag 0AGL, a remark

Sources

Section81.14 Compactifications#

Section81.3 Colimits of algebraic spaces #

Section81.4 Descending étale sheaves #

Section81.5 Descending étale morphisms of algebraic spaces #

Section81.6 Pushouts along thickenings and affine morphisms #

Section81.7 Pushouts along closed immersions and integral morphisms #

Section81.8 Pushouts and derived categories #

Section81.9 Constructing elementary distinguished squares #

Section81.10 Formal glueing of quasi-coherent modules #

Section81.11 Formal glueing of algebraic spaces #

Section81.12 Glueing and the Beauville-Laszlo theorem #

Section81.13 Coequalizers and glueing #

Section81.14 Compactifications #