73 Topologies on Algebraic Spaces

Chapter 73 of the Stacks Project, Topologies on Algebraic Spaces, Tag 03Y4: the 7 sections of its 9 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 46 tags are carried by 141 declarations of the repository (all in StacksFrontier) and 32 registered declarations.

Section73.3 Zariski topology#

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

Tag 041G, a definition

Tag 041G in the Stacks Project.

AlgebraicGeometry.Space.IsZariskiCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/Zariski.lean, line 81.

Stacks 041G. A family of open immersions whose images cover every point of the target.

abbrev IsZariskiCovering (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (I : Type v) (Xᵢ : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (f : ∀ i, Xᵢ i ⟶ X) : Prop

AlgebraicGeometry.Space.isZariskiCovering_yoneda_of_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiCoveringOfOpenCover.lean, line 103. The attribute's comment: “an open cover of an object of the site”.

Stacks 041G for an open cover of an object of the big fppf site of S. A family of morphisms of the site whose underlying morphisms of schemes are open immersions covering the underlying scheme of the target induces a Zariski covering of the presheaf represented by the target.

theorem isZariskiCovering_yoneda_of_openCover
    {I : Type v} {T : BigFppfOver B S hS} (X : I → BigFppfOver B S hS) (g : ∀ i, X i ⟶ T)
    (hopen : ∀ i, _root_.AlgebraicGeometry.IsOpenImmersion
      ((BigFppfOver.toScheme B S hS).map (g i)))
    (hcov : ∀ x : (BigFppfOver.toScheme B S hS).obj T,
      ∃ i, x ∈ Set.range ((BigFppfOver.toScheme B S hS).map (g i))) :
    IsZariskiCovering B S hS I (fun i => yoneda.obj (X i)) (fun i => yoneda.map (g i))
Tag 041H, a lemma

Tag 041H in the Stacks Project.

AlgebraicGeometry.Space.isZariskiCovering_of_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/Zariski.lean, line 92. The attribute's comment: “isomorphism_cover”.

Stacks 041H. An isomorphism gives a singleton Zariski covering.

theorem isZariskiCovering_of_isIso
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (X X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (f : X' ⟶ X) [IsIso f] :
    IsZariskiCovering B S hS PUnit (fun _ => X') (fun _ => f)

AlgebraicGeometry.Space.isZariskiCovering_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/Zariski.lean, line 107. The attribute's comment: “composition_cover”.

Stacks 041H. Composing a Zariski covering with a covering of each member gives a Zariski covering.

theorem isZariskiCovering_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (I : Type v) (J : I → Type w)
    (Xᵢ : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (Xᵢⱼ : ∀ i, J i → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (f : ∀ i, Xᵢ i ⟶ X)
    (g : ∀ i j, Xᵢⱼ i j ⟶ Xᵢ i)
    (hf : IsZariskiCovering B S hS I Xᵢ f)
    (hg : ∀ i, IsZariskiCovering B S hS (J i) (Xᵢⱼ i) (g i)) :
    IsZariskiCovering B S hS (Σ i, J i)
      (fun p => Xᵢⱼ p.1 p.2) (fun p => g p.1 p.2 ≫ f p.1)

AlgebraicGeometry.Space.isZariskiCovering_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/Zariski.lean, line 137. The attribute's comment: “base_change_cover”.

Stacks 041H. Zariski coverings are stable under base change: the first projections of the fibre products of a Zariski covering {Xᵢ ⟶ X} with a morphism g : X' ⟶ X form a Zariski covering of X'.

theorem isZariskiCovering_pullback
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (I : Type v) (Xᵢ : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (f : ∀ i, Xᵢ i ⟶ X) (g : X' ⟶ X)
    (h : IsZariskiCovering B S hS I Xᵢ f) :
    IsZariskiCovering B S hS I (fun i => Limits.pullback g (f i))
      (fun i => Limits.pullback.fst g (f i))
Sources
LeanAlgebraicGeometry.Space.IsZariskiCovering · AlgebraicGeometry.Space.isZariskiCovering_yoneda_of_openCover · AlgebraicGeometry.Space.isZariskiCovering_of_isIso · AlgebraicGeometry.Space.isZariskiCovering_comp · AlgebraicGeometry.Space.isZariskiCovering_pullback

Section73.4 Étale topology#

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

Tag 041E, a definition

Tag 041E in the Stacks Project.

AlgebraicGeometry.Space.IsEtaleCovering, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Coverings.lean, line 344.

Stacks 041E. A family of morphisms of algebraic spaces over S with common target is an étale covering when every member is étale and the family is jointly surjective on points.

structure IsEtaleCovering {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, X i ⟶ F) : Prop
Tag 0DF1, a lemma

Tag 0DF1 in the Stacks Project.

AlgebraicGeometry.Space.isEtaleCovering_of_isZariskiCovering, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/Zariski.lean, line 158.

Stacks 0DF1. Every Zariski covering of algebraic spaces is an étale covering.

lemma isEtaleCovering_of_isZariskiCovering
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {I : Type v} {Xᵢ : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {f : ∀ i, Xᵢ i ⟶ X}
    (hX : IsAlgebraicSpace B S hS X)
    (hXᵢ : ∀ i, IsAlgebraicSpace B S hS (Xᵢ i))
    (h : IsZariskiCovering B S hS I Xᵢ f) :
    IsEtaleCovering B S hS Xᵢ f
Tag 041F, a lemma

Tag 041F in the Stacks Project.

AlgebraicGeometry.Space.isEtaleCovering_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/EtaleCovering.lean, line 75. The attribute's comment: “etale_covering_comp”.

An étale covering of each member of an étale covering composes to an étale covering of the original algebraic space.

public theorem isEtaleCovering_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type v} (J : I → Type w)
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (Xᵢ : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (f : ∀ i, Xᵢ i ⟶ X)
    (Xᵢⱼ : ∀ i, J i → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (g : ∀ i j, Xᵢⱼ i j ⟶ Xᵢ i)
    (hf : IsEtaleCovering B S hS Xᵢ f)
    (hg : ∀ i, IsEtaleCovering B S hS (Xᵢⱼ i) (g i)) :
    IsEtaleCovering B S hS
      (fun ij : (i : I) × J i => Xᵢⱼ ij.1 ij.2)
      (fun ij => g ij.1 ij.2 ≫ f ij.1)

AlgebraicGeometry.Space.isEtaleCovering_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/EtaleCovering.lean, line 103. The attribute's comment: “etale_covering_base_change”.

Stacks 041F, the base-change clause. The first projections of the presheaf fibre products of an étale covering of an algebraic space over S with a morphism g into its target form an étale covering of the source of g.

theorem isEtaleCovering_pullback
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type v} {X X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (g : X' ⟶ X) (hX' : IsAlgebraicSpace B S hS X')
    (Y : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, Y i ⟶ X)
    (h : IsEtaleCovering B S hS Y f) :
    IsEtaleCovering B S hS (fun i => CategoryTheory.Limits.pullback g (f i))
      (fun i => CategoryTheory.Limits.pullback.fst g (f i))

AlgebraicGeometry.Space.isEtaleCovering_of_isIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormallySmooth/EtaleCovering.lean, line 134. The attribute's comment: “isomorphism_etale_covering”.

Stacks 041F, the isomorphism clause. An isomorphism of algebraic spaces over S, regarded as a family indexed by a point, is an étale covering.

lemma isEtaleCovering_of_isIso
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X' ⟶ X) [IsIso f]
    (hX : IsAlgebraicSpace B S hS X) :
    IsEtaleCovering B S hS (fun _ : Unit ↦ X') (fun _ ↦ f)
Tag 0CFV, a lemma

Tag 0CFV in the Stacks Project.

AlgebraicGeometry.Space.exists_isEtaleCovering_refining_isSmoothCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmoothEtaleRefinement.lean, line 41.

A smooth covering of an algebraic space over S is refined by an étale covering of it: there is an étale covering each of whose members factors through a member of the given smooth covering, compatibly with the morphisms to the common target.

theorem exists_isEtaleCovering_refining_isSmoothCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : ∀ i, X i ⟶ F}
    (hf : IsSmoothCovering B S hS X f) :
    ∃ (J : Type u) (U : J → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (g : ∀ j, U j ⟶ F),
      IsEtaleCovering B S hS U g ∧
        ∀ j, ∃ (i : I) (h : U j ⟶ X i), h ≫ f i = g j

AlgebraicGeometry.Space.exists_isEtaleCovering_representable_refining_isSmoothCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmoothEtaleRefinementRepresentable.lean, line 168. The attribute's comment: “the refinement with every member of it representable by a scheme of the site”.

Stacks 0CFV. Every smooth covering of an algebraic space over S is refined by an étale covering: there are an étale covering of the same target, whose members are schemes of the site, and, for each of its members, a member of the given covering together with a morphism to it over the common target.

theorem exists_isEtaleCovering_representable_refining_isSmoothCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : ∀ i, X i ⟶ F}
    (hsm : IsSmoothCovering B S hS X f) :
    ∃ (J : Type (u + 1)) (Y : J → BigFppfOver B S hS) (g : ∀ j, yoneda.obj (Y j) ⟶ F),
      IsEtaleCovering B S hS (fun j => yoneda.obj (Y j)) g ∧
        ∀ j, ∃ (i : I) (h : yoneda.obj (Y j) ⟶ X i), h ≫ f i = g j
Tag 0DBX, a definition

Tag 0DBX in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleSite.lean, line 89.

Stacks 0DBX. A big étale site of algebraic spaces over S: the chosen big étale site of schemes containing S, the category of algebraic spaces over S, and the set-sized system of étale covering families supplied by Stacks 000X.

structure BigEtaleSpaceSite (S : Scheme.{u})
Tag 0DBY, a definition

Tag 0DBY in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.bigEtaleTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleSite.lean, line 184.

Stacks 0DBY. The big étale topology of an algebraic space X of the site: the localization at X of the big étale topology of algebraic spaces over the base scheme.

abbrev bigEtaleTopology (T : BigEtaleSpaceSite S) (X : T.Spaces) :
    GrothendieckTopology (Over X)
Tag 0DF2, a lemma

Tag 0DF2 in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.inclusionFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallToBigEtale.lean, line 88. The attribute's comment: “the inclusion functor”.

Stacks 0DF2. Composition with f regards an algebraic space étale over Y as an object of the big étale site of X.

abbrev inclusionFunctor :
    Space.SpacesEtale T.fppfSite S T.fppf_mem Y ⥤ Over X

AlgebraicGeometry.BigEtaleSpaceSite.inclusionFunctor_isCocontinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallToBigEtale.lean, line 248. The attribute's comment: “cocontinuity”.

Stacks 0DF2. The inclusion of the spaces-étale site of Y into the big étale site of X is cocontinuous.

instance inclusionFunctor_isCocontinuous :
    (inclusionFunctor T f).IsCocontinuous
      (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) (T.bigEtaleTopology X)

AlgebraicGeometry.BigEtaleSpaceSite.smallToBigEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallToBigEtale.lean, line 323. The attribute's comment: “the morphism of topoi”.

Stacks 0DF2. The morphism of topoi from the spaces-étale topos of Y to the big étale topos of X induced by the inclusion functor. Its inverse image is restriction of sheaves along the inclusion, so its sections are computed by CategoryTheory.Functor.sheafPushforwardContinuous_obj_obj_obj.

noncomputable def smallToBigEtaleMorphism :
    MorphismOfTopoi
      (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) (Type (u + 1)))
      (Sheaf (T.bigEtaleTopology X) (Type (u + 1)))

AlgebraicGeometry.BigEtaleSpaceSite.lowerShriek, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallToBigEtale.lean, line 342. The attribute's comment: “the lower-shriek functor”.

Stacks 0DF2. The left adjoint of restriction along the inclusion functor.

noncomputable abbrev lowerShriek :
    Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) (Type (u + 1)) ⥤
      Sheaf (T.bigEtaleTopology X) (Type (u + 1))

AlgebraicGeometry.BigEtaleSpaceSite.lowerShriek_preservesPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallToBigEtale.lean, line 350. The attribute's comment: “lower shriek preserves fibre products”.

Stacks 0DF2. Lower shriek preserves fibre products.

noncomputable instance lowerShriek_preservesPullbacks :
    PreservesLimitsOfShape WalkingCospan (lowerShriek T f)

AlgebraicGeometry.BigEtaleSpaceSite.lowerShriek_preservesEqualizers, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallToBigEtale.lean, line 358. The attribute's comment: “lower shriek preserves equalizers”.

Stacks 0DF2. Lower shriek preserves equalizers.

noncomputable instance lowerShriek_preservesEqualizers :
    PreservesLimitsOfShape WalkingParallelPair (lowerShriek T f)

Declarations registered for the tag:

Tag 0DF3, a lemma

Tag 0DF3 in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.inclusion_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtale.lean, line 73. The attribute's comment: “the morphism of sites”.

Stacks 0DF3. The full inclusion of the spaces-étale site of X into the big étale site of X is a morphism of sites in the reverse direction.

theorem inclusion_isMorphismOfSites :
    (Space.SpacesEtale.inclusion T.fppfSite S T.fppf_mem X).IsMorphismOfSites
      (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) (T.bigEtaleTopology X)

AlgebraicGeometry.BigEtaleSpaceSite.inclusionFunctorIdIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtale.lean, line 96. The attribute's comment: “identification with the identity case of 0DF2”.

Stacks 0DF3. The inclusion of the spaces-étale site of X is canonically the functor of Tag 0DF2 for the identity morphism of X.

noncomputable def inclusionFunctorIdIso :
    inclusionFunctor T (𝟙 X) ≅ Space.SpacesEtale.inclusion T.fppfSite S T.fppf_mem X

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

Stacks 0DF3. The morphism of topoi from the big étale topos of X to its small étale topos, induced by the inclusion of the spaces-étale site as a morphism of sites.

noncomputable def bigToSmallEtaleMorphism :
    MorphismOfTopoi
      (Sheaf (T.bigEtaleTopology X) (Type (u + 1)))
      (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) (Type (u + 1)))

AlgebraicGeometry.BigEtaleSpaceSite.bigToSmall_comp_smallToBig_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtale.lean, line 115. The attribute's comment: “the retraction identity”.

Stacks 0DF3. Composing the morphism of topoi induced by the inclusion with the small-to-big morphism i_X gives the identity on the small étale topos, canonically up to natural isomorphism.

noncomputable def bigToSmall_comp_smallToBig_pushforwardIso :
    ((bigToSmallEtaleMorphism T X).comp (smallToBigEtaleMorphism T (𝟙 X))).pushforward ≅
      𝟭 (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) (Type (u + 1)))

AlgebraicGeometry.BigEtaleSpaceSite.smallToBig_inverseImageIso_bigToSmall_pushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtale.lean, line 136. The attribute's comment: “the inverse-image identification”.

Stacks 0DF3. The inverse image of the small-to-big morphism i_X is the direct image of the big-to-small morphism of sites: both restrict a big étale sheaf to the objects étale over X.

noncomputable def smallToBig_inverseImageIso_bigToSmall_pushforward :
    (smallToBigEtaleMorphism T (𝟙 X)).inverseImage ≅
      (bigToSmallEtaleMorphism T X).pushforward

AlgebraicGeometry.Space.SpacesEtale.hasPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleSite.lean, line 298. The attribute's comment: “fibre products in the small site”.

Stacks 0DF3. The spaces-étale site of X has fibre products: it is the full subcategory of the slice over X cut out by a base-change stable property of morphisms, so a fibre product of algebraic spaces étale over X is again étale over X.

instance hasPullbacks : HasPullbacks (SpacesEtale B S hS X)

AlgebraicGeometry.Space.SpacesEtale.hasTerminal, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleSite.lean, line 320. The attribute's comment: “the final object of the small site”.

Stacks 0DF3. The spaces-étale site of X has a final object, the identity of X.

noncomputable instance hasTerminal : HasTerminal (SpacesEtale B S hS X)

AlgebraicGeometry.Space.SpacesEtale.inclusion_preservesTerminalShape, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleSite.lean, line 344. The attribute's comment: “the inclusion preserves the final object”.

Stacks 0DF3. The final object of the spaces-étale site of X remains final in the slice over X.

noncomputable instance inclusion_preservesTerminalShape :
    PreservesLimitsOfShape (Discrete PEmpty.{1}) (inclusion B S hS X)

AlgebraicGeometry.Space.SpacesEtale.inclusion_preservesPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleSite.lean, line 351. The attribute's comment: “the inclusion preserves fibre products”.

Stacks 0DF3. The inclusion of the spaces-étale site of X into the slice over X preserves fibre products.

instance inclusion_preservesPullbacks :
    PreservesLimitsOfShape WalkingCospan (inclusion B S hS X)

Declarations registered for the tag:

Tag 0DF4, a definition

Tag 0DF4 in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.bigToSmallEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtale.lean, line 105. The attribute's comment: “its pushforward is the restriction to the small étale site”.

Stacks 0DF3. The morphism of topoi from the big étale topos of X to its small étale topos, induced by the inclusion of the spaces-étale site as a morphism of sites.

noncomputable def bigToSmallEtaleMorphism :
    MorphismOfTopoi
      (Sheaf (T.bigEtaleTopology X) (Type (u + 1)))
      (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) (Type (u + 1)))
Tag 0DF5, a lemma

Tag 0DF5 in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.bigEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleMorphism.lean, line 115. The attribute's comment: “the morphism of big étale topoi and its inverse-image formula”. References: SGA 4 IV (4.7), “special case”.

Stacks 0DF5. The morphism of big étale topoi induced by a morphism of algebraic spaces: its direct image is the cocontinuous pushforward along composition with f and its inverse image is the continuous pushforward along the same functor, so sections of the inverse image are given by CategoryTheory.Functor.sheafPushforwardContinuous_obj_obj_obj.

noncomputable def bigEtaleMorphism :
    MorphismOfTopoi
      (Sheaf (T.bigEtaleTopology Y) (Type (u + 1)))
      (Sheaf (T.bigEtaleTopology X) (Type (u + 1)))

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

Stacks 0DF5. The left adjoint of the inverse image of AlgebraicGeometry.BigEtaleSpaceSite.bigEtaleMorphism preserves fibre products.

noncomputable instance bigEtaleLowerShriek_preservesPullbacks :
    PreservesLimitsOfShape WalkingCospan
      ((Over.map f).sheafPullback (Type (u + 1))
        (T.bigEtaleTopology Y) (T.bigEtaleTopology X))

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

Stacks 0DF5. The left adjoint of the inverse image of AlgebraicGeometry.BigEtaleSpaceSite.bigEtaleMorphism preserves equalizers.

noncomputable instance bigEtaleLowerShriek_preservesEqualizers :
    PreservesLimitsOfShape WalkingParallelPair
      ((Over.map f).sheafPullback (Type (u + 1))
        (T.bigEtaleTopology Y) (T.bigEtaleTopology X))

Declarations registered for the tag:

Tag 0DF6, a lemma

Tag 0DF6 in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.smallEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleSquare.lean, line 79. The attribute's comment: “part (2), morphism of small étale topoi”.

Stacks 0DF6, part (2). The morphism of spaces-étale topoi induced by cartesian base change along f.

noncomputable def smallEtaleMorphism :
    MorphismOfTopoi
      (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) (Type (u + 1)))
      (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) (Type (u + 1)))

AlgebraicGeometry.BigEtaleSpaceSite.smallToBig_comp_big_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleSquare.lean, line 88. The attribute's comment: “part (1), factorization of the small-to-big morphism”.

Stacks 0DF6, part (1). The small-to-big morphism i_f agrees with the composite of i_Y and the big étale morphism along f.

noncomputable def smallToBig_comp_big_pushforwardIso :
    (smallToBigEtaleMorphism T f).pushforward ≅
      (smallToBigEtaleMorphism T (𝟙 Y)).pushforward ⋙ (bigEtaleMorphism T f).pushforward

AlgebraicGeometry.BigEtaleSpaceSite.smallBaseChange_comp_inclusionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleSquare.lean, line 138. The attribute's comment: “part (3), commutative square of site functors”.

Stacks 0DF6, part (3). The inclusion of the étale objects commutes with base change in the big slice site, up to the canonical isomorphism of cartesian squares.

noncomputable def smallBaseChange_comp_inclusionIso :
    (Space.spacesBaseChange T.fppfSite S T.fppf_mem f).functor ⋙
        Space.SpacesEtale.inclusion T.fppfSite S T.fppf_mem Y ≅
      Space.SpacesEtale.inclusion T.fppfSite S T.fppf_mem X ⋙ Over.pullback f

AlgebraicGeometry.BigEtaleSpaceSite.smallBaseChange_comp_inclusionIso_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleSquare.lean, line 150. The attribute's comment: “part (3), cartesian projection coherence”.

Stacks 0DF6, part (3). The site-square comparison is the cartesian comparison: its underlying map to the original chart is the projection defining base change.

theorem smallBaseChange_comp_inclusionIso_projection
    (U : Space.SpacesEtale T.fppfSite S T.fppf_mem X) :
    ((smallBaseChange_comp_inclusionIso T f).hom.app U).left ≫ pullback.fst U.1.hom f =
      (Space.spacesBaseChange T.fppfSite S T.fppf_mem f).projection.app U

AlgebraicGeometry.BigEtaleSpaceSite.bigSmallEtale_pushforwardCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleSquare.lean, line 159. The attribute's comment: “part (3), commutative square of topoi”.

Stacks 0DF6, part (3). The square of big and small étale morphisms commutes on direct images.

noncomputable def bigSmallEtale_pushforwardCommIso :
    ((smallEtaleMorphism T f).comp (bigToSmallEtaleMorphism T Y)).pushforward ≅
      ((bigToSmallEtaleMorphism T X).comp (bigEtaleMorphism T f)).pushforward

AlgebraicGeometry.BigEtaleSpaceSite.smallEtale_pushforwardIsoBigFactorization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleSquare.lean, line 199. The attribute's comment: “part (4), factorization through both big topoi”.

Stacks 0DF6, part (4). The small étale direct image factors through the big étale topoi of both Y and X.

noncomputable def smallEtale_pushforwardIsoBigFactorization :
    (smallEtaleMorphism T f).pushforward ≅
      ((bigToSmallEtaleMorphism T X).comp
        ((bigEtaleMorphism T f).comp (smallToBigEtaleMorphism T (𝟙 Y)))).pushforward

AlgebraicGeometry.BigEtaleSpaceSite.smallEtale_pushforwardIsoDirectFactorization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleSquare.lean, line 212. The attribute's comment: “part (4), direct factorization through the big topos”.

Stacks 0DF6, part (4). The small étale direct image factors directly through i_f.

noncomputable def smallEtale_pushforwardIsoDirectFactorization :
    (smallEtaleMorphism T f).pushforward ≅
      ((bigToSmallEtaleMorphism T X).comp (smallToBigEtaleMorphism T f)).pushforward

AlgebraicGeometry.BigEtaleSpaceSite.smallEtale_pushforwardIsoBigFactorization_coherence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleSquare.lean, line 229. The attribute's comment: “part (4), coherence with the topos square”.

Stacks 0DF6, part (4). The factorization through both big topoi is the topos square after inserting the small/big retraction at Y.

theorem smallEtale_pushforwardIsoBigFactorization_coherence
    (F : Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) (Type (u + 1))) :
    (smallEtaleMorphism T f).pushforward.map
        ((bigToSmall_comp_smallToBig_pushforwardIso T Y).inv.app F) ≫
      (bigSmallEtale_pushforwardCommIso T f).hom.app
        ((smallToBigEtaleMorphism T (𝟙 Y)).pushforward.obj F) =
    (smallEtale_pushforwardIsoBigFactorization T f).hom.app F

AlgebraicGeometry.BigEtaleSpaceSite.smallEtale_pushforwardIsoDirectFactorization_coherence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleSquare.lean, line 241. The attribute's comment: “part (4), coherence of the two factorizations”.

Stacks 0DF6, part (4). The direct factorization and the factorization through i_Y are identified by the canonical comparison i_f ≅ f_big ∘ i_Y of part (1).

theorem smallEtale_pushforwardIsoDirectFactorization_coherence
    (F : Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) (Type (u + 1))) :
    (smallEtale_pushforwardIsoDirectFactorization T f).hom.app F ≫
      (bigToSmallEtaleMorphism T X).pushforward.map
        ((smallToBig_comp_big_pushforwardIso T f).hom.app F) =
    (smallEtale_pushforwardIsoBigFactorization T f).hom.app F

Declarations registered for the tag:

Tag 0DF7, a lemma

Tag 0DF7 in the Stacks Project.

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

The direct images of composable morphisms of big étale topoi agree canonically with the direct image of the composite.

def bigEtaleMorphism_comp_pushforwardIso :
    ((bigEtaleMorphism T g).comp (bigEtaleMorphism T f)).pushforward ≅
      (bigEtaleMorphism T (f ≫ g)).pushforward

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

The inverse-image comparison for the big étale topoi is the adjunction mate of the direct-image comparison.

def bigEtaleMorphism_comp_inverseImageIso :
    ((bigEtaleMorphism T g).comp (bigEtaleMorphism T f)).inverseImage ≅
      (bigEtaleMorphism T (f ≫ g)).inverseImage

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

The inverse-image comparison for the small étale topoi is the adjunction mate of the canonical composition comparison for cartesian base change on the spaces-étale sites.

def smallEtaleMorphism_comp_inverseImageIso :
    ((smallEtaleMorphism T g).comp (smallEtaleMorphism T f)).inverseImage ≅
      (smallEtaleMorphism T (f ≫ g)).inverseImage

Declarations registered for the tag:

Tag 0DF8, a lemma

Tag 0DF8 in the Stacks Project.

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

Restriction to the small étale site commutes canonically with big étale direct image across a cartesian square of algebraic spaces.

def smallEtalePushforwardBaseChangeIso :
    (bigEtaleMorphism T f).pushforward ⋙ (smallToBigEtaleMorphism T g).inverseImage ≅
      (smallToBigEtaleMorphism T g').inverseImage ⋙ (smallEtaleMorphism T f').pushforward

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

Big étale inverse image commutes canonically with big étale direct image across a cartesian square of algebraic spaces.

def bigEtalePushforwardBaseChangeIso :
    (bigEtaleMorphism T f).pushforward ⋙ (bigEtaleMorphism T g).inverseImage ≅
      (bigEtaleMorphism T g').inverseImage ⋙ (bigEtaleMorphism T f').pushforward

AlgebraicGeometry.BigEtaleSpaceSite.smallEtaleCartesianIndexIso_projection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/EtaleToposFunctoriality.lean, line 320. The attribute's comment: “projection coherence of the index comparison”.

Projection coherence. The comparison of the two descriptions of the small étale site of X' inside the big étale site of Y is the cartesian comparison: its underlying map, followed by the projection of the fibre product with f, is the projection defining the base change along f'. This is AlgebraicGeometry.BigEtaleSpaceSite.smallBaseChange_comp_inclusionIso_projection across the whole cartesian square.

theorem smallEtaleCartesianIndexIso_projection
    (U : Space.SpacesEtale T.fppfSite S T.fppf_mem X') :
    ((smallEtaleCartesianIndexIso T g' f' f g h).inv.app U).left ≫
        pullback.fst ((inclusionFunctor T g).obj U).hom f =
      (Space.spacesBaseChange T.fppfSite S T.fppf_mem f').projection.app U

AlgebraicGeometry.BigEtaleSpaceSite.sharpCommSqBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/EtaleToposFunctoriality.lean, line 341. The attribute's comment: “structure-map coherence over the cartesian square”.

Structure-map coherence. The structure maps of i_g, f_big, i_{g'} and f'_small are compatible with the comparison of the two composite site functors over the cartesian square: both composite structure maps are pullback of global regular functions along the cartesian projection of the base change. This is AlgebraicGeometry.BigEtaleSpaceSite.sharpCommSq across the whole square.

theorem sharpCommSqBaseChange :
    (restrictAlongSharp T g ≫
        ((inclusionFunctor T g).sheafPushforwardContinuous RingCat.{u + 1}
          (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X')
          (T.bigEtaleTopology X)).map (bigPullbackSharp T f)) ≫
      (Functor.sheafPushforwardContinuousNatTrans
        (smallEtaleCartesianIndexIso T g' f' f g h).symm.hom RingCat.{u + 1}
        (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X')
        (T.bigEtaleTopology Y)).app (bigEtaleRingSheaf T Y) =
    smallBaseChangeSharp T f' ≫
      ((Space.spacesBaseChange T.fppfSite S T.fppf_mem f').functor.sheafPushforwardContinuous
        RingCat.{u + 1} (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X')
        (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y')).map
        (restrictAlongSharp T g')

AlgebraicGeometry.BigEtaleSpaceSite.smallEtaleModulePushforwardBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/EtaleToposFunctoriality.lean, line 371. The attribute's comment: “the sheaf-of-modules form over a cartesian square”.

Restriction to the small étale site commutes canonically with big étale direct image of sheaves of 𝒪-modules across a cartesian square of algebraic spaces: i_g^*(f_{big,*}F) = f'_{small,*}(i_{g'}^*F).

This is the 𝒪-module form of AlgebraicGeometry.BigEtaleSpaceSite.smallEtalePushforwardBaseChangeIso, which states the same square for sheaves of sets.

def smallEtaleModulePushforwardBaseChangeIso :
    bigEtaleModulePushforward.{u, u + 1} T f ⋙ restrictModulesAlong T g ≅
      restrictModulesAlong T g' ⋙ smallEtaleModulePushforward.{u, u + 1} T f'
Tag 0DF9, a remark

Tag 0DF9 in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.restrictSharp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtalePushforwardModules.lean, line 175. The attribute's comment: “item (3), the structure map of the comparison morphism π_X”.

Stacks 0DF9, item (3). The structure map of the comparison morphism π_X: the sections of the direct image of the big étale structure sheaf over an algebraic space étale over X are its own global regular functions, so the structure map is the identity.

def restrictSharp (X : T.Spaces) :
    spacesEtaleRingSheaf T X ⟶
      ((Space.SpacesEtale.inclusion T.fppfSite S T.fppf_mem X).sheafPushforwardContinuous
        RingCat.{u + 1} (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X)
        (T.bigEtaleTopology X)).obj (bigEtaleRingSheaf T X)

AlgebraicGeometry.BigEtaleSpaceSite.bigPullbackSharp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtalePushforwardModules.lean, line 185. The attribute's comment: “item (5), the structure map of the big étale morphism f_big”.

Stacks 0DF9, item (5). The structure map of the big étale morphism f_big: pullback of global regular functions along the projection of the fibre product V ×_X Y to V.

def bigPullbackSharp (f : Y ⟶ X) :
    bigEtaleRingSheaf T X ⟶
      ((Over.pullback f).sheafPushforwardContinuous RingCat.{u + 1}
        (T.bigEtaleTopology X) (T.bigEtaleTopology Y)).obj (bigEtaleRingSheaf T Y)

AlgebraicGeometry.BigEtaleSpaceSite.smallBaseChangeSharp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtalePushforwardModules.lean, line 196. The attribute's comment: “item (4), the structure map of the small étale morphism f_small”.

Stacks 0DF9, item (4). The structure map of the small étale morphism f_small: pullback of global regular functions along the cartesian projection of the base change of an algebraic space étale over X.

def smallBaseChangeSharp (f : Y ⟶ X) :
    spacesEtaleRingSheaf T X ⟶
      ((Space.spacesBaseChange T.fppfSite S T.fppf_mem f).functor.sheafPushforwardContinuous
        RingCat.{u + 1} (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X)
        (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)).obj
        (spacesEtaleRingSheaf T Y)

AlgebraicGeometry.BigEtaleSpaceSite.smallToBigRestrictionStructureIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/EtaleRingedComparison.lean, line 88. The attribute's comment: “case (1): restriction along the inclusion functor”.

Restriction of the big étale structure sheaf of X along the inclusion of the spaces-étale site of Y is the spaces-étale structure sheaf of Y: an object étale over Y has the same ring of global regular functions read in either site, and the restriction maps agree.

noncomputable def smallToBigRestrictionStructureIso (f : Y ⟶ X) :
    ((inclusionFunctor T f).sheafPushforwardContinuous CommRingCat.{u + 1}
        (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
        (T.bigEtaleTopology X)).obj (T.structureSheaf X) ≅
      Space.SpacesEtale.structureSheaf T.fppfSite S T.fppf_mem Y

AlgebraicGeometry.BigEtaleSpaceSite.smallToBigEtaleStructureIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/EtaleRingedComparison.lean, line 101. The attribute's comment: “case (1): the isomorphism i_f⁻¹𝒪 ≅ 𝒪_Y”.

Stacks 0DF9, case (1). The canonical isomorphism from the inverse image along i_f of the big étale structure sheaf of X to the spaces-étale structure sheaf of Y.

noncomputable def smallToBigEtaleStructureIso (f : Y ⟶ X) :
    (inverseImageCommRingFunctor (smallToBigEtaleMorphism T f)).obj
        (bigEtaleRingedTopos T X).O ≅
      (Space.spacesEtaleRingedTopos T.fppfSite S T.fppf_mem Y).O

AlgebraicGeometry.BigEtaleSpaceSite.smallToBigEtaleRingedMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/EtaleRingedComparison.lean, line 113. The attribute's comment: “case (1): i_f as a morphism of ringed topoi”.

Stacks 0DF9, case (1). The morphism i_f from the spaces-étale topos of Y to the big étale topos of X as a morphism of ringed topoi: the structure map is the adjunct of the canonical isomorphism of structure sheaves.

noncomputable def smallToBigEtaleRingedMorphism (f : Y ⟶ X) :
    RingedToposHom (Space.spacesEtaleRingedTopos T.fppfSite S T.fppf_mem Y)
      (bigEtaleRingedTopos T X)

AlgebraicGeometry.BigEtaleSpaceSite.iXEtaleRingedMorphism, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/EtaleRingedComparison.lean, line 131. The attribute's comment: “case (2): i_X as a morphism of ringed topoi”.

Stacks 0DF9, case (2). The morphism i_X as a morphism of ringed topoi: it is the identity-morphism case f = 𝟙 X of i_f.

noncomputable abbrev iXEtaleRingedMorphism (X : T.Spaces) :
    RingedToposHom (Space.spacesEtaleRingedTopos T.fppfSite S T.fppf_mem X)
      (bigEtaleRingedTopos T X)

AlgebraicGeometry.BigEtaleSpaceSite.bigToSmallRestrictionStructureIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/EtaleRingedComparison.lean, line 142. The attribute's comment: “case (3): restriction along the inclusion of the spaces-étale site”.

Restriction of the big étale structure sheaf of X along the inclusion of the spaces-étale site of X is the spaces-étale structure sheaf of X, in the direction needed for the direct image along π_X.

noncomputable def bigToSmallRestrictionStructureIso (X : T.Spaces) :
    Space.SpacesEtale.structureSheaf T.fppfSite S T.fppf_mem X ≅
      ((Space.SpacesEtale.inclusion T.fppfSite S T.fppf_mem X).sheafPushforwardContinuous
          CommRingCat.{u + 1} (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X)
          (T.bigEtaleTopology X)).obj (T.structureSheaf X)

AlgebraicGeometry.BigEtaleSpaceSite.bigToSmallEtaleStructureIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/EtaleRingedComparison.lean, line 155. The attribute's comment: “case (3): the isomorphism 𝒪_X ≅ π_{X,*}𝒪”.

Stacks 0DF9, case (3). The canonical isomorphism from the spaces-étale structure sheaf of X to the direct image along π_X of the big étale structure sheaf of X.

noncomputable def bigToSmallEtaleStructureIso (X : T.Spaces) :
    (Space.spacesEtaleRingedTopos T.fppfSite S T.fppf_mem X).O ≅
      (pushforwardCommRingFunctor (bigToSmallEtaleMorphism T X)).obj
        (bigEtaleRingedTopos T X).O

AlgebraicGeometry.BigEtaleSpaceSite.bigToSmallEtaleRingedMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/EtaleRingedComparison.lean, line 168. The attribute's comment: “case (3): π_X as a morphism of ringed topoi”.

Stacks 0DF9, case (3). The morphism π_X from the big étale topos of X to its spaces-étale topos as a morphism of ringed topoi, with the canonical isomorphism 𝒪_X ≅ π_{X,*}𝒪 as its structure map.

noncomputable def bigToSmallEtaleRingedMorphism (X : T.Spaces) :
    RingedToposHom (bigEtaleRingedTopos T X)
      (Space.spacesEtaleRingedTopos T.fppfSite S T.fppf_mem X)

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.Space.IsEtaleCovering · AlgebraicGeometry.Space.isEtaleCovering_of_isZariskiCovering · AlgebraicGeometry.Space.isEtaleCovering_comp · AlgebraicGeometry.Space.isEtaleCovering_pullback · AlgebraicGeometry.Space.isEtaleCovering_of_isIso · AlgebraicGeometry.Space.exists_isEtaleCovering_refining_isSmoothCovering · AlgebraicGeometry.Space.exists_isEtaleCovering_representable_refining_isSmoothCovering · AlgebraicGeometry.BigEtaleSpaceSite

Section73.5 Smooth topology#

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

Tag 041C, a definition

Tag 041C in the Stacks Project.

AlgebraicGeometry.Space.IsSmoothCovering, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Coverings.lean, line 300.

Stacks 041C. A family of morphisms of algebraic spaces over S with common target is a smooth covering when every member is smooth and the family is jointly surjective on points.

structure IsSmoothCovering {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, X i ⟶ F) : Prop
Tag 0DFA, a lemma

Tag 0DFA in the Stacks Project.

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

Stacks 0DFA, the étale case: an étale covering of algebraic spaces over S is a smooth covering.

theorem isSmoothCovering_of_isEtaleCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : ∀ i, X i ⟶ F}
    (hf : IsEtaleCovering B S hS X f) :
    IsSmoothCovering B S hS X f

AlgebraicGeometry.Space.isSmoothCovering_of_isZariskiCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoveringComparisonTopologies.lean, line 242. The attribute's comment: “Zariski coverings”.

Stacks 0DFA, the Zariski case: a Zariski covering of algebraic spaces over S is a smooth covering, because it is an étale covering by Stacks 0DF1.

theorem isSmoothCovering_of_isZariskiCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : ∀ i, X i ⟶ F}
    (hF : IsAlgebraicSpace B S hS F) (hX : ∀ i, IsAlgebraicSpace B S hS (X i))
    (hf : IsZariskiCovering B S hS I X f) :
    IsSmoothCovering B S hS X f
Tag 041D, a lemma

Tag 041D in the Stacks Project.

AlgebraicGeometry.Space.isSmoothCovering_of_isIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmoothCoverings.lean, line 64. The attribute's comment: “isomorphism”.

Stacks 041D, the isomorphism clause. An isomorphism of algebraic spaces over S, regarded as a family indexed by a point, is a smooth covering.

lemma isSmoothCovering_of_isIso
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X' ⟶ X) [IsIso f]
    (hX : IsAlgebraicSpace B S hS X) :
    IsSmoothCovering B S hS (fun _ : Unit ↦ X') (fun _ ↦ f)

AlgebraicGeometry.Space.isSmoothCovering_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmoothCoverings.lean, line 86. The attribute's comment: “composition”.

Stacks 041D, the composition clause. Composing a smooth covering of an algebraic space over S with a smooth covering of each of its members gives a smooth covering.

theorem isSmoothCovering_comp
    {I : Type v} {J : I → Type w} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, X i ⟶ F)
    (Y : ∀ i, J i → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (g : ∀ i j, Y i j ⟶ X i)
    (hf : IsSmoothCovering B S hS X f)
    (hg : ∀ i, IsSmoothCovering B S hS (Y i) (g i)) :
    IsSmoothCovering B S hS (fun ij : Σ i, J i ↦ Y ij.1 ij.2)
      (fun ij : Σ i, J i ↦ g ij.1 ij.2 ≫ f ij.1)

AlgebraicGeometry.Space.isSmoothCovering_fiberProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmoothCoverings.lean, line 113. The attribute's comment: “base_change”.

Stacks 041D, the base-change clause. The first projections of the fibre products of a smooth covering of an algebraic space over S with a morphism g into its target form a smooth covering of the source of g.

theorem isSmoothCovering_fiberProduct
    {I : Type v} {X X' : AlgebraicSpaces B S hS} (Xi : I → AlgebraicSpaces B S hS)
    (f : ∀ i, Xi i ⟶ X) (g : X' ⟶ X)
    (hf : IsSmoothCovering B S hS (fun i ↦ (Xi i).1) (fun i ↦ (f i).hom)) :
    IsSmoothCovering B S hS (fun i ↦ (AlgebraicSpaces.fiberProduct B S hS g (f i)).1)
      (fun i ↦ pullback.fst g.hom (f i).hom)
Sources
LeanAlgebraicGeometry.Space.IsSmoothCovering · AlgebraicGeometry.Space.isSmoothCovering_of_isEtaleCovering · AlgebraicGeometry.Space.isSmoothCovering_of_isZariskiCovering · AlgebraicGeometry.Space.isSmoothCovering_of_isIso · AlgebraicGeometry.Space.isSmoothCovering_comp · AlgebraicGeometry.Space.isSmoothCovering_fiberProduct

Section73.6 Syntomic topology#

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

Tag 041A, a definition

Tag 041A in the Stacks Project.

AlgebraicGeometry.Space.IsSyntomicCovering, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Coverings.lean, line 242.

Stacks 041A. A family of morphisms of algebraic spaces over S with common target is a syntomic covering when every member is syntomic and the family is jointly surjective on points.

structure IsSyntomicCovering {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, X i ⟶ F) : Prop

AlgebraicGeometry.Space.isSyntomicCovering_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Coverings.lean, line 257. The attribute's comment: “the condition unfolded”.

Stacks 041A. Being a syntomic covering is exactly: the target and all the sources are algebraic spaces, every member of the family is syntomic, and the images of the maps on points exhaust the points of the target.

theorem isSyntomicCovering_iff {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, X i ⟶ F) :
    IsSyntomicCovering B S hS X f ↔
      (IsAlgebraicSpace B S hS F ∧ (∀ i, IsAlgebraicSpace B S hS (X i)) ∧
        (∀ i, IsSyntomic B S hS (f i)) ∧
        Set.univ = ⋃ i, Set.range (pointsMap B S hS (X i) (f i)))
Tag 0DFB, a lemma

Tag 0DFB in the Stacks Project.

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

Stacks 0DFB, the smooth case: a smooth covering of algebraic spaces over S is a syntomic covering.

theorem isSyntomicCovering_of_isSmoothCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : ∀ i, X i ⟶ F}
    (hf : IsSmoothCovering B S hS X f) :
    IsSyntomicCovering B S hS X f

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

Stacks 0DFB, the étale case: an étale covering of algebraic spaces over S is a syntomic covering.

theorem isSyntomicCovering_of_isEtaleCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : ∀ i, X i ⟶ F}
    (hf : IsEtaleCovering B S hS X f) :
    IsSyntomicCovering B S hS X f

AlgebraicGeometry.Space.isSyntomicCovering_of_isZariskiCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoveringComparisonTopologies.lean, line 254. The attribute's comment: “Zariski coverings”.

Stacks 0DFB, the Zariski case: a Zariski covering of algebraic spaces over S is a syntomic covering.

theorem isSyntomicCovering_of_isZariskiCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : ∀ i, X i ⟶ F}
    (hF : IsAlgebraicSpace B S hS F) (hX : ∀ i, IsAlgebraicSpace B S hS (X i))
    (hf : IsZariskiCovering B S hS I X f) :
    IsSyntomicCovering B S hS X f
Tag 041B, a lemma

Tag 041B in the Stacks Project.

AlgebraicGeometry.Space.isSyntomicCovering_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SyntomicCoveringBaseChange.lean, line 84. The attribute's comment: “part (3), base change”.

Stacks 041B, the base-change clause. The first projections of the presheaf fibre products of a syntomic covering of an algebraic space over S with a morphism g into its target form a syntomic covering of the source of g.

theorem isSyntomicCovering_pullback {I : Type v}
    {X X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (g : X' ⟶ X) (hX' : IsAlgebraicSpace B S hS X')
    (Y : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, Y i ⟶ X)
    (h : IsSyntomicCovering B S hS Y f) :
    IsSyntomicCovering B S hS (fun i => pullback g (f i))
      (fun i => pullback.fst g (f i))

AlgebraicGeometry.Space.isSyntomicCovering_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SyntomicCoveringComposition.lean, line 54. The attribute's comment: “part (2), composition”.

Stacks 041B, the composition clause. A syntomic covering of each member of a syntomic covering composes to a syntomic covering of the original algebraic space.

theorem isSyntomicCovering_comp {I : Type v} (J : I → Type w)
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (Xᵢ : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, Xᵢ i ⟶ X)
    (Xᵢⱼ : ∀ i, J i → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (g : ∀ i j, Xᵢⱼ i j ⟶ Xᵢ i)
    (hf : IsSyntomicCovering B S hS Xᵢ f)
    (hg : ∀ i, IsSyntomicCovering B S hS (Xᵢⱼ i) (g i)) :
    IsSyntomicCovering B S hS
      (fun ij : (i : I) × J i => Xᵢⱼ ij.1 ij.2)
      (fun ij => g ij.1 ij.2 ≫ f ij.1)

AlgebraicGeometry.Space.isSyntomicCovering_of_isIso, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SyntomicCoverings.lean, line 46. The attribute's comment: “part (1), isomorphisms”.

Stacks 041B, the isomorphism clause. An isomorphism of algebraic spaces over S, regarded as a family indexed by a point, is a syntomic covering.

lemma isSyntomicCovering_of_isIso
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X' ⟶ X) [IsIso f]
    (hX : IsAlgebraicSpace B S hS X) :
    IsSyntomicCovering B S hS (fun _ : Unit ↦ X') (fun _ ↦ f)
Sources
LeanAlgebraicGeometry.Space.IsSyntomicCovering · AlgebraicGeometry.Space.isSyntomicCovering_iff · AlgebraicGeometry.Space.isSyntomicCovering_of_isSmoothCovering · AlgebraicGeometry.Space.isSyntomicCovering_of_isEtaleCovering · AlgebraicGeometry.Space.isSyntomicCovering_of_isZariskiCovering · AlgebraicGeometry.Space.isSyntomicCovering_pullback · AlgebraicGeometry.Space.isSyntomicCovering_comp · AlgebraicGeometry.Space.isSyntomicCovering_of_isIso

Section73.7 Fppf topology#

Section 73.7 of the Stacks Project, Tag 03Y7. 9 tags here are carried by 27 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03Y8, a definition

Tag 03Y8 in the Stacks Project.

AlgebraicGeometry.Space.IsFppfCovering, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Coverings.lean, line 211.

Stacks 03Y8. A family of morphisms of algebraic spaces over S with common target is an fppf covering when every member is flat and locally of finite presentation and the family is jointly surjective on points.

structure IsFppfCovering {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, X i ⟶ F) : Prop
Tag 0DFC, a lemma

Tag 0DFC in the Stacks Project.

AlgebraicGeometry.Space.isFppfCovering_of_isSyntomicCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoveringComparisonTopologies.lean, line 156. The attribute's comment: “syntomic coverings”.

Stacks 0DFC, the syntomic case: a syntomic covering of algebraic spaces over S is an fppf covering.

theorem isFppfCovering_of_isSyntomicCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : ∀ i, X i ⟶ F}
    (hf : IsSyntomicCovering B S hS X f) :
    IsFppfCovering B S hS X f

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

Stacks 0DFC, the smooth case: a smooth covering of algebraic spaces over S is an fppf covering.

theorem isFppfCovering_of_isSmoothCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : ∀ i, X i ⟶ F}
    (hf : IsSmoothCovering B S hS X f) :
    IsFppfCovering B S hS X f

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

Stacks 0DFC, the étale case: an étale covering of algebraic spaces over S is an fppf covering.

theorem isFppfCovering_of_isEtaleCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : ∀ i, X i ⟶ F}
    (hf : IsEtaleCovering B S hS X f) :
    IsFppfCovering B S hS X f

AlgebraicGeometry.Space.isFppfCovering_of_isZariskiCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoveringComparisonTopologies.lean, line 266. The attribute's comment: “Zariski coverings”.

Stacks 0DFC, the Zariski case: a Zariski covering of algebraic spaces over S is an fppf covering.

theorem isFppfCovering_of_isZariskiCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {f : ∀ i, X i ⟶ F}
    (hF : IsAlgebraicSpace B S hS F) (hX : ∀ i, IsAlgebraicSpace B S hS (X i))
    (hf : IsZariskiCovering B S hS I X f) :
    IsFppfCovering B S hS X f

AlgebraicGeometry.Space.isFppfCovering_yoneda_of_openCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ZariskiCoveringOfOpenCover.lean, line 128. The attribute's comment: “an open cover of an object of the site”.

Stacks 0DFC for an open cover of an object of the big fppf site of S. The family of representables of an open cover of an object of the site is an fppf covering of the representable of that object: it is a Zariski covering by Stacks 041G.

theorem isFppfCovering_yoneda_of_openCover
    {I : Type v} {T : BigFppfOver B S hS} (X : I → BigFppfOver B S hS) (g : ∀ i, X i ⟶ T)
    (hopen : ∀ i, _root_.AlgebraicGeometry.IsOpenImmersion
      ((BigFppfOver.toScheme B S hS).map (g i)))
    (hcov : ∀ x : (BigFppfOver.toScheme B S hS).obj T,
      ∃ i, x ∈ Set.range ((BigFppfOver.toScheme B S hS).map (g i))) :
    IsFppfCovering B S hS (fun i => yoneda.obj (X i)) (fun i => yoneda.map (g i))

AlgebraicGeometry.Space.Topology.precoverage_etale_le_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/CoproductChartPropertyDescent.lean, line 104. The attribute's comment: “étale coverings, at the precoverages”.

The étale precoverage of algebraic spaces over S is contained in the fppf one.

theorem precoverage_etale_le_fppf :
    Topology.precoverage.{u, v} .etale B S hS ≤ Topology.precoverage.{u, v} .fppf B S hS
Tag 03Y9, a lemma

Tag 03Y9 in the Stacks Project.

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

Stacks 03Y9. Pulling an fppf covering of algebraic spaces over S back along a morphism of algebraic spaces gives an fppf covering of the new target: the first projections of the fibre products of Stacks 02X2 form an fppf covering.

theorem isFppfCovering_fibreProduct
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type v} {X X' : AlgebraicSpaces B S hS}
    (Xi : I → AlgebraicSpaces B S hS)
    (f : ∀ i, Xi i ⟶ X) (g : X' ⟶ X)
    (hf : IsFppfCovering B S hS (fun i => (Xi i).1) (fun i => (f i).hom)) :
    IsFppfCovering B S hS
      (fun i => (AlgebraicSpaces.fiberProduct B S hS g (f i)).1)
      (fun i => pullback.fst g.hom (f i).hom)

AlgebraicGeometry.Space.isFppfCovering_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoveringComparison.lean, line 167. The attribute's comment: “composition_cover”.

Stacks 03Y9. Composing an fppf covering of an algebraic space over S with an fppf covering of each of its members gives an fppf covering: flatness and being locally of finite presentation are stable under composition (Stacks 03MN and 03XQ), and a point of the target is hit by a member of the first covering, hence by a member of the covering of that member.

theorem isFppfCovering_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (I : Type v) (J : I → Type w)
    (Xᵢ : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (Xᵢⱼ : ∀ i, J i → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (f : ∀ i, Xᵢ i ⟶ X) (g : ∀ i j, Xᵢⱼ i j ⟶ Xᵢ i)
    (hf : IsFppfCovering B S hS Xᵢ f)
    (hg : ∀ i, IsFppfCovering B S hS (Xᵢⱼ i) (g i)) :
    IsFppfCovering B S hS (fun p : Σ i, J i => Xᵢⱼ p.1 p.2)
      (fun p => g p.1 p.2 ≫ f p.1)

AlgebraicGeometry.Space.isFppfCovering_of_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoveringComparisonTopologies.lean, line 194. The attribute's comment: “isomorphism_cover”.

Stacks 03Y9, the isomorphism clause. An isomorphism of algebraic spaces over S, regarded as a family indexed by a point, is an fppf covering: it is an étale covering by Stacks 041F, hence an fppf covering by Stacks 0DFC.

theorem isFppfCovering_of_isIso
    (X X' : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : X' ⟶ X) [IsIso f]
    (hX : IsAlgebraicSpace B S hS X) :
    IsFppfCovering B S hS (fun _ : PUnit.{v + 1} => X') (fun _ => f)
Tag 042T, a lemma

Tag 042T in the Stacks Project.

AlgebraicGeometry.Space.exists_fppfCovering_scheme_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/FppfCoverings.lean, line 72.

Stacks 042T. An fppf covering of an algebraic space over S admits a refinement by a family of schemes which is again an fppf covering.

theorem exists_fppfCovering_scheme_refinement
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, X i ⟶ F)
    (hf : IsFppfCovering B S hS X f) :
    ∃ (T : I → BigFppfOver B S hS) (h : ∀ i, yoneda.obj (T i) ⟶ X i),
      IsFppfCovering B S hS (fun i => yoneda.obj (T i)) (fun i => h i ≫ f i)
Tag 0469, a lemma

Tag 0469 in the Stacks Project.

AlgebraicGeometry.Space.isLocallySurjective_coproductDesc_of_isFppfCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/FppfCoverings.lean, line 192.

Stacks 0469. The map from the coproduct of an fppf covering family of algebraic spaces over S, taken in the category of fppf sheaves of sets, to its target is surjective as a map of fppf sheaves.

theorem isLocallySurjective_coproductDesc_of_isFppfCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, X i ⟶ F)
    (hf : IsFppfCovering B S hS X f)
    (G : Sheaf (BigFppfOver.topology B S hS) (Type u))
    (ι : ∀ i, (⟨X i, (hf.source_isAlgebraicSpace i).isSheaf⟩ :
      Sheaf (BigFppfOver.topology B S hS) (Type u)) ⟶ G)
    (hG : IsColimit (Cofan.mk G ι)) :
    Sheaf.IsLocallySurjective
      (hG.desc (Cofan.mk
        (⟨F, hf.target_isAlgebraicSpace.isSheaf⟩ :
          Sheaf (BigFppfOver.topology B S hS) (Type u))
        (fun i =>
          (Sheaf.homEquiv (X :=
            (⟨X i, (hf.source_isAlgebraicSpace i).isSheaf⟩ :
              Sheaf (BigFppfOver.topology B S hS) (Type u)))
            (Y :=
            (⟨F, hf.target_isAlgebraicSpace.isSheaf⟩ :
              Sheaf (BigFppfOver.topology B S hS) (Type u)))).symm (f i))))
Tag 0DBV, a definition

Tag 0DBV in the Stacks Project.

AlgebraicGeometry.BigFppfSpaceSite, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfSite.lean, line 115.

Stacks 0DBV. A big fppf site of algebraic spaces over S: the chosen big fppf site of schemes containing S, the category of algebraic spaces over S, and the set-sized system of fppf covering families supplied by Stacks 000X.

structure BigFppfSpaceSite (S : Scheme.{u})
Tag 0DBW, a definition

Tag 0DBW in the Stacks Project.

AlgebraicGeometry.BigFppfSpaceOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfSite.lean, line 210. The attribute's comment: “underlying category”.

Stacks 0DBW. The category underlying the big fppf site of an algebraic space X of the site is the slice of the big fppf category of algebraic spaces at X.

abbrev BigFppfSpaceOver

AlgebraicGeometry.BigFppfSpaceOver.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfSite.lean, line 215. The attribute's comment: “covering families”.

A family over X covers when its underlying family covers in the big fppf site of algebraic spaces.

abbrev BigFppfSpaceOver.IsCovering (E : Covering (BigFppfSpaceOver T X)) : Prop

AlgebraicGeometry.BigFppfSpaceOver.topology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfSite.lean, line 221. The attribute's comment: “localized topology”.

Stacks 0DBW. The big fppf topology of X is the localization at X of the big fppf topology of algebraic spaces over the base scheme.

abbrev BigFppfSpaceOver.topology : GrothendieckTopology (BigFppfSpaceOver T X)
Tag 0DFD, a lemma

Tag 0DFD in the Stacks Project.

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

Stacks 0DFD. The morphism of big fppf topoi induced by a morphism of algebraic spaces: the functor of sites is base change along f, which is continuous with exact pullback.

noncomputable def bigFppfMorphism :
    MorphismOfTopoi
      (Sheaf (BigFppfSpaceOver.topology T Y) (Type (u + 1)))
      (Sheaf (BigFppfSpaceOver.topology T X) (Type (u + 1)))

AlgebraicGeometry.BigFppfSpaceSite.bigFppfMorphism_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfMorphism.lean, line 95. The attribute's comment: “inverse-image functor”.

Stacks 0DFD. The inverse image is naturally restriction along composition with f.

noncomputable def bigFppfMorphism_inverseImageIso :
    (bigFppfMorphism T f).inverseImage ≅
      (Over.map f).sheafPushforwardContinuous (Type (u + 1))
        (BigFppfSpaceOver.topology T Y) (BigFppfSpaceOver.topology T X)

AlgebraicGeometry.BigFppfSpaceSite.bigFppfMorphism_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfMorphism.lean, line 105. The attribute's comment: “equality of the two induced morphisms of topoi”.

Stacks 0DFD. The direct image agrees naturally with the pushforward attached to the cocontinuous composition functor, so the two morphisms of topoi one can attach to f coincide.

noncomputable def bigFppfMorphism_pushforwardIso :
    (bigFppfMorphism T f).pushforward ≅
      (Over.map f).sheafPushforwardCocontinuous (Type (u + 1))
        (BigFppfSpaceOver.topology T Y) (BigFppfSpaceOver.topology T X)

AlgebraicGeometry.BigFppfSpaceSite.bigFppfMorphism_inverseImage_sections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfMorphism.lean, line 114. The attribute's comment: “inverse-image sections”.

Stacks 0DFD. The sections of the inverse image of a sheaf over an object V of the big fppf site of Y are its sections over V composed with f.

noncomputable def bigFppfMorphism_inverseImage_sections
    (G : Sheaf (BigFppfSpaceOver.topology T X) (Type (u + 1))) (V : Over Y) :
    ((bigFppfMorphism T f).inverseImage.obj G).obj.obj (op V) ≃
      G.obj.obj (op ((Over.map f).obj V))

AlgebraicGeometry.BigFppfSpaceSite.bigFppfMorphism_pushforward_sections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfMorphism.lean, line 124. The attribute's comment: “direct-image sections”.

Stacks 0DFD. The sections of the direct image of a sheaf over an object U of the big fppf site of X are its sections over the fibre product of U with Y over X.

noncomputable def bigFppfMorphism_pushforward_sections
    (F : Sheaf (BigFppfSpaceOver.topology T Y) (Type (u + 1))) (U : Over X) :
    ((bigFppfMorphism T f).pushforward.obj F).obj.obj (op U) ≃
      F.obj.obj (op ((Over.pullback f).obj U))

AlgebraicGeometry.BigFppfSpaceSite.bigFppfMorphism_lowerShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfMorphism.lean, line 134. The attribute's comment: “left adjoint to inverse image”.

Stacks 0DFD. The further left adjoint of the inverse image.

noncomputable def bigFppfMorphism_lowerShriek :
    Sheaf (BigFppfSpaceOver.topology T Y) (Type (u + 1)) ⥤
      Sheaf (BigFppfSpaceOver.topology T X) (Type (u + 1))

AlgebraicGeometry.BigFppfSpaceSite.bigFppfMorphism_lowerShriek_adjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfMorphism.lean, line 142. The attribute's comment: “lower-shriek adjunction”.

Stacks 0DFD. Lower shriek is left adjoint to the inverse image.

noncomputable def bigFppfMorphism_lowerShriek_adjunction :
    bigFppfMorphism_lowerShriek T f ⊣ (bigFppfMorphism T f).inverseImage

AlgebraicGeometry.BigFppfSpaceSite.bigFppfMorphism_lowerShriek_preservesPullbacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfMorphism.lean, line 151. The attribute's comment: “lower shriek preserves fibre products”.

Stacks 0DFD. Lower shriek preserves fibre products of big fppf sheaves.

theorem bigFppfMorphism_lowerShriek_preservesPullbacks :
    PreservesLimitsOfShape WalkingCospan (bigFppfMorphism_lowerShriek T f)

AlgebraicGeometry.BigFppfSpaceSite.bigFppfMorphism_lowerShriek_preservesEqualizers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfMorphism.lean, line 158. The attribute's comment: “lower shriek preserves equalizers”.

Stacks 0DFD. Lower shriek preserves equalizers of big fppf sheaves.

theorem bigFppfMorphism_lowerShriek_preservesEqualizers :
    PreservesLimitsOfShape WalkingParallelPair (bigFppfMorphism_lowerShriek T f)

Declarations registered for the tag:

Tag 0DFE, a lemma

Tag 0DFE in the Stacks Project.

AlgebraicGeometry.BigFppfSpaceSite.bigFppfMorphism_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfMorphism.lean, line 170. The attribute's comment: “direct images”.

Stacks 0DFE. The direct images of composable morphisms of big fppf topoi agree canonically with the direct image of the composite.

noncomputable def bigFppfMorphism_comp_pushforwardIso :
    ((bigFppfMorphism T h).comp (bigFppfMorphism T g)).pushforward ≅
      (bigFppfMorphism T (g ≫ h)).pushforward

AlgebraicGeometry.BigFppfSpaceSite.bigFppfMorphism_comp_inverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfMorphism.lean, line 189. The attribute's comment: “inverse images”.

Stacks 0DFE. The inverse-image comparison is the adjunction mate of the direct-image comparison.

noncomputable def bigFppfMorphism_comp_inverseImageIso :
    ((bigFppfMorphism T h).comp (bigFppfMorphism T g)).inverseImage ≅
      (bigFppfMorphism T (g ≫ h)).inverseImage
Sources
LeanAlgebraicGeometry.Space.IsFppfCovering · AlgebraicGeometry.Space.isFppfCovering_of_isSyntomicCovering · AlgebraicGeometry.Space.isFppfCovering_of_isSmoothCovering · AlgebraicGeometry.Space.isFppfCovering_of_isEtaleCovering · AlgebraicGeometry.Space.isFppfCovering_of_isZariskiCovering · AlgebraicGeometry.Space.isFppfCovering_yoneda_of_openCover · AlgebraicGeometry.Space.Topology.precoverage_etale_le_fppf · AlgebraicGeometry.Space.isFppfCovering_fibreProduct

Section73.8 The ph topology#

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

Tag 0DFG, a definition

Tag 0DFG in the Stacks Project.

AlgebraicGeometry.Space.IsPHCovering, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/PhCoverings.lean, line 90.

Stacks 0DFG. A family of morphisms of algebraic spaces over S with common target is a ph covering when every member is locally of finite type and every affine scheme-valued point of the target admits a standard ph covering refining the pullback of the family.

structure IsPHCovering {I : Type v} {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (Xᵢ : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, Xᵢ i ⟶ X) : Prop
Tag 0DFH, a lemma

Tag 0DFH in the Stacks Project.

AlgebraicGeometry.Space.isPHCovering_of_isEtaleCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/EtalePhCoverings.lean, line 207. The attribute's comment: “étale coverings”.

The étale case of Stacks 0DFH. An étale covering of an algebraic space over S is a ph covering of it.

Each member is locally of finite type because it is étale. For an affine scheme-valued point a of the target, the family is base changed along a and each base changed member is replaced by a scheme atlas of it; the resulting family of morphisms of representables is still étale and jointly surjective, so the underlying family of morphisms of schemes is an étale covering of the affine test scheme and is refined by a standard ph covering of it by AlgebraicGeometry.isPHCovering_of_etale. The members of that refinement are affine and of finite type over the test object, hence lie in the site, and the refinement morphisms compose with the atlases and the fibre product projections to refine the original family over a.

theorem isPHCovering_of_isEtaleCovering {I : Type v}
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {f : ∀ i, X i ⟶ F} (hf : IsEtaleCovering B S hS X f) :
    IsPHCovering B S hS X f

AlgebraicGeometry.Space.isPHCovering_of_isFppfCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/FppfPhCoverings.lean, line 57. The attribute's comment: “fppf coverings”.

An fppf covering of an algebraic space over S is a ph covering of it.

theorem isPHCovering_of_isFppfCovering {I : Type v}
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {f : ∀ i, X i ⟶ F} (hf : IsFppfCovering B S hS X f) :
    IsPHCovering B S hS X f

AlgebraicGeometry.Space.isPHCovering_of_isSyntomicCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/FppfPhCoverings.lean, line 119. The attribute's comment: “syntomic coverings”.

A syntomic covering of an algebraic space over S is a ph covering of it.

theorem isPHCovering_of_isSyntomicCovering {I : Type v}
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {f : ∀ i, X i ⟶ F} (hf : IsSyntomicCovering B S hS X f) :
    IsPHCovering B S hS X f

AlgebraicGeometry.Space.isPHCovering_of_isSmoothCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/FppfPhCoverings.lean, line 127. The attribute's comment: “smooth coverings”.

A smooth covering of an algebraic space over S is a ph covering of it.

theorem isPHCovering_of_isSmoothCovering {I : Type v}
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {f : ∀ i, X i ⟶ F} (hf : IsSmoothCovering B S hS X f) :
    IsPHCovering B S hS X f

AlgebraicGeometry.Space.isPHCovering_of_isZariskiCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/FppfPhCoverings.lean, line 136. The attribute's comment: “Zariski coverings”.

A Zariski covering of an algebraic space over S by algebraic spaces is a ph covering of it.

theorem isPHCovering_of_isZariskiCovering {I : Type v}
    {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {f : ∀ i, X i ⟶ F} (hF : IsAlgebraicSpace B S hS F)
    (hX : ∀ i, IsAlgebraicSpace B S hS (X i))
    (hf : IsZariskiCovering B S hS I X f) :
    IsPHCovering B S hS X f
Tag 0DFI, a lemma

Tag 0DFI in the Stacks Project.

AlgebraicGeometry.Space.isPHCovering_of_isProper_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/PhCoveringProperSurjective.lean, line 209.

Stacks 0DFI. A proper surjective morphism of algebraic spaces over S, regarded as a one-member family, is a ph covering.

Over an affine object U of the site the pullback Y ×_X h_U is proper and surjective over h_U, so Chow's lemma over U — in the form AlgebraicGeometry.Space.exists_properSurjective_schemeCover_of_isProper_toAffine — produces a proper surjective morphism of schemes V ⟶ U which factors through that pullback. A finite affine open covering of V is then a standard ph covering of U, and it refines the family pulled back along a through the factorization.

theorem isPHCovering_of_isProper_isSurjective
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X' ⟶ X)
    (hX : IsAlgebraicSpace B S hS X) (hX' : IsAlgebraicSpace B S hS X')
    (hp : IsProper B S hS f) (hs : IsSurjective B S hS f) :
    IsPHCovering B S hS (fun _ : Unit ↦ X') (fun _ ↦ f)
Tag 0DFJ, a lemma

Tag 0DFJ in the Stacks Project.

AlgebraicGeometry.Space.isPHCovering_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/PhCoveringComposition.lean, line 39. The attribute's comment: “composition”.

Ph coverings compose. If {Xᵢ i ⟶ X} is a ph covering of an algebraic space over S and {Xᵢⱼ i j ⟶ Xᵢ i} is a ph covering for every i, then the family of all composites Xᵢⱼ i j ⟶ Xᵢ i ⟶ X, indexed by Σ i, J i, is a ph covering of X.

theorem isPHCovering_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type v} {J : I → Type w}
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (Xᵢ : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, Xᵢ i ⟶ X)
    (Xᵢⱼ : ∀ i, J i → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (g : ∀ i j, Xᵢⱼ i j ⟶ Xᵢ i)
    (hf : IsPHCovering B S hS Xᵢ f)
    (hg : ∀ i, IsPHCovering B S hS (Xᵢⱼ i) (g i)) :
    IsPHCovering B S hS (fun ij : Σ i, J i ↦ Xᵢⱼ ij.1 ij.2)
      (fun ij : Σ i, J i ↦ g ij.1 ij.2 ≫ f ij.1)

AlgebraicGeometry.Space.isPHCovering_of_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/PhCoverings.lean, line 112. The attribute's comment: “ph_covering_of_isomorphism”.

Stacks 0DFJ, the isomorphism clause. An isomorphism of algebraic spaces over S, regarded as a family indexed by a point, is a ph covering: the identity of an affine test scheme is a standard ph covering of it, and it refines the pulled-back family through the inverse isomorphism.

theorem isPHCovering_of_isIso
    {X' X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : X' ⟶ X) [IsIso f]
    (hX : IsAlgebraicSpace B S hS X) :
    IsPHCovering B S hS (fun _ : Unit ↦ X') (fun _ ↦ f)

AlgebraicGeometry.Space.isPHCovering_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/PhCoverings.lean, line 144. The attribute's comment: “ph_covering_base_change”.

Stacks 0DFJ, the base-change clause. The first projections of the fibre products of a ph covering of an algebraic space over S with a morphism g into its target form a ph covering of the source of g: a standard ph refinement of the original family over an affine point a of the new base refines the pulled-back family through the universal property of the fibre product.

theorem isPHCovering_baseChange
    {I : Type v} {X X' : AlgebraicSpaces B S hS} (Xᵢ : I → AlgebraicSpaces B S hS)
    (f : ∀ i, Xᵢ i ⟶ X) (g : X' ⟶ X)
    (hf : IsPHCovering B S hS (fun i ↦ (Xᵢ i).1) (fun i ↦ (f i).hom)) :
    IsPHCovering B S hS (fun i ↦ (AlgebraicSpaces.fiberProduct B S hS g (f i)).1)
      (fun i ↦ pullback.fst g.hom (f i).hom)
Tag 0DFK, a definition

Tag 0DFK in the Stacks Project.

AlgebraicGeometry.BigPHSpaceSite, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhSite.lean, line 99.

Stacks 0DFK. A big ph site of algebraic spaces over S: the chosen big ph site of schemes containing S, the category of algebraic spaces over S, and the set-sized system of ph covering families supplied by Stacks 000X.

structure BigPHSpaceSite (S : Scheme.{u})
Tag 0DFL, a definition

Tag 0DFL in the Stacks Project.

AlgebraicGeometry.BigPHSpaceOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhSite.lean, line 220. The attribute's comment: “underlying category”.

Stacks 0DFL. The category underlying the big ph site of an algebraic space X of the site is the slice of the big ph category of algebraic spaces at X.

abbrev BigPHSpaceOver

AlgebraicGeometry.BigPHSpaceOver.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhSite.lean, line 225. The attribute's comment: “covering families”.

A family over X covers when its underlying family covers in the big ph site of algebraic spaces.

abbrev BigPHSpaceOver.IsCovering (E : Covering (BigPHSpaceOver T X)) : Prop

AlgebraicGeometry.BigPHSpaceOver.topology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhSite.lean, line 231. The attribute's comment: “localized topology”.

Stacks 0DFL. The big ph topology of X is the localization at X of the big ph topology of algebraic spaces over the base scheme.

abbrev BigPHSpaceOver.topology : GrothendieckTopology (BigPHSpaceOver T X)
Tag 0DFM, a lemma

Tag 0DFM in the Stacks Project.

AlgebraicGeometry.Space.isSheaf_of_etale_and_properSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/PhSheafCriterion.lean, line 373. The attribute's comment: “sufficiency: etale descent plus proper-surjective descent imply the ph sheaf condition”.

A presheaf of sets on the big ph site of an algebraic space X of a big ph site of algebraic spaces is a sheaf as soon as it satisfies étale descent and descent along every proper surjective morphism of the site.

theorem isSheaf_of_etale_and_properSurjective (h₁ : IsEtaleSheafOver T X F)
    (h₂ : IsProperSurjectiveSheafOver T X F) :
    Presieve.IsSheaf (BigPHSpaceOver.topology T X) F

AlgebraicGeometry.Space.isEtaleSheafOver_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/PhSheafCriterion.lean, line 436. The attribute's comment: “necessity, etale descent: a ph sheaf satisfies etale descent”.

A sheaf of sets on the big ph site of an algebraic space X of a big ph site of algebraic spaces satisfies étale descent.

theorem isEtaleSheafOver_of_isSheaf (h : Presieve.IsSheaf (BigPHSpaceOver.topology T X) F) :
    IsEtaleSheafOver T X F

AlgebraicGeometry.Space.isProperSurjectiveSheafOver_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/PhSheafCriterion.lean, line 446. The attribute's comment: “necessity, proper-surjective descent: a ph sheaf satisfies descent along every proper surjective morphism of the site”.

A sheaf of sets on the big ph site of an algebraic space X of a big ph site of algebraic spaces satisfies descent along every proper surjective morphism of the site.

theorem isProperSurjectiveSheafOver_of_isSheaf
    (h : Presieve.IsSheaf (BigPHSpaceOver.topology T X) F) :
    IsProperSurjectiveSheafOver T X F

AlgebraicGeometry.Space.isSheaf_iff_isEtaleSheafOver_and_isProperSurjectiveSheafOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/PhSheafCriterion.lean, line 459. The attribute's comment: “the biconditional”.

A presheaf of sets on the big ph site of an algebraic space X of a big ph site of algebraic spaces is a sheaf if and only if it satisfies étale descent and descent along every proper surjective morphism of the site.

theorem isSheaf_iff_isEtaleSheafOver_and_isProperSurjectiveSheafOver :
    Presieve.IsSheaf (BigPHSpaceOver.topology T X) F ↔
      IsEtaleSheafOver T X F ∧ IsProperSurjectiveSheafOver T X F
Tag 0DFN, a lemma

Tag 0DFN in the Stacks Project.

AlgebraicGeometry.BigPHSpaceSite.bigPHMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhMorphism.lean, line 96. The attribute's comment: “the morphism of topoi”. References: SGA 4 IV (4.7), “special case”.

Stacks 0DFN. The morphism of big ph topoi induced by a morphism of algebraic spaces: its direct image is the cocontinuous pushforward along composition with f and its inverse image is the continuous pushforward along the same functor, so sections of the inverse image are given by CategoryTheory.Functor.sheafPushforwardContinuous_obj_obj_obj.

noncomputable def bigPHMorphism :
    MorphismOfTopoi
      (Sheaf (BigPHSpaceOver.topology T Y) (Type (u + 1)))
      (Sheaf (BigPHSpaceOver.topology T X) (Type (u + 1)))

AlgebraicGeometry.BigPHSpaceSite.bigPHMorphismInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhMorphism.lean, line 110. The attribute's comment: “inverse-image formula”.

Stacks 0DFN. The inverse image is restriction along composition with f.

noncomputable def bigPHMorphismInverseImageIso :
    (bigPHMorphism T f).inverseImage ≅
      (Over.map f).sheafPushforwardContinuous (Type (u + 1))
        (BigPHSpaceOver.topology T Y) (BigPHSpaceOver.topology T X)

AlgebraicGeometry.BigPHSpaceSite.bigPHMorphismPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhMorphism.lean, line 120. The attribute's comment: “direct-image formula and agreement of the induced morphisms”.

Stacks 0DFN. The direct image is restriction along base change by f, which is the adjoint comparison of the cocontinuous pushforward with the continuous pushforward along the right adjoint of Over.map f.

noncomputable def bigPHMorphismPushforwardIso :
    (bigPHMorphism T f).pushforward ≅
      (Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
        (BigPHSpaceOver.topology T X) (BigPHSpaceOver.topology T Y)

AlgebraicGeometry.BigPHSpaceSite.bigPHMorphismLowerShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhMorphism.lean, line 129. The attribute's comment: “lower shriek”.

Stacks 0DFN. The left adjoint of the inverse image of AlgebraicGeometry.BigPHSpaceSite.bigPHMorphism.

noncomputable def bigPHMorphismLowerShriek :
    Sheaf (BigPHSpaceOver.topology T Y) (Type (u + 1)) ⥤
      Sheaf (BigPHSpaceOver.topology T X) (Type (u + 1))

AlgebraicGeometry.BigPHSpaceSite.bigPHMorphismLowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhMorphism.lean, line 137. The attribute's comment: “lower-shriek adjunction”.

Stacks 0DFN. Lower shriek is left adjoint to the inverse image.

noncomputable def bigPHMorphismLowerShriekAdjunction :
    bigPHMorphismLowerShriek T f ⊣ (bigPHMorphism T f).inverseImage

AlgebraicGeometry.BigPHSpaceSite.bigPHMorphismLowerShriek_preservesPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhMorphism.lean, line 144. The attribute's comment: “lower shriek preserves fibre products”.

Stacks 0DFN. Lower shriek preserves fibre products.

noncomputable instance bigPHMorphismLowerShriek_preservesPullbacks :
    PreservesLimitsOfShape WalkingCospan (bigPHMorphismLowerShriek T f)

AlgebraicGeometry.BigPHSpaceSite.bigPHMorphismLowerShriek_preservesEqualizers, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhMorphism.lean, line 151. The attribute's comment: “lower shriek preserves equalizers”.

Stacks 0DFN. Lower shriek preserves equalizers.

noncomputable instance bigPHMorphismLowerShriek_preservesEqualizers :
    PreservesLimitsOfShape WalkingParallelPair (bigPHMorphismLowerShriek T f)

Declarations registered for the tag:

Tag 0DFP, a lemma

Tag 0DFP in the Stacks Project.

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

Stacks 0DFP. The direct image of the composite agrees canonically with the composite of the direct images on the big ph topoi, because base change along a composite is the composite of the base changes.

noncomputable def bigPHMorphism_comp_pushforwardIso :
    ((bigPHMorphism T g).comp (bigPHMorphism T f)).pushforward ≅
      (bigPHMorphism T (f ≫ g)).pushforward

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

Stacks 0DFP. The inverse-image comparison is the adjunction mate of the direct-image comparison.

noncomputable def bigPHMorphism_comp_inverseImageIso :
    ((bigPHMorphism T g).comp (bigPHMorphism T f)).inverseImage ≅
      (bigPHMorphism T (f ≫ g)).inverseImage
Tag 0DK6, a lemma

Tag 0DK6 in the Stacks Project.

AlgebraicGeometry.Space.holds_of_affine_of_cechLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/AffineCechCriterion.lean, line 681.

A Čech-local property of objects of the big fppf site over X can be checked on affine objects flat and locally of finite presentation over X.

public theorem holds_of_affine_of_cechLocal
    {S : Scheme.{u}} (T : AlgebraicGeometry.BigFppfSpaceSite S) (X : T.Spaces)
    (P : Over X → Prop)
    (hcech : ∀ (E : Covering (Over X)),
      AlgebraicGeometry.BigFppfSpaceOver.IsCovering T X E →
      (∀ (n : ℕ) (i : Fin (n + 1) → E.2.I₀)
        (c : WidePullbackCone (fun k : Fin (n + 1) => E.2.f (i k))),
        IsLimit c → P c.pt) → P E.1)
    (haffine : ∀ U : Over X,
      AlgebraicGeometry.Space.IsAffineSpace T.schemeSite S T.scheme_mem U.left.1 →
      AlgebraicGeometry.Space.IsFlat T.schemeSite S T.scheme_mem U.hom.hom →
      AlgebraicGeometry.Space.IsLocallyOfFinitePresentation T.schemeSite S T.scheme_mem
        U.hom.hom → P U) :
    P (Over.mk (𝟙 X))
Sources
LeanAlgebraicGeometry.Space.IsPHCovering · AlgebraicGeometry.Space.isPHCovering_of_isEtaleCovering · AlgebraicGeometry.Space.isPHCovering_of_isFppfCovering · AlgebraicGeometry.Space.isPHCovering_of_isSyntomicCovering · AlgebraicGeometry.Space.isPHCovering_of_isSmoothCovering · AlgebraicGeometry.Space.isPHCovering_of_isZariskiCovering · AlgebraicGeometry.Space.isPHCovering_of_isProper_isSurjective · AlgebraicGeometry.Space.isPHCovering_comp

Section73.9 Fpqc topology#

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

Tag 03MQ, a definition

Tag 03MQ in the Stacks Project.

AlgebraicGeometry.Space.IsFpqcCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Coverings.lean, line 177.

Stacks 03MQ. A family of flat morphisms of algebraic spaces over S with common target Y is an fpqc covering when, for every affine object T of the big fppf site of S and every morphism h : T ⟶ Y, there is a finite family of affine objects over T which is an fpqc covering of T and refines the family pulled back along h.

abbrev IsFpqcCovering {I : Type v} {X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : ∀ i, X i ⟶ Y) : Prop
Tag 0DFQ, a lemma

Tag 0DFQ in the Stacks Project.

AlgebraicGeometry.Space.isFpqcCovering_of_isFppfCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoveringComparison.lean, line 246. The attribute's comment: “fppf coverings”.

Stacks 0DFQ, the fppf case: an fppf covering of algebraic spaces over S is an fpqc covering.

theorem isFpqcCovering_of_isFppfCovering
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u)
    (f : ∀ i, X i ⟶ F)
    (hf : IsFppfCovering B S hS X f) :
    IsFpqcCovering B S hS f

AlgebraicGeometry.Space.isFpqcCovering_of_isSyntomicCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoveringComparisonTopologies.lean, line 207. The attribute's comment: “syntomic coverings”.

Stacks 0DFQ, the syntomic case: a syntomic covering of algebraic spaces over S is an fpqc covering.

theorem isFpqcCovering_of_isSyntomicCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, X i ⟶ F)
    (hf : IsSyntomicCovering B S hS X f) :
    IsFpqcCovering B S hS f

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

Stacks 0DFQ, the smooth case: a smooth covering of algebraic spaces over S is an fpqc covering.

theorem isFpqcCovering_of_isSmoothCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, X i ⟶ F)
    (hf : IsSmoothCovering B S hS X f) :
    IsFpqcCovering B S hS f

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

Stacks 0DFQ, the étale case: an étale covering of algebraic spaces over S is an fpqc covering.

theorem isFpqcCovering_of_isEtaleCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, X i ⟶ F)
    (hf : IsEtaleCovering B S hS X f) :
    IsFpqcCovering B S hS f

AlgebraicGeometry.Space.isFpqcCovering_of_isZariskiCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CoveringComparisonTopologies.lean, line 278. The attribute's comment: “Zariski coverings”.

Stacks 0DFQ, the Zariski case: a Zariski covering of algebraic spaces over S is an fpqc covering.

theorem isFpqcCovering_of_isZariskiCovering
    {I : Type v} {F : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (X : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (f : ∀ i, X i ⟶ F)
    (hF : IsAlgebraicSpace B S hS F) (hX : ∀ i, IsAlgebraicSpace B S hS (X i))
    (hf : IsZariskiCovering B S hS I X f) :
    IsFpqcCovering B S hS f

AlgebraicGeometry.Space.Topology.precoverage_etale_le_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/CoproductChartPropertyDescent.lean, line 111. The attribute's comment: “étale coverings, at the precoverages”.

The étale precoverage of algebraic spaces over S is contained in the fpqc one.

theorem precoverage_etale_le_fpqc :
    Topology.precoverage.{u, v} .etale B S hS ≤ Topology.precoverage.{u, v} .fpqc B S hS
Tag 03MR, a lemma

Tag 03MR in the Stacks Project.

AlgebraicGeometry.Space.isFpqcCovering_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FpqcCoveringBaseChange.lean, line 42. The attribute's comment: “part (3): base change”.

Pulling an fpqc covering family of algebraic spaces over S back along a morphism f : X ⟶ Y of algebraic spaces gives an fpqc covering of X: the second projections of the fibre products of Stacks 02X2 form an fpqc covering.

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

AlgebraicGeometry.Space.isFpqcCovering_of_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FpqcCoveringBaseChange.lean, line 59. The attribute's comment: “isomorphism”.

An isomorphism of presheaves on the big fppf site of S, regarded as a family indexed by a point, is an fpqc covering.

theorem isFpqcCovering_of_isIso
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {F G : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (f : F ⟶ G) [IsIso f] :
    IsFpqcCovering B S hS (fun _ : PUnit.{v + 1} => f)

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

Stacks 03MR, the composition clause. Composing an fpqc covering of an algebraic space over S with fpqc coverings of each of its members gives an fpqc covering.

theorem isFpqcCovering_comp
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {I : Type v} {J : I → Type w}
    {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {Xi : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {Xij : (Σ i, J i) → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X)
    (hXi : ∀ i, IsAlgebraicSpace B S hS (Xi i))
    (hXij : ∀ (i : I) (j : J i), IsAlgebraicSpace B S hS (Xij ⟨i, j⟩))
    (f : ∀ i, Xi i ⟶ X)
    (g : ∀ (i : I) (j : J i), Xij ⟨i, j⟩ ⟶ Xi i)
    (hf : IsFpqcCovering B S hS f)
    (hg : ∀ i, IsFpqcCovering B S hS (g i)) :
    IsFpqcCovering B S hS (fun ij : Σ i, J i => g ij.1 ij.2 ≫ f ij.1)
Tag 03MS, a lemma

Tag 03MS in the Stacks Project.

AlgebraicGeometry.Space.isFpqcCovering_iff_pullback_atlas, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FpqcCoveringAtlas.lean, line 78.

A family of morphisms of algebraic spaces over S with target X is an fpqc covering exactly when its pullback along a surjective étale morphism a : U ⟶ X from a scheme in the site is an fpqc covering of U.

theorem isFpqcCovering_iff_pullback_atlas
    {I : Type v} {X : AlgebraicSpaces B S hS} {Xi : I → AlgebraicSpaces B S hS}
    (f : ∀ i, Xi i ⟶ X)
    (U : BigFppfOver B S hS) (a : yoneda.obj U ⟶ X.obj)
    (ha_surj : IsSurjective B S hS a) (ha_etale : IsEtale B S hS a) :
    IsFpqcCovering B S hS (fun i ↦ (f i).hom) ↔
      IsFpqcCovering B S hS (fun i ↦ pullback.fst a (f i).hom)
Tag 0419, a lemma

Tag 0419 in the Stacks Project.

AlgebraicGeometry.Space.exists_fpqc_scheme_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/FpqcCoverings.lean, line 55.

Stacks 0419. Every fpqc covering of an algebraic space over S by algebraic spaces has an fpqc refinement by schemes, with each new member factoring through the corresponding member of the original covering by a relatively étale morphism.

theorem exists_fpqc_scheme_refinement
    {I : Type v} {X : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    {Xᵢ : I → (BigFppfOver B S hS)ᵒᵖ ⥤ Type u}
    (hX : IsAlgebraicSpace B S hS X) (hXᵢ : ∀ i, IsAlgebraicSpace B S hS (Xᵢ i))
    (f : ∀ i, Xᵢ i ⟶ X) (hf : IsFpqcCovering B S hS f) :
    ∃ (T : I → BigFppfOver B S hS) (e : ∀ i, yoneda.obj (T i) ⟶ Xᵢ i),
      (∀ i, (MorphismProperty.inverseImage (@Etale.{u} : MorphismProperty Scheme.{u})
          (BigFppfOver.toScheme B S hS)).presheaf (e i)) ∧
        IsFpqcCovering B S hS (fun i => e i ≫ f i)
Sources
LeanAlgebraicGeometry.Space.IsFpqcCovering · AlgebraicGeometry.Space.isFpqcCovering_of_isFppfCovering · AlgebraicGeometry.Space.isFpqcCovering_of_isSyntomicCovering · AlgebraicGeometry.Space.isFpqcCovering_of_isSmoothCovering · AlgebraicGeometry.Space.isFpqcCovering_of_isEtaleCovering · AlgebraicGeometry.Space.isFpqcCovering_of_isZariskiCovering · AlgebraicGeometry.Space.Topology.precoverage_etale_le_fpqc · AlgebraicGeometry.Space.isFpqcCovering_pullback

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.