35.11 Quasi-coherent modules… to 35.25 Application of fpqc…

Section35.11 Quasi-coherent modules and affines#

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

Tag 0GZU, an equation

Tag 0GZU in the Stacks Project.

AlgebraicGeometry.zariski_affineToBigRingedToposEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/AffineRingedToposEquivalence.lean, line 273. The attribute's comment: “Zariski site”.

Stacks 0GZU, Zariski site. The affine-to-big morphism of ringed topoi over the big Zariski site of S is an equivalence of ringed topoi: its inverse image is an equivalence and its structure morphism is an isomorphism.

public theorem zariski_affineToBigRingedToposEquivalence
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    let f := affineToBigRingedToposHom.{u + 1, u, u + 1, u, w}
      (BigAffineZariski.topology B S hS) (BigZariskiOver.topology B S hS)
      (BigAffineZariski.inclusion B S hS)
      (uliftRingSheaf.{w} (commStructureSheaf S (BigZariskiOver.topology B S hS)
        (Over.post B.inclusion) (BigZariskiOver.structure_isSheaf B S hS)))
    f.toToposHom.inverseImage.IsEquivalence ∧ IsIso f.fSharpInverseImage

AlgebraicGeometry.etale_affineToBigRingedToposEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/AffineRingedToposEquivalence.lean, line 287. The attribute's comment: “étale site”.

Stacks 0GZU, étale site. The affine-to-big morphism of ringed topoi over the big étale site of S is an equivalence of ringed topoi: its inverse image is an equivalence and its structure morphism is an isomorphism.

public theorem etale_affineToBigRingedToposEquivalence
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    let f := affineToBigRingedToposHom.{u + 1, u, u + 1, u, w}
      (BigAffineEtale.topology B S hS) (BigEtaleOver.topology B S hS)
      (BigAffineEtale.inclusion B S hS)
      (uliftRingSheaf.{w} (commStructureSheaf S (BigEtaleOver.topology B S hS)
        (Over.post B.inclusion) (BigEtaleOver.structure_isSheaf B S hS)))
    f.toToposHom.inverseImage.IsEquivalence ∧ IsIso f.fSharpInverseImage

AlgebraicGeometry.smooth_affineToBigRingedToposEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/AffineRingedToposEquivalence.lean, line 301. The attribute's comment: “smooth site”.

Stacks 0GZU, smooth site. The affine-to-big morphism of ringed topoi over the big smooth site of S is an equivalence of ringed topoi: its inverse image is an equivalence and its structure morphism is an isomorphism.

public theorem smooth_affineToBigRingedToposEquivalence
    (B : BigSmoothSite.{u}) (S : Scheme.{u}) (hS : S.size < B.cutoff) :
    let f := affineToBigRingedToposHom.{u + 1, u, u + 1, u, w}
      (BigAffineSmooth.topology B S hS) (BigSmoothOver.topology B S hS)
      (BigAffineSmooth.inclusion B S hS)
      (uliftRingSheaf.{w} (commStructureSheaf S (BigSmoothOver.topology B S hS)
        (Over.post (ObjectProperty.ι _)) (BigSmoothOver.structure_isSheaf B S hS)))
    f.toToposHom.inverseImage.IsEquivalence ∧ IsIso f.fSharpInverseImage

AlgebraicGeometry.syntomic_affineToBigRingedToposEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/AffineRingedToposEquivalence.lean, line 315. The attribute's comment: “syntomic site”.

Stacks 0GZU, syntomic site. The affine-to-big morphism of ringed topoi over the big syntomic site of S is an equivalence of ringed topoi: its inverse image is an equivalence and its structure morphism is an isomorphism.

public theorem syntomic_affineToBigRingedToposEquivalence
    (B : BigSyntomicSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    let f := affineToBigRingedToposHom.{u + 1, u, u + 1, u, w}
      (BigAffineSyntomic.topology B S hS) (BigSyntomicOver.topology B S hS)
      (BigAffineSyntomic.inclusion B S hS)
      (uliftRingSheaf.{w} (commStructureSheaf S (BigSyntomicOver.topology B S hS)
        (Over.post B.inclusion) (BigSyntomicOver.structure_isSheaf B S hS)))
    f.toToposHom.inverseImage.IsEquivalence ∧ IsIso f.fSharpInverseImage

AlgebraicGeometry.fppf_affineToBigRingedToposEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/BigSites/AffineRingedToposEquivalence.lean, line 329. The attribute's comment: “fppf site”.

Stacks 0GZU, fppf site. The affine-to-big morphism of ringed topoi over the big fppf site of S is an equivalence of ringed topoi: its inverse image is an equivalence and its structure morphism is an isomorphism.

public theorem fppf_affineToBigRingedToposEquivalence
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S) :
    let f := affineToBigRingedToposHom.{u + 1, u, u + 1, u, w}
      (BigAffineFppf.topology B S hS) (BigFppfOver.topology B S hS)
      (BigAffineFppf.inclusion B S hS)
      (uliftRingSheaf.{w} (commStructureSheaf S (BigFppfOver.topology B S hS)
        (Over.post B.inclusion) (BigFppfOver.structure_isSheaf B S hS)))
    f.toToposHom.inverseImage.IsEquivalence ∧ IsIso f.fSharpInverseImage

Tag 0GZV, a lemma

Tag 0GZV in the Stacks Project.

AlgebraicGeometry.bigAffineZariski_isIso_restrictionBaseChange_associatedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AffineSiteAssociatedModuleCartesian.lean, line 210. The attribute's comment: “(8) ⇒ (1) on the big affine Zariski category”.

Stacks 0GZV, condition (8) implies condition (1), on (Aff/S)_Zar.

public theorem bigAffineZariski_isIso_restrictionBaseChange_associatedModule
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (G : S.Modules) [G.IsQuasicoherent] {X Y : (BigAffineZariski B S hS)ᵒᵖ} (f : X ⟶ Y) :
    IsIso (Stacks.PresheafOfModules.restrictionBaseChange
      (R := (bigAffineZariskiRingedSite B S hS).O.obj)
      (associatedModulePresheaf S G (bigAffineZariskiToOver B S hS)) f)

AlgebraicGeometry.bigAffineEtale_isIso_restrictionBaseChange_associatedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AffineSiteAssociatedModuleCartesian.lean, line 238. The attribute's comment: “(8) ⇒ (1) on the big affine étale category”.

Stacks 0GZV, condition (8) implies condition (1), on (Aff/S)_étale.

public theorem bigAffineEtale_isIso_restrictionBaseChange_associatedModule
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (G : S.Modules) [G.IsQuasicoherent] {X Y : (BigAffineEtale B S hS)ᵒᵖ} (f : X ⟶ Y) :
    IsIso (Stacks.PresheafOfModules.restrictionBaseChange
      (R := (bigAffineEtaleRingedSite B S hS).O.obj)
      (associatedModulePresheaf S G (bigAffineEtaleToOver B S hS)) f)

AlgebraicGeometry.bigAffineSmooth_isIso_restrictionBaseChange_associatedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AffineSiteAssociatedModuleCartesian.lean, line 266. The attribute's comment: “(8) ⇒ (1) on the big affine smooth category”.

Stacks 0GZV, condition (8) implies condition (1), on (Aff/S)_smooth.

public theorem bigAffineSmooth_isIso_restrictionBaseChange_associatedModule
    (B : BigSmoothSite.{u}) (S : Scheme.{u}) (hS : S.size < B.cutoff)
    (G : S.Modules) [G.IsQuasicoherent] {X Y : (BigAffineSmooth B S hS)ᵒᵖ} (f : X ⟶ Y) :
    IsIso (Stacks.PresheafOfModules.restrictionBaseChange
      (R := (bigAffineSmoothRingedSite B S hS).O.obj)
      (associatedModulePresheaf S G (bigAffineSmoothToOver B S hS)) f)

AlgebraicGeometry.bigAffineSyntomic_isIso_restrictionBaseChange_associatedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AffineSiteAssociatedModuleCartesian.lean, line 294. The attribute's comment: “(8) ⇒ (1) on the big affine syntomic category”.

Stacks 0GZV, condition (8) implies condition (1), on (Aff/S)_syntomic.

public theorem bigAffineSyntomic_isIso_restrictionBaseChange_associatedModule
    (B : BigSyntomicSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (G : S.Modules) [G.IsQuasicoherent] {X Y : (BigAffineSyntomic B S hS)ᵒᵖ} (f : X ⟶ Y) :
    IsIso (Stacks.PresheafOfModules.restrictionBaseChange
      (R := (bigAffineSyntomicRingedSite B S hS).O.obj)
      (associatedModulePresheaf S G (bigAffineSyntomicToOver B S hS)) f)

AlgebraicGeometry.bigAffineFppf_isIso_restrictionBaseChange_associatedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AffineSiteAssociatedModuleCartesian.lean, line 325. The attribute's comment: “(8) ⇒ (1) on the big affine fppf category”.

Stacks 0GZV, condition (8) implies condition (1). The presheaf 𝒢ᵃ of Section 35.8 attached to a quasi-coherent 𝒪_S-module 𝒢 has all its base-change comparisons 𝒢ᵃ(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝒢ᵃ(U) isomorphisms on (Aff/S)_fppf, the category the source states the lemma for.

public theorem bigAffineFppf_isIso_restrictionBaseChange_associatedModule
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (G : S.Modules) [G.IsQuasicoherent] {X Y : (BigAffineFppf B S hS)ᵒᵖ} (f : X ⟶ Y) :
    IsIso (Stacks.PresheafOfModules.restrictionBaseChange
      (R := (bigAffineFppfRingedSite B S hS).O.obj)
      (associatedModulePresheaf S G (bigAffineFppfToOver B S hS)) f)

AlgebraicGeometry.fullyFaithfulBigAffineFppfAssociatedModuleQcoh, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteAssociatedModuleUnique.lean, line 205. The attribute's comment: “(8) at τ = fppf, uniqueness of 𝒢”.

Stacks 0GZV, the uniqueness of 𝒢 in condition (8) at τ = fppf. The functor 𝒢 ↦ 𝒢^a|_{(Aff/S)_fppf} from the quasi-coherent 𝒪_S-modules to the 𝒪_Aff-modules on (Aff/S)_fppf is fully faithful: it is Stacks 0GN7 for the big site followed by the Comparison Lemma for sheaves of modules on the dense subsite of affine objects. No part of Descent, Proposition 03DX is used.

public noncomputable def fullyFaithfulBigAffineFppfAssociatedModuleQcoh :
    (bigAffineFppfAssociatedModuleQcoh B S hS).FullyFaithful

AlgebraicGeometry.bigAffineFppf_iso_of_associatedModuleQcoh_restriction_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteAssociatedModuleUnique.lean, line 214. The attribute's comment: “(8) at τ = fppf, uniqueness of 𝒢”.

Stacks 0GZV, the uniqueness of 𝒢 in condition (8) at τ = fppf, read as a uniqueness statement: two quasi-coherent 𝒪_S-modules whose associated modules have isomorphic restrictions to the big affine fppf site of S are isomorphic.

public theorem bigAffineFppf_iso_of_associatedModuleQcoh_restriction_iso
    (G₁ G₂ : (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory)
    (e : (bigAffineFppfAssociatedModuleQcoh B S hS).obj G₁ ≅
      (bigAffineFppfAssociatedModuleQcoh B S hS).obj G₂) :
    Nonempty (G₁.obj ≅ G₂.obj)

AlgebraicGeometry.bigAffineFppf_isRestrictionOfQuasicoherent_of_isRestrictedAssociatedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteAssociatedModuleUnique.lean, line 249. The attribute's comment: “(8) ⇒ (7) at τ = fppf”.

Stacks 0GZV, (8) ⇒ (7) at τ = fppf. The module on (Sch/S)_fppf that condition (7) asks for is 𝒢^a itself, which is quasi-coherent there by Stacks 03DV (1).

public theorem bigAffineFppf_isRestrictionOfQuasicoherent_of_isRestrictedAssociatedModule
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineFppfRingedSite B S hS).O))
    (hF : BigAffineFppf.IsRestrictedAssociatedModule B S hS F) :
    BigAffineFppf.IsRestrictionOfQuasicoherent B S hS F

AlgebraicGeometry.bigAffineFppf_isRestrictedAssociatedModule_of_isRestrictionOfQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteAssociatedModuleUnique.lean, line 266. The attribute's comment: “(7) ⇒ (8) at τ = fppf, existence and uniqueness of 𝒢”.

Stacks 0GZV, (7) ⇒ (8) at τ = fppf, with the uniqueness of 𝒢 included. The module 𝓜 on (Sch/S)_fppf given by condition (7) is quasi-coherent, hence isomorphic to 𝒢^a for a quasi-coherent 𝒪_S-module 𝒢 by the essential surjectivity half of Descent, Proposition 03DX (1) at τ = fppf; restricting that isomorphism to the affine objects gives 𝓕 ≅ 𝒢^a|_{(Aff/S)_fppf}, and 𝒢 is unique up to isomorphism by AlgebraicGeometry.fullyFaithfulBigAffineFppfAssociatedModuleQcoh.

public theorem bigAffineFppf_isRestrictedAssociatedModule_of_isRestrictionOfQuasicoherent
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineFppfRingedSite B S hS).O))
    (hF : BigAffineFppf.IsRestrictionOfQuasicoherent B S hS F) :
    BigAffineFppf.IsRestrictedAssociatedModule B S hS F

AlgebraicGeometry.bigAffineFppf_isRestrictionOfQuasicoherent_iff_isRestrictedAssociatedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteAssociatedModuleUnique.lean, line 280. The attribute's comment: “(7) ⇔ (8) at τ = fppf”.

Stacks 0GZV, conditions (7) and (8) are equivalent at τ = fppf, which is how the source reads them off each other from Descent, Proposition 03DX.

public theorem bigAffineFppf_isRestrictionOfQuasicoherent_iff_isRestrictedAssociatedModule
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineFppfRingedSite B S hS).O)) :
    BigAffineFppf.IsRestrictionOfQuasicoherent B S hS F ↔
      BigAffineFppf.IsRestrictedAssociatedModule B S hS F

AlgebraicGeometry.bigAffineFppf_isSheaf_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteCartesianSheaf.lean, line 195. The attribute's comment: “(1) ⇒ the sheaf conjunct of (6), at τ = fppf”.

Stacks 0GZV, condition (1) implies the sheaf conjunct of condition (6). A presheaf of 𝒪_Aff-modules on (Aff/S)_fppf all of whose base-change comparisons 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms satisfies the fppf sheaf axiom. The coverings of (Aff/S)_fppf are finite flat coverings of affine schemes, so this is flat descent of modules, Stacks 023M.

public theorem bigAffineFppf_isSheaf_of_cartesian
    (M : PresheafOfModules.{max m u}
      ((bigAffineFppfRingedSite B S hS).O.obj ⋙ forget₂ CommRingCat RingCat))
    (hM : ∀ {X Y : (BigAffineFppf B S hS)ᵒᵖ} (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, m} M f)) :
    Presheaf.IsSheaf (BigAffineFppf.topology B S hS) M.presheaf

AlgebraicGeometry.bigAffineZariski_isSheaf_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteCartesianSheaf.lean, line 232. The attribute's comment: “(1) ⇒ the sheaf conjunct of (2), at τ = Zariski”.

Stacks 0GZV, condition (1) implies the sheaf conjunct of condition (2). A presheaf of 𝒪_Aff-modules on (Aff/S)_Zar all of whose base-change comparisons 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms satisfies the Zariski sheaf axiom. The coverings of (Aff/S)_Zar are finite flat coverings of affine schemes, so this is flat descent of modules, Stacks 023M.

public theorem bigAffineZariski_isSheaf_of_cartesian
    (M : PresheafOfModules.{max m u}
      ((bigAffineZariskiRingedSite B S hS).O.obj ⋙ forget₂ CommRingCat RingCat))
    (hM : ∀ {X Y : (BigAffineZariski B S hS)ᵒᵖ} (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, m} M f)) :
    Presheaf.IsSheaf (BigAffineZariski.topology B S hS) M.presheaf

AlgebraicGeometry.bigAffineEtale_isSheaf_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteCartesianSheaf.lean, line 269. The attribute's comment: “(1) ⇒ the sheaf conjunct of (3), at τ = étale”.

Stacks 0GZV, condition (1) implies the sheaf conjunct of condition (3). A presheaf of 𝒪_Aff-modules on (Aff/S)_étale all of whose base-change comparisons 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms satisfies the étale sheaf axiom. The coverings of (Aff/S)_étale are finite flat coverings of affine schemes, so this is flat descent of modules, Stacks 023M.

public theorem bigAffineEtale_isSheaf_of_cartesian
    (M : PresheafOfModules.{max m u}
      ((bigAffineEtaleRingedSite B S hS).O.obj ⋙ forget₂ CommRingCat RingCat))
    (hM : ∀ {X Y : (BigAffineEtale B S hS)ᵒᵖ} (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, m} M f)) :
    Presheaf.IsSheaf (BigAffineEtale.topology B S hS) M.presheaf

AlgebraicGeometry.bigAffineSmooth_isSheaf_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteCartesianSheaf.lean, line 306. The attribute's comment: “(1) ⇒ the sheaf conjunct of (4), at τ = smooth”.

Stacks 0GZV, condition (1) implies the sheaf conjunct of condition (4). A presheaf of 𝒪_Aff-modules on (Aff/S)_smooth all of whose base-change comparisons 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms satisfies the smooth sheaf axiom. The coverings of (Aff/S)_smooth are finite flat coverings of affine schemes, so this is flat descent of modules, Stacks 023M.

public theorem bigAffineSmooth_isSheaf_of_cartesian
    (M : PresheafOfModules.{max m u}
      ((bigAffineSmoothRingedSite B S hS).O.obj ⋙ forget₂ CommRingCat RingCat))
    (hM : ∀ {X Y : (BigAffineSmooth B S hS)ᵒᵖ} (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, m} M f)) :
    Presheaf.IsSheaf (BigAffineSmooth.topology B S hS) M.presheaf

AlgebraicGeometry.bigAffineSyntomic_isSheaf_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteCartesianSheaf.lean, line 347. The attribute's comment: “(1) ⇒ the sheaf conjunct of (5), at τ = syntomic”.

Stacks 0GZV, condition (1) implies the sheaf conjunct of condition (5). A presheaf of 𝒪_Aff-modules on (Aff/S)_syntomic all of whose base-change comparisons 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms satisfies the syntomic sheaf axiom. The coverings of (Aff/S)_syntomic are finite flat coverings of affine schemes, so this is flat descent of modules, Stacks 023M.

public theorem bigAffineSyntomic_isSheaf_of_cartesian
    (M : PresheafOfModules.{max m u}
      ((bigAffineSyntomicRingedSite B S hS).O.obj ⋙ forget₂ CommRingCat RingCat))
    (hM : ∀ {X Y : (BigAffineSyntomic B S hS)ᵒᵖ} (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, m} M f)) :
    Presheaf.IsSheaf (BigAffineSyntomic.topology B S hS) M.presheaf

AlgebraicGeometry.fullyFaithfulBigAffineAssociatedModuleQcohOf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteCoarserAssociatedModule.lean, line 351. The attribute's comment: “(8) at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, uniqueness of 𝒢”.

Stacks 0GZV, the uniqueness of 𝒢 in condition (8), at every τ. The functor 𝒢 ↦ 𝒢^a|_{(Aff/S)_τ} from the quasi-coherent 𝒪_S-modules to the 𝒪_Aff-modules on (Aff/S)_τ is fully faithful: it is Stacks 0GN7 for the big τ-site followed by the Comparison Lemma for sheaves of modules on the dense subsite of affine objects. No part of Descent, Proposition 03DX is used.

public noncomputable def fullyFaithfulBigAffineAssociatedModuleQcohOf (τ : SiteKind) :
    (bigAffineAssociatedModuleQcohOf B S hS τ).FullyFaithful

AlgebraicGeometry.bigAffine_iso_of_associatedModuleQcohOf_restriction_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteCoarserAssociatedModule.lean, line 360. The attribute's comment: “(8) at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, uniqueness of 𝒢”.

Stacks 0GZV, the uniqueness of 𝒢 in condition (8) at every τ, read as a uniqueness statement: two quasi-coherent 𝒪_S-modules whose associated modules have isomorphic restrictions to (Aff/S)_τ are isomorphic.

public theorem bigAffine_iso_of_associatedModuleQcohOf_restriction_iso (τ : SiteKind)
    (G₁ G₂ : (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory)
    (e : (bigAffineAssociatedModuleQcohOf B S hS τ).obj G₁ ≅
      (bigAffineAssociatedModuleQcohOf B S hS τ).obj G₂) :
    Nonempty (G₁.obj ≅ G₂.obj)

AlgebraicGeometry.bigAffine_isRestrictionOfQuasicoherentOf_of_isRestrictedAssociatedModuleOf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteCoarserAssociatedModule.lean, line 411. The attribute's comment: “(8) ⇒ (7) at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}”.

Stacks 0GZV, (8) ⇒ (7) at every τ. The module on (Sch/S)_τ that condition (7) asks for is 𝒢^a itself, which is quasi-coherent there by Stacks 03DV (1).

public theorem bigAffine_isRestrictionOfQuasicoherentOf_of_isRestrictedAssociatedModuleOf
    (τ : SiteKind) (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineRingedSiteOf B S hS τ).O))
    (hF : BigAffineFppf.IsRestrictedAssociatedModuleOf B S hS τ F) :
    BigAffineFppf.IsRestrictionOfQuasicoherentOf B S hS τ F

AlgebraicGeometry.bigAffine_isRestrictionOfQuasicoherentOf_of_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteCoarserAssociatedModule.lean, line 429. The attribute's comment: “(1) ⇒ (7) at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}”.

Stacks 0GZV, (1) ⇒ (7) at every τ. A sheaf of 𝒪_Aff-modules on (Aff/S)_τ all of whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms corresponds, under the equivalence of ringed topoi of Stacks 0GZU, to a quasi-coherent module on (Sch/S)_τ.

The three inputs are the quasi-coherence conjunct of condition (2)–(6) at τ; the existence of an ambient lift, by the Comparison Lemma at τ; and the quasi-coherence of that lift, by the reflection of quasi-coherence along the dense subsite.

public theorem bigAffine_isRestrictionOfQuasicoherentOf_of_canonicalMap_isIso (τ : SiteKind)
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineRingedSiteOf B S hS τ).O))
    (h : ∀ ⦃U V : BigAffineFppf B S hS⦄ (f : U ⟶ V),
      IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineRingedSiteOf B S hS τ) F f)) :
    BigAffineFppf.IsRestrictionOfQuasicoherentOf B S hS τ F

AlgebraicGeometry.bigAffine_isIso_canonicalMapOf_of_isRestrictionOfQuasicoherentOf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteCoarserAssociatedModule.lean, line 445. The attribute's comment: “(7) ⇒ (1) at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}”.

Stacks 0GZV, (7) ⇒ (1) at every τ. The restriction to (Aff/S)_τ of the quasi-coherent module given by condition (7) is quasi-coherent, hence cartesian by Stacks 0H04.

public theorem bigAffine_isIso_canonicalMapOf_of_isRestrictionOfQuasicoherentOf (τ : SiteKind)
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineRingedSiteOf B S hS τ).O))
    (hF : BigAffineFppf.IsRestrictionOfQuasicoherentOf B S hS τ F)
    ⦃U V : BigAffineFppf B S hS⦄ (f : U ⟶ V) :
    IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineRingedSiteOf B S hS τ) F f)

AlgebraicGeometry.bigAffine_isRestrictedAssociatedModuleOf_of_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteCoarserAssociatedModule.lean, line 466. The attribute's comment: “(1) ⇒ (8) at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, existence and uniqueness of 𝒢”.

Stacks 0GZV, (1) ⇒ (8) at every τ, with the uniqueness of 𝒢 included.

A cartesian sheaf of modules on (Aff/S)_τ satisfies the fppf sheaf axiom, so it is a sheaf of modules on (Aff/S)_fppf with the same underlying presheaf, where (1) ⇒ (8) is proved as AlgebraicGeometry.bigAffineFppf_isRestrictedAssociatedModule_of_canonicalMap_isIso. Reading the resulting isomorphism back for τ and applying Stacks 0GNE to its right-hand side gives condition (8) at τ; the uniqueness is AlgebraicGeometry.fullyFaithfulBigAffineAssociatedModuleQcohOf.

public theorem bigAffine_isRestrictedAssociatedModuleOf_of_canonicalMap_isIso (τ : SiteKind)
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineRingedSiteOf B S hS τ).O))
    (h : ∀ ⦃U V : BigAffineFppf B S hS⦄ (f : U ⟶ V),
      IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineRingedSiteOf B S hS τ) F f)) :
    BigAffineFppf.IsRestrictedAssociatedModuleOf B S hS τ F

AlgebraicGeometry.bigAffine_isRestrictedAssociatedModuleOf_of_isRestrictionOfQuasicoherentOf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteCoarserAssociatedModule.lean, line 487. The attribute's comment: “(7) ⇒ (8) at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, existence and uniqueness of 𝒢”.

Stacks 0GZV, (7) ⇒ (8) at every τ, with the uniqueness of 𝒢 included. The route is (7) ⇒ (1) ⇒ (8); in particular clause (1) of Descent, Proposition 03DX at τ is not used.

public theorem bigAffine_isRestrictedAssociatedModuleOf_of_isRestrictionOfQuasicoherentOf
    (τ : SiteKind) (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineRingedSiteOf B S hS τ).O))
    (hF : BigAffineFppf.IsRestrictionOfQuasicoherentOf B S hS τ F) :
    BigAffineFppf.IsRestrictedAssociatedModuleOf B S hS τ F

AlgebraicGeometry.bigAffine_isRestrictionOfQuasicoherentOf_iff_isRestrictedAssociatedModuleOf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteCoarserAssociatedModule.lean, line 499. The attribute's comment: “(7) ⇔ (8) at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}”.

Stacks 0GZV, conditions (7) and (8) are equivalent, at every τ ∈ {Zariski, étale, smooth, syntomic, fppf}, which is how the source reads them off each other from Descent, Proposition 03DX.

public theorem bigAffine_isRestrictionOfQuasicoherentOf_iff_isRestrictedAssociatedModuleOf
    (τ : SiteKind) (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineRingedSiteOf B S hS τ).O)) :
    BigAffineFppf.IsRestrictionOfQuasicoherentOf B S hS τ F ↔
      BigAffineFppf.IsRestrictedAssociatedModuleOf B S hS τ F

AlgebraicGeometry.bigAffineFppf_isRestrictionOfQuasicoherent_of_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteModuleComparisonLemma.lean, line 142. The attribute's comment: “(1) ⇒ (7) at τ = fppf”.

Stacks 0GZV, (1) ⇒ (7) at τ = fppf. A sheaf of 𝒪_Aff-modules on (Aff/S)_fppf all of whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms corresponds, under the equivalence of ringed topoi of Stacks 0GZU, to a quasi-coherent module on (Sch/S)_fppf.

The three inputs are condition (6), by AlgebraicGeometry.bigAffineFppf_isQuasicoherentOnSite_of_canonicalMap_isIso; the existence of an ambient lift, by AlgebraicGeometry.bigAffineFppf_exists_moduleLift; and the quasi-coherence of that lift, by AlgebraicGeometry.bigAffineFppf_isQuasicoherentOnSite_reflect.

public theorem bigAffineFppf_isRestrictionOfQuasicoherent_of_canonicalMap_isIso
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineFppfRingedSite B S hS).O))
    (h : ∀ ⦃U V : BigAffineFppf B S hS⦄ (f : U ⟶ V),
      IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineFppfRingedSite B S hS) F f)) :
    BigAffineFppf.IsRestrictionOfQuasicoherent B S hS F

AlgebraicGeometry.bigAffineFppf_isRestrictedAssociatedModule_of_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteModuleComparisonLemma.lean, line 161. The attribute's comment: “(1) ⇒ (8) at τ = fppf, existence and uniqueness of 𝒢”.

