59.99 Comparing big and small… to 59.107 Cohomology of the…

Section59.99 Comparing big and small topoi #

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

Tag 0758, a lemma

Tag 0758 in the Stacks Project.

AlgebraicGeometry.injective_smallEtaleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/Restriction.lean, line 200. The attribute's comment: “injective_restrict_s”.

Stacks Project, Tag 0758. Restriction of an injective abelian sheaf from the big étale site over S to the small étale site of S is injective.

public theorem injective_smallEtaleRestriction
    (S : Scheme.{u}) (hS : B.Contains S)
    (I : Sheaf (BigEtaleOver.topology B S hS) Ab.{u + 1})
    [Injective I] :
    Injective (((SmallEtale.inclusion B S hS).sheafPushforwardContinuous
      Ab.{u + 1} (SmallEtale.topology B S hS)
      (BigEtaleOver.topology B S hS)).obj I)

AlgebraicGeometry.injective_smallEtaleRestrictionAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/Restriction.lean, line 212. The attribute's comment: “injective_restrict_t”.

Stacks Project, Tag 0758. Restriction to the small étale site of an object of the big étale site preserves injectivity of abelian sheaves.

public theorem injective_smallEtaleRestrictionAlong
    (T S : B.Scheme) (f : T ⟶ S)
    (I : Sheaf (BigEtaleOver.topology B S.obj S.property) Ab.{u + 1})
    [Injective I] :
    Injective
      (((smallEtaleToBigEtaleFunctor B T S f).sheafPushforwardContinuous
        Ab.{u + 1} (SmallEtale.topology B T.obj T.property)
        (BigEtaleOver.topology B S.obj S.property)).obj I)

AlgebraicGeometry.isKInjective_smallEtaleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/Restriction.lean, line 225. The attribute's comment: “kinjective_restrict_s”.

Stacks Project, Tag 0758. Restriction of a K-injective complex of abelian sheaves from the big étale site to the small étale site is K-injective.

