25 Hypercoverings

Chapter 25 of the Stacks Project, Hypercoverings, Tag 01FX: the 11 sections of its 12 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 53 tags are carried by 114 declarations of the repository (all in StacksFrontier) and 12 registered declarations.

Section25.2 Semi-representable objects#

Section 25.2 of the Stacks Project, Tag 0DBB. 3 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01G0, a definition

Tag 01G0 in the Stacks Project.

Declarations registered for the tag:

Tag 01G1, a definition

Tag 01G1 in the Stacks Project.

Declarations registered for the tag:

Tag 01G2, a lemma

Tag 01G2 in the Stacks Project.

CategoryTheory.Limits.FormalCoproduct.instHasBinaryProducts, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Limits/FormalCoproductBinaryProducts.lean, line 55. The attribute's comment: “products of pairs in SR(C)”.

Stacks Project, Tag 01G2, products of pairs clause. If C has binary products, then so does its category of formal coproducts — equivalently, the category SR(C) of semi-representable objects of C has binary products.

instance instHasBinaryProducts : HasBinaryProducts (FormalCoproduct.{w} C)

CategoryTheory.Limits.FormalCoproduct.instHasEqualizers, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Limits/FormalCoproductEqualizers.lean, line 116. The attribute's comment: “equalizers”. References: SGA 4 V (7.3.0), “equalizers in SR(C)”.

Stacks Project, Tag 01G2, equalizers clause. If C has equalizers, then so does its category of formal coproducts — equivalently, the category SR(C) of semi-representable objects of C has equalizers.

instance instHasEqualizers : HasEqualizers (FormalCoproduct.{w} C)

CategoryTheory.Limits.FormalCoproduct.hasCoproducts_formalCoproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Limits/FormalCoproductLimits.lean, line 81. The attribute's comment: “coproducts in SR(C)”.

Stacks Project, Tag 01G2, coproducts clause, first half. The category of formal coproducts of C — equivalently, the category SR(C) of semi-representable objects of C — has arbitrary coproducts, indexed by types in the index universe w. The coproduct of a family of families of objects is obtained by concatenating the index types.

theorem hasCoproducts_formalCoproduct : HasCoproducts.{w} (FormalCoproduct.{w} C)

CategoryTheory.Limits.FormalCoproduct.preservesColimitsOfShape_yoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Limits/FormalCoproductLimits.lean, line 88. The attribute's comment: “F commutes with coproducts”.

Stacks Project, Tag 01G2, coproducts clause, second half. The functor F : SR(C) ⥤ PSh(C), sending a family {U_i} of objects of C to the coproduct ∐ h_{U_i} of the representable presheaves, commutes with coproducts.

theorem preservesColimitsOfShape_yoneda (J : Type v) :
    PreservesColimitsOfShape (Discrete J) (FormalCoproduct.yoneda (C := C))

CategoryTheory.Limits.FormalCoproduct.preservesLimitsOfSize_yoneda, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Limits/FormalCoproductLimits.lean, line 133. The attribute's comment: “F : SR(C) → PSh(C) commutes with limits”.

Stacks Project, Tag 01G2, limits clause. The functor F : SR(C) ⥤ PSh(C), sending a family {U_i} of objects of C to the coproduct ∐ h_{U_i} of the representable presheaves, commutes with limits — of any shape, and for an arbitrary category C.

Limits of presheaves are computed sectionwise, and each section functor of F is corepresentable by yonedaCompEvaluationIso.