Stacks 0GZV, (1) ⇒ (8) at τ = fppf, with the uniqueness of 𝒢 included. A sheaf of 𝒪_Aff-modules on (Aff/S)_fppf all of whose base-change maps are isomorphisms is the restriction to the affine objects of the associated module 𝒢^a of a quasi-coherent 𝒪_S-module 𝒢, unique up to isomorphism.

This is (1) ⇒ (7) followed by the equivalence of conditions (7) and (8), AlgebraicGeometry.bigAffineFppf_isRestrictionOfQuasicoherent_iff_isRestrictedAssociatedModule.

public theorem bigAffineFppf_isRestrictedAssociatedModule_of_canonicalMap_isIso
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineFppfRingedSite B S hS).O))
    (h : ∀ ⦃U V : BigAffineFppf B S hS⦄ (f : U ⟶ V),
      IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineFppfRingedSite B S hS) F f)) :
    BigAffineFppf.IsRestrictedAssociatedModule B S hS F

AlgebraicGeometry.bigAffineZariski_isSheaf_and_isQuasicoherentOnSite_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSitePresheafConditions.lean, line 66. The attribute's comment: “(1) ⇒ (2) in full, for a presheaf of modules”.

Stacks 0GZV, condition (1) implies condition (2) in full. A presheaf of 𝒪_Aff-modules on (Aff/S)_Zar all of whose base-change comparisons 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms satisfies the Zariski sheaf axiom and is quasi-coherent on the ringed site ((Aff/S)_Zar, 𝒪_Aff).

public theorem bigAffineZariski_isSheaf_and_isQuasicoherentOnSite_of_cartesian
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : PresheafOfModules.{u}
      ((bigAffineZariskiRingedSite B S hS).O.obj ⋙ forget₂ CommRingCat RingCat))
    (hM : ∀ {X Y : (BigAffineZariski B S hS)ᵒᵖ} (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, u} M f)) :
    ∃ hsheaf : Presheaf.IsSheaf (BigAffineZariski.topology B S hS) M.presheaf,
      (⟨M, hsheaf⟩ : SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (bigAffineZariskiRingedSite B S hS).O)).IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineEtale_isSheaf_and_isQuasicoherentOnSite_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSitePresheafConditions.lean, line 84. The attribute's comment: “(1) ⇒ (3) in full, for a presheaf of modules”.

Stacks 0GZV, condition (1) implies condition (3) in full. A presheaf of 𝒪_Aff-modules on (Aff/S)_étale all of whose base-change comparisons 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms satisfies the étale sheaf axiom and is quasi-coherent on the ringed site ((Aff/S)_étale, 𝒪_Aff).

public theorem bigAffineEtale_isSheaf_and_isQuasicoherentOnSite_of_cartesian
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : PresheafOfModules.{u}
      ((bigAffineEtaleRingedSite B S hS).O.obj ⋙ forget₂ CommRingCat RingCat))
    (hM : ∀ {X Y : (BigAffineEtale B S hS)ᵒᵖ} (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, u} M f)) :
    ∃ hsheaf : Presheaf.IsSheaf (BigAffineEtale.topology B S hS) M.presheaf,
      (⟨M, hsheaf⟩ : SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (bigAffineEtaleRingedSite B S hS).O)).IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineSmooth_isSheaf_and_isQuasicoherentOnSite_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSitePresheafConditions.lean, line 102. The attribute's comment: “(1) ⇒ (4) in full, for a presheaf of modules”.

Stacks 0GZV, condition (1) implies condition (4) in full. A presheaf of 𝒪_Aff-modules on (Aff/S)_smooth all of whose base-change comparisons 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms satisfies the smooth sheaf axiom and is quasi-coherent on the ringed site ((Aff/S)_smooth, 𝒪_Aff).

public theorem bigAffineSmooth_isSheaf_and_isQuasicoherentOnSite_of_cartesian
    (B : BigSmoothSite.{u}) (S : Scheme.{u}) (hS : S.size < B.cutoff)
    (M : PresheafOfModules.{u}
      ((bigAffineSmoothRingedSite B S hS).O.obj ⋙ forget₂ CommRingCat RingCat))
    (hM : ∀ {X Y : (BigAffineSmooth B S hS)ᵒᵖ} (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, u} M f)) :
    ∃ hsheaf : Presheaf.IsSheaf (BigAffineSmooth.topology B S hS) M.presheaf,
      (⟨M, hsheaf⟩ : SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (bigAffineSmoothRingedSite B S hS).O)).IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineSyntomic_isSheaf_and_isQuasicoherentOnSite_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSitePresheafConditions.lean, line 120. The attribute's comment: “(1) ⇒ (5) in full, for a presheaf of modules”.

Stacks 0GZV, condition (1) implies condition (5) in full. A presheaf of 𝒪_Aff-modules on (Aff/S)_syntomic all of whose base-change comparisons 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms satisfies the syntomic sheaf axiom and is quasi-coherent on the ringed site ((Aff/S)_syntomic, 𝒪_Aff).

public theorem bigAffineSyntomic_isSheaf_and_isQuasicoherentOnSite_of_cartesian
    (B : BigSyntomicSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : PresheafOfModules.{u}
      ((bigAffineSyntomicRingedSite B S hS).O.obj ⋙ forget₂ CommRingCat RingCat))
    (hM : ∀ {X Y : (BigAffineSyntomic B S hS)ᵒᵖ} (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, u} M f)) :
    ∃ hsheaf : Presheaf.IsSheaf (BigAffineSyntomic.topology B S hS) M.presheaf,
      (⟨M, hsheaf⟩ : SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (bigAffineSyntomicRingedSite B S hS).O)).IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineFppf_isSheaf_and_isQuasicoherentOnSite_of_cartesian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSitePresheafConditions.lean, line 138. The attribute's comment: “(1) ⇒ (6) in full, for a presheaf of modules”.

Stacks 0GZV, condition (1) implies condition (6) in full. A presheaf of 𝒪_Aff-modules on (Aff/S)_fppf all of whose base-change comparisons 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms satisfies the fppf sheaf axiom and is quasi-coherent on the ringed site ((Aff/S)_fppf, 𝒪_Aff).

public theorem bigAffineFppf_isSheaf_and_isQuasicoherentOnSite_of_cartesian
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : PresheafOfModules.{u}
      ((bigAffineFppfRingedSite B S hS).O.obj ⋙ forget₂ CommRingCat RingCat))
    (hM : ∀ {X Y : (BigAffineFppf B S hS)ᵒᵖ} (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, u} M f)) :
    ∃ hsheaf : Presheaf.IsSheaf (BigAffineFppf.topology B S hS) M.presheaf,
      (⟨M, hsheaf⟩ : SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (bigAffineFppfRingedSite B S hS).O)).IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineFppf_isIso_canonicalMap_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteQuasicoherentCartesian.lean, line 302. The attribute's comment: “(6) ⇒ (1), from the quasi-coherence conjunct of (6)”.

Stacks 0GZV, condition (6) implies condition (1). A sheaf of 𝒪_Aff-modules on (Aff/S)_fppf which is quasi-coherent on the ringed site ((Aff/S)_fppf, 𝒪_Aff) has all its base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) isomorphisms.

theorem bigAffineFppf_isIso_canonicalMap_of_isQuasicoherentOnSite
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineFppfRingedSite B S hS).O))
    (hM : M.IsQuasicoherentOnSite) {U V : BigAffineFppf B S hS} (f : U ⟶ V) :
    IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineFppfRingedSite B S hS) M f)

AlgebraicGeometry.bigAffineZariski_isIso_canonicalMap_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteQuasicoherentCartesian.lean, line 372. The attribute's comment: “(2) ⇒ (1), from the quasi-coherence conjunct of (2)”.

Stacks 0GZV, condition (2) implies condition (1). A sheaf of 𝒪_Aff-modules on (Aff/S)_Zar which is quasi-coherent on the ringed site ((Aff/S)_Zar, 𝒪_Aff) has all its base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) isomorphisms.

theorem bigAffineZariski_isIso_canonicalMap_of_isQuasicoherentOnSite
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineZariskiRingedSite B S hS).O))
    (hM : M.IsQuasicoherentOnSite) {U V : BigAffineZariski B S hS} (f : U ⟶ V) :
    IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineZariskiRingedSite B S hS) M f)

AlgebraicGeometry.bigAffineEtale_isIso_canonicalMap_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteQuasicoherentCartesian.lean, line 390. The attribute's comment: “(3) ⇒ (1), from the quasi-coherence conjunct of (3)”.

Stacks 0GZV, condition (3) implies condition (1). A sheaf of 𝒪_Aff-modules on (Aff/S)_étale which is quasi-coherent on the ringed site ((Aff/S)_étale, 𝒪_Aff) has all its base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) isomorphisms.

theorem bigAffineEtale_isIso_canonicalMap_of_isQuasicoherentOnSite
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineEtaleRingedSite B S hS).O))
    (hM : M.IsQuasicoherentOnSite) {U V : BigAffineEtale B S hS} (f : U ⟶ V) :
    IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineEtaleRingedSite B S hS) M f)

AlgebraicGeometry.bigAffineSmooth_isIso_canonicalMap_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteQuasicoherentCartesian.lean, line 408. The attribute's comment: “(4) ⇒ (1), from the quasi-coherence conjunct of (4)”.

Stacks 0GZV, condition (4) implies condition (1). A sheaf of 𝒪_Aff-modules on (Aff/S)_smooth which is quasi-coherent on the ringed site ((Aff/S)_smooth, 𝒪_Aff) has all its base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) isomorphisms.

theorem bigAffineSmooth_isIso_canonicalMap_of_isQuasicoherentOnSite
    (B : BigSmoothSite.{u}) (S : Scheme.{u}) (hS : S.size < B.cutoff)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineSmoothRingedSite B S hS).O))
    (hM : M.IsQuasicoherentOnSite) {U V : BigAffineSmooth B S hS} (f : U ⟶ V) :
    IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineSmoothRingedSite B S hS) M f)

AlgebraicGeometry.bigAffineSyntomic_isIso_canonicalMap_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteQuasicoherentCartesian.lean, line 426. The attribute's comment: “(5) ⇒ (1), from the quasi-coherence conjunct of (5)”.

Stacks 0GZV, condition (5) implies condition (1). A sheaf of 𝒪_Aff-modules on (Aff/S)_syntomic which is quasi-coherent on the ringed site ((Aff/S)_syntomic, 𝒪_Aff) has all its base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) isomorphisms.

theorem bigAffineSyntomic_isIso_canonicalMap_of_isQuasicoherentOnSite
    (B : BigSyntomicSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineSyntomicRingedSite B S hS).O))
    (hM : M.IsQuasicoherentOnSite) {U V : BigAffineSyntomic B S hS} (f : U ⟶ V) :
    IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineSyntomicRingedSite B S hS) M f)

AlgebraicGeometry.bigAffineFppf_isQuasicoherentOnSite_iff_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteQuasicoherentCartesian.lean, line 447. The attribute's comment: “(1) ⇔ (6), for a sheaf of modules”.

Stacks 0GZV, (1) ⇔ (6), for a sheaf of modules. A sheaf of 𝒪_Aff-modules on (Aff/S)_fppf is quasi-coherent on the ringed site ((Aff/S)_fppf, 𝒪_Aff) exactly when all of its base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms.

The sheaf conjunct of condition (6) is carried by the type of M; for a presheaf of modules it is AlgebraicGeometry.bigAffineFppf_isSheaf_of_cartesian.

theorem bigAffineFppf_isQuasicoherentOnSite_iff_canonicalMap_isIso
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineFppfRingedSite B S hS).O)) :
    M.IsQuasicoherentOnSite ↔
      ∀ ⦃U V : BigAffineFppf B S hS⦄ (f : U ⟶ V),
        IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineFppfRingedSite B S hS) M f)

AlgebraicGeometry.bigAffineZariski_isQuasicoherentOnSite_iff_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteQuasicoherentCartesian.lean, line 464. The attribute's comment: “(1) ⇔ (2), for a sheaf of modules”.

Stacks 0GZV, (1) ⇔ (2), for a sheaf of modules. A sheaf of 𝒪_Aff-modules on (Aff/S)_Zar is quasi-coherent on the ringed site ((Aff/S)_Zar, 𝒪_Aff) exactly when all of its base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms.

The sheaf conjunct of condition (2) is carried by the type of M; for a presheaf of modules it is AlgebraicGeometry.bigAffineZariski_isSheaf_of_cartesian.

theorem bigAffineZariski_isQuasicoherentOnSite_iff_canonicalMap_isIso
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineZariskiRingedSite B S hS).O)) :
    M.IsQuasicoherentOnSite ↔
      ∀ ⦃U V : BigAffineZariski B S hS⦄ (f : U ⟶ V),
        IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineZariskiRingedSite B S hS) M f)

AlgebraicGeometry.bigAffineEtale_isQuasicoherentOnSite_iff_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteQuasicoherentCartesian.lean, line 481. The attribute's comment: “(1) ⇔ (3), for a sheaf of modules”.

Stacks 0GZV, (1) ⇔ (3), for a sheaf of modules. A sheaf of 𝒪_Aff-modules on (Aff/S)_étale is quasi-coherent on the ringed site ((Aff/S)_étale, 𝒪_Aff) exactly when all of its base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms.

The sheaf conjunct of condition (3) is carried by the type of M; for a presheaf of modules it is AlgebraicGeometry.bigAffineEtale_isSheaf_of_cartesian.

theorem bigAffineEtale_isQuasicoherentOnSite_iff_canonicalMap_isIso
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineEtaleRingedSite B S hS).O)) :
    M.IsQuasicoherentOnSite ↔
      ∀ ⦃U V : BigAffineEtale B S hS⦄ (f : U ⟶ V),
        IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineEtaleRingedSite B S hS) M f)

AlgebraicGeometry.bigAffineSmooth_isQuasicoherentOnSite_iff_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteQuasicoherentCartesian.lean, line 498. The attribute's comment: “(1) ⇔ (4), for a sheaf of modules”.

Stacks 0GZV, (1) ⇔ (4), for a sheaf of modules. A sheaf of 𝒪_Aff-modules on (Aff/S)_smooth is quasi-coherent on the ringed site ((Aff/S)_smooth, 𝒪_Aff) exactly when all of its base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms.

The sheaf conjunct of condition (4) is carried by the type of M; for a presheaf of modules it is AlgebraicGeometry.bigAffineSmooth_isSheaf_of_cartesian.

theorem bigAffineSmooth_isQuasicoherentOnSite_iff_canonicalMap_isIso
    (B : BigSmoothSite.{u}) (S : Scheme.{u}) (hS : S.size < B.cutoff)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineSmoothRingedSite B S hS).O)) :
    M.IsQuasicoherentOnSite ↔
      ∀ ⦃U V : BigAffineSmooth B S hS⦄ (f : U ⟶ V),
        IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineSmoothRingedSite B S hS) M f)

AlgebraicGeometry.bigAffineSyntomic_isQuasicoherentOnSite_iff_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/BigAffineSiteQuasicoherentCartesian.lean, line 515. The attribute's comment: “(1) ⇔ (5), for a sheaf of modules”.

Stacks 0GZV, (1) ⇔ (5), for a sheaf of modules. A sheaf of 𝒪_Aff-modules on (Aff/S)_syntomic is quasi-coherent on the ringed site ((Aff/S)_syntomic, 𝒪_Aff) exactly when all of its base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms.

The sheaf conjunct of condition (5) is carried by the type of M; for a presheaf of modules it is AlgebraicGeometry.bigAffineSyntomic_isSheaf_of_cartesian.

theorem bigAffineSyntomic_isQuasicoherentOnSite_iff_canonicalMap_isIso
    (B : BigSyntomicSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineSyntomicRingedSite B S hS).O)) :
    M.IsQuasicoherentOnSite ↔
      ∀ ⦃U V : BigAffineSyntomic B S hS⦄ (f : U ⟶ V),
        IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineSyntomicRingedSite B S hS) M f)

AlgebraicGeometry.bigAffineZariski_isQuasicoherentOnSite_of_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 506. The attribute's comment: “(1) ⇒ (2), quasi-coherence conjunct of (2)”.

Stacks 0GZV, condition (2). A sheaf of modules on (Aff/S)_Zar whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are all isomorphisms is quasi-coherent on the ringed site ((Aff/S)_Zar, 𝒪_Aff).

public theorem bigAffineZariski_isQuasicoherentOnSite_of_canonicalMap_isIso
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineZariskiRingedSite B S hS).O))
    (h : ∀ ⦃U V : BigAffineZariski B S hS⦄ (f : U ⟶ V),
      IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineZariskiRingedSite B S hS) F f)) :
    F.IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineZariski_isQuasicoherentOnSite_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 518. The attribute's comment: “(7) ⇒ (2) at τ = Zariski, quasi-coherence conjunct of (2)”.

Stacks 0GZV, condition (2). The restriction to (Aff/S)_Zar of a quasi-coherent module on the ringed site ((Sch/S)_Zar, 𝒪) is quasi-coherent on ((Aff/S)_Zar, 𝒪_Aff).

public theorem bigAffineZariski_isQuasicoherentOnSite_restriction
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigZariskiOverRingedSite B S hS).O))
    (hM : M.IsQuasicoherentOnSite) :
    ((SheafOfModules.pushforward.{u} (F := BigAffineZariski.inclusion B S hS)
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf (bigZariskiOverRingedSite B S hS).O))
      (S := (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineZariskiRingedSite B S hS).O))
        (𝟙 _)).obj
        M).IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineEtale_isQuasicoherentOnSite_of_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 534. The attribute's comment: “(1) ⇒ (3), quasi-coherence conjunct of (3)”.

Stacks 0GZV, condition (3). A sheaf of modules on (Aff/S)_étale whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are all isomorphisms is quasi-coherent on the ringed site ((Aff/S)_étale, 𝒪_Aff).

public theorem bigAffineEtale_isQuasicoherentOnSite_of_canonicalMap_isIso
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineEtaleRingedSite B S hS).O))
    (h : ∀ ⦃U V : BigAffineEtale B S hS⦄ (f : U ⟶ V),
      IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineEtaleRingedSite B S hS) F f)) :
    F.IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineEtale_isQuasicoherentOnSite_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 547. The attribute's comment: “(7) ⇒ (3) at τ = étale, quasi-coherence conjunct of (3)”.

Stacks 0GZV, condition (3). The restriction to (Aff/S)_étale of a quasi-coherent module on the ringed site ((Sch/S)_étale, 𝒪) is quasi-coherent on ((Aff/S)_étale, 𝒪_Aff).

public theorem bigAffineEtale_isQuasicoherentOnSite_restriction
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigEtaleOverRingedSite B S hS).O))
    (hM : M.IsQuasicoherentOnSite) :
    ((SheafOfModules.pushforward.{u} (F := BigAffineEtale.inclusion B S hS)
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf (bigEtaleOverRingedSite B S hS).O))
      (S := (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineEtaleRingedSite B S hS).O))
        (𝟙 _)).obj
        M).IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineSmooth_isQuasicoherentOnSite_of_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 563. The attribute's comment: “(1) ⇒ (4), quasi-coherence conjunct of (4)”.

Stacks 0GZV, condition (4). A sheaf of modules on (Aff/S)_smooth whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are all isomorphisms is quasi-coherent on the ringed site ((Aff/S)_smooth, 𝒪_Aff).

public theorem bigAffineSmooth_isQuasicoherentOnSite_of_canonicalMap_isIso
    (B : BigSmoothSite.{u}) (S : Scheme.{u}) (hS : S.size < B.cutoff)
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineSmoothRingedSite B S hS).O))
    (h : ∀ ⦃U V : BigAffineSmooth B S hS⦄ (f : U ⟶ V),
      IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineSmoothRingedSite B S hS) F f)) :
    F.IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineSmooth_isQuasicoherentOnSite_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 576. The attribute's comment: “(7) ⇒ (4) at τ = smooth, quasi-coherence conjunct of (4)”.

Stacks 0GZV, condition (4). The restriction to (Aff/S)_smooth of a quasi-coherent module on the ringed site ((Sch/S)_smooth, 𝒪) is quasi-coherent on ((Aff/S)_smooth, 𝒪_Aff).

public theorem bigAffineSmooth_isQuasicoherentOnSite_restriction
    (B : BigSmoothSite.{u}) (S : Scheme.{u}) (hS : S.size < B.cutoff)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigSmoothOverRingedSite B S hS).O))
    (hM : M.IsQuasicoherentOnSite) :
    ((SheafOfModules.pushforward.{u} (F := BigAffineSmooth.inclusion B S hS)
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf (bigSmoothOverRingedSite B S hS).O))
      (S := (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineSmoothRingedSite B S hS).O))
        (𝟙 _)).obj
        M).IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineSyntomic_isQuasicoherentOnSite_of_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 592. The attribute's comment: “(1) ⇒ (5), quasi-coherence conjunct of (5)”.

Stacks 0GZV, condition (5). A sheaf of modules on (Aff/S)_syntomic whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are all isomorphisms is quasi-coherent on the ringed site ((Aff/S)_syntomic, 𝒪_Aff).

public theorem bigAffineSyntomic_isQuasicoherentOnSite_of_canonicalMap_isIso
    (B : BigSyntomicSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineSyntomicRingedSite B S hS).O))
    (h : ∀ ⦃U V : BigAffineSyntomic B S hS⦄ (f : U ⟶ V),
      IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineSyntomicRingedSite B S hS) F f)) :
    F.IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineSyntomic_isQuasicoherentOnSite_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 605. The attribute's comment: “(7) ⇒ (5) at τ = syntomic, quasi-coherence conjunct of (5)”.

Stacks 0GZV, condition (5). The restriction to (Aff/S)_syntomic of a quasi-coherent module on the ringed site ((Sch/S)_syntomic, 𝒪) is quasi-coherent on ((Aff/S)_syntomic, 𝒪_Aff).

public theorem bigAffineSyntomic_isQuasicoherentOnSite_restriction
    (B : BigSyntomicSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigSyntomicOverRingedSite B S hS).O))
    (hM : M.IsQuasicoherentOnSite) :
    ((SheafOfModules.pushforward.{u} (F := BigAffineSyntomic.inclusion B S hS)
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf (bigSyntomicOverRingedSite B S hS).O))
      (S := (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineSyntomicRingedSite B S hS).O))
        (𝟙 _)).obj
        M).IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineFppf_isQuasicoherentOnSite_of_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 621. The attribute's comment: “(1) ⇒ (6), quasi-coherence conjunct of (6)”.

Stacks 0GZV, condition (6). A sheaf of modules on (Aff/S)_fppf whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are all isomorphisms is quasi-coherent on the ringed site ((Aff/S)_fppf, 𝒪_Aff).

public theorem bigAffineFppf_isQuasicoherentOnSite_of_canonicalMap_isIso
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineFppfRingedSite B S hS).O))
    (h : ∀ ⦃U V : BigAffineFppf B S hS⦄ (f : U ⟶ V),
      IsIso (Stacks.SheafOfModules.canonicalMap (bigAffineFppfRingedSite B S hS) F f)) :
    F.IsQuasicoherentOnSite

AlgebraicGeometry.bigAffineFppf_isQuasicoherentOnSite_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 633. The attribute's comment: “(7) ⇒ (6) at τ = fppf, quasi-coherence conjunct of (6)”.

Stacks 0GZV, condition (6). The restriction to (Aff/S)_fppf of a quasi-coherent module on the ringed site ((Sch/S)_fppf, 𝒪) is quasi-coherent on ((Aff/S)_fppf, 𝒪_Aff).

public theorem bigAffineFppf_isQuasicoherentOnSite_restriction
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (bigFppfOverRingedSite B S hS).O))
    (hM : M.IsQuasicoherentOnSite) :
    ((SheafOfModules.pushforward.{u} (F := BigAffineFppf.inclusion B S hS)
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf (bigFppfOverRingedSite B S hS).O))
      (S := (Stacks.SheafOfModules.Tensor.ringSheaf (bigAffineFppfRingedSite B S hS).O))
        (𝟙 _)).obj
        M).IsQuasicoherentOnSite

Tag 0GZW, an equation

Tag 0GZW in the Stacks Project.

AlgebraicGeometry.SmallAffineZariski.ringedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmallAffineRingedTopos.lean, line 181. The attribute's comment: “Zariski case”.

The morphism of ringed topoi (Sh(S_{affine, Zar}), 𝒪_affine) ⟶ (Sh(S_Zar), 𝒪) given by the inclusion of the affine objects of the small Zariski site of S, with structure morphism the adjunct of the identification of g⁻¹𝒪 with the restriction 𝒪_affine of 𝒪.

public noncomputable def ringedToposHom :
    RingedToposHom (ringedTopos B S hS) (SmallZariski.ringedTopos B S hS)

AlgebraicGeometry.SmallAffineZariski.ringedToposHom_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmallAffineRingedTopos.lean, line 190. The attribute's comment: “Zariski case”.

The inverse image of the equivalence is restriction along the inclusion of the affine objects, on the nose.

public theorem ringedToposHom_inverseImage :
    (ringedToposHom B S hS).toToposHom.inverseImage =
      (inclusion B S hS).sheafPushforwardContinuous (Type u)
        (topology B S hS) (SmallZariski.topology B S hS)

AlgebraicGeometry.SmallAffineZariski.ringedToposHom_inverseImage_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmallAffineRingedTopos.lean, line 199. The attribute's comment: “Zariski case”.

The underlying morphism of topoi is an equivalence of topoi: its inverse image, restriction along the inclusion of the affine objects, is an equivalence of categories of sheaves.

public theorem ringedToposHom_inverseImage_isEquivalence :
    (ringedToposHom B S hS).toToposHom.inverseImage.IsEquivalence

AlgebraicGeometry.SmallAffineZariski.isIso_ringedToposHom_fSharpInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmallAffineRingedTopos.lean, line 215. The attribute's comment: “Zariski case”.

The structure morphism g⁻¹𝒪 ⟶ 𝒪_affine is an isomorphism, so the morphism of ringed topoi is an equivalence of ringed topoi and not merely a morphism whose underlying morphism of topoi is an equivalence.

public theorem isIso_ringedToposHom_fSharpInverseImage :
    IsIso (ringedToposHom B S hS).fSharpInverseImage

AlgebraicGeometry.SmallAffineZariski.ringedToposHom_fSharpInverseImage_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmallAffineRingedTopos.lean, line 223. The attribute's comment: “Zariski case”.

The structure morphism is the canonical one: on underlying sheaves of sets it is the identity of the restriction of the underlying sheaf of sets of 𝒪, so 𝒪_affine really is 𝒪 restricted and not an arbitrary sheaf of rings with the same underlying sheaf of sets.

public theorem ringedToposHom_fSharpInverseImage_forget :
    (sheafCompose (topology B S hS) (forget CommRingCat.{u})).map
        (ringedToposHom B S hS).fSharpInverseImage =
      𝟙 ((inclusion B S hS).sheafPushforwardContinuous (Type u)
        (topology B S hS) (SmallZariski.topology B S hS) |>.obj
        ((sheafCompose (SmallZariski.topology B S hS) (forget CommRingCat.{u})).obj
          (SmallZariski.ringedTopos B S hS).O))

AlgebraicGeometry.SmallAffineEtale.ringedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmallAffineRingedTopos.lean, line 328. The attribute's comment: “étale case”.

The morphism of ringed topoi (Sh(S_{affine, étale}), 𝒪_affine) ⟶ (Sh(S_étale), 𝒪) given by the inclusion of the affine objects of the small étale site of S, with structure morphism the adjunct of the identification of g⁻¹𝒪 with the restriction 𝒪_affine of 𝒪.

public noncomputable def ringedToposHom :
    RingedToposHom (ringedTopos B S hS) (SmallEtale.ringedTopos B S hS)

AlgebraicGeometry.SmallAffineEtale.ringedToposHom_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmallAffineRingedTopos.lean, line 337. The attribute's comment: “étale case”.

The inverse image of the equivalence is restriction along the inclusion of the affine objects, on the nose.

public theorem ringedToposHom_inverseImage :
    (ringedToposHom B S hS).toToposHom.inverseImage =
      (inclusion B S hS).sheafPushforwardContinuous (Type u)
        (topology B S hS) (SmallEtale.topology B S hS)