public theorem isKInjective_smallEtaleRestriction
    (S : Scheme.{u}) (hS : B.Contains S)
    (I : CochainComplex (Sheaf (BigEtaleOver.topology B S hS) Ab.{u + 1}) ℤ)
    [I.IsKInjective] :
    CochainComplex.IsKInjective
      ((((SmallEtale.inclusion B S hS).sheafPushforwardContinuous
        Ab.{u + 1} (SmallEtale.topology B S hS)
        (BigEtaleOver.topology B S hS)).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj I)

AlgebraicGeometry.isKInjective_smallEtaleRestrictionAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/Restriction.lean, line 239. The attribute's comment: “kinjective_restrict_t”.

Stacks Project, Tag 0758. Restriction to the small étale site of an object of the big étale site preserves K-injectivity of abelian sheaf complexes.

public theorem isKInjective_smallEtaleRestrictionAlong
    (T S : B.Scheme) (f : T ⟶ S)
    (I : CochainComplex (Sheaf (BigEtaleOver.topology B S.obj S.property) Ab.{u + 1}) ℤ)
    [I.IsKInjective] :
    CochainComplex.IsKInjective
      ((((smallEtaleToBigEtaleFunctor B T S f).sheafPushforwardContinuous
        Ab.{u + 1} (SmallEtale.topology B T.obj T.property)
        (BigEtaleOver.topology B S.obj S.property)).mapHomologicalComplex
          (ComplexShape.up ℤ)).obj I)

Tag 0759, an equation

Tag 0759 in the Stacks Project.

AlgebraicGeometry.smallEtaleRestrictionPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/DirectImage.lean, line 65. The attribute's comment: “arbitrary_coefficients”.

For a sheaf ℱ on the big étale site over T with values in any category, the restriction (f_{big, *}ℱ)|_{S_étale} of its direct image along f agrees naturally with the direct image f_{small, *}(ℱ|_{T_étale}) of its restriction.

public noncomputable def smallEtaleRestrictionPushforwardIso (A : Type w) [Category.{w'} A] :
    (Over.pullback f).sheafPushforwardContinuous A
        (BigEtaleOver.topology B S.obj S.property)
        (BigEtaleOver.topology B T.obj T.property) ⋙
      (SmallEtale.inclusion B S.obj S.property).sheafPushforwardContinuous A
        (SmallEtale.topology B S.obj S.property)
        (BigEtaleOver.topology B S.obj S.property) ≅
    (SmallEtale.inclusion B T.obj T.property).sheafPushforwardContinuous A
        (SmallEtale.topology B T.obj T.property)
        (BigEtaleOver.topology B T.obj T.property) ⋙
      (smallEtaleBaseChange B f).sheafPushforwardContinuous A
        (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property)

AlgebraicGeometry.bigEtaleRestrictionPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/DirectImage.lean, line 112. The attribute's comment: “direct_images_of_topoi”.

The direct image along the morphism of topoi f_big followed by restriction along the projection π_S agrees naturally with restriction along π_T followed by the direct image along f_small.

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

AlgebraicGeometry.smallEtaleRestrictionPushforwardModules_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ModulePullback.lean, line 277. The attribute's comment: “sheaves of 𝒪-modules on the big and small étale sites of schemes, at the module universe u + 1 of the étale cohomology comparisons of Stacks 0DDH”.

Restriction to the small étale site of S of the direct image along f_big of a sheaf of 𝒪-modules is the direct image along f_small of its restriction to the small étale site of T: (f_{big,*}ℱ)|_{S_étale} = f_{small,*}(ℱ|_{T_étale}), as an equality of functors.

public theorem smallEtaleRestrictionPushforwardModules_eq :
    Stacks.SheafOfModules.inverseImage.{u + 1}
          (SmallEtale.topology B T.obj T.property)
          (BigEtaleOver.topology B T.obj T.property)
          (SmallEtale.inclusion B T.obj T.property)
          (BigEtaleOver.structureSheaf B T.obj T.property) ⋙
        smallEtaleModulePushforward B T S f =
      bigEtaleModulePushforward B T S f ⋙
        Stacks.SheafOfModules.inverseImage.{u + 1}
          (SmallEtale.topology B S.obj S.property)
          (BigEtaleOver.topology B S.obj S.property)
          (SmallEtale.inclusion B S.obj S.property)
          (BigEtaleOver.structureSheaf B S.obj S.property)

AlgebraicGeometry.smallEtaleModulePullbackProjectionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ModulePullback.lean, line 350. The attribute's comment: “inverse images of sheaves of 𝒪-modules on the big and small étale sites of schemes, at the module universe u + 1 of the étale cohomology comparisons of Stacks 0DDH”.

The mate of AlgebraicGeometry.smallEtaleRestrictionPushforwardModules_eq on inverse images of sheaves of 𝒪-modules on the big and small étale sites of schemes: π_T^* ∘ f_small^* ≅ f_big^* ∘ π_S^*, that is f_big^{-1}(π_S^*K) ≅ π_T^*(f_small^*K), where π^* is the lower shriek of Stacks 0797 along the small étale inclusion and f_big^* is the inverse image of Stacks 04CC part (2).

public def smallEtaleModulePullbackProjectionIso :
    smallEtaleModulePullbackLarge B T S f ⋙
        Stacks.SheafOfModules.lowerShriek.{u + 1}
          (SmallEtale.topology B T.obj T.property)
          (BigEtaleOver.topology B T.obj T.property)
          (SmallEtale.inclusion B T.obj T.property)
          (BigEtaleOver.structureSheaf B T.obj T.property) ≅
      Stacks.SheafOfModules.lowerShriek.{u + 1}
          (SmallEtale.topology B S.obj S.property)
          (BigEtaleOver.topology B S.obj S.property)
          (SmallEtale.inclusion B S.obj S.property)
          (BigEtaleOver.structureSheaf B S.obj S.property) ⋙
        bigEtaleInverseImageModules B T S f

AlgebraicGeometry.bigEtalePullbackProjectionPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ProjectionPullback.lean, line 130. The attribute's comment: “inverse images”.

The inverse-image square of Stacks 0759. Pulling a sheaf on the small étale site of S back to the big étale site over S and then restricting along f agrees with pulling it back to the small étale site of T and then up to the big étale site over T: f_{big}^{-1}π_S^{-1} ≅ π_T^{-1}f_{small}^{-1}.

This is the mate of AlgebraicGeometry.smallEtaleRestrictionPushforwardIso: all four functors are left adjoints of the four restrictions appearing there, and uniqueness of left adjoints transports the isomorphism.

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

Tag 075A, a lemma

Tag 075A in the Stacks Project.

AlgebraicGeometry.bigEtaleDerivedPushforwardBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/BaseChange.lean, line 125. The attribute's comment: “big_site_base_change_abelian”.

Base change for the derived direct image of abelian sheaves on big étale sites.

public noncomputable def bigEtaleDerivedPushforwardBaseChangeIso
    (D : CartesianBaseChangeSituation.{u})
    [HasSheafify (BigEtaleOver.topology D.B D.T.obj D.T.property) Ab.{u + 1}]
    [HasSheafify (BigEtaleOver.topology D.B D.S.obj D.S.property) Ab.{u + 1}]
    [HasSheafify (BigEtaleOver.topology D.B D.T'.obj D.T'.property) Ab.{u + 1}]
    [HasSheafify (BigEtaleOver.topology D.B D.S'.obj D.S'.property) Ab.{u + 1}]
    [HasDerivedCategory.{wT} (Sheaf (BigEtaleOver.topology D.B D.T.obj D.T.property) Ab.{u + 1})]
    [HasDerivedCategory.{wS} (Sheaf (BigEtaleOver.topology D.B D.S.obj D.S.property) Ab.{u + 1})]
    [HasDerivedCategory.{wT'} (Sheaf (BigEtaleOver.topology D.B D.T'.obj D.T'.property) Ab.{u + 1})]
    [HasDerivedCategory.{wS'} (Sheaf (BigEtaleOver.topology D.B D.S'.obj D.S'.property) Ab.{u + 1})]
    [(Over.map D.g.hom).IsContinuous
      (BigEtaleOver.topology D.B D.S'.obj D.S'.property)
      (BigEtaleOver.topology D.B D.S.obj D.S.property)]
    [(Over.map D.g').IsContinuous
      (BigEtaleOver.topology D.B D.T'.obj D.T'.property)
      (BigEtaleOver.topology D.B D.T.obj D.T.property)]
    [((Over.map D.f).sheafPushforwardCocontinuous Ab.{u + 1}
      (BigEtaleOver.topology D.B D.T.obj D.T.property)
      (BigEtaleOver.topology D.B D.S.obj D.S.property)).Additive]
    [((Over.map D.f').sheafPushforwardCocontinuous Ab.{u + 1}
      (BigEtaleOver.topology D.B D.T'.obj D.T'.property)
      (BigEtaleOver.topology D.B D.S'.obj D.S'.property)).Additive]
    [((Over.map D.g.hom).sheafPushforwardContinuous Ab.{u + 1}
      (BigEtaleOver.topology D.B D.S'.obj D.S'.property)
      (BigEtaleOver.topology D.B D.S.obj D.S.property)).Additive]
    [((Over.map D.g').sheafPushforwardContinuous Ab.{u + 1}
      (BigEtaleOver.topology D.B D.T'.obj D.T'.property)
      (BigEtaleOver.topology D.B D.T.obj D.T.property)).Additive]
    (Rf : DerivedCategory (Sheaf (BigEtaleOver.topology D.B D.T.obj D.T.property) Ab.{u + 1}) ⥤
      DerivedCategory (Sheaf (BigEtaleOver.topology D.B D.S.obj D.S.property) Ab.{u + 1}))
    (Rf' : DerivedCategory (Sheaf (BigEtaleOver.topology D.B D.T'.obj D.T'.property) Ab.{u + 1}) ⥤
      DerivedCategory (Sheaf (BigEtaleOver.topology D.B D.S'.obj D.S'.property) Ab.{u + 1}))
    (Rg : DerivedCategory (Sheaf (BigEtaleOver.topology D.B D.S.obj D.S.property) Ab.{u + 1}) ⥤
      DerivedCategory (Sheaf (BigEtaleOver.topology D.B D.S'.obj D.S'.property) Ab.{u + 1}))
    (Rg' : DerivedCategory (Sheaf (BigEtaleOver.topology D.B D.T.obj D.T.property) Ab.{u + 1}) ⥤
      DerivedCategory (Sheaf (BigEtaleOver.topology D.B D.T'.obj D.T'.property) Ab.{u + 1}))
    (αf : homotopyToDerived
      ((Over.map D.f).sheafPushforwardCocontinuous Ab.{u + 1}
        (BigEtaleOver.topology D.B D.T.obj D.T.property)
        (BigEtaleOver.topology D.B D.S.obj D.S.property)) ⟶ DerivedCategory.Qh ⋙ Rf)
    (αf' : homotopyToDerived
      ((Over.map D.f').sheafPushforwardCocontinuous Ab.{u + 1}
        (BigEtaleOver.topology D.B D.T'.obj D.T'.property)
        (BigEtaleOver.topology D.B D.S'.obj D.S'.property)) ⟶ DerivedCategory.Qh ⋙ Rf')
    (αg : homotopyToDerived
      ((Over.map D.g.hom).sheafPushforwardContinuous Ab.{u + 1}
        (BigEtaleOver.topology D.B D.S'.obj D.S'.property)
        (BigEtaleOver.topology D.B D.S.obj D.S.property)) ⟶ DerivedCategory.Qh ⋙ Rg)
    (αg' : homotopyToDerived
      ((Over.map D.g').sheafPushforwardContinuous Ab.{u + 1}
        (BigEtaleOver.topology D.B D.T'.obj D.T'.property)
        (BigEtaleOver.topology D.B D.T.obj D.T.property)) ⟶ DerivedCategory.Qh ⋙ Rg')
    [Rf.IsRightDerivedFunctor αf (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    [Rf'.IsRightDerivedFunctor αf' (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    [Rg.IsRightDerivedFunctor αg (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))]
    [Rg'.IsRightDerivedFunctor αg' (HomotopyCategory.quasiIso _ (ComplexShape.up ℤ))] :
    Rf ⋙ Rg ≅ Rg' ⋙ Rf'

AlgebraicGeometry.bigSmallEtaleDerivedPushforwardRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/DerivedPushforwardRestriction.lean, line 178. The attribute's comment: “part (1)”.

For a morphism f : T ⟶ S of schemes and K in the unbounded derived category D((Sch/T)_étale) of abelian sheaves on the big étale site, (Rf_{big, *}K)|_{S_étale} = Rf_{small, *}(K|_{T_étale}) in D(S_étale), naturally in K.

def bigSmallEtaleDerivedPushforwardRestrictionIso :
    bigEtaleDerivedPushforward B f ⋙ (smallEtaleAbelianRestriction B S).mapDerivedCategory ≅
      (smallEtaleAbelianRestriction B T).mapDerivedCategory ⋙ smallEtaleDerivedPushforward B f

AlgebraicGeometry.bigEtaleDerivedPushforwardInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/DerivedPushforwardRestriction.lean, line 282. The attribute's comment: “part (5)”.

Let f : T ⟶ S be a morphism of schemes, g : S' ⟶ S an object of (Sch/S)_étale and T' = T ×_S S' with projections f' : T' ⟶ S' and g' : T' ⟶ T. For K in D((Sch/T)_étale), g_big^{-1}(Rf_{big, *}K) = Rf'_{big, *}((g'_big)^{-1}K) in D((Sch/S')_étale), naturally in K.

def bigEtaleDerivedPushforwardInverseImageIso :
    bigEtaleDerivedPushforward D.B D.f ⋙
        (bigEtaleAbelianInverseImage D.B D.gHom).mapDerivedCategory ≅
      (bigEtaleAbelianInverseImage D.B D.g').mapDerivedCategory ⋙
        bigEtaleDerivedPushforward D.B D.f'

AlgebraicGeometry.smallEtaleDerivedPushforwardRestrictionAlongIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/DerivedPushforwardRestriction.lean, line 323. The attribute's comment: “part (3)”.

In the situation of part (5), for K in D((Sch/T)_étale), i_g^{-1}(Rf_{big, *}K) = Rf'_{small, *}(i_{g'}^{-1}K) in D(S'_étale), naturally in K.

def smallEtaleDerivedPushforwardRestrictionAlongIso :
    bigEtaleDerivedPushforward D.B D.f ⋙
        (smallEtaleAbelianRestrictionAlong D.B D.gHom).mapDerivedCategory ≅
      (smallEtaleAbelianRestrictionAlong D.B D.g').mapDerivedCategory ⋙
        smallEtaleDerivedPushforward D.B D.f'

AlgebraicGeometry.bigSmallEtaleDerivedModulePushforwardRestrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/DerivedPushforwardRestriction.lean, line 498. The attribute's comment: “part (2)”.

For a morphism f : T ⟶ S of schemes and K in the unbounded derived category D((Sch/T)_étale, 𝒪) of 𝒪-modules on the big étale site, (Rf_{big, *}K)|_{S_étale} = Rf_{small, *}(K|_{T_étale}) in D(Mod(S_étale, 𝒪_S)), naturally in K.

def bigSmallEtaleDerivedModulePushforwardRestrictionIso :
    Stacks.Cohomology.DerivedPushforward.derivedPushforward (X := bigEtaleOverRingedTopos B T)
        (Y := bigEtaleOverRingedTopos B S) (bigEtaleRingedToposHom B f) ⋙
        (bigToSmallEtaleRingedToposHom B S).pushforwardModules.mapDerivedCategory ≅
      (bigToSmallEtaleRingedToposHom B T).pushforwardModules.mapDerivedCategory ⋙
        Stacks.Cohomology.DerivedPushforward.derivedPushforward (X := smallEtaleRingedTopos B T)
          (Y := smallEtaleRingedTopos B S) (smallEtaleRingedToposHom B f)

AlgebraicGeometry.bigEtaleDerivedModulePushforwardInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/DerivedPushforwardRestriction.lean, line 643. The attribute's comment: “part (6)”.

Let f : T ⟶ S be a morphism of schemes, g : S' ⟶ S an object of (Sch/S)_étale and T' = T ×_S S' with projections f' : T' ⟶ S' and g' : T' ⟶ T. For K in D((Sch/T)_étale, 𝒪), g_big^*(Rf_{big, *}K) = Rf'_{big, *}((g'_big)^*K) in D((Sch/S')_étale, 𝒪), naturally in K.

def bigEtaleDerivedModulePushforwardInverseImageIso :
    Stacks.Cohomology.DerivedPushforward.derivedPushforward (X := bigEtaleOverRingedTopos D.B D.T)
        (Y := bigEtaleOverRingedTopos D.B D.S) (bigEtaleRingedToposHom D.B D.f) ⋙
        (bigEtaleModuleInverseImage D.B D.gHom).mapDerivedCategory ≅
      (bigEtaleModuleInverseImage D.B D.g').mapDerivedCategory ⋙
        Stacks.Cohomology.DerivedPushforward.derivedPushforward
          (X := bigEtaleOverRingedTopos D.B D.T') (Y := bigEtaleOverRingedTopos D.B D.S')
          (bigEtaleRingedToposHom D.B D.f')

AlgebraicGeometry.smallEtaleDerivedModulePushforwardRestrictionAlongIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/DerivedPushforwardRestriction.lean, line 693. The attribute's comment: “part (4)”.

In the situation of part (6), for K in D((Sch/T)_étale, 𝒪), i_g^*(Rf_{big, *}K) = Rf'_{small, *}(i_{g'}^*K) in D(Mod(S'_étale, 𝒪_{S'})), naturally in K.

def smallEtaleDerivedModulePushforwardRestrictionAlongIso :
    Stacks.Cohomology.DerivedPushforward.derivedPushforward (X := bigEtaleOverRingedTopos D.B D.T)
        (Y := bigEtaleOverRingedTopos D.B D.S) (bigEtaleRingedToposHom D.B D.f) ⋙
        (smallEtaleModuleRestrictionAlong D.B D.gHom).mapDerivedCategory ≅
      (smallEtaleModuleRestrictionAlong D.B D.g').mapDerivedCategory ⋙
        Stacks.Cohomology.DerivedPushforward.derivedPushforward
          (X := smallEtaleRingedTopos D.B D.T') (Y := smallEtaleRingedTopos D.B D.S')
          (smallEtaleRingedToposHom D.B D.f')

Tag 0DDH, a lemma

Tag 0DDH in the Stacks Project.

AlgebraicGeometry.bigSmallEtaleCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/Cohomology.lean, line 183. The attribute's comment: “big_small_abelian”.

The canonical comparison of big-site cohomology over T with small-site cohomology of the restricted complex, natural in the unbounded derived object. Applying degree-n homology gives the equality of groups in Stacks 0DDH.

public noncomputable def bigSmallEtaleCohomologyIso
    [HasSheafify (SmallEtale.topology B T.obj T.property) Ab.{u + 1}]
    [HasSheafify (BigEtaleOver.topology B S.obj S.property) Ab.{u + 1}]
    [((bigEtaleSections B T S f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh).HasRightDerivedFunctor
        (HomotopyCategory.quasiIso
          (Sheaf (BigEtaleOver.topology B S.obj S.property) Ab.{u + 1})
          (ComplexShape.up ℤ))]
    [((smallEtaleRestriction B T S f).mapHomotopyCategory
      (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).HasRightDerivedFunctor
        (HomotopyCategory.quasiIso
          (Sheaf (BigEtaleOver.topology B S.obj S.property) Ab.{u + 1})
          (ComplexShape.up ℤ))]
    [((Sheaf.Γ (SmallEtale.topology B T.obj T.property) Ab.{u + 1}).mapHomotopyCategory
      (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).HasRightDerivedFunctor
        (HomotopyCategory.quasiIso
          (Sheaf (SmallEtale.topology B T.obj T.property) Ab.{u + 1})
          (ComplexShape.up ℤ))] :
    (((bigEtaleSections B T S f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
        (HomotopyCategory.quasiIso
          (Sheaf (BigEtaleOver.topology B S.obj S.property) Ab.{u + 1})
          (ComplexShape.up ℤ))) ≅
    ((((smallEtaleRestriction B T S f).mapHomotopyCategory
      (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
        (HomotopyCategory.quasiIso
          (Sheaf (BigEtaleOver.topology B S.obj S.property) Ab.{u + 1})
          (ComplexShape.up ℤ))) ⋙
    (((Sheaf.Γ (SmallEtale.topology B T.obj T.property) Ab.{u + 1}).mapHomotopyCategory
      (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (SmallEtale.topology B T.obj T.property) Ab.{u + 1})
          (ComplexShape.up ℤ))))

AlgebraicGeometry.bigSmallEtaleModuleSectionsCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ModuleSectionsCohomology.lean, line 215. The attribute's comment: “part (6)”.

Stacks 0DDH, part (6). Let f : T ⟶ S be a morphism of a big étale site and let M be an unbounded complex of sheaves of 𝒪-modules on the big étale site over S. Cohomology over the object T ⟶ S agrees with cohomology on the small étale site of T of i_f^*M, naturally in M: H^n_étale(T, M) = H^n(T_étale, i_f^*M).

Both sides are computed, as in the source, by the right derived functors of sections on the derived categories of modules. The proof is the comparison on underlying abelian complexes, AlgebraicGeometry.bigSmallEtaleModuleCohomologyIso, transported by Stacks 0D6J on both sites (AlgebraicGeometry.derivedBigEtaleModuleSectionsIso and AlgebraicGeometry.derivedSmallEtaleModuleGlobalSectionsIso).

public def bigSmallEtaleModuleSectionsCohomologyIso :
    derivedBigEtaleModuleSections B T S f ≅
      (smallEtaleModuleRestriction B T S f).mapDerivedCategory ⋙
        derivedSmallEtaleModuleGlobalSections B T

AlgebraicGeometry.bigSmallEtaleModuleProjectionPullbackSectionsCohomologyIsoSelf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ModuleSectionsCohomology.lean, line 233. The attribute's comment: “part (2)”.

Stacks 0DDH, part (2). Let S be an object of a big étale site and let K be an unbounded complex of sheaves of 𝒪_{S_étale}-modules. Cohomology on the big étale site of S of the derived pullback Lπ_S^*K agrees with cohomology of K on the small étale site of S, naturally in K: H^n_étale(S, Lπ_S^*K) = H^n(S_étale, K).

Both sides are computed, as in the source, by the right derived functors of sections on the derived categories of modules. The proof is the comparison on underlying abelian complexes, AlgebraicGeometry.bigSmallEtaleModuleProjectionPullbackCohomologyIsoSelf, transported by Stacks 0D6J on both sites.

public def bigSmallEtaleModuleProjectionPullbackSectionsCohomologyIsoSelf :
    derivedSmallEtaleModuleProjectionPullback B S ⋙ derivedBigEtaleModuleSections B S S (𝟙 S) ≅
      derivedSmallEtaleModuleGlobalSections B S

AlgebraicGeometry.bigSmallEtaleModuleProjectionPullbackSectionsCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ModuleSectionsCohomology.lean, line 251. The attribute's comment: “part (4)”.

Stacks 0DDH, part (4). Let f : T ⟶ S be a morphism of a big étale site and let K be an unbounded complex of sheaves of 𝒪_{S_étale}-modules. Cohomology over the object T ⟶ S of the big étale site of S of the derived pullback Lπ_S^*K agrees with cohomology on the small étale site of T of the derived small étale pullback Lf_small^*K, naturally in K: H^n_étale(T, Lπ_S^*K) = H^n(T_étale, Lf_small^*K).

Both sides are computed, as in the source, by the right derived functors of sections on the derived categories of modules. The proof is the comparison on underlying abelian complexes, AlgebraicGeometry.bigSmallEtaleModuleProjectionPullbackCohomologyIso, transported by Stacks 0D6J on both sites.

public def bigSmallEtaleModuleProjectionPullbackSectionsCohomologyIso :
    derivedSmallEtaleModuleProjectionPullback B S ⋙ derivedBigEtaleModuleSections B T S f ≅
      derivedSmallEtaleModulePullback B T S f ⋙ derivedSmallEtaleModuleGlobalSections B T

AlgebraicGeometry.bigSmallEtaleProjectionPullbackCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ProjectionPullback.lean, line 349. The attribute's comment: “part (3)”.

Stacks 0DDH, part (3). Let f : T ⟶ S be a morphism of a big étale site and let K be an unbounded complex of abelian sheaves on the small étale site of S. Cohomology over the object T ⟶ S of the big étale site of S of the pullback π_S^{-1}K agrees with cohomology on the small étale site of T of f_{small}^{-1}K, naturally in K: H^n_étale(T, π_S^{-1}K) = H^n(T_étale, f_{small}^{-1}K).

Both π_S^{-1} and f_{small}^{-1} are exact, so no derived functor of them intervenes: the statement is between the two unbounded derived section functors precomposed with the functors the two pullbacks induce on derived categories.

The proof is part (5), AlgebraicGeometry.bigSmallEtaleCohomologyIso, followed by AlgebraicGeometry.smallEtaleRestrictionProjectionPullbackIso: the derived functor of the exact i_f^{-1} is the functor it induces on derived categories, and composing that with π_S^{-1}'s gives the one induced by f_{small}^{-1}.

public def bigSmallEtaleProjectionPullbackCohomologyIso :
    (projectionPullback.{u, u + 1} B S.obj S.property).mapDerivedCategory ⋙
      (((bigEtaleSections B T S f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (BigEtaleOver.topology B S.obj S.property) Ab.{u + 1})
            (ComplexShape.up ℤ))) ≅
    (smallEtaleAbelianInverseImage B T S f).mapDerivedCategory ⋙
      (((Sheaf.Γ (SmallEtale.topology B T.obj T.property) Ab.{u + 1}).mapHomotopyCategory
        (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (SmallEtale.topology B T.obj T.property) Ab.{u + 1})
            (ComplexShape.up ℤ)))

AlgebraicGeometry.bigSmallEtaleProjectionPullbackCohomologyIsoSelf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ProjectionPullback.lean, line 400. The attribute's comment: “part (1)”.

Stacks 0DDH, part (1). For an unbounded complex K of abelian sheaves on the small étale site of S, cohomology of the pullback π_S^{-1}K on the big étale site of S agrees with cohomology of K on the small étale site of S, naturally in K: H^n_étale(S, π_S^{-1}K) = H^n(S_étale, K).

This is part (3) at the identity morphism of S, where f_{small}^{-1} is the identity functor by AlgebraicGeometry.smallEtaleSheafPullbackIdIso (Stacks 021J).

public def bigSmallEtaleProjectionPullbackCohomologyIsoSelf :
    (projectionPullback.{u, u + 1} B S.obj S.property).mapDerivedCategory ⋙
      (((bigEtaleSections B S S (𝟙 S)).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (BigEtaleOver.topology B S.obj S.property) Ab.{u + 1})
            (ComplexShape.up ℤ))) ≅
    (((Sheaf.Γ (SmallEtale.topology B S.obj S.property) Ab.{u + 1}).mapHomotopyCategory
      (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
        (HomotopyCategory.quasiIso
          (Sheaf (SmallEtale.topology B S.obj S.property) Ab.{u + 1})
          (ComplexShape.up ℤ)))

AlgebraicGeometry.bigSmallEtaleDerivedSectionsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ProjectionPullback.lean, line 435. The attribute's comment: “part (5)”.

Stacks 0DDH, part (5). Let f : T ⟶ S be a morphism of a big étale site and let M be an unbounded complex of abelian sheaves on the big étale site over S. Cohomology over the object T ⟶ S of the big étale site of S agrees with cohomology on the small étale site of T of the restriction i_f^{-1}M, naturally in M: H^n_étale(T, M) = H^n(T_étale, i_f^{-1}M).

This is AlgebraicGeometry.bigSmallEtaleCohomologyIso with nothing assumed: the three derived functors in the statement exist, the derived functor of the exact i_f^{-1} by AlgebraicGeometry.hasRightDerivedFunctor_smallEtaleRestriction, and the derived sections functors RΓ(T → S, -) and RΓ(T_étale, -) by AlgebraicGeometry.hasRightDerivedFunctor_bigEtaleSections and AlgebraicGeometry.hasRightDerivedFunctor_smallEtaleGlobalSections, from the K-injective resolutions of the two Grothendieck abelian categories of sheaves.

public def bigSmallEtaleDerivedSectionsIso :
    (((bigEtaleSections B T S f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
        (HomotopyCategory.quasiIso
          (Sheaf (BigEtaleOver.topology B S.obj S.property) Ab.{u + 1})
          (ComplexShape.up ℤ))) ≅
    ((((smallEtaleRestriction B T S f).mapHomotopyCategory
      (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
        (HomotopyCategory.quasiIso
          (Sheaf (BigEtaleOver.topology B S.obj S.property) Ab.{u + 1})
          (ComplexShape.up ℤ))) ⋙
    (((Sheaf.Γ (SmallEtale.topology B T.obj T.property) Ab.{u + 1}).mapHomotopyCategory
      (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (SmallEtale.topology B T.obj T.property) Ab.{u + 1})
          (ComplexShape.up ℤ))))

Tag 0DDI, a lemma

Tag 0DDI in the Stacks Project.

AlgebraicGeometry.projectionPullback_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/CohomologicalDescent.lean, line 155. The attribute's comment: “exactness of inverse image”.

Extension from the small to the big étale site is exact.

theorem projectionPullback_exact :
    exactFunctor _ _ (projectionPullback.{u, v} B S hS)

AlgebraicGeometry.projectionInverseImage_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/CohomologicalDescent.lean, line 203. The attribute's comment: “exactness of inverse image, stated with no adjunction assumed”.

The inverse image with no adjunction assumed, AlgebraicGeometry.projectionInverseImage, is exact.

theorem projectionInverseImage_exact :
    exactFunctor _ _ (projectionInverseImage.{u, v} B S hS)

AlgebraicGeometry.projectionRestriction_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/CohomologicalDescent.lean, line 209. The attribute's comment: “exactness of direct image”.

Restriction from the big to the small étale site is exact.

theorem projectionRestriction_exact :
    exactFunctor _ _ (projectionRestriction.{u, v} B S hS)

AlgebraicGeometry.projectionDerivedUnit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/CohomologicalDescent.lean, line 257. The attribute's comment: “derived unit is an isomorphism”.

The derived unit of the projection adjunction is an isomorphism: cohomology on the small étale site agrees with cohomology on the big one.

theorem projectionDerivedUnit_isIso :
    IsIso (projectionDerivedUnit.{u, v} B S hS)

AlgebraicGeometry.projectionInverseImageDerivedUnit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/CohomologicalDescent.lean, line 319. The attribute's comment: “derived unit is an isomorphism, stated with no adjunction assumed”.

For every K in D(S_étale) the map K ⟶ Rπ_{S,*} π_S⁻¹ K is an isomorphism, with the inverse image projectionInverseImage taken with no adjunction assumed. Both functors are exact (projectionInverseImage_exact, projectionRestriction_exact), so their derived functors are the induced functors on derived categories.

theorem projectionInverseImageDerivedUnit_isIso :
    IsIso (projectionInverseImageDerivedUnit.{u, v} B S hS)

Tag 0DDJ, a lemma

Tag 0DDJ in the Stacks Project.

AlgebraicGeometry.isIso_bigSmallEtaleBaseChange_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ProperDirectImageCommutation.lean, line 70. The attribute's comment: “(1)”.

Stacks 0DDJ (1). Let f : T ⟶ S be a proper morphism of a big étale site. Then π_S⁻¹ ∘ f_{small,*} = f_{big,*} ∘ π_T⁻¹ as functors from sheaves of sets on T_étale to sheaves of sets on (Sch/S)_étale: the canonical base change map AlgebraicGeometry.bigSmallEtaleBaseChange is an isomorphism.

public theorem isIso_bigSmallEtaleBaseChange_of_isProper [IsProper (B.inclusion.map f)] :
    IsIso (bigSmallEtaleBaseChange B (Type (u + 1)) f (bigEtaleProjectionAdjunction B T)
      (bigEtaleProjectionAdjunction B S))

AlgebraicGeometry.isIso_bigSmallEtaleDerivedBaseChange_app_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ProperDirectImageCommutation.lean, line 105. The attribute's comment: “(2)”.

Stacks 0DDJ (2). Let f : T ⟶ S be a proper morphism of a big étale site. Then π_S⁻¹ Rf_{small,*} K = Rf_{big,*} π_T⁻¹ K for every K in D^+(T_étale) whose cohomology sheaves are torsion: the canonical base change map AlgebraicGeometry.bigSmallEtaleDerivedBaseChange is invertible at K. Here Rf_{small,*} and Rf_{big,*} are any right derived functors of the direct images of abelian sheaves along f.

public theorem isIso_bigSmallEtaleDerivedBaseChange_app_of_isProper
    [IsProper (B.inclusion.map f)]
    (K : DerivedCategory (Sheaf (SmallEtale.topology B T.obj T.property) AddCommGrpCat.{u + 1}))
    (n : ℤ) (hK : K.IsGE n)
    (hT : Stacks.Torsion.torsionCohomologyProperty.{u + 1}
      (SmallEtale.topology B T.obj T.property) K) :
    IsIso ((bigSmallEtaleDerivedBaseChange B f RfSmall RfBig αSmall αBig).app K)

AlgebraicGeometry.isIso_bigSmallEtaleDerivedBaseChange_app_toSheaf_of_isProper_zmod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ProperDirectImageCommutation.lean, line 121. The attribute's comment: “(3)”.

Stacks 0DDJ (3). Let f : T ⟶ S be a proper morphism of a big étale site and n ≥ 1. Then π_S⁻¹ Rf_{small,*} K = Rf_{big,*} π_T⁻¹ K for every K in D(T_étale, ℤ/nℤ), the unbounded derived category of sheaves of modules over the constant sheaf of rings ℤ/nℤ: the canonical base change map AlgebraicGeometry.bigSmallEtaleDerivedBaseChange is invertible at the underlying abelian complex of K.

public theorem isIso_bigSmallEtaleDerivedBaseChange_app_toSheaf_of_isProper_zmod
    [IsProper (B.inclusion.map f)] {n : ℕ} (hn : 0 < n)
    (E : DerivedCategory (SheafOfModules.{u + 1} (zmodRingSheaf.{u + 1}
      (SmallEtale.topology B T.obj T.property) n))) :
    IsIso ((bigSmallEtaleDerivedBaseChange B f RfSmall RfBig αSmall αBig).app
      ((SheafOfModules.toSheaf _).mapDerivedCategory.obj E))

Declarations registered for the tag:

AlgebraicGeometry.isIso_bigSmallEtaleDerivedBaseChange_of_isFinite, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ProperDirectImageCommutation.lean, line 77 (StacksFrontier): “(4)”.

Sources

LeanAlgebraicGeometry.injective_smallEtaleRestriction · AlgebraicGeometry.injective_smallEtaleRestrictionAlong · AlgebraicGeometry.isKInjective_smallEtaleRestriction · AlgebraicGeometry.isKInjective_smallEtaleRestrictionAlong · AlgebraicGeometry.smallEtaleRestrictionPushforwardIso · AlgebraicGeometry.bigEtaleRestrictionPushforwardIso · AlgebraicGeometry.smallEtaleRestrictionPushforwardModules_eq · AlgebraicGeometry.smallEtaleModulePullbackProjectionIso

Section59.100 Comparing fppf and étale topologies #

Section 59.100 of the Stacks Project, Tag 0DDK. 8 tags here are carried by 18 declarations of the repository (all in StacksFrontier) and 6 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DDL, a lemma

Tag 0DDL in the Stacks Project.

AlgebraicGeometry.smallEtaleInverseImage_isSheaf_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/FppfSheafConditionSmallEtale.lean, line 110. The attribute's comment: “the fppf sheaf condition”.

Stacks 0DDL, the fppf sheaf condition. For a sheaf of sets F on the small étale site of S, the presheaf underlying π_S⁻¹F — by the sections formula the rule X ↦ Γ(X_ét, f_X⁻¹F) — is a sheaf for the big fppf topology over S.

By Stacks 09XN, AlgebraicGeometry.bigEtaleToSmallEtale_inverseImage_isSheaf_fpqc, it is a sheaf for the much finer fpqc topology of the chosen slice, and every chosen fppf covering family is an fpqc covering family.

public theorem smallEtaleInverseImage_isSheaf_fppf
    (F : Sheaf (SmallEtale.topology (associatedBigEtaleSite B) S.1 S.property)
      (Type (u + 1))) :
    Presheaf.IsSheaf (B.topology.over S)
      ((bigEtaleToSmallEtaleMorphism (associatedBigEtaleSite B) S.1 S.property).inverseImage.obj
        F).obj

AlgebraicGeometry.isIso_fppfToBigEtale_unit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/FppfSheafConditionSmallEtale.lean, line 126. The attribute's comment: “the canonical fppf comparison”.

Stacks 0DDL, the canonical fppf comparison. At π_S⁻¹F the unit of ε_S⁻¹ ⊣ ε_{S,*} is an isomorphism. Since ε_{S,*} is restriction along the identity functor, this identifies the fppf sheaf ε_S⁻¹π_S⁻¹F with the rule X ↦ Γ(X_ét, f_X⁻¹F).

By AlgebraicGeometry.isIso_fppfToBigEtale_unit_app_iff the assertion is exactly the fppf sheaf condition AlgebraicGeometry.smallEtaleInverseImage_isSheaf_fppf.

public theorem isIso_fppfToBigEtale_unit_app
    (F : Sheaf (SmallEtale.topology (associatedBigEtaleSite B) S.1 S.property)
      (Type (u + 1))) :
    IsIso ((fppfToBigEtaleMorphism B S).adj.unit.app
      ((bigEtaleToSmallEtaleMorphism (associatedBigEtaleSite B) S.1
        S.property).inverseImage.obj F))

AlgebraicGeometry.smallEtalePullbackSections_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/FppfSheafOfSmallEtaleSections.lean, line 117. The attribute's comment: “the rule X ↦ Γ(X, f_small⁻¹F) is an fppf sheaf, a fortiori an étale sheaf”.

Stacks 0DDL, the sheaf condition. The rule (f : X ⟶ S) ↦ Γ(X, f_small⁻¹F) is a sheaf for the big fppf topology over S, and a fortiori for the big étale topology over S.

public theorem smallEtalePullbackSections_isSheaf :
    Presheaf.IsSheaf (B.topology.over S) (smallEtalePullbackSectionsPresheaf B S F) ∧
      Presheaf.IsSheaf (BigEtaleOver.topology (associatedBigEtaleSite B) S.1 S.property)
        (smallEtalePullbackSectionsPresheaf B S F)

AlgebraicGeometry.smallEtalePullbackSectionsSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/FppfSheafOfSmallEtaleSections.lean, line 140. The attribute's comment: “the rule is π_S⁻¹F on (Sch/S)_étale and ε_S⁻¹π_S⁻¹F on (Sch/S)_fppf”.

Stacks 0DDL, the identification. The sheaf X ↦ Γ(X, f_small⁻¹F) is π_S⁻¹F on the big étale site over S and ε_S⁻¹π_S⁻¹F on the big fppf site over S.

public def smallEtalePullbackSectionsSheafIso :
    (smallEtalePullbackSectionsEtaleSheaf B S F ≅
        (bigEtaleToSmallEtaleMorphism (associatedBigEtaleSite B) S.1 S.property).inverseImage.obj
          F) ×
      (smallEtalePullbackSectionsFppfSheaf B S F ≅
        (fppfToBigEtaleMorphism B S).inverseImage.obj
          ((bigEtaleToSmallEtaleMorphism (associatedBigEtaleSite B) S.1
            S.property).inverseImage.obj F))

Tag 0DDM, a lemma

Tag 0DDM in the Stacks Project.

AlgebraicGeometry.bigEtaleOverTopology_le_fppfOverTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/FppfToEtaleSquares.lean, line 124. The attribute's comment: “étale coverings are fppf on the slice”.

The big-site comparison from fppf to étale is induced by the identity functor on the common slice category.

public theorem bigEtaleOverTopology_le_fppfOverTopology
    (B : BigFppfSite.{u}) (X : B.Schemes) :
      BigEtaleOver.topology (associatedBigEtaleSite B) X.1 X.2 ≤
      B.topology.over X

AlgebraicGeometry.fppfToBigEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/FppfToEtaleSquares.lean, line 166. The attribute's comment: “change-of-topology morphism”.

The morphism of topoi from fppf sheaves to big étale sheaves on the slice over X: its pushforward and inverse image are those of the identity functor of the slice category, continuous because every étale covering is an fppf covering.

public def fppfToBigEtaleMorphism
    (B : BigFppfSite.{u}) (X : B.Schemes) :
    MorphismOfTopoi
      (Sheaf (B.topology.over X) (Type (u + 1)))
      (Sheaf (BigEtaleOver.topology (associatedBigEtaleSite B)
        X.1 X.2) (Type (u + 1)))

AlgebraicGeometry.fppfToBigEtale_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/FppfToEtaleSquares.lean, line 194. The attribute's comment: “direct image of change of topology”.

The direct image of the change-of-topology morphism is restriction of fppf sheaves along the identity functor on the common slice category.

public def fppfToBigEtale_pushforwardIso
    (B : BigFppfSite.{u}) (X : B.Schemes) :
    (fppfToBigEtaleMorphism B X).pushforward ≅
      (𝟭 (Over X)).sheafPushforwardContinuous (Type (u + 1))
        (BigEtaleOver.topology (associatedBigEtaleSite B) X.1 X.2)
        (B.topology.over X)

AlgebraicGeometry.fppfToSmallEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/FppfToEtaleSquares.lean, line 205. The attribute's comment: “factorization through the big étale topos”.

The comparison from the big fppf topos to the small étale topos.

public def fppfToSmallEtaleMorphism
    (B : BigFppfSite.{u}) (X : B.Schemes) :
    MorphismOfTopoi
      (Sheaf (B.topology.over X) (Type (u + 1)))
      (Sheaf (SmallEtale.topology (associatedBigEtaleSite B)
        X.1 X.2) (Type (u + 1)))

AlgebraicGeometry.bigFppfBigEtale_pushforwardCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/FppfToEtaleSquares.lean, line 237. The attribute's comment: “the big fppf–big étale square”.

The square of big fppf and big étale topoi commutes.

public def bigFppfBigEtale_pushforwardCommIso
    (B : BigFppfSite.{u}) {X Y : B.Schemes} (f : X ⟶ Y) :
    ((bigEtaleMorphism (associatedBigEtaleSite B) X Y f).comp
      (fppfToBigEtaleMorphism B X)).pushforward ≅
      ((fppfToBigEtaleMorphism B Y).comp
        (bigFppfMorphism B X Y f)).pushforward

AlgebraicGeometry.bigFppfSmallEtale_pushforwardCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/FppfToEtaleSquares.lean, line 291. The attribute's comment: “the big fppf–small étale square”.

The square of big fppf and small étale topoi commutes.

public def bigFppfSmallEtale_pushforwardCommIso
    (B : BigFppfSite.{u}) {X Y : B.Schemes} (f : X ⟶ Y) :
    ((smallEtaleMorphism B f).comp
        (fppfToSmallEtaleMorphism B X)).pushforward ≅
      ((fppfToSmallEtaleMorphism B Y).comp
        (bigFppfMorphism B X Y f)).pushforward

Tag 0DDN, a lemma

Tag 0DDN in the Stacks Project.

AlgebraicGeometry.isIso_bigFppfSmallEtaleBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ProperFppfDirectImage.lean, line 79.

Stacks 0DDN. Let f : X ⟶ Y be a proper morphism of the big fppf site. Then the base change map a_Y⁻¹ ∘ f_{small,*} ⟶ f_{big,fppf,*} ∘ a_X⁻¹ is an isomorphism.

public theorem isIso_bigFppfSmallEtaleBaseChange [IsProper (B.inclusion.map f)] :
    IsIso (bigFppfSmallEtaleBaseChange B f)

Tag 0DEU, a lemma

Tag 0DEU in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.isEquivalence_fppfSmallEtaleTripleFunctor, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/FppfDescentUnconditional.lean, line 60 (StacksFrontier).

Tag 0F0H, a lemma

Tag 0F0H in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.fppfEtaleWeakSerre_isWeakSerreClass, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/SituationTags.lean, line 31 (StacksFrontier): “𝒜'_X is a weak Serre subcategory”.
AlgebraicGeometry.fppfEtaleFinite_baseChange, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/SituationTags.lean, line 34 (StacksFrontier): “property (0EZ4) of Situation 0EZ3”.
AlgebraicGeometry.fppfEtaleWeakSerre_overMapPullback, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/SituationTags.lean, line 36 (StacksFrontier): “property (0EZ5) of Situation 0EZ3”.
AlgebraicGeometry.fppfEtaleWeakSerre_isSheaf_fppf, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/SituationTags.lean, line 39 (StacksFrontier): “property (0EZ6) of Situation 0EZ3”.
AlgebraicGeometry.fppfCovering_refinement_etale_finite, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/SituationTags.lean, line 42 (StacksFrontier): “property (0EZ8) of Situation 0EZ3”.

Tag 0DDS, a lemma

Tag 0DDS in the Stacks Project.

AlgebraicGeometry.isIso_fppfSmallEtaleDerivedDirectImageBaseChange_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/DirectImageBaseChange.lean, line 316. The attribute's comment: “(4)”.

For a finite morphism f : X ⟶ Y of the big fppf site and K in D⁺(X_étale),

a_Y⁻¹(Rf_{small,*}K) = Rf_{big,fppf,*}(a_X⁻¹K):

the base change map AlgebraicGeometry.fppfSmallEtaleDerivedDirectImageBaseChange is an isomorphism.

theorem isIso_fppfSmallEtaleDerivedDirectImageBaseChange_of_isFinite {X Y : B.Schemes}
    (f : X ⟶ Y) [IsFinite (B.inclusion.map f)]
    (K : DerivedCategory.Plus
      (Sheaf (SmallEtale.topology (associatedBigEtaleSite B) X.1 X.2) Ab.{u + 1})) :
    IsIso (fppfSmallEtaleDerivedDirectImageBaseChange f K)

AlgebraicGeometry.isIso_fppfSmallEtaleDerivedDirectImageBaseChange_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/DirectImageBaseChange.lean, line 335. The attribute's comment: “(5)”.

Stacks 0DDS (5). For a proper morphism f : X ⟶ Y of the big fppf site and K in D⁺(X_étale) with torsion cohomology sheaves,

a_Y⁻¹(Rf_{small,*}K) = Rf_{big,fppf,*}(a_X⁻¹K):

the base change map AlgebraicGeometry.fppfSmallEtaleDerivedDirectImageBaseChange is an isomorphism. Its first factor is invertible by Stacks 0DDJ (2), proper base change, and its second by Stacks 0EZF (2).

theorem isIso_fppfSmallEtaleDerivedDirectImageBaseChange_of_isProper {X Y : B.Schemes}
    (f : X ⟶ Y) [IsProper (B.inclusion.map f)]
    (K : DerivedCategory.Plus
      (Sheaf (SmallEtale.topology (associatedBigEtaleSite B) X.1 X.2) Ab.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (associatedBigEtaleSite B) X.1 X.2)
      ((DerivedCategory.Plus.homologyFunctor _ i).obj K)) :
    IsIso (fppfSmallEtaleDerivedDirectImageBaseChange f K)

AlgebraicGeometry.isIso_fppfSmallEtaleHigherDirectImageBaseChange_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/DirectImageBaseChange.lean, line 406. The attribute's comment: “(2)”.

Stacks 0DDS (2). For a finite morphism f : X ⟶ Y of the big fppf site, an abelian sheaf F on X_étale and every i,

a_Y⁻¹(R^if_{small,*}F) = R^if_{big,fppf,*}(a_X⁻¹F):

the base change map AlgebraicGeometry.fppfSmallEtaleHigherDirectImageBaseChange is an isomorphism. It is the cohomology of the derived base change map of part (4) at F placed in degree zero, read through isomorphisms.

theorem isIso_fppfSmallEtaleHigherDirectImageBaseChange_of_isFinite {X Y : B.Schemes}
    (f : X ⟶ Y) [IsFinite (B.inclusion.map f)]
    (F : Sheaf (SmallEtale.topology (associatedBigEtaleSite B) X.1 X.2) Ab.{u + 1}) (i : ℕ) :
    IsIso (fppfSmallEtaleHigherDirectImageBaseChange f F i)

AlgebraicGeometry.fppfSmallEtale_projectionPullback_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/DirectImageBaseChange.lean, line 426. The attribute's comment: “(1)”.

Stacks 0DDS (1). For an object X of the big fppf site and an abelian sheaf F on X_étale,

ε_{X,*}a_X⁻¹F = π_X⁻¹F and R^iε_{X,*}(a_X⁻¹F) = 0 for i > 0:

the unit π_X⁻¹F ⟶ ε_{X,*}ε_X⁻¹π_X⁻¹F = ε_{X,*}a_X⁻¹F of ε_X⁻¹ ⊣ ε_{X,*} is an isomorphism, and the higher right derived functors of ε_{X,*} vanish at a_X⁻¹F.

theorem fppfSmallEtale_projectionPullback_comparison (X : B.Schemes)
    (F : Sheaf (SmallEtale.topology (associatedBigEtaleSite B) X.1 X.2) Ab.{u + 1}) :
    IsIso ((fppfBigEtaleAbelianAdjunction B X).unit.app ((fppfEtaleProjectionPullback B X).obj F)) ∧
      ∀ i : ℕ, 0 < i → IsZero (((fppfBigEtaleAbelianPushforward B X).rightDerived i).obj
        ((fppfSmallEtaleAbelianPullback B X).obj F))

AlgebraicGeometry.isIso_fppfSmallEtaleDerivedUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/DirectImageBaseChange.lean, line 438. The attribute's comment: “(3)”.

Stacks 0DDS (3). For an object X of the big fppf site and K in D⁺(X_étale) the map π_X⁻¹K ⟶ Rε_{X,*}(a_X⁻¹K), AlgebraicGeometry.fppfSmallEtaleDerivedUnit, is an isomorphism. It is Stacks 0EZF (1) at π_X⁻¹K, which lies in D⁺_{𝒜'_X}.

theorem isIso_fppfSmallEtaleDerivedUnit (X : B.Schemes) :
    IsIso (fppfSmallEtaleDerivedUnit B X)

Tag 0DDT, a lemma

Tag 0DDT in the Stacks Project.

AlgebraicGeometry.isIso_fppfSmallEtaleAdjunctionDerivedUnit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/CohomologicalDescentUnconditional.lean, line 62.

Stacks 0DDT. Let X be a scheme, an object of a big fppf site B, and a_X : Sh((Sch/X)_fppf) ⟶ Sh(X_étale) the morphism of topoi to its small étale site. For K in D⁺(X_étale) the map K ⟶ Ra_{X,*}a_X^{-1}K, the component at K of the derived unit of a_X^{-1} ⊣ a_{X,*} (AlgebraicGeometry.fppfSmallEtaleAdjunctionDerivedUnit), is an isomorphism.

theorem isIso_fppfSmallEtaleAdjunctionDerivedUnit_app
    (K : DerivedCategory.Plus
      (Sheaf (SmallEtale.topology (associatedBigEtaleSite B) X.1 X.2) AddCommGrpCat.{u + 1})) :
    IsIso ((fppfSmallEtaleAdjunctionDerivedUnit B X).app K)

Tag 0DDU, a lemma

Tag 0DDU in the Stacks Project.

AlgebraicGeometry.isIso_fppfSmallEtaleCohomologyPullbacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/EtaleFppfCohomologyEquality.lean, line 85.

Stacks 0DDU. Let X be a scheme and a_X : Sh((Sch/X)_fppf) ⟶ Sh(X_étale). Then, for every q:

H^q(X_étale, F) = H^q_fppf(X, a_X^{-1}F) for an abelian sheaf F on X_étale, with H^q = R^qΓ (CategoryTheory.Functor.rightDerivedPlus, Stacks 015A): the canonical map AlgebraicGeometry.fppfSmallEtaleCohomologyPullback is an isomorphism;

H^q(X_étale, K) = H^q_fppf(X, a_X^{-1}K) for K in D⁺(X_étale): the canonical map AlgebraicGeometry.fppfSmallEtaleHypercohomologyPullback is an isomorphism;

and, the example, H^q_étale(X, A) = H^q_fppf(X, A) for an abelian group A and its constant sheaves: the canonical map AlgebraicGeometry.fppfSmallEtaleConstantCohomologyPullback is an isomorphism.

theorem isIso_fppfSmallEtaleCohomologyPullbacks :
    (∀ (q : ℤ)
      (F : Sheaf (SmallEtale.topology (associatedBigEtaleSite B) X.1 X.2) AddCommGrpCat.{u + 1}),
        IsIso (fppfSmallEtaleCohomologyPullback B X q F)) ∧
    (∀ (q : ℤ) (K : DerivedCategory.Plus
      (Sheaf (SmallEtale.topology (associatedBigEtaleSite B) X.1 X.2) AddCommGrpCat.{u + 1})),
        IsIso (fppfSmallEtaleHypercohomologyPullback B X q K)) ∧
    ∀ (q : ℤ) (A : AddCommGrpCat.{u + 1}),
      IsIso (fppfSmallEtaleConstantCohomologyPullback B X q A)

Sources

LeanAlgebraicGeometry.smallEtaleInverseImage_isSheaf_fppf · AlgebraicGeometry.isIso_fppfToBigEtale_unit_app · AlgebraicGeometry.smallEtalePullbackSections_isSheaf · AlgebraicGeometry.smallEtalePullbackSectionsSheafIso · AlgebraicGeometry.bigEtaleOverTopology_le_fppfOverTopology · AlgebraicGeometry.fppfToBigEtaleMorphism · AlgebraicGeometry.fppfToBigEtale_pushforwardIso · AlgebraicGeometry.fppfToSmallEtaleMorphism

Section59.101 Comparing fppf and étale topologies: modules #

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

Tag 0DEW, a lemma

Tag 0DEW in the Stacks Project.

AlgebraicGeometry.BigFppfOver.isSheaf_sectionsPresheafOfModules_baseOverTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BaseFullyFaithful.lean, line 105. The attribute's comment: “clause (1) only: 𝓕ᵃ satisfies the sheaf condition for fppf and a fortiori étale coverings; 𝓕 on S_étale is the associated module of a quasi-coherent module on the scheme S, the source's first reduction”.

Stacks 03DT on each of the five big sites of S. The pullback-sections presheaf of modules of a quasi-coherent module F on S is a sheaf for each of the five localized topologies, with no hypothesis.

Each of the five topologies is coarser than the fppf one, so this is the fppf statement AlgebraicGeometry.BigFppfOver.isSheaf_sectionsPresheafOfModules — whose hypothesis is discharged by AlgebraicGeometry.fpqcDescentOfQuasicoherentHoms — read through CategoryTheory.Presheaf.IsSheaf.of_le.

public theorem isSheaf_sectionsPresheafOfModules_baseOverTopology (τ : SiteKind)
    (F : S.Modules) [F.IsQuasicoherent] :
    Presheaf.IsSheaf (baseOverTopology B S hS τ)
      (sectionsPresheafOfModules B S hS F).presheaf

AlgebraicGeometry.BigFppfOver.baseAssociatedSheafIsoPiPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/QuasiCoherentPullback.lean, line 274. The attribute's comment: “clause (2) only: 𝓕ᵃ = π_S^*𝓕 on (Sch/S)_étale, with 𝓕 on S_étale the associated module of a quasi-coherent module on the scheme S as in the source's first reduction”.

Stacks 0DEW, clause (2). On (Sch/S)_étale the associated module 𝓕ᵃ of a quasi-coherent module is the inverse image π_S^*𝓕 of its associated module on S_étale, along the morphism of ringed sites π_S : ((Sch/S)_étale, 𝒪) ⟶ (S_étale, 𝒪).

public def baseAssociatedSheafIsoPiPullback :
    (smallEtaleToBaseModulePullback B S hS .etale).obj (smallEtaleAssociatedSheaf B S hS F) ≅
      baseAssociatedSheaf B S hS F .etale

AlgebraicGeometry.BigFppfOver.baseAssociatedSheafIsoAPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/QuasiCoherentPullback.lean, line 284. The attribute's comment: “clause (3) only: 𝓕ᵃ = a_S^*𝓕 on (Sch/S)_fppf, with 𝓕 on S_étale the associated module of a quasi-coherent module on the scheme S as in the source's first reduction”.

Stacks 0DEW, clause (3). On (Sch/S)_fppf the associated module 𝓕ᵃ of a quasi-coherent module is the inverse image a_S^*𝓕 of its associated module on S_étale, along the morphism of ringed sites a_S : ((Sch/S)_fppf, 𝒪) ⟶ (S_étale, 𝒪).

public def baseAssociatedSheafIsoAPullback :
    (SheafOfModules.pullback.{u} (aStructureMap B S hS)).obj
        (smallEtaleAssociatedSheaf B S hS F) ≅
      baseAssociatedSheaf B S hS F .fppf

AlgebraicGeometry.BigFppfOver.pushforward_baseAssociatedSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/QuasiCoherentPushforward.lean, line 253. The attribute's comment: “clause (6), first half, as documented above”.

Stacks 0DEW, clause (6), first half. The direct image along ε_S : ((Sch/S)_fppf, 𝒪) ⟶ ((Sch/S)_τ, 𝒪) of the associated module 𝓕ᵃ = a_S^*𝓕 is the associated module 𝓕ᵃ = π_S^*𝓕 of the big τ-site; at τ = étale this is ε_{S,*}a_S^*𝓕 = π_S^*𝓕.

Both sides are the presheaf (f : T → S) ↦ Γ(T, f⁺𝓕) of Stacks 03DS with its two sheaf conditions, and the direct image along the identity functor is restriction of sections along it.

public theorem pushforward_baseAssociatedSheaf (τ : SiteKind) :
    (epsilonPushforward B S hS τ).obj (baseAssociatedSheaf B S hS F .fppf) =
      baseAssociatedSheaf B S hS F τ

AlgebraicGeometry.BigFppfOver.pushforward_smallEtaleAssociatedSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/QuasiCoherentPushforward.lean, line 313. The attribute's comment: “clause (6), second half, as documented above”.

Stacks 0DEW, clause (6), second half. The direct image along a_S : ((Sch/S)_fppf, 𝒪) ⟶ (S_étale, 𝒪_S) of the associated module 𝓕ᵃ = a_S^*𝓕 is 𝓕 itself, read on the small étale site as its own associated module: a_{S,*}a_S^*𝓕 = 𝓕.

Both sides are the presheaf (f : T → S) ↦ Γ(T, f⁺𝓕) of Stacks 03DS, the right-hand side restricted along the inclusion of the small étale site, and the direct image is exactly that restriction.

public theorem pushforward_smallEtaleAssociatedSheaf :
    (aPushforward B S hS).obj (baseAssociatedSheaf B S hS F .fppf) =
      smallEtaleAssociatedSheaf B S hS F

AlgebraicGeometry.BigFppfOver.isZero_rightDerived_epsilonPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/QuasiCoherentPushforward.lean, line 419. The attribute's comment: “clause (7), first half, as documented above”.

Stacks 0DEW, clause (7), first half. The higher direct images along ε_S : ((Sch/S)_fppf, 𝒪) ⟶ ((Sch/S)_étale, 𝒪) of the associated module 𝓕ᵃ = a_S^*𝓕 vanish: R^p ε_{S,*}(a_S^*𝓕) = 0 for p > 0.

Every object of the big site is covered étale-locally by objects with affine total space, and there the fppf cohomology of 𝓕ᵃ vanishes in positive degrees by [Stacks, Tag 03P2]; so the module-valued criterion Stacks.Cohomology.ModuleDirectImageOnACover.isZero_rightDerived_pushforward_of_presieve applies.

public theorem isZero_rightDerived_epsilonPushforward (p : ℕ) (hp : 0 < p) :
    IsZero (((epsilonPushforward B S hS .etale).rightDerived p).obj
      (baseAssociatedSheaf B S hS F .fppf))

AlgebraicGeometry.BigFppfOver.isZero_rightDerived_aPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/QuasiCoherentPushforward.lean, line 475. The attribute's comment: “clause (7), second half, as documented above”.

Stacks 0DEW, clause (7), second half. The higher direct images along a_S : ((Sch/S)_fppf, 𝒪) ⟶ (S_étale, 𝒪_S) of the associated module 𝓕ᵃ = a_S^*𝓕 vanish: R^p a_{S,*}(a_S^*𝓕) = 0 for p > 0.

Every object of the small étale site is covered by its affine objects (Stacks 04HR), and over an object of the big site with affine total space the fppf cohomology of 𝓕ᵃ vanishes in positive degrees by [Stacks, Tag 03P2].

public theorem isZero_rightDerived_aPushforward (p : ℕ) (hp : 0 < p) :
    IsZero (((aPushforward B S hS).rightDerived p).obj
      (baseAssociatedSheaf B S hS F .fppf))

AlgebraicGeometry.smallEtaleBigEtaleQuasicoherentEquivalence', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/QuasiCoherentSmallEtaleBigSite.lean, line 273. The attribute's comment: “clause (4): 𝓕 ↦ 𝓕ᵃ is an equivalence between QCoh(S_étale, 𝒪) and QCoh((Sch/S)_étale, 𝒪)”.

Stacks 0DEW, clause (4). The rule 𝓕 ↦ 𝓕^a is an equivalence between the quasi-coherent 𝒪_S-modules on S_étale and the quasi-coherent modules on ((Sch/S)_étale, 𝒪).

The source's proof of this clause cites Descent, Proposition 03DX twice, and both citations are theorems of this library. The small-étale one is AlgebraicGeometry.SmallEtale.quasicoherentIsEssImageAssociatedModule; the big-site one at τ = étale is AlgebraicGeometry.BigFppfOver.baseQuasicoherentIsEssImageAssociatedModule (StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/BaseEssentialSurjectivity.lean).

public noncomputable def smallEtaleBigEtaleQuasicoherentEquivalence'
    (BE : BigEtaleSite.{u}) (BF : BigFppfSite.{u}) (S : Scheme.{u})
    (hE : BE.Contains S) (hF : BF.Contains S) :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (SmallEtale.structureSheaf BE S hE)).FullSubcategory ≌
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (FibredSite.baseRingStructureSheaf BF S hF .etale)).FullSubcategory

AlgebraicGeometry.smallEtaleBigFppfQuasicoherentEquivalence', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/QuasiCoherentSmallEtaleBigSite.lean, line 310. The attribute's comment: “clause (5): 𝓕 ↦ 𝓕ᵃ is an equivalence between QCoh(S_étale, 𝒪) and QCoh((Sch/S)_fppf, 𝒪)”.

Stacks 0DEW, clause (5). The rule 𝓕 ↦ 𝓕^a is an equivalence between the quasi-coherent 𝒪_S-modules on S_étale and the quasi-coherent modules on ((Sch/S)_fppf, 𝒪).

The source's proof of this clause cites Descent, Proposition 03DX twice, and both citations are theorems of this library. The small-étale one is AlgebraicGeometry.SmallEtale.quasicoherentIsEssImageAssociatedModule; the big-site one, at τ = fppf, is AlgebraicGeometry.BigFppfOver.quasicoherentIsEssImageAssociatedModule' (StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/EffectiveGlueAgreementTransport.lean :512). The equivalence used below is the τ-indexed one, whose essential surjectivity is AlgebraicGeometry.BigFppfOver.baseQuasicoherentIsEssImageAssociatedModule; that theorem is proved by reducing the τ case to this fppf one.

public noncomputable def smallEtaleBigFppfQuasicoherentEquivalence'
    (BE : BigEtaleSite.{u}) (BF : BigFppfSite.{u}) (S : Scheme.{u})
    (hE : BE.Contains S) (hF : BF.Contains S) :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (SmallEtale.structureSheaf BE S hE)).FullSubcategory ≌
      (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (FibredSite.baseRingStructureSheaf BF S hF .fppf)).FullSubcategory

Tag 0DEX, a lemma

Tag 0DEX in the Stacks Project.

AlgebraicGeometry.BigFppfOver.rightAcyclic_epsilonPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/QuasiCoherentPushforward.lean, line 510. The attribute's comment: “first half, as documented above”.

Stacks 0DEX, first half. The canonical map π_S^*𝓕 = ε_{S,*}(a_S^*𝓕) ⟶ Rε_{S,*}(a_S^*𝓕) is an isomorphism, that is, a_S^*𝓕 is right acyclic for ε_{S,*}.

This is the criterion of [Stacks, Tag 015C] applied to clauses (6) and (7) of [Stacks, Tag 0DEW]: clause (6) identifies the source of the map with π_S^*𝓕 (pushforward_baseAssociatedSheaf, an equality), and clause (7) supplies the vanishing of the higher direct images, which is what right acyclicity amounts to for a left exact functor.

public theorem rightAcyclic_epsilonPushforward :
    (SheafOfModules.pushforward (F := 𝟭 (BigFppfOver B S hS))
        (epsilonStructureMap B S hS .etale)).rightAcyclic
      (baseAssociatedSheaf B S hS F .fppf)

AlgebraicGeometry.BigFppfOver.rightAcyclic_aPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FppfEtaleComparison/QuasiCoherentPushforward.lean, line 531. The attribute's comment: “second half, as documented above”.

Stacks 0DEX, second half. The canonical map 𝓕 = a_{S,*}(a_S^*𝓕) ⟶ Ra_{S,*}(a_S^*𝓕) is an isomorphism, that is, a_S^*𝓕 is right acyclic for a_{S,*}.

Clause (6) of [Stacks, Tag 0DEW] identifies the source of the map with 𝓕 itself (pushforward_smallEtaleAssociatedSheaf, an equality), and clause (7) supplies the vanishing of the higher direct images.

public theorem rightAcyclic_aPushforward :
    (SheafOfModules.pushforward (F := smallEtaleToFppf B S hS)
        (aStructureMap B S hS)).rightAcyclic
      (baseAssociatedSheaf B S hS F .fppf)

Tag 0H0U, a lemma

Tag 0H0U in the Stacks Project.

AlgebraicGeometry.BigAffineFppf.isIso_derivedComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/AffineBaseChangeDerived.lean, line 787. The attribute's comment: “the canonical map to derived global sections is a quasi-isomorphism”.

Stacks 0H0U. For a complex M^• of A-modules the canonical map M^• ⟶ RΓ((Aff/S)_fppf, F^•) is a quasi-isomorphism, where F^• is the complex of sheaves of 𝒪-modules U ↦ M^• ⊗_A Γ(U, 𝒪_U) on the big affine fppf site of S = Spec A.

public theorem isIso_derivedComparison
    (RGamma : DerivedCategory (SheafOfModules.{u} (structureSheaf B A hS)) ⥤
      DerivedCategory (ModuleCat.{u} A))
    (unit : homotopyGlobalSections B A hS ⟶ DerivedCategory.Qh ⋙ RGamma)
    (hRGamma : RGamma.IsRightDerivedFunctor unit
      (HomotopyCategory.quasiIso (SheafOfModules.{u} (structureSheaf B A hS))
        (ComplexShape.up ℤ)))
    (M : CochainComplex (ModuleCat.{u} A) ℤ) :
    IsIso (derivedComparison B A hS RGamma unit M)

AlgebraicGeometry.BigAffineFppf.isIso_derivedComparison_totalRightDerived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/AffineBaseChangeDerivedExistence.lean, line 123. The attribute's comment: “the canonical map M^• ⟶ RΓ((Aff/S)_fppf, F^•) is a quasi-isomorphism, for the canonical total right derived functor of global sections -- no derived-functor parameter assumed”.

Stacks 0H0U for the canonical derived functor. The conclusion of AlgebraicGeometry.BigAffineFppf.isIso_derivedComparison with no derived-functor parameter left: for the total right derived functor of global sections supplied by CategoryTheory.Functor.totalRightDerived, the canonical map M^• ⟶ RΓ((Aff/S)_fppf, F^•) is a quasi-isomorphism.

public theorem isIso_derivedComparison_totalRightDerived
    (M : CochainComplex (ModuleCat.{u} A) ℤ) :
    IsIso (derivedComparison B A hS
      ((homotopyGlobalSections B A hS).totalRightDerived DerivedCategory.Qh
        (HomotopyCategory.quasiIso (SheafOfModules.{u} (structureSheaf B A hS))
          (ComplexShape.up ℤ)))
      ((homotopyGlobalSections B A hS).totalRightDerivedUnit DerivedCategory.Qh
        (HomotopyCategory.quasiIso (SheafOfModules.{u} (structureSheaf B A hS))
          (ComplexShape.up ℤ))) M)

AlgebraicGeometry.BigAffineFppf.baseChangePresheaf_map_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/AffineBaseChangeModule.lean, line 179. The attribute's comment: “the rule is a presheaf of modules”.

Stacks 0H0U. Restriction in the base-change presheaf is semilinear over restriction of functions: the rule U ↦ M ⊗_A Γ(U, 𝒪_U) is a presheaf of 𝒪-modules.

public theorem baseChangePresheaf_map_smul (M : ModuleCat.{u} A)
    ⦃X Y : (BigAffineFppf B (Spec A) hS)ᵒᵖ⦄ (φ : X ⟶ Y)
    (r : (Stacks.Sites.structurePresheaf (Spec A) (toOver B A hS)).obj X)
    (m : (baseChangePresheaf B A hS M).obj X) :
    (baseChangePresheaf B A hS M).map φ (r • m) =
        (Stacks.Sites.structurePresheaf (Spec A) (toOver B A hS)).map φ r •
        (baseChangePresheaf B A hS M).map φ m

AlgebraicGeometry.BigAffineFppf.baseChangePresheaf_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/AffineBaseChangeModule.lean, line 600. The attribute's comment: “the rule is a complex of modules, not only of presheaves of modules”.

Stacks 0H0U. Each term of the rule U ↦ M ⊗_A Γ(U, 𝒪_U) is a sheaf: a complex of A-modules gives a complex of modules, not merely a complex of presheaves of modules.

public theorem baseChangePresheaf_isSheaf (M : ModuleCat.{u} A) :
    Presheaf.IsSheaf (affineTopology B A hS) (baseChangePresheaf B A hS M)

AlgebraicGeometry.BigAffineFppf.baseChangeComplex, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Fppf/AffineBaseChangeModule.lean, line 636. The attribute's comment: “the displayed rule on a complex is a complex of modules”.

Stacks 0H0U. The complex F^• of sheaves of 𝒪-modules attached to a complex M^• of A-modules: in degree n it is the rule U ↦ M^n ⊗_A Γ(U, 𝒪_U), with the base changes of the differentials of M^•.

public abbrev baseChangeComplex : CochainComplex (ModuleCat.{u} A) ℤ ⥤
    CochainComplex (SheafOfModules.{u} (structureSheaf B A hS)) ℤ

Sources

LeanAlgebraicGeometry.BigFppfOver.isSheaf_sectionsPresheafOfModules_baseOverTopology · AlgebraicGeometry.BigFppfOver.baseAssociatedSheafIsoPiPullback · AlgebraicGeometry.BigFppfOver.baseAssociatedSheafIsoAPullback · AlgebraicGeometry.BigFppfOver.pushforward_baseAssociatedSheaf · AlgebraicGeometry.BigFppfOver.pushforward_smallEtaleAssociatedSheaf · AlgebraicGeometry.BigFppfOver.isZero_rightDerived_epsilonPushforward · AlgebraicGeometry.BigFppfOver.isZero_rightDerived_aPushforward · AlgebraicGeometry.smallEtaleBigEtaleQuasicoherentEquivalence'

Section59.102 Comparing ph and étale topologies #

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

Tag 0DDW, a lemma

Tag 0DDW in the Stacks Project.

AlgebraicGeometry.smallEtaleInverseImage_isZariskiSheaf_ph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/SmallEtalePullbackSheaf.lean, line 103. The attribute's comment: “the Zariski half of the ph sheaf condition, Stacks 0DBQ; descent along a proper surjective morphism is not proved”.

Stacks 0DDW, the Zariski half of the ph sheaf condition. For a sheaf of sets F on the small étale site of S, the presheaf underlying π_S⁻¹F — by the sections formula the rule X ↦ Γ(X_ét, f_X⁻¹F) of the source — satisfies descent for every family of the big ph category over S whose underlying family of schemes is a Zariski covering.

A Zariski covering family is an fpqc covering family, and π_S⁻¹F is a sheaf for the fpqc topology of the slice by Stacks 09XN, AlgebraicGeometry.bigEtaleToSmallEtale_inverseImage_isSheaf_fpqc.

public theorem smallEtaleInverseImage_isZariskiSheaf_ph :
    IsZariskiSheaf B S hS
      ((bigEtaleToSmallEtaleMorphism (phAssociatedBigEtaleSite B) S hS).inverseImage.obj
        F).obj

AlgebraicGeometry.smallEtaleInverseImage_isSheaf_ph_and_isIso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Ph/SmallEtalePullbackSheafUnconditional.lean, line 60.

Stacks 0DDW. For a sheaf of sets F on the small étale site of S, the rule (f : X ⟶ S) ↦ Γ(X_ét, f⁻¹F) — the presheaf underlying π_S⁻¹F on the big étale category over S, by the sections formula AlgebraicGeometry.etaleInverseImageSectionsIso and Stacks 09XN — is a sheaf for the ph topology of the big ph category over S, and the unit of ε_S⁻¹ ⊣ ε_{S,*} at π_S⁻¹F is an isomorphism, so that this ph sheaf is ε_S⁻¹π_S⁻¹F.

By Stacks 0DBQ the ph sheaf condition splits into its Zariski half and descent along proper surjections; the latter follows from the proper base change theorem in degree zero, Stacks 0A3U, Stacks.EtaleCohomology.isIso_smallEtaleSetBaseChange_of_isProper.

public theorem smallEtaleInverseImage_isSheaf_ph_and_isIso_unit :
    Presieve.IsSheaf (BigPHOver.topology B S hS)
        ((bigEtaleToSmallEtaleMorphism (phAssociatedBigEtaleSite B) S hS).inverseImage.obj
          F).obj ∧
      IsIso ((phToBigEtaleMorphism B (B.obj S hS)).adj.unit.app
        ((bigEtaleToSmallEtaleMorphism (phAssociatedBigEtaleSite B) S hS).inverseImage.obj F))

Declarations registered for the tag:

AlgebraicGeometry.etaleInverseImageSectionsIso, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Topologies/Ph/SmallEtalePullbackSheaf.lean, line 75 (StacksFrontier): “the rule is the inverse image π_S⁻¹F on the big étale site”.

Tag 0DDX, a lemma

Tag 0DDX in the Stacks Project.

AlgebraicGeometry.phToBigEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/PhToEtaleSquares.lean, line 208. The attribute's comment: “change-of-topology morphism”.

The comparison ε_X from the big ph topos to the big étale topos, induced by the identity functor on the common slice category.

public def phToBigEtaleMorphism (B : BigPHSite.{u}) (X : B.Schemes) :
    MorphismOfTopoi
      (Sheaf (B.topology.over X) (Type (u + 1)))
      (Sheaf (BigEtaleOver.topology (phAssociatedBigEtaleSite B) X.1 X.2)
        (Type (u + 1)))

AlgebraicGeometry.phToSmallEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/PhToEtaleSquares.lean, line 244. The attribute's comment: “factorization through the big étale topos”.

The comparison a_X = π_X ∘ ε_X from the big ph topos to the small étale topos.

public def phToSmallEtaleMorphism (B : BigPHSite.{u}) (X : B.Schemes) :
    MorphismOfTopoi
      (Sheaf (B.topology.over X) (Type (u + 1)))
      (Sheaf (SmallEtale.topology (phAssociatedBigEtaleSite B) X.1 X.2) (Type (u + 1)))

AlgebraicGeometry.bigPHBigEtale_pushforwardCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/PhToEtaleSquares.lean, line 273. The attribute's comment: “the big ph–big étale square”.

Stacks 0DDX, first diagram. The square formed by the big ph and big étale base-change morphisms over the change-of-topology comparisons ε_X and ε_Y commutes on direct images.

public def bigPHBigEtale_pushforwardCommIso (B : BigPHSite.{u}) {X Y : B.Schemes} (f : X ⟶ Y) :
    ((bigEtaleMorphism (phAssociatedBigEtaleSite B) X Y f).comp
      (phToBigEtaleMorphism B X)).pushforward ≅
      ((phToBigEtaleMorphism B Y).comp (bigPHMorphism B X Y f)).pushforward

AlgebraicGeometry.bigPHSmallEtale_pushforwardCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/PhToEtaleSquares.lean, line 320. The attribute's comment: “the big ph–small étale square”.

Stacks 0DDX, second diagram. The square formed by the big ph and small étale base-change morphisms over the comparisons a_X = π_X ∘ ε_X and a_Y = π_Y ∘ ε_Y commutes on direct images.

public def bigPHSmallEtale_pushforwardCommIso
    (B : BigPHSite.{u}) {X Y : B.Schemes} (f : X ⟶ Y) :
    ((phSmallEtaleMorphism B f).comp (phToSmallEtaleMorphism B X)).pushforward ≅
      ((phToSmallEtaleMorphism B Y).comp (bigPHMorphism B X Y f)).pushforward

Tag 0DDY, a lemma

Tag 0DDY in the Stacks Project.

AlgebraicGeometry.isIso_bigPHSmallEtaleDirectImageBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/PhProperDirectImage.lean, line 93.

Stacks 0DDY. Let B be a big ph site and f : X ⟶ Y a proper morphism of it. Then a_Y⁻¹ ∘ f_{small,*} = f_{big,ph,*} ∘ a_X⁻¹ as functors from sheaves of sets on X_étale to sheaves of sets on (Sch/Y)_ph: the base change map AlgebraicGeometry.bigPHSmallEtaleDirectImageBaseChange of the square of topoi of Stacks 0DDX is an isomorphism.

public theorem isIso_bigPHSmallEtaleDirectImageBaseChange [IsProper (B.inclusion.map f)] :
    IsIso (bigPHSmallEtaleDirectImageBaseChange B f)

Tag 0F0I, a lemma

Tag 0F0I in the Stacks Project.

AlgebraicGeometry.BigPHSite.exists_phEtaleCohomologyComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/PhComparisonSituationProperties.lean, line 74.

Consider the comparison of the ph topology of a big ph site B with the étale topology on the same category of schemes. Let 𝒫 be the class of proper morphisms, and for X in the site let 𝒜'_X ⊂ Ab((Sch/X)_étale) be the full subcategory of sheaves of the form π_X⁻¹F with F a torsion abelian sheaf on X_étale. Then 𝒜'_X is a weak Serre subcategory and properties (0EZ4)–(0EZ8) of the comparison situation of Stacks 0EZ3 hold: there is a comparison situation with the ph topology as finer topology, the étale topology as coarser topology, 𝒫 as distinguished class and the 𝒜'_X as weak Serre classes.

public theorem exists_phEtaleCohomologyComparison (B : BigPHSite.{u}) :
    ∃ S : Stacks.ComparingTopologies.CohomologyComparison (phAssociatedBigEtaleSite B).Scheme,
      S.fineCoverage = B.precoverage ∧
      S.coarseCoverage = (phAssociatedBigEtaleSite B).precoverage ∧
      S.morphismProperty = (fun _ _ f => IsProper ((phAssociatedBigEtaleSite B).inclusion.map f)) ∧
      ∀ X : (phAssociatedBigEtaleSite B).Scheme,
        HEq (S.weakSerre X)
          (smallEtaleTorsionPullbackClass (phAssociatedBigEtaleSite B) X
            ((phAssociatedBigEtaleSite B).topology.over X))

Tag 0DE4, a lemma

Tag 0DE4 in the Stacks Project.

AlgebraicGeometry.phEtaleTorsionComparison_smallEtaleInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/PhTorsionComparison.lean, line 123. The attribute's comment: “(1)”.

Stacks 0DE4 (1). For an object X of the big ph site and an abelian torsion sheaf F on X_étale, ε_{X,*}a_X⁻¹F = π_X⁻¹F — the unit π_X⁻¹F ⟶ ε_{X,*}ε_X⁻¹π_X⁻¹F of ε_X⁻¹ ⊣ ε_{X,*} is an isomorphism, a_X⁻¹ = ε_X⁻¹ ∘ π_X⁻¹ — and R^i ε_{X,*}(a_X⁻¹F) = 0 for i > 0.

public theorem phEtaleTorsionComparison_smallEtaleInclusion
    (X : (phAssociatedBigEtaleSite B).Scheme)
    (F : Sheaf (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property) Ab.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property) F) :
    IsIso ((abelianComparisonAdjunction B.precoverage
        (phAssociatedBigEtaleSite B).precoverage
        (BigPHSite.etalePrecoverage_le_precoverage B) X).unit.app
        (((SmallEtale.inclusion (phAssociatedBigEtaleSite B) X.obj X.property).sheafPullback
          Ab.{u + 1} (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
          ((phAssociatedBigEtaleSite B).topology.over X)).obj F)) ∧
      ∀ i : ℕ, 0 < i → IsZero (((abelianComparisonPushforward B.precoverage
          (phAssociatedBigEtaleSite B).precoverage
          (BigPHSite.etalePrecoverage_le_precoverage B) X).rightDerived i).obj
        ((abelianComparisonPullback B.precoverage
          (phAssociatedBigEtaleSite B).precoverage X).obj
          (((SmallEtale.inclusion (phAssociatedBigEtaleSite B) X.obj X.property).sheafPullback
            Ab.{u + 1} (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
            ((phAssociatedBigEtaleSite B).topology.over X)).obj F)))

AlgebraicGeometry.isIso_phEtaleTorsionHigherBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/PhTorsionComparison.lean, line 154. The attribute's comment: “(2)”.

Stacks 0DE4 (2). For a proper morphism f : X ⟶ Y of the big ph site and an abelian torsion sheaf F on X_étale, the base change map a_Y⁻¹(R^i f_{small,*}F) ⟶ R^i f_{big,ph,*}(a_X⁻¹F) is an isomorphism for every i. The map is AlgebraicGeometry.higherSmallEtaleFineBaseChange, the degree i cohomology of the derived base change map of part (4) at F placed in degree zero; f_{big,ph,*} is the direct image overPushforward of the ph topology along f.

public theorem isIso_phEtaleTorsionHigherBaseChange
    {X Y : (phAssociatedBigEtaleSite B).Scheme} (f : X ⟶ Y)
    (hf : IsProper ((phAssociatedBigEtaleSite B).inclusion.map f))
    (F : Sheaf (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property) Ab.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property) F)
    (i : ℕ) :
    IsIso (higherSmallEtaleFineBaseChange (phAssociatedBigEtaleSite B) B.precoverage
      (BigPHSite.etalePrecoverage_le_precoverage B)
      (fun X F => (smallEtaleInverseImage_isSheaf_ph B X.1 X.2 F).1)
      (properDirectImageComparison _) (BigPHSite.exists_properRefinement B) f F i)

AlgebraicGeometry.isIso_phEtaleTorsionDerivedComparisonUnit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/PhTorsionComparison.lean, line 173. The attribute's comment: “(3)”.

Stacks 0DE4 (3). For an object X of the big ph site and K in D⁺(X_étale) with torsion cohomology sheaves, the map π_X⁻¹K ⟶ Rε_{X,*}(a_X⁻¹K) is an isomorphism: it is the derived unit of ε_X⁻¹ ⊣ ε_{X,*} at π_X⁻¹K, and a_X⁻¹K = ε_X⁻¹π_X⁻¹K.

public theorem isIso_phEtaleTorsionDerivedComparisonUnit_app
    (X : (phAssociatedBigEtaleSite B).Scheme)
    (K : DerivedCategory.Plus
      (Sheaf (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property) Ab.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
      ((DerivedCategory.Plus.homologyFunctor _ i).obj K)) :
    IsIso ((derivedComparisonUnit (phEtaleTorsionComparison B) X).app
      (((SmallEtale.inclusion (phAssociatedBigEtaleSite B) X.obj X.property).sheafPullback
        Ab.{u + 1} (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
        ((phAssociatedBigEtaleSite B).topology.over X)).mapDerivedCategoryPlus.obj K))

AlgebraicGeometry.isIso_phEtaleTorsionDerivedBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/PhTorsionComparison.lean, line 194. The attribute's comment: “(4)”.

Stacks 0DE4 (4). For a proper morphism f : X ⟶ Y of the big ph site and K in D⁺(X_étale) with torsion cohomology sheaves, the base change map a_Y⁻¹(Rf_{small,*}K) ⟶ Rf_{big,ph,*}(a_X⁻¹K) is an isomorphism. The map is AlgebraicGeometry.derivedSmallEtaleFineBaseChange, the base change map of the square of topoi a_Y ∘ f_{big,ph} = f_{small} ∘ a_X.

public theorem isIso_phEtaleTorsionDerivedBaseChange
    {X Y : (phAssociatedBigEtaleSite B).Scheme} (f : X ⟶ Y)
    (hf : IsProper ((phAssociatedBigEtaleSite B).inclusion.map f))
    (K : DerivedCategory.Plus
      (Sheaf (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property) Ab.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
      ((DerivedCategory.Plus.homologyFunctor _ i).obj K)) :
    IsIso (derivedSmallEtaleFineBaseChange (phAssociatedBigEtaleSite B) B.precoverage
      (BigPHSite.etalePrecoverage_le_precoverage B)
      (fun X F => (smallEtaleInverseImage_isSheaf_ph B X.1 X.2 F).1)
      (properDirectImageComparison _) (BigPHSite.exists_properRefinement B) f K)

Tag 0DE5, a lemma

Tag 0DE5 in the Stacks Project.

AlgebraicGeometry.isIso_phEtaleTorsionDerivedSmallEtaleUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/PhTorsionDerivedUnit.lean, line 62.

For an object X of the big ph site and K in D⁺(X_étale) with torsion cohomology sheaves, the map K ⟶ Ra_{X,*}a_X⁻¹K is an isomorphism, where a_X = π_X ∘ ε_X : Sh((Sch/X)_ph) ⟶ Sh(X_étale); the map is AlgebraicGeometry.derivedSmallEtaleFineUnit, the unit of a_X⁻¹ ⊣ a_{X,*} on D⁺.

public theorem isIso_phEtaleTorsionDerivedSmallEtaleUnit (X : (phAssociatedBigEtaleSite B).Scheme)
    (K : DerivedCategory.Plus
      (Sheaf (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property) Ab.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
      ((DerivedCategory.Plus.homologyFunctor _ i).obj K)) :
    IsIso (derivedSmallEtaleFineUnit (phAssociatedBigEtaleSite B) B.precoverage
      (BigPHSite.etalePrecoverage_le_precoverage B)
      (fun X F => (smallEtaleInverseImage_isSheaf_ph B X.1 X.2 F).1)
      (properDirectImageComparison _) (BigPHSite.exists_properRefinement B) X K)

Tag 0DE6, a lemma

Tag 0DE6 in the Stacks Project.

AlgebraicGeometry.phEtaleTorsionCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/PhTorsionCohomology.lean, line 78. The attribute's comment: “(1)”.

Stacks 0DE6 (1). For an object X of the big ph site, a torsion abelian sheaf F on X_étale and every q, H^q(X_étale, F) = H^q_ph(X, a_X⁻¹F), where a_X⁻¹F = ε_X⁻¹π_X⁻¹F is the pullback to the ph site over X. The isomorphism is the canonical one, the pullback along a_X on cohomology (AlgebraicGeometry.cohomologyFineComparisonIso).

public def phEtaleTorsionCohomologyIso
    (F : Sheaf (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
      AddCommGrpCat.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property) F)
    (q : ℕ) :
    (((sheafSections (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
        AddCommGrpCat.{u + 1}).obj
        (op (SmallEtale.final (phAssociatedBigEtaleSite B) X.obj X.property))).rightDerived q).obj
        F ≅
      ((Stacks.globalSectionsOver (phEtaleTorsionComparison B).fineCoverage.toGrothendieck
          X).rightDerived q).obj
        ((abelianComparisonPullback (phEtaleTorsionComparison B).fineCoverage
            (phEtaleTorsionComparison B).coarseCoverage X).obj
          (((SmallEtale.inclusion (phAssociatedBigEtaleSite B) X.obj X.property).sheafPullback
            AddCommGrpCat.{u + 1}
            (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
            ((phAssociatedBigEtaleSite B).topology.over X)).obj F))

AlgebraicGeometry.phEtaleTorsionDerivedCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/PhTorsionCohomology.lean, line 107. The attribute's comment: “(2)”.

Stacks 0DE6 (2). For an object X of the big ph site, K in D⁺(X_étale) with torsion cohomology sheaves and every q, H^q(X_étale, K) = H^q_ph(X, a_X⁻¹K): the degree q cohomology of the derived global sections RΓ(X_étale, K) and RΓ_ph(X, a_X⁻¹K), with a_X⁻¹ = ε_X⁻¹ ∘ π_X⁻¹ on D⁺. The isomorphism is the canonical one, the degree q cohomology of the pullback along a_X, AlgebraicGeometry.derivedGlobalSectionsFineComparisonIso.

public def phEtaleTorsionDerivedCohomologyIso
    (K : DerivedCategory.Plus (Sheaf (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj
      X.property) AddCommGrpCat.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
      ((DerivedCategory.Plus.homologyFunctor _ i).obj K))
    (q : ℤ) :
    (DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{u + 1} q).obj
        (((sheafSections (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
          AddCommGrpCat.{u + 1}).obj
          (op (SmallEtale.final (phAssociatedBigEtaleSite B) X.obj
            X.property))).rightDerivedFunctorPlus.obj K) ≅
      (DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{u + 1} q).obj
        ((Stacks.globalSectionsOver (phEtaleTorsionComparison B).fineCoverage.toGrothendieck
            X).rightDerivedFunctorPlus.obj
          ((abelianComparisonPullback (phEtaleTorsionComparison B).fineCoverage
              (phEtaleTorsionComparison B).coarseCoverage X).mapDerivedCategoryPlus.obj
            (((SmallEtale.inclusion (phAssociatedBigEtaleSite B) X.obj X.property).sheafPullback
              AddCommGrpCat.{u + 1}
              (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
              ((phAssociatedBigEtaleSite B).topology.over X)).mapDerivedCategoryPlus.obj K)))

AlgebraicGeometry.phEtaleTorsionConstantCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/PhTorsionCohomology.lean, line 139. The attribute's comment: “the example: H^q_et(X, A) = H^q_ph(X, A) for a torsion abelian group A”.

Stacks 0DE6, the example. For an object X of the big ph site, a torsion abelian group A and every q, H^q_étale(X, A) = H^q_ph(X, A), the cohomology of the constant sheaves with value A on X_étale and on the ph site over X. The isomorphism is part (1) at the constant sheaf, which is torsion, followed by the identification a_X⁻¹A = A of constant sheaves (both are left adjoint to global sections); see AlgebraicGeometry.cohomologyConstantFineComparisonIso.

public def phEtaleTorsionConstantCohomologyIso (A : AddCommGrpCat.{u + 1}) (hA : IsAddTorsion A)
    (q : ℕ) :
    (((sheafSections (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
        AddCommGrpCat.{u + 1}).obj
        (op (SmallEtale.final (phAssociatedBigEtaleSite B) X.obj X.property))).rightDerived q).obj
        ((constantSheaf (SmallEtale.topology (phAssociatedBigEtaleSite B) X.obj X.property)
          AddCommGrpCat.{u + 1}).obj A) ≅
      ((Stacks.globalSectionsOver (phEtaleTorsionComparison B).fineCoverage.toGrothendieck
          X).rightDerived q).obj
        ((constantSheaf ((phEtaleTorsionComparison B).fineCoverage.toGrothendieck.over X)
          AddCommGrpCat.{u + 1}).obj A)

Sources

LeanAlgebraicGeometry.smallEtaleInverseImage_isZariskiSheaf_ph · AlgebraicGeometry.smallEtaleInverseImage_isSheaf_ph_and_isIso_unit · AlgebraicGeometry.etaleInverseImageSectionsIso · AlgebraicGeometry.phToBigEtaleMorphism · AlgebraicGeometry.phToSmallEtaleMorphism · AlgebraicGeometry.bigPHBigEtale_pushforwardCommIso · AlgebraicGeometry.bigPHSmallEtale_pushforwardCommIso · AlgebraicGeometry.isIso_bigPHSmallEtaleDirectImageBaseChange

Section59.103 Comparing h and étale topologies #

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

Tag 0EW8, a lemma

Tag 0EW8 in the Stacks Project.

AlgebraicGeometry.smallEtaleInverseImage_isZariskiSheaf_h, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopologyEtaleComparison.lean, line 107. The attribute's comment: “the Zariski half of the h sheaf condition, condition (1) of Stacks 0EU5; descent along a proper surjective morphism of finite presentation is not proved”.

Stacks 0EW8, the Zariski half of the h sheaf condition. For a sheaf of sets F on the small étale site of S, the presheaf underlying π_S⁻¹F — by the sections formula the rule X ↦ Γ(X_ét, f_X⁻¹F) of the source — satisfies descent for every family of the big h category over S whose underlying family of schemes is a Zariski covering.

A Zariski covering family is an fpqc covering family, and π_S⁻¹F is a sheaf for the fpqc topology of the slice by Stacks 09XN, AlgebraicGeometry.bigEtaleToSmallEtale_inverseImage_isSheaf_fpqc.

public theorem smallEtaleInverseImage_isZariskiSheaf_h :
    BigHOver.IsZariskiSheaf B S hS
      ((bigEtaleToSmallEtaleMorphism (hAssociatedBigEtaleSite B) S hS).inverseImage.obj
        F).obj

AlgebraicGeometry.smallEtaleInverseImage_isSheaf_h_and_isIso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/HTopologyEtaleComparisonProperBaseChange.lean, line 86.

Stacks 0EW8. For a sheaf of sets F on the small étale site of S, the rule (f : X ⟶ S) ↦ Γ(X_ét, f⁻¹F) — the presheaf underlying π_S⁻¹F on the big étale category over S, by the sections formula AlgebraicGeometry.etaleInverseImageSectionsIso and Stacks 09XN — is a sheaf for the h topology of the big h category over S, and the unit of ε_S⁻¹ ⊣ ε_{S,*} at π_S⁻¹F is an isomorphism, so that this h sheaf is ε_S⁻¹π_S⁻¹F.

The h sheaf condition is Stacks 0EU5: the Zariski half is AlgebraicGeometry.smallEtaleInverseImage_isZariskiSheaf_h and the proper half is AlgebraicGeometry.smallEtaleInverseImage_isProperFinitePresentationSheaf.

public theorem smallEtaleInverseImage_isSheaf_h_and_isIso_unit :
    Presieve.IsSheaf (BigHOver.topology B S hS)
        ((bigEtaleToSmallEtaleMorphism (hAssociatedBigEtaleSite B) S hS).inverseImage.obj
          F).obj ∧
      IsIso ((hToBigEtaleMorphism B (B.obj S hS)).adj.unit.app
        ((bigEtaleToSmallEtaleMorphism (hAssociatedBigEtaleSite B) S hS).inverseImage.obj F))

Tag 0EW9, a lemma

Tag 0EW9 in the Stacks Project.

AlgebraicGeometry.hToBigEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/HToEtaleSquares.lean, line 192. The attribute's comment: “change-of-topology morphism”.

The comparison ε_X from the big h topos to the big étale topos, induced by the identity functor on the common slice category.

public def hToBigEtaleMorphism (B : BigHSite.{u}) (X : B.Schemes) :
    MorphismOfTopoi
      (Sheaf (B.topology.over X) (Type (u + 1)))
      (Sheaf (BigEtaleOver.topology (hAssociatedBigEtaleSite B) X.1 X.2) (Type (u + 1)))

AlgebraicGeometry.hToSmallEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/HToEtaleSquares.lean, line 227. The attribute's comment: “factorization through the big étale topos”.

The comparison a_X = π_X ∘ ε_X from the big h topos to the small étale topos.

public def hToSmallEtaleMorphism (B : BigHSite.{u}) (X : B.Schemes) :
    MorphismOfTopoi
      (Sheaf (B.topology.over X) (Type (u + 1)))
      (Sheaf (SmallEtale.topology (hAssociatedBigEtaleSite B) X.1 X.2) (Type (u + 1)))

AlgebraicGeometry.bigHBigEtale_pushforwardCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/HToEtaleSquares.lean, line 256. The attribute's comment: “the big h–big étale square”.

Stacks 0EW9, first diagram. The square formed by the big h and big étale base-change morphisms over the change-of-topology comparisons ε_X and ε_Y commutes on direct images.

public def bigHBigEtale_pushforwardCommIso (B : BigHSite.{u}) {X Y : B.Schemes} (f : X ⟶ Y) :
    ((bigEtaleMorphism (hAssociatedBigEtaleSite B) X Y f).comp
      (hToBigEtaleMorphism B X)).pushforward ≅
      ((hToBigEtaleMorphism B Y).comp (bigHMorphismOfTopoi B f)).pushforward

AlgebraicGeometry.bigHSmallEtale_pushforwardCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/HToEtaleSquares.lean, line 294. The attribute's comment: “the big h–small étale square”.

Stacks 0EW9, second diagram. The square formed by the big h and small étale base-change morphisms over the comparisons a_X = π_X ∘ ε_X and a_Y = π_Y ∘ ε_Y commutes on direct images.

public def bigHSmallEtale_pushforwardCommIso (B : BigHSite.{u}) {X Y : B.Schemes} (f : X ⟶ Y) :
    ((hSmallEtaleMorphism B f).comp (hToSmallEtaleMorphism B X)).pushforward ≅
      ((hToSmallEtaleMorphism B Y).comp (bigHMorphismOfTopoi B f)).pushforward

Tag 0EWA, a lemma

Tag 0EWA in the Stacks Project.

AlgebraicGeometry.isIso_bigHSmallEtaleBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/ProperHDirectImage.lean, line 68.

Stacks 0EWA. Let f : X ⟶ Y be a proper morphism of the big h site. Then the base change map a_Y⁻¹ ∘ f_{small,*} ⟶ f_{big,h,*} ∘ a_X⁻¹ of the square of topoi of Stacks 0EW9 is an isomorphism.

public theorem isIso_bigHSmallEtaleBaseChange [IsProper (B.inclusion.map f)] :
    IsIso (bigHSmallEtaleBaseChange B f)

Tag 0F0J, a lemma

Tag 0F0J in the Stacks Project.

AlgebraicGeometry.BigHSite.exists_hEtaleCohomologyComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/HComparisonSituationProperties.lean, line 70.

Stacks 0F0J. Consider the comparison of the h topology of a big h site B with the étale topology on the same category of schemes. Let 𝒫 be the class of proper morphisms, and for X in the site let 𝒜'_X ⊂ Ab((Sch/X)_étale) be the full subcategory of sheaves of the form π_X⁻¹F with F a torsion abelian sheaf on X_étale. Then 𝒜'_X is a weak Serre subcategory and properties (0EZ4)–(0EZ8) of the comparison situation of Stacks 0EZ3 hold: there is a comparison situation with the h topology as finer topology, the étale topology as coarser topology, 𝒫 as distinguished class and the 𝒜'_X as weak Serre classes.

public theorem exists_hEtaleCohomologyComparison (B : BigHSite.{u}) :
    ∃ S : Stacks.ComparingTopologies.CohomologyComparison (hAssociatedBigEtaleSite B).Scheme,
      S.fineCoverage = B.precoverage ∧
      S.coarseCoverage = (hAssociatedBigEtaleSite B).precoverage ∧
      S.morphismProperty = (fun _ _ f => IsProper ((hAssociatedBigEtaleSite B).inclusion.map f)) ∧
      ∀ X : (hAssociatedBigEtaleSite B).Scheme,
        HEq (S.weakSerre X)
          (smallEtaleTorsionPullbackClass (hAssociatedBigEtaleSite B) X
            ((hAssociatedBigEtaleSite B).topology.over X))

Tag 0EWF, a lemma

Tag 0EWF in the Stacks Project.

AlgebraicGeometry.hTorsionComparison_smallEtaleInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/HTorsionInverseImageComparison.lean, line 87. The attribute's comment: “(1)”.

For an object X of the big h site and an abelian torsion sheaf F on X_étale, ε_{X,*}a_X⁻¹F = π_X⁻¹F — the unit π_X⁻¹F ⟶ ε_{X,*}ε_X⁻¹π_X⁻¹F of the change of topology is an isomorphism — and R^i ε_{X,*}(a_X⁻¹F) = 0 for i > 0.

public theorem hTorsionComparison_smallEtaleInclusion (X : (hAssociatedBigEtaleSite B).Scheme)
    (F : Sheaf (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property) Ab.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property) F) :
    IsIso ((abelianComparisonAdjunction B.precoverage
        (hAssociatedBigEtaleSite B).precoverage
        (BigHSite.etalePrecoverage_le_precoverage B) X).unit.app
        (((SmallEtale.inclusion (hAssociatedBigEtaleSite B) X.obj X.property).sheafPullback
          Ab.{u + 1} (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
          ((hAssociatedBigEtaleSite B).topology.over X)).obj F)) ∧
      ∀ i : ℕ, 0 < i → IsZero (((abelianComparisonPushforward B.precoverage
          (hAssociatedBigEtaleSite B).precoverage
          (BigHSite.etalePrecoverage_le_precoverage B) X).rightDerived i).obj
        ((abelianComparisonPullback B.precoverage
          (hAssociatedBigEtaleSite B).precoverage X).obj
          (((SmallEtale.inclusion (hAssociatedBigEtaleSite B) X.obj X.property).sheafPullback
            Ab.{u + 1} (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
            ((hAssociatedBigEtaleSite B).topology.over X)).obj F)))

AlgebraicGeometry.isIso_hTorsionHigherSmallEtaleBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/HTorsionInverseImageComparison.lean, line 124. The attribute's comment: “(2)”.

For a proper morphism f : X ⟶ Y of the big h site and an abelian torsion sheaf F on X_étale, the base change map a_Y⁻¹(R^i f_{small,*}F) ⟶ R^i f_{big,h,*}(a_X⁻¹F) is an isomorphism for every i. The map is AlgebraicGeometry.higherSmallEtaleFineBaseChange, the degree i cohomology of the derived base change map AlgebraicGeometry.derivedSmallEtaleFineBaseChange at F placed in degree zero.

public theorem isIso_hTorsionHigherSmallEtaleBaseChange
    {X Y : (hAssociatedBigEtaleSite B).Scheme} (f : X ⟶ Y)
    (hf : IsProper ((hAssociatedBigEtaleSite B).inclusion.map f))
    (F : Sheaf (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property) Ab.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property) F)
    (i : ℕ) :
    IsIso (higherSmallEtaleFineBaseChange (hAssociatedBigEtaleSite B) B.precoverage
      (BigHSite.etalePrecoverage_le_precoverage B)
      (fun X F => (smallEtaleInverseImage_isSheaf_h_and_isIso_unit B X.1 X.2 F).1)
      (BigHSite.properDirectImageComparison B)
      (BigHSite.exists_properRefinement B) f F i)

AlgebraicGeometry.isIso_hTorsionDerivedComparisonUnit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/HTorsionInverseImageComparison.lean, line 143. The attribute's comment: “(3)”.

For an object X of the big h site and K in D⁺(X_étale) with torsion cohomology sheaves, the map π_X⁻¹K ⟶ Rε_{X,*}(a_X⁻¹K), the derived unit of the change of topology at π_X⁻¹K, is an isomorphism.

public theorem isIso_hTorsionDerivedComparisonUnit_app (X : (hAssociatedBigEtaleSite B).Scheme)
    (K : DerivedCategory.Plus
      (Sheaf (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property) Ab.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
      ((DerivedCategory.Plus.homologyFunctor _ i).obj K)) :
    IsIso ((derivedComparisonUnit (hEtaleCohomologyComparison B) X).app
      (((SmallEtale.inclusion (hAssociatedBigEtaleSite B) X.obj X.property).sheafPullback
        Ab.{u + 1} (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
        ((hAssociatedBigEtaleSite B).topology.over X)).mapDerivedCategoryPlus.obj K))

AlgebraicGeometry.isIso_hTorsionDerivedSmallEtaleBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/HTorsionInverseImageComparison.lean, line 165. The attribute's comment: “(4)”.

For a proper morphism f : X ⟶ Y of the big h site and K in D⁺(X_étale) with torsion cohomology sheaves, the base change map a_Y⁻¹(Rf_{small,*}K) ⟶ Rf_{big,h,*}(a_X⁻¹K) of the square of topoi a_Y ∘ f_h = f_small ∘ a_X, AlgebraicGeometry.derivedSmallEtaleFineBaseChange, is an isomorphism.

public theorem isIso_hTorsionDerivedSmallEtaleBaseChange
    {X Y : (hAssociatedBigEtaleSite B).Scheme} (f : X ⟶ Y)
    (hf : IsProper ((hAssociatedBigEtaleSite B).inclusion.map f))
    (K : DerivedCategory.Plus
      (Sheaf (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property) Ab.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
      ((DerivedCategory.Plus.homologyFunctor _ i).obj K)) :
    IsIso (derivedSmallEtaleFineBaseChange (hAssociatedBigEtaleSite B) B.precoverage
      (BigHSite.etalePrecoverage_le_precoverage B)
      (fun X F => (smallEtaleInverseImage_isSheaf_h_and_isIso_unit B X.1 X.2 F).1)
      (BigHSite.properDirectImageComparison B)
      (BigHSite.exists_properRefinement B) f K)

Tag 0EWG, a lemma

Tag 0EWG in the Stacks Project.

AlgebraicGeometry.isIso_hDerivedSmallEtaleUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/HCohomologyComparison.lean, line 84.

Let X be a scheme, an object of a big h site B. For K in D⁺(X_étale) with torsion cohomology sheaves, the map K ⟶ Ra_{X,*}a_X⁻¹K is an isomorphism, with a_X : Sh((Sch/X)_h) ⟶ Sh(X_étale) the composite of the change of topology ε_X : Sh((Sch/X)_h) ⟶ Sh((Sch/X)_étale) and the projection π_X : Sh((Sch/X)_étale) ⟶ Sh(X_étale).

public theorem isIso_hDerivedSmallEtaleUnit (X : (hAssociatedBigEtaleSite B).Scheme)
    (K : DerivedCategory.Plus
      (Sheaf (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property) Ab.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
      ((DerivedCategory.Plus.homologyFunctor _ i).obj K)) :
    IsIso (hDerivedSmallEtaleUnit B X K)

Tag 0EWH, a lemma

Tag 0EWH in the Stacks Project.

AlgebraicGeometry.hCohomologyComparisonIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/HTorsionCohomologyComparison.lean, line 85. The attribute's comment: “(1)”.

Stacks 0EWH (1). Let X be a scheme, an object of a big h site B, and let F be a torsion abelian sheaf on X_étale. For every q,

H^q(X_étale, F) = H^q_h(X, a_X⁻¹F),

where a_X⁻¹F = ε_X⁻¹π_X⁻¹F is the h sheafification of the pullback of F to the big étale site over X. The isomorphism is the canonical one: the degree q cohomology, at F placed in degree zero, of AlgebraicGeometry.derivedGlobalSectionsFineComparisonIso, the pullback along a_X on derived global sections.

public def hCohomologyComparisonIso
    (F : Sheaf (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
      AddCommGrpCat.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property) F)
    (q : ℕ) :
    (((sheafSections (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
        AddCommGrpCat.{u + 1}).obj
        (op (SmallEtale.final (hAssociatedBigEtaleSite B) X.obj X.property))).rightDerived q).obj
        F ≅
      ((Stacks.globalSectionsOver B.precoverage.toGrothendieck X).rightDerived q).obj
        ((abelianComparisonPullback B.precoverage (hAssociatedBigEtaleSite B).precoverage X).obj
          (((SmallEtale.inclusion (hAssociatedBigEtaleSite B) X.obj X.property).sheafPullback
            AddCommGrpCat.{u + 1} (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
            ((hAssociatedBigEtaleSite B).topology.over X)).obj F))

AlgebraicGeometry.hCohomologyComparisonPlusIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/HTorsionCohomologyComparison.lean, line 115. The attribute's comment: “(2)”.

Stacks 0EWH (2). Let X be a scheme, an object of a big h site B, and let K be an object of D⁺(X_étale) whose cohomology sheaves are torsion. For every q,

H^q(X_étale, K) = H^q_h(X, a_X⁻¹K),

the cohomology of the derived global sections RΓ(X_étale, K) and RΓ_h(X, a_X⁻¹K), where a_X⁻¹ = ε_X⁻¹ ∘ π_X⁻¹ on D⁺. The isomorphism is the canonical one: the degree q cohomology of AlgebraicGeometry.derivedGlobalSectionsFineComparisonIso, the pullback along a_X on derived global sections.

public def hCohomologyComparisonPlusIso
    (K : DerivedCategory.Plus (Sheaf (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj
      X.property) AddCommGrpCat.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty.{u + 1}
      (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
      ((DerivedCategory.Plus.homologyFunctor _ i).obj K))
    (q : ℤ) :
    (DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{u + 1} q).obj
        (((sheafSections (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
          AddCommGrpCat.{u + 1}).obj
          (op (SmallEtale.final (hAssociatedBigEtaleSite B) X.obj
            X.property))).rightDerivedFunctorPlus.obj K) ≅
      (DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{u + 1} q).obj
        ((Stacks.globalSectionsOver B.precoverage.toGrothendieck X).rightDerivedFunctorPlus.obj
          ((abelianComparisonPullback B.precoverage (hAssociatedBigEtaleSite B).precoverage
              X).mapDerivedCategoryPlus.obj
            (((SmallEtale.inclusion (hAssociatedBigEtaleSite B) X.obj X.property).sheafPullback
              AddCommGrpCat.{u + 1}
              (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
              ((hAssociatedBigEtaleSite B).topology.over X)).mapDerivedCategoryPlus.obj K)))

AlgebraicGeometry.hCohomologyConstantComparisonIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ComparingBigSmall/HTorsionCohomologyComparison.lean, line 150. The attribute's comment: “example”.

Stacks 0EWH, the example. Let X be a scheme, an object of a big h site B, and let A be a torsion abelian group. For every q,

H^q_étale(X, A) = H^q_h(X, A),

the cohomology of the constant sheaves with value A on the small étale site of X and on the h site over X. The isomorphism is the canonical one: part (1) at the constant sheaf, followed by the identification a_X⁻¹A = A of constant sheaves (both are left adjoint to global sections).

public def hCohomologyConstantComparisonIso (A : AddCommGrpCat.{u + 1}) (hA : IsAddTorsion A)
    (q : ℕ) :
    (((sheafSections (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
        AddCommGrpCat.{u + 1}).obj
        (op (SmallEtale.final (hAssociatedBigEtaleSite B) X.obj X.property))).rightDerived q).obj
        ((constantSheaf (SmallEtale.topology (hAssociatedBigEtaleSite B) X.obj X.property)
          AddCommGrpCat.{u + 1}).obj A) ≅
      ((Stacks.globalSectionsOver B.precoverage.toGrothendieck X).rightDerived q).obj
        ((constantSheaf (B.precoverage.toGrothendieck.over X) AddCommGrpCat.{u + 1}).obj A)

Sources

LeanAlgebraicGeometry.smallEtaleInverseImage_isZariskiSheaf_h · AlgebraicGeometry.smallEtaleInverseImage_isSheaf_h_and_isIso_unit · AlgebraicGeometry.hToBigEtaleMorphism · AlgebraicGeometry.hToSmallEtaleMorphism · AlgebraicGeometry.bigHBigEtale_pushforwardCommIso · AlgebraicGeometry.bigHSmallEtale_pushforwardCommIso · AlgebraicGeometry.isIso_bigHSmallEtaleBaseChange · AlgebraicGeometry.BigHSite.exists_hEtaleCohomologyComparison

Section59.104 Descending étale sheaves #

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

Tag 0GEY, a lemma

Tag 0GEY in the Stacks Project.

AlgebraicGeometry.smallEtaleSheafDescentFunctor_isEquivalence_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SheafDescent.lean, line 434.

Stacks 0GEY. The canonical small étale sheaf descent functor for a morphism of schemes admitting a section is an equivalence.

public theorem smallEtaleSheafDescentFunctor_isEquivalence_of_section
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    (s : Y ⟶ X) (hs : s ≫ f = 𝟙 Y) :
    (smallEtaleSheafDescentFunctor B f).IsEquivalence

Tag 0GEZ, a lemma

Tag 0GEZ in the Stacks Project.

AlgebraicGeometry.smallEtaleSheafDescentFunctor_isEquivalence_of_surjective_integral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SheafDescentIntegralSurjective.lean, line 88. The attribute's comment: “conditional. Carried as the hypothesis devissage: the integral branch of the base-change criterion [Stacks, Tag 0GF1], namely that descent along a morphism is effective once it is effective after base change along a surjective integral morphism g and after base change along pullback.fst g g ≫ g. Proved here: an integral surjection f satisfies every hypothesis of that criterion for the covering g = f, because the two base changes of f that occur there are split -- by the diagonal and by the graph of the first projection -- so that descent is effective along them. NOT proved: that the source's equalizer construction is a quasi-inverse. The construction itself is AlgebraicGeometry.smallEtaleDescentSheaf, with its comparison AlgebraicGeometry.smallEtaleDescentComparison, and the stalkwise criterion [Stacks, Tag 03PU] is available as AlgebraicGeometry.isIso_of_bijective_etaleStalkMap; what is missing is the compatibility of the construction with base change [Stacks, Tag 0EYP], which the library carries only conditionally on a presentation of an integral morphism by finite ones.”.

An integral surjection is an effective descent morphism for small étale sheaves.

public theorem smallEtaleSheafDescentFunctor_isEquivalence_of_surjective_integral
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    [Surjective (B.inclusion.map f)] [IsIntegralHom (B.inclusion.map f)]
    (devissage : ∀ {X' Y' Z' : B.Scheme} (f' : X' ⟶ Y') (g' : Z' ⟶ Y'),
      Surjective (B.inclusion.map g') → IsIntegralHom (B.inclusion.map g') →
      (smallEtaleSheafDescentFunctor B (pullback.snd f' g')).IsEquivalence →
      (smallEtaleSheafDescentFunctor B
        (pullback.snd f' (pullback.fst g' g' ≫ g'))).IsEquivalence →
      (smallEtaleSheafDescentFunctor B f').IsEquivalence) :
    (smallEtaleSheafDescentFunctor B f).IsEquivalence

AlgebraicGeometry.smallEtaleSheafDescentFunctor_isEquivalence_of_surjective_integral_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SheafDescentIntegralSurjectiveGeneral.lean, line 50.

Let f : X ⟶ Y be a surjective integral morphism of a big étale site. The functor from sheaves of sets on the small étale site of Y to descent data for {X ⟶ Y} is an equivalence of categories.

public theorem smallEtaleSheafDescentFunctor_isEquivalence_of_surjective_integral_unconditional
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    [Surjective (B.inclusion.map f)] [IsIntegralHom (B.inclusion.map f)] :
    (smallEtaleSheafDescentFunctorGeneral B f).IsEquivalence

Tag 0GF0, a lemma

Tag 0GF0 in the Stacks Project.

AlgebraicGeometry.smallEtaleSheafDescentFunctor_isEquivalence_of_surjective_proper_of_section, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SheafDescentProperSurjective.lean, line 72. The attribute's comment: “the case of a proper surjection admitting a section, proved unconditionally. This case is degenerate: the conclusion for a split morphism is already [Stacks, Tag 0GEY], so neither surjectivity nor properness enters the proof. No other case of the source statement is proved unconditionally.”.

A proper surjection admitting a section is an effective descent morphism for small étale sheaves.

public theorem smallEtaleSheafDescentFunctor_isEquivalence_of_surjective_proper_of_section
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    [Surjective (B.inclusion.map f)] [IsProper (B.inclusion.map f)]
    (s : Y ⟶ X) (hs : s ≫ f = 𝟙 Y) :
    (smallEtaleSheafDescentFunctor B f).IsEquivalence

AlgebraicGeometry.smallEtaleSheafDescentFunctor_isEquivalence_of_surjective_proper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SheafDescentProperSurjective.lean, line 89. The attribute's comment: “conditional. Carried as the hypothesis devissage: the proper branch of the base-change criterion [Stacks, Tag 0GF1], namely that descent along a morphism is effective once it is effective after base change along a surjective proper morphism g and after base change along pullback.fst g g ≫ g. Proved here: a proper surjection f satisfies every hypothesis of that criterion for the covering g = f, because the two base changes of f that occur there are split -- by the diagonal and by the graph of the first projection -- so that descent is effective along them. NOT proved: the source's own argument for this lemma, that is the proof of [Stacks, Tag 0GEZ] rerun with the proper base-change theorem [Stacks, Tag 0A3U] in place of [Stacks, Tag 0EYP].”.

A proper surjection is an effective descent morphism for small étale sheaves.

public theorem smallEtaleSheafDescentFunctor_isEquivalence_of_surjective_proper
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    [Surjective (B.inclusion.map f)] [IsProper (B.inclusion.map f)]
    (devissage : ∀ {X' Y' Z' : B.Scheme} (f' : X' ⟶ Y') (g' : Z' ⟶ Y'),
      Surjective (B.inclusion.map g') → IsProper (B.inclusion.map g') →
      (smallEtaleSheafDescentFunctor B (pullback.snd f' g')).IsEquivalence →
      (smallEtaleSheafDescentFunctor B
        (pullback.snd f' (pullback.fst g' g' ≫ g'))).IsEquivalence →
      (smallEtaleSheafDescentFunctor B f').IsEquivalence) :
    (smallEtaleSheafDescentFunctor B f).IsEquivalence

AlgebraicGeometry.smallEtaleSheafDescentFunctor_isEquivalence_of_isProper_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SheafDescentProperSurjectiveUnconditional.lean, line 113. References: SGA 4 VIII (9.4).

Effective descent of small étale sheaves along a proper surjection. For a surjective proper morphism f : X ⟶ Y of a big étale site, the functor sending a sheaf of sets on the small étale site of Y to its canonical descent datum for {X ⟶ Y} is an equivalence of categories.

public theorem smallEtaleSheafDescentFunctor_isEquivalence_of_isProper_of_surjective
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    [Surjective (B.inclusion.map f)] [IsProper (B.inclusion.map f)] :
    (smallEtaleSheafDescentFunctor B f).IsEquivalence

Tag 0GF1, a lemma

Tag 0GF1 in the Stacks Project.

AlgebraicGeometry.smallEtaleSheafDescentFunctor_isEquivalence_of_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SheafDescentBaseChange.lean, line 110. The attribute's comment: “only the case of a g admitting a section, and with the two hypotheses of the source -- effectivity over Z and over Z ×_Y Z -- replaced by effectivity of descent along the base change X ×_Y Z read along its structure morphism to Y rather than along its projection to Z. The surjective integral and the surjective proper cases, where the content of the source lemma lies (these are the cases in which 0GEZ resp. 0GF0 supplies effective descent along g), are NOT proved here; neither is the passage from effectivity over Z and over Z ×_Y Z to effectivity over Y of the base change.”.

Descent of small étale sheaves along f : X ⟶ Y is effective as soon as it is effective along the structure morphism X ×_Y Z ⟶ Y of the base change of f along a morphism g : Z ⟶ Y admitting a section.

public theorem smallEtaleSheafDescentFunctor_isEquivalence_of_baseChange
    (B : BigEtaleSite.{u}) {X Y Z : B.Scheme} (f : X ⟶ Y) (g : Z ⟶ Y) (s : Y ⟶ Z)
    (hs : s ≫ g = 𝟙 Y)
    (hXZ : (smallEtaleSheafDescentFunctor B (pullback.fst f g ≫ f)).IsEquivalence) :
    (smallEtaleSheafDescentFunctor B f).IsEquivalence

AlgebraicGeometry.smallEtaleSheafDescentFunctor_isEquivalence_of_baseChange_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SheafDescentBaseChange.lean, line 123. The attribute's comment: “the case Z = Y, g = 𝟙 Y of the source statement, with the hypothesis in the shape the source gives it, namely effectivity along the projection X ×_Y Z ⟶ Z. The hypothesis over Z ×_Y Z is not needed in this case. No other case of the source statement is proved.”.

Descent of small étale sheaves along f : X ⟶ Y is effective as soon as it is effective along the projection X ×_Y Y ⟶ Y.

public theorem smallEtaleSheafDescentFunctor_isEquivalence_of_baseChange_id
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
    (hZ : (smallEtaleSheafDescentFunctor B (pullback.snd f (𝟙 Y))).IsEquivalence) :
    (smallEtaleSheafDescentFunctor B f).IsEquivalence

AlgebraicGeometry.smallEtaleSheafDescentFunctor_isEquivalence_of_baseChange_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SheafDescentOfCoverBaseChange.lean, line 120.

Descent of small étale sheaves, tested after a surjective integral or proper base change. Let f : X ⟶ Y and g : Z ⟶ Y be morphisms of a big étale site, with g surjective and either integral or proper. If the functors from sheaves on the small étale sites of Z and of Z ×_Y Z to descent data for {X ×_Y Z ⟶ Z} and for {X ×_Y (Z ×_Y Z) ⟶ Z ×_Y Z} are equivalences of categories, then so is the functor from sheaves on the small étale site of Y to descent data for {X ⟶ Y}.

public theorem smallEtaleSheafDescentFunctor_isEquivalence_of_baseChange_of_surjective
    (B : BigEtaleSite.{u}) {X Y Z : B.Scheme} (f : X ⟶ Y) (g : Z ⟶ Y)
    [Surjective (B.inclusion.map g)]
    (hg : IsIntegralHom (B.inclusion.map g) ∨ IsProper (B.inclusion.map g))
    (hZ : (smallEtaleSheafDescentFunctor B (pullback.snd f g)).IsEquivalence)
    (hZZ : (smallEtaleSheafDescentFunctor B
      (pullback.snd f (pullback.fst g g ≫ g))).IsEquivalence) :
    (smallEtaleSheafDescentFunctor B f).IsEquivalence

Tag 0GF2, a lemma

Tag 0GF2 in the Stacks Project.

AlgebraicGeometry.smallEtaleSheafDescentFunctor_isEquivalence_of_fppf_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SheafDescentFppfCoveringUnconditional.lean, line 406.

[Stacks, Tag 0GF2]. Let f : X ⟶ Y be a morphism of a big étale site which is surjective, flat and locally of finite presentation. Then the canonical functor from sheaves on the small étale site of Y to descent data for {X ⟶ Y} is an equivalence of categories.

This is [Stacks, Tag 0GF3] for the one-member fppf covering {f}, smallEtaleSheafFamilyDescentFunctor_isEquivalence_of_fppfCovering_unconditional, whose proof is the source's proof of this lemma: the problem is local on Y, which reduces it to a quasi-compact quasi-separated base; there [Stacks, Tag 0CP0] supplies a finite surjective Z ⟶ Y with an open covering of Z factoring through X, the dévissage of [Stacks, Tag 0GF1] replaces Y by Z and Z ×_Y Z, and over those f has sections Zariski locally, which is [Stacks, Tag 0GEY] after localizing once more.

public theorem smallEtaleSheafDescentFunctor_isEquivalence_of_fppf_unconditional
    (B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y) [Surjective (B.inclusion.map f)]
    [Flat (B.inclusion.map f)] [LocallyOfFinitePresentation (B.inclusion.map f)] :
    (smallEtaleSheafDescentFunctorGeneral B f).IsEquivalence

Tag 0GF3, a lemma

Tag 0GF3 in the Stacks Project.

AlgebraicGeometry.smallEtaleSheafFamilyDescentFunctor_isEquivalence_of_fppfCovering_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SheafDescentFppfCoveringUnconditional.lean, line 368.

[Stacks, Tag 0GF3]. Let {f i : X i ⟶ Y} be a family of morphisms of a big étale site whose underlying family of morphisms of schemes is an fppf covering. Then the canonical functor from sheaves on the small étale site of Y to descent data for small étale sheaves with respect to the covering is an equivalence of categories.

The base is covered by affine opens V k; each V k ×_Y V l and each V k ×_Y V l ×_Y V m is an open subscheme of the affine V k, hence quasi-separated, so the quasi-separated case smallEtaleSheafFamilyDescentFunctor_isEquivalence_of_fppfCovering_of_quasiSeparated applies to the base change of the covering to each of them, and descent is local on the base (AlgebraicGeometry.isEquivalence_toDescentData_smallEtaleSheafPullbackSystem_of_openCover). The quasi-separated case is reduced in the same way to the quasi-compact quasi-separated case, which is the source's argument for [Stacks, Tag 0GF2] run for a family: [Stacks, Tag 0CP0], the integral branch of [Stacks, Tag 0GF1], and sections Zariski locally. The source instead applies [Stacks, Tag 0GF2] to the single morphism ∐ X i ⟶ Y; the family is treated directly here.

public theorem smallEtaleSheafFamilyDescentFunctor_isEquivalence_of_fppfCovering_unconditional
    (B : BigEtaleSite.{u}) {I : Type t} {X : I → B.Scheme} {Y : B.Scheme} (f : ∀ i, X i ⟶ Y)
    (hf : Presieve.ofArrows (fun i ↦ B.inclusion.obj (X i)) (fun i ↦ B.inclusion.map (f i)) ∈
      Scheme.fppfPrecoverage (B.inclusion.obj Y)) :
    (smallEtaleSheafFamilyDescentFunctorGeneral B f).IsEquivalence

Tag 0GF4, a lemma

Tag 0GF4 in the Stacks Project.

Stacks.EtaleCohomology.isEquivalence_smallEtaleSheafToCategoricalPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BlowUpSquare/SetSheafEquivalence.lean, line 478.

Stacks Project, Tag 0GF4. Let f : X' ⟶ X be a proper morphism of schemes, i : Z ⟶ X a closed immersion and E = Z ×_X X' with projections j : E ⟶ X' and g : E ⟶ Z. If f is an isomorphism over the open complement U of Z, the functor Sh(X_étale) ⥤ Sh(X'_étale) ×_{Sh(E_étale)} Sh(Z_étale), F ↦ (f⁻¹ F, i⁻¹ F, c) with c the canonical isomorphism j⁻¹ f⁻¹ F ≅ g⁻¹ i⁻¹ F, is an equivalence of categories.

theorem isEquivalence_smallEtaleSheafToCategoricalPullback (U : X.Opens)
    (hU : (U : Set X) = (Set.range i.base)ᶜ) [IsIso (f ∣_ U)] :
    (smallEtaleSheafToCategoricalPullback.{u, 0} f i j g sq.w).IsEquivalence

Tag 0GF5, a lemma

Tag 0GF5 in the Stacks Project.

AlgebraicGeometry.BigHOver.isStackInGroupoids_etaleSheafGroupoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PullbackStalk/SheafHStack.lean, line 228.

Stacks 0GF5. The category fibred in groupoids over the big h site (Sch/S)_h whose fibre over U is the category of sheaves on the small étale site of U is a stack in groupoids.

public theorem isStackInGroupoids_etaleSheafGroupoid :
    (etaleSheafGroupoidProjection B E hBE S hS).IsStackInGroupoids.{w}
      (BigHOver.topology B S hS)

Sources

Section59.105 Blow up squares and étale cohomology #

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

Tag 0EW5, a lemma

Tag 0EW5 in the Stacks Project.

AlgebraicGeometry.exists_distTriang_blowUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BlowUpSquare/BlowUpTriangle.lean, line 77.

Stacks Project, Tag 0EW5. Let X be a scheme and Z ⊆ X the closed subscheme cut out by a quasi-coherent ideal I of finite type (finitely generated on every affine open), with blowup square
E --j--> X'
|π       |b
v        v
Z --i--> X
(X' the blowup of X in I, E = b⁻¹(Z) the exceptional divisor) and c = i ∘ π = b ∘ j. For every K in D⁺(X_étale) (a complex of abelian sheaves on the small étale site, bounded below: K.IsGE n) with torsion cohomology sheaves there is a distinguished triangle K ⟶ Ri_*(K|_Z) ⊕ Rb_*(K|_{X'}) ⟶ Rc_*(K|_E) ⟶ K[1] in D(X_étale), where K|_Y is the derived inverse image. Its first map is formed by the two adjunction units and its second map is the difference of the two comparison maps Ri_*(K|_Z) ⟶ Rc_*(K|_E) (along c = i ∘ π) and Rb_*(K|_{X'}) ⟶ Rc_*(K|_E) (along c = b ∘ j).

public theorem exists_distTriang_blowUp {X : Scheme.{u}} (I : X.IdealSheafData)
    (hI : ∀ U : X.affineOpens, (I.ideal U).FG)
    (K : DerivedCategory (Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})) (n : ℤ)
    (hK : K.IsGE n)
    (hT : Stacks.Torsion.torsionCohomologyProperty.{u + 1} X.smallEtaleTopology K) :
    ∃ δ : (etaleAbelianDerivedDirectImage.{u, 0}
          ((exceptionalIdeal I).subschemeι ≫ blowUpToBase I)).obj
        ((etaleAbelianDerivedInverseImage.{u, 0}
          ((exceptionalIdeal I).subschemeι ≫ blowUpToBase I)).obj K) ⟶ K⟦(1 : ℤ)⟧,
      Triangle.mk (etaleAbelianDerivedSquareUnits.{u, 0} I.subschemeι (blowUpToBase I) K)
        (etaleAbelianDerivedSquareDifference.{u, 0} I.subschemeι (blowUpToBase I)
          (exceptionalIdeal I).subschemeι (exceptionalDivisorToCenter I)
          ((exceptionalIdeal I).subschemeι ≫ blowUpToBase I)
          (isPullback_exceptionalDivisor I).w rfl K) δ ∈
        distTriang (DerivedCategory (Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1}))

Tag 0EW3, a lemma

Tag 0EW3 in the Stacks Project.

AlgebraicGeometry.exists_longExactSequence_blowUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BlowUpSquare/BlowUpLongExactSequence.lean, line 72.

Stacks Project, Tag 0EW3. Let X be a scheme, K an object of D⁺(X_étale) (a complex of abelian sheaves on the small étale site, bounded below: K.IsGE n) with torsion cohomology sheaves, and Z ⊆ X the closed subscheme cut out by a quasi-coherent ideal I of finite type (finitely generated on every affine open). In the blowup square
E --j--> X'
|π       |b
v        v
Z --i--> X
(X' the blowup of X in I, E = b⁻¹(Z) the exceptional divisor) there is a long exact sequence H^p(X, K) ⟶ H^p(X', K|_{X'}) × H^p(Z, K|_Z) ⟶ H^p(E, K|_E) ⟶ H^{p+1}(X, K) ⟶ ⋯ whose first map is x ↦ (x|_{X'}, x|_Z), whose second map is (x', z) ↦ x'|_E - z|_E (the two restrictions read in H^p(E, K|_E), K|_E = (j ≫ b)⁻¹ K, through j⁻¹ b⁻¹ K ≅ K|_E ≅ π⁻¹ i⁻¹ K), and whose third map is a connecting map δ, exact at all three places for every p. Here H^p(Y, M) = Hom(ℤ_Y[-p], M) in D(Y_étale) (Stacks.EtaleCohomology.etaleDerivedCohomology) and K|_Y is the derived inverse image.

public theorem exists_longExactSequence_blowUp {X : Scheme.{u}} (I : X.IdealSheafData)
    (hI : ∀ U : X.affineOpens, (I.ideal U).FG)
    (K : DerivedCategory (Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})) (n : ℤ)
    (hK : K.IsGE n)
    (hT : Stacks.Torsion.torsionCohomologyProperty.{u + 1} X.smallEtaleTopology K) :
    ∃ δ : ∀ p : ℤ, etaleDerivedCohomology.{u, 0} (exceptionalDivisor I) p
        ((etaleAbelianDerivedInverseImage.{u, 0}
          ((exceptionalIdeal I).subschemeι ≫ blowUpToBase I)).obj K) →+
      etaleDerivedCohomology.{u, 0} X (p + 1) K,
    ∀ p : ℤ,
      Function.Exact
        (fun x : etaleDerivedCohomology.{u, 0} X p K ↦
          (etaleDerivedCohomologyRestriction.{u, 0} (blowUpToBase I) p K x,
            etaleDerivedCohomologyRestriction.{u, 0} I.subschemeι p K x))
        (fun y : etaleDerivedCohomology.{u, 0} (blowUp I) p
              ((etaleAbelianDerivedInverseImage.{u, 0} (blowUpToBase I)).obj K) ×
            etaleDerivedCohomology.{u, 0} I.subscheme p
              ((etaleAbelianDerivedInverseImage.{u, 0} I.subschemeι).obj K) ↦
          etaleDerivedCohomologyRestriction.{u, 0} (exceptionalIdeal I).subschemeι p _ y.1 ≫
              (etaleAbelianDerivedInverseImageCompIso'.{u, 0} (exceptionalIdeal I).subschemeι
                (blowUpToBase I) _ rfl).inv.app K -
            etaleDerivedCohomologyRestriction.{u, 0} (exceptionalDivisorToCenter I) p _ y.2 ≫
              (etaleAbelianDerivedInverseImageCompIso'.{u, 0} (exceptionalDivisorToCenter I)
                I.subschemeι _ (isPullback_exceptionalDivisor I).w).inv.app K) ∧
      Function.Exact
        (fun y : etaleDerivedCohomology.{u, 0} (blowUp I) p
              ((etaleAbelianDerivedInverseImage.{u, 0} (blowUpToBase I)).obj K) ×
            etaleDerivedCohomology.{u, 0} I.subscheme p
              ((etaleAbelianDerivedInverseImage.{u, 0} I.subschemeι).obj K) ↦
          etaleDerivedCohomologyRestriction.{u, 0} (exceptionalIdeal I).subschemeι p _ y.1 ≫
              (etaleAbelianDerivedInverseImageCompIso'.{u, 0} (exceptionalIdeal I).subschemeι
                (blowUpToBase I) _ rfl).inv.app K -
            etaleDerivedCohomologyRestriction.{u, 0} (exceptionalDivisorToCenter I) p _ y.2 ≫
              (etaleAbelianDerivedInverseImageCompIso'.{u, 0} (exceptionalDivisorToCenter I)
                I.subschemeι _ (isPullback_exceptionalDivisor I).w).inv.app K)
        (δ p) ∧
      Function.Exact (δ p)
        (fun x : etaleDerivedCohomology.{u, 0} X (p + 1) K ↦
          (etaleDerivedCohomologyRestriction.{u, 0} (blowUpToBase I) (p + 1) K x,
            etaleDerivedCohomologyRestriction.{u, 0} I.subschemeι (p + 1) K x))

Tag 0EW6, a lemma

Tag 0EW6 in the Stacks Project.

AlgebraicGeometry.exists_gluing_blowUp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BlowUpSquare/BlowUpGluing.lean, line 92.

Stacks Project, Tag 0EW6. Let X be a scheme and Z ⊆ X the closed subscheme cut out by a quasi-coherent ideal I of finite type (finitely generated on every affine open), with blowup square
E --j--> X'
|π       |b
v        v
Z --i--> X
(X' the blowup of X in I, E = b⁻¹(Z) the exceptional divisor, c = i ∘ π = b ∘ j). Let K' be an object of D⁺(X'_étale) (bounded below: K'.IsGE n₁) with torsion cohomology sheaves, L an object of D⁺(Z_étale) (L.IsGE n₂), and γ : K'|_E ≅ L|_E an isomorphism, where N|_Y is the derived inverse image. Then there are an object K of D⁺(X_étale) and isomorphisms f : K|_{X'} ≅ K', g : K|_Z ≅ L such that γ = g|_E ∘ f⁻¹|_E (both sides read through the canonical identifications (K|_{X'})|_E ≅ K|_E ≅ (K|_Z)|_E). Moreover, given an object M of D⁺(X_étale) with torsion cohomology sheaves and morphisms α : K' ⟶ M|_{X'}, β : L ⟶ M|_Z with α|_E = β|_E ∘ γ (read through (M|_{X'})|_E ≅ M|_E ≅ (M|_Z)|_E), there is a morphism K ⟶ M in D(X_étale) whose restriction to X' is α ∘ f and whose restriction to Z is β ∘ g.

The source writes the last morphism as M ⟶ K with restrictions a ∘ f, b ∘ g; these are typos for α ∘ f : K|_{X'} ⟶ M|_{X'} and β ∘ g : K|_Z ⟶ M|_Z, which forces the direction K ⟶ M, the direction of the morphism of triangles in the source's proof. The source's hypothesis that L has torsion cohomology sheaves is not needed and is omitted.

public theorem exists_gluing_blowUp {X : Scheme.{u}} (I : X.IdealSheafData)
    (hI : ∀ U : X.affineOpens, (I.ideal U).FG)
    (K' : DerivedCategory (Sheaf (blowUp I).smallEtaleTopology AddCommGrpCat.{u + 1})) (n₁ : ℤ)
    (hK' : K'.IsGE n₁)
    (hK'T : Stacks.Torsion.torsionCohomologyProperty.{u + 1} (blowUp I).smallEtaleTopology K')
    (L : DerivedCategory (Sheaf I.subscheme.smallEtaleTopology AddCommGrpCat.{u + 1})) (n₂ : ℤ)
    (hL : L.IsGE n₂)
    (γ : (etaleAbelianDerivedInverseImage.{u, 0} (exceptionalIdeal I).subschemeι).obj K' ≅
      (etaleAbelianDerivedInverseImage.{u, 0} (exceptionalDivisorToCenter I)).obj L) :
    ∃ (K : DerivedCategory (Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1}))
      (_ : K.IsGE (min n₁ n₂))
      (f : (etaleAbelianDerivedInverseImage.{u, 0} (blowUpToBase I)).obj K ≅ K')
      (g : (etaleAbelianDerivedInverseImage.{u, 0} I.subschemeι).obj K ≅ L),
      γ.hom = (etaleAbelianDerivedInverseImage.{u, 0} (exceptionalIdeal I).subschemeι).map f.inv ≫
          (etaleAbelianDerivedInverseImageCompIso'.{u, 0} (exceptionalIdeal I).subschemeι
            (blowUpToBase I) _ rfl).inv.app K ≫
          (etaleAbelianDerivedInverseImageCompIso'.{u, 0} (exceptionalDivisorToCenter I)
            I.subschemeι _ (isPullback_exceptionalDivisor I).w).hom.app K ≫
          (etaleAbelianDerivedInverseImage.{u, 0} (exceptionalDivisorToCenter I)).map g.hom ∧
      ∀ (M : DerivedCategory (Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})) (m : ℤ),
        M.IsGE m →
        Stacks.Torsion.torsionCohomologyProperty.{u + 1} X.smallEtaleTopology M →
        ∀ (α : K' ⟶ (etaleAbelianDerivedInverseImage.{u, 0} (blowUpToBase I)).obj M)
          (β : L ⟶ (etaleAbelianDerivedInverseImage.{u, 0} I.subschemeι).obj M),
          (etaleAbelianDerivedInverseImage.{u, 0} (exceptionalIdeal I).subschemeι).map α ≫
              (etaleAbelianDerivedInverseImageCompIso'.{u, 0} (exceptionalIdeal I).subschemeι
                (blowUpToBase I) _ rfl).inv.app M ≫
              (etaleAbelianDerivedInverseImageCompIso'.{u, 0} (exceptionalDivisorToCenter I)
                I.subschemeι _ (isPullback_exceptionalDivisor I).w).hom.app M =
            γ.hom ≫ (etaleAbelianDerivedInverseImage.{u, 0} (exceptionalDivisorToCenter I)).map β →
          ∃ φ : K ⟶ M, (etaleAbelianDerivedInverseImage.{u, 0} (blowUpToBase I)).map φ = f.hom ≫ α ∧
            (etaleAbelianDerivedInverseImage.{u, 0} I.subschemeι).map φ = g.hom ≫ β

Sources

LeanAlgebraicGeometry.exists_distTriang_blowUp · AlgebraicGeometry.exists_longExactSequence_blowUp · AlgebraicGeometry.exists_gluing_blowUp

Section59.106 Almost blow up squares and the h topology #

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

Tag 0EWM, an equation

Tag 0EWM in the Stacks Project.

AlgebraicGeometry.IsAlmostBlowUpSquare, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AlmostBlowUp/Basic.lean, line 44.

An almost blowup square with centre I.subscheme and modification b. The exceptional closed subscheme is (I.comap b).subscheme.

public structure IsAlmostBlowUpSquare {X X' : Scheme.{u}}
    (I : X.IdealSheafData) (b : X' ⟶ X) : Prop

Tag 0EWN, a lemma

Tag 0EWN in the Stacks Project.

AlgebraicGeometry.isCSquareIso_of_essImage_almostBlowUpSquare_bigH, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AlmostBlowUp/DerivedHDescent.lean, line 149.

Stacks 0EWN. Let J' ≤ J be a topology coarser than the h topology on the big h category over S — the fppf topology in the source — and let 𝒪 be a sheaf of rings for the h topology, so that the identity functor is a comparison of ringed sites ε : (C_J, 𝒪_J) ⟶ (C_{J'}, 𝒪_{J'}). Then for every almost blowup square in the big h category over S and every object K of D(𝒪_{J'}) in the essential image of the derived direct image Rε_*, the canonical Mayer–Vietoris comparison c^K_{X,Z,X',E} of Stacks 0F16 for the coarser topology is an isomorphism, i.e. a quasi-isomorphism of complexes of abelian groups.

The h sheafified representables of the square form a pushout square by Stacks 0EVD, and h_E^# ⟶ h_{X'}^# is a monomorphism because E ⟶ X' is one, so Stacks 0F19 applies.

theorem isCSquareIso_of_essImage_almostBlowUpSquare_bigH
    (B : BigHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (O : Sheaf (BigHOver.topology B S hS) CommRingCat.{r})
    {J' : GrothendieckTopology (BigHOver B S hS)} (hJ : J' ≤ BigHOver.topology B S hS)
    [HasSheafify (BigHOver.topology B S hS) AddCommGrpCat.{v}]
    [(BigHOver.topology B S hS).WEqualsLocallyBijective AddCommGrpCat.{v}]
    [HasSheafify J' AddCommGrpCat.{v}] [J'.WEqualsLocallyBijective AddCommGrpCat.{v}]
    [UnivLE.{u + 1, v}] [UnivLE.{u, v}] [UnivLE.{r, v}]
    (Rε : DerivedCategory (SheafOfModules.{v}
        (Stacks.SheafOfModules.Tensor.ringSheaf (bigHRingedSite B S hS O).O)) ⥤
      DerivedCategory (SheafOfModules.{v}
        (Stacks.SheafOfModules.Tensor.ringSheaf ((bigHRingedSite B S hS O).ofLe hJ).O)))
    (η : (Stacks.Sites.CoarserTopology.modulePushforward.{u + 1, v, u, r} hJ
          (Stacks.SheafOfModules.Tensor.ringSheaf (bigHRingedSite B S hS O).O)).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rε)
    [Rε.IsRightDerivedFunctor η (HomotopyCategory.quasiIso
      (SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf (bigHRingedSite B S hS O).O))
        (ComplexShape.up ℤ))]
    (K : DerivedCategory (SheafOfModules.{v}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((bigHRingedSite B S hS O).ofLe hJ).O)))
    (hK : Rε.essImage K)
    (sq : Square (BigHOver B S hS))
    (I : ((BigHOver.toScheme B S hS).obj sq.X₄).IdealSheafData)
    (hb : IsAlmostBlowUpSquare I ((BigHOver.toScheme B S hS).map sq.f₂₄))
    (hZ : Nonempty (Over.mk ((BigHOver.toScheme B S hS).map sq.f₃₄) ≅ Over.mk I.subschemeι))
    (hSquare : (sq.map (BigHOver.toScheme B S hS)).IsPullback) :
    (Stacks.MayerVietoris.CanonicalMapOfComplexes.derivedCSquareData.{u + 1, v}
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf ((bigHRingedSite B S hS O).ofLe hJ).O))
        sq).IsCSquareIso K

Tag 0EWQ, a proposition

Tag 0EWQ in the Stacks Project.

AlgebraicGeometry.isCSquareIso_of_essImage_affineAlmostBlowUp_bigH, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AlmostBlowUp/AffineAlmostBlowUpCriterion.lean, line 171. The attribute's comment: “only if”.

Stacks 0EWQ, the direction "only if". Let J' ≤ J be a topology coarser than the h topology on the big h category over S and let 𝒪 be a sheaf of rings for the h topology, so that the identity functor is a comparison of ringed sites ε : (C_J, 𝒪_J) ⟶ (C_{J'}, 𝒪_{J'}). Then for every object K of D(𝒪_{J'}) in the essential image of the derived direct image Rε_* and every almost blowup square of the site with affine base, the canonical Mayer–Vietoris comparison c^K_{X,X',Z,E} of Stacks 0F16 is an isomorphism.

This is Stacks 0EWN; affineness of the base is not used, and K need not be bounded below.

theorem isCSquareIso_of_essImage_affineAlmostBlowUp_bigH
    (Rε : DerivedCategory (SheafOfModules.{v}
        (Stacks.SheafOfModules.Tensor.ringSheaf (bigHRingedSite B S hS O).O)) ⥤
      DerivedCategory (SheafOfModules.{v}
        (Stacks.SheafOfModules.Tensor.ringSheaf ((bigHRingedSite B S hS O).ofLe hJ).O)))
    (η : (modulePushforward.{u + 1, v, u, r} hJ
          (Stacks.SheafOfModules.Tensor.ringSheaf (bigHRingedSite B S hS O).O)).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rε)
    [Rε.IsRightDerivedFunctor η (HomotopyCategory.quasiIso
      (SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf (bigHRingedSite B S hS O).O))
        (ComplexShape.up ℤ))]
    (K : DerivedCategory (SheafOfModules.{v}
        (Stacks.SheafOfModules.Tensor.ringSheaf ((bigHRingedSite B S hS O).ofLe hJ).O)))
    (hK : Rε.essImage K) (sq : AffineAlmostBlowUpSquare B S hS) :
    (Stacks.MayerVietoris.CanonicalMapOfComplexes.derivedCSquareData.{u + 1, v}
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf ((bigHRingedSite B S hS O).ofLe hJ).O))
        sq.square).IsCSquareIso K

AlgebraicGeometry.essImage_iff_forall_isCSquareIso_affineAlmostBlowUp_bigH, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AlmostBlowUp/AffineAlmostBlowUpCriterion.lean, line 280. The attribute's comment: “the iff, given the detection hypothesis”.

Stacks 0EWQ. Let J' ≤ J be a topology coarser than the h topology on the big h category over S and let 𝒪 be a sheaf of rings for the h topology, so that the identity functor is a comparison of ringed sites ε : (C_J, 𝒪_J) ⟶ (C_{J'}, 𝒪_{J'}), and assume that affine almost blowup squares detect h sheaves among J'-sheaves of sets. Then an object K of D⁺(𝒪_{J'}) lies in the essential image of the derived direct image Rε_* if and only if the canonical Mayer–Vietoris comparison c^K_{X,X',Z,E} of Stacks 0F16 is an isomorphism for every almost blowup square of the site whose base is affine.

This is the derived functor, its unit and the object spelled out as binders, which is AlgebraicGeometry.essImageIffAffineAlmostBlowUpBigH_of_isAffineAlmostBlowUpDetecting with its conclusion unfolded; the bundled form is the one a downstream file can state, because there the binders no longer elaborate. The tag is registered here with the detection hypothesis named, and again unconditionally on AlgebraicGeometry.essImage_iff_forall_isCSquareIso_affineAlmostBlowUp_fppf_bigH, the assertion at the fppf topology, where detection holds.

theorem essImage_iff_forall_isCSquareIso_affineAlmostBlowUp_bigH
    (hdetect : BigHOver.IsAffineAlmostBlowUpDetecting B S hS J')
    (Rε : DerivedCategory (SheafOfModules.{v}
        (Stacks.SheafOfModules.Tensor.ringSheaf (bigHRingedSite B S hS O).O)) ⥤
      DerivedCategory (SheafOfModules.{v}
        (Stacks.SheafOfModules.Tensor.ringSheaf ((bigHRingedSite B S hS O).ofLe hJ).O)))
    (η : (modulePushforward.{u + 1, v, u, r} hJ
          (Stacks.SheafOfModules.Tensor.ringSheaf (bigHRingedSite B S hS O).O)).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rε)
    [hRD : Rε.IsRightDerivedFunctor η (HomotopyCategory.quasiIso
      (SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf (bigHRingedSite B S hS O).O))
        (ComplexShape.up ℤ))]
    (K : DerivedCategory (SheafOfModules.{v}
        (Stacks.SheafOfModules.Tensor.ringSheaf ((bigHRingedSite B S hS O).ofLe hJ).O)))
    (hK : (DerivedCategory.TStructure.t (C := SheafOfModules.{v}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((bigHRingedSite B S hS O).ofLe hJ).O))).plus K) :
    Rε.essImage K ↔ ∀ sq : AffineAlmostBlowUpSquare B S hS,
      (Stacks.MayerVietoris.CanonicalMapOfComplexes.derivedCSquareData.{u + 1, v}
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf ((bigHRingedSite B S hS O).ofLe hJ).O))
        sq.square).IsCSquareIso K

AlgebraicGeometry.essImage_iff_forall_isCSquareIso_affineAlmostBlowUp_fppf_bigH, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AlmostBlowUp/AffineAlmostBlowUpFppfCriterion.lean, line 234.

Stacks 0EWQ. Let 𝒪 be a sheaf of rings for the h topology on the big h category over S, and let ε : (C_h, 𝒪_h) ⟶ (C_{fppf}, 𝒪_{fppf}) be the comparison of ringed sites given by the identity functor, the fppf topology on that category being coarser than the h topology. Then an object K of D⁺(𝒪_{fppf}) lies in the essential image of the derived direct image Rε_* if and only if the canonical Mayer–Vietoris comparison c^K_{X,X',Z,E} of Stacks 0F16 is an isomorphism for every almost blowup square of the site whose base is affine.

This is AlgebraicGeometry.essImageIffAffineAlmostBlowUpBigH_of_isAffineAlmostBlowUpDetecting at the fppf topology, where the detection of h sheaves by affine almost blowup squares is AlgebraicGeometry.BigHOver.isAffineAlmostBlowUpDetecting_fppfTopology, the sufficiency direction of Stacks 0EVF.

theorem essImage_iff_forall_isCSquareIso_affineAlmostBlowUp_fppf_bigH :
    EssImageIffAffineAlmostBlowUpBigH.{u, v, r} B S hS O
      (BigHOver.fppfTopology_le_topology B S hS)

Tag 0EWR, a lemma

Tag 0EWR in the Stacks Project.

AlgebraicGeometry.essImage_iff_forall_isCSquareIso_generatorAlmostBlowUp_fppf_bigH, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AlmostBlowUp/GeneratorAlmostBlowUpFppfCriterion.lean, line 250.

Stacks 0EWR. Let 𝒪 be a sheaf of rings for the h topology on the big h category over S, and let ε : (C_h, 𝒪_h) ⟶ (C_{fppf}, 𝒪_{fppf}) be the comparison of ringed sites given by the identity functor, the fppf topology on that category being coarser than the h topology. Then an object K of D⁺(𝒪_{fppf}) lies in the essential image of the derived direct image Rε_* if and only if the canonical Mayer–Vietoris comparison c^K_{X,X',Z,E} of Stacks 0F16 is an isomorphism for every almost blow up square of the site as in More on Flatness, Examples 0EVG and 0EVH.

This is AlgebraicGeometry.essImageIffAffineAlmostBlowUpFamilyBigH_of_isDetecting at the fppf topology for the family of squares of the two shapes, whose detection of h sheaves among fppf sheaves of sets is the sufficiency direction of More on Flatness, Lemma 0EVI, AlgebraicGeometry.BigHOver.isAffineAlmostBlowUpFamilyDetecting_generator_fppfTopology.

theorem essImage_iff_forall_isCSquareIso_generatorAlmostBlowUp_fppf_bigH :
    EssImageIffAffineAlmostBlowUpFamilyBigH.{u + 1, u, v, r} B S hS O
      (BigHOver.fppfTopology_le_topology B S hS)
      (GeneratorAlmostBlowUpSquare.toAffineAlmostBlowUpSquare (B := B) (S := S) (hS := hS))

AlgebraicGeometry.isCSquareIso_of_essImage_principalCenterModelPair_bigH, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/AlmostBlowUp/PrincipalCenterHDescent.lean, line 233. The attribute's comment: “only if, for the almost blow up squares of More on Flatness, Example 0EVG”.

Stacks 0EWR, the "only if" direction for the almost blow up squares of More on Flatness, Example 0EVG. Let J' ≤ J be a topology coarser than the h topology on the big h category over S — the fppf topology in the source — and let 𝒪 be a sheaf of rings for the h topology, so that the identity functor is a comparison of ringed sites ε : (C_J, 𝒪_J) ⟶ (C_{J'}, 𝒪_{J'}). Let K be an object of D(𝒪_{J'}) in the essential image of the derived direct image Rε_*. Then for every almost blow up square of the shape of More on Flatness, Example 0EVG in the big h category over S the canonical Mayer–Vietoris comparison c^K_{X,X',Z,E} of Stacks 0F16 for the coarser topology is a quasi-isomorphism.

The squares named by the source are almost blow up squares, by Stacks 0EVG transported along the isomorphism recognizing the shape, so this is Stacks 0EWN.

theorem isCSquareIso_of_essImage_principalCenterModelPair_bigH
    (B : BigHSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    (O : Sheaf (BigHOver.topology B S hS) CommRingCat.{r})
    {J' : GrothendieckTopology (BigHOver B S hS)} (hJ : J' ≤ BigHOver.topology B S hS)
    [HasSheafify (BigHOver.topology B S hS) AddCommGrpCat.{v}]
    [(BigHOver.topology B S hS).WEqualsLocallyBijective AddCommGrpCat.{v}]
    [HasSheafify J' AddCommGrpCat.{v}] [J'.WEqualsLocallyBijective AddCommGrpCat.{v}]
    [UnivLE.{u + 1, v}] [UnivLE.{u, v}] [UnivLE.{r, v}]
    (Rε : DerivedCategory (SheafOfModules.{v}
        (Stacks.SheafOfModules.Tensor.ringSheaf (bigHRingedSite B S hS O).O)) ⥤
      DerivedCategory (SheafOfModules.{v}
        (Stacks.SheafOfModules.Tensor.ringSheaf ((bigHRingedSite B S hS O).ofLe hJ).O)))
    (η : (Stacks.Sites.CoarserTopology.modulePushforward.{u + 1, v, u, r} hJ
          (Stacks.SheafOfModules.Tensor.ringSheaf (bigHRingedSite B S hS O).O)).mapHomotopyCategory
            (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rε)
    [Rε.IsRightDerivedFunctor η (HomotopyCategory.quasiIso
      (SheafOfModules.{v} (Stacks.SheafOfModules.Tensor.ringSheaf (bigHRingedSite B S hS O).O))
      (ComplexShape.up ℤ))]
    (K : DerivedCategory (SheafOfModules.{v}
      (Stacks.SheafOfModules.Tensor.ringSheaf ((bigHRingedSite B S hS O).ofLe hJ).O)))
    (hK : Rε.essImage K)
    (sq : Square (BigHOver B S hS))
    (hmodel : IsPrincipalCenterModelPair ((BigHOver.toScheme B S hS).map sq.f₂₄)
      ((BigHOver.toScheme B S hS).map sq.f₃₄))
    (hSquare : (sq.map (BigHOver.toScheme B S hS)).IsPullback) :
    (Stacks.MayerVietoris.CanonicalMapOfComplexes.derivedCSquareData.{u + 1, v}
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf ((bigHRingedSite B S hS O).ofLe hJ).O))
      sq).IsCSquareIso K

Sources

LeanAlgebraicGeometry.IsAlmostBlowUpSquare · AlgebraicGeometry.isCSquareIso_of_essImage_almostBlowUpSquare_bigH · AlgebraicGeometry.isCSquareIso_of_essImage_affineAlmostBlowUp_bigH · AlgebraicGeometry.essImage_iff_forall_isCSquareIso_affineAlmostBlowUp_bigH · AlgebraicGeometry.essImage_iff_forall_isCSquareIso_affineAlmostBlowUp_fppf_bigH · AlgebraicGeometry.essImage_iff_forall_isCSquareIso_generatorAlmostBlowUp_fppf_bigH · AlgebraicGeometry.isCSquareIso_of_essImage_principalCenterModelPair_bigH

Section59.107 Cohomology of the structure sheaf in the h topology #

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

Tag 0EWT, a lemma

Tag 0EWT in the Stacks Project.

AlgebraicGeometry.BigHOver.essImage_singleFunctor_perfectionModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HStructureSheaf/EssentialImage.lean, line 119.

Stacks 0EWT. Let p be a prime number and let S be a scheme over 𝔽_p. Consider the sheaf 𝒪^{perf} = colim_F 𝒪 on (Sch/S)_{fppf}. Then 𝒪^{perf} is in the essential image of Rε_* : D((Sch/S)_h) ⟶ D((Sch/S)_{fppf}).

Here (Sch/S)_h is a big h site over S and (Sch/S)_{fppf} its underlying category with the fppf topology. 𝒪^{perf} is the colimit of the Frobenius system of fppf sheaves of rings (AlgebraicGeometry.BigHOver.isColimitPerfectionCocone); it is an h sheaf, so the identity is a comparison of ringed sites ε : ((Sch/S)_h, 𝒪^{perf}) ⟶ ((Sch/S)_{fppf}, 𝒪^{perf}), and Rε_* is any right derived functor of its direct image on sheaves of modules, with its unit η. The object is 𝒪^{perf} regarded as a module over itself and placed in degree zero.

theorem essImage_singleFunctor_perfectionModule
    (Rε : DerivedCategory (SheafOfModules.{u + 1} (Stacks.SheafOfModules.Tensor.ringSheaf
        (bigHRingedSite B S hS (awnRingSheaf B S hS)).O)) ⥤
      DerivedCategory (SheafOfModules.{u + 1} (Stacks.SheafOfModules.Tensor.ringSheaf
        ((bigHRingedSite B S hS (awnRingSheaf B S hS)).ofLe
          (BigHOver.fppfTopology_le_topology B S hS)).O)))
    (η : (Stacks.Sites.CoarserTopology.modulePushforward.{u + 1, u + 1, u, u}
          (BigHOver.fppfTopology_le_topology B S hS)
          (Stacks.SheafOfModules.Tensor.ringSheaf
            (bigHRingedSite B S hS (awnRingSheaf B S hS)).O)).mapHomotopyCategory
          (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh ⟶ DerivedCategory.Qh ⋙ Rε)
    [Rε.IsRightDerivedFunctor η (HomotopyCategory.quasiIso
      (SheafOfModules.{u + 1} (Stacks.SheafOfModules.Tensor.ringSheaf
        (bigHRingedSite B S hS (awnRingSheaf B S hS)).O))
        (ComplexShape.up ℤ))] :
    Rε.essImage ((DerivedCategory.singleFunctor _ 0).obj (perfectionModule B S hS))

Tag 0EWU, a proposition

Tag 0EWU in the Stacks Project.

AlgebraicGeometry.BigHOver.hCohomologyIsoColimitFrobenius, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HStructureSheaf/StructureSheafCohomology.lean, line 116.

Let p be a prime number and let S be a quasi-compact and quasi-separated scheme over 𝔽_p. Then

H^i((Sch/S)_h, 𝒪^h) ≅ colim_F H^i(S, 𝒪)

for every i, where 𝒪^h is the h sheafification of the structure sheaf of the big h site of S, and the colimit is over the system H^i(S, 𝒪) →^F H^i(S, 𝒪) →^F ⋯ induced by the Frobenius F : 𝒪_S ⟶ 𝒪_S, f ↦ f^p.

The left-hand side is cohomology over the final object of the big h category over S, and the right-hand side is the colimit of the right derived functors of sections over S applied to the Frobenius system AlgebraicGeometry.Scheme.abelianFrobeniusSystem.

def hCohomologyIsoColimitFrobenius [CompactSpace S] [QuasiSeparatedSpace S]
    (i : ℕ) :
    (((sheafSections (BigHOver.topology B S hS) AddCommGrpCat.{u}).obj
        (op (BigHOver.final B S hS))).rightDerived i).obj (hStructureSheaf B S hS) ≅
      colimit (S.abelianFrobeniusSystem p hSp ⋙
        ((sheafSections (Opens.grothendieckTopology S) AddCommGrpCat.{u}).obj
          (op ⊤)).rightDerived i)

Sources

LeanAlgebraicGeometry.BigHOver.essImage_singleFunctor_perfectionModule · AlgebraicGeometry.BigHOver.hCohomologyIsoColimitFrobenius

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

59.99 Comparing big and small… to 59.107 Cohomology of the…

Section59.99 Comparing big and small topoi#

Tag 0758, a lemma

Tag 0759, an equation

Tag 075A, a lemma

Tag 0DDH, a lemma

Tag 0DDI, a lemma

Tag 0DDJ, a lemma

Sources

Section59.100 Comparing fppf and étale topologies#

Tag 0DDL, a lemma

Tag 0DDM, a lemma

Tag 0DDN, a lemma

Tag 0DEU, a lemma

Tag 0F0H, a lemma

Tag 0DDS, a lemma

Tag 0DDT, a lemma

Tag 0DDU, a lemma

Sources

Section59.101 Comparing fppf and étale topologies: modules#

Tag 0DEW, a lemma

Tag 0DEX, a lemma

Tag 0H0U, a lemma

Sources

Section59.102 Comparing ph and étale topologies#

Tag 0DDW, a lemma

Tag 0DDX, a lemma

Tag 0DDY, a lemma

Tag 0F0I, a lemma

Tag 0DE4, a lemma

Tag 0DE5, a lemma

Tag 0DE6, a lemma

Sources

Section59.103 Comparing h and étale topologies#

Tag 0EW8, a lemma

Tag 0EW9, a lemma

Tag 0EWA, a lemma

Tag 0F0J, a lemma

Tag 0EWF, a lemma

Tag 0EWG, a lemma

Tag 0EWH, a lemma

Sources

Section59.104 Descending étale sheaves#

Tag 0GEY, a lemma

Tag 0GEZ, a lemma

Tag 0GF0, a lemma

Tag 0GF1, a lemma

Tag 0GF2, a lemma

Tag 0GF3, a lemma

Tag 0GF4, a lemma

Tag 0GF5, a lemma

Sources

Section59.105 Blow up squares and étale cohomology#

Tag 0EW5, a lemma

Tag 0EW3, a lemma

Tag 0EW6, a lemma

Sources

Section59.106 Almost blow up squares and the h topology#

Tag 0EWM, an equation

Tag 0EWN, a lemma

Tag 0EWQ, a proposition

Tag 0EWR, a lemma

Sources

Section59.107 Cohomology of the structure sheaf in the h topology#

Tag 0EWT, a lemma

Tag 0EWU, a proposition

Sources

Section59.99 Comparing big and small topoi #

Section59.100 Comparing fppf and étale topologies #

Section59.101 Comparing fppf and étale topologies: modules #

Section59.102 Comparing ph and étale topologies #

Section59.103 Comparing h and étale topologies #

Section59.104 Descending étale sheaves #

Section59.105 Blow up squares and étale cohomology #

Section59.106 Almost blow up squares and the h topology #

Section59.107 Cohomology of the structure sheaf in the h topology #