The Čech comparison as a construction on complexes of sheaves #
Every step of the Čech-to-derived comparison built in
DerivedAlgGeo.Topology.Sheaves.Cech.GlobalComparison reads its injective
resolution I only through the cochain complex I.cochainComplex. This file makes that
dependence explicit: each construction is restated for an arbitrary cochain complex of sheaves,
agreeing with the original by definition, and each is shown to commute with an arbitrary
morphism of such complexes.
This is the content that the bare Nonempty (_ ≃+ _) form of the comparison cannot supply.
A k-action on cohomology arrives as the map induced by a single endomorphism of the sheaf,
so k-linearity of the comparison is exactly the statement that the comparison commutes with
the maps induced by that endomorphism — which is what the naturality squares below record.
Sections over X, applied degreewise to a cochain complex of sheaves.
Equations
Instances For
The Čech bicomplex C^{p,q} = Čech^p(U, K^q) of a cochain complex of sheaves.
Equations
Instances For
The injective Čech bicomplex reads its resolution only through the underlying complex.
The sections complex of an injective resolution reads it only through the underlying complex.
A morphism of cochain complexes of sheaves induces a morphism of Čech bicomplexes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A morphism of cochain complexes of sheaves induces a morphism of sections complexes.
Equations
Instances For
Global sections of a complex of sheaves map to its degree-zero Čech column.
Equations
- CategoryTheory.Sheaf.sectionsToCechZeroColumn hT U K = { f := fun (q : ℤ) => CategoryTheory.Sheaf.globalSectionsToCechZeroInt hT U (K.X q), comm' := ⋯ }
Instances For
The degree-zero Čech column map of an injective resolution reads it only through the underlying complex.
The degree-zero Čech column map commutes with an arbitrary morphism of complexes.
The augmented row map from the global-sections complex, placed in Čech degree zero, to the full Čech bicomplex of a cochain complex of sheaves.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The augmented bicomplex map of an injective resolution reads it only through the underlying complex.
The augmented bicomplex map commutes with an arbitrary morphism of complexes.
The global-sections complex maps to the Čech total complex of a cochain complex of sheaves.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The comparison into the Čech total complex reads an injective resolution only through the underlying complex.
The comparison into the Čech total complex commutes with an arbitrary morphism of complexes.
The bicomplex augmentation induced by an augmentation of a cochain complex of sheaves.
Instances For
The augmentation source of the Čech bicomplex is the Čech bicomplex of the complex concentrated in degree zero.
The augmentation of the Čech bicomplex of an injective resolution is the augmentation
induced by I.ι'.
The identification of the total complex of the augmentation source with the ordinary Čech complex is natural in the sheaf.
The induced map of Čech bicomplexes is functorial.
Inverse form of cechInjectiveBicomplexAugmentationSourceTotalIso_naturality.
The comparison from the ordinary Čech complex into the Čech total complex of an augmented cochain complex of sheaves.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Čech-to-total comparison of an injective resolution reads it only through the underlying complex and its augmentation.
The Čech-to-total comparison commutes with a morphism of augmented complexes.
The degreewise identification between the integer-extended Čech complex and ordinary Čech cohomology is natural in the sheaf.
The universe-lifting identification of sections complexes is natural in the complex.
The terminal-object comparison between H' and H is natural in the sheaf.
Sections over X of a cochain complex of sheaves, lifted to the universe in which
morphisms of sheaves live.
Equations
Instances For
In each degree, cochains from the free abelian representable sheaf are sections.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Degreewise, the resolution-specific identification is the general one: the construction never sees the resolution, only its underlying complex.
The Hom complex from the free abelian representable sheaf is the sections complex.
Equations
Instances For
The same at the level of complexes, which is what the naturality square below is stated against.
Post-composing a cochain out of a single complex with a morphism of complexes.
The identification of the Hom complex with the sections complex is natural in the complex.
The lifted sections complex of an injective resolution reads it only through the underlying complex.
The map on H' induced by a morphism of sheaves is post-composition in Ext.
The identification of the cohomology of the sections of an injective resolution with H'
commutes with a morphism of sheaves, once that morphism is lifted to the resolutions.
The Čech-to-sections half of the comparison commutes with a morphism of sheaves, once that morphism is lifted to the resolutions.
Each of the four factors is the homology of an explicit chain map or its inverse, so each
square is the image under homologyMap of a square of chain maps proved earlier in this
file.
The Čech-to-derived comparison commutes with a morphism of sheaves.
This is what the bare existential form cannot state. A scalar action on cohomology is the map
induced by an endomorphism of the sheaf, so k-linearity of the comparison is this square at
φ = multiplication by a scalar, with Φ any lift of it to the resolutions.
The HasExt witness is passed positionally throughout, for the reason recorded across this
lane: HasExt.{u} and HasExt.{u + 1} name different groups, and instance search must not be
allowed to choose.