34.3 The Zariski topology to 34.9 The fpqc topology

Section34.3 The Zariski topology#

Section 34.3 of the Stacks Project, Tag 020N. 20 tags here are carried by 78 declarations of the repository (all in StacksFrontier) and 15 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 020O, a definition

Tag 020O in the Stacks Project.

Declarations registered for the tag:

Tag 020P, a lemma

Tag 020P in the Stacks Project.

Declarations registered for the tag:

Tag 020Q, a lemma

Tag 020Q in the Stacks Project.

AlgebraicGeometry.Scheme.OpenCover.exists_isStandardZariski_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Zariski/StandardCovering.lean, line 56.

Stacks Project, Tag 020Q. Every Zariski covering of an affine scheme has a finite refinement by standard opens, each contained in a member of the original covering.

public theorem OpenCover.exists_isStandardZariski_refinement {T : Scheme.{u}} [IsAffine T]
    (𝒰 : T.OpenCover.{v}) :
    ∃ (𝒱 : T.OpenCover.{v}) (_refinement : 𝒱 ⟶ 𝒰),
      AlgebraicGeometry.IsStandardZariskiCovering 𝒱
Tag 020R, a definition

Tag 020R in the Stacks Project.

AlgebraicGeometry.IsStandardZariskiCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiTopology/StandardCoverings.lean, line 32.

A Zariski covering of an affine scheme T is standard if it has finitely many members and every member identifies with a standard affine open T.basicOpen f of the target.

public abbrev IsStandardZariskiCovering {T : Scheme.{u}} [IsAffine T]
    (𝒰 : T.Cover.{v} Scheme.zariskiPrecoverage) : Prop
Tag 020S, a definition

Tag 020S in the Stacks Project.

AlgebraicGeometry.BigZariskiSite, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Zariski/BigSite.lean, line 90.

Stacks 020S. A big Zariski site consists of an initial set of schemes and initial Zariski covering families, a sufficiently large cutoff category containing those schemes, and a bounded set of Zariski covering families.

The last two fields say that the selected families satisfy the site axioms and that every Zariski covering family has a combinatorially equivalent selected representative.

public structure BigZariskiSite
Tag 03WV, a lemma

Tag 03WV in the Stacks Project.

AlgebraicGeometry.BigZariskiSite.exists_isCovering_tautologicallyEquivalent_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Zariski/BigSite.lean, line 171.

Stacks Project, Tag 03WV. Every Zariski covering of an object of a big Zariski site is tautologically equivalent to a covering belonging to that site.

public theorem exists_isCovering_tautologicallyEquivalent_openCover
    (B : BigZariskiSite.{u}) (T : B.Schemes)
    (U : (B.inclusion.obj T).OpenCover.{v}) :
    ∃ V : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, V⟩ ∧
        PreZeroHypercover.TautologicallyEquivalent U.toPreZeroHypercover
          (V.map B.inclusion)
Tag 020T, a definition

Tag 020T in the Stacks Project.

AlgebraicGeometry.BigZariskiOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiTopology/Sites.lean, line 53. The attribute's comment: “part (1), category”.

The big Zariski category of S is the slice of the chosen big category.

public abbrev BigZariskiOver

AlgebraicGeometry.BigZariskiOver.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiTopology/Sites.lean, line 66. The attribute's comment: “part (1), coverings”.

A family over S covers when its underlying family covers in the chosen big site.

public abbrev IsCovering (E : Covering (BigZariskiOver B S hS)) : Prop

AlgebraicGeometry.SmallZariski, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiTopology/Sites.lean, line 95. The attribute's comment: “part (2), category”.

The small Zariski category consists of schemes open in S.

public abbrev SmallZariski

AlgebraicGeometry.SmallZariski.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiTopology/Sites.lean, line 112. The attribute's comment: “part (2), coverings”.

Small-site coverings are precisely big-site coverings of small-site objects.

public abbrev IsCovering (E : Covering (SmallZariski B S hS)) : Prop

AlgebraicGeometry.BigAffineZariski, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiTopology/Sites.lean, line 151. The attribute's comment: “part (3), category”.

The big affine Zariski category consists of affine schemes over S.

public abbrev BigAffineZariski

AlgebraicGeometry.BigAffineZariski.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiTopology/Sites.lean, line 169. The attribute's comment: “part (3), coverings”.

Big affine coverings are standard Zariski coverings.

public abbrev IsCovering (E : Covering (BigAffineZariski B S hS)) : Prop

AlgebraicGeometry.SmallAffineZariski, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiTopology/Sites.lean, line 200. The attribute's comment: “part (4), category”.

The small affine Zariski category consists of affine opens in S.

public abbrev SmallAffineZariski

AlgebraicGeometry.SmallAffineZariski.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiTopology/Sites.lean, line 220. The attribute's comment: “part (4), coverings”.

Small affine coverings are the standard Zariski coverings inherited from the small site.

public abbrev IsCovering (E : Covering (SmallAffineZariski B S hS)) : Prop
Tag 020U, a lemma

Tag 020U in the Stacks Project.

AlgebraicGeometry.SmallZariski.isSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiSiteAxioms.lean, line 239. The attribute's comment: “small Zariski site”.

Zariski coverings of schemes open in S satisfy the site axioms.

public theorem isSite (B : AlgebraicGeometry.BigZariskiSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) : IsSite (AlgebraicGeometry.SmallZariski.IsCovering B S hS)

AlgebraicGeometry.BigAffineZariski.isSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiSiteAxioms.lean, line 314. The attribute's comment: “big affine Zariski site”.

Standard Zariski coverings of affine schemes over S satisfy the site axioms.

public theorem isSite (B : AlgebraicGeometry.BigZariskiSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) : IsSite (AlgebraicGeometry.BigAffineZariski.IsCovering B S hS)

AlgebraicGeometry.SmallAffineZariski.isSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiSiteAxioms.lean, line 414. The attribute's comment: “small affine Zariski site”.

Standard Zariski coverings of affine opens of S satisfy the site axioms.

public theorem isSite (B : AlgebraicGeometry.BigZariskiSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) : IsSite (AlgebraicGeometry.SmallAffineZariski.IsCovering B S hS)
Tag 020V, a lemma

Tag 020V in the Stacks Project.

AlgebraicGeometry.hasPullbacks_bigZariskiSite, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiLimits.lean, line 94. The attribute's comment: “fibre products in the big Zariski site”.

The underlying category of a big Zariski site has fibre products.

public instance hasPullbacks_bigZariskiSite : HasPullbacks B.Schemes

AlgebraicGeometry.hasPullbacks_smallZariski, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiLimits.lean, line 107. The attribute's comment: “fibre products in the small Zariski site”.

The small Zariski category of S has fibre products.

public instance hasPullbacks_smallZariski : HasPullbacks (SmallZariski B S hS)

AlgebraicGeometry.hasPullbacks_bigAffineZariski, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiLimits.lean, line 128. The attribute's comment: “fibre products in the big affine Zariski site”.

The category of affine objects in the big Zariski category over S has fibre products.

public instance hasPullbacks_bigAffineZariski : HasPullbacks (BigAffineZariski B S hS)

AlgebraicGeometry.hasPullbacks_smallAffineZariski, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiLimits.lean, line 143. The attribute's comment: “fibre products in the small affine Zariski site”.

The affine small Zariski category of S has fibre products.

public instance hasPullbacks_smallAffineZariski : HasPullbacks (SmallAffineZariski B S hS)

AlgebraicGeometry.preservesPullbacks_bigZariskiSiteInclusion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiLimits.lean, line 150. The attribute's comment: “preservation by the big Zariski site inclusion”.

The inclusion of a big Zariski site's underlying category into schemes preserves fibre products.

public instance preservesPullbacks_bigZariskiSiteInclusion :
    PreservesLimitsOfShape WalkingCospan B.inclusion

AlgebraicGeometry.preservesPullbacks_smallZariskiToScheme, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiLimits.lean, line 165. The attribute's comment: “preservation by the small Zariski functor to schemes”.

The canonical functor from the small Zariski category to schemes preserves fibre products.

public instance preservesPullbacks_smallZariskiToScheme :
    PreservesLimitsOfShape WalkingCospan (SmallZariski.toScheme B S hS)

AlgebraicGeometry.preservesPullbacks_bigAffineZariskiToScheme, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiLimits.lean, line 174. The attribute's comment: “preservation by the big affine Zariski functor to schemes”.

The canonical functor from affine objects over S to schemes preserves fibre products.

public instance preservesPullbacks_bigAffineZariskiToScheme :
    PreservesLimitsOfShape WalkingCospan (BigAffineZariski.toScheme B S hS)

AlgebraicGeometry.preservesPullbacks_smallAffineZariskiToScheme, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiLimits.lean, line 180. The attribute's comment: “preservation by the small affine Zariski functor to schemes”.

The canonical functor from affine open objects over S to schemes preserves fibre products.

public instance preservesPullbacks_smallAffineZariskiToScheme :
    PreservesLimitsOfShape WalkingCospan (SmallAffineZariski.toScheme B S hS)

AlgebraicGeometry.SmallZariski.finalIsTerminal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiLimits.lean, line 194. The attribute's comment: “the final object of the small Zariski site”.

The object S / S is final in the small Zariski category of S.

public noncomputable def SmallZariski.finalIsTerminal :
    IsTerminal (SmallZariski.final B S hS)

Declarations registered for the tag:

Tag 020W, a lemma

Tag 020W in the Stacks Project.

AlgebraicGeometry.BigAffineZariski.inclusion_isSpecialCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/AffineZariskiDenseSubsite.lean, line 317.

Stacks 020W. The inclusion of the big affine Zariski site over a scheme into its big Zariski site is special cocontinuous. Its dense-subsite component gives the induced equivalence of topoi.