noncomputable instance preservesLimitsOfSize_yoneda :
    PreservesLimitsOfSize.{w, w'} (FormalCoproduct.yoneda (C := C))

CategoryTheory.Limits.FormalCoproduct.hasPullbacks_formalCoproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Limits/FormalCoproductLimits.lean, line 149. The attribute's comment: “fibre products in SR(C)”.

Stacks Project, Tag 01G2, fibre products clause. If C has fibre products, then so does its category of formal coproducts — equivalently, the category SR(C) of semi-representable objects of C has fibre products. They are computed componentwise, the index type of {U_i} ×_{{V_j}} {W_k} being the set of triples (i, j, k) with j the common image of i and of k.

theorem hasPullbacks_formalCoproduct [HasPullbacks C] :
    HasPullbacks (FormalCoproduct.{w} C)

CategoryTheory.Limits.FormalCoproduct.hasTerminal_formalCoproduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Limits/FormalCoproductLimits.lean, line 162. The attribute's comment: “final object in SR(C)”.

Stacks Project, Tag 01G2, final object clause. If C has a final object X, then the one-member family {X} is a final object of the category of formal coproducts of C — equivalently, of the category SR(C) of semi-representable objects of C.

theorem hasTerminal_formalCoproduct [HasTerminal C] :
    HasTerminal (FormalCoproduct.{w} C)

Stacks.CategoryTheory.Hypercovering.hasFiniteLimits_formalCoproductOver, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CoveringPermanence.lean, line 915. The attribute's comment: “SR(C, X) has finite limits”.

Stacks Project, Tag 01G2, finite limits clause for SR(C, X), first half. If C has fibre products then SR(C, X) has finite limits: it has a terminal object, namely {X → X}, and it has fibre products, computed componentwise.

The second half of the clause, that F : SR(C, X) ⥤ PSh(C)/h_X commutes with those finite limits, is the instance CategoryTheory.Limits.FormalCoproduct.preservesLimitsOfSize_yonedaOver in StacksFrontier.CategoryTheory.Sites.Localization.SemiRepresentableOver, for limits of every shape.

instance hasFiniteLimits_formalCoproductOver {X : C} :
    HasFiniteLimits (FormalCoproduct.{w} (Over X))

CategoryTheory.Limits.FormalCoproduct.yonedaOverObjIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/SemiRepresentableOver.lean, line 207. The attribute's comment: “the value of F: F({U_i → X}) is ∐ h_{U_i} augmented to h_X”.

The value of F on a family, Stacks Project, Tag 01G2. F({U_i → X}) is the coproduct ∐ h_{U_i} of the representable presheaves of the U_i, equipped with the map to h_X whose component on h_{U_i} is h of the structure morphism U_i → X. This is the source's F({U_i → X}) = (∐ h_{U_i} → h_X), and it is what makes the clauses below statements about the source's F.

The proof is the source's description read backwards: FormalCoproduct.yoneda of C/X sends {U_i → X} to the coproduct of the presheaves on C/X represented by the U_i → X, the presheaf level j_{X!} preserves that coproduct because it is a left adjoint (OverShriek.presheafAdjunction), and it takes the presheaf represented by U_i → X to the presheaf represented by U_i over h_X (OverShriek.presheafFunctorToOverYonedaIso).

noncomputable def yonedaOverObjIso (A : FormalCoproduct.{v} (Over X)) :
    (yonedaOver X).obj A ≅
      Over.mk (Sigma.desc fun i : A.I ↦ CategoryTheory.yoneda.map (A.obj i).hom)

CategoryTheory.Limits.FormalCoproduct.hasCoproducts_formalCoproductOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/SemiRepresentableOver.lean, line 216. The attribute's comment: “coproducts in SR(C, X)”.

Stacks Project, Tag 01G2, coproducts clause for SR(C, X), first half. The category SR(C, X) of semi-representable objects over X has arbitrary coproducts, obtained by concatenating the index types of the families.

theorem hasCoproducts_formalCoproductOver :
    HasCoproducts.{w} (FormalCoproduct.{w} (Over X))

CategoryTheory.Limits.FormalCoproduct.preservesColimitsOfShape_yonedaOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/SemiRepresentableOver.lean, line 224. The attribute's comment: “F commutes with coproducts in SR(C, X)”.

Stacks Project, Tag 01G2, coproducts clause for SR(C, X), second half. The functor F : SR(C, X) ⥤ PSh(C)/h_X commutes with coproducts: the semi-representable Yoneda embedding of C/X does, and j_{X!} : PSh(C/X) ⥤ PSh(C)/h_X is an equivalence.

theorem preservesColimitsOfShape_yonedaOver (J : Type v) :
    PreservesColimitsOfShape (Discrete J) (yonedaOver X)

CategoryTheory.Limits.FormalCoproduct.preservesLimitsOfSize_yonedaOver, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/SemiRepresentableOver.lean, line 235. The attribute's comment: “F : SR(C, X) → PSh(C)/h_X commutes with finite limits”.

Stacks Project, Tag 01G2, finite limits clause for SR(C, X), second half. The functor F : SR(C, X) ⥤ PSh(C)/h_X commutes with limits of every shape, with no hypothesis on C; this strengthens the finite limits of the source's clause. The first half, that SR(C, X) has finite limits as soon as C has fibre products, is Stacks.CategoryTheory.Hypercovering.hasFiniteLimits_formalCoproductOver.

noncomputable instance preservesLimitsOfSize_yonedaOver :
    PreservesLimitsOfSize.{w, w'} (yonedaOver X)
Sources
LeanCategoryTheory.Limits.FormalCoproduct · CategoryTheory.Limits.FormalCoproduct.Hom · CategoryTheory.Limits.FormalCoproduct.category · CategoryTheory.Limits.FormalCoproduct.yoneda · CategoryTheory.Limits.FormalCoproduct.instHasBinaryProducts · CategoryTheory.Limits.FormalCoproduct.instHasEqualizers · CategoryTheory.Limits.FormalCoproduct.hasCoproducts_formalCoproduct · CategoryTheory.Limits.FormalCoproduct.preservesColimitsOfShape_yoneda

Section25.3 Hypercoverings#

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

Tag 01G3, a definition

Tag 01G3 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.CoveringFamilies.IsCovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CoveringFamilies.lean, line 157. The attribute's comment: “the definition for SR(C)”.

Stacks Project, Tag 01G3. A morphism of semi-representable objects is covering when every one of its fibre families is a covering family of the site. The target is allowed to be an arbitrary formal coproduct, as it is for a matching object.

abbrev IsCovering (Cov : CoveringFamilies.{s, w} C) {U : SetFamily.{w} C}
    {V : FormalCoproduct.{w + 1} C} (f : U.toFormalCoproduct ⟶ V) : Prop

Stacks.CategoryTheory.Hypercovering.CoveringFamilies.IsCoveringOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CoveringFamilies.lean, line 164. The attribute's comment: “the definition for SR(C, X)”.

Stacks Project, Tag 01G3. A morphism of semi-representable objects over X is covering when every one of its underlying fibre families is a covering family of the site.

abbrev IsCoveringOver (Cov : CoveringFamilies.{s, w} C)
    {X : C} {U : SetFamily.{w} (Over X)} {V : FormalCoproduct.{w + 1} (Over X)}
    (f : U.toFormalCoproduct ⟶ V) : Prop
Tag 01G4, a lemma

Tag 01G4 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.IsCovering.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CoveringPermanence.lean, line 192. The attribute's comment: “part (1), for SR(C)”.

Stacks Project, Tag 01G4, part (1). The composition of two covering morphisms of semi-representable objects is a covering morphism.

theorem IsCovering.comp (J : Pretopology C)
    [Precoverage.IsStableUnderComposition J.toPrecoverage]
    {U V W : FormalCoproduct.{w} C} {f : U ⟶ V} {g : V ⟶ W}
    (hf : IsCovering J f) (hg : IsCovering J g) : IsCovering J (f ≫ g)

Stacks.CategoryTheory.Hypercovering.IsCoveringOver.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CoveringPermanence.lean, line 213. The attribute's comment: “part (1), for SR(C, X)”.

Stacks Project, Tag 01G4, part (1). The composition of two covering morphisms of semi-representable objects over X is a covering morphism.

theorem IsCoveringOver.comp (J : Pretopology C)
    [Precoverage.IsStableUnderComposition J.toPrecoverage] {X : C}
    {U V W : FormalCoproduct.{w} (Over X)} {f : U ⟶ V} {g : V ⟶ W}
    (hf : IsCoveringOver J f) (hg : IsCoveringOver J g) : IsCoveringOver J (f ≫ g)

Stacks.CategoryTheory.Hypercovering.IsCovering.pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CoveringPermanence.lean, line 352. The attribute's comment: “part (2), for SR(C)”.

Stacks Project, Tag 01G4, part (2). The base change of a covering morphism of semi-representable objects along any morphism exists and is a covering morphism.

theorem IsCovering.pullback (J : Pretopology C) {U V W : FormalCoproduct.{w} C}
    (f : U ⟶ V) (g : W ⟶ V) (hf : IsCovering J f) :
    IsCovering J (pullbackFormalCoproduct.snd f g (pullbackConeFamily f g))

Stacks.CategoryTheory.Hypercovering.IsCoveringOver.pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CoveringPermanence.lean, line 375. The attribute's comment: “part (2), for SR(C, X)”.

Stacks Project, Tag 01G4, part (2). The base change of a covering morphism of semi-representable objects over X along any morphism exists and is a covering morphism.

theorem IsCoveringOver.pullback (J : Pretopology C) {X : C}
    {U V W : FormalCoproduct.{w} (Over X)} (f : U ⟶ V) (g : W ⟶ V) (hf : IsCoveringOver J f) :
    IsCoveringOver J (pullbackFormalCoproduct.snd f g (pullbackConeFamilyOver f g))

Stacks.CategoryTheory.Hypercovering.IsCovering.prod_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CoveringPermanence.lean, line 436. The attribute's comment: “part (3), for SR(C)”.

Stacks Project, Tag 01G4, part (3). The product of two covering morphisms of semi-representable objects is a covering morphism.

theorem IsCovering.prod_map (J : Pretopology C)
    [Precoverage.IsStableUnderComposition J.toPrecoverage]
    [HasBinaryProducts (FormalCoproduct.{w} C)]
    {A B K L : FormalCoproduct.{w} C} {f : A ⟶ B} {g : K ⟶ L}
    (hf : IsCovering J f) (hg : IsCovering J g) : IsCovering J (prod.map f g)

Stacks.CategoryTheory.Hypercovering.IsCoveringOver.prod_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CoveringPermanence.lean, line 449. The attribute's comment: “part (3), for SR(C, X)”.

Stacks Project, Tag 01G4, part (3). The product of two covering morphisms of semi-representable objects over X is a covering morphism.

theorem IsCoveringOver.prod_map (J : Pretopology C)
    [Precoverage.IsStableUnderComposition J.toPrecoverage] {X : C}
    [HasBinaryProducts (FormalCoproduct.{w} (Over X))]
    {A B K L : FormalCoproduct.{w} (Over X)} {f : A ⟶ B} {g : K ⟶ L}
    (hf : IsCoveringOver J f) (hg : IsCoveringOver J g) :
    IsCoveringOver J (prod.map f g)
Tag 01G5, a definition

Tag 01G5 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.CoveringFamilies.IsHypercovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CoveringFamilies.lean, line 186. References: SGA 4 V (7.3.3), “object case, no type p”.

Stacks Project, Tag 01G5. A hypercovering of X for the site's covering families: the degree-zero family is one of the covering families of X, and all fibres of the successive matching morphisms are covering families of the site. The coskeleton is computed in formal coproducts, after including the set-indexed families.

abbrev IsHypercovering (Cov : CoveringFamilies.{s, w} C) {X : C}
    (K : SimplicialObject (SetFamily.{w} (Over X))) : Prop
Tag 01G6, an example

Tag 01G6 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.isCoveringOver_terminal_from_power, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Cech.lean, line 286. The attribute's comment: “condition (1) of Definition 01G5, for the degree-zero term of the Čech object”.

Stacks Project, Tag 01G6, condition (1) of Definition 01G5 for the Čech construction. If the family U covers X then so does its α-fold power for a one-element index type α, which is the degree-zero term of the Čech object of U: that term is U again, its component at i being a product of one copy of the component of U at i default.

theorem isCoveringOver_terminal_from_power (J : Pretopology C) {X : C}
    (U : FormalCoproduct.{w} (Over X)) (α : Type) [Unique α] [HasProductsOfShape α (Over X)]
    (hU : IsCoveringOver J (terminal.from U)) :
    IsCoveringOver J (terminal.from (U.power α))

Stacks.CategoryTheory.Hypercovering.IsCechHypercovering, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Cech.lean, line 328. The attribute's comment: “the definition of a Čech hypercovering”.

Stacks Project, Tag 01G6. A simplicial object K of SR(C, X) is a Čech hypercovering of X when its degree-zero family K_0 covers X and K is the zeroth coskeleton of K_0, that is, when K is isomorphic to cosk₀ U for a zero-truncated simplicial object U of SR(C, X).

abbrev IsCechHypercovering (J : Pretopology C) {X : C}
    (K : SimplicialObject (FormalCoproduct.{w} (Over X))) : Prop

Stacks.CategoryTheory.Hypercovering.IsCechHypercovering.isHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Cech.lean, line 339. The attribute's comment: “condition (2) of Definition 01G5 by Tag 018B, hence the hypercovering property”.

Stacks Project, Tag 01G6, condition (2) of Definition 01G5 and the hypercovering property. A Čech hypercovering of X is a hypercovering of X: its degree-zero family covers X by definition, and each of its matching morphisms is an isomorphism, hence covering, because cosk₀ U is n-coskeletal for every n (Tag 018B).

theorem IsCechHypercovering.isHypercovering {J : Pretopology C} {X : C}
    {K : SimplicialObject (FormalCoproduct.{w} (Over X))} (hK : IsCechHypercovering J K) :
    IsHypercovering J K

Stacks.CategoryTheory.Hypercovering.isCechHypercovering_cech, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Cech.lean, line 363. The attribute's comment: “the Čech object of a covering family is a Čech hypercovering”.

Stacks Project, Tag 01G6. The Čech object of a covering family of X is a Čech hypercovering of X: its degree-zero term is the covering family again, and it is 0-coskeletal, hence isomorphic to the zeroth coskeleton of that term.

theorem isCechHypercovering_cech (J : Pretopology C) {X : C}
    (A : FormalCoproduct.{w} (Over X)) (hA : IsCoveringOver J (terminal.from A)) :
    let : HasTerminal (Over X) := Over.over_hasTerminal X
    let : HasBinaryProducts (Over X) :=
      Over.ConstructProducts.over_binaryProduct_of_pullback
    let : HasFiniteProducts (Over X) := hasFiniteProducts_of_has_binary_and_terminal
    IsCechHypercovering J A.cech

Stacks.CategoryTheory.Hypercovering.isHypercovering_cech_of_isCoveringOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Cech.lean, line 383. The attribute's comment: “the Čech object of a covering family is a hypercovering”.

Stacks Project, Tag 01G6. The Čech object of a covering family {U_i → X}_{i ∈ I} of X is a hypercovering of X. Its degree-n term is the family of the (n + 1)-fold fibre products U_{i_0} ×_X ⋯ ×_X U_{i_n} over X, indexed by I^{n + 1}; see FormalCoproduct.cech_obj, FormalCoproduct.power_I and FormalCoproduct.power_obj. The one-member case is isHypercovering_cech, Tag 0GMA.

theorem isHypercovering_cech_of_isCoveringOver (J : Pretopology C) {X : C}
    (A : FormalCoproduct.{w} (Over X)) (hA : IsCoveringOver J (terminal.from A)) :
    let : HasTerminal (Over X) := Over.over_hasTerminal X
    let : HasBinaryProducts (Over X) :=
      Over.ConstructProducts.over_binaryProduct_of_pullback
    let : HasFiniteProducts (Over X) := hasFiniteProducts_of_has_binary_and_terminal
    IsHypercovering J A.cech

Stacks.CategoryTheory.Hypercovering.isHypercovering_cosk_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Cech.lean, line 409. The attribute's comment: “the hypercovering property in the cosk₀ form”.

Stacks Project, Tag 01G6, in the cosk₀ shape in which the source states it: the zeroth coskeleton of a zero-truncated simplicial object of SR(C, X) is a hypercovering of X as soon as its degree-zero family covers X. The degree-zero family of cosk₀ U is U up to the isomorphism given by the counit of the coskeletal adjunction; the covering hypothesis is stated for cosk₀ U itself because a covering family of a pretopology need not stay covering under an arbitrary isomorphism of SR(C, X) — see the implementation notes.

This is a convenience restatement, not the tag's assertion, and its hypothesis placement is not claimed to be optimal: the counit comparison at level 0 is a limit over a one-object, one-morphism indexing category, so it is of the objectwise shape that isCoveringOver_terminal_from_of_objFun transports, and stating the hypothesis on U itself is expected to be reachable by that route — it would need an explicit description of the pointwise right Kan extension at degree 0, which is not developed here. For the covering family itself as the hypothesis, use isHypercovering_cech_of_isCoveringOver, which carries the source's own hypothesis and whose Čech object is 0-coskeletal and therefore of this form.

theorem isHypercovering_cosk_zero (J : Pretopology C) {X : C}
    (U : SimplicialObject.Truncated (FormalCoproduct.{w} (Over X)) 0)
    (hU : IsCoveringOver J
      (terminal.from (((SimplicialObject.Truncated.cosk 0).obj U).obj (op ⦋0⦌)))) :
    IsHypercovering J ((SimplicialObject.Truncated.cosk 0).obj U)

Stacks.CategoryTheory.Hypercovering.isLimitWidePullbackConePowerObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Cech.lean, line 427. The attribute's comment: “the terms in C: each component is the fibre product over X of its factors”.

Stacks Project, Tag 01G6, the terms clause read in C. The component at i : α → I of the α-fold power of the family A = {U_i → X} is a product taken in Over X; its underlying object of C is the fibre product over X of the U_{i a}. Precisely, the cone in C with apex that underlying object, projections the underlying morphisms of the product projections of Over X and base the structure morphism to X, is a limit of the wide cospan of the structure morphisms U_{i a} → X.

Together with FormalCoproduct.cech_obj, FormalCoproduct.power_I and FormalCoproduct.power_obj this is the source's formula K_n = {U_{i_0} ×_X ⋯ ×_X U_{i_n} → X} indexed by I^{n + 1}: take α = Fin (n + 1).

noncomputable def isLimitWidePullbackConePowerObj {X : C} (A : FormalCoproduct.{w} (Over X))
    (α : Type) [Finite α] :
    let : HasTerminal (Over X) := Over.over_hasTerminal X
    let : HasBinaryProducts (Over X) :=
      Over.ConstructProducts.over_binaryProduct_of_pullback
    let : HasFiniteProducts (Over X) := hasFiniteProducts_of_has_binary_and_terminal
    ∀ i : α → A.I, IsLimit (WidePullbackCone.mk (f := fun a ↦ (A.obj (i a)).hom)
      ((A.power α).obj i).hom (fun a ↦ (Pi.π (A.obj ∘ i) a).left)
      fun a ↦ Over.w (Pi.π (A.obj ∘ i) a))

Declarations registered for the tag:

Tag 0GM9, an example

Tag 0GM9 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.associatedSimplicialObject, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/FromSimplicialObject.lean, line 172. The attribute's comment: “the associated simplicial object”.

Stacks Project, Tag 0GM9. The one-summand simplicial semi-representable object associated to an augmented simplicial object of the site.

def associatedSimplicialObject :
    SimplicialObject (FormalCoproduct.{w} (Over X))

Stacks.CategoryTheory.Hypercovering.isHypercovering_associatedSimplicialObject_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/FromSimplicialObject.lean, line 682. The attribute's comment: “the covering characterization”.

Stacks Project, Tag 0GM9. The simplicial semi-representable object over X associated to an augmented simplicial object U ⟶ X is a hypercovering exactly when the augmentation in degree zero, the degree-one morphism to U₀ ×_X U₀, and every higher matching morphism generate a covering presieve of the site.

theorem isHypercovering_associatedSimplicialObject_iff (J : Pretopology C) :
    IsHypercovering J (associatedSimplicialObject U a) ↔
      (Presieve.singleton (a.app (Opposite.op (SimplexCategory.mk 0))) ∈ J X) ∧
      (Presieve.singleton (oneSimplexToFiberProduct U a) ∈
        J (pullback (a.app (Opposite.op (SimplexCategory.mk 0)))
          (a.app (Opposite.op (SimplexCategory.mk 0))))) ∧
      ∀ n : ℕ, 1 ≤ n → Presieve.singleton (matchingMap U a n) ∈
        J ((((SimplicialObject.cosk n).obj (Over.lift U a)).obj
          (Opposite.op (SimplexCategory.mk (n + 1)))).left)
Tag 0GMA, an example

Tag 0GMA in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.isHypercovering_cech, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CechOfCovering.lean, line 211. The attribute's comment: “the hypercovering property”.

Stacks Project, Tag 0GMA. The Čech object of a covering morphism is a hypercovering of its target.

theorem isHypercovering_cech (J : Pretopology C) {U X : C} (f : U ⟶ X)
    (hf : Presieve.singleton f ∈ J.coverings X) :
    let : HasTerminal (Over X) := Over.over_hasTerminal X
    let : HasBinaryProducts (Over X) :=
      Over.ConstructProducts.over_binaryProduct_of_pullback
    let : HasFiniteProducts (Over X) := hasFiniteProducts_of_has_binary_and_terminal
    IsHypercovering J ((FormalCoproduct.incl (Over X)).obj (Over.mk f)).cech

Declarations registered for the tag:

Tag 01G7, a lemma

Tag 01G7 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.small_hypercoverings, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Small.lean, line 92.

Stacks Project, Tag 01G7. Hypercoverings of an object of a site with fibre products form a set.

public theorem small_hypercoverings (Cov : CoveringFamilies.{s, w} C) (X : C) :
    Small.{max s u v w}
      {K : SimplicialObject (SetFamily.{w} (Over X)) //
        CoveringFamilies.IsHypercovering Cov K}
Tag 01G9, a lemma

Tag 01G9 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.locallySurjective_augmentation_of_isHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/LocallySurjective.lean, line 852. The attribute's comment: “part (1)”.

The degree-zero augmentation of the simplicial presheaf associated to a hypercovering is locally surjective.

theorem locallySurjective_augmentation_of_isHypercovering
    (J : Pretopology C) {X : C}
    (K : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (hK : IsHypercovering J K) :
    Presheaf.IsLocallySurjective J.toGrothendieck
      ((associatedAugmentedSimplicialPresheafOver K).hom.app
        (Opposite.op (SimplexCategory.mk 0)))

Stacks.CategoryTheory.Hypercovering.locallySurjective_oneMatchingMap_of_isHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/LocallySurjective.lean, line 879. The attribute's comment: “part (2)”.

The map from one-simplices to the fibre product of two copies of the presheaf of vertices over the representable presheaf of X is locally surjective.

theorem locallySurjective_oneMatchingMap_of_isHypercovering
    (J : Pretopology C) {X : C}
    (K : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (hK : IsHypercovering J K) :
    Presheaf.IsLocallySurjective J.toGrothendieck
      (oneMatchingMap (associatedAugmentedSimplicialPresheafOver K).left
        (associatedAugmentedSimplicialPresheafOver K).right
        (associatedAugmentedSimplicialPresheafOver K).hom)

Stacks.CategoryTheory.Hypercovering.locallySurjective_higherMatchingMap_of_isHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/LocallySurjective.lean, line 895. The attribute's comment: “part (3)”.

Every higher matching map of the simplicial presheaf associated to a hypercovering is locally surjective.

theorem locallySurjective_higherMatchingMap_of_isHypercovering
    (J : Pretopology C) {X : C}
    (K : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (hK : IsHypercovering J K) (n : ℕ) (hn : 1 ≤ n) :
    Presheaf.IsLocallySurjective J.toGrothendieck
      (((SimplicialObject.coskAdj n).unit.app
        (associatedAugmentedSimplicialPresheafOver K).left).app
          (Opposite.op (SimplexCategory.mk (n + 1))))
Sources
LeanStacks.CategoryTheory.Hypercovering.CoveringFamilies.IsCovering · Stacks.CategoryTheory.Hypercovering.CoveringFamilies.IsCoveringOver · Stacks.CategoryTheory.Hypercovering.IsCovering.comp · Stacks.CategoryTheory.Hypercovering.IsCoveringOver.comp · Stacks.CategoryTheory.Hypercovering.IsCovering.pullback · Stacks.CategoryTheory.Hypercovering.IsCoveringOver.pullback · Stacks.CategoryTheory.Hypercovering.IsCovering.prod_map · Stacks.CategoryTheory.Hypercovering.IsCoveringOver.prod_map

Section25.4 Acyclicity#

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

Tag 01GB, a definition

Tag 01GB in the Stacks Project.

Declarations registered for the tag:

Tag 01GC, a lemma

Tag 01GC in the Stacks Project.

CategoryTheory.Presheaf.isZero_sheafHomology_cechNerve_of_isLocallySurjective, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CechNerveHomology.lean, line 530. The attribute's comment: “positive degrees”.

The positive homology sheaves of the Čech nerve of a locally surjective morphism of presheaves of sets vanish.

lemma isZero_sheafHomology_cechNerve_of_isLocallySurjective (hf : IsLocallySurjective J f)
    (n : ℕ) (hn : 0 < n) :
    IsZero (SimplicialObject.sheafHomology J (Arrow.mk f).cechNerve n)

CategoryTheory.Presheaf.isIso_cechNerveSheafHomologyZeroAugmentation, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CechNerveHomology.lean, line 547. The attribute's comment: “degree zero”.

The augmentation of the Čech nerve of a locally surjective morphism induces an isomorphism from its degree-zero homology sheaf to the free abelian sheaf on the target.

lemma isIso_cechNerveSheafHomologyZeroAugmentation (hf : IsLocallySurjective J f) :
    IsIso (cechNerveSheafHomologyZeroAugmentation J f)
Tag 01GD, a lemma

Tag 01GD in the Stacks Project.

CategoryTheory.SimplicialObject.isIso_sheafHomologyFunctor_map_of_coskeletal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CoskeletalAcyclicity.lean, line 507. References: SGA 4 V (7.2.1), “homology iso”.

Stacks Project, Tag 01GD. A morphism between n-coskeletal simplicial presheaves which is an isomorphism in degrees below n and locally surjective in degree n induces an isomorphism on every homology sheaf.

theorem isIso_sheafHomologyFunctor_map_of_coskeletal
    (J : GrothendieckTopology C) [HasSheafify J AddCommGrpCat.{w}]
    {L K : SimplicialObject (Cᵒᵖ ⥤ Type w)} (f : L ⟶ K) (n i : ℕ)
    (h_lt : ∀ j : ℕ, j < n → IsIso (f.app (op (SimplexCategory.mk j))))
    (h_surjective :
      Presheaf.IsLocallySurjective J (f.app (op (SimplexCategory.mk n))))
    (hL : IsIso ((SimplicialObject.coskAdj n).unit.app L))
    (hK : IsIso ((SimplicialObject.coskAdj n).unit.app K)) :
    IsIso ((sheafHomologyFunctor J i).map f)
Tag 01GE, a lemma

Tag 01GE in the Stacks Project.

CategoryTheory.SimplicialObject.Augmented.isZero_sheafHomology_of_isLocallySurjective_matchingMaps, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/AugmentedAcyclicity.lean, line 568. The attribute's comment: “positive-degree vanishing”. References: SGA 4 V (7.3.2), “more general”.

Stacks Project, Tag 01GE (positive degrees). An augmented simplicial presheaf whose degree-zero augmentation, relation map and matching maps are all locally surjective has zero homology sheaf in every positive degree.

theorem isZero_sheafHomology_of_isLocallySurjective_matchingMaps
    (J : GrothendieckTopology C) [HasSheafify J AddCommGrpCat.{w}]
    (K : SimplicialObject.Augmented (Cᵒᵖ ⥤ Type w))
    (h₀ : Presheaf.IsLocallySurjective J
      (K.hom.app (op (SimplexCategory.mk 0))))
    (h₁ : Presheaf.IsLocallySurjective J (edgesToFiberProduct K))
    (hmatching : ∀ n : ℕ, 1 ≤ n → Presheaf.IsLocallySurjective J
      (((SimplicialObject.coskAdj n).unit.app K.left).app
        (op (SimplexCategory.mk (n + 1)))))
    (i : ℕ) (hi : 0 < i) :
    IsZero (SimplicialObject.sheafHomology J K.left i)

CategoryTheory.SimplicialObject.Augmented.sheafHomologyZeroIso_of_isLocallySurjective_matchingMaps, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/AugmentedAcyclicity.lean, line 588. The attribute's comment: “degree-zero identification”.

Stacks Project, Tag 01GE (degree zero). The degree-zero homology sheaf of an augmented simplicial presheaf whose degree-zero augmentation, relation map and matching maps are all locally surjective is the free abelian sheaf on its presheaf of augmentation points.

noncomputable def sheafHomologyZeroIso_of_isLocallySurjective_matchingMaps
    (J : GrothendieckTopology C) [HasSheafify J AddCommGrpCat.{w}]
    (K : SimplicialObject.Augmented (Cᵒᵖ ⥤ Type w))
    (h₀ : Presheaf.IsLocallySurjective J
      (K.hom.app (op (SimplexCategory.mk 0))))
    (h₁ : Presheaf.IsLocallySurjective J (edgesToFiberProduct K))
    (hmatching : ∀ n : ℕ, 1 ≤ n → Presheaf.IsLocallySurjective J
      (((SimplicialObject.coskAdj n).unit.app K.left).app
        (op (SimplexCategory.mk (n + 1))))) :
    SimplicialObject.sheafHomology J K.left 0 ≅
      (Presheaf.freeAbelianSheaf J).obj K.right
Tag 01GF, a lemma

Tag 01GF in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.isZero_sheafHomology_of_isHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/ObjectAcyclicity.lean, line 90. The attribute's comment: “positive-degree vanishing”. References: SGA 4 V (7.3.2), “3) positive degrees”.

Stacks Project, Tag 01GF (positive degrees). The homology of the simplicial presheaf associated to a hypercovering vanishes in every positive degree.

theorem isZero_sheafHomology_of_isHypercovering (hK : IsHypercovering J K) (i : ℕ) (hi : 0 < i) :
    IsZero (SimplicialObject.sheafHomology J.toGrothendieck
      (SectionsOver.associatedSimplicialPresheaf.{w} K) i)

Stacks.CategoryTheory.Hypercovering.sheafHomologyZeroIso_of_isHypercovering, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/ObjectAcyclicity.lean, line 100. The attribute's comment: “degree-zero identification”. References: SGA 4 V (7.3.2), “3) degree zero”.

Stacks Project, Tag 01GF (degree zero). The degree-zero homology of the simplicial presheaf associated to a hypercovering is the free abelian sheaf on the represented object.

noncomputable def sheafHomologyZeroIso_of_isHypercovering (hK : IsHypercovering J K) :
    SimplicialObject.sheafHomology J.toGrothendieck
        (SectionsOver.associatedSimplicialPresheaf.{w} K) 0 ≅
      (presheafToSheaf J.toGrothendieck AddCommGrpCat.{max u v w}).obj
        (uliftYoneda.{max u w}.obj X ⋙ AddCommGrpCat.free.{max u v w})
Sources
LeanCategoryTheory.SimplicialObject.sheafHomology · CategoryTheory.Presheaf.isZero_sheafHomology_cechNerve_of_isLocallySurjective · CategoryTheory.Presheaf.isIso_cechNerveSheafHomologyZeroAugmentation · CategoryTheory.SimplicialObject.isIso_sheafHomologyFunctor_map_of_coskeletal · CategoryTheory.SimplicialObject.Augmented.isZero_sheafHomology_of_isLocallySurjective_matchingMaps · CategoryTheory.SimplicialObject.Augmented.sheafHomologyZeroIso_of_isLocallySurjective_matchingMaps · Stacks.CategoryTheory.Hypercovering.isZero_sheafHomology_of_isHypercovering · Stacks.CategoryTheory.Hypercovering.sheafHomologyZeroIso_of_isHypercovering

Section25.5 Čech cohomology and hypercoverings#

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

Tag 01GV, a lemma

Tag 01GV in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.nonempty_zerothCechCohomologyIsoSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/ObjectCohomology.lean, line 153. The attribute's comment: “some isomorphism Ȟ⁰(K, 𝓕) ≅ 𝓕(X) exists”.

Stacks Project, Tag 01GV, the existence half. Degree-zero Čech cohomology of a hypercovering is isomorphic to the group of sections of the coefficient sheaf on the covered object.

This asserts only that some isomorphism exists. The canonical one, inverse to the map induced by the augmentation of the Čech complex and natural in the sheaf, is zerothCechCohomologyIsoSections.

theorem nonempty_zerothCechCohomologyIsoSections (J : Pretopology C) {X : C}
    (K : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (hK : IsHypercovering J K)
    (F : Sheaf J.toGrothendieck AddCommGrpCat.{max u v w}) :
    Nonempty ((SectionsOver.sectionsComplex J.toGrothendieck K F).homology 0 ≅
      F.obj.obj (op X))

Stacks.CategoryTheory.Hypercovering.zerothCechCohomologyFunctorIsoSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/ObjectCohomologyZeroNatural.lean, line 126. The attribute's comment: “the identification Ȟ⁰(K, 𝓕) = 𝓕(X), as functors on Ab(C)”.

For a hypercovering K of X the degree-zero Čech cohomology Ȟ⁰(K, -) is the functor of sections on X, as an isomorphism of functors on the abelian sheaves, inverse to the canonical map induced by the augmentation of the Čech complex by the sections on X.

noncomputable def zerothCechCohomologyFunctorIsoSections (hK : IsHypercovering J K) :
    SectionsOver.sectionsComplexFunctor J.toGrothendieck K ⋙
        HomologicalComplex.homologyFunctor AddCommGrpCat.{max u v w} (ComplexShape.up ℕ) 0 ≅
      sheafToPresheaf J.toGrothendieck AddCommGrpCat.{max u v w} ⋙
        (evaluation Cᵒᵖ AddCommGrpCat.{max u v w}).obj (op X)

Stacks.CategoryTheory.Hypercovering.zerothCechCohomologyIsoSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/ObjectCohomologyZeroNatural.lean, line 145. The attribute's comment: “the identification Ȟ⁰(K, 𝓕) = 𝓕(X)”.

For a hypercovering K of X and an abelian sheaf F, the degree-zero Čech cohomology Ȟ⁰(K, F) is the group F(X) of sections on X: the component at F of zerothCechCohomologyFunctorIsoSections.

noncomputable def zerothCechCohomologyIsoSections (hK : IsHypercovering J K)
    (F : Sheaf J.toGrothendieck AddCommGrpCat.{max u v w}) :
    (SectionsOver.sectionsComplex J.toGrothendieck K F).homology 0 ≅ F.obj.obj (op X)

Stacks.CategoryTheory.Hypercovering.isIso_kernelLift_terminalAugZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/TerminalAugmentationCohomologyZero.lean, line 392. The attribute's comment: “degree zero, as a kernel of the first differential of the Čech complex”.

[Stacks, Tag 01GV] in degree zero, in canonical-map form. For a hypercovering K of an object X of a site and an arbitrary abelian sheaf F, the canonical augmentation F(X) ⟶ ∏_{i ∈ K₀} F(K₀(i)) of the Čech complex of K exhibits F(X) as the kernel of the first differential.

No injectivity of F is assumed: the input CategoryTheory.SimplicialObject.Augmented.isIso_kernelLift_freeAbelianSheafAugZero needs only conditions (1) and (2) of a hypercovering, which Stacks.CategoryTheory.Hypercovering.isLocallySurjective_of_isHypercovering supplies.

The terminal object of Over X at which the augmentation is formed is arbitrary; the proof transports it to Over.mk (𝟙 X) by terminalAugZero_eq_comp_of_isTerminal.

theorem isIso_kernelLift_terminalAugZero (J : Pretopology C) {X : C}
    (K : SimplicialObject (Limits.FormalCoproduct.{w} (Over X)))
    (hK : IsHypercovering J K) {T : Over X} (hT : IsTerminal T)
    (F : Sheaf J.toGrothendieck AddCommGrpCat.{max u v w}) :
    IsIso (kernel.lift ((SectionsOver.sectionsComplex J.toGrothendieck K F).d 0 1)
      (terminalAugZero K hT
        (((Functor.whiskeringLeft (Over X)ᵒᵖ Cᵒᵖ AddCommGrpCat.{max u v w}).obj
          (Over.forget X).op).obj
          ((sheafToPresheaf J.toGrothendieck AddCommGrpCat.{max u v w}).obj F)))
      (terminalAugZero_comp_d K hT
        (((Functor.whiskeringLeft (Over X)ᵒᵖ Cᵒᵖ AddCommGrpCat.{max u v w}).obj
          (Over.forget X).op).obj
          ((sheafToPresheaf J.toGrothendieck AddCommGrpCat.{max u v w}).obj F))))
Tag 01GW, a lemma

Tag 01GW in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.cechCohomologyOver_isZero_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/ObjectCohomology.lean, line 197. The attribute's comment: “positive degrees”.

Stacks Project, Tag 01GW (positive degrees). The positive-degree Čech cohomology of an injective abelian sheaf on a hypercovering vanishes.

Sheafification, which the statement does not need, is supplied inside the proof from hasSheafify_addCommGrpCat.

theorem cechCohomologyOver_isZero_of_injective (J : Pretopology C) {X : C}
    (K : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (hK : IsHypercovering J K)
    (I : Sheaf J.toGrothendieck AddCommGrpCat.{max u v w}) [Injective I]
    (p : ℕ) (hp : 0 < p) :
    IsZero ((SectionsOver.sectionsComplex J.toGrothendieck K I).homology p)

Stacks.CategoryTheory.Hypercovering.cechCohomologyOverIsoOfInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/ObjectCohomologyZeroNatural.lean, line 154.

For a hypercovering K of X and an injective abelian sheaf I, the Čech cohomology Ȟᵖ(K, I) is the group I(X) of sections on X when p = 0 and is zero when p > 0.

noncomputable def cechCohomologyOverIsoOfInjective (hK : IsHypercovering J K)
    (I : Sheaf J.toGrothendieck AddCommGrpCat.{max u v w}) [Injective I] (p : ℕ) :
    (SectionsOver.sectionsComplex J.toGrothendieck K I).homology p ≅
      if p = 0 then I.obj.obj (op X) else 0
Tag 01GX, an equation

Tag 01GX in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.SemiRepresentable.sectionsComplexIsoHomFreeAbelianSheafComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/SectionsComplex.lean, line 670. The attribute's comment: “arbitrary semi-representable simplicial object”.

Stacks Project, Tag 01GX. The cochain complex of sections on any simplicial semi-representable presheaf is canonically the Hom complex from its complex of free abelian sheaves.

noncomputable def sectionsComplexIsoHomFreeAbelianSheafComplex
    (J : GrothendieckTopology C)
    [HasSheafify J AddCommGrpCat.{max (max u v) (max q w)}]
    (K : SimplicialObject (FormalCoproduct.{w} C))
    (F : Sheaf J AddCommGrpCat.{max (max u v) (max q w)}) :
    sectionsComplex.{q, w, v, u} J K F ≅
      homFreeAbelianSheafComplex.{q, w, v, u} J K F

Stacks.CategoryTheory.Hypercovering.SectionsOver.sectionsComplexIsoHomFreeAbelianSheafComplex, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/SectionsComplexOver.lean, line 551. The attribute's comment: “formal coproducts over an object”.

The complex obtained by evaluating an abelian sheaf F on a simplicial semi-representable object K is isomorphic to the complex of morphisms from the associated complex of free abelian sheaves into F.

noncomputable def sectionsComplexIsoHomFreeAbelianSheafComplex {X : C}
    (J : GrothendieckTopology C) [HasSheafify J AddCommGrpCat.{max u v w}]
    (K : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (F : Sheaf J AddCommGrpCat.{max u v w}) :
    sectionsComplex J K F ≅ homFreeAbelianSheafComplex J K F
Tag 01GY, a lemma

Tag 01GY in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.exists_hypercoverToDerivedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CohomologyComparison.lean, line 120. The attribute's comment: “the comparison map s(F(K)) ⟶ RΓ(X, F) in D⁺(Ab), functorial in F”.

Stacks Project, Tag 01GY. For a hypercovering K of an object X of a site with fibre products there are a canonical map ψ from the sections on X to derived sections at the single complex, and a map

α : s(-(K)) ⟶ RΓ(X, -)

in D⁺(Ab), functorial in the abelian sheaf, compatible with the augmentation of s(-(K)) by the sections on X; and both are isomorphisms at every injective sheaf.

The last clause is what makes the statement non-vacuous: by StacksDraft.DerivedSectionsComparison.isZero_of_pin_zero, α = 0 would force Q(s(I(K))) to be a zero object for every injective I.

theorem exists_hypercoverToDerivedSections (hK : IsHypercovering J K) :
    ∃ (ψ : (sheafSectionsFunctor.{w} J X ⋙ singlePlus AddCommGrpCat.{max u v w}) ⋙
          DerivedCategory.Plus.Q ⟶ derivedSectionsFunctor.{w} J X)
      (α : hypercoverDerivedFunctor.{w} J X K ⟶ derivedSectionsFunctor.{w} J X),
      Functor.whiskerRight
            (epsNat (sheafSectionsFunctor.{w} J X) (hypercoverCochainIntFunctor.{w} J X K)
              (sectionsEps.{w} J X K)
              (fun {_ _} φ ↦ sectionsEps_naturality.{w} J X K φ)
              (isZero_hypercoverCochainIntFunctor_obj_X.{w} J X K))
            DerivedCategory.Plus.Q ≫ α = ψ ∧
        (∀ F : Sheaf J.toGrothendieck AddCommGrpCat.{max u v w}, Injective F → IsIso (ψ.app F)) ∧
        ∀ F : Sheaf J.toGrothendieck AddCommGrpCat.{max u v w}, Injective F → IsIso (α.app F)

Stacks.CategoryTheory.Hypercovering.exists_cechCohomologyToSheafCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CohomologyComparison.lean, line 166. The attribute's comment: “the induced natural transformations Ȟ^i(K, -) ⟶ H^i(X, -)”.

Stacks Project, Tag 01GY. The comparison map of exists_hypercoverToDerivedSections induces, in every degree i, a natural transformation

Ȟ^i(K, -) ⟶ H^i(X, -)

of functors from abelian sheaves to abelian groups, and these are isomorphisms at every injective sheaf.

The source is the i-th cohomology of the complex s(-(K)) itself, i.e. the Čech cohomology of the hypercovering, and the target is the i-th cohomology of RΓ(X, -), i.e. sheaf cohomology on X. The invertibility at injectives is again what rules out the zero transformation.

theorem exists_cechCohomologyToSheafCohomology (hK : IsHypercovering J K) :
    ∃ β : ∀ i : ℤ,
        (hypercoverCochainIntFunctor.{w} J X K ⋙
            HomologicalComplex.homologyFunctor AddCommGrpCat.{max u v w}
              (ComplexShape.up ℤ) i) ⟶
          (derivedSectionsFunctor.{w} J X ⋙
            DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{max u v w} i),
      ∀ (i : ℤ) (F : Sheaf J.toGrothendieck AddCommGrpCat.{max u v w}),
        Injective F → IsIso ((β i).app F)

Stacks.CategoryTheory.Hypercovering.hypercoverComparisonMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/DerivedComparisonBoundedBelow.lean, line 546. The attribute's comment: “comparison_map”.

The comparison map of Stacks 01GY: for a hypercovering K of X, the natural transformation s(F(K)) ⟶ RΓ(X, F) in D⁺(Ab).

It is s(F(K)) ≅ Θ(F[0]) ⟶ RΘ(F[0]) ≅ RΓ(X, F): the identification of s(F(K)) with the hypercover total complex of F[0], the unit of the right derived functor of Θ, and the inverse of the comparison RΓ(X, -) ⟶ RΘ induced by the augmentation. It is pinned down by hypercoverAugDerivedSections_comp_hypercoverComparisonMap.

def hypercoverComparisonMap (hK : IsHypercovering J K) :
    hypercoverDerivedFunctor J U K ⟶ derivedSectionsFunctor J U

Stacks.CategoryTheory.Hypercovering.hypercoverCohomologyComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/DerivedComparisonBoundedBelow.lean, line 585. The attribute's comment: “cohomology_comparison”.

The natural map from the Čech cohomology of a hypercovering K of X to sheaf cohomology in degree i, induced by the comparison map hypercoverComparisonMap.

def hypercoverCohomologyComparison (hK : IsHypercovering J K) (i : ℤ) :
    (hypercoverDerivedFunctor J U K ⋙ homologyFunctor AddCommGrpCat.{max u v w} i) ⟶
      (derivedSectionsFunctor J U ⋙ homologyFunctor AddCommGrpCat.{max u v w} i)

Stacks.CategoryTheory.Hypercovering.hypercoverSpectralSequenceHypercoveringFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/SpectralSequence/Assembled.lean, line 284. The attribute's comment: “spectral sequence functorial in the hypercovering”.

The spectral sequence of [Stacks, Tag 01GY] is functorial in the hypercovering, which is the last sentence of its third clause: the assignment taking a simplicial semi-representable object K over X to the functorial spectral sequence hypercoverSpectralSequenceFunctor J X K of HypercoveringSpectralSequenceData.sequence is a functor on the opposite category, contravariance being the direction in which a morphism of hypercoverings acts on Čech cochains.

Morphisms are taken to be all morphisms of simplicial semi-representable objects over X, which is more than the source asks for: a morphism of hypercoverings is in particular one of these, the hypercovering conditions being conditions on an object and not on a morphism.

def hypercoverSpectralSequenceHypercoveringFunctor :
    (SimplicialObject (FormalCoproduct.{w} (Over X)))ᵒᵖ ⥤
      (Sheaf J.toGrothendieck AddCommGrpCat.{max u v w} ⥤
        E₂CohomologicalSpectralSequenceNat AddCommGrpCat.{max u v w})

Stacks.CategoryTheory.Hypercovering.hypercoveringSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/SpectralSequence/Assembled.lean, line 339. The attribute's comment: “spectral sequence”.

The functorial spectral sequence of a hypercovering, with second page Ȟ^p(K, H̲^q(F)) and abutment H^{p+q}(X, F).

This is the third clause of [Stacks, Tag 01GY]: the four fields are CategoryTheory.Sheaf.enoughInjectives_addCommGrpCat, hypercoverSpectralSequenceFunctor, hypercoverPageTwoIso and hypercoverAbutment. The functoriality of this spectral sequence in the hypercovering, which is the last sentence of that clause, is hypercoverSpectralSequenceHypercoveringFunctor, whose value at K is the sequence field below.

def hypercoveringSpectralSequence (hK : IsHypercovering J K) :
    HypercoveringSpectralSequenceData.{w} J X K hK

Stacks.CategoryTheory.Hypercovering.Functorial.hypercoveringCohomologyAbutment, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/SpectralSequenceAbutmentIsCohomology.lean, line 941. The attribute's comment: “spectral_sequence”. References: SGA 4 V (7.4.0), “(7.4.0.3) abutment”.

Clause (3) of [Stacks, Tag 01GY], the functorial abutment: the hypercovering spectral sequence abuts to H^{p+q}(X, F), functorially in the hypercovering and in the coefficient sheaf.

hypercoveringFunctorialAbutment with the cohomology of the total complex replaced by sheaf cohomology through hypercoverAbutmentNatIso; Stacks.Cohomology.Leray.FunctorialFirstQuadrantAbutsTo.ofIsoAbutment touches no other field -- the structure mentions the asserted abutment in abutmentIso alone.

def hypercoveringCohomologyAbutment :
    _root_.Stacks.Cohomology.Leray.FunctorialFirstQuadrantAbutsTo
      (hypercoveringSpectralSequence X J)
      (fun n ↦ hypercoveringCohomologyFunctor X J n)

Stacks.CategoryTheory.Hypercovering.Functorial.hypercoveringPageTwoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/SpectralSequenceSecondPage.lean, line 642. The attribute's comment: “spectral_sequence”. References: SGA 4 V (7.4.0), “(7.4.0.3) E₂ page”; SGA 4 Vbis (2.5.6), “E_2 term”.

The pageTwoIso of clause (3) of [Stacks, Tag 01GY]: the second page of Stacks.CategoryTheory.Hypercovering.Functorial.hypercoveringSpectralSequence at (p, q) is Ȟ^p(K, H^q(F)), naturally in the hypercovering and in the coefficient sheaf simultaneously. It is hypercoverPageTwoIso restricted along the inclusion of the full subcategory of hypercoverings, since nothing in the second-page identification uses the hypercovering condition -- that is needed only for the abutment.

The source is written as the whiskering rather than as Stacks.CategoryTheory.Hypercovering.Functorial.hypercoveringSpectralSequence composed with the page functor. The two are the same functor -- hypercoveringSpectralSequence is that whiskering, and composition of functors is associative definitionally -- but checking that at the ambient heartbeat budget means unfolding CategoryTheory.SpectralSequence.natRestrictE₂Comp inside a functor-level defeq, which does not finish.

def hypercoveringPageTwoIso (p q : ℕ) :
    (ObjectProperty.ι (fun K : SimplicialObject (Limits.FormalCoproduct.{v} (Over X)) =>
            IsHypercovering J K)).op.prod
          (𝟭 (Sheaf J.toGrothendieck AddCommGrpCat.{v})) ⋙
        hypercoverSpectralSequenceFunctor X J.toGrothendieck ⋙
          CategoryTheory.SpectralSequence.pageFunctor _ _ 2 2 ⋙
            HomologicalComplex.eval _ _ (p, q) ≅
      pageTwoHypercovering.{v} X J p q

Stacks.CategoryTheory.Hypercovering.Functorial.hypercoveringSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/SpectralSequenceSmallSite.lean, line 395. The attribute's comment: “spectral_sequence”. References: SGA 4 V (7.4.0), “(7.4.0.3)”.

The sequence of clause (3) of [Stacks, Tag 01GY]: the first-quadrant E₂ cohomological spectral sequence of a hypercovering of X and a sheaf of abelian groups, functorial in the hypercovering (contravariantly) and in the sheaf. It is the restriction of hypercoverSpectralSequenceFunctor along the inclusion of the full subcategory of hypercoverings, since nothing in the construction of the sequence itself uses the hypercovering condition -- that is needed only for the abutment, which is not here.

def hypercoveringSpectralSequence :
    (HypercoveringCat X J)ᵒᵖ × Sheaf J.toGrothendieck AddCommGrpCat.{v} ⥤
      E₂CohomologicalSpectralSequenceNat AddCommGrpCat.{v}
Sources
LeanStacks.CategoryTheory.Hypercovering.nonempty_zerothCechCohomologyIsoSections · Stacks.CategoryTheory.Hypercovering.zerothCechCohomologyFunctorIsoSections · Stacks.CategoryTheory.Hypercovering.zerothCechCohomologyIsoSections · Stacks.CategoryTheory.Hypercovering.isIso_kernelLift_terminalAugZero · Stacks.CategoryTheory.Hypercovering.cechCohomologyOver_isZero_of_injective · Stacks.CategoryTheory.Hypercovering.cechCohomologyOverIsoOfInjective · Stacks.CategoryTheory.Hypercovering.SemiRepresentable.sectionsComplexIsoHomFreeAbelianSheafComplex · Stacks.CategoryTheory.Hypercovering.SectionsOver.sectionsComplexIsoHomFreeAbelianSheafComplex

Section25.6 Hypercoverings a la Verdier#

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

Tag 09VU, a definition

Tag 09VU in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.HypercoveringOf, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Presheaf.lean, line 201. The attribute's comment: “hypercovering of a presheaf”. References: SGA 4 V (7.3.1.2); SGA 4 V (7.3.1.3), “a)”.

A hypercovering of a presheaf of sets.

structure HypercoveringOf (J : Pretopology C) (G : Cᵒᵖ ⥤ Type q)

Stacks.CategoryTheory.Hypercovering.HypercoveringOfTerminal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Presheaf.lean, line 226. The attribute's comment: “hypercovering of the final presheaf”. References: SGA 4 V (7.3.1.2); SGA 4 V (7.3.1.3), “a)”.

A hypercovering is a hypercovering of the final presheaf.

abbrev HypercoveringOfTerminal (J : Pretopology C)
Tag 09VV, a lemma

Tag 09VV in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.nonempty_cechCohomologyZeroIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Cohomology.lean, line 527.

Stacks Project, Tag 09VV. Degree-zero Čech cohomology of a hypercovering of a presheaf is the degree-zero cohomology of that presheaf with coefficients in the given sheaf of abelian groups.

The source asserts an identification; the isomorphism realising it is cechCohomologyZeroIso, of which this is the existence statement.

theorem nonempty_cechCohomologyZeroIso (J : Pretopology C)
    (G : Functor Cᵒᵖ (Type q)) (K : HypercoveringOf.{q, w} J G)
    (F : Sheaf J.toGrothendieck AddCommGrpCat.{max (max u v) (max q w)}) :
    Nonempty (cechCohomology J G K F 0 ≅ presheafCohomologyZero J G F)
Tag 09VW, a lemma

Tag 09VW in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.cechCohomology_isZero_of_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Injectives.lean, line 362. The attribute's comment: “positive degrees”.

Stacks Project, Tag 09VW (positive degrees). Positive-degree Čech cohomology of an injective abelian sheaf on a hypercovering of a presheaf vanishes.

theorem cechCohomology_isZero_of_injective (J : Pretopology C)
    (G : Cᵒᵖ ⥤ Type q) (K : HypercoveringOf.{q, w} J G)
    (I : Sheaf J.toGrothendieck AddCommGrpCat.{max (max u v) (max q w)})
    [Injective I] (p : ℕ) (hp : 0 < p) :
    IsZero (cechCohomology.{q, w, v, u} J G K I p)

Stacks.CategoryTheory.Hypercovering.cechCohomologyIsoOfInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Injectives.lean, line 423.

Stacks Project, Tag 09VW. For a hypercovering K of a presheaf G and an injective abelian sheaf I, the Čech cohomology Ȟᵖ(K, I) is the degree-zero cohomology H⁰(G, I) of G when p = 0 and is zero when p > 0.

The degree-zero branch is Tag 09VV's cechCohomologyZeroIso, which holds for every abelian sheaf and needs no injectivity; the positive-degree branch is cechCohomology_isZero_of_injective.

noncomputable def cechCohomologyIsoOfInjective (J : Pretopology C)
    (G : Cᵒᵖ ⥤ Type q) (K : HypercoveringOf.{q, w} J G)
    (I : Sheaf J.toGrothendieck AddCommGrpCat.{max (max u v) (max q w)})
    [Injective I] (p : ℕ) :
    cechCohomology.{q, w, v, u} J G K I p ≅
      if p = 0 then presheafCohomologyZero.{q, w, v, u} J G I else 0
Tag 09VX, a lemma

Tag 09VX in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.exists_hypercoverPresheafToDerivedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/PresheafCohomologyComparison.lean, line 162. The attribute's comment: “the comparison map s(F(K)) ⟶ RΓ(G, F) in D⁺(Ab), functorial in F”.

For a hypercovering K of a presheaf G on a site with equalizers and fibre products there are a canonical map ψ from the sections over G to derived sections at the single complex, and a map

α : s(-(K)) ⟶ RΓ(G, -)

in D⁺(Ab), functorial in the abelian sheaf, compatible with the augmentation of s(-(K)) by the sections over G; and both are isomorphisms at every injective sheaf.

theorem exists_hypercoverPresheafToDerivedSections :
    ∃ (ψ : (presheafSectionsFunctor.{q, w, v, u} J G K ⋙
          singlePlus AddCommGrpCat.{max (max u v) (max q w)}) ⋙ DerivedCategory.Plus.Q ⟶
        presheafDerivedSectionsFunctor.{q, w, v, u} J G K)
      (α : hypercoverPresheafDerivedFunctor.{q, w, v, u} J G K ⟶
        presheafDerivedSectionsFunctor.{q, w, v, u} J G K),
      Functor.whiskerRight
            (epsNat (presheafSectionsFunctor.{q, w, v, u} J G K)
              (SemiRepresentable.sectionsComplexIntFunctor.{q, w, v, u} J.toGrothendieck
                K.toSimplicialObject)
              ((hypercoverPresheafAugmentation.{q, w, v, u} J G K).app)
              (fun {_ _} φ ↦ (hypercoverPresheafAugmentation.{q, w, v, u} J G K).naturality φ)
              (SemiRepresentable.isZero_sectionsComplexIntFunctor_obj_X.{q, w, v, u}
                J.toGrothendieck K.toSimplicialObject))
            DerivedCategory.Plus.Q ≫ α = ψ ∧
        (∀ F : Sheaf J.toGrothendieck AddCommGrpCat.{max (max u v) (max q w)},
          Injective F → IsIso (ψ.app F)) ∧
        ∀ F : Sheaf J.toGrothendieck AddCommGrpCat.{max (max u v) (max q w)},
          Injective F → IsIso (α.app F)

Stacks.CategoryTheory.Hypercovering.exists_presheafCechCohomologyToCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/PresheafCohomologyComparison.lean, line 220. The attribute's comment: “the induced natural transformations Ȟ^i(K, -) ⟶ H^i(G, -)”.

The comparison map of exists_hypercoverPresheafToDerivedSections induces, in every degree i, a natural transformation

Ȟ^i(K, -) ⟶ H^i(G, -)

of functors from abelian sheaves to abelian groups, and these are isomorphisms at every injective sheaf.

The source is the i-th cohomology of the complex s(-(K)) itself, i.e. the Čech cohomology of the hypercovering, and the target is the i-th cohomology of RΓ(G, -).

theorem exists_presheafCechCohomologyToCohomology :
    ∃ β : ∀ i : ℤ,
        (SemiRepresentable.sectionsComplexIntFunctor.{q, w, v, u} J.toGrothendieck
              K.toSimplicialObject ⋙
            HomologicalComplex.homologyFunctor AddCommGrpCat.{max (max u v) (max q w)}
              (ComplexShape.up ℤ) i) ⟶
          (presheafDerivedSectionsFunctor.{q, w, v, u} J G K ⋙
            DerivedCategory.Plus.homologyFunctor
              AddCommGrpCat.{max (max u v) (max q w)} i),
      ∀ (i : ℤ) (F : Sheaf J.toGrothendieck AddCommGrpCat.{max (max u v) (max q w)}),
        Injective F → IsIso ((β i).app F)

Stacks.CategoryTheory.Hypercovering.presheafHypercoveringSpectralSequenceFunctoriality, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/PresheafSpectralSequence/Functoriality.lean, line 280. The attribute's comment: “spectral sequence functorial in the hypercovering”.

The spectral sequence of [Stacks, Tag 09VX] is functorial in the hypercovering: the data PresheafHypercoveringSpectralSequenceFunctoriality, supplied by hypercoverPresheafSpectralSequenceFunctorMap and its two laws.

def presheafHypercoveringSpectralSequenceFunctoriality :
    PresheafHypercoveringSpectralSequenceFunctoriality.{q, w, v, u} J G

Stacks.CategoryTheory.Hypercovering.presheafHypercoveringSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/PresheafSpectralSequence/Functoriality.lean, line 332. The attribute's comment: “spectral sequence”. References: SGA 4 V (7.4.0), “(7.4.0.3)”.

The functorial spectral sequence of a hypercovering of a presheaf, with second page Ȟ^p(K, H̲^{q'}(F)) and abutment H^{p+q'}(G, F).

This is the spectral sequence clause of [Stacks, Tag 09VX]: the three fields are hypercoverPresheafSpectralSequenceFunctor, hypercoverPresheafPageTwoIso and hypercoverPresheafAbutment. The functoriality of this spectral sequence in the hypercovering, which is the last sentence of that clause, is presheafHypercoveringSpectralSequenceFunctoriality, whose map is a morphism between the sequence fields of two hypercoverings.

def presheafHypercoveringSpectralSequence :
    PresheafHypercoveringSpectralSequenceData J G K
Tag 09VY, a lemma

Tag 09VY in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.hypercoveringGlobalSpectralSequence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/GlobalCohomologySpectralSequence.lean, line 245. References: SGA 4 V (7.4.0), “(7.4.0.3)”; SGA 4 V (3.6), “more general”.

Stacks Project, Tag 09VY. For a hypercovering K of the final presheaf on a site with equalizers and fibre products there is a spectral sequence, functorial in the sheaf of abelian groups F, with second page E_2^{p,q} = Ȟ^p(K, H̲^q(F)) converging to the global cohomology groups H^{p+q}(F).

It is [Stacks, Tag 09VX] at the final presheaf, with its abutment transported along globalCohomologyAbutmentIso.

def hypercoveringGlobalSpectralSequence :
    HypercoveringGlobalSpectralSequenceData J K
Sources
LeanStacks.CategoryTheory.Hypercovering.HypercoveringOf · Stacks.CategoryTheory.Hypercovering.HypercoveringOfTerminal · Stacks.CategoryTheory.Hypercovering.nonempty_cechCohomologyZeroIso · Stacks.CategoryTheory.Hypercovering.cechCohomology_isZero_of_injective · Stacks.CategoryTheory.Hypercovering.cechCohomologyIsoOfInjective · Stacks.CategoryTheory.Hypercovering.exists_hypercoverPresheafToDerivedSections · Stacks.CategoryTheory.Hypercovering.exists_presheafCechCohomologyToCohomology · Stacks.CategoryTheory.Hypercovering.presheafHypercoveringSpectralSequenceFunctoriality

Section25.7 Covering hypercoverings#

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

Tag 01GH, a lemma

Tag 01GH in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.isHypercovering_fibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CoveringAndHomotopies/FibreProduct.lean, line 270.

A fibre product with a hypercovering is a hypercovering when the other morphism is covering in degree zero and on every relative matching object.

theorem isHypercovering_fibreProduct (J : Pretopology C)
    [Precoverage.IsStableUnderComposition J.toPrecoverage] {X : C}
    {K L M : SimplicialObject (FormalCoproduct.{w} (Over X))} (a : K ⟶ L) (b : M ⟶ L)
    (hK : IsHypercovering J K)
    (h₀ : IsCoveringOver J (b.app (op ⦋0⦌)))
    (hmatching : ∀ n : ℕ, IsCoveringOver J
      (Limits.pullback.lift
        (f := (((SimplicialObject.coskAdj n).unit.app L).app (op ⦋n + 1⦌)))
        (g := (((SimplicialObject.Truncated.cosk n).map
          ((SimplicialObject.truncation n).map b)).app (op ⦋n + 1⦌)))
        (b.app (op ⦋n + 1⦌))
        (((SimplicialObject.coskAdj n).unit.app M).app (op ⦋n + 1⦌))
        (NatTrans.congr_app ((SimplicialObject.coskAdj n).unit.naturality b)
          (op ⦋n + 1⦌)))) :
    IsHypercovering J (SimplicialObject.fibreProduct a b)
Tag 01GI, a lemma

Tag 01GI in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.IsHypercovering.prod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CoveringAndHomotopies/Product.lean, line 169.

Stacks Project, Tag 01GI. The product of two hypercoverings of an object of a site with fibre products is a hypercovering.

theorem IsHypercovering.prod (J : Pretopology C)
    [Precoverage.IsStableUnderComposition J.toPrecoverage] {X : C}
    {K L : SimplicialObject (FormalCoproduct.{w} (Over X))}
    (hK : IsHypercovering J K) (hL : IsHypercovering J L) :
    IsHypercovering J (K ⨯ L)
Tag 01GJ, a lemma

Tag 01GJ in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.exists_hypercovering_map_factoring_through_covering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Refinement/FactoringThroughCovering.lean, line 289. References: SGA 4 V (7.3.2), “2)”.

Stacks Project, Tag 01GJ. A covering of the term in any fixed degree of a hypercovering can be refined by a morphism from another hypercovering, whose component in that degree factors through the covering.

public theorem exists_hypercovering_map_factoring_through_covering
    (J : Pretopology C) [Precoverage.IsStableUnderComposition J.toPrecoverage] {X : C}
    (K : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (hK : IsHypercovering J K) (k : ℕ)
    {Z : FormalCoproduct.{w} (Over X)}
    (u : Z ⟶ K.obj (Opposite.op (SimplexCategory.mk k)))
    (hu : IsCoveringOver J u) :
    ∃ (L : SimplicialObject (FormalCoproduct.{w} (Over X))),
      IsHypercovering J L ∧
        ∃ (f : L ⟶ K) (g : L.obj (Opposite.op (SimplexCategory.mk k)) ⟶ Z),
          g ≫ u = f.app (Opposite.op (SimplexCategory.mk k))
Tag 0B16, an equation

Tag 0B16 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.power_cosk_unit_isProjection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/ConstantPowerMatching.lean, line 599.

The (n + 1)-st matching map of Hom(C[k], T) is, functorially in T, a projection of finite powers of T.

public theorem power_cosk_unit_isProjection
    {D : Type u} [Category.{v} D] [HasFiniteLimits D]
    (k n : ℕ) (hn : 0 < n) :
    letI : ∀ F : SimplicialObject.Truncated D n,
        (SimplexCategory.Truncated.inclusion n).op.HasPointwiseRightKanExtension F :=
      fun F =>
        (hasPointwiseRightKanExtension_of_hasBinaryProducts_or_hasFiniteConnectedLimits
            (C := D)).2 (fun _ => inferInstance) n hn F;
    letI : ∀ m : SimplexCategoryᵒᵖ,
        Fintype ((uliftCoyoneda.{w}.obj (op ⦋k⦌)).obj m.unop) :=
      fun m => by
        rw [CosimplicialObject.uliftCoyoneda_spec.1 ⦋k⦌ m.unop]
        exact Fintype.ofFinite _;
    ∃ S : Finset ((uliftCoyoneda.{w}.obj (op ⦋k⦌)).obj ⦋n + 1⦌),
      ∃ e : ∀ T : D,
          (((SimplicialObject.cosk n).obj
            (((SimplicialObject.const D).obj T).power
              (uliftCoyoneda.{w}.obj (op ⦋k⦌)))).obj (op ⦋n + 1⦌)) ≅
            ∏ᶜ fun _ : ↥S => T,
        (∀ T : D,
          (((SimplicialObject.coskAdj n).unit.app
            (((SimplicialObject.const D).obj T).power
              (uliftCoyoneda.{w}.obj (op ⦋k⦌)))).app
              (op ⦋n + 1⦌)) ≫ (e T).hom =
            eqToHom (SimplicialObject.power_obj
              ((SimplicialObject.const D).obj T)
              (uliftCoyoneda.{w}.obj (op ⦋k⦌)) (op ⦋n + 1⦌)) ≫
              Limits.Pi.map' (fun s : ↥S => (s : _)) (fun _ => 𝟙 T)) ∧
        (∀ (T T' : D) (f : T ⟶ T')
          (g : (((SimplicialObject.const D).obj T).power
              (uliftCoyoneda.{w}.obj (op ⦋k⦌))) ⟶
            (((SimplicialObject.const D).obj T').power
              (uliftCoyoneda.{w}.obj (op ⦋k⦌)))),
          (∀ m : SimplexCategoryᵒᵖ,
            g.app m = Limits.Pi.map (fun _ => f)) →
          (((SimplicialObject.cosk n).map g).app (op ⦋n + 1⦌)) ≫ (e T').hom =
            (e T).hom ≫ Limits.Pi.map (fun _ : ↥S => f))
Tag 01GK, a lemma

Tag 01GK in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.exists_hypercovering_map_factoring_through_locallySurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/LocallySurjectiveRefinement.lean, line 224. References: SGA 4 V (7.3.2), “2)”.

Stacks Project, Tag 01GK. A locally surjective map onto the presheaf represented by one term of a hypercovering can be factored through after refining the hypercovering.

public theorem exists_hypercovering_map_factoring_through_locallySurjective
    (J : Pretopology C) [Precoverage.IsStableUnderComposition J.toPrecoverage] {X : C}
    (K : SimplicialObject (FormalCoproduct.{max u v w} (Over X)))
    (hK : IsHypercovering J K) (n : ℕ)
    (F : Cᵒᵖ ⥤ Type (max u v w))
    (u : F ⟶ (associatedPresheafFunctorOver (X := X)).obj
      (K.obj (Opposite.op (SimplexCategory.mk n))))
    [Presheaf.IsLocallySurjective J.toGrothendieck u] :
    ∃ (L : SimplicialObject (FormalCoproduct.{max u v w} (Over X))),
      IsHypercovering J L ∧
        ∃ (f : L ⟶ K)
          (g : (associatedPresheafFunctorOver (X := X)).obj
            (L.obj (Opposite.op (SimplexCategory.mk n))) ⟶ F),
            g ≫ u = (associatedPresheafFunctorOver (X := X)).map
              (f.app (Opposite.op (SimplexCategory.mk n)))
Sources
LeanStacks.CategoryTheory.Hypercovering.isHypercovering_fibreProduct · Stacks.CategoryTheory.Hypercovering.IsHypercovering.prod · Stacks.CategoryTheory.Hypercovering.exists_hypercovering_map_factoring_through_covering · Stacks.CategoryTheory.Hypercovering.power_cosk_unit_isProjection · Stacks.CategoryTheory.Hypercovering.exists_hypercovering_map_factoring_through_locallySurjective

Section25.8 Adding simplices#

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

Tag 01GM, a lemma

Tag 01GM in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.isCoveringOver_homFromSSetMap_app_zero_of_oneMoreSimplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CoveringPermanence.lean, line 840.

Stacks Project, Tag 01GM. Let K be a hypercovering of X. If the finite simplicial set V is obtained from a subcomplex U by adjoining a single n-simplex x, with every simplex of V outside U in degree above n degenerate, then the restriction morphism Hom(V, K)₀ ⟶ Hom(U, K)₀ is a covering in SR(C, X).

theorem isCoveringOver_homFromSSetMap_app_zero_of_oneMoreSimplex (J : Pretopology C)
    [Precoverage.IsStableUnderComposition J.toPrecoverage] {X : C}
    (K : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (hK : IsHypercovering J K)
    (V : SSet.{max w v}) (U : V.Subcomplex)
    [SSet.Finite (U : SSet.{max w v})]
    (_hUnonempty : ∀ m : ℕ, Nonempty (U.obj (op ⦋m⦌)))
    (_hVfinite : ∀ m : ℕ, Finite (V.obj (op ⦋m⦌)))
    (_hVnonempty : ∀ m : ℕ, Nonempty (V.obj (op ⦋m⦌)))
    (n : ℕ) (x : V.obj (op ⦋n⦌))
    (hx : x ∉ Set.range (U.ι.app (op ⦋n⦌)))
    (hbelow : ∀ m < n, Function.Bijective (U.ι.app (op ⦋m⦌)))
    (hat : ∀ y : V.obj (op ⦋n⦌), y ∈ Set.range (U.ι.app (op ⦋n⦌)) ∨ y = x)
    (habove : ∀ m, n < m → ∀ y : V.obj (op ⦋m⦌),
      y ∉ Set.range (U.ι.app (op ⦋m⦌)) → y ∈ V.degenerate m)
    (HV HU : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (hV : SimplicialObject.IsHomFromSSet V K HV)
    (hU : SimplicialObject.IsHomFromSSet U K HU) :
    IsCoveringOver J ((homFromSSetMap hV hU U.ι).app (op ⦋0⦌))
Tag 01GN, a lemma

Tag 01GN in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.isCoveringOver_homFromSSetRestriction_app_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CoveringPermanence.lean, line 1277.

Stacks Project, Tag 01GN. Let K be a hypercovering of X and let U ⊆ V be finite nonempty simplicial sets. Then restriction Hom(V, K)₀ ⟶ Hom(U, K)₀ is a covering morphism in SR(C, X).

theorem isCoveringOver_homFromSSetRestriction_app_zero (J : Pretopology C)
    [Precoverage.IsStableUnderComposition J.toPrecoverage] (X : C)
    (K : SimplicialObject (FormalCoproduct.{w} (Over X))) (hK : IsHypercovering J K)
    (V : SSet.{max w v}) [V.Finite] [V.Nonempty]
    (U : V.Subcomplex) [SSet.Finite (U : SSet)] [SSet.Nonempty (U : SSet)] :
    IsCoveringOver J ((homFromSSetRestriction U.ι K).app (op ⦋0⦌))
Tag 0DEQ, a lemma

Tag 0DEQ in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.isCoveringOver_delta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/HypercoverDescent.lean, line 186. The attribute's comment: “part (2)”.

Stacks Project, Tag 0DEQ, part (2). Every face map of a hypercovering of X is a covering morphism in SR(C, X).

theorem isCoveringOver_delta (hK : IsHypercovering J K) (n : ℕ) (i : Fin (n + 2)) :
    IsCoveringOver J (K.δ i)

Stacks.CategoryTheory.Hypercovering.isCoveringOver_terminalFrom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/HypercoverDescent.lean, line 236. The attribute's comment: “part (1)”.

Stacks Project, Tag 0DEQ, part (1). Every level of a hypercovering of X is a covering of X.

theorem isCoveringOver_terminalFrom (hK : IsHypercovering J K) (n : ℕ) :
    IsCoveringOver J (terminal.from (K.obj (op ⦋n⦌)))
Tag 0DER, a remark

Tag 0DER in the Stacks Project.

CategoryTheory.MorphismProperty.IsHypercovering, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/MorphismProperty.lean, line 140. The attribute's comment: “p_hypercovering”.

Stacks Project, Tag 0DER. An augmented simplicial object is a P-hypercovering when its degree-zero augmentation, its canonical degree-one morphism to U₀ ×_X U₀, and all of its higher matching morphisms belong to P.

structure MorphismProperty.IsHypercovering {C : Type u} [Category.{v} C] [HasPullbacks C]
    (P : MorphismProperty C) (A : SimplicialObject.Augmented C) : Prop

CategoryTheory.MorphismProperty.IsHypercovering.face_mem, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/MorphismPropertyCovering.lean, line 104. The attribute's comment: “faces_in_p”.

Every face map in positive degree of a P-hypercovering belongs to P.

lemma face_mem (P : MorphismProperty C) [P.IsStableUnderBaseChange] [P.IsMultiplicative]
    {A : SimplicialObject.Augmented C}
    (hA : MorphismProperty.IsHypercovering P A) (n : ℕ) (i : Fin (n + 2)) :
    P (A.left.δ i)

CategoryTheory.MorphismProperty.IsHypercovering.hom_app, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/MorphismPropertyCovering.lean, line 124. The attribute's comment: “levels_in_p”.

Every level of a P-hypercovering maps to its augmentation point by a morphism in P.

This is the levels_in_p assertion of Stacks Project, Tag 0DER.

lemma hom_app [P.IsMultiplicative] [P.IsStableUnderBaseChange]
    (hA : MorphismProperty.IsHypercovering P A) (n : ℕ) :
    P (A.hom.app (Opposite.op (SimplexCategory.mk n)))
Sources
LeanStacks.CategoryTheory.Hypercovering.isCoveringOver_homFromSSetMap_app_zero_of_oneMoreSimplex · Stacks.CategoryTheory.Hypercovering.isCoveringOver_homFromSSetRestriction_app_zero · Stacks.CategoryTheory.Hypercovering.isCoveringOver_delta · Stacks.CategoryTheory.Hypercovering.isCoveringOver_terminalFrom · CategoryTheory.MorphismProperty.IsHypercovering · CategoryTheory.MorphismProperty.IsHypercovering.face_mem · CategoryTheory.MorphismProperty.IsHypercovering.hom_app

Section25.9 Homotopies#

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

Tag 01GP, a lemma

Tag 01GP in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.boundaryIntervalRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CoveringAndHomotopies/MatchingSquare.lean, line 82. The attribute's comment: “the two endpoint copies”.

Restriction to the two vertices of the interval is represented by the product of two copies of a simplicial semi-representable object.

theorem boundaryIntervalRepresentable
    (L : SimplicialObject (FormalCoproduct.{w} (Over X))) :
    Nonempty (SimplicialObject.IsHomFromSSet (SSet.boundary.{max v w} 1) L (L ⨯ L))

Stacks.CategoryTheory.Hypercovering.intervalEndpointMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CoveringAndHomotopies/MatchingSquare.lean, line 90. The attribute's comment: “the ordered endpoint map”.

The fixed endpoint-evaluation morphism Hom(Δ[1], L) ⟶ L × L. Its two components are, in order, the restrictions of the universal interval map to the vertices zero and one.

noncomputable def intervalEndpointMap
    (L H : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (hH : SimplicialObject.IsHomFromSSet Δ[1] L H) :
    { e : H ⟶ L ⨯ L //
      (∀ m : SimplexCategoryᵒᵖ,
        (e ≫ prod.fst).app m =
          (Functor.functorHomEquiv H L Δ[1] (hH.homEquiv (𝟙 H))).app m
            (SSet.stdSimplex.const 1 0 m)) ∧
      (∀ m : SimplexCategoryᵒᵖ,
        (e ≫ prod.snd).app m =
          (Functor.functorHomEquiv H L Δ[1] (hH.homEquiv (𝟙 H))).app m
            (SSet.stdSimplex.const 1 1 m)) }

Stacks.CategoryTheory.Hypercovering.homotopyMatchingSquare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CoveringAndHomotopies/MatchingSquare.lean, line 116.

Stacks Project, Tag 01GP. The four matching objects are represented by the corresponding simplicial sets, and the Hom object of the union is their fibre product. All arrows in the fibre product square are those induced by inclusions of simplicial sets.

theorem homotopyMatchingSquare
    (L : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (H : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (hH : SimplicialObject.IsHomFromSSet Δ[1] L H) :
    ∀ n : ℕ, ∃ Q : FormalCoproduct.{w} (Over X),
      let e := (intervalEndpointMap X L H hH).1;
      let m := n + 1;
      let S := SSet.boundary.{max v w} 1;
      let T := SSet.boundary.{max v w} m;
      let U := S.unionProd T;
      let F := coyoneda ⋙
        (Functor.whiskeringLeft SimplexCategoryᵒᵖ
          (FormalCoproduct.{w} (Over X)) (Type (max v w))).obj L;
      ∃ (hFull : (F ⋙ coyoneda.obj (op (Δ[1] ⊗ Δ[m]))).RepresentableBy (H _⦋m⦌))
        (hTop : (F ⋙ coyoneda.obj (op (Δ[1] ⊗ (T : SSet)))).RepresentableBy
          (((SimplicialObject.cosk n).obj H) _⦋m⦌))
        (hBottom : (F ⋙ coyoneda.obj (op ((S : SSet) ⊗ Δ[m]))).RepresentableBy
          ((L ⨯ L) _⦋m⦌))
        (hRight : (F ⋙ coyoneda.obj (op ((S : SSet) ⊗ (T : SSet)))).RepresentableBy
          (((SimplicialObject.cosk n).obj (L ⨯ L)) _⦋m⦌))
        (hUnion : (F ⋙ coyoneda.obj (op (U : SSet))).RepresentableBy Q),
        let comparison := hUnion.homEquiv.symm (U.ι ≫ hFull.homEquiv (𝟙 _));
        (e.app (op ⦋m⦌) =
          hBottom.homEquiv.symm ((S.ι ▷ Δ[m]) ≫ hFull.homEquiv (𝟙 _))) ∧
        ((((SimplicialObject.coskAdj n).unit.app H).app (op ⦋m⦌)) =
          hTop.homEquiv.symm ((Δ[1] ◁ T.ι) ≫ hFull.homEquiv (𝟙 _))) ∧
        ((((SimplicialObject.coskAdj n).unit.app (L ⨯ L)).app (op ⦋m⦌)) =
          hRight.homEquiv.symm (((S : SSet) ◁ T.ι) ≫ hBottom.homEquiv (𝟙 _))) ∧
        ((((SimplicialObject.cosk n).map e).app (op ⦋m⦌)) =
          hRight.homEquiv.symm ((S.ι ▷ (T : SSet)) ≫ hTop.homEquiv (𝟙 _))) ∧
        (comparison ≫ hTop.homEquiv.symm
          (SSet.Subcomplex.unionProd.ι₁ S T ≫ hUnion.homEquiv (𝟙 Q)) =
          ((SimplicialObject.coskAdj n).unit.app H).app (op ⦋m⦌)) ∧
        (comparison ≫ hBottom.homEquiv.symm
          (SSet.Subcomplex.unionProd.ι₂ S T ≫ hUnion.homEquiv (𝟙 Q)) =
          e.app (op ⦋m⦌)) ∧
        IsPullback
          (hTop.homEquiv.symm (SSet.Subcomplex.unionProd.ι₁ S T ≫
            hUnion.homEquiv (𝟙 Q)))
          (hBottom.homEquiv.symm (SSet.Subcomplex.unionProd.ι₂ S T ≫
            hUnion.homEquiv (𝟙 Q)))
          (hRight.homEquiv.symm ((S.ι ▷ (T : SSet)) ≫ hTop.homEquiv (𝟙 _)))
          (hRight.homEquiv.symm (((S : SSet) ◁ T.ι) ≫ hBottom.homEquiv (𝟙 _)))
Tag 01GS, a lemma

Tag 01GS in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.exists_homotopy_after_hypercovering_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CoveringAndHomotopies/Homotopy.lean, line 366.

Stacks Project, Tag 01GS. Two morphisms between hypercoverings become simplicially homotopic after precomposition with a morphism from a further hypercovering.

theorem exists_homotopy_after_hypercovering_refinement (J : Pretopology C)
    [Precoverage.IsStableUnderComposition J.toPrecoverage] {X : C}
    {K L : SimplicialObject (FormalCoproduct.{w} (Over X))}
    (hK : IsHypercovering J K) (hL : IsHypercovering J L) (a b : K ⟶ L) :
    ∃ (K' : SimplicialObject (FormalCoproduct.{w} (Over X))) (c : K' ⟶ K),
      IsHypercovering J K' ∧
        ∃ h : K'.copower Δ[1] ⟶ L, SimplicialObject.IsHomotopy h (c ≫ a) (c ≫ b)
Sources
LeanStacks.CategoryTheory.Hypercovering.boundaryIntervalRepresentable · Stacks.CategoryTheory.Hypercovering.intervalEndpointMap · Stacks.CategoryTheory.Hypercovering.homotopyMatchingSquare · Stacks.CategoryTheory.Hypercovering.exists_homotopy_after_hypercovering_refinement

Section25.10 Cohomology and hypercoverings#

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

Tag 01GZ, the section

Tag 01GZ in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.homologyMap_hypercoverCochainNatFunctorMap_app_eq_of_isHomotopy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CohomologyHomotopyInvariance.lean, line 174. The attribute's comment: “homotopic maps of hypercoverings have the same effect on Čech cohomology”.

Stacks Project, Tag 01GZ. Homotopic maps of simplicial semi-representable objects over X have the same effect on the Čech cohomology of an abelian sheaf: by [Stacks, Tag 019Y] their images on the cosimplicial object of sections are homotopic, and by [Stacks, Tag 01A0] homotopic maps of cosimplicial objects induce the same map on the cohomology of the associated cochain complexes.

theorem homologyMap_hypercoverCochainNatFunctorMap_app_eq_of_isHomotopy
    {K K' : SimplicialObject (FormalCoproduct.{w} (Over X))}
    [∀ m, HasCoproduct fun _ : (Δ[1] : SSet.{t}).obj m ↦ K.obj m]
    {ψ ψ' : K ⟶ K'} {h : K.copower (Δ[1] : SSet.{t}) ⟶ K'}
    (hh : SimplicialObject.IsHomotopy h ψ ψ')
    (F : Sheaf J.toGrothendieck AddCommGrpCat.{max u v w}) (p : ℕ) :
    HomologicalComplex.homologyMap
        ((hypercoverCochainNatFunctorMap.{w} J X ψ).app F) p =
      HomologicalComplex.homologyMap
        ((hypercoverCochainNatFunctorMap.{w} J X ψ').app F) p

Stacks.CategoryTheory.Hypercovering.whiskerRight_hypercoverCochainNatFunctorMap_eq_of_isHomotopy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CohomologyHomotopyInvariance.lean, line 190. The attribute's comment: “the induced natural transformation on Ȟ^p depends only on the homotopy class”.

Stacks Project, Tag 01GZ, as natural transformations. The map Ȟ^p(K', -) ⟶ Ȟ^p(K, -) of Čech cohomology functors induced by a map K ⟶ K' depends only on its homotopy class.

theorem whiskerRight_hypercoverCochainNatFunctorMap_eq_of_isHomotopy
    {K K' : SimplicialObject (FormalCoproduct.{w} (Over X))}
    [∀ m, HasCoproduct fun _ : (Δ[1] : SSet.{t}).obj m ↦ K.obj m]
    {ψ ψ' : K ⟶ K'} {h : K.copower (Δ[1] : SSet.{t}) ⟶ K'}
    (hh : SimplicialObject.IsHomotopy h ψ ψ') (p : ℕ) :
    Functor.whiskerRight (hypercoverCochainNatFunctorMap.{w} J X ψ)
        (HomologicalComplex.homologyFunctor AddCommGrpCat.{max u v w}
          (ComplexShape.up ℕ) p) =
      Functor.whiskerRight (hypercoverCochainNatFunctorMap.{w} J X ψ')
        (HomologicalComplex.homologyFunctor AddCommGrpCat.{max u v w}
          (ComplexShape.up ℕ) p)

Stacks.CategoryTheory.Hypercovering.cechCohomologyHypercoveringsHomotopyFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CohomologyHomotopyInvariance.lean, line 235. The attribute's comment: “Ȟ^p(-, 𝓕) as a diagram on HC(C, X)ᵒᵖ”.

Stacks Project, Tag 01GZ. Ȟ^p(-, -) : HC(C, X)ᵒᵖ ⥤ (Ab(C) ⥤ Ab): the Čech cohomology of a hypercovering of X, as a diagram on the hypercoverings of X with maps up to homotopy.

This is the diagram whose colimit [Stacks, Tag 01H0] compares with sheaf cohomology; it exists because homotopic maps have the same effect on Čech cohomology, which is whiskerRight_hypercoverCochainNatFunctorMap_eq_of_isHomotopy.

noncomputable def cechCohomologyHypercoveringsHomotopyFunctor (p : ℕ) :
    (HypercoveringsHomotopy.{w} J X)ᵒᵖ ⥤
      (Sheaf J.toGrothendieck AddCommGrpCat.{max u v w} ⥤
        AddCommGrpCat.{max u v w})
Tag 01H0, a theorem

Tag 01H0 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.Functorial.isColimit_cechCohomologyZeroCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CohomologyAsColimit.lean, line 698. The attribute's comment: “the case i = 0: colim over hypercoverings of Ȟ⁰(K, H⁰(-)) is H⁰(X, -), as functors on Ab(C); the hypotheses carried are fibre products in C and stability of the pretopology under composition”.

For a site with fibre products and an object X, the functor 𝓕 ↦ H⁰(X, 𝓕) on abelian sheaves is the colimit over all hypercoverings K of X of the functors 𝓕 ↦ Ȟ⁰(K, H⁰(𝓕)), the cocone being the canonical identification of each Ȟ⁰(K, H⁰(-)) with H⁰(X, -).

def isColimit_cechCohomologyZeroCocone
    [Precoverage.IsStableUnderComposition J.toPrecoverage] :
    IsColimit (cechCohomologyZeroCocone X J)

Stacks.CategoryTheory.Hypercovering.Functorial.isColimit_cechCoconeAtSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CohomologyAsColimit.lean, line 1224. The attribute's comment: “the general case at a fixed abelian sheaf: colim over hypercoverings of Ȟ^i(K, 𝓕) is H^i(X, 𝓕); the index category is the hypercoverings of X themselves rather than the homotopy quotient HC(C, X), and the hypotheses carried are fibre products in C and stability of the pretopology under composition”. References: SGA 4 V (7.4.1), “Clause 2)”.

For a site with fibre products, an object X and an abelian sheaf 𝓕, the cohomology H^n(X, 𝓕) is the colimit over the hypercoverings of X of the Čech cohomology groups Ȟ^n(K, 𝓕), the cocone being the canonical edge maps hypercoveringCechEdge. The index category is the category of hypercoverings itself, not the homotopy quotient HC(C, X).

def isColimit_cechCoconeAtSheaf (n : ℕ) (F : Sheaf J.toGrothendieck AddCommGrpCat.{v}) :
    IsColimit (cechCoconeAtSheaf X J n F)

Stacks.CategoryTheory.Hypercovering.Functorial.isColimit_cechFunctorCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/CohomologyAsColimit.lean, line 1309. The attribute's comment: “the functor-level statement in every degree, which is the claim of the tag: the edge maps exhibit the functor 𝓕 ↦ H^i(X, 𝓕) on Ab(C) as the colimit over the hypercoverings K of X of the functors 𝓕 ↦ Ȟ^i(K, 𝓕), the colimit being taken in the category of functors Ab(C) ⥤ Ab; the index category is the hypercoverings of X themselves rather than the homotopy quotient HC(C, X), and the hypotheses carried are fibre products in C and stability of the pretopology under composition”.

Let C be a site with fibre products and X an object of C. For every i, the two functors Ab(C) ⥤ Ab given by 𝓕 ↦ H^i(X, 𝓕) and by 𝓕 ↦ colim_K Ȟ^i(K, 𝓕), the colimit being over the hypercoverings K of X, are canonically isomorphic: the edge maps hypercoveringCechEdge exhibit the functor H^i(X, -) as the colimit of the functors Ȟ^i(K, -) in the category of functors Ab(C) ⥤ Ab. The index category is the category of hypercoverings itself, not the homotopy quotient HC(C, X).

def isColimit_cechFunctorCocone (n : ℕ) : IsColimit (cechFunctorCocone X J n)
Tag 09VZ, a proposition

Tag 09VZ in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.exists_hom_cechCohomologyEdge_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/GlobalDegeneration.lean, line 841. The attribute's comment: “part (2) in every degree, at the hypercovering universe max u v w, which is what Tag 01GJ forces; the canonical map is the bottom-row edge map of the spectral sequence of Tag 09VY, i.e. the comparison of Tag 01GY. The size binders are those the chapter's presheaf-side tags carry -- sheafification, enough injectives and HasExt at the coefficient universe -- together with WEqualsLocallyBijective, a theorem for every essentially small site. See exists_hom_cechCohomologyEdge_zero_eq for degree zero at a free universe w”.

In every degree i, two Čech classes in Ȟ^i(K, 𝓕) and Ȟ^i(L, 𝓕), for hypercoverings K and L of the final presheaf, whose images under the canonical comparison Ȟ^i(-, 𝓕) ⟶ H^i(𝓕) agree restrict to the same class on a common refinement.

The coefficients are the sheaf 𝓕 itself, not its degree-zero cohomology presheaf. On the common refinement exists_hom_of_prod the difference of the two restrictions is killed by the comparison, so it dies after a further refinement (exists_hom_cechCohomologyMap_apply_eq_zero), and on that refinement the two restrictions agree.

theorem exists_hom_cechCohomologyEdge_eq (i : ℕ)
    (K L : HypercoveringOfTerminal.{max u v w} J)
    (ξK : cechCohomology J (⊤_ (Cᵒᵖ ⥤ Type v)) K F i)
    (ξL : cechCohomology J (⊤_ (Cᵒᵖ ⥤ Type v)) L F i)
    (h : ConcreteCategory.hom (cechCohomologyEdge.{max u v w} J K i F) ξK =
      ConcreteCategory.hom (cechCohomologyEdge.{max u v w} J L i F) ξL) :
    ∃ (M : HypercoveringOfTerminal.{max u v w} J) (f : M.Hom K) (g : M.Hom L),
      ConcreteCategory.hom (f.cechCohomologyMap F i) ξK =
        ConcreteCategory.hom (g.cechCohomologyMap F i) ξL

Stacks.CategoryTheory.Hypercovering.exists_hypercoveringOfTerminal_cechCohomologyEdge_zero_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/GlobalEdgeNaturality.lean, line 1326. The attribute's comment: “part (1) in degree i = 0, universe-general: the hypercoverings are at a free universe w, which is what keeps this statement from being subsumed by exists_hypercoveringOfTerminal_cechCohomologyEdge_eq, which has every degree but is at max u v w because Tag 01GJ forces it; the canonical map is the bottom-row edge map of the spectral sequence of Tag 09VY, i.e. the comparison of Tag 01GY”.

Stacks Project, Tag 09VZ, part (1), in degree zero. Every degree-zero cohomology class of an abelian sheaf is the image, under the canonical comparison Ȟ⁰(K, 𝓕) ⟶ H⁰(𝓕) of [Stacks, Tag 09VY], of a degree-zero Čech class on some hypercovering K of the final presheaf.

A hypercovering exists by [Stacks, Tag 0DAX] applied to the identity coverings, and in degree zero the comparison is an isomorphism, isIso_cechCohomologyEdge_zero.

theorem exists_hypercoveringOfTerminal_cechCohomologyEdge_zero_eq
    (F : Sheaf J.toGrothendieck AddCommGrpCat.{max (max u v) (max v w)})
    (ξ : (globalCohomologyFunctor.{max u v w} J 0).obj F) :
    ∃ (K : HypercoveringOfTerminal.{max u v w} J)
      (ξK : cechCohomology J (⊤_ (Cᵒᵖ ⥤ Type v)) K F 0),
      ConcreteCategory.hom (cechCohomologyEdge.{max u v w} J K 0 F) ξK = ξ

Stacks.CategoryTheory.Hypercovering.exists_hom_cechCohomologyEdge_zero_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/GlobalEdgeNaturality.lean, line 1380. The attribute's comment: “part (2) in degree i = 0, universe-general: the hypercoverings are at a free universe w, which is what keeps this statement from being subsumed by exists_hom_cechCohomologyEdge_eq, the same part (2) in every degree but with the hypercoverings at max u v w, the universe Tag 01GJ forces. The canonical map is the bottom-row edge map of the spectral sequence of Tag 09VY, i.e. the comparison of Tag 01GY, and its naturality in the hypercovering is proved, not assumed”.

Stacks Project, Tag 09VZ, part (2), in degree zero. Two degree-zero Čech classes on hypercoverings K and L of the final presheaf whose images under the canonical comparison Ȟ⁰(-, 𝓕) ⟶ H⁰(𝓕) of [Stacks, Tag 09VY] agree restrict to the same class on a common refinement.

Nothing is assumed beyond the source's hypotheses. The common refinement is the degreewise product, exists_hom_of_prod, which is what products of pairs in C are assumed for; that the two restrictions then agree is cechCohomologyMap_apply_eq_of_cechCohomologyEdge_apply_eq, which rests on the naturality of the comparison in the hypercovering, HypercoveringOf.Hom.globalCechEdge_comp_cechCohomologyMap.

theorem exists_hom_cechCohomologyEdge_zero_eq [HasBinaryProducts C]
    (F : Sheaf J.toGrothendieck AddCommGrpCat.{max (max u v) (max v w)})
    (K L : HypercoveringOfTerminal.{w} J)
    (ξK : cechCohomology J (⊤_ (Cᵒᵖ ⥤ Type v)) K F 0)
    (ξL : cechCohomology J (⊤_ (Cᵒᵖ ⥤ Type v)) L F 0)
    (h : ConcreteCategory.hom (cechCohomologyEdge.{w} J K 0 F) ξK =
      ConcreteCategory.hom (cechCohomologyEdge.{w} J L 0 F) ξL) :
    ∃ (M : HypercoveringOfTerminal.{w} J) (f : M.Hom K) (g : M.Hom L),
      ConcreteCategory.hom (f.cechCohomologyMap F 0) ξK =
        ConcreteCategory.hom (g.cechCohomologyMap F 0) ξL

Stacks.CategoryTheory.Hypercovering.exists_hypercoveringOfTerminal_cechCohomologyEdge_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/GlobalFiltrationDescent.lean, line 742. The attribute's comment: “part (1) in every degree, at the hypercovering universe max u v w, which is what Tag 01GJ forces; the canonical map is the bottom-row edge map of the spectral sequence of Tag 09VY, i.e. the comparison of Tag 01GY. The size binders are those the chapter's presheaf-side tags carry -- sheafification, enough injectives and HasExt at the coefficient universe -- together with WEqualsLocallyBijective, a theorem for every essentially small site, which is carried here because the degeneration of the spectral sequence rests on Tag 01GJ. See exists_hypercoveringOfTerminal_cechCohomologyEdge_zero_eq for degree zero at a free universe w”. References: SGA 4 V (7.4.1), “Clause 2)”.

Stacks Project, Tag 09VZ, part (1), in every degree. Every cohomology class of an abelian sheaf is the image, under the canonical comparison Ȟ^i(K, 𝓕) ⟶ H^i(𝓕) of [Stacks, Tag 09VY], of a Čech class on some hypercovering K of the final presheaf.

The coefficients are the sheaf 𝓕 itself, not its degree-zero cohomology presheaf. A hypercovering exists by [Stacks, Tag 0DAX] applied to the identity coverings; the zeroth step of the abutment filtration is the whole of H^i(𝓕) (isIso_globalStepToAbutment_zero), the class descends from there to the bottom step F^iH^i(𝓕) after a refinement (exists_hom_globalStepToAbutment_eq, whose engine is the degeneration of StacksFrontier/CategoryTheory/Sites/Hypercovering/GlobalDegeneration.lean), and the bottom step is the image of Ȟ^i(L, 𝓕) under the comparison (exists_cechCohomologyEdge_apply_eq_globalStepToAbutment_apply).

theorem exists_hypercoveringOfTerminal_cechCohomologyEdge_eq (i : ℕ)
    (ξ : (globalCohomologyFunctor.{max u v w} J i).obj F) :
    ∃ (K : HypercoveringOfTerminal.{max u v w} J)
      (ξK : cechCohomology J (⊤_ (Cᵒᵖ ⥤ Type v)) K F i),
      ConcreteCategory.hom (cechCohomologyEdge.{max u v w} J K i F) ξK = ξ
Sources
LeanStacks.CategoryTheory.Hypercovering.homologyMap_hypercoverCochainNatFunctorMap_app_eq_of_isHomotopy · Stacks.CategoryTheory.Hypercovering.whiskerRight_hypercoverCochainNatFunctorMap_eq_of_isHomotopy · Stacks.CategoryTheory.Hypercovering.cechCohomologyHypercoveringsHomotopyFunctor · Stacks.CategoryTheory.Hypercovering.Functorial.isColimit_cechCohomologyZeroCocone · Stacks.CategoryTheory.Hypercovering.Functorial.isColimit_cechCoconeAtSheaf · Stacks.CategoryTheory.Hypercovering.Functorial.isColimit_cechFunctorCocone · Stacks.CategoryTheory.Hypercovering.exists_hom_cechCohomologyEdge_eq · Stacks.CategoryTheory.Hypercovering.exists_hypercoveringOfTerminal_cechCohomologyEdge_zero_eq

Section25.11 Hypercoverings of spaces#

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

Tag 01H2, an equation

Tag 01H2 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.iSup_eq_top_of_isHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Spaces.lean, line 451.

Stacks Project, Tag 01H2. In a hypercovering of a topological space, the opens attached to the degree-zero indices cover the whole space.

theorem iSup_eq_top_of_isHypercovering {X : Type u} [TopologicalSpace X]
    (K : SimplicialObject (FormalCoproduct.{w} (Over (⊤ : Opens X))))
    (hK : IsHypercovering (Opens.pretopology X) K) :
    (⨆ i : (K.obj (Opposite.op ⦋0⦌)).I, ((K.obj (Opposite.op ⦋0⦌)).obj i).left) = ⊤
Tag 01H3, an equation

Tag 01H3 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.inf_eq_iSup_edges, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Spaces.lean, line 468.

Stacks Project, Tag 01H3. In a hypercovering of a topological space, the intersection of the opens attached to two vertices is the union of the opens attached to the edges whose zeroth and first faces are those vertices.

theorem inf_eq_iSup_edges {X : Type u} [TopologicalSpace X]
    (K : SimplicialObject (FormalCoproduct.{w} (Over (⊤ : Opens X))))
    (hK : IsHypercovering (Opens.pretopology X) K)
    (i₀ i₁ : (K.obj (Opposite.op ⦋0⦌)).I) :
    ((K.obj (Opposite.op ⦋0⦌)).obj i₀).left ⊓
        ((K.obj (Opposite.op ⦋0⦌)).obj i₁).left =
      ⨆ i : { i : (K.obj (Opposite.op ⦋1⦌)).I //
          (K.δ (0 : Fin 2)).f i = i₀ ∧ (K.δ (1 : Fin 2)).f i = i₁ },
        ((K.obj (Opposite.op ⦋1⦌)).obj i.1).left
Tag 01H4, an equation

Tag 01H4 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.intersection_eq_union_of_isHypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Spaces.lean, line 485.

Stacks Project, Tag 01H4. In a hypercovering of a topological space, the intersection of a compatible family of n + 3 degree-n + 1 opens is the union of the degree-n + 2 opens whose faces are the prescribed family. This is the source's equation in every degree at least one.

theorem intersection_eq_union_of_isHypercovering
    (X : Type u) [TopologicalSpace X]
    (K : SimplicialObject (FormalCoproduct.{w} (Over (⊤ : Opens X))))
    (hK : IsHypercovering (Opens.pretopology X) K)
    (n : ℕ)
    (i : (a : Fin (n + 3)) → (K.obj (Opposite.op (SimplexCategory.mk (n + 1)))).I)
    (hi : ∀ (a b : Fin (n + 3)) (hab : a < b),
      (K.δ (b.pred (ne_of_gt (lt_of_le_of_lt (Fin.zero_le a) hab)))).f (i a) =
        (K.δ (a.castPred (ne_of_lt (lt_of_lt_of_le hab (Fin.le_last b))))).f (i b)) :
    (⨅ a, ((K.obj (Opposite.op (SimplexCategory.mk (n + 1)))).obj (i a)).left) =
      ⨆ j : { j : (K.obj (Opposite.op (SimplexCategory.mk (n + 2)))).I //
        ∀ a, (K.δ a).f j = i a },
        ((K.obj (Opposite.op (SimplexCategory.mk (n + 2)))).obj j.1).left
Tag 01H6, a lemma

Tag 01H6 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.exists_hypercovering_of_isTopologicalBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Construction/TopologicalBasis.lean, line 260.

Stacks Project, Tag 01H6. Every basis of a topological space supports a hypercovering all of whose constituent open subsets belong to that basis.

theorem exists_hypercovering_of_isTopologicalBasis
    (B : Set (Set X)) (hB : IsTopologicalBasis B) :
    ∃ K : SimplicialObject (FormalCoproduct.{u} (Over (⊤ : Opens X))),
      IsHypercovering (Opens.pretopology X) K ∧
        ∀ n : ℕ, ∀ i : (K.obj (Opposite.op ⦋n⦌)).I,
          ((K.obj (Opposite.op ⦋n⦌)).obj i).left.1 ∈ B
Tag 01H7, a lemma

Tag 01H7 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.exists_finite_hypercovering_of_isTopologicalBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Construction/TopologicalBasis.lean, line 314.

Stacks Project, Tag 01H7. A quasi-compact topological space with a basis of quasi-compact opens and quasi-compact intersections of quasi-compact opens has a hypercovering subordinate to that basis whose index type is finite in every degree.

theorem exists_finite_hypercovering_of_isTopologicalBasis
    (B : Set (Set X)) (hB : IsTopologicalBasis B)
    (hX : IsCompact (Set.univ : Set X))
    (hBcompact : ∀ U ∈ B, IsCompact U)
    (hInter : ∀ U V : Set X, IsOpen U → IsCompact U →
      IsOpen V → IsCompact V → IsCompact (U ∩ V)) :
    ∃ K : SimplicialObject (FormalCoproduct.{u} (Over (⊤ : Opens X))),
      IsHypercovering (Opens.pretopology X) K ∧
        ∀ n : ℕ, Finite (K.obj (Opposite.op (SimplexCategory.mk n))).I ∧
          ∀ i : (K.obj (Opposite.op (SimplexCategory.mk n))).I,
            ((K.obj (Opposite.op (SimplexCategory.mk n))).obj i).left.1 ∈ B
Sources
LeanStacks.CategoryTheory.Hypercovering.iSup_eq_top_of_isHypercovering · Stacks.CategoryTheory.Hypercovering.inf_eq_iSup_edges · Stacks.CategoryTheory.Hypercovering.intersection_eq_union_of_isHypercovering · Stacks.CategoryTheory.Hypercovering.exists_hypercovering_of_isTopologicalBasis · Stacks.CategoryTheory.Hypercovering.exists_finite_hypercovering_of_isTopologicalBasis

Section25.12 Constructing hypercoverings#

Section 25.12 of the Stacks Project, Tag 094J. 9 tags here are carried by 14 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DAU, a lemma

Tag 0DAU in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.split_iff_components_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Split.lean, line 850. The attribute's comment: “simplicial: (1) iff (2)”.

Stacks Project, Tag 0DAU, parts (1) and (2). A simplicial formal coproduct is split iff each component map over a surjective simplicial operator is an isomorphism.

theorem split_iff_components_of_epi
    (K : SimplicialObject (FormalCoproduct.{w} C)) :
    Nonempty K.Splitting ↔
      ∀ {m n : SimplexCategory} (φ : m ⟶ n) [Epi φ]
        (i : (K.obj (op n)).I),
        IsIso ((K.map φ.op).φ i)

Stacks.CategoryTheory.Hypercovering.components_of_epi_iff_components_of_degeneracy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Split.lean, line 864. The attribute's comment: “simplicial: (2) iff (3)”.

Stacks Project, Tag 0DAU, parts (2) and (3). It suffices to test the elementary degeneracies of a simplicial formal coproduct.

theorem components_of_epi_iff_components_of_degeneracy
    (K : SimplicialObject (FormalCoproduct.{w} C)) :
    (∀ {m n : SimplexCategory} (φ : m ⟶ n) [Epi φ]
      (i : (K.obj (op n)).I), IsIso ((K.map φ.op).φ i)) ↔
    (∀ (n : ℕ) (j : Fin (n + 1))
      (i : (K.obj (op (SimplexCategory.mk n))).I),
      IsIso ((K.map (SimplexCategory.σ j).op).φ i))

Stacks.CategoryTheory.Hypercovering.truncated_split_iff_components_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Split.lean, line 895. The attribute's comment: “truncated: (1) iff (2)”.

Stacks Project, Tag 0DAU, truncated parts (1) and (2).

theorem truncated_split_iff_components_of_epi (r : ℕ)
    (K : SimplicialObject.Truncated (FormalCoproduct.{w} C) r) :
    IsTruncatedSplit r K ↔
      ∀ {m n : SimplexCategory.Truncated r} (φ : m ⟶ n) [Epi φ]
        (i : (K.obj (op n)).I),
        IsIso ((K.map φ.op).φ i)

Stacks.CategoryTheory.Hypercovering.truncated_components_of_epi_iff_components_of_degeneracy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Split.lean, line 918. The attribute's comment: “truncated: (2) iff (3)”.

Stacks Project, Tag 0DAU, truncated parts (2) and (3).

theorem truncated_components_of_epi_iff_components_of_degeneracy (r : ℕ)
    (K : SimplicialObject.Truncated (FormalCoproduct.{w} C) r) :
    (∀ {m n : SimplexCategory.Truncated r} (φ : m ⟶ n) [Epi φ]
      (i : (K.obj (op n)).I), IsIso ((K.map φ.op).φ i)) ↔
    (∀ (n : ℕ) (hn : n + 1 ≤ r) (j : Fin (n + 1))
      (i : (K.obj (op (⟨SimplexCategory.mk n, Nat.le_of_succ_le hn⟩ :
        SimplexCategory.Truncated r))).I),
      IsIso ((K.map (ObjectProperty.homMk (SimplexCategory.σ j) :
        (⟨SimplexCategory.mk (n + 1), hn⟩ : SimplexCategory.Truncated r) ⟶
        (⟨SimplexCategory.mk n, Nat.le_of_succ_le hn⟩ :
          SimplexCategory.Truncated r)).op).φ i))
Tag 0DAV, a lemma

Tag 0DAV in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.exists_hypercovering_with_objects_in, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Construction/ObjectsInCollection.lean, line 1156.

Stacks Project, Tag 0DAV. If the objects in B cover every object of a site and adjoining one more morphism whose source lies in B preserves such a covering, then every object has a hypercovering all of whose constituent objects lie in B.

theorem exists_hypercovering_with_objects_in
    (J : Pretopology C) (B : Set C)
    (hcover : ∀ U : C, ∃ (ι : Type w) (V : ι → C) (f : ∀ i, V i ⟶ U),
      (∀ i, V i ∈ B) ∧ Presieve.ofArrows V f ∈ J U)
    (hadjoin : ∀ {ι : Type w} (V : ι → C) {U : C} (f : ∀ i, V i ⟶ U),
      (∀ i, V i ∈ B) → Presieve.ofArrows V f ∈ J U →
      ∀ {U' : C}, U' ∈ B → ∀ g : U' ⟶ U,
        (fun {_} h ↦ Presieve.ofArrows V f h ∨ Presieve.singleton g h) ∈ J U)
    (X : C) :
    ∃ K : SimplicialObject (FormalCoproduct.{w} (Over X)),
      IsHypercovering J K ∧
        ∀ (n : ℕ) (i : (K.obj (op (SimplexCategory.mk n))).I),
          ((K.obj (op (SimplexCategory.mk n))).obj i).left ∈ B
Tag 0DAX, a lemma

Tag 0DAX in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.exists_hypercoveringOfTerminal_with_objects_in, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Construction/PresheafObjects/Existence.lean, line 29.

Stacks Project, Tag 0DAX. A covering collection of objects supplies a hypercovering of the final presheaf all of whose terms are coproducts of objects in that collection.

theorem exists_hypercoveringOfTerminal_with_objects_in
    (J : Pretopology C) (B : Set C)
    (hcover : ∀ U : C, ∃ (ι : Type (max w u v)) (V : ι → C) (f : ∀ i, V i ⟶ U),
      (∀ i, V i ∈ B) ∧ Presieve.ofArrows V f ∈ J U) :
    ∃ K : HypercoveringOfTerminal.{max w u v} J,
      ∀ (n : ℕ) (i : (K.toSimplicialObject.obj (op (SimplexCategory.mk n))).I),
        (K.toSimplicialObject.obj (op (SimplexCategory.mk n))).obj i ∈ B
Tag 0DAY, a lemma

Tag 0DAY in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.exists_hypercovering_of_map, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/MorphismOfSites.lean, line 585.

The underlying functor of a morphism of sites which preserves equalizers and pullbacks carries a hypercovering to a hypercovering.

lemma exists_hypercovering_of_map
    [HasEqualizers C] [HasPullbacks C] [HasEqualizers D] [HasPullbacks D]
    (J : Pretopology C) (K : Pretopology D) (u : D ⥤ C)
    [IsMorphismOfSites.{max w vC vD uC uD} u K.toGrothendieck J.toGrothendieck]
    [PreservesLimitsOfShape WalkingParallelPair u]
    [PreservesLimitsOfShape WalkingCospan u]
    (X : HypercoveringOfTerminal.{w} K) :
    ∃ Y : HypercoveringOfTerminal.{w} J,
      Y.toSimplicialObject = X.toSimplicialObject ⋙ mapFormalCoproduct u
Tag 0DAZ, a lemma

Tag 0DAZ in the Stacks Project.

Stacks.Topology.LocallyQuasiCompactQcSite.isHypercovering_map_smallSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/LocallyQuasiCompact/QcSmallModel.lean, line 265. The attribute's comment: “a hypercovering of LC_qc transported to a small model of it”.

Stacks 0DAZ at the comparison with the small model. A hypercovering of an object of LC_qc, carried degreewise to the small model, is a hypercovering of the image object there.

This is the transport the simplicial-hypercovering apparatus needs: that apparatus consumes a hypercovering of a small site --- isLocallyFull_totalForget_over and essImage_of_isCartesianSheaf take an IsHypercovering --- and LC_qc is not one. The comparison functor preserves fibre products, being an equivalence, and takes coverings to coverings by mapsCoveringsToCoverings_smallEquivalence, which are exactly the two hypotheses of Stacks 0DAZ.

theorem isHypercovering_map_smallSite {Y : S.category}
    (K : SimplicialObject (FormalCoproduct.{t₁} (Over Y)))
    (hK : IsHypercovering S.pretopology K) :
    IsHypercovering S.smallPretopology
      (K ⋙ mapFormalCoproduct.{t₁} (Over.post S.smallEquivalence.functor))

Stacks.CategoryTheory.Hypercovering.IsHypercovering.map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Map.lean, line 467. The attribute's comment: “the hypothesis that u be continuous is used only through its covering clause MapsCoveringsToCoverings, which is Tag 00WV(1) verbatim — the same index type and the same image family — together with the preservation of fibre products that is Tag 00WV(2); the conclusion is the full statement, both the degree-zero clause and the clause in degree n + 1”.

Stacks Project, Tag 0DAZ. Let u : D ⥤ C be a functor between sites given by pretopologies which takes covering families to covering families and preserves fibre products. Then the degreewise image under u of a hypercovering of Y : D is a hypercovering of u Y.

theorem IsHypercovering.map (JD : Pretopology D) (JC : Pretopology C) (u : D ⥤ C)
    (hu : MapsCoveringsToCoverings.{w} u JD JC) [PreservesLimitsOfShape WalkingCospan u] {Y : D}
    (K : SimplicialObject (FormalCoproduct.{w} (Over Y)))
    (hK : IsHypercovering JD K) :
    IsHypercovering JC (K ⋙ mapFormalCoproduct.{w} (Over.post u))
Tag 094K, a lemma

Tag 094K in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.exists_finite_hypercovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/FiniteConstruction.lean, line 890.

Stacks Project, Tag 094K. If a class B supplies finite coverings and every such covering remains covering after adjoining one further arrow from an object of B, then every object has a hypercovering whose family in every degree is finite and consists of objects of B.

theorem exists_finite_hypercovering
    {C : Type u} [Category.{v} C] [HasPullbacks C] (J : Pretopology C) (B : Set C)
    (exists_finite_cover : ∀ X : C,
      ∃ (I : Type w) (U : I → C) (f : ∀ i, U i ⟶ X),
        Finite I ∧ (∀ i, B (U i)) ∧ Presieve.ofArrows U f ∈ J X)
    (cover_of_adjoin : ∀ {X : C} {I : Type w} (U : I → C) (f : ∀ i, U i ⟶ X),
      Finite I → (∀ i, B (U i)) → Presieve.ofArrows U f ∈ J X →
      ∀ (V : C) (g : V ⟶ X), B V →
        Presieve.ofArrows
          (fun i : Sum I PUnit ↦ match i with | Sum.inl i => U i | Sum.inr _ => V)
          (fun i : Sum I PUnit ↦ match i with | Sum.inl i => f i | Sum.inr _ => g) ∈ J X) :
    ∀ X : C, ∃ K : SimplicialObject (FormalCoproduct.{w} (Over X)),
      IsHypercovering J K ∧
        ∀ n : ℕ, Finite (K.obj (Opposite.op ⦋n⦌)).I ∧
          ∀ i, B ((K.obj (Opposite.op ⦋n⦌)).obj i).left
Tag 0DB0, a remark

Tag 0DB0 in the Stacks Project.

Declarations registered for the tag:

Tag 0DB1, a remark

Tag 0DB1 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.degreewiseUnions, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Construction/DegreewiseUnions.lean, line 311. The attribute's comment: “the simplicial object of degreewise disjoint unions”.

Take disjoint unions in each degree of a simplicial semi-representable object. Only the coproducts of the objects actually occurring are required to exist.

noncomputable def degreewiseUnions (K : SimplicialObject (FormalCoproduct.{w} C))
    (hsum : ∀ n, HasCoproduct (K.obj n).obj) : SimplicialObject (FormalCoproduct.{w} C)

Stacks.CategoryTheory.Hypercovering.hypercoveringDegreewiseUnions, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Construction/DegreewiseUnions.lean, line 443. The attribute's comment: “the degreewise disjoint unions again form a hypercovering”.

Stacks Project, Tag 0DB1. Let K be a hypercovering on a site with fibre products and equalizers. If the coproduct of the objects in each degree of K exists and the map from the coproduct of their representable presheaves to the presheaf represented by that coproduct becomes an isomorphism after sheafification, then the degreewise disjoint unions again form a hypercovering.

noncomputable def hypercoveringDegreewiseUnions (K : HypercoveringOfTerminal.{w} J)
    (hsum : ∀ n, HasCoproduct (K.toSimplicialObject.obj n).obj)
    (hinj : ∀ n, Presheaf.IsLocallyInjective J.toGrothendieck
      ((associatedPresheafFunctor.{v}).map
        ((toDegreewiseUnions K.toSimplicialObject hsum).app n)))
    (hsurj : ∀ n, Presheaf.IsLocallySurjective J.toGrothendieck
      ((associatedPresheafFunctor.{v}).map
        ((toDegreewiseUnions K.toSimplicialObject hsum).app n))) :
    HypercoveringOfTerminal.{w} J
Tag 0DB2, a remark

Tag 0DB2 in the Stacks Project.

Stacks.CategoryTheory.Hypercovering.takeUnionsSimplicial, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Construction/DisjointUnions.lean, line 95. The attribute's comment: “the degreewise construction”.

Take the disjoint unions in each degree of a simplicial formal coproduct over X. Only the coproducts of its actual terms are required to exist.

noncomputable def takeUnionsSimplicial
    (K : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (hsum : ∀ n, HasCoproduct (K.obj n).obj) :
    SimplicialObject (FormalCoproduct.{w} (Over X))

Stacks.CategoryTheory.Hypercovering.isHypercovering_takeUnionsSimplicial, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Hypercovering/Construction/DisjointUnions.lean, line 226. The attribute's comment: “preservation of hypercoverings”.

If summable semi-representable objects over X are closed under finite limits, taking their coproducts commutes with those limits, and it sends coverings to coverings, then applying it degreewise to a hypercovering again gives a hypercovering.

lemma isHypercovering_takeUnionsSimplicial
    [ObjectProperty.IsClosedUnderFiniteLimits
      (fun U : FormalCoproduct.{w} (Over X) ↦ HasCoproduct U.obj)]
    [PreservesFiniteLimits (takeUnions.{w, v, max u v} (C := Over X))]
    (hcover : ∀ ⦃U V : SummableFormalCoproduct.{w} (Over X)⦄ (f : U ⟶ V),
      IsCoveringOver J ((summableInclusion (C := Over X)).map f) →
        IsCoveringOver J ((takeUnions (C := Over X)).map f))
    (K : SimplicialObject (FormalCoproduct.{w} (Over X)))
    (hsum : ∀ n, HasCoproduct (K.obj n).obj)
    (hK : IsHypercovering J K) :
    IsHypercovering J (takeUnionsSimplicial K hsum)
Sources
LeanStacks.CategoryTheory.Hypercovering.split_iff_components_of_epi · Stacks.CategoryTheory.Hypercovering.components_of_epi_iff_components_of_degeneracy · Stacks.CategoryTheory.Hypercovering.truncated_split_iff_components_of_epi · Stacks.CategoryTheory.Hypercovering.truncated_components_of_epi_iff_components_of_degeneracy · Stacks.CategoryTheory.Hypercovering.exists_hypercovering_with_objects_in · Stacks.CategoryTheory.Hypercovering.exists_hypercoveringOfTerminal_with_objects_in · Stacks.CategoryTheory.Hypercovering.exists_hypercovering_of_map · Stacks.Topology.LocallyQuasiCompactQcSite.isHypercovering_map_smallSite

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.