AlgebraicGeometry.SmallAffineEtale.ringedToposHom_inverseImage_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmallAffineRingedTopos.lean, line 346. The attribute's comment: “étale case”.

The underlying morphism of topoi is an equivalence of topoi: its inverse image, restriction along the inclusion of the affine objects, is an equivalence of categories of sheaves.

public theorem ringedToposHom_inverseImage_isEquivalence :
    (ringedToposHom B S hS).toToposHom.inverseImage.IsEquivalence

AlgebraicGeometry.SmallAffineEtale.isIso_ringedToposHom_fSharpInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmallAffineRingedTopos.lean, line 362. The attribute's comment: “étale case”.

The structure morphism g⁻¹𝒪 ⟶ 𝒪_affine is an isomorphism, so the morphism of ringed topoi is an equivalence of ringed topoi and not merely a morphism whose underlying morphism of topoi is an equivalence.

public theorem isIso_ringedToposHom_fSharpInverseImage :
    IsIso (ringedToposHom B S hS).fSharpInverseImage

AlgebraicGeometry.SmallAffineEtale.ringedToposHom_fSharpInverseImage_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmallAffineRingedTopos.lean, line 370. The attribute's comment: “étale case”.

The structure morphism is the canonical one: on underlying sheaves of sets it is the identity of the restriction of the underlying sheaf of sets of 𝒪, so 𝒪_affine really is 𝒪 restricted and not an arbitrary sheaf of rings with the same underlying sheaf of sets.

public theorem ringedToposHom_fSharpInverseImage_forget :
    (sheafCompose (topology B S hS) (forget CommRingCat.{u})).map
        (ringedToposHom B S hS).fSharpInverseImage =
      𝟙 ((inclusion B S hS).sheafPushforwardContinuous (Type u)
        (topology B S hS) (SmallEtale.topology B S hS) |>.obj
        ((sheafCompose (SmallEtale.topology B S hS) (forget CommRingCat.{u})).obj
          (SmallEtale.ringedTopos B S hS).O))

Tag 0GZX, a lemma

Tag 0GZX in the Stacks Project.

AlgebraicGeometry.smallAffineZariski_isQuasicoherentOnSite_of_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 366. The attribute's comment: “(1) ⇒ (2) at τ = Zariski, quasi-coherence conjunct of (2)”.

Stacks 0GZX, Zariski case. A sheaf of modules on the small affine Zariski site of S whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are all isomorphisms is quasi-coherent on the ringed site (S_{affine, Zar}, 𝒪_affine).

public theorem smallAffineZariski_isQuasicoherentOnSite_of_canonicalMap_isIso
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallAffineZariskiRingedSite B S hS).O))
    (h : ∀ ⦃U V : SmallAffineZariski B S hS⦄ (f : U ⟶ V),
      IsIso (Stacks.SheafOfModules.canonicalMap (smallAffineZariskiRingedSite B S hS) F f)) :
    F.IsQuasicoherentOnSite

AlgebraicGeometry.smallAffineZariski_isQuasicoherentOnSite_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 379. The attribute's comment: “(3) ⇒ (2) at τ = Zariski, quasi-coherence conjunct of (2)”.

Stacks 0GZX, Zariski case. The restriction to the small affine Zariski site of S of a quasi-coherent module on the ringed site (S_Zar, 𝒪) is quasi-coherent on (S_{affine, Zar}, 𝒪_affine).

public theorem smallAffineZariski_isQuasicoherentOnSite_restriction
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallZariskiRingedSite B S hS).O))
    (hM : M.IsQuasicoherentOnSite) :
    ((SheafOfModules.pushforward.{u} (F := SmallAffineZariski.inclusion B S hS)
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf (smallZariskiRingedSite B S hS).O))
      (S := (Stacks.SheafOfModules.Tensor.ringSheaf (smallAffineZariskiRingedSite B S hS).O))
        (𝟙 _)).obj
        M).IsQuasicoherentOnSite

AlgebraicGeometry.smallAffineEtale_isQuasicoherentOnSite_of_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 395. The attribute's comment: “(1) ⇒ (2) at τ = étale, quasi-coherence conjunct of (2)”.

Stacks 0GZX, étale case. A sheaf of modules on the small affine étale site of S whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are all isomorphisms is quasi-coherent on the ringed site (S_{affine, étale}, 𝒪_affine).

public theorem smallAffineEtale_isQuasicoherentOnSite_of_canonicalMap_isIso
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallAffineEtaleRingedSite B S hS).O))
    (h : ∀ ⦃U V : SmallAffineEtale B S hS⦄ (f : U ⟶ V),
      IsIso (Stacks.SheafOfModules.canonicalMap (smallAffineEtaleRingedSite B S hS) F f)) :
    F.IsQuasicoherentOnSite

AlgebraicGeometry.smallAffineEtale_isQuasicoherentOnSite_restriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffines.lean, line 408. The attribute's comment: “(3) ⇒ (2) at τ = étale, quasi-coherence conjunct of (2)”.

Stacks 0GZX, étale case. The restriction to the small affine étale site of S of a quasi-coherent module on the ringed site (S_étale, 𝒪) is quasi-coherent on (S_{affine, étale}, 𝒪_affine).

public theorem smallAffineEtale_isQuasicoherentOnSite_restriction
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (M : SheafOfModules.{u}
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS).O))
    (hM : M.IsQuasicoherentOnSite) :
    ((SheafOfModules.pushforward.{u} (F := SmallAffineEtale.inclusion B S hS)
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS).O))
      (S := (Stacks.SheafOfModules.Tensor.ringSheaf (smallAffineEtaleRingedSite B S hS).O))
        (𝟙 _)).obj
        M).IsQuasicoherentOnSite

AlgebraicGeometry.smallAffineEtale_exists_isQuasicoherentOnSite_restriction_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesExists.lean, line 125. The attribute's comment: “(2) ⇒ (3) at τ = étale”.

A sheaf of modules on the small affine étale site of S which is quasi-coherent on the ringed site (S_{affine, étale}, 𝒪_affine) is the restriction of a quasi-coherent 𝒪-module on (S_étale, 𝒪).

public theorem smallAffineEtale_exists_isQuasicoherentOnSite_restriction_iso
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineEtaleRingedSite B S hS).O))
    (hF : F.IsQuasicoherentOnSite) :
    ∃ N : SheafOfModules.{u} (SmallEtale.structureSheaf B S hS), N.IsQuasicoherentOnSite ∧
      Nonempty ((smallAffineEtaleModuleRestriction B S hS).obj N ≅ F)

AlgebraicGeometry.smallAffineEtale_essImage_associatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesExists.lean, line 142. The attribute's comment: “(4) at τ = étale, existence of 𝒢”.

A sheaf of modules 𝓕 on the small affine étale site of S which is quasi-coherent on the ringed site (S_{affine, étale}, 𝒪_affine) lies in the essential image of the functor 𝒢 ↦ 𝒢ᵃ|_{S_{affine, étale}} on quasi-coherent 𝒪_S-modules.

public theorem smallAffineEtale_essImage_associatedModuleQcoh
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineEtaleRingedSite B S hS).O))
    (hF : F.IsQuasicoherentOnSite) :
    (smallAffineEtaleAssociatedModuleQcoh B S hS).essImage F

AlgebraicGeometry.smallAffineEtale_exists_associatedModuleQcoh_restriction_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesExists.lean, line 161. The attribute's comment: “(1) ⇒ (4) at τ = étale, existence of 𝒢”.

A sheaf of modules on the small affine étale site of S all of whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms is isomorphic to 𝒢ᵃ|_{S_{affine, étale}} for a quasi-coherent 𝒪_S-module 𝒢.

public theorem smallAffineEtale_exists_associatedModuleQcoh_restriction_iso
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineEtaleRingedSite B S hS).O))
    (hF : ∀ ⦃U V : SmallAffineEtale B S hS⦄ (f : U ⟶ V),
      IsIso (Stacks.SheafOfModules.canonicalMap (smallAffineEtaleRingedSite B S hS) F f)) :
    ∃ G : (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory,
      Nonempty ((smallAffineEtaleAssociatedModuleQcoh B S hS).obj G ≅ F)

AlgebraicGeometry.isEquivalence_smallAffineEtaleModuleRestrictionQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesExists.lean, line 206. The attribute's comment: “(2) ⇔ (3) at τ = étale”.

Restriction to the affine objects is an equivalence QCoh(S_étale, 𝒪) ≌ QCoh(S_{affine, étale}, 𝒪_affine) between the categories of quasi-coherent modules.

public theorem isEquivalence_smallAffineEtaleModuleRestrictionQcoh :
    (smallAffineEtaleModuleRestrictionQcoh B S hS).IsEquivalence

AlgebraicGeometry.isEquivalence_smallAffineEtaleAssociatedModuleQcohOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesExists.lean, line 249. The attribute's comment: “(2) ⇔ (4) at τ = étale”.

The functor 𝒢 ↦ 𝒢ᵃ|_{S_{affine, étale}} is an equivalence from the quasi-coherent 𝒪_S-modules onto the quasi-coherent modules on the ringed site (S_{affine, étale}, 𝒪_affine): every such module comes from a 𝒢, and from a unique one.

public theorem isEquivalence_smallAffineEtaleAssociatedModuleQcohOnSite :
    (smallAffineEtaleAssociatedModuleQcohOnSite B S hS).IsEquivalence

AlgebraicGeometry.smallAffineEtaleAssociatedModuleQcohEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesExists.lean, line 260. The attribute's comment: “(2) ⇔ (4) at τ = étale”.

The equivalence of categories QCoh(𝒪_S) ≌ QCoh(S_{affine, étale}, 𝒪_affine) with functor 𝒢 ↦ 𝒢ᵃ|_{S_{affine, étale}}.

public noncomputable def smallAffineEtaleAssociatedModuleQcohEquivalence :
    (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory ≌
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (smallAffineEtaleRingedSite B S hS).O)).FullSubcategory

AlgebraicGeometry.smallAffineZariski_isSheaf_of_baseChange_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesSheaf.lean, line 68. The attribute's comment: “(1) ⇒ (2) at τ = Zariski, sheaf conjunct of (2)”.

A presheaf of 𝒪_affine-modules on the small affine Zariski site of S all of whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms is a sheaf.

theorem smallAffineZariski_isSheaf_of_baseChange_isIso
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : PresheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineZariskiRingedSite B S hS).O).obj)
    (h : ∀ ⦃X Y : (SmallAffineZariski B S hS)ᵒᵖ⦄ (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, u} F f)) :
    Presheaf.IsSheaf (smallAffineZariskiRingedSite B S hS).J F.presheaf

AlgebraicGeometry.smallAffineEtale_isSheaf_of_baseChange_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesSheaf.lean, line 80. The attribute's comment: “(1) ⇒ (2) at τ = étale, sheaf conjunct of (2)”.

A presheaf of 𝒪_affine-modules on the small affine étale site of S all of whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms is a sheaf.

theorem smallAffineEtale_isSheaf_of_baseChange_isIso
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : PresheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineEtaleRingedSite B S hS).O).obj)
    (h : ∀ ⦃X Y : (SmallAffineEtale B S hS)ᵒᵖ⦄ (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, u} F f)) :
    Presheaf.IsSheaf (smallAffineEtaleRingedSite B S hS).J F.presheaf

AlgebraicGeometry.smallAffineZariski_isSheaf_and_isQuasicoherentOnSite_of_baseChange_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesSheaf.lean, line 110. The attribute's comment: “(1) ⇒ (2) at τ = Zariski, for a presheaf of modules”.

A presheaf of 𝒪_affine-modules on the small affine Zariski site of S all of whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms is a sheaf, and the resulting sheaf of modules is quasi-coherent on the ringed site (S_{affine, Zar}, 𝒪_affine).

theorem smallAffineZariski_isSheaf_and_isQuasicoherentOnSite_of_baseChange_isIso
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : PresheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineZariskiRingedSite B S hS).O).obj)
    (h : ∀ ⦃X Y : (SmallAffineZariski B S hS)ᵒᵖ⦄ (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, u} F f)) :
    ∃ hs : Presheaf.IsSheaf (smallAffineZariskiRingedSite B S hS).J F.presheaf,
      (⟨F, hs⟩ : SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (smallAffineZariskiRingedSite B S hS).O)).IsQuasicoherentOnSite

AlgebraicGeometry.smallAffineEtale_isSheaf_and_isQuasicoherentOnSite_of_baseChange_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesSheaf.lean, line 127. The attribute's comment: “(1) ⇒ (2) at τ = étale, for a presheaf of modules”.

A presheaf of 𝒪_affine-modules on the small affine étale site of S all of whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms is a sheaf, and the resulting sheaf of modules is quasi-coherent on the ringed site (S_{affine, étale}, 𝒪_affine).

theorem smallAffineEtale_isSheaf_and_isQuasicoherentOnSite_of_baseChange_isIso
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : PresheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineEtaleRingedSite B S hS).O).obj)
    (h : ∀ ⦃X Y : (SmallAffineEtale B S hS)ᵒᵖ⦄ (f : X ⟶ Y),
      IsIso (Stacks.PresheafOfModules.restrictionBaseChange.{u + 1, u, u, u} F f)) :
    ∃ hs : Presheaf.IsSheaf (smallAffineEtaleRingedSite B S hS).J F.presheaf,
      (⟨F, hs⟩ : SheafOfModules.{u}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (smallAffineEtaleRingedSite B S hS).O)).IsQuasicoherentOnSite

AlgebraicGeometry.smallAffineZariski_canonicalMap_isIso_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesSheaf.lean, line 146. The attribute's comment: “(2) ⇒ (1) at τ = Zariski”.

If a sheaf of modules on the small affine Zariski site of S is quasi-coherent on the ringed site (S_{affine, Zar}, 𝒪_affine), then its base-change map 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) along every morphism is an isomorphism.

theorem smallAffineZariski_canonicalMap_isIso_of_isQuasicoherentOnSite
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineZariskiRingedSite B S hS).O))
    (hF : F.IsQuasicoherentOnSite)
    {U V : SmallAffineZariski B S hS} (f : U ⟶ V) :
    IsIso (Stacks.SheafOfModules.canonicalMap (smallAffineZariskiRingedSite B S hS) F f)

AlgebraicGeometry.smallAffineEtale_canonicalMap_isIso_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesSheaf.lean, line 165. The attribute's comment: “(2) ⇒ (1) at τ = étale”.

If a sheaf of modules on the small affine étale site of S is quasi-coherent on the ringed site (S_{affine, étale}, 𝒪_affine), then its base-change map 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) along every morphism is an isomorphism.

theorem smallAffineEtale_canonicalMap_isIso_of_isQuasicoherentOnSite
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineEtaleRingedSite B S hS).O))
    (hF : F.IsQuasicoherentOnSite)
    {U V : SmallAffineEtale B S hS} (f : U ⟶ V) :
    IsIso (Stacks.SheafOfModules.canonicalMap (smallAffineEtaleRingedSite B S hS) F f)

AlgebraicGeometry.smallAffineZariski_isQuasicoherentOnSite_iff_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesSheaf.lean, line 186. The attribute's comment: “(1) ⇔ (2) at τ = Zariski, for a sheaf of modules”.

A sheaf of modules on the small affine Zariski site of S is quasi-coherent on the ringed site (S_{affine, Zar}, 𝒪_affine) exactly when all of its base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms.

theorem smallAffineZariski_isQuasicoherentOnSite_iff_canonicalMap_isIso
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineZariskiRingedSite B S hS).O)) :
    F.IsQuasicoherentOnSite ↔
      ∀ ⦃U V : SmallAffineZariski B S hS⦄ (f : U ⟶ V),
        IsIso (Stacks.SheafOfModules.canonicalMap (smallAffineZariskiRingedSite B S hS) F f)

AlgebraicGeometry.smallAffineEtale_isQuasicoherentOnSite_iff_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesSheaf.lean, line 201. The attribute's comment: “(1) ⇔ (2) at τ = étale, for a sheaf of modules”.

A sheaf of modules on the small affine étale site of S is quasi-coherent on the ringed site (S_{affine, étale}, 𝒪_affine) exactly when all of its base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms.

theorem smallAffineEtale_isQuasicoherentOnSite_iff_canonicalMap_isIso
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineEtaleRingedSite B S hS).O)) :
    F.IsQuasicoherentOnSite ↔
      ∀ ⦃U V : SmallAffineEtale B S hS⦄ (f : U ⟶ V),
        IsIso (Stacks.SheafOfModules.canonicalMap (smallAffineEtaleRingedSite B S hS) F f)

AlgebraicGeometry.fullyFaithfulSmallAffineEtaleAssociatedModuleQcoh, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesUnique.lean, line 114. The attribute's comment: “(4) at τ = étale, uniqueness of 𝒢”.

Stacks 0GZX, the uniqueness of 𝒢 in condition (4) at τ = étale. The functor 𝒢 ↦ 𝒢ᵃ|_{S_{affine, étale}} from the quasi-coherent 𝒪_S-modules to the 𝒪_affine-modules on S_{affine, étale} is fully faithful: it is Stacks 0GN7 at τ = étale followed by the Comparison Lemma for sheaves of modules on the dense subsite of affine objects.

public noncomputable def fullyFaithfulSmallAffineEtaleAssociatedModuleQcoh :
    (smallAffineEtaleAssociatedModuleQcoh B S hS).FullyFaithful

AlgebraicGeometry.smallAffineEtale_iso_of_associatedModuleQcoh_restriction_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesUnique.lean, line 123. The attribute's comment: “(4) at τ = étale, uniqueness of 𝒢”.

Stacks 0GZX, the uniqueness of 𝒢 in condition (4) at τ = étale, read as a uniqueness statement: two quasi-coherent 𝒪_S-modules whose associated modules have isomorphic restrictions to the small affine étale site of S are isomorphic.

public theorem smallAffineEtale_iso_of_associatedModuleQcoh_restriction_iso
    (G₁ G₂ : (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory)
    (e : (smallAffineEtaleAssociatedModuleQcoh B S hS).obj G₁ ≅
      (smallAffineEtaleAssociatedModuleQcoh B S hS).obj G₂) :
    Nonempty (G₁.obj ≅ G₂.obj)

AlgebraicGeometry.smallAffineZariski_exists_isQuasicoherentOnSite_restriction_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesZariskiExists.lean, line 239. The attribute's comment: “(2) ⇒ (3) at τ = Zariski”.

A sheaf of modules on the small affine Zariski site of S which is quasi-coherent on the ringed site (S_{affine, Zar}, 𝒪_affine) is the restriction of a quasi-coherent 𝒪-module on (S_Zar, 𝒪), i.e. corresponds to one under the equivalence of ringed topoi (0GZW).

public theorem smallAffineZariski_exists_isQuasicoherentOnSite_restriction_iso
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineZariskiRingedSite B S hS).O))
    (hF : F.IsQuasicoherentOnSite) :
    ∃ N : SheafOfModules.{u} (SmallZariski.structureSheaf B S hS), N.IsQuasicoherentOnSite ∧
      Nonempty ((smallAffineZariskiModuleRestriction B S hS).obj N ≅ F)

AlgebraicGeometry.smallAffineZariski_essImage_associatedModuleQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesZariskiExists.lean, line 261. The attribute's comment: “(4) at τ = Zariski, existence of 𝒢”.

A sheaf of modules 𝓕 on the small affine Zariski site of S which is quasi-coherent on the ringed site (S_{affine, Zar}, 𝒪_affine) comes from a quasi-coherent 𝒪_S-module 𝒢 by the procedure of Descent, Section 35.8: it is in the essential image of 𝒢 ↦ 𝒢ᵃ|_{S_{affine, Zar}}.

public theorem smallAffineZariski_essImage_associatedModuleQcoh
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineZariskiRingedSite B S hS).O))
    (hF : F.IsQuasicoherentOnSite) :
    (smallAffineZariskiAssociatedModuleQcoh B S hS).essImage F

AlgebraicGeometry.smallAffineZariski_exists_associatedModuleQcoh_restriction_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesZariskiExists.lean, line 279. The attribute's comment: “(1) ⇒ (4) at τ = Zariski, existence of 𝒢”.

A sheaf of modules 𝓕 on the small affine Zariski site of S all of whose base-change maps 𝓕(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝓕(U) are isomorphisms is isomorphic to 𝒢ᵃ|_{S_{affine, Zar}} for a quasi-coherent 𝒪_S-module 𝒢.

public theorem smallAffineZariski_exists_associatedModuleQcoh_restriction_iso
    (F : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallAffineZariskiRingedSite B S hS).O))
    (hF : ∀ ⦃U V : SmallAffineZariski B S hS⦄ (f : U ⟶ V),
      IsIso (Stacks.SheafOfModules.canonicalMap (smallAffineZariskiRingedSite B S hS) F f)) :
    ∃ G : (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory,
      Nonempty ((smallAffineZariskiAssociatedModuleQcoh B S hS).obj G ≅ F)

AlgebraicGeometry.isEquivalence_smallAffineZariskiModuleRestrictionQcoh, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesZariskiExists.lean, line 323. The attribute's comment: “(2) ⇔ (3) at τ = Zariski”.

The equivalence of ringed topoi (0GZW) induces an equivalence QCoh(S_Zar, 𝒪) ≌ QCoh(S_{affine, Zar}, 𝒪_affine) between the categories of quasi-coherent modules.

public theorem isEquivalence_smallAffineZariskiModuleRestrictionQcoh :
    (smallAffineZariskiModuleRestrictionQcoh B S hS).IsEquivalence

AlgebraicGeometry.isEquivalence_smallAffineZariskiAssociatedModuleQcohOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesZariskiExists.lean, line 364. The attribute's comment: “(2) ⇔ (4) at τ = Zariski”.

The functor 𝒢 ↦ 𝒢ᵃ|_{S_{affine, Zar}} is an equivalence from the quasi-coherent 𝒪_S-modules onto the quasi-coherent modules on the ringed site (S_{affine, Zar}, 𝒪_affine): every such module comes from a 𝒢, and from a unique one.

public theorem isEquivalence_smallAffineZariskiAssociatedModuleQcohOnSite :
    (smallAffineZariskiAssociatedModuleQcohOnSite B S hS).IsEquivalence

AlgebraicGeometry.smallAffineZariskiAssociatedModuleQcohEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesZariskiExists.lean, line 375. The attribute's comment: “(2) ⇔ (4) at τ = Zariski”.

The equivalence of categories QCoh(𝒪_S) ≌ QCoh(S_{affine, Zar}, 𝒪_affine) whose functor is 𝒢 ↦ 𝒢ᵃ|_{S_{affine, Zar}}.

public noncomputable def smallAffineZariskiAssociatedModuleQcohEquivalence :
    (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory ≌
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (smallAffineZariskiRingedSite B S hS).O)).FullSubcategory

AlgebraicGeometry.fullyFaithfulSmallAffineZariskiAssociatedModuleQcoh, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesZariskiUnique.lean, line 83. The attribute's comment: “(4) at τ = Zariski, uniqueness of 𝒢”.

The functor 𝒢 ↦ 𝒢ᵃ|_{S_{affine, Zar}} from the quasi-coherent 𝒪_S-modules to the 𝒪_affine-modules on S_{affine, Zar} is fully faithful.

public noncomputable def fullyFaithfulSmallAffineZariskiAssociatedModuleQcoh :
    (smallAffineZariskiAssociatedModuleQcoh B S hS).FullyFaithful

AlgebraicGeometry.smallAffineZariski_iso_of_associatedModuleQcoh_restriction_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/QuasiCoherentModulesAndAffinesZariskiUnique.lean, line 91. The attribute's comment: “(4) at τ = Zariski, uniqueness of 𝒢”.

Two quasi-coherent 𝒪_S-modules whose associated modules have isomorphic restrictions to the small affine Zariski site of S are isomorphic.

public theorem smallAffineZariski_iso_of_associatedModuleQcoh_restriction_iso
    (G₁ G₂ : (SheafOfModules.isQuasicoherent S.ringCatSheaf).FullSubcategory)
    (e : (smallAffineZariskiAssociatedModuleQcoh B S hS).obj G₁ ≅
      (smallAffineZariskiAssociatedModuleQcoh B S hS).obj G₂) :
    Nonempty (G₁.obj ≅ G₂.obj)

AlgebraicGeometry.smallAffineZariski_isIso_restrictionBaseChange_associatedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmallAffineSiteAssociatedModuleCartesian.lean, line 104. The attribute's comment: “(4) ⇒ (1) at τ = Zariski”.