public theorem BigAffineZariski.inclusion_isSpecialCocontinuous
    (B : BigZariskiSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    IsSpecialCocontinuous
      (BigAffineZariski.topology B S hS)
      (BigZariskiOver.topology B S hS)
      (BigAffineZariski.inclusion B S hS)
Tag 0F1B, a lemma

Tag 0F1B in the Stacks Project.

AlgebraicGeometry.SmallAffineZariski.inclusion_isSpecialCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiTopology/SmallAffineDenseSubsite.lean, line 320.

Stacks 0F1B. The inclusion of the small affine Zariski site of a scheme into its small Zariski site is a special cocontinuous functor. Its dense-subsite component is the induced equivalence of topoi Sh(S_{affine, Zar}) ≌ Sh(S_Zar), given by CategoryTheory.Functor.IsDenseSubsite.sheafEquiv.

public theorem SmallAffineZariski.inclusion_isSpecialCocontinuous
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    IsSpecialCocontinuous (SmallAffineZariski.topology B S hS)
      (SmallZariski.topology B S hS) (SmallAffineZariski.inclusion B S hS)
Tag 020X, a lemma

Tag 020X in the Stacks Project.

AlgebraicGeometry.smallZariskiSheafEquivWith, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiOpens.lean, line 412.

The equivalence between sheaves with values in a category A on the small Zariski site of S and on the opens of S, induced by smallZariskiSiteEquiv B S hS.

public noncomputable def smallZariskiSheafEquivWith (A : Type w) [Category.{v} A] :
    Sheaf (SmallZariski.topology B S hS) A ≌
      Sheaf (Opens.grothendieckTopology S.carrier) A
Tag 020Y, a lemma

Tag 020Y in the Stacks Project.

AlgebraicGeometry.smallZariskiToBigZariskiToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/RingedToposIf.lean, line 110. The attribute's comment: “the morphism of topoi, at the universe of the structure rings”.

Stacks 020Y at the universe of the structure rings. The morphism of topoi i_f : \mathrm{Sh}(T_{Zar}) ⟶ \mathrm{Sh}((\Sch/S)_{Zar}) on sheaves of sets in Type u.

The library's AlgebraicGeometry.smallZariskiToBigZariskiMorphism is the same morphism for sheaves of sets in Type (u + 1), the universe of the objects of the sites; a ringed topos declares its topos at the universe of the sections of its structure sheaf, so that one cannot carry a morphism of ringed topoi.

public noncomputable def smallZariskiToBigZariskiToposHom :
    MorphismOfTopoi (Sheaf (SmallZariski.topology B T.1 T.property) (Type u))
      (Sheaf (BigZariskiOver.topology B S.1 S.property) (Type u))

AlgebraicGeometry.smallZariskiToBigZariskiFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiToBig.lean, line 107. The attribute's comment: “the functor”.

Send an open immersion U ⟶ T to the composite U ⟶ S.

public abbrev smallZariskiToBigZariskiFunctor :
    SmallZariski B T.obj T.property ⥤ BigZariskiOver B S.obj S.property

AlgebraicGeometry.smallZariskiToBigZariskiFunctor_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiToBig.lean, line 123. The attribute's comment: “cocontinuity”.

Postcomposition from the small Zariski site is cocontinuous.

public instance smallZariskiToBigZariskiFunctor_isCocontinuous :
    (smallZariskiToBigZariskiFunctor B T S f).IsCocontinuous
      (SmallZariski.topology B T.obj T.property)
      (BigZariskiOver.topology B S.obj S.property)

AlgebraicGeometry.smallZariskiToBigZariskiFunctor_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiToBig.lean, line 194. The attribute's comment: “continuity”.

Postcomposition preserves coverings and fibre products, hence is continuous.

public instance smallZariskiToBigZariskiFunctor_isContinuous :
    (smallZariskiToBigZariskiFunctor B T S f).IsContinuous
      (SmallZariski.topology B T.obj T.property)
      (BigZariskiOver.topology B S.obj S.property)

AlgebraicGeometry.smallZariskiToBigZariskiMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiToBig.lean, line 226. The attribute's comment: “the morphism of topoi”.

The geometric morphism i_f : Sh(T_Zar) ⟶ Sh((Sch/S)_Zar).

public noncomputable def smallZariskiToBigZariskiMorphism :
    MorphismOfTopoi
      (Sheaf (SmallZariski.topology B T.obj T.property) (Type (u + 1)))
      (Sheaf (BigZariskiOver.topology B S.obj S.property) (Type (u + 1)))

AlgebraicGeometry.smallZariskiToBigZariskiLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiToBig.lean, line 251. The attribute's comment: “existence of lower shriek”.

Lower shriek is left adjoint to inverse image.

public noncomputable def smallZariskiToBigZariskiLowerShriekAdjunction :
    smallZariskiToBigZariskiLowerShriek B T S f ⊣
      (smallZariskiToBigZariskiMorphism B T S f).inverseImage

AlgebraicGeometry.smallZariskiToBigZariskiLowerShriek_preservesPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiToBig.lean, line 267. The attribute's comment: “lower shriek preserves fibre products”.

Lower shriek preserves fibre products.

public instance smallZariskiToBigZariskiLowerShriek_preservesPullbacks :
    PreservesLimitsOfShape WalkingCospan
      (smallZariskiToBigZariskiLowerShriek B T S f)

AlgebraicGeometry.smallZariskiToBigZariskiLowerShriek_preservesEqualizers, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiToBig.lean, line 277. The attribute's comment: “lower shriek preserves equalizers”.

Lower shriek preserves equalizers.

public instance smallZariskiToBigZariskiLowerShriek_preservesEqualizers :
    PreservesLimitsOfShape WalkingParallelPair
      (smallZariskiToBigZariskiLowerShriek B T S f)

Declarations registered for the tag:

Tag 020Z, a lemma

Tag 020Z in the Stacks Project.

AlgebraicGeometry.smallZariskiInclusion_isMorphismOfSites_ringUniverse, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/RingedProjectionAndIf.lean, line 108. The attribute's comment: “the morphism of sites, at the universe of the structure rings”.

The inclusion of the small Zariski site of S into the big Zariski site over S defines a morphism of sites for sheaves of sets valued in the universe of the sections of the structure sheaves.

public instance smallZariskiInclusion_isMorphismOfSites_ringUniverse :
    IsMorphismOfSites.{u} (SmallZariski.inclusion B S.1 S.property)
      (SmallZariski.topology B S.1 S.property) (BigZariskiOver.topology B S.1 S.property)

AlgebraicGeometry.smallZariskiInclusion_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiProjection.lean, line 72. The attribute's comment: “continuity of the site morphism”.

The inclusion of the small Zariski site in the big slice site is continuous.

public instance smallZariskiInclusion_isContinuous :
    (SmallZariski.inclusion B S.obj S.property).IsContinuous
      (SmallZariski.topology B S.obj S.property)
      (BigZariskiOver.topology B S.obj S.property)

AlgebraicGeometry.smallZariskiInclusion_preservesFiniteLimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiProjection.lean, line 85. The attribute's comment: “exactness of the site morphism”.

The inverse-image functor of the site morphism is left exact.

public instance smallZariskiInclusion_preservesFiniteLimits :
    PreservesFiniteLimits
      ((SmallZariski.inclusion B S.obj S.property).sheafPullback (Type (u + 1))
        (SmallZariski.topology B S.obj S.property)
        (BigZariskiOver.topology B S.obj S.property))

AlgebraicGeometry.smallZariskiProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiProjection.lean, line 112. The attribute's comment: “the projection of topoi”.

The projection π_S from the big Zariski topos to the small one.

public noncomputable def smallZariskiProjection :
    MorphismOfTopoi
      (Sheaf (BigZariskiOver.topology B S.obj S.property) (Type (u + 1)))
      (Sheaf (SmallZariski.topology B S.obj S.property) (Type (u + 1)))

AlgebraicGeometry.smallZariskiProjection_comp_identity, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiProjection.lean, line 129. The attribute's comment: “the retraction”.

The inverse-image functor of π_S ∘ i_{id_S} is naturally the identity.

public noncomputable def smallZariskiProjection_comp_identity :
    ((smallZariskiProjection B S).comp
      (smallZariskiToBigZariskiMorphism B S S (𝟙 S))).inverseImage ≅
        𝟭 (Sheaf (SmallZariski.topology B S.obj S.property) (Type (u + 1)))

AlgebraicGeometry.smallZariskiIdentityInverseImageIsoProjectionPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiProjection.lean, line 188. The attribute's comment: “the inverse-image formula”.

Inverse image along i_S = i_{id_S} is the direct image along π_S, namely restriction of a big-site sheaf to the small site.

public noncomputable def smallZariskiIdentityInverseImageIsoProjectionPushforward :
    (smallZariskiToBigZariskiMorphism B S S (𝟙 S)).inverseImage ≅
      (smallZariskiProjection B S).pushforward

AlgebraicGeometry.smallZariskiIdentityInverseImageSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiProjection.lean, line 214. The attribute's comment: “the formula on sections”.

For a big-site sheaf G and an open subscheme U / S, inverse image along i_S has sections canonically isomorphic to G(U / S).

public noncomputable def smallZariskiIdentityInverseImageSections
    (G : Sheaf (BigZariskiOver.topology B S.obj S.property) (Type (u + 1)))
    (U : SmallZariski B S.obj S.property) :
    (((smallZariskiToBigZariskiMorphism B S S (𝟙 S)).inverseImage.obj G).obj.obj
      (Opposite.op U)) ≅ G.obj.obj (Opposite.op U.obj)

AlgebraicGeometry.preservesPullbacks_smallZariskiInclusion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiLimits.lean, line 116. The attribute's comment: “preservation of site pullbacks”.

The full inclusion of the small Zariski category into the big Zariski category over S preserves fibre products.

public instance preservesPullbacks_smallZariskiInclusion :
    PreservesLimitsOfShape WalkingCospan (SmallZariski.inclusion B S hS)

AlgebraicGeometry.preservesTerminal_smallZariskiInclusion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiLimits.lean, line 207. The attribute's comment: “preservation of the final object”.

The full inclusion of the small Zariski category into the big Zariski category over S carries S / S to the final object of the slice, hence preserves the final object.

public instance preservesTerminal_smallZariskiInclusion :
    PreservesLimitsOfShape (Discrete PEmpty.{1}) (SmallZariski.inclusion B S hS)

Declarations registered for the tag:

Tag 04BS, a definition

Tag 04BS in the Stacks Project.

AlgebraicGeometry.smallZariskiProjection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiProjection.lean, line 112. The attribute's comment: “restriction to the small Zariski site is its direct image”.

The projection π_S from the big Zariski topos to the small one.

public noncomputable def smallZariskiProjection :
    MorphismOfTopoi
      (Sheaf (BigZariskiOver.topology B S.obj S.property) (Type (u + 1)))
      (Sheaf (SmallZariski.topology B S.obj S.property) (Type (u + 1)))
Tag 0210, a lemma

Tag 0210 in the Stacks Project.

AlgebraicGeometry.bigZariskiMap_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiCovering/BigZariskiMorphism.lean, line 104. The attribute's comment: “cocontinuity”.

Stacks 0210. Postcomposition with f is cocontinuous for the big Zariski topologies.

public instance bigZariskiMap_isCocontinuous :
    (Over.map f).IsCocontinuous
      (BigZariskiOver.topology B T.1 T.property)
      (BigZariskiOver.topology B S.1 S.property)

AlgebraicGeometry.bigZariskiMap_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiCovering/BigZariskiMorphism.lean, line 114. The attribute's comment: “continuity”.

Stacks 0210. Postcomposition with f is continuous as well. This is the continuity used to identify inverse image with restriction and to construct the lower shriek.

public instance bigZariskiMap_isContinuous :
    (Over.map f).IsContinuous
      (BigZariskiOver.topology B T.1 T.property)
      (BigZariskiOver.topology B S.1 S.property)

AlgebraicGeometry.bigZariskiPullback_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiCovering/BigZariskiMorphism.lean, line 124. The attribute's comment: “continuity of the base-change right adjoint”.

Stacks 0210. Base change along f, sending U / S to the canonical fibre product U ×_S T / T, is continuous.

public instance bigZariskiPullback_isContinuous :
    (Over.pullback f).IsContinuous
      (BigZariskiOver.topology B S.1 S.property)
      (BigZariskiOver.topology B T.1 T.property)

AlgebraicGeometry.bigZariskiMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiCovering/BigZariskiMorphism.lean, line 133. The attribute's comment: “the morphism of topoi”.

Stacks 0210. The morphism of big Zariski topoi induced by postcomposition.

public noncomputable def bigZariskiMorphism :
    MorphismOfTopoi
      (Sheaf (BigZariskiOver.topology B T.1 T.property) (Type (u + 1)))
      (Sheaf (BigZariskiOver.topology B S.1 S.property) (Type (u + 1)))

AlgebraicGeometry.bigZariskiLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiCovering/BigZariskiMorphism.lean, line 151. The attribute's comment: “existence of lower shriek”.

Stacks 0210. The sheaf pullback along postcomposition is the lower shriek, left adjoint to inverse image.

public noncomputable def bigZariskiLowerShriekAdjunction :
    (Over.map f).sheafPullback (Type (u + 1))
      (BigZariskiOver.topology B T.1 T.property)
      (BigZariskiOver.topology B S.1 S.property) ⊣
        (bigZariskiMorphism B T S f).inverseImage

AlgebraicGeometry.bigZariskiLowerShriek_preservesPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiCovering/BigZariskiMorphism.lean, line 168. The attribute's comment: “lower shriek preserves fibre products”.

Stacks 0210. The lower shriek commutes with fibre products.

public instance bigZariskiLowerShriek_preservesPullbacks :
    PreservesLimitsOfShape WalkingCospan
      ((Over.map f).sheafPullback (Type (u + 1))
        (BigZariskiOver.topology B T.1 T.property)
        (BigZariskiOver.topology B S.1 S.property))

AlgebraicGeometry.bigZariskiLowerShriek_preservesEqualizers, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ZariskiCovering/BigZariskiMorphism.lean, line 183. The attribute's comment: “lower shriek preserves equalizers”.

Stacks 0210. The lower shriek commutes with equalizers.

public instance bigZariskiLowerShriek_preservesEqualizers :
    PreservesLimitsOfShape WalkingParallelPair
      ((Over.map f).sheafPullback (Type (u + 1))
        (BigZariskiOver.topology B T.1 T.property)
        (BigZariskiOver.topology B S.1 S.property))

Declarations registered for the tag:

Tag 0211, a lemma

Tag 0211 in the Stacks Project.

AlgebraicGeometry.exists_smallZariskiBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiBaseChange.lean, line 276. The attribute's comment: “f_small”.

There is a morphism of small Zariski sites from T to S whose underlying functor, after including both small sites into schemes over T and S, is naturally isomorphic to base change along f.

public theorem exists_smallZariskiBaseChange :
    ∃ F : SmallZariski B S.1 S.property ⥤
        SmallZariski B T.1 T.property,
      _root_.IsMorphismOfSites.{u + 1} F
        (SmallZariski.topology B S.1 S.property)
        (SmallZariski.topology B T.1 T.property) ∧
      Nonempty (F ⋙ smallSiteInSchemesOver B T ≅
        smallSiteInSchemesOver B S ⋙ Over.pullback (B.inclusion.map f))

AlgebraicGeometry.smallZariskiBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiBaseChange.lean, line 296. The attribute's comment: “f_small”.

The continuous base-change functor on small Zariski sites.

public noncomputable def smallZariskiBaseChange :
    SmallZariski B S.1 S.property ⥤
      SmallZariski B T.1 T.property

AlgebraicGeometry.smallZariskiBaseChange_isMorphismOfSites_ringUniverse, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiRingedSiteHom.lean, line 171. The attribute's comment: “f_small on small Zariski sites, at the universe of the structure rings”.

Stacks 0211 at the universe of the structure rings. Small Zariski base change along f defines a morphism of sites for sheaves of sets valued in the universe u of the sections of the structure sheaves.

This is the input a morphism of ringed sites needs, and AlgebraicGeometry.smallZariskiBaseChange_isMorphismOfSites does not provide it: that one is stated for sheaves of sets in Type (u + 1), the universe of the objects of the site.

public instance smallZariskiBaseChange_isMorphismOfSites_ringUniverse :
    IsMorphismOfSites.{u} (smallZariskiBaseChange B f)
      (SmallZariski.topology B S.1 S.property) (SmallZariski.topology B T.1 T.property)

AlgebraicGeometry.smallZariskiPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiSpaceFunctors.lean, line 146. The attribute's comment: “usual_small_functors”.

Under the small-site equivalences, inverse image is the usual inverse image of sheaves on the underlying topological spaces.

public noncomputable def smallZariskiPullbackIso :
    (smallZariskiSheafEquiv B S.1 S.property).functor ⋙
      (Opens.map (B.inclusion.map f).base).sheafPullback (Type (u + 1))
        (Opens.grothendieckTopology ((B.inclusion.obj S).toPresheafedSpace : TopCat))
        (Opens.grothendieckTopology ((B.inclusion.obj T).toPresheafedSpace : TopCat)) ≅
      (smallZariskiBaseChange B f).sheafPullback (Type (u + 1))
      (SmallZariski.topology B S.1 S.property)
      (SmallZariski.topology B T.1 T.property) ⋙
      (smallZariskiSheafEquiv B T.1 T.property).functor

AlgebraicGeometry.smallZariskiPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/SmallZariskiSpaceFunctors.lean, line 177. The attribute's comment: “usual_small_functors”.

Under the small-site equivalences, direct image is the usual direct image of sheaves on the underlying topological spaces.

public noncomputable def smallZariskiPushforwardIso :
    (smallZariskiSheafEquiv B T.1 T.property).functor ⋙
      (Opens.map (B.inclusion.map f).base).sheafPushforwardContinuous (Type (u + 1))
        (Opens.grothendieckTopology ((B.inclusion.obj S).toPresheafedSpace : TopCat))
        (Opens.grothendieckTopology ((B.inclusion.obj T).toPresheafedSpace : TopCat)) ≅
      (smallZariskiBaseChange B f).sheafPushforwardContinuous
      (Type (u + 1))
      (SmallZariski.topology B S.1 S.property)
      (SmallZariski.topology B T.1 T.property) ⋙
      (smallZariskiSheafEquiv B S.1 S.property).functor

AlgebraicGeometry.smallZariskiBaseChange_comp_inclusionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiFactorization.lean, line 83. The attribute's comment: “commutative_square”.

The square of functors underlying the four morphisms of Zariski sites commutes up to a natural isomorphism.

public noncomputable def smallZariskiBaseChange_comp_inclusionIso :
    smallZariskiBaseChange B f ⋙
        SmallZariski.inclusion B T.1 T.property ≅
      SmallZariski.inclusion B S.1 S.property ⋙ Over.pullback f

AlgebraicGeometry.smallZariskiProjection_baseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiFactorization.lean, line 110. The attribute's comment: “commutative_square”.

The geometric morphisms satisfy f_small ∘ π_T ≅ π_S ∘ f_big; the isomorphism of inverse-image functors is natural in sheaves.

public noncomputable def smallZariskiProjection_baseChangeIso :
    ((smallZariskiMorphism B T S f).comp
      (smallZariskiProjection B T)).inverseImage ≅
    ((smallZariskiProjection B S).comp
      (bigZariskiMorphism B T S f)).inverseImage

AlgebraicGeometry.smallZariskiToBigZariskiMorphism_factor_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiFactorization.lean, line 163. The attribute's comment: “if_factorization”.

The direct image of i_f agrees naturally with that of f_big ∘ i_T.

public noncomputable def smallZariskiToBigZariskiMorphism_factor_pushforwardIso :
    (smallZariskiToBigZariskiMorphism B T S f).pushforward ≅
      ((bigZariskiMorphism B T S f).comp
        (smallZariskiToBigZariskiMorphism B T T (𝟙 T))).pushforward

AlgebraicGeometry.smallZariskiToBigZariskiMorphism_factor_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiFactorization.lean, line 210. The attribute's comment: “if_factorization”.

The inverse image of i_f agrees naturally with that of f_big ∘ i_T.

public noncomputable def smallZariskiToBigZariskiMorphism_factor_inverseImageIso :
    (smallZariskiToBigZariskiMorphism B T S f).inverseImage ≅
      ((bigZariskiMorphism B T S f).comp
        (smallZariskiToBigZariskiMorphism B T T (𝟙 T))).inverseImage

AlgebraicGeometry.smallZariskiMorphismIsoProjectionCompBig, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiFactorization.lean, line 226. The attribute's comment: “small_factorization”.

The small-site morphism factors through the two big Zariski topoi.

public noncomputable def smallZariskiMorphismIsoProjectionCompBig :
    (smallZariskiMorphism B T S f).inverseImage ≅
      ((smallZariskiProjection B S).comp
        ((bigZariskiMorphism B T S f).comp
          (smallZariskiToBigZariskiMorphism B T T (𝟙 T)))).inverseImage

AlgebraicGeometry.smallZariskiMorphismIsoProjectionCompInclusion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiFactorization.lean, line 255. The attribute's comment: “small_factorization”.

The same morphism factors through i_f and the projection at S.

public noncomputable def smallZariskiMorphismIsoProjectionCompInclusion :
    (smallZariskiMorphism B T S f).inverseImage ≅
      ((smallZariskiProjection B S).comp
        (smallZariskiToBigZariskiMorphism B T S f)).inverseImage
Tag 0212, a lemma

Tag 0212 in the Stacks Project.

AlgebraicGeometry.bigZariskiMorphism_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiMorphismComposition.lean, line 73. The attribute's comment: “the big sites, direct image”.

Stacks 0212. The direct image of g_big ∘ f_big agrees naturally with that of (g ∘ f)_big.

Both are read as restriction along slice base change, where the comparison is the canonical isomorphism (U ×_Z Y) ×_Y X ≅ U ×_Z X of iterated fibre products.

public noncomputable def bigZariskiMorphism_comp_pushforwardIso :
    ((bigZariskiMorphism B Y Z g).comp (bigZariskiMorphism B X Y f)).pushforward ≅
      (bigZariskiMorphism B X Z (f ≫ g)).pushforward

AlgebraicGeometry.bigZariskiMorphism_comp_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiMorphismComposition.lean, line 95. The attribute's comment: “the big sites, inverse image”.

Stacks 0212. The inverse image of g_big ∘ f_big agrees naturally with that of (g ∘ f)_big; the isomorphism is the mate of the direct-image comparison under the three geometric adjunctions.

public noncomputable def bigZariskiMorphism_comp_inverseImageIso :
    ((bigZariskiMorphism B Y Z g).comp (bigZariskiMorphism B X Y f)).inverseImage ≅
      (bigZariskiMorphism B X Z (f ≫ g)).inverseImage

AlgebraicGeometry.smallZariskiMorphism_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiMorphismComposition.lean, line 108. The attribute's comment: “the small sites, direct image”.

Stacks 0212. The direct image of g_small ∘ f_small agrees naturally with that of (g ∘ f)_small, by the composition comparison of the underlying small-site base-change functors.

public noncomputable def smallZariskiMorphism_comp_pushforwardIso :
    ((smallZariskiMorphism B Y Z g).comp (smallZariskiMorphism B X Y f)).pushforward ≅
      (smallZariskiMorphism B X Z (f ≫ g)).pushforward

AlgebraicGeometry.smallZariskiMorphism_comp_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiMorphismComposition.lean, line 121. The attribute's comment: “the small sites, inverse image”.

Stacks 0212. The inverse image of g_small ∘ f_small agrees naturally with that of (g ∘ f)_small; the isomorphism is the mate of the direct-image comparison under the three sheaf adjunctions.

public noncomputable def smallZariskiMorphism_comp_inverseImageIso :
    ((smallZariskiMorphism B Y Z g).comp (smallZariskiMorphism B X Y f)).inverseImage ≅
      (smallZariskiMorphism B X Z (f ≫ g)).inverseImage
Tag 0DD9, a lemma

Tag 0DD9 in the Stacks Project.

AlgebraicGeometry.bigZariskiBaseChange_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiPushforwardBaseChange.lean, line 122. The attribute's comment: “big-site equality”.

Big-site inverse image commutes with big-site direct image around a cartesian square, naturally in the sheaf.

public noncomputable def bigZariskiBaseChange_pushforwardIso
    (h : IsPullback g' f' f g) :
    (bigZariskiMorphism B T S f).pushforward ⋙
        (bigZariskiMorphism B S' S g).inverseImage ≅
      (bigZariskiMorphism B T' T g').inverseImage ⋙
        (bigZariskiMorphism B T' S' f').pushforward

AlgebraicGeometry.smallZariskiBaseChange_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/ZariskiPushforwardBaseChange.lean, line 210. The attribute's comment: “small-site equality”.

Restricting a big-site direct image to the small site of S' agrees, naturally, with restricting to the small site of T' and taking the small-site direct image.

public noncomputable def smallZariskiBaseChange_pushforwardIso
    (h : IsPullback g' f' f g) :
    (bigZariskiMorphism B T S f).pushforward ⋙
        (smallZariskiToBigZariskiMorphism B S' S g).inverseImage ≅
      (smallZariskiToBigZariskiMorphism B T' T g').inverseImage ⋙
        (smallZariskiBaseChange B f').sheafPushforwardContinuous
          (Type (u + 1))
          (SmallZariski.topology B S'.1 S'.property)
          (SmallZariski.topology B T'.1 T'.property)
Tag 0213, a lemma

Tag 0213 in the Stacks Project.

AlgebraicGeometry.BigZariskiSheafData, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigZariski/CompatibleData.lean, line 45. The attribute's comment: “the compatible data”.

A sheaf on each scheme over S, with compatible inverse-image comparisons.

public structure BigZariskiSheafData

AlgebraicGeometry.characterizeSheafBigZariski, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigZariski/Equivalence.lean, line 673. The attribute's comment: “equivalence of categories”.

The canonical restriction functor is an equivalence of categories.

public noncomputable def characterizeSheafBigZariski :
    Sheaf (BigZariskiOver.topology B S hS) (Type (max u v)) ≌
      BigZariskiSheafData.{u, v} B S hS

AlgebraicGeometry.characterizeSheafBigZariski_functor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigZariski/Equivalence.lean, line 682. The attribute's comment: “canonicality of the equivalence”.

The equivalence uses the canonical restriction functor, not an arbitrary equivalent object assignment.

public theorem characterizeSheafBigZariski_functor :
    (characterizeSheafBigZariski.{u, v} B S hS).functor =
      bigZariskiSheafRestriction.{u, v} B S hS

AlgebraicGeometry.bigZariskiSheafRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigZariski/Restriction.lean, line 48. The attribute's comment: “canonical restriction functor”.

The canonical restriction of a big-site sheaf to all ordinary Zariski sites, including its comparison maps induced by big-site restrictions.

public noncomputable def bigZariskiSheafRestriction :
    Sheaf (BigZariskiOver.topology B S hS) (Type (max u v)) ⥤
      BigZariskiSheafData.{u, v} B S hS

AlgebraicGeometry.bigZariskiSheafRestriction_sectionEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigZariski/Restriction.lean, line 160. The attribute's comment: “canonical identification of sections”.

Global sections of the canonical restriction at a scheme are the sections of the original big-site sheaf at that scheme.

public noncomputable def bigZariskiSheafRestriction_sectionEquiv
    (F : Sheaf (BigZariskiOver.topology B S hS) (Type (max u v)))
    (T : BigZariskiOver B S hS) :
    (((bigZariskiSheafRestriction.{u, v} B S hS).obj F).sheaf T).1.obj (op ⊤) ≃
      F.1.obj (op T)

AlgebraicGeometry.bigZariskiSheafRestriction_sectionEquiv_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigZariski/Restriction.lean, line 169. The attribute's comment: “naturality of section identification”.

The identification of global sections is natural in the big-site sheaf.

public theorem bigZariskiSheafRestriction_sectionEquiv_naturality
    {F G : Sheaf (BigZariskiOver.topology B S hS) (Type (max u v))}
    (α : F ⟶ G) (T : BigZariskiOver B S hS)
    (s : (((bigZariskiSheafRestriction.{u, v} B S hS).obj F).sheaf T).1.obj (op ⊤)) :
  bigZariskiSheafRestriction_sectionEquiv B S hS G T
      (((((bigZariskiSheafRestriction.{u, v} B S hS).map α).app T).1.app (op ⊤)) s) =
    α.1.app (op T)
      (bigZariskiSheafRestriction_sectionEquiv B S hS F T s)

AlgebraicGeometry.bigZariskiSheafRestriction_pullback_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigZariski/Restriction.lean, line 222. The attribute's comment: “canonicality of pullback comparisons”.

Under the canonical identifications of global sections, the pullback comparison is exactly the restriction map of the big-site sheaf. Applying this to every object, including open subschemes, controls the comparison on opens.

public theorem bigZariskiSheafRestriction_pullback_sections
    (F : Sheaf (BigZariskiOver.topology B S hS) (Type (max u v)))
    {T T' : BigZariskiOver B S hS} (f : T' ⟶ T)
    (s : F.1.obj (op T)) :
    let D := (bigZariskiSheafRestriction.{u, v} B S hS).obj F
    let ftop := (B.inclusion.map f.left).base
    let η := (TopCat.Sheaf.inverseImagePushforwardAdjunction.{u, v} ftop).unit.app
      (D.sheaf T)
    bigZariskiSheafRestriction_sectionEquiv B S hS F T'
      ((D.pullback f).1.app (op ⊤)
        (η.1.app (op ⊤)
          ((bigZariskiSheafRestriction_sectionEquiv B S hS F T).symm s))) =
      F.1.map f.op s

AlgebraicGeometry.bigZariskiSheafRestriction_sheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigZariski/Restriction.lean, line 284. The attribute's comment: “canonical sheaf on each scheme”.

At each scheme over S the sheaf produced by canonical restriction is the inverse image of the big-site sheaf along the small-to-big morphism of topoi, transported to the space of that scheme.

public noncomputable def bigZariskiSheafRestriction_sheaf
    (F : Sheaf (BigZariskiOver.topology B S hS) (Type (max u v)))
    (T : BigZariskiOver B S hS) :
    ((bigZariskiSheafRestriction.{u, v} B S hS).obj F).sheaf T ≅
      canonicalSmallSheaf B S hS F T

AlgebraicGeometry.bigZariskiSheafRestriction_sheafNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigZariski/Restriction.lean, line 294. The attribute's comment: “naturality on opens and in the sheaf”.

The componentwise identification is natural in the big-site sheaf; hence its maps on every open subset are the canonical restriction maps.

public noncomputable def bigZariskiSheafRestriction_sheafNatIso
    (T : BigZariskiOver B S hS) :
    bigZariskiSheafRestriction.{u, v} B S hS ⋙ BigZariskiSheafData.eval B S hS T ≅
      canonicalSmallSheafFunctor.{u, v} B S hS T
Sources
LeanAlgebraicGeometry.Scheme.zariskiPrecoverage · AlgebraicGeometry.Scheme.OpenCover · AlgebraicGeometry.Scheme.zariskiPretopology · AlgebraicGeometry.Scheme.OpenCover.exists_isStandardZariski_refinement · AlgebraicGeometry.IsStandardZariskiCovering · AlgebraicGeometry.BigZariskiSite · AlgebraicGeometry.BigZariskiSite.exists_isCovering_tautologicallyEquivalent_openCover · AlgebraicGeometry.BigZariskiOver

Section34.4 The étale topology#

Section 34.4 of the Stacks Project, Tag 0214. 20 tags here are carried by 78 declarations of the repository (all in StacksFrontier) and 14 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0215, a definition

Tag 0215 in the Stacks Project.

Declarations registered for the tag:

Tag 0216, a lemma

Tag 0216 in the Stacks Project.

AlgebraicGeometry.Scheme.zariskiPrecoverage_le_etalePrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SmoothAndStandardEtaleCoverings.lean, line 67.

Every Zariski covering is an étale covering.

public theorem zariskiPrecoverage_le_etalePrecoverage :
    zariskiPrecoverage.{u} ≤ etalePrecoverage
Tag 0217, a lemma

Tag 0217 in the Stacks Project.

Declarations registered for the tag:

Tag 0218, a lemma

Tag 0218 in the Stacks Project.

AlgebraicGeometry.exists_finite_affine_etaleCovering_le_of_mem_etaleTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/ChosenEtaleAffineRefinement.lean, line 69. The attribute's comment: “for the étale subcollection of a big fppf site, inside a covering sieve”.

Stacks 0218 for the étale subcollection of a big fppf site. A covering sieve of the big étale topology AlgebraicGeometry.etaleTopology B at an object X whose underlying scheme is affine contains a selected étale covering family of X which is finite and whose members again have affine underlying scheme.

This is the étale analogue of AlgebraicGeometry.exists_standardFppf_refinement (Stacks 021P) on the same category, and it is proved by reading the étale subcollection as the big étale site AlgebraicGeometry.BigFppfSite.toBigEtaleSite and applying AlgebraicGeometry.BigEtaleSite.exists_finite_affine_refinement there; see the module documentation.

theorem exists_finite_affine_etaleCovering_le_of_mem_etaleTopology (B : BigFppfSite.{u})
    {X : B.Schemes} (hX : IsAffine (B.inclusion.obj X))
    {R : Sieve X} (hR : R ∈ etaleTopology B X) :
    ∃ E : PreZeroHypercover.{u + 1} X, etaleCovering B ⟨X, E⟩ ∧ Finite E.I₀ ∧
      (∀ i, IsAffine (B.inclusion.obj (E.X i))) ∧ E.presieve₀ ≤ R.arrows

Declarations registered for the tag:

Tag 0219, a definition

Tag 0219 in the Stacks Project.

AlgebraicGeometry.IsStandardEtaleCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SmoothAndStandardEtaleCoverings.lean, line 50.

A standard étale covering of an affine scheme T: a finite family of étale morphisms f i : U i ⟶ T with affine sources whose images cover T, that is, the étale case of AlgebraicGeometry.IsStandardCovering.

public abbrev IsStandardEtaleCovering {T : Scheme.{u}} [IsAffine T] {I : Type v}
    (U : I → Scheme.{u}) (f : ∀ i, U i ⟶ T) : Prop
Tag 021A, a definition

Tag 021A in the Stacks Project.

AlgebraicGeometry.BigEtaleSite, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale.lean, line 80.

A big étale site: a size-bounded full category of schemes and a chosen bounded class of étale covering families on it, containing an initial set of schemes and an initial set of étale coverings.

public structure BigEtaleSite

Declarations registered for the tag:

Tag 03WW, a lemma

Tag 03WW in the Stacks Project.

AlgebraicGeometry.BigEtaleSite.exists_covering_refining_etale_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BigSiteCoverings.lean, line 82. The attribute's comment: “etale_refinement”.

Stacks Project, Tag 03WW. Every étale covering family of an object of a big étale site, formed in the ambient category of schemes, is refined by a covering family internal to the site.

public theorem exists_covering_refining_etale_cover
    (B : AlgebraicGeometry.BigEtaleSite.{u}) {T : B.Scheme}
    (𝒰 : PreZeroHypercover.{u + 1} (B.inclusion.obj T))
    (h𝒰 : 𝒰.presieve₀ ∈ Scheme.etalePrecoverage (B.inclusion.obj T)) :
    ∃ 𝒱 : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, 𝒱⟩ ∧ Nonempty ((𝒱.map B.inclusion).Hom 𝒰)

AlgebraicGeometry.BigEtaleSite.exists_isCovering_tautologicallyEquivalent_affineCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BigSiteCoverings.lean, line 166. The attribute's comment: “standard_etale_equivalence”.

Stacks Project, Tag 03WW. A standard étale covering of an object of a big étale site is tautologically equivalent to a covering belonging to that site.

public theorem exists_isCovering_tautologicallyEquivalent_affineCover
    (B : AlgebraicGeometry.BigEtaleSite.{u}) (T : B.Scheme)
    [IsAffine (B.inclusion.obj T)]
    (U : (B.inclusion.obj T).AffineCover.{u + 1} @Etale) [Finite U.I₀] :
    ∃ V : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, V⟩ ∧
        PreZeroHypercover.TautologicallyEquivalent U.cover.toPreZeroHypercover
          (V.map B.inclusion)

AlgebraicGeometry.BigEtaleSite.exists_isCovering_tautologicallyEquivalent_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BigSiteCoverings.lean, line 192. The attribute's comment: “zariski_equivalence”.

Stacks Project, Tag 03WW. A Zariski covering of an object of a big étale site is tautologically equivalent to a covering belonging to that site.

public theorem exists_isCovering_tautologicallyEquivalent_openCover
    (B : AlgebraicGeometry.BigEtaleSite.{u}) (T : B.Scheme)
    (U : (B.inclusion.obj T).OpenCover.{u + 1}) :
    ∃ V : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, V⟩ ∧
        PreZeroHypercover.TautologicallyEquivalent U.toPreZeroHypercover
          (V.map B.inclusion)
Tag 021B, a definition

Tag 021B in the Stacks Project.

AlgebraicGeometry.BigEtaleOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Sites.lean, line 73. The attribute's comment: “part (1), category”. References: SGA 4 XVII (0.10), “big étale site”.

Stacks 021B, part (1). The underlying category of the big étale site of S is the slice of the chosen big étale category over S.

public abbrev BigEtaleOver

AlgebraicGeometry.BigEtaleOver.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Sites.lean, line 88. The attribute's comment: “part (1), coverings”. References: SGA 4 XVII (0.10), “big étale site”.

Stacks 021B, part (1). A family in the slice is covering precisely when its underlying family is a covering in the chosen big étale site.

public abbrev IsCovering (E : Covering (BigEtaleOver B S hS)) : Prop

AlgebraicGeometry.SmallEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Sites.lean, line 132. The attribute's comment: “part (2), category”.

Stacks 021B, part (2). The small étale category of S is the full subcategory of the big étale category over S consisting of objects étale over S.

public abbrev SmallEtale

AlgebraicGeometry.SmallEtale.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Sites.lean, line 153. The attribute's comment: “part (2), coverings”.

Stacks 021B, part (2). A family in the small étale category is covering when its image in the big étale category over S is covering.

public abbrev IsCovering (E : Covering (SmallEtale B S hS)) : Prop

AlgebraicGeometry.BigAffineEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Sites.lean, line 179. The attribute's comment: “part (3), category”.

Stacks 021B, part (3). The big affine étale category over S is the full subcategory of the big étale category over S consisting of affine source schemes.

public abbrev BigAffineEtale

AlgebraicGeometry.BigAffineEtale.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Sites.lean, line 200. The attribute's comment: “part (3), coverings”.

Stacks 021B, part (3). A family in the big affine étale category is covering when its image in the big étale category over S is a standard étale covering.

public abbrev IsCovering (E : Covering (BigAffineEtale B S hS)) : Prop

AlgebraicGeometry.SmallAffineEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Sites.lean, line 231. The attribute's comment: “part (4), category”.

Stacks 021B, part (4). The small affine étale category of S is the full subcategory of the small étale category consisting of affine schemes.

public abbrev SmallAffineEtale

AlgebraicGeometry.SmallAffineEtale.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Sites.lean, line 253. The attribute's comment: “part (4), coverings”.

Stacks 021B, part (4). A family in the small affine étale category is covering when its image in the small étale category is covering and it is finite (hence standard étale, since its source objects are affine).

public abbrev IsCovering (E : Covering (SmallAffineEtale B S hS)) : Prop
Tag 021C, a lemma

Tag 021C in the Stacks Project.

AlgebraicGeometry.SmallEtale.isSite, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SiteAxioms.lean, line 70. The attribute's comment: “small_etale_site”.

Stacks 021C, small étale site. The étale covering families on the small étale category of a scheme satisfy the axioms of a site.

public lemma SmallEtale.isSite (B : AlgebraicGeometry.BigEtaleSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) : IsSite (SmallEtale.IsCovering B S hS)

AlgebraicGeometry.BigAffineEtale.isSite, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SiteAxioms.lean, line 111. The attribute's comment: “big_affine_etale_site”.

Stacks 021C, big affine étale site. The standard étale covering families of affine objects over S satisfy the site axioms.

public lemma BigAffineEtale.isSite (B : AlgebraicGeometry.BigEtaleSite.{u})
    (S : Scheme.{u})
    (hS : B.Contains S) : IsSite (BigAffineEtale.IsCovering B S hS)

AlgebraicGeometry.SmallAffineEtale.isSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SiteAxioms.lean, line 177. The attribute's comment: “small_affine_etale_site”.

Stacks 021C, small affine étale site. The standard étale covering families on the small affine étale category of a scheme satisfy the axioms of a site.

public theorem SmallAffineEtale.isSite (B : AlgebraicGeometry.BigEtaleSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) :
    IsSite (SmallAffineEtale.IsCovering B S hS)
Tag 021D, a lemma

Tag 021D in the Stacks Project.

AlgebraicGeometry.hasPullbacks_bigEtaleSite, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Limits.lean, line 75. The attribute's comment: “fibre products in the big étale site”.

The underlying category of a big étale site admits fibre products.

public instance hasPullbacks_bigEtaleSite : HasPullbacks B.Scheme

AlgebraicGeometry.hasPullbacks_smallEtale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Limits.lean, line 102. The attribute's comment: “fibre products in the small étale site”.

The small étale category of S admits fibre products.

public instance hasPullbacks_smallEtale :
    HasPullbacks (SmallEtale B S hS)

AlgebraicGeometry.preservesPullbacks_smallEtaleToScheme, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Limits.lean, line 118. The attribute's comment: “preservation by the small étale functor to schemes”.

The canonical functor from the small étale category of S to schemes preserves fibre products.

public instance preservesPullbacks_smallEtaleToScheme :
    PreservesLimitsOfShape WalkingCospan (SmallEtale.toScheme B S hS)

AlgebraicGeometry.hasPullbacks_bigAffineEtale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Limits.lean, line 129. The attribute's comment: “fibre products in the big affine étale site”.

The category of affine objects in the big étale category over S admits fibre products.

public instance hasPullbacks_bigAffineEtale :
    HasPullbacks (BigAffineEtale B S hS)

AlgebraicGeometry.hasPullbacks_smallAffineEtale, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Limits.lean, line 139. The attribute's comment: “fibre products in the affine small étale site”.

The affine small étale category of S admits fibre products.

public instance hasPullbacks_smallAffineEtale :
    HasPullbacks (SmallAffineEtale B S hS)

AlgebraicGeometry.preservesPullbacks_bigEtaleSiteInclusion, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Limits.lean, line 146. The attribute's comment: “preservation by the big étale site inclusion”.

The inclusion of a big étale site's underlying category into schemes preserves fibre products.

public instance preservesPullbacks_bigEtaleSiteInclusion :
    PreservesLimitsOfShape WalkingCospan B.inclusion

AlgebraicGeometry.preservesPullbacks_bigAffineEtaleToScheme, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Limits.lean, line 157. The attribute's comment: “preservation by the big affine étale functor to schemes”.

The canonical functor from affine objects over S to schemes preserves fibre products.

public instance preservesPullbacks_bigAffineEtaleToScheme :
    PreservesLimitsOfShape WalkingCospan (BigAffineEtale.toScheme B S hS)

AlgebraicGeometry.preservesPullbacks_smallAffineEtaleToScheme, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Limits.lean, line 164. The attribute's comment: “preservation by the affine small étale functor to schemes”.

The canonical functor from the affine small étale category of S to schemes preserves fibre products.

public instance preservesPullbacks_smallAffineEtaleToScheme :
    PreservesLimitsOfShape WalkingCospan
      (SmallAffineEtale.toScheme B S hS)

AlgebraicGeometry.SmallEtale.finalIsTerminal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Limits.lean, line 180. The attribute's comment: “the final object of the small étale site”.

The object S / S is final in the small étale category of S.

public noncomputable def SmallEtale.finalIsTerminal :
    IsTerminal (SmallEtale.final B S hS)

Declarations registered for the tag:

Tag 021E, a lemma

Tag 021E in the Stacks Project.

AlgebraicGeometry.BigAffineEtale.inclusion_isSpecialCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/AffineDenseSubsite.lean, line 359.

Stacks 021E. The inclusion of the big affine étale site over a scheme into its big étale site is special cocontinuous. Its dense-subsite component gives the induced equivalence of topoi.

public theorem BigAffineEtale.inclusion_isSpecialCocontinuous
    (B : AlgebraicGeometry.BigEtaleSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    IsSpecialCocontinuous
      (BigAffineEtale.topology B S hS)
      (BigEtaleOver.topology B S hS)
      (BigAffineEtale.inclusion B S hS)
Tag 04HR, a lemma

Tag 04HR in the Stacks Project.

AlgebraicGeometry.SmallAffineEtale.sheafEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/SmallEtaleAffineSheafEquiv.lean, line 67. The attribute's comment: “the induced equivalence of topoi Sh(S_{affine,étale}) ≌ Sh(S_étale), for sheaves of sets with values in Type (u + 1)”.

Stacks 04HR on sheaves of sets. Restriction along the inclusion of the small affine étale site of S into its small étale site is an equivalence of categories of sheaves of sets with values in Type (u + 1). No affineness of S is needed.

public noncomputable def sheafEquiv :
    Sheaf (topology B S hS) (Type (u + 1)) ≌
      Sheaf (SmallEtale.topology B S hS) (Type (u + 1))

AlgebraicGeometry.SmallAffineEtale.inclusion_isSpecialCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PointsOtherTopologies/SmallEtale.lean, line 372.

The inclusion of the small affine étale site of a scheme into its small étale site is a special cocontinuous functor.

public theorem SmallAffineEtale.inclusion_isSpecialCocontinuous
    (B : AlgebraicGeometry.BigEtaleSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    IsSpecialCocontinuous
      (AlgebraicGeometry.SmallAffineEtale.topology B S hS)
      (AlgebraicGeometry.SmallEtale.topology B S hS)
      (AlgebraicGeometry.SmallAffineEtale.inclusion B S hS)
Tag 021F, a lemma

Tag 021F in the Stacks Project.

AlgebraicGeometry.smallEtaleToBigEtaleToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/RingedToposIf.lean, line 197. The attribute's comment: “the morphism of topoi, at the universe of the structure rings”.

Stacks 021F at the universe of the structure rings. The morphism of topoi i_f : \mathrm{Sh}(T_\etale) ⟶ \mathrm{Sh}((\Sch/S)_\etale) on sheaves of sets in Type u.

public noncomputable def smallEtaleToBigEtaleToposHom :
    MorphismOfTopoi (Sheaf (SmallEtale.topology B T.obj T.property) (Type u))
      (Sheaf (BigEtaleOver.topology B S.obj S.property) (Type u))

AlgebraicGeometry.smallEtaleToBigEtaleFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallToBigTopos.lean, line 83. The attribute's comment: “the functor”.

Send an étale object U / T to the composite U / S.

public abbrev smallEtaleToBigEtaleFunctor :
    SmallEtale B T.obj T.property ⥤ BigEtaleOver B S.obj S.property

AlgebraicGeometry.smallEtaleToBigEtaleFunctor_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallToBigTopos.lean, line 215. The attribute's comment: “cocontinuity”.

Postcomposition from the small étale site of T to the big étale site over S is cocontinuous.

public instance smallEtaleToBigEtaleFunctor_isCocontinuous :
    (smallEtaleToBigEtaleFunctor B T S f).IsCocontinuous
      (SmallEtale.topology B T.obj T.property)
      (BigEtaleOver.topology B S.obj S.property)

AlgebraicGeometry.smallEtaleToBigEtaleFunctor_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallToBigTopos.lean, line 255. The attribute's comment: “continuity”.

Postcomposition also preserves coverings and fibre products, hence is continuous.

public instance smallEtaleToBigEtaleFunctor_isContinuous :
    (smallEtaleToBigEtaleFunctor B T S f).IsContinuous
      (SmallEtale.topology B T.obj T.property)
      (BigEtaleOver.topology B S.obj S.property)

AlgebraicGeometry.smallEtaleToBigEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallToBigTopos.lean, line 265. The attribute's comment: “the morphism of topoi”.

The geometric morphism i_f : Sh(Tₑₜ) ⟶ Sh((Sch/S)ₑₜ) induced by postcomposition.

public noncomputable def smallEtaleToBigEtaleMorphism :
    MorphismOfTopoi
      (Sheaf (SmallEtale.topology B T.obj T.property) (Type (u + 1)))
      (Sheaf (BigEtaleOver.topology B S.obj S.property) (Type (u + 1)))

AlgebraicGeometry.smallEtaleToBigEtaleLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallToBigTopos.lean, line 290. The attribute's comment: “existence of lower shriek”.

The lower shriek is left adjoint to inverse image.

public noncomputable def smallEtaleToBigEtaleLowerShriekAdjunction :
    smallEtaleToBigEtaleLowerShriek B T S f ⊣
      (smallEtaleToBigEtaleMorphism B T S f).inverseImage

AlgebraicGeometry.smallEtaleToBigEtaleLowerShriek_preservesPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallToBigTopos.lean, line 306. The attribute's comment: “lower shriek preserves fibre products”.

The lower shriek preserves fibre products.

public instance smallEtaleToBigEtaleLowerShriek_preservesPullbacks :
    PreservesLimitsOfShape WalkingCospan
      (smallEtaleToBigEtaleLowerShriek B T S f)

AlgebraicGeometry.smallEtaleToBigEtaleLowerShriek_preservesEqualizers, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallToBigTopos.lean, line 315. The attribute's comment: “lower shriek preserves equalizers”.

The lower shriek preserves equalizers.

public instance smallEtaleToBigEtaleLowerShriek_preservesEqualizers :
    PreservesLimitsOfShape WalkingParallelPair
      (smallEtaleToBigEtaleLowerShriek B T S f)

Declarations registered for the tag:

Tag 021G, a lemma

Tag 021G in the Stacks Project.

AlgebraicGeometry.smallEtaleInclusion_isMorphismOfSites_ringUniverse, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/RingedProjectionAndIf.lean, line 191. The attribute's comment: “the morphism of sites, at the universe of the structure rings”.

The inclusion of the small étale site of S into the big étale site over S defines a morphism of sites for sheaves of sets valued in the universe of the sections of the structure sheaves.

AlgebraicGeometry.smallEtaleInclusion_isMorphismOfSites is the same assertion for sheaves of sets in Type (u + 1), the universe of the objects of the sites; neither implies the other.

public instance smallEtaleInclusion_isMorphismOfSites_ringUniverse :
    IsMorphismOfSites.{u} (SmallEtale.inclusion B S.obj S.property)
      (SmallEtale.topology B S.obj S.property) (BigEtaleOver.topology B S.obj S.property)

AlgebraicGeometry.smallEtaleInclusion_preservesTerminal, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/Limits.lean, line 200. The attribute's comment: “preservation of the final object”.

The inclusion of the small étale category carries its final object to the final object of the big étale slice.

public instance smallEtaleInclusion_preservesTerminal :
    PreservesLimit (Functor.empty.{0} (SmallEtale B S hS))
      (SmallEtale.inclusion B S hS)

AlgebraicGeometry.smallEtaleInclusion_isMorphismOfSites, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleProjection.lean, line 94. The attribute's comment: “the morphism of sites”.

The full inclusion of the small étale site defines a morphism of sites from the big étale slice to the small étale site.

public instance smallEtaleInclusion_isMorphismOfSites :
    _root_.IsMorphismOfSites.{u + 1} (SmallEtale.inclusion B S hS)
      (SmallEtale.topology B S hS) (BigEtaleOver.topology B S hS)

AlgebraicGeometry.bigEtaleToSmallEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleProjection.lean, line 149. The attribute's comment: “the projection of topoi”.

The geometric morphism π_S associated to the inclusion of the small étale site into the big étale slice.

public noncomputable def bigEtaleToSmallEtaleMorphism :
    MorphismOfTopoi
      (Sheaf (BigEtaleOver.topology B S hS) (Type (u + 1)))
      (Sheaf (SmallEtale.topology B S hS) (Type (u + 1)))

AlgebraicGeometry.projectionCompInclusionPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleProjection.lean, line 166. The attribute's comment: “the section property”.

The composite π_S ∘ i_S is naturally the identity of the small étale topos, where i_S is the geometric morphism attached to 𝟙_S.

public noncomputable def projectionCompInclusionPushforwardIso :
    (smallEtaleToBigEtaleMorphism B (B.obj S hS) (B.obj S hS)
        (𝟙 (B.obj S hS))).pushforward ⋙
      (bigEtaleToSmallEtaleMorphism B S hS).pushforward ≅
        𝟭 (Sheaf (SmallEtale.topology B S hS) (Type (u + 1)))

AlgebraicGeometry.inclusionInverseImageIsoProjectionPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleProjection.lean, line 211. The attribute's comment: “inverse image is restriction”.

Inverse image along i_S is naturally restriction to the small étale site, equivalently direct image along π_S.

public noncomputable def inclusionInverseImageIsoProjectionPushforward :
    (smallEtaleToBigEtaleMorphism B (B.obj S hS) (B.obj S hS)
        (𝟙 (B.obj S hS))).inverseImage ≅
      (bigEtaleToSmallEtaleMorphism B S hS).pushforward
Tag 04BT, a definition

Tag 04BT in the Stacks Project.

AlgebraicGeometry.inclusionInverseImageIsoProjectionPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleProjection.lean, line 211. The attribute's comment: “restriction to the small étale site, i.e. i_S^{-1} = π_{S,*}”.

Inverse image along i_S is naturally restriction to the small étale site, equivalently direct image along π_S.

public noncomputable def inclusionInverseImageIsoProjectionPushforward :
    (smallEtaleToBigEtaleMorphism B (B.obj S hS) (B.obj S hS)
        (𝟙 (B.obj S hS))).inverseImage ≅
      (bigEtaleToSmallEtaleMorphism B S hS).pushforward
Tag 021H, a lemma

Tag 021H in the Stacks Project.

AlgebraicGeometry.bigEtaleMap_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BigEtaleMorphism.lean, line 83. The attribute's comment: “cocontinuity”.

Stacks 021H. Composition with f is cocontinuous for the big étale topologies.

public instance bigEtaleMap_isCocontinuous :
    (Over.map f).IsCocontinuous
      (BigEtaleOver.topology B T.obj T.property)
      (BigEtaleOver.topology B S.obj S.property)

AlgebraicGeometry.bigEtaleMap_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BigEtaleMorphism.lean, line 94. The attribute's comment: “continuity”.

Composition with f is also continuous. This is the continuity used to identify inverse image with restriction and to construct the lower shriek.

public instance bigEtaleMap_isContinuous :
    (Over.map f).IsContinuous
      (BigEtaleOver.topology B T.obj T.property)
      (BigEtaleOver.topology B S.obj S.property)

AlgebraicGeometry.bigEtalePullback_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BigEtaleMorphism.lean, line 105. The attribute's comment: “continuity of the base-change right adjoint”.

Stacks 021H. Pullback along f, sending U / S to the canonical fibre product U ×_S T / T, is continuous for the big étale topologies.

public instance bigEtalePullback_isContinuous :
    (Over.pullback f).IsContinuous
      (BigEtaleOver.topology B S.obj S.property)
      (BigEtaleOver.topology B T.obj T.property)

AlgebraicGeometry.bigEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BigEtaleMorphism.lean, line 116. The attribute's comment: “the morphism of topoi”.

Stacks 021H. The morphism of big étale topoi induced by the cocontinuous functor Over.map f.

public noncomputable def bigEtaleMorphism (f : T ⟶ S) :
    MorphismOfTopoi
      (Sheaf (BigEtaleOver.topology B T.obj T.property) (Type (u + 1)))
      (Sheaf (BigEtaleOver.topology B S.obj S.property) (Type (u + 1)))

AlgebraicGeometry.bigEtaleMorphismInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BigEtaleMorphism.lean, line 139. The attribute's comment: “the inverse-image formula”.

Stacks 021H. Inverse image is restriction along composition with f. On an object U / T, this is the formula f_big⁻¹(G)(U / T) ≅ G(U / S).

public noncomputable def bigEtaleMorphismInverseImageIso :
    (bigEtaleMorphism B T S f).inverseImage ≅
      (Over.map f).sheafPushforwardContinuous (Type (u + 1))
        (BigEtaleOver.topology B T.obj T.property)
        (BigEtaleOver.topology B S.obj S.property)

AlgebraicGeometry.bigEtaleMorphismPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BigEtaleMorphism.lean, line 151. The attribute's comment: “the direct-image formula”.

Stacks 021H. Direct image is restriction along base change. On an object U / S, this is the formula f_big,*(F)(U / S) ≅ F(U ×_S T / T).

public noncomputable def bigEtaleMorphismPushforwardIso :
    (bigEtaleMorphism B T S f).pushforward ≅
      (Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
        (BigEtaleOver.topology B S.obj S.property)
        (BigEtaleOver.topology B T.obj T.property)

AlgebraicGeometry.bigEtaleLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BigEtaleMorphism.lean, line 162. The attribute's comment: “existence of lower shriek”.

Stacks 021H. The inverse-image functor has the sheaf pullback along postcomposition as a left adjoint; this is f_big!.

public noncomputable def bigEtaleLowerShriekAdjunction :
    (Over.map f).sheafPullback (Type (u + 1))
      (BigEtaleOver.topology B T.obj T.property)
      (BigEtaleOver.topology B S.obj S.property) ⊣
        (bigEtaleMorphism B T S f).inverseImage

AlgebraicGeometry.bigEtaleLowerShriek_preservesPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BigEtaleMorphism.lean, line 177. The attribute's comment: “lower shriek preserves fibre products”.

Stacks 021H. The lower shriek commutes with fibre products.

public instance bigEtaleLowerShriek_preservesPullbacks :
    PreservesLimitsOfShape WalkingCospan
      ((Over.map f).sheafPullback (Type (u + 1))
        (BigEtaleOver.topology B T.obj T.property)
        (BigEtaleOver.topology B S.obj S.property))

AlgebraicGeometry.bigEtaleLowerShriek_preservesEqualizers, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BigEtaleMorphism.lean, line 191. The attribute's comment: “lower shriek preserves equalizers”.

Stacks 021H. The lower shriek commutes with equalizers.

public instance bigEtaleLowerShriek_preservesEqualizers :
    PreservesLimitsOfShape WalkingParallelPair
      ((Over.map f).sheafPullback (Type (u + 1))
        (BigEtaleOver.topology B T.obj T.property)
        (BigEtaleOver.topology B S.obj S.property))

Declarations registered for the tag:

Tag 021I, a lemma

Tag 021I in the Stacks Project.

AlgebraicGeometry.smallEtaleRestrictionProjectionPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ProjectionPullback.lean, line 170. The attribute's comment: “small-site factorization, inverse images”.

i_f^{-1}π_S^{-1} = f_{small}^{-1}. Pulling a sheaf back from the small étale site of S to the big étale site over S and then restricting it to the small étale site of T along f is pulling it back along f_{small} directly.

This is the identity the clauses of Stacks 0DDH about π_S^{-1} reduce to: it converts the comparison of big-site cohomology over T with small-site cohomology of i_f^{-1} into a statement about f_{small}^{-1}.

public def smallEtaleRestrictionProjectionPullbackIso :
    (SmallEtale.inclusion B S.obj S.property).sheafPullback A
        (SmallEtale.topology B S.obj S.property)
        (BigEtaleOver.topology B S.obj S.property) ⋙
      (smallEtaleToBigEtaleFunctor B T S f).sheafPushforwardContinuous A
        (SmallEtale.topology B T.obj T.property)
        (BigEtaleOver.topology B S.obj S.property) ≅
    (smallEtaleBaseChange B f).sheafPullback A
      (SmallEtale.topology B S.obj S.property)
      (SmallEtale.topology B T.obj T.property)

AlgebraicGeometry.smallEtaleBaseChange_isMorphismOfSites_ringUniverse, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/RingedSiteHom.lean, line 205. The attribute's comment: “small_etale_morphism at the universe of the structure rings”.

Stacks 021I at the universe of the structure rings. Base change along f : T ⟶ S defines a morphism of sites from the small étale site of T to that of S, for sheaves of sets valued in the universe u of the sections of the structure sheaves.

public instance smallEtaleBaseChange_isMorphismOfSites_ringUniverse :
    IsMorphismOfSites.{u} (smallEtaleBaseChange B f)
      (SmallEtale.topology B S.obj S.property)
      (SmallEtale.topology B T.obj T.property)

AlgebraicGeometry.smallEtaleBaseChange_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleBaseChange.lean, line 247. The attribute's comment: “base_change_continuous”.

Stacks 021I, base-change continuity. Base change along a morphism in a big étale site is a continuous functor between the corresponding small étale sites.

public instance smallEtaleBaseChange_isContinuous {S T : B.Scheme} (f : T ⟶ S) :
    Functor.IsContinuous (smallEtaleBaseChange B f)
      (SmallEtale.topology B S.obj S.property)
      (SmallEtale.topology B T.obj T.property)

AlgebraicGeometry.smallEtaleBaseChange_isMorphismOfSites, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleBaseChange.lean, line 262. The attribute's comment: “small_etale_morphism”.

Stacks 021I, small étale morphism. Base change along f : T ⟶ S defines a morphism of sites from the small étale site of T to that of S.

public instance smallEtaleBaseChange_isMorphismOfSites {S T : B.Scheme} (f : T ⟶ S) :
    IsMorphismOfSites.{u + 1} (smallEtaleBaseChange B f)
      (SmallEtale.topology B S.obj S.property)
      (SmallEtale.topology B T.obj T.property)

AlgebraicGeometry.bigSmallEtalePushforwardCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleBaseChange.lean, line 327. The attribute's comment: “commutative_diagram”.

Stacks 021I, commutative diagram. The square formed by small étale base change, big étale base change, and the two projections from big to small étale topoi commutes on direct images.

public noncomputable def bigSmallEtalePushforwardCommIso :
    (bigEtaleToSmallEtaleMorphism B T.obj T.property).pushforward ⋙
        (smallEtaleBaseChange B f).sheafPushforwardContinuous
          (Type (u + 1)) (SmallEtale.topology B S.obj S.property)
          (SmallEtale.topology B T.obj T.property) ≅
      (bigEtaleMorphism B T S f).pushforward ⋙
        (bigEtaleToSmallEtaleMorphism B S.obj S.property).pushforward

AlgebraicGeometry.smallEtaleToBigEtaleMorphism_comp_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleBaseChange.lean, line 373. The attribute's comment: “big_site_factorization”.

Stacks 021I, big-site factorization. The inverse-image functor of i_f is naturally isomorphic to the inverse image of f_big ∘ i_T.

public noncomputable def smallEtaleToBigEtaleMorphism_comp_inverseImageIso :
    (smallEtaleToBigEtaleMorphism B T S f).inverseImage ≅
      (bigEtaleMorphism B T S f).inverseImage ⋙
        (smallEtaleToBigEtaleMorphism B T T (𝟙 T)).inverseImage

AlgebraicGeometry.smallEtaleToBigEtaleMorphism_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleBaseChange.lean, line 401. The attribute's comment: “big_site_factorization”.

Stacks 021I, big-site factorization. The direct-image comparison for i_f = f_big ∘ i_T, naturally in the small étale sheaf.

public noncomputable def smallEtaleToBigEtaleMorphism_comp_pushforwardIso :
    (smallEtaleToBigEtaleMorphism B T S f).pushforward ≅
      (smallEtaleToBigEtaleMorphism B T T (𝟙 T)).pushforward ⋙
        (bigEtaleMorphism B T S f).pushforward

AlgebraicGeometry.smallEtalePushforwardIsoBigFactorization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleBaseChange.lean, line 415. The attribute's comment: “small_site_factorization”.

Stacks 021I, small-site factorization. The small étale direct image is canonically the composite of inclusion into the big étale topos over T, big-site direct image along f, and projection to the small étale topos of S.

public noncomputable def smallEtalePushforwardIsoBigFactorization :
    (smallEtaleBaseChange B f).sheafPushforwardContinuous
        (Type (u + 1)) (SmallEtale.topology B S.obj S.property)
          (SmallEtale.topology B T.obj T.property) ≅
      (smallEtaleToBigEtaleMorphism B T T (𝟙 T)).pushforward ⋙
        (bigEtaleMorphism B T S f).pushforward ⋙
          (bigEtaleToSmallEtaleMorphism B S.obj S.property).pushforward

AlgebraicGeometry.smallEtalePushforwardIsoDirectFactorization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/SmallEtaleBaseChange.lean, line 439. The attribute's comment: “small_site_factorization”.

Stacks 021I, small-site factorization. The small étale direct image is canonically the composite of the direct morphism i_f to the big étale topos over S and its projection.

public noncomputable def smallEtalePushforwardIsoDirectFactorization :
    (smallEtaleBaseChange B f).sheafPushforwardContinuous
        (Type (u + 1)) (SmallEtale.topology B S.obj S.property)
          (SmallEtale.topology B T.obj T.property) ≅
      (smallEtaleToBigEtaleMorphism B T S f).pushforward ⋙
        (bigEtaleToSmallEtaleMorphism B S.obj S.property).pushforward

Declarations registered for the tag:

Tag 021J, a lemma

Tag 021J in the Stacks Project.

AlgebraicGeometry.smallEtaleBaseChange_idIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtalePullbackFunctoriality.lean, line 126. The attribute's comment: “small étale site functor at the identity”.

Stacks 021J. Small étale base change along an identity morphism is the identity functor, since pullback along an identity is.

public def smallEtaleBaseChange_idIso (X : B.Scheme) :
    smallEtaleBaseChange B (𝟙 X) ≅ 𝟭 (SmallEtale B X.obj X.property)

AlgebraicGeometry.smallEtaleSheafPullbackIdIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtalePullbackFunctoriality.lean, line 137. The attribute's comment: “small étale inverse image at the identity”.

Stacks 021J. Inverse image along the identity morphism of a scheme is the identity on sheaves on its small étale site, for any coefficient category.

public def smallEtaleSheafPullbackIdIso (X : B.Scheme) (A : Type u₁) [Category.{v₁} A]
    [((smallEtaleBaseChange B (𝟙 X)).sheafPushforwardContinuous A
      (SmallEtale.topology B X.obj X.property)
      (SmallEtale.topology B X.obj X.property)).IsRightAdjoint] :
    (smallEtaleBaseChange B (𝟙 X)).sheafPullback A
        (SmallEtale.topology B X.obj X.property)
        (SmallEtale.topology B X.obj X.property) ≅
      𝟭 (Sheaf (SmallEtale.topology B X.obj X.property) A)

AlgebraicGeometry.smallEtaleSheafPullbackCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtalePullbackFunctoriality.lean, line 150. The attribute's comment: “small étale inverse images, general coefficients”.

Stacks 021J. Inverse image along a composite of morphisms of a big étale site is the composite of the inverse images, for any coefficient category.

public def smallEtaleSheafPullbackCompIso (X Y Z : B.Scheme) (f : X ⟶ Y) (g : Y ⟶ Z)
    (A : Type u₁) [Category.{v₁} A]
    [((smallEtaleBaseChange B g).sheafPushforwardContinuous A
      (SmallEtale.topology B Z.obj Z.property)
      (SmallEtale.topology B Y.obj Y.property)).IsRightAdjoint]
    [((smallEtaleBaseChange B f).sheafPushforwardContinuous A
      (SmallEtale.topology B Y.obj Y.property)
      (SmallEtale.topology B X.obj X.property)).IsRightAdjoint]
    [((smallEtaleBaseChange B (f ≫ g)).sheafPushforwardContinuous A
      (SmallEtale.topology B Z.obj Z.property)
      (SmallEtale.topology B X.obj X.property)).IsRightAdjoint] :
    (smallEtaleBaseChange B g).sheafPullback A
        (SmallEtale.topology B Z.obj Z.property)
        (SmallEtale.topology B Y.obj Y.property) ⋙
      (smallEtaleBaseChange B f).sheafPullback A
        (SmallEtale.topology B Y.obj Y.property)
        (SmallEtale.topology B X.obj X.property) ≅
    (smallEtaleBaseChange B (f ≫ g)).sheafPullback A
      (SmallEtale.topology B Z.obj Z.property)
      (SmallEtale.topology B X.obj X.property)

AlgebraicGeometry.smallEtaleBaseChange_compIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/MorphismComposition.lean, line 99. The attribute's comment: “small étale site functor composition”.

Stacks 021J. The canonical comparison of successive small étale base changes with base change along the composite, characterized by its image under the inclusion of the small étale category.

public noncomputable def smallEtaleBaseChange_compIso :
    { e : smallEtaleBaseChange B g ⋙ smallEtaleBaseChange B f ≅
        smallEtaleBaseChange B (f ≫ g) //
      ∀ U : SmallEtale B Z.obj Z.property,
        (SmallEtale.inclusion B X.obj X.property).map (e.hom.app U) =
          (Over.pullbackComp f g).inv.app U.obj }

AlgebraicGeometry.smallEtaleBaseChange_compIso_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/MorphismComposition.lean, line 124. The attribute's comment: “canonicity of small étale site composition”.

Stacks 021J. The small-site comparison is the canonical comparison of pullbacks in the ambient slice category, after forgetting the étale condition.

public theorem smallEtaleBaseChange_compIso_app
    (U : SmallEtale B Z.obj Z.property) :
    (SmallEtale.inclusion B X.obj X.property).map
      ((smallEtaleBaseChange_compIso B X Y Z f g).val.hom.app U) =
    (Over.pullbackComp f g).inv.app U.obj

AlgebraicGeometry.bigEtaleMorphism_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/MorphismComposition.lean, line 161. The attribute's comment: “big étale direct images”.

Stacks 021J. The canonical big-site direct-image comparison, obtained from the base-change formula and the composition comparison of pullbacks.

public noncomputable def bigEtaleMorphism_comp_pushforwardIso :
    (bigEtaleMorphism B X Y f).pushforward ⋙
        (bigEtaleMorphism B Y Z g).pushforward ≅
      (bigEtaleMorphism B X Z (f ≫ g)).pushforward

AlgebraicGeometry.bigEtaleMorphism_comp_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/MorphismComposition.lean, line 182. The attribute's comment: “big étale inverse images”.

Stacks 021J. The inverse-image comparison is the mate of the big direct-image comparison under the three geometric adjunctions.

public noncomputable def bigEtaleMorphism_comp_inverseImageIso :
    (bigEtaleMorphism B Y Z g).inverseImage ⋙
        (bigEtaleMorphism B X Y f).inverseImage ≅
      (bigEtaleMorphism B X Z (f ≫ g)).inverseImage

AlgebraicGeometry.smallEtaleMorphism_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/MorphismComposition.lean, line 195. The attribute's comment: “small étale direct images”.

Stacks 021J. The direct-image comparison induced by the canonical composition comparison of small-site base-change functors.

public noncomputable def smallEtaleMorphism_comp_pushforwardIso :
    (smallEtaleBaseChange B f).sheafPushforwardContinuous
        (Type (u + 1)) (SmallEtale.topology B Y.obj Y.property)
          (SmallEtale.topology B X.obj X.property) ⋙
      (smallEtaleBaseChange B g).sheafPushforwardContinuous
        (Type (u + 1)) (SmallEtale.topology B Z.obj Z.property)
          (SmallEtale.topology B Y.obj Y.property) ≅
    (smallEtaleBaseChange B (f ≫ g)).sheafPushforwardContinuous
      (Type (u + 1)) (SmallEtale.topology B Z.obj Z.property)
        (SmallEtale.topology B X.obj X.property)

AlgebraicGeometry.smallEtaleMorphism_comp_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/MorphismComposition.lean, line 214. The attribute's comment: “small étale inverse images”.

Stacks 021J. The inverse-image comparison is the mate of the small direct-image comparison under the three sheaf adjunctions.

public noncomputable def smallEtaleMorphism_comp_inverseImageIso :
    (smallEtaleBaseChange B g).sheafPullback
        (Type (u + 1)) (SmallEtale.topology B Z.obj Z.property)
          (SmallEtale.topology B Y.obj Y.property) ⋙
      (smallEtaleBaseChange B f).sheafPullback
        (Type (u + 1)) (SmallEtale.topology B Y.obj Y.property)
          (SmallEtale.topology B X.obj X.property) ≅
    (smallEtaleBaseChange B (f ≫ g)).sheafPullback
      (Type (u + 1)) (SmallEtale.topology B Z.obj Z.property)
        (SmallEtale.topology B X.obj X.property)
Tag 0DDA, a lemma

Tag 0DDA in the Stacks Project.

AlgebraicGeometry.smallEtalePushforwardBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BaseChangeCommutation.lean, line 142. The attribute's comment: “small-site base change”.

On a cartesian square, restriction to the small étale site commutes canonically with big-site direct image.

public noncomputable def smallEtalePushforwardBaseChangeIso
    (B : AlgebraicGeometry.BigEtaleSite.{u}) {T' T S' S : B.Scheme}
    (g' : T' ⟶ T) (f' : T' ⟶ S') (f : T ⟶ S) (g : S' ⟶ S)
    (h : IsPullback g' f' f g) :
    (bigEtaleMorphism B T S f).pushforward ⋙
      (smallEtaleToBigEtaleMorphism B S' S g).inverseImage ≅
    (smallEtaleToBigEtaleMorphism B T' T g').inverseImage ⋙
      (smallEtaleBaseChange B f').sheafPushforwardContinuous
        (Type (u + 1)) (SmallEtale.topology B S'.obj S'.property)
          (SmallEtale.topology B T'.obj T'.property)

AlgebraicGeometry.bigEtalePushforwardBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/BaseChangeCommutation.lean, line 222. The attribute's comment: “big-site base change”.

On a cartesian square, big étale direct image commutes canonically with big étale inverse image.

public noncomputable def bigEtalePushforwardBaseChangeIso
    (B : AlgebraicGeometry.BigEtaleSite.{u}) {T' T S' S : B.Scheme}
    (g' : T' ⟶ T) (f' : T' ⟶ S') (f : T ⟶ S) (g : S' ⟶ S)
    (h : IsPullback g' f' f g) :
    (bigEtaleMorphism B T S f).pushforward ⋙
      (bigEtaleMorphism B S' S g).inverseImage ≅
    (bigEtaleMorphism B T' T g').inverseImage ⋙
      (bigEtaleMorphism B T' S' f').pushforward
Tag 021K, a lemma

Tag 021K in the Stacks Project.

AlgebraicGeometry.BigEtaleSheafData, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigEtale/CompatibleSystem.lean, line 58. The attribute's comment: “the compatible data”.

A compatible system of sheaves on the small étale sites of the schemes over S: a sheaf on the small étale site of every T / S, a comparison map from the inverse image of the sheaf at T to the sheaf at T' along every morphism T' ⟶ T over S, subject to the cocycle condition for a composite and to being an isomorphism whenever the morphism is étale.

public structure BigEtaleSheafData

AlgebraicGeometry.characterizeSheafBigEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigEtale/SmallEtaleComparison.lean, line 1206. The attribute's comment: “equivalence with big étale sheaves”.

Stacks Project, Tag 021K. A sheaf on the big étale site over S is precisely a compatible family of sheaves on the small étale sites of all the schemes over S: the restriction functor is an equivalence of categories.

public def characterizeSheafBigEtale :
    Sheaf (BigEtaleOver.topology B S hS) (Type (max (u + 1) v)) ≌
      BigEtaleSheafData.{u, v} B S hS

AlgebraicGeometry.characterizeSheafBigEtale_functor_comp_eval, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigEtale/SmallEtaleComparison.lean, line 1221. The attribute's comment: “equivalence with big étale sheaves”.

Stacks Project, Tag 021K. Evaluating the equivalence at a scheme T over S is restriction to the small étale site of T.

public theorem characterizeSheafBigEtale_functor_comp_eval (T : BigEtaleOver B S hS) :
    (characterizeSheafBigEtale.{u, v} B S hS).functor ⋙ BigEtaleSheafData.eval B S hS T =
      bigEtaleSheafRestrictionAt B S hS T

AlgebraicGeometry.characterizeSheafBigEtale_pullback_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigEtale/SmallEtaleComparison.lean, line 1230. The attribute's comment: “equivalence with big étale sheaves”.

Stacks Project, Tag 021K. Under the equivalence the adjoint of each comparison map is restriction along the projection U ×[T] T' ⟶ U, for every small étale object U of T; so the equivalence determines the comparison maps as well as the sheaves.

public theorem characterizeSheafBigEtale_pullback_app
    (F : Sheaf (BigEtaleOver.topology B S hS) (Type (max (u + 1) v)))
    {T T' : BigEtaleOver B S hS} (f : T' ⟶ T)
    (U : SmallEtale B T.left.1 T.left.property) :
    ((B.smallPullbackAdjunction f.left (Type (max (u + 1) v))).homEquiv _ _
        (((characterizeSheafBigEtale.{u, v} B S hS).functor.obj F).pullback f)).hom.app
          (op U) =
      F.obj.map (bigEtaleBaseChangeProjection B S hS f U).op
Sources
LeanAlgebraicGeometry.Scheme.etalePrecoverage · AlgebraicGeometry.Scheme.zariskiPrecoverage_le_etalePrecoverage · AlgebraicGeometry.Scheme.etalePretopology · AlgebraicGeometry.exists_finite_affine_etaleCovering_le_of_mem_etaleTopology · exists_finite_affine_etale_refinement · AlgebraicGeometry.IsStandardEtaleCovering · AlgebraicGeometry.BigEtaleSite · AlgebraicGeometry.Scheme.etaleTopology

Section34.5 The smooth topology#

Section 34.5 of the Stacks Project, Tag 021Y. 10 tags here are carried by 29 declarations of the repository (all in StacksFrontier) and 6 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 021Z, a definition

Tag 021Z in the Stacks Project.

AlgebraicGeometry.Scheme.smoothPrecoverage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SmoothAndStandardEtaleCoverings.lean, line 74.

The smooth precoverage on the category of schemes: its covering families are the jointly surjective families of smooth morphisms.

public def smoothPrecoverage : Precoverage Scheme.{u}
Tag 0220, a lemma

Tag 0220 in the Stacks Project.

AlgebraicGeometry.Scheme.zariskiPrecoverage_le_smoothPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SmoothCoverings.lean, line 55. The attribute's comment: “Zariski coverings”.

Every Zariski covering is a smooth covering.

public theorem zariskiPrecoverage_le_smoothPrecoverage :
    zariskiPrecoverage.{u} ≤ smoothPrecoverage

Declarations registered for the tag:

Tag 0221, a lemma

Tag 0221 in the Stacks Project.

AlgebraicGeometry.Scheme.singleton_mem_smoothPrecoverage_of_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SmoothCoverings.lean, line 61. The attribute's comment: “part (1)”.

The singleton family of an isomorphism T' ⟶ T is a smooth covering of T.

public theorem singleton_mem_smoothPrecoverage_of_isIso {T' T : Scheme.{u}} (f : T' ⟶ T)
    [IsIso f] : Presieve.singleton f ∈ smoothPrecoverage T

AlgebraicGeometry.Scheme.ofArrows_comp_mem_smoothPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SmoothCoverings.lean, line 72. The attribute's comment: “part (2)”.

If {fᵢ : Tᵢ ⟶ T} is a smooth covering and {gᵢⱼ : Tᵢⱼ ⟶ Tᵢ} is a smooth covering of each Tᵢ, then the composite family {gᵢⱼ ≫ fᵢ : Tᵢⱼ ⟶ T} is a smooth covering.

public theorem ofArrows_comp_mem_smoothPrecoverage {I : Type w} {T : Scheme.{u}}
    {T' : I → Scheme.{u}} (f : ∀ i, T' i ⟶ T)
    (hf : Presieve.ofArrows T' f ∈ smoothPrecoverage T) {J : I → Type w'}
    {T'' : ∀ i, J i → Scheme.{u}} (g : ∀ i j, T'' i j ⟶ T' i)
    (hg : ∀ i, Presieve.ofArrows (T'' i) (g i) ∈ smoothPrecoverage (T' i)) :
    Presieve.ofArrows (fun p : Σ i, J i ↦ T'' p.1 p.2) (fun p ↦ g p.1 p.2 ≫ f p.1) ∈
      smoothPrecoverage T

AlgebraicGeometry.Scheme.ofArrows_pullback_mem_smoothPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SmoothCoverings.lean, line 84. The attribute's comment: “part (3)”.

If {fᵢ : Tᵢ ⟶ T} is a smooth covering and g : T' ⟶ T is a morphism of schemes, then the family of first projections {T' ×_T Tᵢ ⟶ T'} is a smooth covering.

public theorem ofArrows_pullback_mem_smoothPrecoverage {I : Type w} {T T' : Scheme.{u}}
    {Tᵢ : I → Scheme.{u}} (f : ∀ i, Tᵢ i ⟶ T)
    (hf : Presieve.ofArrows Tᵢ f ∈ smoothPrecoverage T) (g : T' ⟶ T) :
    Presieve.ofArrows (fun i ↦ pullback g (f i)) (fun i ↦ pullback.fst g (f i)) ∈
      smoothPrecoverage T'
Tag 0222, a lemma

Tag 0222 in the Stacks Project.

AlgebraicGeometry.exists_finite_affine_standardSmooth_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/StandardRefinement.lean, line 75.

A smooth covering of an affine scheme has a finite refinement by affine schemes which are standard smooth over the target; each member of the refinement is an open subscheme of a member of the original covering.

public theorem exists_finite_affine_standardSmooth_refinement {T : Scheme.{u}} [IsAffine T]
    (U : T.Cover.{v} (Scheme.precoverage (@Smooth.{u}))) :
    ∃ (V : T.AffineCover.{u} (@Smooth.{u}))
        (refinement : V.cover.toPreZeroHypercover.Hom U.toPreZeroHypercover),
      Finite V.I₀ ∧
        (∀ j, IsStandardSmooth (V.f j)) ∧
          ∀ j, IsOpenImmersion (refinement.h₀ j)
Tag 0223, a definition

Tag 0223 in the Stacks Project.

AlgebraicGeometry.IsStandardSmoothCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/StandardCovering.lean, line 39.

A finite family fᵢ : Uᵢ ⟶ T of morphisms between affine schemes is a standard smooth covering if every fᵢ is standard smooth and their images cover T.

public abbrev IsStandardSmoothCovering {T : Scheme.{u}} [IsAffine T]
    {I : Type v} [Finite I] (U : I → Scheme.{u}) [∀ i, IsAffine (U i)]
    (f : ∀ i, U i ⟶ T) : Prop
Tag 03WY, a definition

Tag 03WY in the Stacks Project.

AlgebraicGeometry.BigSmoothSite, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/BigSite.lean, line 69.

A big smooth site.

Besides the cutoff category and its selected bounded smooth coverings, this structure records the initial sets S₀ and Cov₀ and all the conditions imposed by the size-cutoff and set-sized-covering constructions.

public structure BigSmoothSite
Tag 03WZ, a lemma

Tag 03WZ in the Stacks Project.

AlgebraicGeometry.exists_covering_refining_smooth_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/BigSiteCoverings.lean, line 153. The attribute's comment: “part (1)”.

Stacks Project, Tag 03WZ, part (1). Every smooth covering family of an object of a big smooth site is refined by a covering family belonging to the site.

public theorem exists_covering_refining_smooth_cover
    (B : BigSmoothSite.{u}) {T : B.category}
    (U : PreZeroHypercover.{v} ((ObjectProperty.ι _).obj T))
    (hU : U.presieve₀ ∈ Scheme.precoverage (@Smooth.{u}) ((ObjectProperty.ι _).obj T)) :
    ∃ V : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, V⟩ ∧ Nonempty ((V.map (ObjectProperty.ι _)).Hom U)

AlgebraicGeometry.exists_covering_tautologicallyEquivalent_standardSmoothCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/BigSiteCoverings.lean, line 193. The attribute's comment: “part (2)”.

Stacks Project, Tag 03WZ, part (2). A standard smooth covering of an object of a big smooth site is tautologically equivalent to a covering family belonging to the site.

public theorem exists_covering_tautologicallyEquivalent_standardSmoothCover
    (B : BigSmoothSite.{u}) {T : B.category}
    [IsAffine ((ObjectProperty.ι _).obj T)]
    (U : PreZeroHypercover.{v} ((ObjectProperty.ι _).obj T)) [Finite U.I₀]
    [∀ i, IsAffine (U.X i)]
    (hU : IsStandardSmoothCovering (fun i ↦ U.X i) (fun i ↦ U.f i)) :
    ∃ V : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, V⟩ ∧
        PreZeroHypercover.TautologicallyEquivalent U (V.map (ObjectProperty.ι _))

AlgebraicGeometry.exists_covering_tautologicallyEquivalent_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/BigSiteCoverings.lean, line 217. The attribute's comment: “part (3)”.

Stacks Project, Tag 03WZ, part (3). A Zariski covering of an object of a big smooth site is tautologically equivalent to a covering family belonging to the site.

public theorem exists_covering_tautologicallyEquivalent_openCover
    (B : BigSmoothSite.{u}) (T : B.category)
    (U : ((ObjectProperty.ι _).obj T).OpenCover.{v}) :
    ∃ V : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, V⟩ ∧
        PreZeroHypercover.TautologicallyEquivalent U.toPreZeroHypercover
          (V.map (ObjectProperty.ι _))
Tag 03X0, a definition

Tag 03X0 in the Stacks Project.

AlgebraicGeometry.BigSmoothOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/BigSiteOver.lean, line 46. The attribute's comment: “part (1), category”.

The big smooth category over S: the slice of the chosen big smooth category over S.

public abbrev BigSmoothOver

AlgebraicGeometry.BigSmoothOver.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/BigSiteOver.lean, line 61. The attribute's comment: “part (1), coverings”.

A family in the big smooth category over S is covering precisely when its underlying family is a covering in the chosen big smooth site.

public abbrev IsCovering (E : Covering (BigSmoothOver B S hS)) : Prop

AlgebraicGeometry.BigAffineSmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/BigSiteOver.lean, line 79. The attribute's comment: “part (2), category”.

The big affine smooth category over S: the full subcategory of the big smooth category over S consisting of the objects whose underlying scheme is affine.

public abbrev BigAffineSmooth

AlgebraicGeometry.BigAffineSmooth.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/BigSiteOver.lean, line 108. The attribute's comment: “part (2), coverings”.

A family in the big affine smooth category over S is covering precisely when its image in the big smooth category over S is covering and its underlying family is a standard smooth covering.

public abbrev IsCovering (E : Covering (BigAffineSmooth B S hS)) : Prop
Tag 06VC, a lemma

Tag 06VC in the Stacks Project.

AlgebraicGeometry.BigAffineSmooth.inclusion_isSpecialCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/AffineDenseSubsite.lean, line 333.

Stacks 06VC. The inclusion of the big affine smooth site over a scheme into its big smooth site is special cocontinuous. Its dense-subsite component is precisely the datum which gives the induced equivalence of topoi.

public theorem BigAffineSmooth.inclusion_isSpecialCocontinuous
    (B : BigSmoothSite.{u}) (S : Scheme.{u}) (hS : S.size < B.cutoff) :
    IsSpecialCocontinuous
      (BigAffineSmooth.topology B S hS)
      (BigSmoothOver.topology B S hS)
      (BigAffineSmooth.inclusion B S hS)
Tag 04HC, a lemma

Tag 04HC in the Stacks Project.

AlgebraicGeometry.bigSmoothOverMap_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/MorphismOfTopoi.lean, line 108. The attribute's comment: “cocontinuity”.

The functor V / T ↦ V / S between the big smooth sites over T and over S, given by composing the structure morphism with f, is cocontinuous.

public instance bigSmoothOverMap_isCocontinuous
    (B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S) :
    (Over.map f).IsCocontinuous
      (BigSmoothOver.topology B T.obj T.property)
      (BigSmoothOver.topology B S.obj S.property)

AlgebraicGeometry.bigSmoothOverMap_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/MorphismOfTopoi.lean, line 118. The attribute's comment: “continuity”.

The functor V / T ↦ V / S between the big smooth sites over T and over S is continuous.

public instance bigSmoothOverMap_isContinuous
    (B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S) :
    (Over.map f).IsContinuous
      (BigSmoothOver.topology B T.obj T.property)
      (BigSmoothOver.topology B S.obj S.property)

AlgebraicGeometry.bigSmoothOverMapPullbackAdj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/MorphismOfTopoi.lean, line 128. The attribute's comment: “continuous_right_adjoint”.

Base change along f, the functor (U → S) ↦ (U ×_S T → T) between the big smooth sites over S and over T, is right adjoint to composition with f.

public noncomputable def bigSmoothOverMapPullbackAdj
    (B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S) :
    (Over.map f : BigSmoothOver B T.obj T.property ⥤ BigSmoothOver B S.obj S.property) ⊣
      Over.pullback f

AlgebraicGeometry.bigSmoothOverPullback_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/MorphismOfTopoi.lean, line 136. The attribute's comment: “continuous_right_adjoint”.

Base change along f is continuous for the two localized big smooth topologies.

public instance bigSmoothOverPullback_isContinuous
    (B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S) :
    (Over.pullback f).IsContinuous
      (BigSmoothOver.topology B S.obj S.property)
      (BigSmoothOver.topology B T.obj T.property)

AlgebraicGeometry.bigSmoothMorphismOfTopoi, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/MorphismOfTopoi.lean, line 146. The attribute's comment: “big_smooth_morphism_of_topoi”.

The big smooth morphism of topoi associated to a morphism f : T ⟶ S in a big smooth site, induced by the cocontinuous functor sending V ⟶ T to the composite V ⟶ T ⟶ S.

public noncomputable def bigSmoothMorphismOfTopoi
    (B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S) :
    MorphismOfTopoi
      (Sheaf (BigSmoothOver.topology B T.obj T.property) (Type (u + 1)))
      (Sheaf (BigSmoothOver.topology B S.obj S.property) (Type (u + 1)))

AlgebraicGeometry.bigSmoothMorphismOfTopoiPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/MorphismOfTopoi.lean, line 169. The attribute's comment: “agreement”.

The direct image of the big smooth morphism of topoi attached to postcomposition along f is isomorphic to the direct image along the continuous base-change functor Over.pullback f.

public noncomputable def bigSmoothMorphismOfTopoiPushforwardIso
    (B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S) :
    (bigSmoothMorphismOfTopoi B f).pushforward ≅
      (Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
        (BigSmoothOver.topology B S.obj S.property)
        (BigSmoothOver.topology B T.obj T.property)

AlgebraicGeometry.bigSmoothMorphismOfTopoiPullbackAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/MorphismOfTopoi.lean, line 180. The attribute's comment: “agreement”.

The inverse image of the big smooth morphism of topoi is left adjoint to restriction along base change.

public noncomputable def bigSmoothMorphismOfTopoiPullbackAdjunction
    (B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S) :
    (bigSmoothMorphismOfTopoi B f).inverseImage ⊣
      (Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
        (BigSmoothOver.topology B S.obj S.property)
        (BigSmoothOver.topology B T.obj T.property)

AlgebraicGeometry.bigSmoothMorphismOfTopoiInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/MorphismOfTopoi.lean, line 200. The attribute's comment: “agreement”.

The inverse image of the big smooth morphism of topoi is isomorphic to the left adjoint of restriction along base change.

public noncomputable def bigSmoothMorphismOfTopoiInverseImageIso
    (B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S) :
    (bigSmoothMorphismOfTopoi B f).inverseImage ≅
      ((Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
        (BigSmoothOver.topology B S.obj S.property)
        (BigSmoothOver.topology B T.obj T.property)).leftAdjoint

AlgebraicGeometry.bigSmoothInverseImageObjIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/MorphismOfTopoi.lean, line 212. The attribute's comment: “inverse_image”.

The sections of an inverse image on U / T are the sections of the sheaf on U / S: f⁻¹(G)(U / T) = G(U / S).

public noncomputable def bigSmoothInverseImageObjIso
    (B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S)
    (G : Sheaf (BigSmoothOver.topology B S.obj S.property) (Type (u + 1))) (U : Over T) :
    ((bigSmoothMorphismOfTopoi B f).inverseImage.obj G).obj.obj (Opposite.op U) ≅
      G.obj.obj (Opposite.op (Over.mk (U.hom ≫ f)))

AlgebraicGeometry.bigSmoothPushforwardObjIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/MorphismOfTopoi.lean, line 224. The attribute's comment: “direct_image”.

The sections of a direct image on U / S are the sections of the sheaf on the base change U ×_S T / T: f_*(F)(U / S) = F(U ×_S T / T).

public noncomputable def bigSmoothPushforwardObjIso
    (B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S)
    (F : Sheaf (BigSmoothOver.topology B T.obj T.property) (Type (u + 1))) (U : Over S) :
    ((bigSmoothMorphismOfTopoi B f).pushforward.obj F).obj.obj (Opposite.op U) ≅
      F.obj.obj (Opposite.op (Over.mk (pullback.snd U.hom f)))

AlgebraicGeometry.bigSmoothInverseImage_isRightAdjoint, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/MorphismOfTopoi.lean, line 236. The attribute's comment: “left_adjoint”.

The inverse image of a big smooth morphism of topoi has a left adjoint.

public noncomputable instance bigSmoothInverseImage_isRightAdjoint
    (B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S) :
    (bigSmoothMorphismOfTopoi B f).inverseImage.IsRightAdjoint

AlgebraicGeometry.bigSmoothLowerShriek_preservesPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/MorphismOfTopoi.lean, line 268. The attribute's comment: “shriek_limits”.

The lower shriek of a big smooth morphism of topoi preserves fibre products.

public noncomputable instance bigSmoothLowerShriek_preservesPullbacks
    (B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S) :
    PreservesLimitsOfShape WalkingCospan
      (bigSmoothMorphismOfTopoi B f).inverseImage.leftAdjoint

AlgebraicGeometry.bigSmoothLowerShriek_preservesEqualizers, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Smooth/MorphismOfTopoi.lean, line 276. The attribute's comment: “shriek_limits”.

The lower shriek of a big smooth morphism of topoi preserves equalizers.

public noncomputable instance bigSmoothLowerShriek_preservesEqualizers
    (B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S) :
    PreservesLimitsOfShape WalkingParallelPair
      (bigSmoothMorphismOfTopoi B f).inverseImage.leftAdjoint

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.Scheme.smoothPrecoverage · AlgebraicGeometry.Scheme.zariskiPrecoverage_le_smoothPrecoverage · AlgebraicGeometry.Scheme.etalePrecoverage_le_smoothPrecoverage · AlgebraicGeometry.Scheme.singleton_mem_smoothPrecoverage_of_isIso · AlgebraicGeometry.Scheme.ofArrows_comp_mem_smoothPrecoverage · AlgebraicGeometry.Scheme.ofArrows_pullback_mem_smoothPrecoverage · AlgebraicGeometry.exists_finite_affine_standardSmooth_refinement · AlgebraicGeometry.IsStandardSmoothCovering

Section34.6 The syntomic topology#

Section 34.6 of the Stacks Project, Tag 0224. 10 tags here are carried by 23 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0225, a definition

Tag 0225 in the Stacks Project.

AlgebraicGeometry.IsSyntomicCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/Coverings.lean, line 51.

A family fᵢ : Tᵢ ⟶ T is a syntomic covering if every fᵢ is syntomic and their images cover T.

public abbrev IsSyntomicCovering {T : AlgebraicGeometry.Scheme.{u}}
    {I : Type v} (X : I → AlgebraicGeometry.Scheme.{u}) (f : ∀ i, X i ⟶ T) : Prop
Tag 0226, a lemma

Tag 0226 in the Stacks Project.

AlgebraicGeometry.isSyntomicCovering_of_mem_smoothPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SyntomicTopology/Coverings.lean, line 46. The attribute's comment: “smooth coverings”.

Stacks Project, Tag 0226. Every smooth covering is a syntomic covering.

public theorem isSyntomicCovering_of_mem_smoothPrecoverage
    {T : Scheme.{u}} {I : Type v} {X : I → Scheme.{u}} {f : ∀ i, X i ⟶ T}
    (hf : Presieve.ofArrows X f ∈ Scheme.precoverage (@Smooth.{u}) T) :
    IsSyntomicCovering X f

AlgebraicGeometry.isSyntomicCovering_of_mem_etalePrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SyntomicTopology/Coverings.lean, line 56. The attribute's comment: “étale coverings”.

Stacks Project, Tag 0226. Every étale covering is a syntomic covering.

public theorem isSyntomicCovering_of_mem_etalePrecoverage
    {T : Scheme.{u}} {I : Type v} {X : I → Scheme.{u}} {f : ∀ i, X i ⟶ T}
    (hf : Presieve.ofArrows X f ∈ Scheme.etalePrecoverage T) :
    IsSyntomicCovering X f

AlgebraicGeometry.isSyntomicCovering_of_mem_zariskiPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SyntomicTopology/Coverings.lean, line 66. The attribute's comment: “Zariski coverings”.

Stacks Project, Tag 0226. Every Zariski covering is a syntomic covering.

public theorem isSyntomicCovering_of_mem_zariskiPrecoverage
    {T : Scheme.{u}} {I : Type v} {X : I → Scheme.{u}} {f : ∀ i, X i ⟶ T}
    (hf : Presieve.ofArrows X f ∈ Scheme.zariskiPrecoverage T) :
    IsSyntomicCovering X f
Tag 0227, a lemma

Tag 0227 in the Stacks Project.

AlgebraicGeometry.isSyntomicCovering_singleton_of_isIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/Stability.lean, line 54. The attribute's comment: “part (1)”.

Stacks Project, Tag 0227, part (1). An isomorphism, regarded as a singleton family, is a syntomic covering.

public lemma isSyntomicCovering_singleton_of_isIso {T' T : Scheme.{u}}
    (f : T' ⟶ T) [IsIso f] :
    IsSyntomicCovering (fun _ : Unit ↦ T') (fun _ ↦ f)

AlgebraicGeometry.IsSyntomicCovering.comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/Stability.lean, line 65. The attribute's comment: “part (2)”.

Stacks Project, Tag 0227, part (2). Refining every member of a syntomic covering by a syntomic covering gives another syntomic covering.

public lemma IsSyntomicCovering.comp {T : Scheme.{u}} {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hf : IsSyntomicCovering X f) {J : I → Type w}
    (Y : ∀ i, J i → Scheme.{u}) (g : ∀ i j, Y i j ⟶ X i)
    (hg : ∀ i, IsSyntomicCovering (Y i) (g i)) :
    IsSyntomicCovering
      (fun ij : Σ i, J i ↦ Y ij.1 ij.2)
      (fun ij ↦ g ij.1 ij.2 ≫ f ij.1)

AlgebraicGeometry.isSyntomicCovering_pullback, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/Stability.lean, line 82. The attribute's comment: “part (3)”.

Stacks Project, Tag 0227, part (3). Pulling a syntomic covering back along an arbitrary morphism gives a syntomic covering.

public lemma isSyntomicCovering_pullback {T : Scheme.{u}} {I : Type v}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T) {T' : Scheme.{u}}
    (g : T' ⟶ T) (hf : IsSyntomicCovering X f) :
    IsSyntomicCovering
      (fun i ↦ pullback (f i) g)
      (fun i ↦ pullback.snd (f i) g)
Tag 0228, a lemma

Tag 0228 in the Stacks Project.

AlgebraicGeometry.exists_finite_affine_standardSyntomic_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/StandardRefinement.lean, line 163.

Stacks Project, Tag 0228. A syntomic covering of an affine scheme has a finite refinement by affine schemes which are standard syntomic over the target; each member of the refinement is an open subscheme of a member of the original covering.

public theorem exists_finite_affine_standardSyntomic_refinement
    {T : Scheme.{u}} [IsAffine T] (U : PreZeroHypercover.{v} T)
    (hU : IsSyntomicCovering U.X U.f) :
    ∃ (V : T.AffineCover.{u} (@Syntomic.{u}))
        (refinement : V.cover.toPreZeroHypercover.Hom U),
      Finite V.I₀ ∧
        (∀ j, IsStandardSyntomic (V.f j)) ∧
          ∀ j, IsOpenImmersion (refinement.h₀ j)
Tag 0229, a definition

Tag 0229 in the Stacks Project.

AlgebraicGeometry.IsStandardSyntomicCovering, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/Coverings.lean, line 58.

A family fᵢ : Uᵢ ⟶ T is a standard syntomic covering if its indexing type is finite, its source and target schemes are affine, every fᵢ is standard syntomic, and their images cover T.

public structure IsStandardSyntomicCovering {T : Scheme.{u}} {I : Type v}
    (U : I → Scheme.{u}) (f : ∀ i, U i ⟶ T) : Prop
Tag 03X1, a definition

Tag 03X1 in the Stacks Project.

AlgebraicGeometry.BigSyntomicSite, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/BigSite.lean, line 69.

Stacks 03X1. A big syntomic site consists of an initial set of schemes and syntomic coverings, a size cutoff containing those schemes, and a bounded collection of syntomic coverings containing the initial ones and satisfying the site axioms.

public structure BigSyntomicSite
Tag 03X2, a lemma

Tag 03X2 in the Stacks Project.

AlgebraicGeometry.BigSyntomicSite.exists_isCovering_tautologicallyEquivalent_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/ConstantSheaf.lean, line 61. The attribute's comment: “part (3)”.

A Zariski covering of an object of a big syntomic site is tautologically equivalent to one of the site's own covering families.

public theorem BigSyntomicSite.exists_isCovering_tautologicallyEquivalent_openCover
    (B : BigSyntomicSite.{u}) (T : B.category) (𝒰 : Scheme.OpenCover.{w} T.1) :
    ∃ V : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, V⟩ ∧
        PreZeroHypercover.TautologicallyEquivalent 𝒰.toPreZeroHypercover
          (V.map B.inclusion)

AlgebraicGeometry.exists_siteCovering_refining, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SyntomicTopology/SiteRefinement.lean, line 78. The attribute's comment: “site_refinement”.

Every syntomic covering of an object of a big syntomic site admits a refinement by a covering in the site.

public theorem exists_siteCovering_refining
    (B : BigSyntomicSite.{u}) (T : B.category)
    (E : PreZeroHypercover.{v} (B.inclusion.obj T))
    (hE : IsSyntomicCovering E.X E.f) :
    ∃ 𝒰 : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, 𝒰⟩ ∧
        Nonempty ((𝒰.map B.inclusion).Hom E)

AlgebraicGeometry.BigSyntomicSite.exists_isCovering_tautologicallyEquivalent_standardCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SyntomicTopology/SiteRefinement.lean, line 132. The attribute's comment: “part (2)”.

A standard syntomic covering of an object of a big syntomic site is tautologically equivalent to a covering belonging to the site.

public theorem BigSyntomicSite.exists_isCovering_tautologicallyEquivalent_standardCovering
    (B : BigSyntomicSite.{u}) (T : B.category)
    (U : PreZeroHypercover.{v} (B.inclusion.obj T))
    (hU : IsStandardSyntomicCovering U.X U.f) :
    ∃ V : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, V⟩ ∧
        PreZeroHypercover.TautologicallyEquivalent U (V.map B.inclusion)
Tag 03X3, a definition

Tag 03X3 in the Stacks Project.

AlgebraicGeometry.BigSyntomicOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/BigSiteOver.lean, line 48. The attribute's comment: “part (1), category”.

The big syntomic category over S is the slice of the chosen big syntomic category at S.

public abbrev BigSyntomicOver

AlgebraicGeometry.BigSyntomicOver.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/BigSiteOver.lean, line 62. The attribute's comment: “part (1), coverings”.

A family in the slice is covering precisely when its underlying family is covering in the chosen big syntomic site.

public abbrev IsCovering (E : Covering (BigSyntomicOver B S hS)) : Prop

AlgebraicGeometry.BigAffineSyntomic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/BigSiteOver.lean, line 78. The attribute's comment: “part (2), category”.

The big affine syntomic category over S is the full subcategory of the big syntomic category over S on affine source schemes.

public abbrev BigAffineSyntomic

AlgebraicGeometry.BigAffineSyntomic.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/BigSiteOver.lean, line 103. The attribute's comment: “part (2), coverings”.

A family in the big affine syntomic site is covering exactly when it is covering in the localized big syntomic site and is a standard syntomic covering of schemes.

public abbrev IsCovering (E : Covering (BigAffineSyntomic B S hS)) : Prop
Tag 06VD, a lemma

Tag 06VD in the Stacks Project.

AlgebraicGeometry.BigAffineSyntomic.inclusion_isSpecialCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/AffineSyntomicDenseSubsite.lean, line 352.

Stacks 06VD. The inclusion of affine objects over S into the big syntomic site over S is special cocontinuous. Its dense-subsite component gives the induced equivalence of topoi.

public theorem BigAffineSyntomic.inclusion_isSpecialCocontinuous
    (B : BigSyntomicSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    IsSpecialCocontinuous
      (BigAffineSyntomic.topology B S hS)
      (BigSyntomicOver.topology B S hS)
      (BigAffineSyntomic.inclusion B S hS)
Tag 04HD, a lemma

Tag 04HD in the Stacks Project.

AlgebraicGeometry.bigSyntomicMorphismOfTopoi, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/MorphismOfTopoi.lean, line 111. The attribute's comment: “big_syntomic_morphism”.

Stacks Project, Tag 04HD. The big syntomic morphism of topoi attached to f : T ⟶ S in a chosen big syntomic site. Its defining functor sends V ⟶ T to the composite V ⟶ T ⟶ S.

public noncomputable def bigSyntomicMorphismOfTopoi : MorphismOfTopoi
    (Sheaf (BigSyntomicOver.topology B T.obj T.property) (Type (u + 1)))
    (Sheaf (BigSyntomicOver.topology B S.obj S.property) (Type (u + 1)))

AlgebraicGeometry.bigSyntomicMorphismPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/MorphismOfTopoi.lean, line 133. The attribute's comment: “same_morphism”.

Stacks Project, Tag 04HD. The big syntomic morphism of topoi defined by postcomposition along f is the morphism of topoi induced by the continuous base-change functor Over.pullback f: their direct images are canonically isomorphic.

public noncomputable def bigSyntomicMorphismPushforwardIso :
    (bigSyntomicMorphismOfTopoi B f).pushforward ≅
      (Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
        (BigSyntomicOver.topology B S.obj S.property)
        (BigSyntomicOver.topology B T.obj T.property)

AlgebraicGeometry.bigSyntomicLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/MorphismOfTopoi.lean, line 143. The attribute's comment: “lower_shriek”.

Stacks Project, Tag 04HD. The lower shriek on big syntomic sheaves is left adjoint to inverse image.

public noncomputable def bigSyntomicLowerShriekAdjunction :
    (Over.map f).sheafPullback (Type (u + 1))
      (BigSyntomicOver.topology B T.obj T.property)
      (BigSyntomicOver.topology B S.obj S.property) ⊣
        (bigSyntomicMorphismOfTopoi B f).inverseImage

AlgebraicGeometry.bigSyntomicLowerShriek_preservesPullbacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/MorphismOfTopoi.lean, line 160. The attribute's comment: “lower_shriek”.

Stacks Project, Tag 04HD. The lower shriek preserves fibre products.

public theorem bigSyntomicLowerShriek_preservesPullbacks :
    PreservesLimitsOfShape WalkingCospan
      ((Over.map f).sheafPullback (Type (u + 1))
        (BigSyntomicOver.topology B T.obj T.property)
        (BigSyntomicOver.topology B S.obj S.property))

AlgebraicGeometry.bigSyntomicLowerShriek_preservesEqualizers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Syntomic/MorphismOfTopoi.lean, line 171. The attribute's comment: “lower_shriek”.

Stacks Project, Tag 04HD. The lower shriek preserves equalizers.

public theorem bigSyntomicLowerShriek_preservesEqualizers :
    PreservesLimitsOfShape WalkingParallelPair
      ((Over.map f).sheafPullback (Type (u + 1))
        (BigSyntomicOver.topology B T.obj T.property)
        (BigSyntomicOver.topology B S.obj S.property))

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.IsSyntomicCovering · AlgebraicGeometry.isSyntomicCovering_of_mem_smoothPrecoverage · AlgebraicGeometry.isSyntomicCovering_of_mem_etalePrecoverage · AlgebraicGeometry.isSyntomicCovering_of_mem_zariskiPrecoverage · AlgebraicGeometry.isSyntomicCovering_singleton_of_isIso · AlgebraicGeometry.IsSyntomicCovering.comp · AlgebraicGeometry.isSyntomicCovering_pullback · AlgebraicGeometry.exists_finite_affine_standardSyntomic_refinement

Section34.7 The fppf topology#

Section 34.7 of the Stacks Project, Tag 021L. 13 tags here are carried by 30 declarations of the repository (all in StacksFrontier) and 17 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 021M, a definition

Tag 021M in the Stacks Project.

Declarations registered for the tag:

Tag 021N, a lemma

Tag 021N in the Stacks Project.

AlgebraicGeometry.coveringPrecoverage_le_of_isFiner, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/RingedChangeOfTopologies.lean, line 119. The attribute's comment: “the five precoverages of schemes are nested along the chain of topologies”. References: SGA 3 IV (6.6), “Diagram 6.6.1”.

Stacks 021N and its companions. Along the chain, the precoverages of jointly surjective families of schemes are nested: an open immersion is étale, an étale morphism is smooth, a smooth morphism is syntomic, and a syntomic morphism is flat and locally of finite presentation.

public theorem coveringPrecoverage_le_of_isFiner (h : τ.IsFiner τ') :
    Scheme.precoverage (coveringMorphismProperty τ') ≤
      Scheme.precoverage (coveringMorphismProperty τ)

AlgebraicGeometry.Scheme.smoothPrecoverage_le_fppfPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/Coverings.lean, line 45. The attribute's comment: “smooth coverings”.

Stacks 021N. Every smooth covering family is an fppf covering family.

public theorem smoothPrecoverage_le_fppfPrecoverage :
    Scheme.precoverage (@Smooth : MorphismProperty Scheme.{u}) ≤
      Scheme.fppfPrecoverage

AlgebraicGeometry.Scheme.etalePrecoverage_le_fppfPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/Coverings.lean, line 54. The attribute's comment: “étale coverings”.

Stacks 021N. Every étale covering family is an fppf covering family.

public theorem etalePrecoverage_le_fppfPrecoverage :
    Scheme.etalePrecoverage ≤ Scheme.fppfPrecoverage

AlgebraicGeometry.Scheme.syntomicPrecoverage_le_fppfPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/FinerTopologies.lean, line 78. The attribute's comment: “syntomic coverings”.

Stacks 021N. Every syntomic covering family is an fppf covering family: a syntomic morphism is flat by Stacks 01UL and locally of finite presentation by Stacks 01UK.

public theorem syntomicPrecoverage_le_fppfPrecoverage :
    Scheme.precoverage (@Syntomic : MorphismProperty Scheme.{u}) ≤ Scheme.fppfPrecoverage

Declarations registered for the tag:

Tag 021O, a lemma

Tag 021O in the Stacks Project.

Declarations registered for the tag:

Tag 021P, a lemma

Tag 021P in the Stacks Project.

AlgebraicGeometry.exists_standardFppf_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/Equivalence.lean, line 51. The attribute's comment: “the finite affine refinement; the tag's further assertion that each member may be chosen open affine inside one of the given members is not claimed”.

Every covering sieve of an affine object of a big fppf site is refined by a chosen covering family which is a standard fppf covering, that is, by a finite family of flat morphisms of finite presentation, jointly surjective, whose sources are affine over the affine target.

theorem exists_standardFppf_refinement
    (B : AlgebraicGeometry.BigFppfSite.{u})
    {T : B.Schemes} [IsAffine (B.inclusion.obj T)] {R : Sieve T}
    (hR : R ∈ B.topology T) :
    ∃ Q : PreZeroHypercover T,
      B.IsCovering ⟨T, Q⟩ ∧
      AlgebraicGeometry.IsStandardFppfCovering
        (fun i ↦ B.inclusion.obj (Q.X i)) (fun i ↦ B.inclusion.map (Q.f i)) ∧
      Q.presieve₀ ≤ R
Tag 021Q, a definition

Tag 021Q in the Stacks Project.

AlgebraicGeometry.IsStandardFppfCovering, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf.lean, line 78.

A family fᵢ : Uᵢ ⟶ T is a standard fppf covering if it is finite, its source and target schemes are affine, every fᵢ is flat and of finite presentation, and the images of the fᵢ cover T.

public structure IsStandardFppfCovering {T : Scheme.{u}} {I : Type v}
    (U : I → Scheme.{u}) (f : ∀ i, U i ⟶ T) : Prop
Tag 021R, a definition

Tag 021R in the Stacks Project.

AlgebraicGeometry.BigFppfSite, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf.lean, line 110.

A big fppf site, retaining all choices in the construction: the initial set of schemes and coverings, the size cutoff defining its underlying full subcategory, and the bounded family of fppf coverings of Stacks 000X.

structure BigFppfSite

Declarations registered for the tag:

Tag 03WX, a lemma

Tag 03WX in the Stacks Project.

AlgebraicGeometry.exists_isCovering_tautologicallyEquivalent_standardFppfCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/StandardCoverings.lean, line 148. The attribute's comment: “standard_equivalence”.

A standard fppf covering of an object of a big fppf site is tautologically equivalent to a covering belonging to that site.

public theorem exists_isCovering_tautologicallyEquivalent_standardFppfCovering
    (B : AlgebraicGeometry.BigFppfSite.{u}) (T : B.Schemes)
    (U : PreZeroHypercover.{w} (B.inclusion.obj T))
    (hU : U.presieve₀ ∈ Scheme.fppfPrecoverage (B.inclusion.obj T))
    (hstandard : AlgebraicGeometry.IsStandardFppfCovering U.X U.f) :
    ∃ V : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, V⟩ ∧
        PreZeroHypercover.TautologicallyEquivalent U (V.map B.inclusion)

AlgebraicGeometry.exists_isCovering_tautologicallyEquivalent_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/StandardCoverings.lean, line 167. The attribute's comment: “zariski_equivalence”.

A Zariski covering of an object of a big fppf site is tautologically equivalent to a covering belonging to that site.

public theorem exists_isCovering_tautologicallyEquivalent_openCover
    (B : AlgebraicGeometry.BigFppfSite.{u}) (T : B.Schemes)
    (U : (B.inclusion.obj T).OpenCover.{w}) :
    ∃ V : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, V⟩ ∧
        PreZeroHypercover.TautologicallyEquivalent U.toPreZeroHypercover
          (V.map B.inclusion)

AlgebraicGeometry.exists_isCovering_refining_fppfCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/StandardCoverings.lean, line 194. The attribute's comment: “site_refinement”.

An arbitrary fppf covering of an object of a big fppf site is refined by a covering belonging to that site.

public theorem exists_isCovering_refining_fppfCovering
    (B : AlgebraicGeometry.BigFppfSite.{u}) (T : B.Schemes)
    (E : PreZeroHypercover.{w} (B.inclusion.obj T))
    (hE : E.presieve₀ ∈ Scheme.fppfPrecoverage (B.inclusion.obj T)) :
    ∃ V : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, V⟩ ∧ Nonempty ((V.map B.inclusion).Hom E)
Tag 021S, a definition

Tag 021S in the Stacks Project.

AlgebraicGeometry.BigFppfOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf.lean, line 232. The attribute's comment: “part (1), category”. References: SGA 4 XVII (0.10), “big fppf site”.

The big fppf category over S: the slice of the chosen big fppf category over its object S.

public abbrev BigFppfOver

AlgebraicGeometry.BigFppfOver.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf.lean, line 247. The attribute's comment: “part (1), coverings”.

A family in the slice covers when its underlying family covers in the chosen big fppf site.

public abbrev IsCovering (E : Covering (BigFppfOver B S hS)) : Prop

AlgebraicGeometry.BigAffineFppf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf.lean, line 270. The attribute's comment: “part (2), category”.

The big affine fppf category over S: the full subcategory of the big fppf category over S on objects with affine underlying scheme.

public abbrev BigAffineFppf

AlgebraicGeometry.BigAffineFppf.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf.lean, line 296. The attribute's comment: “part (2), coverings”.

A family in the big affine category covers exactly when it is a covering of the big fppf site over S and is standard fppf.

public abbrev IsCovering (E : Covering (BigAffineFppf B S hS)) : Prop
Tag 021T, a lemma

Tag 021T in the Stacks Project.

AlgebraicGeometry.bigAffineFppf_isSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/BigSite.lean, line 112.

Stacks 021T. Standard fppf coverings of affine schemes over S satisfy the site axioms.

public theorem bigAffineFppf_isSite (B : AlgebraicGeometry.BigFppfSite.{u})
    (S : Scheme.{u}) (hS : B.Contains S) :
    IsSite (AlgebraicGeometry.BigAffineFppf.IsCovering B S hS)
Tag 021U, a lemma

Tag 021U in the Stacks Project.

AlgebraicGeometry.BigFppfSite.hasPullbacks_schemes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/FibreProducts.lean, line 104. The attribute's comment: “fibre products in the big fppf site”.

The underlying category of a big fppf site admits fibre products.

public theorem BigFppfSite.hasPullbacks_schemes : HasPullbacks B.Schemes

AlgebraicGeometry.hasPullbacks_bigFppfOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/FibreProducts.lean, line 111. The attribute's comment: “fibre products in the big fppf slice”.

The big fppf category over S admits fibre products.

public theorem hasPullbacks_bigFppfOver :
    HasPullbacks (AlgebraicGeometry.BigFppfOver B S hS)

AlgebraicGeometry.preservesPullbacks_bigFppfOverToScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/FibreProducts.lean, line 117. The attribute's comment: “preservation by the big fppf slice functor to schemes”.

The canonical functor from the big fppf category over S to the category of all schemes preserves fibre products.

public theorem preservesPullbacks_bigFppfOverToScheme :
    PreservesLimitsOfShape WalkingCospan
      (AlgebraicGeometry.BigFppfOver.toScheme B S hS)

AlgebraicGeometry.isTerminal_mkId_bigFppfOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/FibreProducts.lean, line 124. The attribute's comment: “the final object of the big fppf slice is S / S”.

The final object of the big fppf category over S is S / S, the identity of S viewed as an object over S.

public noncomputable def isTerminal_mkId_bigFppfOver :
    IsTerminal (C := AlgebraicGeometry.BigFppfOver B S hS) (Over.mk (𝟙 (B.obj hS)))

AlgebraicGeometry.hasPullbacks_bigAffineFppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/FibreProducts.lean, line 149. The attribute's comment: “fibre products in the big affine fppf site”.

The category of affine objects in the big fppf category over S admits fibre products.

public instance hasPullbacks_bigAffineFppf :
    HasPullbacks (AlgebraicGeometry.BigAffineFppf B S hS)

AlgebraicGeometry.preservesPullbacks_bigAffineFppfToScheme, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/FibreProducts.lean, line 162. The attribute's comment: “preservation by the big affine fppf functor to schemes”.

The canonical functor from affine objects over S to schemes preserves fibre products.

public instance preservesPullbacks_bigAffineFppfToScheme :
    PreservesLimitsOfShape WalkingCospan
      (AlgebraicGeometry.BigAffineFppf.toScheme B S hS)

Declarations registered for the tag:

Tag 021V, a lemma

Tag 021V in the Stacks Project.

AlgebraicGeometry.bigAffineFppfInclusion_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/Equivalence.lean, line 235. The attribute's comment: “cocontinuity”.

The inclusion of affine objects over S in a chosen big fppf site is cocontinuous.

public instance bigAffineFppfInclusion_isCocontinuous
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    (AlgebraicGeometry.BigAffineFppf.inclusion B S hS).IsCocontinuous
      (AlgebraicGeometry.BigAffineFppf.topology B S hS)
      (AlgebraicGeometry.BigFppfOver.topology B S hS)

AlgebraicGeometry.bigAffineFppfInclusion_isDenseSubsite, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/Equivalence.lean, line 296. The attribute's comment: “equivalence of topoi”.

The inclusion of affine objects over S in a chosen big fppf site is a dense subsite, so the induced morphism of sheaf topoi is an equivalence.

public instance bigAffineFppfInclusion_isDenseSubsite
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) :
    (AlgebraicGeometry.BigAffineFppf.inclusion B S hS).IsDenseSubsite
      (AlgebraicGeometry.BigAffineFppf.topology B S hS)
      (AlgebraicGeometry.BigFppfOver.topology B S hS)
Tag 021W, a lemma

Tag 021W in the Stacks Project.

AlgebraicGeometry.bigFppfMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/MorphismOfTopoi.lean, line 105. The attribute's comment: “the morphism of topoi”.

Stacks 021W. The morphism of big fppf topoi induced by postcomposition along f.

public noncomputable def bigFppfMorphism :
    MorphismOfTopoi
      (Sheaf (B.topology.over T) (Type (u + 1)))
      (Sheaf (B.topology.over S) (Type (u + 1)))

AlgebraicGeometry.bigFppfLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/MorphismOfTopoi.lean, line 120. The attribute's comment: “existence of lower shriek”.

Stacks 021W. The left adjoint of the inverse image is sheaf pullback along postcomposition.

public noncomputable def bigFppfLowerShriekAdjunction :
    (Over.map f).sheafPullback (Type (u + 1))
      (B.topology.over T) (B.topology.over S) ⊣
        (bigFppfMorphism B T S f).inverseImage

AlgebraicGeometry.bigFppfLowerShriek_preservesPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/MorphismOfTopoi.lean, line 133. The attribute's comment: “lower shriek preserves fibre products”.

Stacks 021W. The left adjoint of the inverse image preserves fibre products.

public instance bigFppfLowerShriek_preservesPullbacks :
    PreservesLimitsOfShape WalkingCospan
      ((Over.map f).sheafPullback (Type (u + 1))
        (B.topology.over T) (B.topology.over S))

AlgebraicGeometry.bigFppfLowerShriek_preservesEqualizers, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/MorphismOfTopoi.lean, line 144. The attribute's comment: “lower shriek preserves equalizers”.

Stacks 021W. The left adjoint of the inverse image preserves equalizers.

public instance bigFppfLowerShriek_preservesEqualizers :
    PreservesLimitsOfShape WalkingParallelPair
      ((Over.map f).sheafPullback (Type (u + 1))
        (B.topology.over T) (B.topology.over S))

Declarations registered for the tag:

Tag 021X, a lemma

Tag 021X in the Stacks Project.

AlgebraicGeometry.bigFppfMorphism_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/Composition.lean, line 94. The attribute's comment: “canonical direct-image comparison”.

Stacks 021X. Composition of the morphisms of big fppf topoi agrees, naturally on sheaves, with the morphism attached to the composite map of schemes.

public noncomputable def bigFppfMorphism_comp_pushforwardIso
    (B : AlgebraicGeometry.BigFppfSite.{u}) {X Y Z : B.Schemes}
    (f : X ⟶ Y) (g : Y ⟶ Z) :
    (bigFppfMorphism B X Z (f ≫ g)).pushforward ≅
      ((bigFppfMorphism B Y Z g).comp
        (bigFppfMorphism B X Y f)).pushforward

AlgebraicGeometry.bigFppfMorphism_comp_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/Composition.lean, line 113. The attribute's comment: “canonical inverse-image comparison”.

Stacks 021X. The inverse-image comparison is the mate of the direct-image comparison.

public noncomputable def bigFppfMorphism_comp_inverseImageIso
    (B : AlgebraicGeometry.BigFppfSite.{u}) {X Y Z : B.Schemes}
    (f : X ⟶ Y) (g : Y ⟶ Z) :
    (bigFppfMorphism B X Z (f ≫ g)).inverseImage ≅
      ((bigFppfMorphism B Y Z g).comp
        (bigFppfMorphism B X Y f)).inverseImage

AlgebraicGeometry.bigFppfMorphism_comp_adjunction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/Composition.lean, line 127. The attribute's comment: “compatibility with the adjunction”.

Stacks 021X. The two canonical comparisons respect the units of the geometric morphisms.

public theorem bigFppfMorphism_comp_adjunction
    (B : AlgebraicGeometry.BigFppfSite.{u}) {X Y Z : B.Schemes}
    (f : X ⟶ Y) (g : Y ⟶ Z)
    (V : Sheaf (B.topology.over Z) (Type (u + 1))) :
    let h := bigFppfMorphism B X Z (f ≫ g)
    let k := (bigFppfMorphism B Y Z g).comp
      (bigFppfMorphism B X Y f)
    h.adj.unit.app V ≫
        h.pushforward.map ((bigFppfMorphism_comp_inverseImageIso B f g).hom.app V) ≫
        (bigFppfMorphism_comp_pushforwardIso B f g).hom.app
          (k.inverseImage.obj V) = k.adj.unit.app V
Sources
LeanAlgebraicGeometry.Scheme.fppfPrecoverage · AlgebraicGeometry.coveringPrecoverage_le_of_isFiner · AlgebraicGeometry.Scheme.smoothPrecoverage_le_fppfPrecoverage · AlgebraicGeometry.Scheme.etalePrecoverage_le_fppfPrecoverage · AlgebraicGeometry.Scheme.syntomicPrecoverage_le_fppfPrecoverage · Scheme.zariskiPrecoverage_le_fppfPrecoverage · AlgebraicGeometry.Scheme.Hom.singleton_mem_fppfPrecoverage · AlgebraicGeometry.Scheme.instIsStableUnderCompositionFppfPrecoverage

Section34.8 The ph topology#

Section 34.8 of the Stacks Project, Tag 0DBC. 17 tags here are carried by 32 declarations of the repository (all in StacksFrontier) and 10 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DBD, a definition

Tag 0DBD in the Stacks Project.

AlgebraicGeometry.StandardPHCovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/StandardCoverings.lean, line 54.

A family fᵢ : Xᵢ ⟶ T is a standard ph covering if its index type is finite, every Xᵢ is affine, and the family is obtained from a finite affine open cover of the source of a proper surjective morphism to the affine scheme T.

def StandardPHCovering {ι : Type v} {T : Scheme.{u}} [IsAffine T] {X : ι → Scheme.{u}}
    (f : ∀ i, X i ⟶ T) : Prop
Tag 0DBE, a lemma

Tag 0DBE in the Stacks Project.

AlgebraicGeometry.StandardPHCovering.pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/StandardCoverings.lean, line 104.

Stacks 0DBE. A standard ph covering remains standard after pullback along a morphism of affine schemes.

theorem StandardPHCovering.pullback {ι : Type v} {T T' : Scheme.{u}}
    [IsAffine T] [IsAffine T'] {X : ι → Scheme.{u}} {f : ∀ i, X i ⟶ T}
    (hf : StandardPHCovering f) (g : T' ⟶ T) :
    StandardPHCovering (fun i ↦ pullback.snd (f i) g)
Tag 0DBF, a lemma

Tag 0DBF in the Stacks Project.

AlgebraicGeometry.exists_standardPHCovering_refinement_bind, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/StandardRefinementParts0DBF.lean, line 156. The attribute's comment: “part (2)”.

Stacks Project, Tag 0DBF, part (2). Let T be an affine scheme, let E be a standard ph covering of T, and for each member E.X i let F i be a standard ph covering of it. Then the composite family E.bind F, whose members are the (F i).X j ⟶ E.X i ⟶ T, has a refinement by a standard ph covering of T.

This consumes Chow's lemma (Stacks 0202) through AlgebraicGeometry.chowLemmaStatement.

theorem exists_standardPHCovering_refinement_bind {T : Scheme.{u}} [IsAffine T]
    (E : PreZeroHypercover.{v} T) (hE : StandardPHCovering E.f)
    (F : ∀ i, PreZeroHypercover.{w} (E.X i))
    (hF : ∀ i, @StandardPHCovering (F i).I₀ (E.X i) (hE.isAffine i) (F i).X (F i).f) :
    ∃ G : PreZeroHypercover.{max v w} T,
      StandardPHCovering G.f ∧ Nonempty (G.Hom (E.bind F))

AlgebraicGeometry.exists_standardPHCovering_refinement_of_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/StandardPhRefinement.lean, line 113. The attribute's comment: “part (1)”.

Stacks Project, Tag 0DBF, part (1). Every Zariski open covering of an affine scheme has a refinement which is a standard ph covering.

The standard ph covering is the finite affine refinement of AlgebraicGeometry.exists_finite_affine_refinement, presented by the identity of T, which is proper and surjective.

theorem exists_standardPHCovering_refinement_of_openCover {T : Scheme.{u}} [IsAffine T]
    (U : T.OpenCover.{v}) :
    ∃ E : PreZeroHypercover.{v} T,
      StandardPHCovering E.f ∧ Nonempty (E.Hom U.toPreZeroHypercover)
Tag 0DBG, a definition

Tag 0DBG in the Stacks Project.

AlgebraicGeometry.IsPHCovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/Coverings.lean, line 62.

Stacks 0DBG. A family {X i ⟶ T} is a ph covering if every member is locally of finite type and, over every affine open U of T, a standard ph covering of U.toScheme refines the pullback of the family to U.

public noncomputable def IsPHCovering {T : Scheme.{u}}
    {I : Type v} (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T) : Prop
Tag 0DBH, a lemma

Tag 0DBH in the Stacks Project.

AlgebraicGeometry.IsPHCovering.of_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/StandardPhRefinement.lean, line 128.

Stacks Project, Tag 0DBH. A Zariski open covering of a scheme is a ph covering.

Over an affine open V of the target, the base change of the covering is again a Zariski open covering, so AlgebraicGeometry.exists_standardPHCovering_refinement_of_openCover refines it by a standard ph covering; that covering is then reindexed into the universe of the schemes by AlgebraicGeometry.StandardPHCovering.reindex.

theorem IsPHCovering.of_openCover {T : Scheme.{u}} (𝒰 : T.OpenCover.{v}) :
    IsPHCovering 𝒰.X 𝒰.f
Tag 0DES, a lemma

Tag 0DES in the Stacks Project.

AlgebraicGeometry.surjective_proper_isPHCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/Coverings.lean, line 107.

Stacks 0DES. A proper surjection of schemes is a ph covering.

public theorem surjective_proper_isPHCovering {X Y : Scheme.{u}} (f : Y ⟶ X)
    [Surjective f] [IsProper f] :
    IsPHCovering (fun _ : Unit ↦ Y) (fun _ ↦ f)
Tag 0ET9, a lemma

Tag 0ET9 in the Stacks Project.

AlgebraicGeometry.isPHCovering_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/PhCoveringRefinement.lean, line 60.

A family of locally finite type morphisms is a ph covering if and only if some ph covering refines it, if and only if its disjoint-union morphism is a ph covering.

public theorem isPHCovering_tfae {T : Scheme.{u}} {I : Type v} [Small.{u} I]
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hf : ∀ i, LocallyOfFiniteType (f i)) :
    List.TFAE [
      IsPHCovering X f,
      ∃ (K : Type v) (Y : K → Scheme.{u}) (g : ∀ k, Y k ⟶ T),
        IsPHCovering Y g ∧
          Nonempty
            (({ I₀ := K, X := Y, f := g } : PreZeroHypercover T).Hom
              ({ I₀ := I, X := X, f := f } : PreZeroHypercover T)),
      IsPHCovering
        (fun _ : Unit ↦ ∐ X) (fun _ ↦ Sigma.desc f)]
Tag 0DBI, a lemma

Tag 0DBI in the Stacks Project.

AlgebraicGeometry.isPHCovering_of_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/Coverings.lean, line 101. The attribute's comment: “isomorphisms”.

Stacks 0DBI. A singleton isomorphism is a ph covering of schemes.

public theorem isPHCovering_of_isIso {T' T : Scheme.{u}} (f : T' ⟶ T) [IsIso f] :
    IsPHCovering (fun _ : Unit ↦ T') (fun _ ↦ f)

AlgebraicGeometry.isPHCovering_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/CoveringsParts0DBI.lean, line 178. The attribute's comment: “part (3)”.

Stacks 0DBI part (3). If {X i ⟶ T} is a ph covering and g : T' ⟶ T is any morphism of schemes, then the base change {X i ×_T T' ⟶ T'} is a ph covering of T'.

Fix an affine open U' of T'. It is a compact space, so AlgebraicGeometry.exists_finite_affineOpens_confined covers it by finitely many affine opens W l, each mapping into an affine open V l of T; the family {W l ⟶ U'} is a standard ph covering of U' presented by the identity of U'. Over V l the given covering has a standard ph refinement, and W l ⟶ V l base changes it to a standard ph covering of W l refining the base changed family, by the universal property of the fibre products involved. Stacks 0DBF part (2), AlgebraicGeometry.exists_standardPHCovering_refinement_bind, collapses this two-step covering of U' into a single standard ph covering.

public theorem isPHCovering_pullback {T T' : Scheme.{u}} {I : Type v} {X : I → Scheme.{u}}
    {f : ∀ i, X i ⟶ T} (hf : IsPHCovering X f) (g : T' ⟶ T) :
    IsPHCovering (fun i ↦ pullback (f i) g) (fun i ↦ pullback.snd (f i) g)

AlgebraicGeometry.isPHCovering_bind, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/CoveringsParts0DBI.lean, line 246. The attribute's comment: “part (2)”.

Stacks 0DBI part (2). If E is a ph covering of T and F i is a ph covering of the member E.X i for each i, then the family of all composites (F i).X j ⟶ E.X i ⟶ T, which is CategoryTheory.PreZeroHypercover.bind, is a ph covering of T.

Fix an affine open U of T. The outer covering has a standard ph refinement 𝒜 over U, say with 𝒜.X q mapping to E.X (i q) by a morphism c q over U. Each 𝒜.X q is affine, so the base change of the inner covering F (i q) along c q, which is a ph covering of 𝒜.X q by AlgebraicGeometry.isPHCovering_pullback, has a standard ph refinement 𝒞 q by AlgebraicGeometry.IsPHCovering.exists_standardPHCovering. The two-step covering 𝒜.bind 𝒞 of U refines the base change of E.bind F to U, and Stacks 0DBF part (2), AlgebraicGeometry.exists_standardPHCovering_refinement_bind, collapses it into a single standard ph covering of U.

public theorem isPHCovering_bind {T : Scheme.{u}} (E : PreZeroHypercover.{v} T)
    (hE : IsPHCovering E.X E.f) (F : ∀ i, PreZeroHypercover.{w} (E.X i))
    (hF : ∀ i, IsPHCovering (F i).X (F i).f) :
    IsPHCovering (E.bind F).X (E.bind F).f
Tag 0DBJ, a definition

Tag 0DBJ in the Stacks Project.

AlgebraicGeometry.BigPHSite, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/BigSite.lean, line 71.

Stacks 0DBJ. A big ph site consists of an initial set of schemes and initial ph coverings, a sufficiently large cutoff category containing them, and a bounded collection of ph coverings satisfying the site axioms and representing every ph covering.

public structure BigPHSite
Tag 0DBK, a lemma

Tag 0DBK in the Stacks Project.

AlgebraicGeometry.standardPHCovering_tautologicallyEquivalent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/PhSiteCoverings.lean, line 180. The attribute's comment: “part (2)”.

Stacks 0DBK, part (2). A standard ph covering is tautologically equivalent to a covering in the big ph site.

public theorem standardPHCovering_tautologicallyEquivalent
    (B : BigPHSite.{u}) (T : B.Schemes) [IsAffine T.1]
    (E : PreZeroHypercover.{v} T.1) (hE : StandardPHCovering E.f) :
    ∃ F : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, F⟩ ∧
        PreZeroHypercover.TautologicallyEquivalent E (F.map B.inclusion)

AlgebraicGeometry.openCover_tautologicallyEquivalent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/PhSiteCoverings.lean, line 209. The attribute's comment: “part (3)”.

Stacks 0DBK, part (3). A Zariski open covering is tautologically equivalent to a covering in the big ph site.

public theorem openCover_tautologicallyEquivalent
    (B : BigPHSite.{u}) (T : B.Schemes) (U : T.1.OpenCover.{v}) :
    ∃ F : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, F⟩ ∧
        PreZeroHypercover.TautologicallyEquivalent U.toPreZeroHypercover
          (F.map B.inclusion)

AlgebraicGeometry.exists_isCovering_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/PhSiteCoverings.lean, line 277. The attribute's comment: “part (1)”.

Stacks 0DBK, part (1). Every ph covering of an object of a big ph site is refined by one of the site's own covering families.

The refinement is assembled from parts (2) and (3) by the site's composition axiom: the affine opens of the target form a Zariski covering, hence by part (3) are tautologically equivalent to a covering G of the site, and each member of G is isomorphic over the target to an affine open, hence by the definition of a ph covering carries a standard ph covering refining the given family there, which by part (2) is tautologically equivalent to a covering of the site.

public theorem exists_isCovering_refinement
    (B : BigPHSite.{u}) (T : B.Schemes)
    (E : PreZeroHypercover.{v} T.1) (hE : IsPHCovering E.X E.f) :
    ∃ F : PreZeroHypercover.{u + 1} T,
      B.IsCovering ⟨T, F⟩ ∧ Nonempty ((F.map B.inclusion).Hom E)
Tag 0DBL, a definition

Tag 0DBL in the Stacks Project.

AlgebraicGeometry.BigPHOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/BigSite.lean, line 173. The attribute's comment: “part (1), category”.

Stacks 0DBL, part (1). The big ph category of S is the slice of the chosen big ph category over its object S.

public abbrev BigPHOver

AlgebraicGeometry.BigPHOver.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/BigSite.lean, line 188. The attribute's comment: “part (1), coverings”.

Stacks 0DBL, part (1). A family in the slice covers precisely when its underlying family covers in the chosen big ph site.

public abbrev IsCovering (E : Covering (BigPHOver B S hS)) : Prop

AlgebraicGeometry.BigAffinePH, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/BigSite.lean, line 204. The attribute's comment: “part (2), category”.

Stacks 0DBL, part (2). The big affine ph category is the full subcategory of affine objects in the big ph category over S.

public abbrev BigAffinePH

AlgebraicGeometry.BigAffinePH.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/BigSite.lean, line 223. The attribute's comment: “part (2), coverings”.

Stacks 0DBL, part (2). An affine family covers exactly when it is a finite covering family in the big ph site over S.

public abbrev IsCovering (E : Covering (BigAffinePH B S hS)) : Prop
Tag 0DBM, a lemma

Tag 0DBM in the Stacks Project.

AlgebraicGeometry.BigAffinePH.isSite, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/BigSite.lean, line 274.

Stacks 0DBM. Finite ph covering families of affine objects over S satisfy the axioms of a site.

public lemma isSite (B : BigPHSite.{u}) (S : Scheme.{u})
    (hS : B.Contains S) : IsSite (BigAffinePH.IsCovering B S hS)
Tag 0DBN, a lemma

Tag 0DBN in the Stacks Project.

Declarations registered for the tag:

Tag 0DBP, a lemma

Tag 0DBP in the Stacks Project.

AlgebraicGeometry.BigAffinePH.inclusion_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/AffinePhDenseSubsite.lean, line 200. The attribute's comment: “cocontinuity”.

Stacks 0DBP, cocontinuity. The inclusion of affine objects over S in a chosen big ph site is cocontinuous.

public instance BigAffinePH.inclusion_isCocontinuous
    (B : BigPHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    (BigAffinePH.inclusion B S hS).IsCocontinuous
      (BigAffinePH.topology B S hS)
      (BigPHOver.topology B S hS)

AlgebraicGeometry.BigAffinePH.inclusion_isDenseSubsite, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/AffinePhDenseSubsite.lean, line 287. The attribute's comment: “equivalence of topoi”.

Stacks 0DBP, equivalence of topoi. The inclusion of affine objects is a dense subsite, hence its induced morphism of sheaf topoi is an equivalence.

public instance BigAffinePH.inclusion_isDenseSubsite
    (B : BigPHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    (BigAffinePH.inclusion B S hS).IsDenseSubsite
      (BigAffinePH.topology B S hS)
      (BigPHOver.topology B S hS)
Tag 0DBQ, a lemma

Tag 0DBQ in the Stacks Project.

AlgebraicGeometry.isSheaf_iff_zariski_and_properSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/PhSheafCriterion.lean, line 959. The attribute's comment: “sheaf characterization”.

Stacks 0DBQ, characterization. The ph sheaf condition is equivalent to Zariski descent together with proper-surjective descent.

public theorem isSheaf_iff_zariski_and_properSurjective :
    Presieve.IsSheaf (BigPHOver.topology B S hS) F ↔
      (IsZariskiSheaf B S hS F ∧ IsProperSurjectiveSheaf B S hS F)

AlgebraicGeometry.properSurjective_iff_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/PhSheafCriterion.lean, line 981. The attribute's comment: “affine reduction”.

Stacks 0DBQ, affine reduction. Under Zariski descent, proper-surjective descent may be checked only when the target is affine.

public theorem properSurjective_iff_affine (hF : IsZariskiSheaf B S hS F) :
    IsProperSurjectiveSheaf B S hS F ↔
      IsAffineProperSurjectiveSheaf B S hS F
Tag 0DBR, a lemma

Tag 0DBR in the Stacks Project.

AlgebraicGeometry.bigPHMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/MorphismOfTopoi.lean, line 71. The attribute's comment: “the morphism of topoi”.

Stacks 0DBR. The morphism of big ph topoi induced by f.

public noncomputable def bigPHMorphism :
    MorphismOfTopoi
      (Sheaf (BigPHOver.topology B T.obj T.property) (Type (u + 1)))
      (Sheaf (BigPHOver.topology B S.obj S.property) (Type (u + 1)))

AlgebraicGeometry.bigPHMorphismInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/MorphismOfTopoi.lean, line 89. The attribute's comment: “the inverse-image formula”.

Stacks 0DBR. Inverse image is restriction along postcomposition, naturally in sheaves and objects.

public noncomputable def bigPHMorphismInverseImageIso :
    (bigPHMorphism B T S f).inverseImage ≅
      (Over.map f).sheafPushforwardContinuous (Type (u + 1))
        (BigPHOver.topology B T.obj T.property)
        (BigPHOver.topology B S.obj S.property)

AlgebraicGeometry.bigPHMorphismPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/MorphismOfTopoi.lean, line 101. The attribute's comment: “the direct-image formula”.

Stacks 0DBR. Direct image is restriction along base change, naturally in sheaves and objects.

public noncomputable def bigPHMorphismPushforwardIso :
    (bigPHMorphism B T S f).pushforward ≅
      (Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
        (BigPHOver.topology B S.obj S.property)
        (BigPHOver.topology B T.obj T.property)

AlgebraicGeometry.bigPHLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/MorphismOfTopoi.lean, line 110. The attribute's comment: “existence of lower shriek”.

Stacks 0DBR. The lower shriek functor is left adjoint to inverse image.

public noncomputable def bigPHLowerShriekAdjunction :
    (Over.map f).sheafPullback (Type (u + 1))
      (BigPHOver.topology B T.obj T.property)
      (BigPHOver.topology B S.obj S.property) ⊣
        (bigPHMorphism B T S f).inverseImage

AlgebraicGeometry.bigPHLowerShriek_preservesPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/MorphismOfTopoi.lean, line 122. The attribute's comment: “lower shriek preserves fibre products”.

Stacks 0DBR. Lower shriek preserves fibre products.

public instance bigPHLowerShriek_preservesPullbacks :
    PreservesLimitsOfShape WalkingCospan
      ((Over.map f).sheafPullback (Type (u + 1))
        (BigPHOver.topology B T.obj T.property)
        (BigPHOver.topology B S.obj S.property))

AlgebraicGeometry.bigPHLowerShriek_preservesEqualizers, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/MorphismOfTopoi.lean, line 135. The attribute's comment: “lower shriek preserves equalizers”.

Stacks 0DBR. Lower shriek preserves equalizers.

public instance bigPHLowerShriek_preservesEqualizers :
    PreservesLimitsOfShape WalkingParallelPair
      ((Over.map f).sheafPullback (Type (u + 1))
        (BigPHOver.topology B T.obj T.property)
        (BigPHOver.topology B S.obj S.property))

Declarations registered for the tag:

Tag 0DBS, a lemma

Tag 0DBS in the Stacks Project.

AlgebraicGeometry.bigPHMorphism_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/Composition.lean, line 45. The attribute's comment: “direct-image composition”.

Stacks 0DBS. Direct image for the composite morphism of big ph topoi is naturally isomorphic to the composite of the direct-image functors.

public noncomputable def bigPHMorphism_comp_pushforwardIso :
    (bigPHMorphism B X Z (f ≫ g)).pushforward ≅
      (bigPHMorphism B X Y f).pushforward ⋙
      (bigPHMorphism B Y Z g).pushforward

AlgebraicGeometry.bigPHMorphism_comp_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/Composition.lean, line 67. The attribute's comment: “inverse-image composition”.

Stacks 0DBS. Inverse image for the composite morphism of big ph topoi is naturally isomorphic to the composite of the inverse-image functors.

public noncomputable def bigPHMorphism_comp_inverseImageIso :
    (bigPHMorphism B X Z (f ≫ g)).inverseImage ≅
      (bigPHMorphism B Y Z g).inverseImage ⋙
        (bigPHMorphism B X Y f).inverseImage
Sources
LeanAlgebraicGeometry.StandardPHCovering · AlgebraicGeometry.StandardPHCovering.pullback · AlgebraicGeometry.exists_standardPHCovering_refinement_bind · AlgebraicGeometry.exists_standardPHCovering_refinement_of_openCover · AlgebraicGeometry.IsPHCovering · AlgebraicGeometry.IsPHCovering.of_openCover · AlgebraicGeometry.surjective_proper_isPHCovering · AlgebraicGeometry.isPHCovering_tfae

Section34.9 The fpqc topology#

Section 34.9 of the Stacks Project, Tag 022A. 12 tags here are carried by 21 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03L7, a lemma

Tag 03L7 in the Stacks Project.

AlgebraicGeometry.mem_fpqcPrecoverage_iff_affine_finite_support, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/Characterization.lean, line 169. The attribute's comment: “conditions (1) and (2)”.

A family is an fpqc covering if and only if every member is flat and every affine open of the target is the union of the images of quasi-compact opens in the sources, all but finitely many of which are empty.

public lemma mem_fpqcPrecoverage_iff_affine_finite_support :
    Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage T ↔
      ((∀ i, Flat (f i)) ∧
        (∀ U : T.Opens, IsAffineOpen U →
            ∃ V : ∀ i, (X i).Opens,
              ((∀ i, IsCompact (V i : Set (X i))) ∧
                ({i | V i ≠ ⊥} : Set I).Finite ∧
                ⋃ i, f i '' (V i : Set (X i)) = (U : Set T))))

AlgebraicGeometry.mem_fpqcPrecoverage_iff_exists_affine_open_cover, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/Characterization.lean, line 228. The attribute's comment: “conditions (1) and (3)”.

A family is an fpqc covering if and only if its members are flat and some affine open covering of the target is, member by member, the union of images of finitely many quasi-compact opens in the sources.

public lemma mem_fpqcPrecoverage_iff_exists_affine_open_cover :
    Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage T ↔
      ((∀ i, Flat (f i)) ∧
        ∃ (A : Type u) (U : A → T.Opens),
          ((∀ a, IsAffineOpen (U a)) ∧
            (⋃ a, (U a : Set T)) = Set.univ ∧
            ∀ a, ∃ (n : ℕ) (i : Fin n → I) (V : ∀ j, (X (i j)).Opens),
              ((∀ j, IsCompact (V j : Set (X (i j)))) ∧
                ⋃ j, f (i j) '' (V j : Set (X (i j))) = (U a : Set T))))

AlgebraicGeometry.mem_fpqcPrecoverage_iff_pointwise_compact_open_neighborhood, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/Characterization.lean, line 303. The attribute's comment: “conditions (1) and (4)”.

If the target is quasi-separated, a family is an fpqc covering if and only if its members are flat and every point has a neighborhood which is the union of the images of finitely many quasi-compact opens in the sources. The neighborhood itself is not required to be open.

public lemma mem_fpqcPrecoverage_iff_pointwise_compact_open_neighborhood
    [QuasiSeparatedSpace T] :
    Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage T ↔
      ((∀ i, Flat (f i)) ∧
        ∀ t : T, ∃ (n : ℕ) (i : Fin n → I) (V : ∀ j, (X (i j)).Opens),
          ((∀ j, IsCompact (V j : Set (X (i j)))) ∧
            (⋃ j, f (i j) '' (V j : Set (X (i j)))) ∈ nhds t))
Tag 0H7E, an example

Tag 0H7E in the Stacks Project.

AlgebraicGeometry.DoubledOriginSource.flat_map, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/FpqcCounterexample/DoubledOriginSource.lean, line 115. The attribute's comment: “flatness”.

The canonical map from the first chart and the local scheme of the second chart to the doubled-origin scheme is flat.

public instance flat_map (S : DoubledOriginSource.{u}) : Flat S.map

AlgebraicGeometry.DoubledOriginSource.surjective_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/FpqcCounterexample/DoubledOriginSource.lean, line 223. The attribute's comment: “surjectivity”.

The canonical map from an affine chart and the local spectrum covers the scheme with doubled origin.

public theorem surjective_map (S : DoubledOriginSource.{u}) :
    Surjective S.map

AlgebraicGeometry.DoubledOriginSource.map_image_ne_range_secondChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/FpqcCounterexample/NotFpqc.lean, line 250. The attribute's comment: “no_quasicompact_open”.

No quasi-compact open of the source maps onto the second affine chart of the infinite-dimensional doubled-origin scheme.

public theorem map_image_ne_range_secondChart (S : DoubledOriginSource)
    (W : S.source.Opens) (hW : IsCompact (W : Set S.source)) :
    S.map.base '' (W : Set S.source) ≠ Set.range S.secondChart.base

AlgebraicGeometry.DoubledOriginSource.exists_isCompact_opens_image_mem_nhds, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/FpqcCounterexample/NotFpqc.lean, line 307. The attribute's comment: “pointwise_condition”.

Every point of the doubled-origin scheme has a neighbourhood that is the image of a quasi-compact open of the source of the canonical map.

public theorem exists_isCompact_opens_image_mem_nhds
    (S : DoubledOriginSource.{u}) (x : S.target) :
    ∃ V : S.source.Opens,
      IsCompact (V : Set S.source) ∧ S.map '' (V : Set S.source) ∈ nhds x

AlgebraicGeometry.DoubledOriginSource.singleton_map_notMem_fpqcPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/FpqcCounterexample/NotFpqc.lean, line 319. The attribute's comment: “not_fpqc”.

The map from the affine chart and the local scheme at the origin to the infinite-dimensional doubled-origin scheme does not form an fpqc covering.

public theorem singleton_map_notMem_fpqcPrecoverage (S : DoubledOriginSource.{u}) :
    Presieve.singleton S.map ∉ Scheme.fpqcPrecoverage S.target
Tag 040I, a lemma

Tag 040I in the Stacks Project.

AlgebraicGeometry.ofArrows_mem_fpqcPrecoverage_iff_singleton_sigmaDesc_mem, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/DisjointUnion.lean, line 157.

A family of morphisms of schemes is an fpqc covering precisely when the induced morphism from the disjoint union of the source schemes is an fpqc covering.

public lemma ofArrows_mem_fpqcPrecoverage_iff_singleton_sigmaDesc_mem
    {ι : Type v} [Small.{u} ι] {T : Scheme.{u}} (T' : ι → Scheme.{u})
    (f : ∀ i, T' i ⟶ T) :
    Presieve.ofArrows T' f ∈ Scheme.fpqcPrecoverage T ↔
      Presieve.singleton (Sigma.desc f) ∈ Scheme.fpqcPrecoverage T
Tag 03L9, a lemma

Tag 03L9 in the Stacks Project.

AlgebraicGeometry.ofArrows_mem_fpqcPrecoverage_of_fpqc_locally, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/Characterization.lean, line 441.

Being an fpqc covering is local on an fpqc covering of the base. If every member of a family f i : X i ⟶ T is flat and there is an fpqc covering g j : S j ⟶ T of the target such that for every j the base-changed family S j ×[T] X i ⟶ S j is an fpqc covering of S j, then f is an fpqc covering of T.

public lemma ofArrows_mem_fpqcPrecoverage_of_fpqc_locally
    {J : Type w} {S : J → Scheme.{u}} (g : ∀ j, S j ⟶ T)
    (hflat : ∀ i, Flat (f i))
    (hg : Presieve.ofArrows S g ∈ Scheme.fpqcPrecoverage T)
    (hbc : ∀ j, Presieve.ofArrows (fun i ↦ pullback (g j) (f i))
      (fun i ↦ pullback.fst (g j) (f i)) ∈ Scheme.fpqcPrecoverage (S j)) :
    Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage T
Tag 022C, a lemma

Tag 022C in the Stacks Project.

AlgebraicGeometry.Scheme.smoothPrecoverage_le_fpqcPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/Coverings.lean, line 53. The attribute's comment: “smooth coverings”.

Stacks 022C. Every smooth covering family is an fpqc covering family.

public theorem smoothPrecoverage_le_fpqcPrecoverage :
    Scheme.precoverage (@Smooth : MorphismProperty Scheme.{u}) ≤
      Scheme.fpqcPrecoverage

AlgebraicGeometry.Scheme.etalePrecoverage_le_fpqcPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/Coverings.lean, line 60. The attribute's comment: “étale coverings”.

Stacks 022C, 03PH. Every étale covering family is an fpqc covering family.

public theorem etalePrecoverage_le_fpqcPrecoverage :
    Scheme.etalePrecoverage ≤ Scheme.fpqcPrecoverage

AlgebraicGeometry.Scheme.syntomicPrecoverage_le_fpqcPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/FinerTopologies.lean, line 84. The attribute's comment: “syntomic coverings”.

Stacks 022C. Every syntomic covering family is an fpqc covering family.

public theorem syntomicPrecoverage_le_fpqcPrecoverage :
    Scheme.precoverage (@Syntomic : MorphismProperty Scheme.{u}) ≤ Scheme.fpqcPrecoverage

Declarations registered for the tag:

Tag 022E, a lemma

Tag 022E in the Stacks Project.

AlgebraicGeometry.exists_finite_affineCover_flat_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/StandardRefinement.lean, line 163.

An fpqc covering of an affine scheme admits a refinement by a standard fpqc covering: a finite jointly surjective family of flat morphisms from affine schemes, again an fpqc covering, whose members are affine open subschemes of members of the given covering.

public theorem exists_finite_affineCover_flat_refinement {T : Scheme.{u}} [IsAffine T]
    (U : PreZeroHypercover.{v} T) (hU : U.presieve₀ ∈ Scheme.fpqcPrecoverage T) :
    ∃ (V : T.AffineCover.{0} (@Flat.{u})) (refinement : V.cover.toPreZeroHypercover.Hom U),
      Finite V.I₀ ∧ V.cover.presieve₀ ∈ Scheme.fpqcPrecoverage T ∧
        ∀ j, IsOpenImmersion (refinement.h₀ j)
Tag 022F, a definition

Tag 022F in the Stacks Project.

AlgebraicGeometry.IsStandardFpqcCovering, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/StandardCoverings.lean, line 69.

A family fᵢ : Uᵢ ⟶ T is a standard fpqc covering if it is finite, its target and all its sources are affine, every fᵢ is flat, and the images of the fᵢ cover T.

public structure IsStandardFpqcCovering {T : Scheme.{u}} {I : Type v}
    (U : I → Scheme.{u}) (f : ∀ i, U i ⟶ T) : Prop
Tag 03LA, a lemma

Tag 03LA in the Stacks Project.

AlgebraicGeometry.isStandardFpqcCovering_of_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/StandardCoveringProperties.lean, line 116. The attribute's comment: “(1)”.

Stacks 03LA (1). If T' ⟶ T is an isomorphism onto an affine scheme, then the one-member family {T' ⟶ T} is a standard fpqc covering: the source is affine because it is isomorphic to the affine target, and an isomorphism is flat and surjective.

public theorem isStandardFpqcCovering_of_isIso {T T' : Scheme.{u}} [IsAffine T] (f : T' ⟶ T)
    [IsIso f] : IsStandardFpqcCovering (fun _ : PUnit.{v + 1} ↦ T') (fun _ ↦ f)

AlgebraicGeometry.IsStandardFpqcCovering.bind, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/StandardCoveringProperties.lean, line 133. The attribute's comment: “(2)”.

Stacks 03LA (2). If {T_i ⟶ T}_{i ∈ I} is a standard fpqc covering and {T_ij ⟶ T_i}_{j ∈ J i} is a standard fpqc covering for every i, then the family of composites {T_ij ⟶ T}_{⟨i, j⟩ ∈ Σ i, J i} is a standard fpqc covering. Its index is the sigma type of the indices, finite because each of its factors is; its members are composites of flat morphisms, hence flat; and a point of T is hit through some member of the outer family and then through some member of the inner family above it. The inner and the outer index types may lie in different universes.

public theorem IsStandardFpqcCovering.bind {T : Scheme.{u}} {I : Type v} {U : I → Scheme.{u}}
    {f : ∀ i, U i ⟶ T} (hf : IsStandardFpqcCovering U f) {J : I → Type w}
    {V : ∀ i, J i → Scheme.{u}} {g : ∀ i (j : J i), V i j ⟶ U i}
    (hg : ∀ i, IsStandardFpqcCovering (V i) (g i)) :
    IsStandardFpqcCovering (fun ij : Σ i, J i ↦ V ij.1 ij.2)
      (fun ij : Σ i, J i ↦ g ij.1 ij.2 ≫ f ij.1)

AlgebraicGeometry.IsStandardFpqcCovering.pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/StandardCoveringProperties.lean, line 161. The attribute's comment: “(3)”.

Stacks 03LA (3). If {T_i ⟶ T}_{i ∈ I} is a standard fpqc covering and T' ⟶ T is a morphism of affine schemes, then the family of first projections {T' ×_T T_i ⟶ T'}_{i ∈ I} is a standard fpqc covering. The index is unchanged, flatness is preserved by base change, each fibre product is affine because it is a fibre product of affine schemes over an affine base, Stacks 01JQ, and a point of T' lies under a point of the fibre product over any point of T_i with the same image in T.

public theorem IsStandardFpqcCovering.pullback {T : Scheme.{u}} {I : Type v} {U : I → Scheme.{u}}
    {f : ∀ i, U i ⟶ T} (hf : IsStandardFpqcCovering U f) {T' : Scheme.{u}} [IsAffine T']
    (g : T' ⟶ T) :
    IsStandardFpqcCovering (fun i ↦ Limits.pullback g (f i))
      (fun i ↦ Limits.pullback.fst g (f i))
Tag 03LB, a lemma

Tag 03LB in the Stacks Project.

AlgebraicGeometry.presieve₀_mem_fpqcPrecoverage_of_affine_refinements, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/Characterization.lean, line 350. References: SGA 3 IV (6.3.1), “(i) fpqc, sufficiency”.

A flat family which admits a standard fpqc refinement after every affine base change is an fpqc covering.

public lemma presieve₀_mem_fpqcPrecoverage_of_affine_refinements
    {T : Scheme.{u}} (U : PreZeroHypercover.{v} T)
    (hflat : ∀ i, Flat (U.f i))
    (hrefine : ∀ {Z : Scheme.{u}} [IsAffine Z] (h : Z ⟶ T),
      ∃ (V : Z.AffineCover.{0} @Flat), Finite V.I₀ ∧
        Nonempty (V.cover.toPreZeroHypercover.Hom (U.pullback₂ h))) :
    U.presieve₀ ∈ Scheme.fpqcPrecoverage T
Tag 022G, a definition

Tag 022G in the Stacks Project.

Declarations registered for the tag:

Tag 022H, a lemma

Tag 022H in the Stacks Project.

AlgebraicGeometry.isSheaf_fpqcTopology_iff_zariski_and_standardCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/StandardSheafCondition.lean, line 112. The attribute's comment: “condition (2): the sheaf property for an arbitrary standard fpqc covering, the clause Mathlib's isSheaf_type_propQCTopology_iff does not state; conditions (1) and (2') are Mathlib's, tagged there”. References: SGA 3 XI (3.4), “special case”.

Stacks 022H, condition (2). A presheaf of sets on the category of schemes is a sheaf for the fpqc topology if and only if it is a sheaf for the Zariski topology and satisfies the sheaf property for every standard fpqc covering: every finite jointly surjective family of flat morphisms with affine sources over an affine base.

public theorem isSheaf_fpqcTopology_iff_zariski_and_standardCovering
    (F : Scheme.{u}ᵒᵖ ⥤ Type v) :
    Presieve.IsSheaf Scheme.fpqcTopology.{u} F ↔
      Presieve.IsSheaf Scheme.zariskiTopology.{u} F ∧
        ∀ {T : Scheme.{u}} [IsAffine T] (𝒱 : T.AffineCover.{w} (@Flat.{u})), Finite 𝒱.I₀ →
          Presieve.IsSheafFor F 𝒱.cover.presieve₀
Tag 0BBK, a lemma

Tag 0BBK in the Stacks Project.

AlgebraicGeometry.exists_fpqcCover_not_refined_by_family, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fpqc/NoCofinalSet.lean, line 170.

No small family of fpqc coverings of the spectrum of a nonzero ring is cofinal under refinement.

public theorem exists_fpqcCover_not_refined_by_family
    (R : Type u) [CommRing R] [Nontrivial R]
    (A : Type u)
    (U : A → Scheme.fpqcPrecoverage.ZeroHypercover.{u} (Spec (.of R))) :
    ∃ V : Scheme.fpqcPrecoverage.ZeroHypercover.{u} (Spec (.of R)),
      ∀ a : A, ¬ Nonempty ((U a).toPreZeroHypercover.Hom V.toPreZeroHypercover)
Sources
LeanAlgebraicGeometry.mem_fpqcPrecoverage_iff_affine_finite_support · AlgebraicGeometry.mem_fpqcPrecoverage_iff_exists_affine_open_cover · AlgebraicGeometry.mem_fpqcPrecoverage_iff_pointwise_compact_open_neighborhood · AlgebraicGeometry.DoubledOriginSource.flat_map · AlgebraicGeometry.DoubledOriginSource.surjective_map · AlgebraicGeometry.DoubledOriginSource.map_image_ne_range_secondChart · AlgebraicGeometry.DoubledOriginSource.exists_isCompact_opens_image_mem_nhds · AlgebraicGeometry.DoubledOriginSource.singleton_map_notMem_fpqcPrecoverage

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.