The ordered Čech complex of a functor on finite sets #
Let ι be a linearly ordered type and let F : (Finset ι)ᵒᵖ ⥤ C be a functor to a preadditive
category with coproducts, so that F assigns an object F(s) to every finite set s of indices
and a restriction F(s) ⟶ F(t) to every inclusion t ⊆ s. The ordered Čech complex of F is the
chain complex whose degree p term is the coproduct of the F(s) over the sets
s = {i₀ < ⋯ < iₚ} with p + 1 elements, and whose differential is the alternating sum
d = ∑ₖ (-1)ᵏ rₖ of the restrictions rₖ : F({i₀ < ⋯ < iₚ}) ⟶ F({i₀ < ⋯ < îₖ < ⋯ < iₚ}).
In terms of the deleted index i ∈ s, the sign is (-1) to the number of elements of s below
i.
The main example is a covariant theory evaluated on the finite intersections of an open cover
U : ι → Opens X, s ↦ C(⋂_{i ∈ s} U i): for singular chains this gives the Čech double complex
of the cover. Unlike Mathlib's Čech complex CategoryTheory.cechComplexFunctor, which is indexed
by all tuples Fin (p + 1) → ι, the ordered complex only involves strictly increasing tuples, so
it vanishes above the cardinality of a finite index type. The value F(∅) receives the
augmentation ∑ᵢ F({i}) ⟶ F(∅).
Main definitions #
CategoryTheory.Functor.orderedCechComplex F: the ordered Čech complex ofF; its terms are coproducts (Functor.isColimitOrderedCechComplexCofan), its differential is characterised on summands byFunctor.ι_orderedCechComplex_d, and it vanishes from the cardinality of a finite index type on (Functor.isZero_orderedCechComplex_X).CategoryTheory.orderedCechComplexFunctor C ι: the ordered Čech complex as a functor ofF.CategoryTheory.Functor.orderedCechAugmentation F: the augmentation toF(∅), placed in degree0, which restricts each summandF({i})toF(∅).
References #
- R. Bott and L. W. Tu, Differential Forms in Algebraic Topology, Graduate Texts in Mathematics 82, Springer, 1982, §8 (the generalized Mayer–Vietoris principle).
The ordered Čech complex of a functor F on finite sets of indices: in degree p it is the
coproduct of the F(s) over the sets s = {i₀ < ⋯ < iₚ} with p + 1 elements, with differential
∑ₖ (-1)ᵏ times the restriction deleting iₖ. It is characterised by the inclusions
Functor.orderedCechComplexι of the summands, which are a coproduct cocone, and by
Functor.ι_orderedCechComplex_d.
Instances For
The inclusion of the summand F(s) into the degree p term of the ordered Čech complex, for
a set s with p + 1 elements.
Instances For
The morphism out of the degree p term of the ordered Čech complex given on each summand.
Instances For
The morphism Functor.orderedCechComplexDesc f restricts to f s on the summand F(s).
The morphism Functor.orderedCechComplexDesc f restricts to f s on the summand F(s).
The summand inclusions Functor.orderedCechComplexι exhibit the degree p term of the ordered
Čech complex as the coproduct of the F(s) over the sets s with p + 1 elements.
Instances For
Morphisms out of a term of the ordered Čech complex agree when they agree on every summand.
The ordered Čech complex vanishes in the degrees p at least the cardinality of a finite index
type, as there is no set of p + 1 indices.
The ordered Čech differential on the summand of s = {i₀ < ⋯ < iₚ₊₁} is the alternating sum
of the restrictions deleting one index i, with sign (-1) to the number of elements of s
below i.
The ordered Čech differential on the summand of s = {i₀ < ⋯ < iₚ₊₁} is the alternating sum
of the restrictions deleting one index i, with sign (-1) to the number of elements of s
below i.
On the summand of a pair {a < b}, the ordered Čech differential is the restriction to F({b})
minus the restriction to F({a}).
On the summand of a pair {a < b}, the ordered Čech differential is the restriction to F({b})
minus the restriction to F({a}).
The augmentation of the ordered Čech complex: the summand F({i}) of the degree 0 term is
restricted to F(∅). It vanishes on the boundaries
(Functor.orderedCechComplex_d_comp_orderedCechAugmentation), so it augments the complex by
F(∅) in the sense of ChainComplex.augment.
Instances For
The augmentation restricts the summand F({i}) of the degree 0 term to F(∅).
The augmentation restricts the summand F({i}) of the degree 0 term to F(∅).
The augmentation vanishes on the boundaries.
The augmentation vanishes on the boundaries.
The chain map of ordered Čech complexes induced by a natural transformation, acting summand by
summand (NatTrans.ι_orderedCechComplexMap_f).
Instances For
The chain map induced by α restricts to α on the summand F(s).
The chain map induced by α restricts to α on the summand F(s).
The augmentation is natural in F.
The augmentation is natural in F.
The ordered Čech complex Functor.orderedCechComplex as a functor of F.