Stacks 0GZX, condition (4) implies condition (1) at τ = Zariski. The presheaf 𝒢ᵃ of Descent, Section 35.8 attached to a quasi-coherent 𝒪_S-module 𝒢 has all its base-change comparisons 𝒢ᵃ(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝒢ᵃ(U) isomorphisms on the small affine Zariski site of S.

public theorem smallAffineZariski_isIso_restrictionBaseChange_associatedModule
    (B : BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (G : S.Modules) [G.IsQuasicoherent] {X Y : (SmallAffineZariski B S hS)ᵒᵖ} (f : X ⟶ Y) :
    IsIso (Stacks.PresheafOfModules.restrictionBaseChange
      (R := (smallAffineZariskiRingedSite B S hS).O.obj)
      (associatedModulePresheaf S G (smallAffineZariskiToOver B S hS)) f)

AlgebraicGeometry.smallAffineEtale_isIso_restrictionBaseChange_associatedModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmallAffineSiteAssociatedModuleCartesian.lean, line 135. The attribute's comment: “(4) ⇒ (1) at τ = étale”.

Stacks 0GZX, condition (4) implies condition (1) at τ = étale. The presheaf 𝒢ᵃ of Descent, Section 35.8 attached to a quasi-coherent 𝒪_S-module 𝒢 has all its base-change comparisons 𝒢ᵃ(U') ⊗_{𝒪(U')} 𝒪(U) ⟶ 𝒢ᵃ(U) isomorphisms on the small affine étale site of S.

public theorem smallAffineEtale_isIso_restrictionBaseChange_associatedModule
    (B : BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (G : S.Modules) [G.IsQuasicoherent] {X Y : (SmallAffineEtale B S hS)ᵒᵖ} (f : X ⟶ Y) :
    IsIso (Stacks.PresheafOfModules.restrictionBaseChange
      (R := (smallAffineEtaleRingedSite B S hS).O.obj)
      (associatedModulePresheaf S G (smallAffineEtaleToOver B S hS)) f)

Sources

• Section 35.11, Tag 0GZT
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.zariski_affineToBigRingedToposEquivalence · AlgebraicGeometry.etale_affineToBigRingedToposEquivalence · AlgebraicGeometry.smooth_affineToBigRingedToposEquivalence · AlgebraicGeometry.syntomic_affineToBigRingedToposEquivalence · AlgebraicGeometry.fppf_affineToBigRingedToposEquivalence · AlgebraicGeometry.bigAffineZariski_isIso_restrictionBaseChange_associatedModule · AlgebraicGeometry.bigAffineEtale_isIso_restrictionBaseChange_associatedModule · AlgebraicGeometry.bigAffineSmooth_isIso_restrictionBaseChange_associatedModule

Section35.12 Parasitic modules#

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

Tag 06ZL, a definition

Tag 06ZL in the Stacks Project.

AlgebraicGeometry.IsParasitic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/Defs.lean, line 53. The attribute's comment: “part (1)”.

A presheaf of modules is parasitic when its sections vanish on every object of the site which is flat over the base scheme.

public abbrev IsParasitic (S : Scheme.{u}) {C : Type (u + 1)} [Category.{u} C]
    (toOver : C ⥤ Over S) {𝒪 : Cᵒᵖ ⥤ RingCat.{u}} (F : PresheafOfModules.{u} 𝒪) : Prop

AlgebraicGeometry.IsParasiticFor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/Defs.lean, line 60. The attribute's comment: “part (2)”.

A presheaf of modules is parasitic for a topology when its sections vanish on every member of every covering family of the base scheme.

public abbrev IsParasiticFor (S : Scheme.{u}) {C : Type (u + 1)} [Category.{u} C]
    (toOver : C ⥤ Over S) (isCovering : Covering C → Prop)
    {𝒪 : Cᵒᵖ ⥤ RingCat.{u}} (F : PresheafOfModules.{u} 𝒪) : Prop

Tag 0755, a lemma

Tag 0755 in the Stacks Project.

AlgebraicGeometry.bigZariskiCohomology_isZero_of_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/FlatVanishing.lean, line 318. The attribute's comment: “flat_parasitic_vanishing”.

A parasitic module on the big Zariski site has no cohomology at a flat object.

public theorem bigZariskiCohomology_isZero_of_isParasitic
    (B : AlgebraicGeometry.BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [HasSheafify (AlgebraicGeometry.BigZariskiOver.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (AlgebraicGeometry.BigZariskiOver.topology B S hS) AddCommGrpCat.{u})]
    {𝒪 : Sheaf (AlgebraicGeometry.BigZariskiOver.topology B S hS) RingCat.{u}}
    (F : SheafOfModules.{u} 𝒪)
    (hF : ∀ X : AlgebraicGeometry.BigZariskiOver B S hS,
      Flat ((Over.post B.inclusion).obj X).hom → Subsingleton (F.val.obj (Opposite.op X)))
    (U : AlgebraicGeometry.BigZariskiOver B S hS)
    (hU : Flat ((Over.post B.inclusion).obj U).hom) (p : ℕ) :
    IsZero (((SheafOfModules.toSheaf _).obj F).H' p U)

AlgebraicGeometry.bigEtaleCohomology_isZero_of_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/FlatVanishing.lean, line 380. The attribute's comment: “flat_parasitic_vanishing”.

A parasitic module on the big étale site has no cohomology at a flat object.

public theorem bigEtaleCohomology_isZero_of_isParasitic
    (B : AlgebraicGeometry.BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [HasSheafify (AlgebraicGeometry.BigEtaleOver.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (AlgebraicGeometry.BigEtaleOver.topology B S hS) AddCommGrpCat.{u})]
    {𝒪 : Sheaf (AlgebraicGeometry.BigEtaleOver.topology B S hS) RingCat.{u}}
    (F : SheafOfModules.{u} 𝒪)
    (hF : ∀ X : AlgebraicGeometry.BigEtaleOver B S hS,
      Flat ((Over.post B.inclusion).obj X).hom → Subsingleton (F.val.obj (Opposite.op X)))
    (U : AlgebraicGeometry.BigEtaleOver B S hS)
    (hU : Flat ((Over.post B.inclusion).obj U).hom) (p : ℕ) :
    IsZero (((SheafOfModules.toSheaf _).obj F).H' p U)

AlgebraicGeometry.bigSmoothCohomology_isZero_of_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/FlatVanishing.lean, line 440. The attribute's comment: “flat_parasitic_vanishing”.

A parasitic module on the big smooth site has no cohomology at a flat object.

public theorem bigSmoothCohomology_isZero_of_isParasitic
    (B : AlgebraicGeometry.BigSmoothSite.{u}) (S : Scheme.{u}) (hS : S.size < B.cutoff)
    [HasSheafify (AlgebraicGeometry.BigSmoothOver.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (AlgebraicGeometry.BigSmoothOver.topology B S hS) AddCommGrpCat.{u})]
    {𝒪 : Sheaf (AlgebraicGeometry.BigSmoothOver.topology B S hS) RingCat.{u}}
    (F : SheafOfModules.{u} 𝒪)
    (hF : ∀ X : AlgebraicGeometry.BigSmoothOver B S hS,
      Flat ((Over.post (ObjectProperty.ι _)).obj X).hom →
        Subsingleton (F.val.obj (Opposite.op X)))
    (U : AlgebraicGeometry.BigSmoothOver B S hS)
    (hU : Flat ((Over.post (ObjectProperty.ι _)).obj U).hom) (p : ℕ) :
    IsZero (((SheafOfModules.toSheaf _).obj F).H' p U)

AlgebraicGeometry.bigSyntomicCohomology_isZero_of_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/FlatVanishing.lean, line 512. The attribute's comment: “flat_parasitic_vanishing”.

A parasitic module on the big syntomic site has no cohomology at a flat object.

public theorem bigSyntomicCohomology_isZero_of_isParasitic
    (B : AlgebraicGeometry.BigSyntomicSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [HasSheafify (AlgebraicGeometry.BigSyntomicOver.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (AlgebraicGeometry.BigSyntomicOver.topology B S hS) AddCommGrpCat.{u})]
    {𝒪 : Sheaf (AlgebraicGeometry.BigSyntomicOver.topology B S hS) RingCat.{u}}
    (F : SheafOfModules.{u} 𝒪)
    (hF : ∀ X : AlgebraicGeometry.BigSyntomicOver B S hS,
      Flat ((Over.post B.inclusion).obj X).hom → Subsingleton (F.val.obj (Opposite.op X)))
    (U : AlgebraicGeometry.BigSyntomicOver B S hS)
    (hU : Flat ((Over.post B.inclusion).obj U).hom) (p : ℕ) :
    IsZero (((SheafOfModules.toSheaf _).obj F).H' p U)

AlgebraicGeometry.bigFppfCohomology_isZero_of_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/FlatVanishing.lean, line 596. The attribute's comment: “flat_parasitic_vanishing”.

A parasitic module on the big fppf site has no cohomology at a flat object.

public theorem bigFppfCohomology_isZero_of_isParasitic
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [HasSheafify (AlgebraicGeometry.BigFppfOver.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) AddCommGrpCat.{u})]
    {𝒪 : Sheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) RingCat.{u}}
    (F : SheafOfModules.{u} 𝒪)
    (hF : ∀ X : AlgebraicGeometry.BigFppfOver B S hS,
      Flat ((Over.post B.inclusion).obj X).hom → Subsingleton (F.val.obj (Opposite.op X)))
    (U : AlgebraicGeometry.BigFppfOver B S hS)
    (hU : Flat ((Over.post B.inclusion).obj U).hom) (p : ℕ) :
    IsZero (((SheafOfModules.toSheaf _).obj F).H' p U)

AlgebraicGeometry.cohomology_isZero_of_isParasiticFor_zariski, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/TopologyVanishing.lean, line 469. The attribute's comment: “topology_parasitic_vanishing”.

Vanishing on objects open over the base in the big Zariski site.

public theorem cohomology_isZero_of_isParasiticFor_zariski
    (B : AlgebraicGeometry.BigZariskiSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [HasSheafify (AlgebraicGeometry.BigZariskiOver.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (AlgebraicGeometry.BigZariskiOver.topology B S hS) AddCommGrpCat.{u})]
    {𝒪 : Sheaf (AlgebraicGeometry.BigZariskiOver.topology B S hS) RingCat.{u}}
    (G : SheafOfModules.{u} 𝒪)
    (hG : ∀ E : Covering (AlgebraicGeometry.BigZariskiOver B S hS),
      IsIso (((Over.post B.inclusion).obj E.1).hom) →
      AlgebraicGeometry.BigZariskiOver.IsCovering B S hS E →
      ∀ i : E.2.I₀, Subsingleton (G.val.obj (Opposite.op (E.2.X i))))
    (U : AlgebraicGeometry.BigZariskiOver B S hS)
    (hU : IsOpenImmersion ((Over.post B.inclusion).obj U).hom)
    (p : ℕ) :
    IsZero (((SheafOfModules.toSheaf _).obj G).H' p U)

AlgebraicGeometry.cohomology_isZero_of_isParasiticFor_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/TopologyVanishing.lean, line 504. The attribute's comment: “topology_parasitic_vanishing”.

Vanishing on objects étale over the base in the big étale site.

public theorem cohomology_isZero_of_isParasiticFor_etale
    (B : AlgebraicGeometry.BigEtaleSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [HasSheafify (AlgebraicGeometry.BigEtaleOver.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (AlgebraicGeometry.BigEtaleOver.topology B S hS) AddCommGrpCat.{u})]
    {𝒪 : Sheaf (AlgebraicGeometry.BigEtaleOver.topology B S hS) RingCat.{u}}
    (G : SheafOfModules.{u} 𝒪)
    (hG : ∀ E : Covering (AlgebraicGeometry.BigEtaleOver B S hS),
      IsIso (((Over.post B.inclusion).obj E.1).hom) →
      AlgebraicGeometry.BigEtaleOver.IsCovering B S hS E →
      ∀ i : E.2.I₀, Subsingleton (G.val.obj (Opposite.op (E.2.X i))))
    (U : AlgebraicGeometry.BigEtaleOver B S hS)
    (hU : Etale ((Over.post B.inclusion).obj U).hom)
    (p : ℕ) :
    IsZero (((SheafOfModules.toSheaf _).obj G).H' p U)

AlgebraicGeometry.cohomology_isZero_of_isParasiticFor_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/TopologyVanishing.lean, line 538. The attribute's comment: “topology_parasitic_vanishing”.

Vanishing on objects smooth over the base in the big smooth site.

public theorem cohomology_isZero_of_isParasiticFor_smooth
    (B : AlgebraicGeometry.BigSmoothSite.{u}) (S : Scheme.{u}) (hS : S.size < B.cutoff)
    [HasSheafify (AlgebraicGeometry.BigSmoothOver.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (AlgebraicGeometry.BigSmoothOver.topology B S hS) AddCommGrpCat.{u})]
    {𝒪 : Sheaf (AlgebraicGeometry.BigSmoothOver.topology B S hS) RingCat.{u}}
    (G : SheafOfModules.{u} 𝒪)
    (hG : ∀ E : Covering (AlgebraicGeometry.BigSmoothOver B S hS),
      IsIso (((Over.post (ObjectProperty.ι _)).obj E.1).hom) →
      AlgebraicGeometry.BigSmoothOver.IsCovering B S hS E →
      ∀ i : E.2.I₀, Subsingleton (G.val.obj (Opposite.op (E.2.X i))))
    (U : AlgebraicGeometry.BigSmoothOver B S hS)
    (hU : Smooth ((Over.post (ObjectProperty.ι _)).obj U).hom)
    (p : ℕ) :
    IsZero (((SheafOfModules.toSheaf _).obj G).H' p U)

AlgebraicGeometry.cohomology_isZero_of_isParasiticFor_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/TopologyVanishing.lean, line 572. The attribute's comment: “topology_parasitic_vanishing”.

Vanishing on objects syntomic over the base in the big syntomic site.

public theorem cohomology_isZero_of_isParasiticFor_syntomic
    (B : AlgebraicGeometry.BigSyntomicSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [HasSheafify (AlgebraicGeometry.BigSyntomicOver.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (AlgebraicGeometry.BigSyntomicOver.topology B S hS) AddCommGrpCat.{u})]
    {𝒪 : Sheaf (AlgebraicGeometry.BigSyntomicOver.topology B S hS) RingCat.{u}}
    (G : SheafOfModules.{u} 𝒪)
    (hG : ∀ E : Covering (AlgebraicGeometry.BigSyntomicOver B S hS),
      IsIso (((Over.post B.inclusion).obj E.1).hom) →
      AlgebraicGeometry.BigSyntomicOver.IsCovering B S hS E →
      ∀ i : E.2.I₀, Subsingleton (G.val.obj (Opposite.op (E.2.X i))))
    (U : AlgebraicGeometry.BigSyntomicOver B S hS)
    (hU : Syntomic ((Over.post B.inclusion).obj U).hom)
    (p : ℕ) :
    IsZero (((SheafOfModules.toSheaf _).obj G).H' p U)

AlgebraicGeometry.cohomology_isZero_of_isParasiticFor_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/TopologyVanishing.lean, line 602. The attribute's comment: “topology_parasitic_vanishing”.

Vanishing on objects flat and locally of finite presentation over the base in the big fppf site.

public theorem cohomology_isZero_of_isParasiticFor_fppf
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [HasSheafify (AlgebraicGeometry.BigFppfOver.topology B S hS) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) AddCommGrpCat.{u})]
    {𝒪 : Sheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) RingCat.{u}}
    (G : SheafOfModules.{u} 𝒪)
    (hG : ∀ E : Covering (AlgebraicGeometry.BigFppfOver B S hS),
      IsIso (((Over.post B.inclusion).obj E.1).hom) →
      AlgebraicGeometry.BigFppfOver.IsCovering B S hS E →
      ∀ i : E.2.I₀, Subsingleton (G.val.obj (Opposite.op (E.2.X i))))
    (U : AlgebraicGeometry.BigFppfOver B S hS)
    (hU : Flat ((Over.post B.inclusion).obj U).hom ∧
      LocallyOfFinitePresentation ((Over.post B.inclusion).obj U).hom)
    (p : ℕ) :
    IsZero (((SheafOfModules.toSheaf _).obj G).H' p U)

Tag 07AG, a lemma

Tag 07AG in the Stacks Project.

AlgebraicGeometry.bigZariskiPushforward_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/ParasiticPushforward.lean, line 490. The attribute's comment: “big Zariski direct image”.

Direct image of a parasitic module on the big Zariski site is parasitic.

public theorem bigZariskiPushforward_isParasitic
    (B : AlgebraicGeometry.BigZariskiSite.{u}) (T S : B.Schemes) (f : T ⟶ S)
    {𝒪S : Sheaf (AlgebraicGeometry.BigZariskiOver.topology B S.1 S.2) RingCat.{u}}
    {𝒪T : Sheaf (AlgebraicGeometry.BigZariskiOver.topology B T.1 T.2) RingCat.{u}}
    (φ : 𝒪S ⟶
      ((Over.pullback f).sheafPushforwardContinuous RingCat.{u}
        (AlgebraicGeometry.BigZariskiOver.topology B S.1 S.2)
        (AlgebraicGeometry.BigZariskiOver.topology B T.1 T.2)).obj
          𝒪T)
    (F : SheafOfModules.{u} 𝒪T)
    (hF : IsParasitic T.1 (Over.post B.inclusion) F.val) :
    IsParasitic S.1 (Over.post B.inclusion)
      ((SheafOfModules.pushforward.{u} φ).obj F).val

AlgebraicGeometry.bigZariskiHigherDirectImage_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/ParasiticPushforward.lean, line 510. The attribute's comment: “big Zariski higher direct images”.

Every higher direct image of a parasitic module on the big Zariski site is parasitic.

public theorem bigZariskiHigherDirectImage_isParasitic
    (B : AlgebraicGeometry.BigZariskiSite.{u}) (T S : B.Schemes) (f : T ⟶ S)
    {𝒪S : Sheaf (AlgebraicGeometry.BigZariskiOver.topology B S.1 S.2) RingCat.{u}}
    {𝒪T : Sheaf (AlgebraicGeometry.BigZariskiOver.topology B T.1 T.2) RingCat.{u}}
    (φ : 𝒪S ⟶
      ((Over.pullback f).sheafPushforwardContinuous RingCat.{u}
        (AlgebraicGeometry.BigZariskiOver.topology B S.1 S.2)
        (AlgebraicGeometry.BigZariskiOver.topology B T.1 T.2)).obj
          𝒪T)
    (F : SheafOfModules.{u} 𝒪T)
    (hF : IsParasitic T.1 (Over.post B.inclusion) F.val) (i : ℕ) :
    IsParasitic S.1 (Over.post B.inclusion)
      ((Functor.rightDerived (C := SheafOfModules.{u} 𝒪T) (D := SheafOfModules.{u} 𝒪S)
        (SheafOfModules.pushforward.{u} φ) i).obj F).val

AlgebraicGeometry.bigEtalePushforward_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/ParasiticPushforward.lean, line 546. The attribute's comment: “big étale direct image”.

Direct image of a parasitic module on the big étale site is parasitic.

public theorem bigEtalePushforward_isParasitic
    (B : AlgebraicGeometry.BigEtaleSite.{u}) (T S : B.Scheme) (f : T ⟶ S)
    {𝒪S : Sheaf (AlgebraicGeometry.BigEtaleOver.topology B S.1 S.2) RingCat.{u}}
    {𝒪T : Sheaf (AlgebraicGeometry.BigEtaleOver.topology B T.1 T.2) RingCat.{u}}
    (φ : 𝒪S ⟶
      ((Over.pullback f).sheafPushforwardContinuous RingCat.{u}
        (AlgebraicGeometry.BigEtaleOver.topology B S.1 S.2)
        (AlgebraicGeometry.BigEtaleOver.topology B T.1 T.2)).obj
          𝒪T)
    (F : SheafOfModules.{u} 𝒪T)
    (hF : IsParasitic T.1 (Over.post B.inclusion) F.val) :
    IsParasitic S.1 (Over.post B.inclusion)
      ((SheafOfModules.pushforward.{u} φ).obj F).val

AlgebraicGeometry.bigEtaleHigherDirectImage_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/ParasiticPushforward.lean, line 565. The attribute's comment: “big étale higher direct images”.

Higher direct images of a parasitic module on the big étale site are parasitic.

public theorem bigEtaleHigherDirectImage_isParasitic
    (B : AlgebraicGeometry.BigEtaleSite.{u}) (T S : B.Scheme) (f : T ⟶ S)
    {𝒪S : Sheaf (AlgebraicGeometry.BigEtaleOver.topology B S.1 S.2) RingCat.{u}}
    {𝒪T : Sheaf (AlgebraicGeometry.BigEtaleOver.topology B T.1 T.2) RingCat.{u}}
    (φ : 𝒪S ⟶
      ((Over.pullback f).sheafPushforwardContinuous RingCat.{u}
        (AlgebraicGeometry.BigEtaleOver.topology B S.1 S.2)
        (AlgebraicGeometry.BigEtaleOver.topology B T.1 T.2)).obj
          𝒪T)
    (F : SheafOfModules.{u} 𝒪T)
    (hF : IsParasitic T.1 (Over.post B.inclusion) F.val) (i : ℕ) :
    IsParasitic S.1 (Over.post B.inclusion)
      ((Functor.rightDerived (C := SheafOfModules.{u} 𝒪T) (D := SheafOfModules.{u} 𝒪S)
        (SheafOfModules.pushforward.{u} φ) i).obj F).val

AlgebraicGeometry.bigSmoothPushforward_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/ParasiticPushforward.lean, line 601. The attribute's comment: “big smooth direct image”.

Direct image of a parasitic module on the big smooth site is parasitic.

public theorem bigSmoothPushforward_isParasitic
    (B : AlgebraicGeometry.BigSmoothSite.{u}) (T S : B.category) (f : T ⟶ S)
    {𝒪S : Sheaf (AlgebraicGeometry.BigSmoothOver.topology B S.1 S.2) RingCat.{u}}
    {𝒪T : Sheaf (AlgebraicGeometry.BigSmoothOver.topology B T.1 T.2) RingCat.{u}}
    (φ : 𝒪S ⟶
      ((Over.pullback f).sheafPushforwardContinuous RingCat.{u}
        (AlgebraicGeometry.BigSmoothOver.topology B S.1 S.2)
        (AlgebraicGeometry.BigSmoothOver.topology B T.1 T.2)).obj
          𝒪T)
    (F : SheafOfModules.{u} 𝒪T)
    (hF : IsParasitic T.1 (Over.post (ObjectProperty.ι _)) F.val) :
    IsParasitic S.1 (Over.post (ObjectProperty.ι _))
      ((SheafOfModules.pushforward.{u} φ).obj F).val

AlgebraicGeometry.bigSmoothHigherDirectImage_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/ParasiticPushforward.lean, line 620. The attribute's comment: “big smooth higher direct images”.

Higher direct images of a parasitic module on the big smooth site are parasitic.

public theorem bigSmoothHigherDirectImage_isParasitic
    (B : AlgebraicGeometry.BigSmoothSite.{u}) (T S : B.category) (f : T ⟶ S)
    {𝒪S : Sheaf (AlgebraicGeometry.BigSmoothOver.topology B S.1 S.2) RingCat.{u}}
    {𝒪T : Sheaf (AlgebraicGeometry.BigSmoothOver.topology B T.1 T.2) RingCat.{u}}
    (φ : 𝒪S ⟶
      ((Over.pullback f).sheafPushforwardContinuous RingCat.{u}
        (AlgebraicGeometry.BigSmoothOver.topology B S.1 S.2)
        (AlgebraicGeometry.BigSmoothOver.topology B T.1 T.2)).obj
          𝒪T)
    (F : SheafOfModules.{u} 𝒪T)
    (hF : IsParasitic T.1 (Over.post (ObjectProperty.ι _)) F.val) (i : ℕ) :
    IsParasitic S.1 (Over.post (ObjectProperty.ι _))
      ((Functor.rightDerived (C := SheafOfModules.{u} 𝒪T) (D := SheafOfModules.{u} 𝒪S)
        (SheafOfModules.pushforward.{u} φ) i).obj F).val

AlgebraicGeometry.bigSyntomicPushforward_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/ParasiticPushforward.lean, line 656. The attribute's comment: “big syntomic direct image”.

Direct image of a parasitic module on the big syntomic site is parasitic.

public theorem bigSyntomicPushforward_isParasitic
    (B : AlgebraicGeometry.BigSyntomicSite.{u}) (T S : B.category) (f : T ⟶ S)
    {𝒪S : Sheaf (AlgebraicGeometry.BigSyntomicOver.topology B S.1 S.2) RingCat.{u}}
    {𝒪T : Sheaf (AlgebraicGeometry.BigSyntomicOver.topology B T.1 T.2) RingCat.{u}}
    (φ : 𝒪S ⟶
      ((Over.pullback f).sheafPushforwardContinuous RingCat.{u}
        (AlgebraicGeometry.BigSyntomicOver.topology B S.1 S.2)
        (AlgebraicGeometry.BigSyntomicOver.topology B T.1 T.2)).obj
          𝒪T)
    (F : SheafOfModules.{u} 𝒪T)
    (hF : IsParasitic T.1 (Over.post B.inclusion) F.val) :
    IsParasitic S.1 (Over.post B.inclusion)
      ((SheafOfModules.pushforward.{u} φ).obj F).val

AlgebraicGeometry.bigSyntomicHigherDirectImage_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/ParasiticPushforward.lean, line 675. The attribute's comment: “big syntomic higher direct images”.

Higher direct images of a parasitic module on the big syntomic site are parasitic.

public theorem bigSyntomicHigherDirectImage_isParasitic
    (B : AlgebraicGeometry.BigSyntomicSite.{u}) (T S : B.category) (f : T ⟶ S)
    {𝒪S : Sheaf (AlgebraicGeometry.BigSyntomicOver.topology B S.1 S.2) RingCat.{u}}
    {𝒪T : Sheaf (AlgebraicGeometry.BigSyntomicOver.topology B T.1 T.2) RingCat.{u}}
    (φ : 𝒪S ⟶
      ((Over.pullback f).sheafPushforwardContinuous RingCat.{u}
        (AlgebraicGeometry.BigSyntomicOver.topology B S.1 S.2)
        (AlgebraicGeometry.BigSyntomicOver.topology B T.1 T.2)).obj
          𝒪T)
    (F : SheafOfModules.{u} 𝒪T)
    (hF : IsParasitic T.1 (Over.post B.inclusion) F.val) (i : ℕ) :
    IsParasitic S.1 (Over.post B.inclusion)
      ((Functor.rightDerived (C := SheafOfModules.{u} 𝒪T) (D := SheafOfModules.{u} 𝒪S)
        (SheafOfModules.pushforward.{u} φ) i).obj F).val

AlgebraicGeometry.bigFppfPushforward_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/ParasiticPushforward.lean, line 711. The attribute's comment: “big fppf direct image”.

Direct image of a parasitic module on the big fppf site is parasitic.

public theorem bigFppfPushforward_isParasitic
    (B : AlgebraicGeometry.BigFppfSite.{u}) (T S : B.Schemes) (f : T ⟶ S)
    {𝒪S : Sheaf (AlgebraicGeometry.BigFppfOver.topology B S.1 S.2) RingCat.{u}}
    {𝒪T : Sheaf (AlgebraicGeometry.BigFppfOver.topology B T.1 T.2) RingCat.{u}}
    (φ : 𝒪S ⟶
      ((Over.pullback f).sheafPushforwardContinuous RingCat.{u}
        (AlgebraicGeometry.BigFppfOver.topology B S.1 S.2)
        (AlgebraicGeometry.BigFppfOver.topology B T.1 T.2)).obj
          𝒪T)
    (F : SheafOfModules.{u} 𝒪T)
    (hF : IsParasitic T.1 (Over.post B.inclusion) F.val) :
    IsParasitic S.1 (Over.post B.inclusion)
      ((SheafOfModules.pushforward.{u} φ).obj F).val

AlgebraicGeometry.bigFppfHigherDirectImage_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/ParasiticPushforward.lean, line 730. The attribute's comment: “big fppf higher direct images”.

Higher direct images of a parasitic module on the big fppf site are parasitic.

public theorem bigFppfHigherDirectImage_isParasitic
    (B : AlgebraicGeometry.BigFppfSite.{u}) (T S : B.Schemes) (f : T ⟶ S)
    {𝒪S : Sheaf (AlgebraicGeometry.BigFppfOver.topology B S.1 S.2) RingCat.{u}}
    {𝒪T : Sheaf (AlgebraicGeometry.BigFppfOver.topology B T.1 T.2) RingCat.{u}}
    (φ : 𝒪S ⟶
      ((Over.pullback f).sheafPushforwardContinuous RingCat.{u}
        (AlgebraicGeometry.BigFppfOver.topology B S.1 S.2)
        (AlgebraicGeometry.BigFppfOver.topology B T.1 T.2)).obj
          𝒪T)
    (F : SheafOfModules.{u} 𝒪T)
    (hF : IsParasitic T.1 (Over.post B.inclusion) F.val) (i : ℕ) :
    IsParasitic S.1 (Over.post B.inclusion)
      ((Functor.rightDerived (C := SheafOfModules.{u} 𝒪T) (D := SheafOfModules.{u} 𝒪S)
        (SheafOfModules.pushforward.{u} φ) i).obj F).val

Tag 0756, a lemma

Tag 0756 in the Stacks Project.

AlgebraicGeometry.bigFppfCohomology_map_bijective_of_isParasitic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/FlatCohomologyComparison.lean, line 299. The attribute's comment: “cohomology comparison step, from Tag 0755”.

A morphism of sheaves of 𝒪-modules on the big fppf site over S whose kernel and cokernel are parasitic induces isomorphisms H^p(U, ℱ) → H^p(U, 𝒢) at every object U flat over S.

This is the step of Stacks 0756 which rests on Stacks 0755: the kernel and the cokernel have vanishing cohomology at U by AlgebraicGeometry.bigFppfCohomology_isZero_of_isParasitic, and a morphism with that property is an isomorphism on cohomology. The source lemma then identifies H^p(U, ℱ) with the small-site cohomology H^p(U, 𝒢|_{U_τ}) by Stacks 03DW, which this statement does not assert.

The parasitic hypotheses are the pointwise expansion of AlgebraicGeometry.IsParasitic, as in AlgebraicGeometry.bigFppfCohomology_isZero_of_isParasitic, and the kernel and cokernel are those of the category of sheaves of 𝒪-modules.

The clause string says which step this is. Its hypotheses are part (2) of [Stacks, Tag 06ZL] — vanishing at every object flat over S, finite presentation not assumed — whereas 0756 derives part (1), vanishing at the objects flat and locally of finite presentation over S. The step in that second form is AlgebraicGeometry.bigFppfCohomology_map_bijective_of_isParasiticFor below, which carries the same tag with a clause string naming it.

public theorem bigFppfCohomology_map_bijective_of_isParasitic
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [HasSheafify (AlgebraicGeometry.BigFppfOver.topology B S hS) AddCommGrpCat.{u}]
    [(AlgebraicGeometry.BigFppfOver.topology B S hS).WEqualsLocallyBijective AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) AddCommGrpCat.{u})]
    {𝒪 : Sheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) RingCat.{u}}
    {F G : SheafOfModules.{u} 𝒪} (φ : F ⟶ G)
    (hker : ∀ X : AlgebraicGeometry.BigFppfOver B S hS,
      Flat ((Over.post B.inclusion).obj X).hom →
        Subsingleton ((kernel φ).val.obj (Opposite.op X)))
    (hcoker : ∀ X : AlgebraicGeometry.BigFppfOver B S hS,
      Flat ((Over.post B.inclusion).obj X).hom →
        Subsingleton ((cokernel φ).val.obj (Opposite.op X)))
    (U : AlgebraicGeometry.BigFppfOver B S hS)
    (hU : Flat ((Over.post B.inclusion).obj U).hom) (p : ℕ) :
    Function.Bijective
      (Stacks.Cohomology.LongExactSequence.map.{w}
        ((SheafOfModules.toSheaf 𝒪).map φ) p U)

AlgebraicGeometry.bigFppfCohomology_map_bijective_of_isParasiticFor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/FlatCohomologyComparison.lean, line 358. The attribute's comment: “cohomology comparison step, from Tag 0755, at the objects flat and locally of finite presentation over S, which is the shape 0756 uses”.

A morphism of sheaves of 𝒪-modules on the big fppf site over S whose kernel and cokernel are parasitic for the fppf topology induces isomorphisms H^p(U, ℱ) → H^p(U, 𝒢) at every object U flat and locally of finite presentation over S.

This is the step of [Stacks, Tag 0756] which rests on [Stacks, Tag 0755], in the form 0756 uses it: the kernel and the cokernel have vanishing cohomology at U by AlgebraicGeometry.cohomology_isZero_of_isParasiticFor_fppf, which is part (1) of 0755, and a morphism with that property is an isomorphism on cohomology by Stacks.Cohomology.LongExactSequence.bijective_map_of_subsingleton_kernel_cokernel.

The hypotheses are AlgebraicGeometry.IsParasiticFor, part (2) of [Stacks, Tag 06ZL], for the fppf coverings of S: vanishing on the members of fppf coverings of the base, which are exactly the objects flat and locally of finite presentation over S. They are what 0756 derives from its assumptions (1) and (2), and they are weaker than the AlgebraicGeometry.IsParasitic of AlgebraicGeometry.bigFppfCohomology_map_bijective_of_isParasitic, which asks for vanishing at every flat object, finite presentation not assumed. Correspondingly the conclusion here is at the objects flat and locally of finite presentation, which is where 0756 states it.

This is the form with parasiticity hypothesised, which is what an arbitrary morphism needs. For a morphism which is an isomorphism on sections over every such object the two hypotheses are themselves theorems, and the resulting statement is AlgebraicGeometry.bigFppfCohomology_map_bijective_of_isIso_sections (StacksFrontier.AlgebraicGeometry.Descent.Parasitic.FlatCohomologySectionwiseIso). The identification of H^p(U, ℱ) with the small-site cohomology H^p(U, 𝒢|_{U_τ}), which is the conclusion of 0756, is established at τ = Zariski and U = S by AlgebraicGeometry.BigFppfOver.zariskiSmallSiteCohomologyAddEquiv (StacksFrontier.AlgebraicGeometry.Descent.Parasitic.FlatCohomologySmallSiteComparison).

public theorem bigFppfCohomology_map_bijective_of_isParasiticFor
    (B : AlgebraicGeometry.BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    [HasSheafify (AlgebraicGeometry.BigFppfOver.topology B S hS) AddCommGrpCat.{u}]
    [(AlgebraicGeometry.BigFppfOver.topology B S hS).WEqualsLocallyBijective AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) AddCommGrpCat.{u})]
    {𝒪 : Sheaf (AlgebraicGeometry.BigFppfOver.topology B S hS) RingCat.{u}}
    {F G : SheafOfModules.{u} 𝒪} (φ : F ⟶ G)
    (hker : AlgebraicGeometry.IsParasiticFor S (Over.post B.inclusion)
      (AlgebraicGeometry.BigFppfOver.IsCovering B S hS) (kernel φ).val)
    (hcoker : AlgebraicGeometry.IsParasiticFor S (Over.post B.inclusion)
      (AlgebraicGeometry.BigFppfOver.IsCovering B S hS) (cokernel φ).val)
    (U : AlgebraicGeometry.BigFppfOver B S hS)
    (hU : Flat ((Over.post B.inclusion).obj U).hom ∧
      LocallyOfFinitePresentation ((Over.post B.inclusion).obj U).hom) (p : ℕ) :
    Function.Bijective
      (Stacks.Cohomology.LongExactSequence.map.{w}
        ((SheafOfModules.toSheaf 𝒪).map φ) p U)

AlgebraicGeometry.BigFppfOver.flatSmallEtaleSiteCohomologyAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/FlatCohomologyEtaleConclusion.lean, line 277. The attribute's comment: “étale topology”.

The conclusion of [Stacks, Tag 0756] at τ = étale. Let B be a big fppf site, S a scheme below its cutoff and 𝒢 a sheaf of 𝒪-modules on (Sch/S)_fppf such that

1. 𝒢|_{S_étale} is quasi-coherent on the small étale site of S, and
2. for every object of (Sch/S)_fppf flat and locally of finite presentation over S, with structure morphism g : X ⟶ S, the canonical map ε_g^*(𝒢|_{S_étale}) ⟶ 𝒢|_{X_étale} of AlgebraicGeometry.BigFppfOver.etaleClause2Map is an isomorphism; this is the adjoint transpose of the restriction map 𝒢|_{S_étale} ⟶ ε_{g,*}(𝒢|_{X_étale}) by AlgebraicGeometry.BigFppfOver.etaleClause2Map_eq_homEquiv_symm.

Then for every object U of (Sch/S)_fppf flat and locally of finite presentation over S, with scheme X, and every p,

H^p(U, 𝒢)  ≅  H^p(U, 𝒢|_{U_étale}).

The left-hand side is global cohomology of 𝒢|_{(Sch/X)_fppf} on the big fppf site of X, which is the reading of cohomology over an object that AlgebraicGeometry.BigFppfOver.flatSmallSiteCohomologyAddEquiv fixes at τ = Zariski; the right-hand side is the cohomology of the size-bounded small étale site of X of [Stacks, Tag 021B] with values in the restriction of 𝒢 along a_X : ((Sch/X)_fppf, 𝒪) ⟶ (X_étale, 𝒪).

The attribute records the topology: this is the tag at τ = étale. See AlgebraicGeometry.BigFppfOver.flatSmallSiteCohomologyAddEquiv for the tag at τ = Zariski.

public def flatSmallEtaleSiteCohomologyAddEquiv (p : ℕ) :
    Sheaf.H.{u} ((SheafOfModules.toSheaf (structureSheaf B (objScheme B S hS U)
        (contains_objScheme B S hS U))).obj ((objRestrict B S hS U).obj G)) p ≃+
      Sheaf.H.{u} ((SheafOfModules.toSheaf (SmallEtale.structureSheaf B.toBigEtaleSite
        (objScheme B S hS U) (contains_objScheme B S hS U))).obj
          (objSmallEtaleRestrict B S hS U G)) p

AlgebraicGeometry.BigFppfOver.flatSmallSiteCohomologyAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/FlatCohomologyGeneralBase.lean, line 457. The attribute's comment: “Zariski topology”.

The conclusion of [Stacks, Tag 0756] at τ = Zar. Let B be a big fppf site, S a scheme below its cutoff and 𝒢 a sheaf of 𝒪-modules on (Sch/S)_fppf such that

1. 𝒢|_{S_Zar} is quasi-coherent, and
2. for every object of (Sch/S)_fppf flat and locally of finite presentation over S, with structure morphism g : X ⟶ S, the canonical map g^*(𝒢|_{S_Zar}) ⟶ 𝒢|_{X_Zar}, AlgebraicGeometry.BigFppfOver.zariskiClause2Map, is an isomorphism; this is the adjoint transpose of the restriction map 𝒢|_{S_Zar} ⟶ g_*(𝒢|_{X_Zar}) by AlgebraicGeometry.BigFppfOver.zariskiClause2Map_eq_homEquiv_symm, and it is an isomorphism exactly when the transpose of restriction along g^{-1}V ⟶ V is, by AlgebraicGeometry.BigFppfOver.isIso_zariskiClause2Map_iff.

Then for every object U of (Sch/S)_fppf flat and locally of finite presentation over S, with scheme X, and every p,

H^p(U, 𝒢)  ≅  H^p(U, 𝒢|_{U_Zar}).

The left-hand side is global cohomology of 𝒢|_{(Sch/X)_fppf} on the big fppf site of X, the localization of (Sch/S)_fppf at U by [Stacks, Tag 06WI]; the right-hand side is the cohomology of the site of opens of X with values in the restriction of 𝒢 along the inclusion of the small Zariski site of X. See AlgebraicGeometry.BigFppfOver.flatSmallZariskiSiteCohomologyAddEquiv for the same statement with that side read on the site AlgebraicGeometry.SmallZariski of [Stacks, Tag 020T] (2).

This is AlgebraicGeometry.BigFppfOver.zariskiSmallSiteCohomologyAddEquiv — the conclusion at the base of a big site — applied at the base X to 𝒢|_{(Sch/X)_fppf}. Its two hypotheses there are clause (1) over X, which is AlgebraicGeometry.BigFppfOver.isQuasicoherent_objZariskiRestrict, and clause (2) over X, which is AlgebraicGeometry.BigFppfOver.isIso_zariskiClause2Map_objRestrict and rests on the mate square AlgebraicGeometry.BigFppfOver.mateSquare_objRestrictCounit.

The attribute records the topology: this is the tag at τ = Zariski, and nothing here claims the étale half; that is AlgebraicGeometry.BigFppfOver.flatSmallEtaleSiteCohomologyAddEquiv, in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/FlatCohomologyEtaleConclusion.lean.

public def flatSmallSiteCohomologyAddEquiv (p : ℕ) :
    Sheaf.H.{u} ((SheafOfModules.toSheaf (structureSheaf B (objScheme B S hS U)
        (contains_objScheme B S hS U))).obj ((objRestrict B S hS U).obj G)) p ≃+
      Sheaf.H.{u} ((SheafOfModules.toSheaf (objScheme B S hS U).ringCatSheaf).obj
        ((restrictModule B (objScheme B S hS U) (contains_objScheme B S hS U)).obj
          ((objRestrict B S hS U).obj G))) p

AlgebraicGeometry.BigFppfOver.flatSmallZariskiSiteCohomologyAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Parasitic/FlatCohomologyGeneralBase.lean, line 488. The attribute's comment: “Zariski topology, with the small site read as in 020T (2)”.

The conclusion of [Stacks, Tag 0756] at τ = Zar, with the right-hand side on the small Zariski site. Under the hypotheses of AlgebraicGeometry.BigFppfOver.flatSmallSiteCohomologyAddEquiv, for every object U of (Sch/S)_fppf flat and locally of finite presentation over S, with scheme X, and every p,

H^p(U, 𝒢)  ≅  H^p(X_Zar, (𝒢|_{X_Zar})^a),

the right-hand side being the cohomology of the small Zariski site of [Stacks, Tag 020T] (2) with values in the associated sheaf of [Stacks, Tag 03DU] (4) at τ = Zariski. This is the previous statement composed with the small Zariski link of [Stacks, Tag 03DW] clause (2), AlgebraicGeometry.smallZariskiQuasiCoherentSiteCohomologyAddEquiv.

The big Zariski site BZ carrying X_Zar is unrelated to the big fppf site B: the restriction 𝒢|_{X_Zar} is produced as an 𝒪_X-module and only then read on X_Zar.

The attribute records the topology: this is the tag at τ = Zariski.

public def flatSmallZariskiSiteCohomologyAddEquiv (BZ : BigZariskiSite.{u})
    (hXZ : BZ.Contains (objScheme B S hS U)) (p : ℕ) :
    Sheaf.H.{u} ((SheafOfModules.toSheaf (structureSheaf B (objScheme B S hS U)
        (contains_objScheme B S hS U))).obj ((objRestrict B S hS U).obj G)) p ≃+
      Sheaf.H.{u} (@smallZariskiAssociatedSheaf BZ (objScheme B S hS U) hXZ
        ((restrictModule B (objScheme B S hS U) (contains_objScheme B S hS U)).obj
          ((objRestrict B S hS U).obj G))
        (isQuasicoherent_objZariskiRestrict B S hS U G hqc (hcl2 U hU₁ hU₂))) p

Sources

• Section 35.12, Tag 07AF
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.IsParasitic · AlgebraicGeometry.IsParasiticFor · AlgebraicGeometry.bigZariskiCohomology_isZero_of_isParasitic · AlgebraicGeometry.bigEtaleCohomology_isZero_of_isParasitic · AlgebraicGeometry.bigSmoothCohomology_isZero_of_isParasitic · AlgebraicGeometry.bigSyntomicCohomology_isZero_of_isParasitic · AlgebraicGeometry.bigFppfCohomology_isZero_of_isParasitic · AlgebraicGeometry.cohomology_isZero_of_isParasiticFor_zariski

Section35.13 Fpqc coverings are universal effective epimorphisms#

Section 35.13 of the Stacks Project, Tag 023P. 8 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02KI, a lemma

Tag 02KI in the Stacks Project.

AlgebraicGeometry.Scheme.pullbackComparison_forget_self_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EffectiveEpi/Points.lean, line 43.

Stacks 02KI. For a morphism of schemes f : X ⟶ S the natural map |X ×_S X| → |X| ×_{|S|} |X| of underlying sets is surjective.

public theorem pullbackComparison_forget_self_surjective {X S : Scheme.{u}} (f : X ⟶ S) :
    Function.Surjective (pullbackComparison forget f f)

Tag 0EUA, a lemma

Tag 0EUA in the Stacks Project.

AlgebraicGeometry.quasicoherentSectionsEqualizer_iff_isUniversalEffectiveEpiFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EffectiveEpi/QuasicoherentSectionsEqualizer/UniversalEffectiveEpi.lean, line 787.

Stacks Project, Tag 0EUA. A family of morphisms of affine schemes satisfies the global-section equalizer condition for every quasi-coherent module if and only if it is a universal effective epimorphic family in the category of affine schemes.

theorem quasicoherentSectionsEqualizer_iff_isUniversalEffectiveEpiFamily
    {I : Type w} (X : AffineScheme.{u}) (U : I → AffineScheme.{u})
    (f : ∀ i, U i ⟶ X) :
    IsQuasicoherentSectionsEqualizer X U f ↔
      StacksEffectiveEpi.IsUniversalEffectiveEpiFamily U f

Tag 0EUB, a lemma

Tag 0EUB in the Stacks Project.

AlgebraicGeometry.jointlySurjective_of_isUniversalEffectiveEpiFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EffectiveEpi/Surjective.lean, line 56. The attribute's comment: “schemes_surjective”. References: SGA 3 IV (6.7.2), “univ. eff. epi ⇒ surj”; SGA 3 IV (1.3), “special case”.

A universal effective epimorphic family of schemes is jointly surjective on the underlying spaces.

theorem jointlySurjective_of_isUniversalEffectiveEpiFamily
    {I : Type w} {X : Scheme.{u}} (U : I → Scheme.{u})
    (f : ∀ i, U i ⟶ X)
    (h : StacksEffectiveEpi.IsUniversalEffectiveEpiFamily U f) :
    ∀ x : X, ∃ i, x ∈ Set.range (f i)

AlgebraicGeometry.exists_preimage_of_isUniversalEffectiveEpiFamily, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EffectiveEpi/Surjective.lean, line 74. The attribute's comment: “affine_schemes_surjective”. References: SGA 3 IV (6.7.2), “affine case”.

A universal effective epimorphic family of affine schemes is jointly surjective.

theorem exists_preimage_of_isUniversalEffectiveEpiFamily
    {I : Type w} (X : AffineScheme.{u}) (U : I → AffineScheme.{u})
    (f : ∀ i, U i ⟶ X)
    (h : StacksEffectiveEpi.IsUniversalEffectiveEpiFamily U f) :
    ∀ x : X.obj, ∃ (i : I) (y : (U i).obj),
      (AffineScheme.forgetToScheme.map (f i)) y = x

Tag 0EUC, a lemma

Tag 0EUC in the Stacks Project.

AlgebraicGeometry.isUniversalEffectiveEpiFamily_of_affine_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EffectiveEpi/AffineBase.lean, line 100.

A family of morphisms of schemes is universally effective epimorphic if all its base changes to affine schemes are effective epimorphic families.

theorem isUniversalEffectiveEpiFamily_of_affine_baseChange
    {I : Type w} {X : Scheme.{u}} (X' : I → Scheme.{u}) (f : ∀ i, X' i ⟶ X)
    (h : ∀ (Y : Scheme.{u}) [IsAffine Y] (g : Y ⟶ X),
      StacksEffectiveEpi.IsEffectiveEpiFamily
        (fun i => pullback (f i) g) (fun i => pullback.snd (f i) g)) :
    StacksEffectiveEpi.IsUniversalEffectiveEpiFamily X' f

Tag 0EUD, a lemma

Tag 0EUD in the Stacks Project.

AlgebraicGeometry.isUniversalEffectiveEpiFamily_of_affine_of_submersive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EffectiveEpi/FromAffine.lean, line 403.

Stacks Project, Tag 0EUD. A universally effective epimorphic family of affine schemes whose every affine base change is submersive is a universally effective epimorphic family in schemes.

public theorem isUniversalEffectiveEpiFamily_of_affine_of_submersive
    {I : Type w} (X : AffineScheme.{u}) (U : I → AffineScheme.{u})
    (f : ∀ i, U i ⟶ X)
    (h_affine : StacksEffectiveEpi.IsUniversalEffectiveEpiFamily U f)
    (h_submersive : ∀ (Y : Scheme.{u}) [IsAffine Y] (g : Y ⟶ X.obj),
      Topology.IsQuotientMap
        (fun p : Σ i : I,
            (pullback (AffineScheme.forgetToScheme.map (f i)) g : Scheme.{u}) =>
          (pullback.snd (AffineScheme.forgetToScheme.map (f p.1)) g).base p.2)) :
    StacksEffectiveEpi.IsUniversalEffectiveEpiFamily
      (fun i => (U i).obj) (fun i => AffineScheme.forgetToScheme.map (f i))

Tag 03N0, a lemma

Tag 03N0 in the Stacks Project.

AlgebraicGeometry.existsUnique_isOpen_preimage_eq_of_mem_fpqcPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/OpenSubsetFpqc.lean, line 202. References: SGA 1 VIII (4.4), “more general”.

Stacks 03N0. Let {f i : X i ⟶ T} be an fpqc covering of schemes and let W i be an open subset of X i for each i, such that the two projections of X i ×_T X j pull W i and W j back to the same open subset for all i and j. Then there is a unique open subset V of T whose inverse image in X i is W i for every i.

theorem existsUnique_isOpen_preimage_eq_of_mem_fpqcPrecoverage {I : Type v} {T : Scheme.{u}}
    (X : I → Scheme.{u}) (f : ∀ i, X i ⟶ T)
    (hf : Presieve.ofArrows X f ∈ Scheme.fpqcPrecoverage T)
    (W : ∀ i, (X i).Opens)
    (hW : ∀ i j, pullback.fst (f i) (f j) ⁻¹ᵁ W i = pullback.snd (f i) (f j) ⁻¹ᵁ W j) :
    ∃! V : T.Opens, ∀ i, f i ⁻¹ᵁ V = W i

AlgebraicGeometry.existsUnique_isOpen_preimage_eq_of_flat_of_quasiCompact_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/OpenSubsetSingleMorphism.lean, line 60. The attribute's comment: “covering by a single surjective flat quasi-compact morphism”.

An open subset descends along a surjective flat quasi-compact morphism. Let f : T' ⟶ T be a surjective, flat, quasi-compact morphism of schemes and let W' ⊆ T' be open with pr₀⁻¹(W') = pr₁⁻¹(W') in T' ×_T T'. Then there is a unique open W ⊆ T with W' = f⁻¹(W).

theorem existsUnique_isOpen_preimage_eq_of_flat_of_quasiCompact_of_surjective {W' : Set T'}
    (hW' : IsOpen W')
    (hcompat : (pullback.fst f f).base ⁻¹' W' = (pullback.snd f f).base ⁻¹' W') :
    ∃! W : Set T, IsOpen W ∧ f.base ⁻¹' W = W'

AlgebraicGeometry.existsUnique_opens_preimage_eq_of_flat_of_quasiCompact_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/OpenSubsetSingleMorphism.lean, line 78. The attribute's comment: “covering by a single surjective flat quasi-compact morphism, as open subschemes”.

An open subscheme descends along a surjective flat quasi-compact morphism. For f : T' ⟶ T surjective, flat and quasi-compact, an open subscheme W' of T' whose two preimages in T' ×_T T' agree is the preimage of a unique open subscheme of T.

theorem existsUnique_opens_preimage_eq_of_flat_of_quasiCompact_of_surjective (W' : T'.Opens)
    (hcompat : (pullback.fst f f).base ⁻¹' (W' : Set T') =
      (pullback.snd f f).base ⁻¹' (W' : Set T')) :
    ∃! W : T.Opens, f ⁻¹ᵁ W = W'

Tag 023Q, a lemma

Tag 023Q in the Stacks Project.

isUniversalEffectiveEpi_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Representable/EffectiveEpiFamily.lean, line 365. The attribute's comment: “every fpqc covering family of schemes is a universal effective epimorphism, in the unpacked equalizer form of Stacks 00WP: along every base change of the family, a morphism to any scheme is determined by, and glues from, a pullback-compatible family on the members”. References: SGA 1 VIII (5.3), “more general”; SGA 3 IV (3.4), “more general”; SGA 3 IV (6.3.1), “(iii), fpqc case (T1)”; SGA 3 IX (5.4), “more general”; SGA 3 XI (3.9), “partial”.

Main statement (Stacks Tag 023Q). Every fpqc covering of schemes is a universal effective epimorphism in the category of schemes.

theorem isUniversalEffectiveEpi_of_isFpqcCovering
    {ι : Type*} {T : Scheme} (T' : ι → Scheme) (f : ∀ i, T' i ⟶ T)
    (hf : IsFpqcCoveringFamily T' f) :
    IsUniversalEffectiveEpi T' f

Tag 0BMN, a lemma

Tag 0BMN in the Stacks Project.

AlgebraicGeometry.isColimit_cofork_of_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EffectiveEpi/FpqcCoequalizer.lean, line 65.

Stacks Project, Tag 0BMN. A coequalizer of schemes can be checked after an fpqc covering provided it is also a coequalizer on every pairwise overlap.

theorem isColimit_cofork_of_fpqc {X Y Z : Scheme.{u}} (a b : X ⟶ Y) (c : Y ⟶ Z)
    (h : a ≫ c = b ≫ c) {I : Type v} (Z' : I → Scheme.{u}) (f : ∀ i, Z' i ⟶ Z)
    (hfpqc : Presieve.ofArrows Z' f ∈ Scheme.fpqcPrecoverage Z)
    (hlocal : ∀ i, Nonempty (IsColimit (baseChangeCofork a b c h (f i))))
    (hoverlap : ∀ i j, Nonempty (IsColimit
      (baseChangeCofork a b c h (pullback.fst (f i) (f j) ≫ f i)))) :
    Nonempty (IsColimit (Cofork.ofπ c h))

Sources

• Section 35.13, Tag 023P
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Scheme.pullbackComparison_forget_self_surjective · AlgebraicGeometry.quasicoherentSectionsEqualizer_iff_isUniversalEffectiveEpiFamily · AlgebraicGeometry.jointlySurjective_of_isUniversalEffectiveEpiFamily · AlgebraicGeometry.exists_preimage_of_isUniversalEffectiveEpiFamily · AlgebraicGeometry.isUniversalEffectiveEpiFamily_of_affine_baseChange · AlgebraicGeometry.isUniversalEffectiveEpiFamily_of_affine_of_submersive · AlgebraicGeometry.existsUnique_isOpen_preimage_eq_of_mem_fpqcPrecoverage · AlgebraicGeometry.existsUnique_isOpen_preimage_eq_of_flat_of_quasiCompact_of_surjective

Section35.14 Descent of finiteness and smoothness properties of morphisms#

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

Tag 02KK, a lemma

Tag 02KK in the Stacks Project.

RingHom.finitePresentation_of_comp_of_faithfullyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/MorphismProperty/FaithfullyFlatRing.lean, line 98. References: EGA IV (11.3.17), “finite presentation case”; EGA IV (11.3.16), “affine, fin. pres. case”; SGA 3 V (9.1), “affine, finite pres.”; SGA 3 XIX (2.1), “special case”.

Stacks Project, Tag 02KK. If R → B is of finite presentation and A → B is faithfully flat and of finite presentation, then R → A is of finite presentation.

theorem finitePresentation_of_comp_of_faithfullyFlat
    {R : Type u} {A : Type v} {B : Type w} [CommRing R] [CommRing A] [CommRing B]
    (f : R →+* A) (g : A →+* B) (hcomp : (g.comp f).FinitePresentation)
    (hff : g.FaithfullyFlat) (hfp : g.FinitePresentation) : f.FinitePresentation

Tag 0367, a lemma

Tag 0367 in the Stacks Project.

RingHom.finiteType_of_comp_of_faithfullyFlat_of_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/MorphismProperty/FaithfullyFlatRing.lean, line 167. References: EGA IV (11.3.17), “finite type case”; EGA IV (11.3.16), “affine, finite type case”; EGA IV (17.7.5), “affine schemes”; SGA 3 V (9.1), “affine, finite type”.

Stacks Project, Tag 0367. If R → A → B are ring maps, the composite is of finite type, and A → B is faithfully flat and of finite presentation, then R → A is of finite type.

theorem finiteType_of_comp_of_faithfullyFlat_of_finitePresentation
    {R : Type u} {A : Type v} {B : Type w}
    [CommRing R] [CommRing A] [CommRing B]
    {f : R →+* A} {g : A →+* B}
    (hgf : (g.comp f).FiniteType) (hflat : g.FaithfullyFlat)
    (hfp : g.FinitePresentation) :
    f.FiniteType

Tag 02KL, a lemma

Tag 02KL in the Stacks Project.

AlgebraicGeometry.locallyOfFinitePresentation_of_comp_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/MorphismProperty/LocalFiniteness.lean, line 183. The attribute's comment: “locally of finite presentation”. References: EGA IV (17.7.5), “(ii)”; EGA IV (11.3.16), “loc. fin. presentation”.

Stacks Project, Tag 02KL (finite-presentation case). Local finite presentation descends through a surjective flat morphism which is locally of finite presentation.

theorem locallyOfFinitePresentation_of_comp_of_fppf
    {X Y S : Scheme.{u}} (f : X ⟶ Y) (q : Y ⟶ S)
    [Surjective f] [Flat f] [LocallyOfFinitePresentation f]
    [LocallyOfFinitePresentation (f ≫ q)] :
    LocallyOfFinitePresentation q

AlgebraicGeometry.locallyOfFiniteType_of_comp_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/MorphismProperty/LocalFiniteness.lean, line 196. The attribute's comment: “locally of finite type”. References: EGA IV (17.7.5), “(i)”; EGA IV (11.3.16), “locally of finite type”.

Stacks Project, Tag 02KL (finite-type case). Local finite type descends through a surjective flat morphism which is locally of finite presentation.

theorem locallyOfFiniteType_of_comp_of_fppf
    {X Y S : Scheme.{u}} (f : X ⟶ Y) (q : Y ⟶ S)
    [Surjective f] [Flat f] [LocallyOfFinitePresentation f]
    [LocallyOfFiniteType (f ≫ q)] :
    LocallyOfFiniteType q

Tag 02KM, a lemma

Tag 02KM in the Stacks Project.

Stacks.Smooth.smooth_of_comp_surjective_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmoothDescent.lean, line 143. The attribute's comment: “smooth_case”.

Stacks Project, Tag 02KM (smooth case). If f is surjective and smooth and f ≫ q is smooth, then q is smooth.

This is also Stacks 02K5: there the target of f ≫ q is additionally assumed locally of finite presentation, which that source's own footnote observes is implied by the other hypotheses.

theorem smooth_of_comp_surjective_smooth (f : X ⟶ Y) (q : Y ⟶ S) [Surjective f] [Smooth f]
    [Smooth (f ≫ q)] : Smooth q

Stacks.Etale.etale_of_comp_surjective_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SurjectiveEtaleDescent.lean, line 76. The attribute's comment: “etale_case”. References: EGA IV (17.7.5), “special case”.

Stacks 02KM, étale case. If f : X ⟶ Y is surjective and étale and the composite f ≫ q is étale, then q : Y ⟶ S is étale.

The missing hypothesis of Tag 02K6, that q be locally of finite presentation, follows from Tag 02KL: f is surjective, flat and locally of finite presentation, and f ≫ q is locally of finite presentation because it is étale.

theorem etale_of_comp_surjective_etale {X Y S : Scheme.{u}}
    (f : X ⟶ Y) (q : Y ⟶ S) [Surjective f] [Etale f] [Etale (f ≫ q)] :
    Etale q

Stacks.Syntomic.syntomic_of_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SyntomicLciDescent.lean, line 317. The attribute's comment: “syntomic_case”.

Stacks Project, Tag 02KM (syntomic case). Syntomicity descends along a surjective syntomic morphism: if f : X ⟶ Y is surjective and syntomic and f ≫ q is syntomic, then q : Y ⟶ S is syntomic.

This is the syntomic one of the lemma's three cases; the étale case is Stacks.Etale.etale_of_comp_surjective_etale and the smooth case is Stacks.Smooth.smooth_of_comp_surjective_smooth.

theorem syntomic_of_comp (f : X ⟶ Y) (q : Y ⟶ S) [Surjective f] (hf : Syntomic f)
    (hcomp : Syntomic (f ≫ q)) : Syntomic q

Tag 05B5, a lemma

Tag 05B5 in the Stacks Project.

Stacks.Smooth.smooth_of_comp_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmoothDescent.lean, line 116. The attribute's comment: “smooth_permanence”.

Stacks Project, Tag 05B5 (smooth case). Smoothness descends along a surjective flat morphism which is locally of finite presentation: if f : X ⟶ Y is surjective, flat and locally of finite presentation and f ≫ q is smooth, then q : Y ⟶ S is smooth.

theorem smooth_of_comp_of_fppf (f : X ⟶ Y) (q : Y ⟶ S) [Surjective f] [Flat f]
    [LocallyOfFinitePresentation f] [Smooth (f ≫ q)] : Smooth q

Stacks.Etale.etale_of_comp_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/Descent.lean, line 169. The attribute's comment: “etale_permanence”.

Stacks Project, Tag 05B5 (étale case). Étaleness descends along a surjective flat morphism which is locally of finite presentation: if f : X ⟶ Y is surjective, flat and locally of finite presentation and f ≫ q is étale, then q : Y ⟶ S is étale.

theorem etale_of_comp_of_fppf (f : X ⟶ Y) (q : Y ⟶ S) [Surjective f] [Flat f]
    [LocallyOfFinitePresentation f] [Etale (f ≫ q)] : Etale q

Tag 05B7, a lemma

Tag 05B7 in the Stacks Project.

AlgebraicGeometry.syntomic_of_comp_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SyntomicDescent.lean, line 130. The attribute's comment: “q_syntomic”.

Stacks Project, Tag 05B7. Syntomicity descends along a surjective flat morphism which is locally of finite presentation: if f : X ⟶ Y is surjective, flat and locally of finite presentation and f ≫ q is syntomic, then q : Y ⟶ S is syntomic.

theorem syntomic_of_comp_of_fppf (f : X ⟶ Y) (q : Y ⟶ S) [Surjective f] [Flat f]
    [LocallyOfFinitePresentation f] (hp : Syntomic (f ≫ q)) : Syntomic q

AlgebraicGeometry.syntomic_of_syntomic_comp_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/Descent/Fppf.lean, line 101. The attribute's comment: “f_syntomic”.

Stacks Project, Tag 05B7. A surjective flat morphism locally of finite presentation is syntomic as soon as its composite with another morphism is syntomic.

theorem syntomic_of_syntomic_comp_of_fppf [Surjective f] [Flat f]
    [LocallyOfFinitePresentation f] (hp : Syntomic (f ≫ q)) : Syntomic f

AlgebraicGeometry.syntomic_of_syntomic_comp_of_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Syntomic/FactorSyntomic.lean, line 198. The attribute's comment: “f_syntomic”.

If f : X ⟶ Y is surjective, flat and locally of finite presentation and f ≫ q is syntomic, then f is syntomic.

theorem syntomic_of_syntomic_comp_of_fppf (f : X ⟶ Y) (q : Y ⟶ S) [Surjective f] [Flat f]
    [LocallyOfFinitePresentation f] (hcomp : Syntomic (f ≫ q)) : Syntomic f

Tag 06NB, a lemma

Tag 06NB in the Stacks Project.

AlgebraicGeometry.flat_of_comp_of_fppf_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/MorphismProperty/FppfRefinement.lean, line 114. The attribute's comment: “flat”.

Stacks Project, Tag 06NB (flat). If f ≫ g is flat and the singleton family consisting of f is refined by an fppf covering of Y, then g is flat.

theorem flat_of_comp_of_fppf_refinement
    {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [Flat (f ≫ g)]
    (h : ∃ 𝒰 : Y.Cover.{v} Scheme.fppfPrecoverage,
      Nonempty (𝒰.toPreZeroHypercover.Hom (PreZeroHypercover.singleton f))) :
    Flat g

AlgebraicGeometry.locallyOfFiniteType_of_comp_of_fppf_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/MorphismProperty/FppfRefinement.lean, line 199. The attribute's comment: “locally_finite_type”.

Stacks Project, Tag 06NB (locally finite type). If f ≫ g is locally of finite type and the singleton family consisting of f is refined by an fppf covering of Y, then g is locally of finite type.

theorem locallyOfFiniteType_of_comp_of_fppf_refinement
    {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [LocallyOfFiniteType (f ≫ g)]
    (h : ∃ 𝒰 : Y.Cover.{v} Scheme.fppfPrecoverage,
      Nonempty (𝒰.toPreZeroHypercover.Hom (PreZeroHypercover.singleton f))) :
    LocallyOfFiniteType g

AlgebraicGeometry.locallyOfFinitePresentation_of_comp_of_fppf_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/MorphismProperty/FppfRefinement.lean, line 249. The attribute's comment: “locally_finite_presentation”.

Stacks Project, Tag 06NB (locally finite presentation). If f ≫ g is locally of finite presentation and the singleton family consisting of f is refined by an fppf covering of Y, then g is locally of finite presentation.

theorem locallyOfFinitePresentation_of_comp_of_fppf_refinement
    {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [LocallyOfFinitePresentation (f ≫ g)]
    (h : ∃ 𝒰 : Y.Cover.{v} Scheme.fppfPrecoverage,
      Nonempty (𝒰.toPreZeroHypercover.Hom (PreZeroHypercover.singleton f))) :
    LocallyOfFinitePresentation g

Sources

• Section 35.14, Tag 02KJ
• AxiomMath/Stacks at 5ed82d14

LeanRingHom.finitePresentation_of_comp_of_faithfullyFlat · RingHom.finiteType_of_comp_of_faithfullyFlat_of_finitePresentation · AlgebraicGeometry.locallyOfFinitePresentation_of_comp_of_fppf · AlgebraicGeometry.locallyOfFiniteType_of_comp_of_fppf · Stacks.Smooth.smooth_of_comp_surjective_smooth · Stacks.Etale.etale_of_comp_surjective_etale · Stacks.Syntomic.syntomic_of_comp · Stacks.Smooth.smooth_of_comp_of_fppf

Section35.15 Local properties of schemes#

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

Tag 0348, a definition

Tag 0348 in the Stacks Project.

Declarations registered for the tag:

• CategoryTheory.ObjectProperty.IsLocal registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/Defs.lean, line 47 (StacksFrontier). References: SGA 4 IV (8.2); SGA 4½ Arcata (1.1), “more general”.

Tag 0349, a lemma

Tag 0349 in the Stacks Project.

AlgebraicGeometry.isLocal_fpqcPrecoverage_of_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/Criterion.lean, line 207. The attribute's comment: “fpqc case”.

Stacks Project, Tag 0349. A Zariski-local property of schemes which ascends along flat morphisms of affine schemes and descends along the surjective ones is fpqc local.

theorem isLocal_fpqcPrecoverage_of_affine (P : ObjectProperty Scheme.{u})
    [ObjectProperty.IsLocal P Scheme.zariskiPrecoverage]
    (ascends : ∀ {X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S),
      Flat f → P S → P X)
    (descends : ∀ {X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S),
      Flat f → Surjective f → P X → P S) :
    ObjectProperty.IsLocal P Scheme.fpqcPrecoverage

AlgebraicGeometry.isLocal_fppfPrecoverage_of_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/Criterion.lean, line 261. The attribute's comment: “fppf case”.

Stacks Project, Tag 0349. A Zariski-local property of schemes which ascends along flat morphisms of finite presentation of affine schemes and descends along the surjective ones is fppf local.

theorem isLocal_fppfPrecoverage_of_affine (P : ObjectProperty Scheme.{u})
    [ObjectProperty.IsLocal P Scheme.zariskiPrecoverage]
    (ascends : ∀ {X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S),
      Flat f → FinitePresentation f → P S → P X)
    (descends : ∀ {X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S),
      Flat f → FinitePresentation f → Surjective f → P X → P S) :
    ObjectProperty.IsLocal P Scheme.fppfPrecoverage

AlgebraicGeometry.isLocal_etalePrecoverage_of_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/Criterion.lean, line 289. The attribute's comment: “étale case”.

Stacks Project, Tag 0349. A Zariski-local property of schemes which ascends along étale morphisms of affine schemes and descends along the surjective ones is étale local.

theorem isLocal_etalePrecoverage_of_affine (P : ObjectProperty Scheme.{u})
    [ObjectProperty.IsLocal P Scheme.zariskiPrecoverage]
    (ascends : ∀ {X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S),
      Etale f → P S → P X)
    (descends : ∀ {X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S),
      Etale f → Surjective f → P X → P S) :
    ObjectProperty.IsLocal P Scheme.etalePrecoverage

AlgebraicGeometry.isLocal_smoothPrecoverage_of_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/Criterion.lean, line 304. The attribute's comment: “smooth case”.

Stacks Project, Tag 0349. A Zariski-local property of schemes which ascends along smooth morphisms of affine schemes and descends along the surjective ones is smooth local.

theorem isLocal_smoothPrecoverage_of_affine (P : ObjectProperty Scheme.{u})
    [ObjectProperty.IsLocal P Scheme.zariskiPrecoverage]
    (ascends : ∀ {X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S),
      Smooth f → P S → P X)
    (descends : ∀ {X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S),
      Smooth f → Surjective f → P X → P S) :
    ObjectProperty.IsLocal P (Scheme.precoverage @Smooth)

AlgebraicGeometry.isLocal_syntomicPrecoverage_of_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/Criterion.lean, line 319. The attribute's comment: “syntomic case”.

Stacks Project, Tag 0349. A Zariski-local property of schemes which ascends along syntomic morphisms of affine schemes and descends along the surjective ones is syntomic local.

theorem isLocal_syntomicPrecoverage_of_affine (P : ObjectProperty Scheme.{u})
    [ObjectProperty.IsLocal P Scheme.zariskiPrecoverage]
    (ascends : ∀ {X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S),
      Syntomic f → P S → P X)
    (descends : ∀ {X S : Scheme.{u}} [IsAffine X] [IsAffine S] (f : X ⟶ S),
      Syntomic f → Surjective f → P X → P S) :
    ObjectProperty.IsLocal P (Scheme.precoverage @Syntomic)

Sources

• Section 35.15, Tag 0347
• AxiomMath/Stacks at 5ed82d14

LeanCategoryTheory.ObjectProperty.IsLocal · AlgebraicGeometry.isLocal_fpqcPrecoverage_of_affine · AlgebraicGeometry.isLocal_fppfPrecoverage_of_affine · AlgebraicGeometry.isLocal_etalePrecoverage_of_affine · AlgebraicGeometry.isLocal_smoothPrecoverage_of_affine · AlgebraicGeometry.isLocal_syntomicPrecoverage_of_affine

Section35.16 Properties of schemes local in the fppf topology#

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

Tag 034C, a lemma

Tag 034C in the Stacks Project.

AlgebraicGeometry.isLocallyNoetherian_isLocal_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/Noetherian.lean, line 68.

Stacks Project, Tag 034C. Being locally Noetherian is local for fppf coverings of schemes.

instance isLocallyNoetherian_isLocal_fppf :
    ObjectProperty.IsLocal (fun X : Scheme.{u} => IsLocallyNoetherian X)
      Scheme.fppfPrecoverage

Tag 0368, a lemma

Tag 0368 in the Stacks Project.

AlgebraicGeometry.jacobsonSpace_isLocal_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/Jacobson.lean, line 119.

Stacks Project, Tag 0368. Being Jacobson is local for fppf coverings of schemes.

instance jacobsonSpace_isLocal_fppf :
    ObjectProperty.IsLocal (fun X : Scheme.{u} => JacobsonSpace X)
      Scheme.fppfPrecoverage

Tag 0BAL, a lemma

Tag 0BAL in the Stacks Project.

AlgebraicGeometry.finiteIrreducibleComponents_isLocal_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/IrreducibleComponents.lean, line 163.

Having finitely many irreducible components on every quasi-compact open is local in the fppf topology.

instance finiteIrreducibleComponents_isLocal_fppf :
    ObjectProperty.IsLocal
      (fun X : Scheme.{u} =>
        ∀ U : X.Opens, IsCompact (U : Set X) → (irreducibleComponents U).Finite)
      Scheme.fppfPrecoverage

Sources

• Section 35.16, Tag 034B
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isLocallyNoetherian_isLocal_fppf · AlgebraicGeometry.jacobsonSpace_isLocal_fppf · AlgebraicGeometry.finiteIrreducibleComponents_isLocal_fppf

Section35.17 Properties of schemes local in the syntomic topology#

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

Tag 036A, a lemma

Tag 036A in the Stacks Project.

AlgebraicGeometry.isLocallyNoetherian_and_hasPropertySk_isLocal_syntomic, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/SerreCondition.lean, line 155.

Stacks Project, Tag 036A. Being locally Noetherian and satisfying (Sₖ) is local for syntomic coverings.

instance isLocallyNoetherian_and_hasPropertySk_isLocal_syntomic (k : ℕ) :
    ObjectProperty.IsLocal
      (fun X : Scheme.{u} => ∃ h : IsLocallyNoetherian X, @HasPropertySk X h k)
      (Scheme.precoverage @Syntomic)

Tag 036B, a lemma

Tag 036B in the Stacks Project.

AlgebraicGeometry.isCohenMacaulay_isLocal_syntomic, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/CohenMacaulay.lean, line 54.

Stacks Project, Tag 036B. Being Cohen–Macaulay is local for syntomic coverings.

instance isCohenMacaulay_isLocal_syntomic :
    ObjectProperty.IsLocal (fun X : Scheme.{u} => IsCohenMacaulay X)
      (Scheme.precoverage @Syntomic)

Sources

• Section 35.17, Tag 0369
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isLocallyNoetherian_and_hasPropertySk_isLocal_syntomic · AlgebraicGeometry.isCohenMacaulay_isLocal_syntomic

Section35.18 Properties of schemes local in the smooth topology#

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

Tag 034E, a lemma

Tag 034E in the Stacks Project.

AlgebraicGeometry.isReduced_isLocal_smooth, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/Reduced.lean, line 46.

Stacks Project, Tag 034E. Reducedness of schemes is local for the smooth precoverage.

instance isReduced_isLocal_smooth :
    ObjectProperty.IsLocal (fun X : Scheme.{u} => IsReduced X)
      (Scheme.precoverage @Smooth)

Tag 034F, a lemma

Tag 034F in the Stacks Project.

AlgebraicGeometry.isLocal_isNormal_etalePrecoverage, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/Normal.lean, line 239. The attribute's comment: “for the étale precoverage, AlgebraicGeometry.Scheme.etalePrecoverage, rather than for the smooth one; normality of a scheme is AlgebraicGeometry.IsNormal, Definition 033I, i.e. every local ring is a normal domain”. References: SGA 1 II (3.1), “special case”.

Stacks 034F for the étale precoverage. Normality of a scheme is a local object property for AlgebraicGeometry.Scheme.etalePrecoverage: a scheme étale over a normal scheme is normal, and a scheme covered by normal schemes étale over it is normal.

The source states Lemma 034F for the smooth topology; the étale precoverage is what the algebraic-spaces layer consumes, and both affine inputs — Stacks 033C for ascent and Stacks 033G for descent — are the smooth ones, so nothing is lost by restricting.

This is item (7) of Remark 03E7: it is the instance that AlgebraicGeometry.Space.exists_atlas_iff_forall_etale needs in order to turn AlgebraicGeometry.Space.IsNormal — Definition 03E6 at normality — from a some-chart condition into an every-chart equivalence.

instance isLocal_isNormal_etalePrecoverage :
    ObjectProperty.IsLocal (fun X : Scheme.{u} => IsNormal X) Scheme.etalePrecoverage

AlgebraicGeometry.isNormal_isLocal_smooth, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/NormalMorphism/SmoothLocalSource.lean, line 88. References: SGA 3 X (8.9), “more general”.

Normality of schemes is local in the smooth topology.

public instance isNormal_isLocal_smooth :
    ObjectProperty.IsLocal (fun X : Scheme.{u} => IsNormal X)
      (Scheme.precoverage (@Smooth : MorphismProperty Scheme.{u}))

Tag 036C, a lemma

Tag 036C in the Stacks Project.

AlgebraicGeometry.isLocallyNoetherian_and_isRegularInCodimension_isLocal_smooth, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/RegularInCodimension.lean, line 142. References: EGA IV (17.5.8), “(iii)”.

Stacks Project, Tag 036C. Being locally Noetherian and regular in codimension k is local for smooth coverings.

instance isLocallyNoetherian_and_isRegularInCodimension_isLocal_smooth (k : ℕ) :
    ObjectProperty.IsLocal
      (fun X : Scheme.{u} => IsLocallyNoetherian X ∧ IsRegularInCodimension X k)
      (Scheme.precoverage @Smooth)

Tag 036D, a lemma

Tag 036D in the Stacks Project.

AlgebraicGeometry.isRegular_isLocal_smooth, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/Regular.lean, line 59.

Stacks Project, Tag 036D. Regularity of schemes is local for the smooth precoverage.

instance isRegular_isLocal_smooth :
    ObjectProperty.IsLocal (fun X : Scheme.{u} => IsRegular X)
      (Scheme.precoverage @Smooth)

Tag 036E, a lemma

Tag 036E in the Stacks Project.

AlgebraicGeometry.isNagataScheme_isLocal_smooth, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/Nagata.lean, line 67.

Stacks Project, Tag 036E. Being Nagata is local for the smooth precoverage on schemes.

instance isNagataScheme_isLocal_smooth :
    ObjectProperty.IsLocal (fun X : Scheme.{u} => IsNagataScheme X)
      (Scheme.precoverage @Smooth)

Sources

• Section 35.18, Tag 034D
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isReduced_isLocal_smooth · AlgebraicGeometry.isLocal_isNormal_etalePrecoverage · AlgebraicGeometry.isNormal_isLocal_smooth · AlgebraicGeometry.isLocallyNoetherian_and_isRegularInCodimension_isLocal_smooth · AlgebraicGeometry.isRegular_isLocal_smooth · AlgebraicGeometry.isNagataScheme_isLocal_smooth

Section35.19 Variants on descending properties#

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

Tag 06QM, a lemma

Tag 06QM in the Stacks Project.

AlgebraicGeometry.isReduced_of_flat_of_surjective, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SchemeProperty/Reduced.lean, line 45. References: SGA 3 VIB (2.1.2), “partial”.

The target of a flat surjective morphism of schemes with reduced source is reduced.

lemma isReduced_of_flat_of_surjective {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Flat f] [Surjective f] [IsReduced X] : IsReduced Y

Tag 06QN, a lemma

Tag 06QN in the Stacks Project.

AlgebraicGeometry.Space.hasEtaleLocalProperty_isRegular_of_isSurjective_of_isFlat_of_isLocallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Descent/Properties/Regular.lean, line 109. The attribute's comment: “the same statement in the descent chapter”. References: SGA 1 I (9.2), “converse (X reg ⇒ Y reg)”.

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

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

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

Sources

• Section 35.19, Tag 06QL
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isReduced_of_flat_of_surjective · AlgebraicGeometry.Space.hasEtaleLocalProperty_isRegular_of_isSurjective_of_isFlat_of_isLocallyOfFinitePresentation

Section35.20 Germs of schemes#

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

Tag 04QR, a definition

Tag 04QR in the Stacks Project.

AlgebraicGeometry.GermOfScheme, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germ/Basic.lean, line 58. The attribute's comment: “germ_of_scheme”.

A germ of a scheme is a scheme together with a distinguished point.

structure GermOfScheme

AlgebraicGeometry.MorphismOfGerms, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germ/Basic.lean, line 111. The attribute's comment: “morphism_of_germs”.

A morphism of germs of schemes is a representative defined on an open neighbourhood of the distinguished source point, modulo agreement on a possibly smaller such neighbourhood.

noncomputable def MorphismOfGerms (X S : GermOfScheme.{u}) : Type u

AlgebraicGeometry.MorphismOfGerms.comp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germ/Basic.lean, line 294. The attribute's comment: “composition_of_germs”.

Composition of morphisms of germs, obtained by composing representatives after restricting the first one to the inverse image of the domain of the second.

noncomputable def comp {X Y Z : GermOfScheme.{u}} :
    MorphismOfGerms X Y → MorphismOfGerms Y Z → MorphismOfGerms X Z

Tag 04QS, a definition

Tag 04QS in the Stacks Project.

AlgebraicGeometry.MorphismOfGerms.IsEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germ/Etale.lean, line 48. The attribute's comment: “etale”.

A morphism of germs is étale if it is represented on some open neighbourhood by an étale morphism of schemes.

abbrev IsEtale {X S : GermOfScheme.{u}} (f : MorphismOfGerms X S) : Prop

AlgebraicGeometry.MorphismOfGerms.IsSmooth, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germ/Etale.lean, line 54. The attribute's comment: “smooth”.

A morphism of germs is smooth if it is represented on some open neighbourhood by a smooth morphism of schemes.

abbrev IsSmooth {X S : GermOfScheme.{u}} (f : MorphismOfGerms X S) : Prop

Sources

• Section 35.20, Tag 04QQ
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.GermOfScheme · AlgebraicGeometry.MorphismOfGerms · AlgebraicGeometry.MorphismOfGerms.comp · AlgebraicGeometry.MorphismOfGerms.IsEtale · AlgebraicGeometry.MorphismOfGerms.IsSmooth

Section35.21 Local properties of germs#

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

Tag 04N1, a definition

Tag 04N1 in the Stacks Project.

AlgebraicGeometry.GermOfScheme.IsEtaleLocal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germ/Local.lean, line 52. The attribute's comment: “etale”.

A property of germs is étale local if it has the same truth value at the source and target of every étale morphism of germs.

abbrev GermOfScheme.IsEtaleLocal (P : GermOfScheme.{u} → Prop) : Prop

AlgebraicGeometry.GermOfScheme.IsSmoothLocal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germ/Local.lean, line 59. The attribute's comment: “smooth”.

A property of germs is smooth local if it has the same truth value at the source and target of every smooth morphism of germs.

abbrev GermOfScheme.IsSmoothLocal (P : GermOfScheme.{u} → Prop) : Prop

Tag 04N4, a lemma

Tag 04N4 in the Stacks Project.

AlgebraicGeometry.topologicalKrullDimAt_eq_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/EtaleLocalDimension.lean, line 149.

Stacks Project, Tag 04N4. An étale morphism preserves the local Krull dimension at corresponding points.

theorem topologicalKrullDimAt_eq_of_etale
    {U V : Scheme.{u}} (f : U ⟶ V) [Etale f] (u : U) :
    topologicalKrullDimAt U u = topologicalKrullDimAt V (f u)

Tag 04N8, a lemma

Tag 04N8 in the Stacks Project.

AlgebraicGeometry.ringKrullDim_stalk_eq_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/EtaleStalkDimension.lean, line 43. References: EGA IV (17.6.4).

Stacks Project, Tag 04N8. An étale morphism preserves the Krull dimension of local rings at corresponding points.

theorem ringKrullDim_stalk_eq_of_etale {U V : Scheme.{u}} (f : U ⟶ V) [Etale f] (u : U) :
    ringKrullDim (U.presheaf.stalk u) = ringKrullDim (V.presheaf.stalk (f u))

Tag 0AH7, a lemma

Tag 0AH7 in the Stacks Project.

AlgebraicGeometry.isRegularLocalRing_stalk_iff_of_etale, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/RegularGerm.lean, line 48.

Stacks Project, Tag 0AH7. For an étale morphism of schemes, the local ring at a point of the source is regular if and only if the local ring at its image is regular.

lemma isRegularLocalRing_stalk_iff_of_etale {U V : Scheme.{u}} (f : U ⟶ V) [Etale f] (u : U) :
    IsRegularLocalRing (U.presheaf.stalk u) ↔
      IsRegularLocalRing (V.presheaf.stalk (f u))

Sources

• Section 35.21, Tag 04QT
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.GermOfScheme.IsEtaleLocal · AlgebraicGeometry.GermOfScheme.IsSmoothLocal · AlgebraicGeometry.topologicalKrullDimAt_eq_of_etale · AlgebraicGeometry.ringKrullDim_stalk_eq_of_etale · AlgebraicGeometry.isRegularLocalRing_stalk_iff_of_etale

Section35.22 Properties of morphisms local on the target#

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

Tag 02KO, a definition

Tag 02KO in the Stacks Project.

Declarations registered for the tag:

• CategoryTheory.MorphismProperty.IsLocalAtTarget registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/LocalOnSource/Defs.lean, line 51 (StacksFrontier). References: SGA 3 IV (4.6.3), “(e_T)”; SGA 3 VIB (2.0), “b)”.

Tag 04QU, a lemma

Tag 04QU in the Stacks Project.

AlgebraicGeometry.pullbackSnd_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/BaseChange.lean, line 60. The attribute's comment: “fpqc case”.

A property of morphisms of schemes which is fpqc local on the target is preserved by flat base change.

theorem pullbackSnd_of_flat
    (P : MorphismProperty Scheme.{u}) [P.IsLocalAtTarget Scheme.fpqcPrecoverage]
    {X Y Y' : Scheme.{u}} (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : P f) (hg : Flat g) : P (pullback.snd f g)

AlgebraicGeometry.pullbackSnd_of_flat_locallyOfFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/BaseChange.lean, line 86. The attribute's comment: “fppf case”.

A property of morphisms of schemes which is fppf local on the target is preserved by base change along a flat morphism which is locally of finite presentation.

theorem pullbackSnd_of_flat_locallyOfFinitePresentation
    (P : MorphismProperty Scheme.{u}) [P.IsLocalAtTarget Scheme.fppfPrecoverage]
    {X Y Y' : Scheme.{u}} (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : P f) (hg : Flat g) (hlfp : LocallyOfFinitePresentation g) :
    P (pullback.snd f g)

AlgebraicGeometry.pullbackSnd_of_syntomic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/BaseChange.lean, line 98. The attribute's comment: “syntomic case”.

A property of morphisms of schemes which is syntomic local on the target is preserved by syntomic base change.

theorem pullbackSnd_of_syntomic (P : MorphismProperty Scheme.{u})
    [P.IsLocalAtTarget (Scheme.precoverage (@Syntomic.{u}))]
    {X Y Y' : Scheme.{u}} (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : P f) (hg : Syntomic g) : P (pullback.snd f g)

AlgebraicGeometry.pullbackSnd_of_smooth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/BaseChange.lean, line 109. The attribute's comment: “smooth case”.

A property of morphisms of schemes which is smooth local on the target is preserved by smooth base change.

theorem pullbackSnd_of_smooth (P : MorphismProperty Scheme.{u})
    [P.IsLocalAtTarget (Scheme.precoverage (@Smooth))]
    {X Y Y' : Scheme.{u}} (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : P f) (hg : Smooth g) : P (pullback.snd f g)

AlgebraicGeometry.pullbackSnd_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/BaseChange.lean, line 119. The attribute's comment: “étale case”.

A property of morphisms of schemes which is étale local on the target is preserved by étale base change.

theorem pullbackSnd_of_etale (P : MorphismProperty Scheme.{u})
    [P.IsLocalAtTarget Scheme.etalePrecoverage]
    {X Y Y' : Scheme.{u}} (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : P f) (hg : Etale g) : P (pullback.snd f g)

AlgebraicGeometry.pullbackSnd_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/BaseChange.lean, line 129. The attribute's comment: “Zariski case”.

A property of morphisms of schemes which is Zariski local on the target is preserved by base change along an open immersion.

theorem pullbackSnd_of_isOpenImmersion (P : MorphismProperty Scheme.{u})
    [P.IsLocalAtTarget Scheme.zariskiPrecoverage]
    {X Y Y' : Scheme.{u}} (f : X ⟶ Y) (g : Y' ⟶ Y)
    (hf : P f) (hg : IsOpenImmersion g) : P (pullback.snd f g)

Tag 06QP, a lemma

Tag 06QP in the Stacks Project.

AlgebraicGeometry.largestTargetOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/LargestTargetOpen.lean, line 212. The attribute's comment: “largest open”.

The supremum of the opens of the target over which f has the property P.

noncomputable def largestTargetOpen (P : MorphismProperty Scheme.{u}) {X Y : Scheme.{u}}
    (f : X ⟶ Y) : Y.Opens

AlgebraicGeometry.property_largestTargetOpen, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/LargestTargetOpen.lean, line 218. The attribute's comment: “existence”. References: SGA 3 VIB (2.1), “partial”.

Stacks Project, Tag 06QP. A target-local property holds over the largest open.

lemma property_largestTargetOpen (P Q : MorphismProperty Scheme.{u})
    (hQ : IsDescentMorphismClass Q) [P.IsLocalAtTarget (Scheme.precoverage Q)]
    {X Y : Scheme.{u}} (f : X ⟶ Y) : P (f ∣_ largestTargetOpen P f)

AlgebraicGeometry.le_largestTargetOpen, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/LargestTargetOpen.lean, line 244. The attribute's comment: “maximality”.

Stacks Project, Tag 06QP. Every open over which the property holds lies in the largest open.

lemma le_largestTargetOpen (P : MorphismProperty Scheme.{u}) {X Y : Scheme.{u}} (f : X ⟶ Y)
    (U : Y.Opens) (hU : P (f ∣_ U)) : U ≤ largestTargetOpen P f

AlgebraicGeometry.range_le_largestTargetOpen, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/LargestTargetOpen.lean, line 250. The attribute's comment: “part (1)”.

Stacks Project, Tag 06QP. The image of a morphism of the chosen class whose base change has the property lies in the largest open.

lemma range_le_largestTargetOpen (P Q : MorphismProperty Scheme.{u})
    (hQ : IsDescentMorphismClass Q) [P.IsLocalAtTarget (Scheme.precoverage Q)]
    {X Y Y' : Scheme.{u}} (f : X ⟶ Y) (g : Y' ⟶ Y) (hg : Q g)
    (hfg : P (pullback.snd f g)) : Set.range g ⊆ (largestTargetOpen P f).1

AlgebraicGeometry.largestTargetOpen_baseChange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/LargestTargetOpen.lean, line 280. The attribute's comment: “part (2)”.

Stacks Project, Tag 06QP. The largest open commutes with base change along a morphism of the chosen class.

lemma largestTargetOpen_baseChange (P Q : MorphismProperty Scheme.{u})
    (hQ : IsDescentMorphismClass Q) [P.IsLocalAtTarget (Scheme.precoverage Q)]
    {X Y Y' : Scheme.{u}} (f : X ⟶ Y) (g : Y' ⟶ Y) (hg : Q g) :
    largestTargetOpen P (pullback.snd f g) = g ⁻¹ᵁ largestTargetOpen P f

AlgebraicGeometry.largestTargetOpen_covering, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalProperties/LargestTargetOpen.lean, line 298. The attribute's comment: “part (3)”.

Stacks Project, Tag 06QP. The largest opens of the members of a covering family are the inverse images of the largest open downstairs.

lemma largestTargetOpen_covering (P Q : MorphismProperty Scheme.{u})
    (hQ : IsDescentMorphismClass Q) [P.IsLocalAtTarget (Scheme.precoverage Q)]
    {X Y : Scheme.{u}} {I : Type v} (f : X ⟶ Y) (Y' : I → Scheme.{u})
    (g : ∀ i, Y' i ⟶ Y) (hg : Presieve.ofArrows Y' g ∈ Scheme.precoverage Q Y) (i : I) :
    largestTargetOpen P (pullback.snd f (g i)) = (g i) ⁻¹ᵁ largestTargetOpen P f

Tag 02KP, a lemma

Tag 02KP in the Stacks Project.

Stacks.Descent.isLocalAtTarget_fpqcPrecoverage_of_affineDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcLocalAtTarget.lean, line 298. The attribute's comment: “the fpqc case”.

Stacks Project, Tag 02KP for the fpqc topology. Let P be a property of morphisms of schemes. Assume that

1. P is stable under base change along flat morphisms;
2. P is Zariski local on the base;
3. for every surjective flat morphism g : S' ⟶ S of affine schemes and every morphism of schemes f : X ⟶ S, the property P holds for f if it holds for the base change S' ×_S X ⟶ S'.

Then P is fpqc local on the base.

theorem isLocalAtTarget_fpqcPrecoverage_of_affineDescent
    (hdesc : ∀ {S S' T : Scheme.{u}} [IsAffine S] [IsAffine S'] (g : S' ⟶ S), Surjective g →
      Flat g → ∀ f : T ⟶ S, P (pullback.snd f g) → P f) :
    P.IsLocalAtTarget Scheme.fpqcPrecoverage

AlgebraicGeometry.isLocalAtTarget_precoverage_of_affineDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/MorphismPropertyTopology/CoveringTopologyLocalAtTarget.lean, line 109. The attribute's comment: “the fppf, étale, smooth and syntomic cases”.

Stacks Project, Tag 02KP for the fppf, étale, smooth and syntomic topologies. Let P be a property of morphisms of schemes and let τ be one of fppf, étale, smooth and syntomic. Assume that

1. P is preserved by base change along the morphisms belonging to τ, that is along flat morphisms locally of finite presentation, syntomic, smooth or étale morphisms depending on whether τ is fppf, syntomic, smooth or étale;
2. P is Zariski local on the base;
3. for every surjective morphism g : S' ⟶ S of affine schemes belonging to τ and every morphism of schemes f : X ⟶ S, the property P holds for f if it holds for the base change S' ×_S X ⟶ S'.

Then P is τ local on the base.

theorem isLocalAtTarget_precoverage_of_affineDescent (P : MorphismProperty Scheme.{u})
    (τ : CoveringTopology) (hτ : τ ≠ .zariski)
    [P.IsStableUnderBaseChangeAgainst (coveringMorphismProperty τ)]
    [IsZariskiLocalAtTarget P]
    (hdesc : ∀ {S S' X : Scheme.{u}} [IsAffine S] [IsAffine S'] (g : S' ⟶ S), Surjective g →
      coveringMorphismProperty τ g → ∀ f : X ⟶ S, P (pullback.snd f g) → P f) :
    P.IsLocalAtTarget (Scheme.precoverage (coveringMorphismProperty τ))

Tag 034G, a remark

Tag 034G in the Stacks Project.

AlgebraicGeometry.isLocalAtTarget_etale_of_standard_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/StandardForm/Descent.lean, line 253. The attribute's comment: “étale case”.

Stacks Project, Tag 034G, étale case. A property of morphisms of schemes which is Zariski local on the target and stable under étale base change is étale local on the target as soon as it descends along surjective standard étale morphisms of affine schemes.

theorem isLocalAtTarget_etale_of_standard_descent
    [P.IsStableUnderBaseChangeAgainst (@Etale)]
    [P.IsLocalAtTarget Scheme.zariskiPrecoverage]
    (h : ∀ {S S' X : Scheme.{u}} [IsAffine S] [IsAffine S']
      (g : S' ⟶ S) [Surjective g] (_hg : IsStandardEtale g)
      (f : X ⟶ S), P (pullback.snd f g) → P f) :
    P.IsLocalAtTarget Scheme.etalePrecoverage

AlgebraicGeometry.isLocalAtTarget_smooth_of_standard_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/StandardForm/Descent.lean, line 279. The attribute's comment: “smooth case”.

Stacks Project, Tag 034G, smooth case. A property of morphisms of schemes which is Zariski local on the target and stable under smooth base change is smooth local on the target as soon as it descends along surjective standard smooth morphisms of affine schemes.

theorem isLocalAtTarget_smooth_of_standard_descent
    [P.IsStableUnderBaseChangeAgainst (@Smooth)]
    [P.IsLocalAtTarget Scheme.zariskiPrecoverage]
    (h : ∀ {S S' X : Scheme.{u}} [IsAffine S] [IsAffine S']
      (g : S' ⟶ S) [Surjective g] (_hg : IsStandardSmooth g)
      (f : X ⟶ S), P (pullback.snd f g) → P f) :
    P.IsLocalAtTarget (Scheme.precoverage (@Smooth))

AlgebraicGeometry.isLocalAtTarget_syntomic_of_standard_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/StandardForm/Descent.lean, line 306. The attribute's comment: “syntomic case”.

Stacks Project, Tag 034G, syntomic case. A property of morphisms of schemes which is Zariski local on the target and stable under syntomic base change is syntomic local on the target as soon as it descends along surjective standard syntomic morphisms of affine schemes.

theorem isLocalAtTarget_syntomic_of_standard_descent
    [P.IsStableUnderBaseChangeAgainst (@Syntomic)]
    [P.IsLocalAtTarget Scheme.zariskiPrecoverage]
    (h : ∀ {S S' X : Scheme.{u}} [IsAffine S] [IsAffine S']
      (g : S' ⟶ S) [Surjective g] (_hg : IsStandardSyntomic g)
      (f : X ⟶ S), P (pullback.snd f g) → P f) :
    P.IsLocalAtTarget (Scheme.precoverage (@Syntomic))

Sources

• Section 35.22, Tag 02KN
• AxiomMath/Stacks at 5ed82d14

LeanCategoryTheory.MorphismProperty.IsLocalAtTarget · AlgebraicGeometry.pullbackSnd_of_flat · AlgebraicGeometry.pullbackSnd_of_flat_locallyOfFinitePresentation · AlgebraicGeometry.pullbackSnd_of_syntomic · AlgebraicGeometry.pullbackSnd_of_smooth · AlgebraicGeometry.pullbackSnd_of_etale · AlgebraicGeometry.pullbackSnd_of_isOpenImmersion · AlgebraicGeometry.largestTargetOpen

Section35.23 Properties of morphisms local in the fpqc topology on the target#

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

Tag 02KQ, a lemma

Tag 02KQ in the Stacks Project.

Stacks.Descent.quasiCompact_descendsAlong_surjective_inf_flat_inf_quasiCompact, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcLocalAtTarget.lean, line 327. The attribute's comment: “the descent step”. References: EGA IV (1.1.4), “special case”.

Stacks Project, Tag 02KQ. Quasi-compact morphisms satisfy fpqc descent: if the base change of g along a surjective flat quasi-compact morphism is quasi-compact, then so is g.

instance quasiCompact_descendsAlong_surjective_inf_flat_inf_quasiCompact :
    MorphismProperty.DescendsAlong (@QuasiCompact : MorphismProperty Scheme.{u})
      (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Stacks.Descent.quasiCompact_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcLocalAtTarget.lean, line 351. References: SGA 4 IV (8.5.5).

Stacks Project, Tag 02KQ. Quasi-compactness of a morphism of schemes is fpqc local on the base.

instance quasiCompact_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@QuasiCompact : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02KR, a lemma

Tag 02KR in the Stacks Project.

AlgebraicGeometry.quasiSeparated_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/FinitePresentation.lean, line 71. References: EGA IV (2.7.1), “more general”; SGA 4 IV (8.5.5).

Stacks Project, Tag 02KR. Quasi-separatedness of morphisms of schemes is fpqc local on the base.

instance quasiSeparated_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@QuasiSeparated : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02KS, a lemma

Tag 02KS in the Stacks Project.

AlgebraicGeometry.universallyClosed_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/ProperFpqcLocalAtTarget.lean, line 96. References: EGA IV (2.6.4), “more general”.

Stacks Project, Tag 02KS. Universal closedness of morphisms of schemes is fpqc local on the target.

instance universallyClosed_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@UniversallyClosed : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02KT, a lemma

Tag 02KT in the Stacks Project.

AlgebraicGeometry.universallyOpen_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/UniversalHomeomorphism.lean, line 56. References: EGA IV (2.4.3), “more general”; EGA IV (2.6.4), “more general”; SGA 1 VIII (4.7), “more general”; SGA 3 VIB (2.1.2), “partial”; SGA 4 IV (8.5.5).

Stacks Project, Tag 02KT. Universal openness of morphisms of schemes is fpqc local on the base.

instance universallyOpen_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@UniversallyOpen : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 0CEW, a lemma

Tag 0CEW in the Stacks Project.

AlgebraicGeometry.universallyQuotientMap_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/Submersive.lean, line 151. References: EGA IV (15.7.11.1), “partial”.

Stacks Project, Tag 0CEW. Universal submersiveness of morphisms of schemes is fpqc local on the base.

instance universallyQuotientMap_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      ((topologically @Topology.IsQuotientMap : MorphismProperty Scheme.{u}).universally)
      Scheme.fpqcPrecoverage

Tag 02KU, a lemma

Tag 02KU in the Stacks Project.

AlgebraicGeometry.isSeparated_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/ProperFpqcLocalAtTarget.lean, line 106. References: EGA IV (2.7.1), “more general”; SGA 1 VIII (4.8), “more general”; SGA 4 IV (8.5.5).

Stacks Project, Tag 02KU. Separatedness of morphisms of schemes is fpqc local on the target.

instance isSeparated_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@IsSeparated : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02KV, a lemma

Tag 02KV in the Stacks Project.

Stacks.Descent.surjective_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcLocalAtTarget.lean, line 362. References: SGA 4 IV (8.5.5).

Stacks Project, Tag 02KV. Surjectivity of a morphism of schemes is fpqc local on the base.

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

Tag 0H8H, a lemma

Tag 0H8H in the Stacks Project.

AlgebraicGeometry.quasiCompact_isDominant_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/Dominant.lean, line 83. References: SGA 3 VIB (2.1.2), “qc+dominant example”; SGA 4 IV (8.5.5).

Stacks Project, Tag 0H8H. Being quasi-compact and dominant is fpqc local on the base.

instance quasiCompact_isDominant_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (@QuasiCompact ⊓ @IsDominant : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage

Tag 0H8I, a lemma

Tag 0H8I in the Stacks Project.

AlgebraicGeometry.isDominant_iff_baseChange_fieldExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/Germs/DominantFieldExtension.lean, line 43.

Stacks Project, Tag 0H8I. A morphism of schemes over a field is dominant exactly when its base change along a field extension is dominant.

theorem isDominant_iff_baseChange_fieldExtension
    (k K : Type u) [Field k] [Field K] [Algebra k K]
    {X Y : Scheme.{u}} (pX : X ⟶ Spec (.of k)) (pY : Y ⟶ Spec (.of k))
    (f : X ⟶ Y) (h : f ≫ pY = pX) :
    let g : Spec (.of K) ⟶ Spec (.of k) :=
      Spec.map (CommRingCat.ofHom (algebraMap k K))
    let fK : pullback pX g ⟶ pullback pY g :=
      pullback.map pX g pY g f (𝟙 _) (𝟙 _) (by simpa using h.symm) (by simp)
    IsDominant f ↔ IsDominant fK

Tag 02KW, a lemma

Tag 02KW in the Stacks Project.

AlgebraicGeometry.universallyInjective_iff_of_fpqcCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/UniversallyInjectiveFpqcLocalBase.lean, line 62.

Stacks Project, Tag 02KW. Universal injectivity is fpqc local on the base: for an fpqc covering 𝒰 of Y, a morphism f : X ⟶ Y is universally injective if and only if each base change 𝒰.X i ×_Y X ⟶ 𝒰.X i is universally injective.

theorem universallyInjective_iff_of_fpqcCover {X Y : Scheme.{u}} (f : X ⟶ Y)
    (𝒰 : Precoverage.ZeroHypercover.{w} Scheme.fpqcPrecoverage Y) :
    UniversallyInjective f ↔ ∀ i, UniversallyInjective (pullback.snd f (𝒰.f i))

Declarations registered for the tag:

• AlgebraicGeometry.UniversallyInjective.isStableUnderBaseChange registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/SchemeProperty/FpqcLocal.lean, line 47 (StacksFrontier). References: SGA 3 VIB (10.1), “partial, sufficiency”; SGA 3 VIB (2.6), “more general”.
• AlgebraicGeometry.universallyInjective_isZariskiLocalAtTarget registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/SchemeProperty/FpqcLocal.lean, line 51 (StacksFrontier).
• AlgebraicGeometry.universallyInjective_isLocalAtTarget_fpqc, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Representable/FpqcLocal.lean, line 248 (StacksFrontier): “universal injectivity is fpqc local on the target”.

Tag 0CEX, a lemma

Tag 0CEX in the Stacks Project.

AlgebraicGeometry.universalHomeomorphism_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/UniversalHomeomorphism.lean, line 110. References: EGA IV (2.6.2), “(iv), special case”; EGA IV (2.6.4), “more general”; SGA 1 VIII (4.7), “more general”; SGA 4 IV (8.5.5).

Stacks Project, Tag 0CEX. Being a universal homeomorphism of schemes is fpqc local on the base.

instance universalHomeomorphism_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (@UniversalHomeomorphism : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage

Tag 02KX, a lemma

Tag 02KX in the Stacks Project.

Stacks.Descent.locallyOfFiniteType_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcLocalAtTarget.lean, line 371.

Stacks Project, Tag 02KX. Being locally of finite type is fpqc local on the base.

instance locallyOfFiniteType_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@LocallyOfFiniteType : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02KY, a lemma

Tag 02KY in the Stacks Project.

Stacks.Descent.locallyOfFinitePresentation_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteLocallyFree/FpqcDescent.lean, line 108. References: EGA IV (2.7.1), “(iv)”; SGA 4 IV (8.5.5), “fpqc target locality”.

Stacks Project, Tag 02KY. Being locally of finite presentation is fpqc local on the base.

instance locallyOfFinitePresentation_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (@LocallyOfFinitePresentation : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage

Tag 02KZ, a lemma

Tag 02KZ in the Stacks Project.

Stacks.Descent.finiteType_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcLocalAtTarget.lean, line 382.

Stacks Project, Tag 02KZ. Being of finite type is fpqc local on the target for scheme morphisms.

instance finiteType_isLocalAtTarget_fpqc :
    IsLocalAtTarget (@LocallyOfFiniteType ⊓ @QuasiCompact : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02L0, a lemma

Tag 02L0 in the Stacks Project.

AlgebraicGeometry.finitePresentation_isLocalAtTarget, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/FinitePresentation.lean, line 81. References: SGA 4 IV (8.5.5).

Stacks Project, Tag 02L0. Being of finite presentation is fpqc local on the base.

instance finitePresentation_isLocalAtTarget :
    MorphismProperty.IsLocalAtTarget
      (@FinitePresentation : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage

Tag 02L1, a lemma

Tag 02L1 in the Stacks Project.

AlgebraicGeometry.isProper_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/ProperFpqcLocalAtTarget.lean, line 117. References: EGA IV (2.7.1), “more general”; SGA 1 VIII (4.8), “more general”; SGA 4 IV (8.5.5).

Stacks Project, Tag 02L1. Properness of morphisms of schemes is fpqc local on the target.

instance isProper_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@IsProper : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02L2, a lemma

Tag 02L2 in the Stacks Project.

Stacks.Descent.flat_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteLocallyFree/FpqcDescent.lean, line 97. References: SGA 4 IV (8.5.5), “partial”.

Stacks Project, Tag 02L2. Flatness of a morphism of schemes is fpqc local on the base.

instance flat_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@Flat : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02L3, a lemma

Tag 02L3 in the Stacks Project.

Stacks.Descent.isOpenImmersion_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcOpenImmersion.lean, line 54. References: EGA IV (2.7.1), “descent direction of (x)”; SGA 1 VIII (5.5), “open-immersion clause”; SGA 4 IV (8.5.5).

Stacks Project, Tag 02L3. Being an open immersion is fpqc local on the base: f is an open immersion if and only if its base change along every member of an fpqc covering of its target is one.

instance isOpenImmersion_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@IsOpenImmersion : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02L5, a lemma

Tag 02L5 in the Stacks Project.

Stacks.Descent.isAffineHom_descendsAlong_surjective_inf_flat_inf_quasiCompact, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcAffine.lean, line 119. The attribute's comment: “the descent step”.

Affine morphisms satisfy fpqc descent: if the base change of g along a surjective flat quasi-compact morphism is affine, then so is g.

instance isAffineHom_descendsAlong_surjective_inf_flat_inf_quasiCompact :
    MorphismProperty.DescendsAlong (@IsAffineHom : MorphismProperty Scheme.{u})
      (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Stacks.Descent.isAffineHom_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcAffine.lean, line 145. References: SGA 4 IV (8.5.5).

Being an affine morphism of schemes is fpqc local on the base.

instance isAffineHom_isLocalAtTarget_fpqc :
    (show MorphismProperty Scheme.{u} from @IsAffineHom).IsLocalAtTarget
      Scheme.fpqcPrecoverage

Tag 02L6, a lemma

Tag 02L6 in the Stacks Project.

Stacks.Descent.isClosedImmersion_descendsAlong_surjective_inf_flat_inf_quasiCompact, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcLocalAtTarget.lean, line 402. The attribute's comment: “the descent step”. References: EGA IV (2.7.1), “(xii)”; SGA 1 VIII (5.5), “closed-immersion clause”; SGA 3 IV (4.7), “partial”; SGA 4 IV (8.5.5), “partial”.

Closed immersions satisfy fpqc descent: if the base change of g along a surjective flat quasi-compact morphism is a closed immersion, then so is g.

instance isClosedImmersion_descendsAlong_surjective_inf_flat_inf_quasiCompact :
    MorphismProperty.DescendsAlong (@IsClosedImmersion : MorphismProperty Scheme.{u})
      (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Stacks.Descent.isClosedImmersion_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcLocalAtTarget.lean, line 454. References: EGA IV (2.7.1), “(xii)”; SGA 3 VIB (12.1), “more general”; SGA 3 VIII (1.7.3), “Closed immersion clause”; SGA 4 IV (8.5.5).

Stacks Project, Tag 02L6. Being a closed immersion is fpqc local on the base.

instance isClosedImmersion_isLocalAtTarget_fpqc :
    (show MorphismProperty Scheme.{u} from @IsClosedImmersion).IsLocalAtTarget
      Scheme.fpqcPrecoverage

Tag 02L7, a lemma

Tag 02L7 in the Stacks Project.

Stacks.Descent.isQuasiAffineHom_descendsAlong_surjective_inf_flat_inf_quasiCompact, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcQuasiAffine.lean, line 133. The attribute's comment: “the descent step”.

Stacks Project, Tag 02L7. Quasi-affine morphisms satisfy fpqc descent: if the base change of g along a surjective flat quasi-compact morphism is quasi-affine, then so is g.

instance isQuasiAffineHom_descendsAlong_surjective_inf_flat_inf_quasiCompact :
    MorphismProperty.DescendsAlong (@IsQuasiAffineHom : MorphismProperty Scheme.{u})
      (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Stacks.Descent.isQuasiAffineHom_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcQuasiAffine.lean, line 153. References: SGA 4 IV (8.5.5).

Stacks Project, Tag 02L7. Being a quasi-affine morphism of schemes is fpqc local on the base.

instance isQuasiAffineHom_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@IsQuasiAffineHom : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02L8, a lemma

Tag 02L8 in the Stacks Project.

AlgebraicGeometry.isLocalAtTarget_isImmersion_inf_quasiCompact_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/Immersion.lean, line 159. References: EGA IV (2.7.1), “more general”; SGA 4 IV (8.5.5).

Stacks Project, Tag 02L8. Quasi-compact immersions are fpqc local on the target.

instance isLocalAtTarget_isImmersion_inf_quasiCompact_fpqc :
    MorphismProperty.IsLocalAtTarget
      (@IsImmersion ⊓ @QuasiCompact : MorphismProperty Scheme.{u}) Scheme.fpqcPrecoverage

Tag 02L9, a lemma

Tag 02L9 in the Stacks Project.

Stacks.Descent.isIntegralHom_descendsAlong_surjective_inf_flat_inf_quasiCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcIntegral.lean, line 91. The attribute's comment: “the descent step”. References: EGA IV (2.7.1), “(xvii)”; SGA 1 VIII (5.7), “detection (integral)”.

Stacks Project, Tag 02L9, the descent step. Integral morphisms satisfy fpqc descent: if the base change of g along a surjective flat quasi-compact morphism is integral, then so is g.

Integrality is universal closedness together with affineness (AlgebraicGeometry.IsIntegralHom.eq_universallyClosed_inf_isAffineHom), and both factors descend along surjective flat quasi-compact morphisms, the second by Tag 02L5.

theorem isIntegralHom_descendsAlong_surjective_inf_flat_inf_quasiCompact :
    MorphismProperty.DescendsAlong (@IsIntegralHom.{u} : MorphismProperty Scheme.{u})
      (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Stacks.Descent.isIntegralHom_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcIntegral.lean, line 100. References: EGA IV (2.7.1), “(xvii)”; SGA 1 VIII (5.7), “more general”; SGA 4 IV (8.5.5).

Stacks Project, Tag 02L9. Integrality of a morphism of schemes is fpqc local on the base.

instance isIntegralHom_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@IsIntegralHom.{u} : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02LA, a lemma

Tag 02LA in the Stacks Project.

Stacks.Morphisms.isFinite_isLocalAtTarget_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FiniteFpqcLocalAtTarget.lean, line 105. References: EGA II (6.3.10), “Locality on X”; EGA IV (2.7.1), “(xv)”; SGA 1 VIII (5.7), “more general”; SGA 4 IV (8.5.5).

Stacks Project, Tag 02LA. Finiteness of a morphism of schemes is local on the base for the fpqc topology.

A finite morphism is an integral morphism which is locally of finite type, integrality is universal closedness together with affineness, and of those three constituents only affineness was missing; it is Tag 02L5, Stacks.Descent.isAffineHom_isLocalAtTarget_fpqc. So this is Stacks.Morphisms.isFinite_isLocalAtTarget_fpqc_of_isAffineHom with its hypothesis discharged.

theorem isFinite_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@IsFinite.{u} : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02VI, a lemma

Tag 02VI in the Stacks Project.

Stacks.Descent.locallyOfFiniteType_inf_locallyQuasiFinite_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcQuasiFinite.lean, line 88. The attribute's comment: “locally quasi-finite case”. References: SGA 1 VIII (3.5), “special case”.

Stacks Project, Tag 02VI. Local quasi-finiteness of a scheme morphism is fpqc local on the base.

instance locallyOfFiniteType_inf_locallyQuasiFinite_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      ((@LocallyOfFiniteType : MorphismProperty Scheme.{u}) ⊓ @LocallyQuasiFinite)
      Scheme.fpqcPrecoverage

Stacks.Descent.finiteType_inf_locallyQuasiFinite_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FpqcQuasiFinite.lean, line 100. The attribute's comment: “quasi-finite case”. References: SGA 1 VIII (3.5), “more general”; SGA 3 VIB (2.1.2), “partial”; SGA 4 IV (8.5.5).

Stacks Project, Tag 02VI. Quasi-finiteness of a scheme morphism is fpqc local on the base.

instance finiteType_inf_locallyQuasiFinite_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget
      (((@LocallyOfFiniteType : MorphismProperty Scheme.{u}) ⊓ @QuasiCompact) ⊓
        @LocallyQuasiFinite) Scheme.fpqcPrecoverage

Tag 02VJ, a lemma

Tag 02VJ in the Stacks Project.

AlgebraicGeometry.locallyOfFiniteTypeRelativeDimension_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/FibreDimension.lean, line 201.

Stacks Project, Tag 02VJ. Being locally of finite type of relative dimension d is fpqc local on the base.

instance locallyOfFiniteTypeRelativeDimension_isLocalAtTarget_fpqc (d : ℕ) :
    (locallyOfFiniteTypeRelativeDimension.{u} d).IsLocalAtTarget Scheme.fpqcPrecoverage

Tag 02VK, a lemma

Tag 02VK in the Stacks Project.

AlgebraicGeometry.syntomic_isLocalAtTarget, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/Syntomic.lean, line 90.

Stacks Project, Tag 02VK. Syntomicity of a morphism of schemes is fpqc local on the base.

instance syntomic_isLocalAtTarget :
    MorphismProperty.IsLocalAtTarget (@Syntomic : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02VL, a lemma

Tag 02VL in the Stacks Project.

Stacks.Descent.smooth_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SmoothFpqcLocalAtTarget.lean, line 51. References: SGA 3 VIB (2.1.2), “partial”; SGA 3 VIIA (8.3.1), “Final descent step”.

Stacks 02VL. Smoothness of morphisms of schemes is local on the base for the fpqc topology.

instance smooth_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@Smooth : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02VM, a lemma

Tag 02VM in the Stacks Project.

AlgebraicGeometry.unramified_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/Unramified.lean, line 65. The attribute's comment: “unramified”. References: EGA IV (17.7.3), “special case”.

Stacks Project, Tag 02VM. Unramifiedness of morphisms of schemes is fpqc local on the base.

instance unramified_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@Unramified : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

AlgebraicGeometry.gUnramified_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/Unramified.lean, line 78. The attribute's comment: “g_unramified”. References: EGA IV (17.7.3), “special case”; SGA 3 VIB (2.1.2), “Remark 2.1.2”; SGA 4 IV (8.5.5), “partial”.

Stacks Project, Tag 02VM. G-unramifiedness of morphisms of schemes is fpqc local on the base.

instance gUnramified_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@GUnramified : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Tag 02VN, a lemma

Tag 02VN in the Stacks Project.

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

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

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

Tag 02VO, a lemma

Tag 02VO in the Stacks Project.

Stacks.Morphisms.isFiniteLocallyFree_descendsAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FiniteFpqcLocalAtTarget.lean, line 119. The attribute's comment: “the descent step, finite locally free”. References: SGA 1 VIII (5.7), “partial”.

The first assertion of Stacks Project, Tag 02VO, the descent step. Finite locally free morphisms satisfy fpqc descent: if the base change of g along a surjective flat quasi-compact morphism is finite locally free, then so is g.

Being finite locally free is being finite, flat and locally of finite presentation, and each factor descends: the first is AlgebraicGeometry.Space.isFinite_descendsAlong_surjective_inf_flat_inf_quasiCompact, which is the descent step of Tag 02LA, and the other two are Mathlib's.

theorem isFiniteLocallyFree_descendsAlong :
    MorphismProperty.DescendsAlong
      (@IsFiniteLocallyFree.{u} : MorphismProperty Scheme.{u})
      ((@Surjective.{u} ⊓ @Flat.{u} ⊓ @QuasiCompact.{u} : MorphismProperty Scheme.{u}))

Stacks.Morphisms.isFiniteLocallyFreeOfRank_descendsAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/FiniteFpqcLocalAtTarget.lean, line 150. The attribute's comment: “the descent step, fixed degree”. References: SGA 1 VIII (5.7), “special case”.

The second assertion of Stacks Project, Tag 02VO, the descent step. Morphisms which are finite locally free of a fixed degree r satisfy fpqc descent: if the base change of g along a surjective flat quasi-compact morphism is finite locally free of degree r, then so is g.

The degree-free case makes g finite, flat and locally of finite presentation, so the rank criterion Stacks.Morphisms.isFiniteLocallyFreeOfRank_iff_forall_finrank_eq applies to both g and its base change and turns the statement into one about the rank function AlgebraicGeometry.Scheme.Hom.finrank. That function is compatible with base change by AlgebraicGeometry.Scheme.Hom.finrank_of_isPullback, and the covering morphism is surjective on points, so the rank of g at an arbitrary point of its target is the rank of the base change at a point above it, which is r.

theorem isFiniteLocallyFreeOfRank_descendsAlong (r : ℕ) :
    MorphismProperty.DescendsAlong (IsFiniteLocallyFreeOfRank.property.{u} r)
      ((@Surjective.{u} ⊓ @Flat.{u} ⊓ @QuasiCompact.{u} : MorphismProperty Scheme.{u}))

Stacks.Morphisms.isFiniteLocallyFree_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteLocallyFree/FpqcLocalAtTarget.lean, line 122. The attribute's comment: “finite locally free”.

Stacks Project, Tag 02VO. Being finite locally free is fpqc local on the base.

instance isFiniteLocallyFree_isLocalAtTarget_fpqc :
    MorphismProperty.IsLocalAtTarget (@IsFiniteLocallyFree : MorphismProperty Scheme.{u})
      Scheme.fpqcPrecoverage

Stacks.Morphisms.isFiniteLocallyFreeOfRank_isLocalAtTarget_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FiniteLocallyFree/FpqcLocalAtTarget.lean, line 131. The attribute's comment: “finite locally free of fixed degree”.

Stacks Project, Tag 02VO. For d : ℕ, being finite locally free of degree d is fpqc local on the base.

instance isFiniteLocallyFreeOfRank_isLocalAtTarget_fpqc (d : ℕ) :
    MorphismProperty.IsLocalAtTarget (IsFiniteLocallyFreeOfRank.property.{u} d)
      Scheme.fpqcPrecoverage

Tag 02YK, a lemma

Tag 02YK in the Stacks Project.

AlgebraicGeometry.isLocalAtTarget_monomorphisms_fpqc, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SchemeProperty/FpqcLocal.lean, line 55. References: EGA IV (2.7.1), “more general”; SGA 4 IV (8.5.5).

Stacks Project, Tag 02YK. Monomorphisms of schemes are fpqc local on the target.

instance isLocalAtTarget_monomorphisms_fpqc :
    (MorphismProperty.monomorphisms Scheme.{u}).IsLocalAtTarget Scheme.fpqcPrecoverage

Tag 0694, a lemma

Tag 0694 in the Stacks Project.

AlgebraicGeometry.isLocalAtTarget_koszulRegularImmersion_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/RegularImmersion.lean, line 311. The attribute's comment: “koszul_regular, étale topology”.

Stacks Project, Tag 0694, the Koszul-regular clause, for the étale topology. Being a Koszul-regular immersion of schemes is local on the target for the étale topology.

theorem isLocalAtTarget_koszulRegularImmersion_etale :
    MorphismProperty.IsLocalAtTarget
      (fun _ _ f => ∃ hf : IsImmersion f, @IsKoszulRegularImmersion _ _ f hf)
      Scheme.etalePrecoverage.{u}

AlgebraicGeometry.isLocalAtTarget_h1RegularImmersion_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/RegularImmersion.lean, line 329. The attribute's comment: “h1_regular, étale topology”.

Stacks Project, Tag 0694, the H₁-regular clause, for the étale topology. Being an H₁-regular immersion of schemes is local on the target for the étale topology.

theorem isLocalAtTarget_h1RegularImmersion_etale :
    MorphismProperty.IsLocalAtTarget
      (fun _ _ f => ∃ hf : IsImmersion f, @IsH1RegularImmersion _ _ f hf)
      Scheme.etalePrecoverage.{u}

AlgebraicGeometry.isLocalAtTarget_quasiRegularImmersion_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/EtaleLocal/RegularImmersion.lean, line 347. The attribute's comment: “quasi_regular, étale topology”.

Stacks Project, Tag 0694, the quasi-regular clause, for the étale topology. Being a quasi-regular immersion of schemes is local on the target for the étale topology.

theorem isLocalAtTarget_quasiRegularImmersion_etale :
    MorphismProperty.IsLocalAtTarget
      (fun _ _ f => ∃ hf : IsImmersion f,
        @RegularIdealSheaf.IsQuasiRegularImmersion _ _ f hf)
      Scheme.etalePrecoverage.{u}

AlgebraicGeometry.isLocalAtTarget_koszulRegularImmersion_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/RegularImmersionFppf.lean, line 214. The attribute's comment: “koszul_regular, erratum: fppf in place of fpqc; counterexample Stacks.Descent.counterexampleHom”. References: SGA 6 VII (1.5), “special case”.

Stacks Project, Tag 0694, the Koszul-regular clause, for the fppf topology. Being a Koszul-regular immersion of schemes is local on the target for the fppf topology, with no quasi-compactness and no hypothesis that the morphism is an immersion.

The tag asserts this for the fpqc topology, where it is false.

theorem isLocalAtTarget_koszulRegularImmersion_fppf :
    MorphismProperty.IsLocalAtTarget
      (fun _ _ f => ∃ hf : IsImmersion f, @IsKoszulRegularImmersion _ _ f hf)
      Scheme.fppfPrecoverage.{u}

AlgebraicGeometry.isLocalAtTarget_h1RegularImmersion_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/RegularImmersionFppf.lean, line 233. The attribute's comment: “h1_regular, erratum: fppf in place of fpqc; counterexample Stacks.Descent.counterexampleHom”.

Stacks Project, Tag 0694, the H₁-regular clause, for the fppf topology. Being an H₁-regular immersion of schemes is local on the target for the fppf topology, with no quasi-compactness and no hypothesis that the morphism is an immersion.

The tag asserts this for the fpqc topology, where it is false.

theorem isLocalAtTarget_h1RegularImmersion_fppf :
    MorphismProperty.IsLocalAtTarget
      (fun _ _ f => ∃ hf : IsImmersion f, @IsH1RegularImmersion _ _ f hf)
      Scheme.fppfPrecoverage.{u}

AlgebraicGeometry.isLocalAtTarget_quasiRegularImmersion_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/RegularImmersionFppf.lean, line 253. The attribute's comment: “quasi_regular, erratum: fppf in place of fpqc; counterexample Stacks.Descent.counterexampleHom”. References: EGA IV (19.1.5), “(ii), special case”.

Stacks Project, Tag 0694, the quasi-regular clause, for the fppf topology. Being a quasi-regular immersion of schemes is local on the target for the fppf topology, with no quasi-compactness and no hypothesis that the morphism is an immersion.

The tag asserts this for the fpqc topology, where it is false.

theorem isLocalAtTarget_quasiRegularImmersion_fppf :
    MorphismProperty.IsLocalAtTarget
      (fun _ _ f => ∃ hf : IsImmersion f,
        @RegularIdealSheaf.IsQuasiRegularImmersion _ _ f hf)
      Scheme.fppfPrecoverage.{u}

AlgebraicGeometry.isLocalAtTarget_koszulRegularImmersion_inf_quasiCompact_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/RegularImmersionFpqc.lean, line 716. The attribute's comment: “koszul_regular”. References: SGA 6 VII (1.5), “special case”.

Stacks Project, Tag 0694, the Koszul-regular clause. Being a quasi-compact Koszul-regular immersion of schemes is local on the target for the fpqc topology.

theorem isLocalAtTarget_koszulRegularImmersion_inf_quasiCompact_fpqc :
    MorphismProperty.IsLocalAtTarget
      ((fun _ _ f => ∃ hf : IsImmersion f, @IsKoszulRegularImmersion _ _ f hf) ⊓
        (@QuasiCompact : MorphismProperty Scheme.{u})) Scheme.fpqcPrecoverage

AlgebraicGeometry.isLocalAtTarget_h1RegularImmersion_inf_quasiCompact_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/RegularImmersionFpqc.lean, line 734. The attribute's comment: “h1_regular”.

Stacks Project, Tag 0694, the H₁-regular clause. Being a quasi-compact H₁-regular immersion of schemes is local on the target for the fpqc topology.

theorem isLocalAtTarget_h1RegularImmersion_inf_quasiCompact_fpqc :
    MorphismProperty.IsLocalAtTarget
      ((fun _ _ f => ∃ hf : IsImmersion f, @IsH1RegularImmersion _ _ f hf) ⊓
        (@QuasiCompact : MorphismProperty Scheme.{u})) Scheme.fpqcPrecoverage

AlgebraicGeometry.isLocalAtTarget_quasiRegularImmersion_inf_quasiCompact_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/RegularImmersionFpqc.lean, line 752. The attribute's comment: “quasi_regular”. References: EGA IV (19.1.5), “(ii), special case”.

Stacks Project, Tag 0694, the quasi-regular clause. Being a quasi-compact quasi-regular immersion of schemes is local on the target for the fpqc topology.

theorem isLocalAtTarget_quasiRegularImmersion_inf_quasiCompact_fpqc :
    MorphismProperty.IsLocalAtTarget
      ((fun _ _ f => ∃ hf : IsImmersion f,
          @RegularIdealSheaf.IsQuasiRegularImmersion _ _ f hf) ⊓
        (@QuasiCompact : MorphismProperty Scheme.{u})) Scheme.fpqcPrecoverage

AlgebraicGeometry.isKoszulRegularImmersion_iff_of_fpqcZeroHypercover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/RegularImmersionFpqcOfImmersion.lean, line 177. The attribute's comment: “koszul_regular, erratum: morphisms that are immersions; fpqc, no quasi-compactness”. References: SGA 6 VII (1.5).

Stacks Project, Tag 0694, the Koszul-regular clause, for an immersion. An immersion of schemes is Koszul-regular if and only if its base changes along the members of an fpqc covering of the target are, with no quasi-compactness.

theorem isKoszulRegularImmersion_iff_of_fpqcZeroHypercover
    {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
    (𝒰 : Precoverage.ZeroHypercover.{w} Scheme.fpqcPrecoverage X) :
    IsKoszulRegularImmersion i ↔ ∀ k, IsKoszulRegularImmersion (pullback.snd i (𝒰.f k))

AlgebraicGeometry.isH1RegularImmersion_iff_of_fpqcZeroHypercover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/RegularImmersionFpqcOfImmersion.lean, line 197. The attribute's comment: “h1_regular, erratum: morphisms that are immersions; fpqc, no quasi-compactness”.

Stacks Project, Tag 0694, the H₁-regular clause, for an immersion. An immersion of schemes is H₁-regular if and only if its base changes along the members of an fpqc covering of the target are, with no quasi-compactness.

theorem isH1RegularImmersion_iff_of_fpqcZeroHypercover
    {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
    (𝒰 : Precoverage.ZeroHypercover.{w} Scheme.fpqcPrecoverage X) :
    IsH1RegularImmersion i ↔ ∀ k, IsH1RegularImmersion (pullback.snd i (𝒰.f k))

AlgebraicGeometry.isQuasiRegularImmersion_iff_of_fpqcZeroHypercover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/RegularImmersionFpqcOfImmersion.lean, line 218. The attribute's comment: “quasi_regular, erratum: morphisms that are immersions; fpqc, no quasi-compactness”. References: EGA IV (19.1.5), “more general”.

Stacks Project, Tag 0694, the quasi-regular clause, for an immersion. An immersion of schemes is quasi-regular if and only if its base changes along the members of an fpqc covering of the target are, with no quasi-compactness.

theorem isQuasiRegularImmersion_iff_of_fpqcZeroHypercover
    {Z X : Scheme.{u}} (i : Z ⟶ X) [IsImmersion i]
    (𝒰 : Precoverage.ZeroHypercover.{w} Scheme.fpqcPrecoverage X) :
    RegularIdealSheaf.IsQuasiRegularImmersion i ↔
      ∀ k, RegularIdealSheaf.IsQuasiRegularImmersion (pullback.snd i (𝒰.f k))

Stacks.Descent.not_isLocalAtTarget_koszulRegularImmersion_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/RegularImmersionNotFpqcLocal.lean, line 224. The attribute's comment: “koszul_regular, counterexample: false for fpqc coverings without quasi-compactness”.

Stacks Project, Tag 0694, the Koszul-regular clause, is false for the fpqc topology. Being a Koszul-regular immersion is not local on the target for the fpqc precoverage.

theorem not_isLocalAtTarget_koszulRegularImmersion_fpqc :
    ¬ MorphismProperty.IsLocalAtTarget
      (fun _ _ f => ∃ hf : IsImmersion f, @IsKoszulRegularImmersion _ _ f hf)
      Scheme.fpqcPrecoverage.{0}

Stacks.Descent.not_isLocalAtTarget_h1RegularImmersion_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/RegularImmersionNotFpqcLocal.lean, line 241. The attribute's comment: “h1_regular, counterexample: false for fpqc coverings without quasi-compactness”.

Stacks Project, Tag 0694, the H₁-regular clause, is false for the fpqc topology. Being an H₁-regular immersion is not local on the target for the fpqc precoverage.

theorem not_isLocalAtTarget_h1RegularImmersion_fpqc :
    ¬ MorphismProperty.IsLocalAtTarget
      (fun _ _ f => ∃ hf : IsImmersion f, @IsH1RegularImmersion _ _ f hf)
      Scheme.fpqcPrecoverage.{0}

Stacks.Descent.not_isLocalAtTarget_quasiRegularImmersion_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/RegularImmersionNotFpqcLocal.lean, line 258. The attribute's comment: “quasi_regular, counterexample: false for fpqc coverings without quasi-compactness”.

Stacks Project, Tag 0694, the quasi-regular clause, is false for the fpqc topology. Being a quasi-regular immersion is not local on the target for the fpqc precoverage.

theorem not_isLocalAtTarget_quasiRegularImmersion_fpqc :
    ¬ MorphismProperty.IsLocalAtTarget
      (fun _ _ f => ∃ hf : IsImmersion f, @RegularIdealSheaf.IsQuasiRegularImmersion _ _ f hf)
      Scheme.fpqcPrecoverage.{0}

Sources

• Section 35.23, Tag 02YJ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Descent.quasiCompact_descendsAlong_surjective_inf_flat_inf_quasiCompact · Stacks.Descent.quasiCompact_isLocalAtTarget_fpqc · AlgebraicGeometry.quasiSeparated_isLocalAtTarget_fpqc · AlgebraicGeometry.universallyClosed_isLocalAtTarget_fpqc · AlgebraicGeometry.universallyOpen_isLocalAtTarget_fpqc · AlgebraicGeometry.universallyQuotientMap_isLocalAtTarget_fpqc · AlgebraicGeometry.isSeparated_isLocalAtTarget_fpqc · Stacks.Descent.surjective_isLocalAtTarget_fpqc

Section35.24 Properties of morphisms local in the fppf topology on the target#

Section 35.24 of the Stacks Project, Tag 02YL. 2 tags here are carried by 1 declaration of the repository (in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02YM, a lemma

Tag 02YM in the Stacks Project.

Declarations registered for the tag:

• Stacks.Descent.isImmersion_isLocalAtTarget_fppf, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Descent/MorphismPropertyTopology/FppfLocalAtTarget.lean, line 345 (StacksFrontier).

Tag 0H8J, a lemma

Tag 0H8J in the Stacks Project.

AlgebraicGeometry.isDominant_isLocalAtTarget_fppf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/LocalOnTarget/Dominant.lean, line 113. References: EGA I (2.2.8), “more general”.

Stacks Project, Tag 0H8J. Being dominant is fppf local on the base.

instance isDominant_isLocalAtTarget_fppf :
    MorphismProperty.IsLocalAtTarget (@IsDominant : MorphismProperty Scheme.{u})
      Scheme.fppfPrecoverage

Sources

• Section 35.24, Tag 02YL
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Descent.isImmersion_isLocalAtTarget_fppf · AlgebraicGeometry.isDominant_isLocalAtTarget_fppf

Section35.25 Application of fpqc descent of properties of morphisms#

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

Tag 02LC, a lemma

Tag 02LC in the Stacks Project.

AlgebraicGeometry.isOpenImmersion_of_etale_universallyInjective, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FpqcDescentApplication/OpenImmersion.lean, line 53. References: EGA IV (17.9.1), “c) => a)”; SGA 1 IX (1.4), “étale+radicial ⇒ open”; SGA 1 I (5.1), “sufficiency”.

A universally injective étale morphism of schemes is an open immersion.

public instance isOpenImmersion_of_etale_universallyInjective
    {X Y : Scheme.{u}} (f : X ⟶ Y) [Etale f] [UniversallyInjective f] :
    IsOpenImmersion f

Tag 09NP, a lemma

Tag 09NP in the Stacks Project.

AlgebraicGeometry.universallyInjective_of_flat_of_separated_of_genericPoints_injOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/SchemeProperty/UniversallyInjective.lean, line 60.

Stacks Project, Tag 09NP. A flat separated morphism with isomorphic residue fields at, and distinct images of, the generic points of its source is universally injective.

public theorem universallyInjective_of_flat_of_separated_of_genericPoints_injOn
    {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsSeparated f]
    (hres : ∀ ξ ∈ genericPoints X, IsIso (f.residueFieldMap ξ))
    (hinj : Set.InjOn f (genericPoints X)) :
    UniversallyInjective f

Tag 09NQ, a lemma

Tag 09NQ in the Stacks Project.

AlgebraicGeometry.isOpenImmersion_of_etale_of_separated_of_genericPoints_injOn, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FpqcDescentApplication/OpenImmersion.lean, line 63.

An étale separated morphism with isomorphic residue fields at, and distinct images of, the generic points of its source is an open immersion.

public theorem isOpenImmersion_of_etale_of_separated_of_genericPoints_injOn
    {X Y : Scheme.{u}} (f : X ⟶ Y) [Etale f] [IsSeparated f]
    (hres : ∀ ξ ∈ genericPoints X, IsIso (f.residueFieldMap ξ))
    (hinj : Set.InjOn f (genericPoints X)) :
    IsOpenImmersion f

Tag 0F4J, a lemma

Tag 0F4J in the Stacks Project.

AlgebraicGeometry.isProperOver_of_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/ProperClosedSubsetFpqc.lean, line 49.

Stacks 0F4J. Properness over a base of a closed subset descends along an fpqc covering of the base.

public theorem isProperOver_of_fpqc {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f]
    (Z : Closeds X)
    (h : ∃ (ι : Type v) (Y' : ι → Scheme.{u}) (g : ∀ i, Y' i ⟶ Y),
      Presieve.ofArrows Y' g ∈ Scheme.fpqcPrecoverage Y ∧
        ∀ i, IsProperOver (pullback.snd f (g i))
          (Z.preimage (pullback.fst f (g i)).continuous)) :
    IsProperOver f Z

Tag 0D2P, a lemma

Tag 0D2P in the Stacks Project.

Stacks.Descent.isRelativelyAmple_pullbackModule_of_fpqcCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/RelativeAmpleFpqcLocalOnBase.lean, line 181. The attribute's comment: “(1) implies (2)”.

Stacks Tag 0D2P, clause (1) implies clause (2). Let f : X ⟶ S be a morphism of schemes, L an invertible 𝒪_X-module and {g i : S' i ⟶ S} an fpqc covering of S. Let f' i be the base change of f along g i, presented by a cartesian square with the other projection p i : X' i ⟶ X. If L is ample relative to f, then (p i)^* L is ample relative to f' i for every i.

This is [Stacks, Tag 0893] for a cartesian square, Stacks.AmpleBridge.isRelativelyAmple_pullbackModule_of_isPullback, applied one index at a time; no property of the covering enters, and the fpqc hypothesis is carried only so that the statement is literally the implication of the source.

theorem isRelativelyAmple_pullbackModule_of_fpqcCover {S : Scheme.{u}} {I : Type v}
    {S' : I → Scheme.{u}} (g : ∀ i, S' i ⟶ S)
    (_hg : Presieve.ofArrows S' g ∈ Scheme.fpqcPrecoverage S) {X : Scheme.{u}} (f : X ⟶ S)
    (L : X.Modules) [IsInvertibleModule X L] {X' : I → Scheme.{u}} {p : ∀ i, X' i ⟶ X}
    {f' : ∀ i, X' i ⟶ S' i} (hsq : ∀ i, IsPullback (p i) (f' i) f (g i))
    (hL : Stacks.RelativeAmple.IsRelativelyAmple f L) :
    ∀ i, Stacks.RelativeAmple.IsRelativelyAmple (f' i) (pullbackModule (p i) L)

Stacks.Descent.isRelativelyAmple_iff_forall_of_fpqcCover_of_iso_unitModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/RelativeAmpleFpqcLocalOnBase.lean, line 238. The attribute's comment: “the full equivalence for an invertible module isomorphic to the structure sheaf”. References: SGA 1 VIII (7.8), “special case”.

Stacks Tag 0D2P, both directions, for an invertible module isomorphic to 𝒪_X. With {g i : S' i ⟶ S} an fpqc covering of S and each square with sides p i, f' i, f and g i cartesian, a module L isomorphic to the structure sheaf is ample relative to f if and only if (p i)^* L is ample relative to f' i for every i.

Both sides are quasi-affineness: on the left by Stacks.AmplePullback.isRelativelyAmple_iff_isQuasiAffineHom_of_iso_unitModule, which is [Stacks, Tag 0891] for a module merely isomorphic to 𝒪_X, and on the right by the same lemma applied to the isomorphism Stacks.AmplePullback.modulePullbackIsoUnitModule of (p i)^* L with 𝒪_{X' i}. The equivalence between them is then [Stacks, Tag 02L7], that quasi-affine morphisms are fpqc local on the base.

theorem isRelativelyAmple_iff_forall_of_fpqcCover_of_iso_unitModule {S : Scheme.{u}} {I : Type v}
    {S' : I → Scheme.{u}} {g : ∀ i, S' i ⟶ S}
    (hg : Presieve.ofArrows S' g ∈ Scheme.fpqcPrecoverage S) {X : Scheme.{u}} (f : X ⟶ S)
    (L : X.Modules) [IsInvertibleModule X L] (e : L ≅ unitModule X) {X' : I → Scheme.{u}}
    {p : ∀ i, X' i ⟶ X} {f' : ∀ i, X' i ⟶ S' i}
    (hsq : ∀ i, IsPullback (p i) (f' i) f (g i)) :
    Stacks.RelativeAmple.IsRelativelyAmple f L ↔
      ∀ i, Stacks.RelativeAmple.IsRelativelyAmple (f' i) (pullbackModule (p i) L)

Stacks.Descent.isRelativelyAmple_iff_forall_of_fpqcCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/RelativeAmpleFpqcLocalOnBaseFull.lean, line 363. References: SGA 1 VIII (7.8), “more general”.

Stacks Tag 0D2P. Let f : X ⟶ S be a morphism of schemes, L an invertible 𝒪_X-module and {g i : S' i ⟶ S}_{i ∈ I} an fpqc covering of S. Let f' i : X' i ⟶ S' i be the base change of f along g i, presented by a cartesian square with other projection p i : X' i ⟶ X, and let (p i)^* L be the pullback of L. The following are equivalent:

1. L is ample on X / S;
2. (p i)^* L is ample on X' i / S' i for every i ∈ I.

Clause (1) implies clause (2) by [Stacks, Tag 0893] applied to each square, Stacks.Descent.isRelativelyAmple_pullbackModule_of_fpqcCover. Clause (2) implies clause (1) is Stacks.Descent.isRelativelyAmple_of_forall_of_fpqcCover.

theorem isRelativelyAmple_iff_forall_of_fpqcCover {S : Scheme.{u}} {I : Type v}
    {S' : I → Scheme.{u}} {g : ∀ i, S' i ⟶ S}
    (hg : Presieve.ofArrows S' g ∈ Scheme.fpqcPrecoverage S) {X : Scheme.{u}} (f : X ⟶ S)
    (L : X.Modules) [IsInvertibleModule X L] {X' : I → Scheme.{u}} {p : ∀ i, X' i ⟶ X}
    {f' : ∀ i, X' i ⟶ S' i} (hsq : ∀ i, IsPullback (p i) (f' i) f (g i)) :
    Stacks.RelativeAmple.IsRelativelyAmple f L ↔
      ∀ i, Stacks.RelativeAmple.IsRelativelyAmple (f' i) (pullbackModule (p i) L)

Sources

• Section 35.25, Tag 02LB
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isOpenImmersion_of_etale_universallyInjective · AlgebraicGeometry.universallyInjective_of_flat_of_separated_of_genericPoints_injOn · AlgebraicGeometry.isOpenImmersion_of_etale_of_separated_of_genericPoints_injOn · AlgebraicGeometry.isProperOver_of_fpqc · Stacks.Descent.isRelativelyAmple_pullbackModule_of_fpqcCover · Stacks.Descent.isRelativelyAmple_iff_forall_of_fpqcCover_of_iso_unitModule · Stacks.Descent.isRelativelyAmple_iff_forall_of_fpqcCover

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.