The Čech differential in coordinates

Mathlib defines the Čech complex of a presheaf as alternatingCofaceMapComplex applied to the cosimplicial object attached to the Čech nerve of a formal coproduct. That definition is compact but says nothing directly about components: it never names the index of a cochain, nor the restriction that carries a face into it.

This file supplies that reading. cechComplexFunctor_delta_π computes one coface at one index, and cechComplexFunctor_d_π assembles the alternating sum. Both are statements about Mathlib's construction, so they live in Mathlib's namespace.

Main statements

• cechComplexFunctor_delta_π — the j-th coface, projected at x, is the projection at the face x ∘ j.succAbove followed by the presheaf on the face inclusion;
• cechComplexFunctor_d_π — the differential, projected at x, is the alternating sum of those;
• cechComplexFunctor_map_f_π — the map induced by a morphism of presheaves, projected at x, is the projection at x followed by that morphism on the intersection.

Implementation notes

The projections are stated in the shape Mathlib's construction produces, indexed by ToType (mk n) → ι with the object written through the Čech nerve rather than as ∏ᶜ (U ∘ x). A caller-friendly restatement belongs downstream, together with the identification of the intersection.

Both proofs finish with exact rather than rw. The two sides differ in the HasProduct instance argument that Pi.π carries, which rw will not see through but definitional unification will. Rewriting with Pi.lift_π fails here for that reason alone.

Fin.succAbove needs no reindexing lemma: SimplexCategory.δ j has toOrderHom = Fin.succAbove j, so this is the shape the Čech nerve already produces via FormalCoproduct.mapPower.

@[reducible, inline]

noncomputable abbrev CategoryTheory.cechNerve {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] {ι : Type w} (U : ι → C) : SimplicialObject (Limits.FormalCoproduct C)

The Čech nerve of the family U, as a simplicial formal coproduct.

Equations

• CategoryTheory.cechNerve U = { I := ι, obj := U }.cech

@[reducible, inline]

noncomputable abbrev CategoryTheory.cechCosimplicial {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] [Limits.HasFiniteProducts C] {ι : Type w} (U : ι → C) (P : Functor Cᵒᵖ A) : CosimplicialObject A

The Čech cosimplicial object of a presheaf against the nerve of U.

Equations

• CategoryTheory.cechCosimplicial U P = (CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor (CategoryTheory.cechNerve U)).obj P

@[reducible, inline]

noncomputable abbrev CategoryTheory.cechTermFamily {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasFiniteProducts C] {ι : Type w} (U : ι → C) (P : Functor Cᵒᵖ A) (n : ℕ) : (ToType { len := n } → ι) → A

Degree-n Čech cochains, in the shape Mathlib's construction produces.

Equations

• CategoryTheory.cechTermFamily U P n x = P.obj (Opposite.op (((CategoryTheory.cechNerve U).obj (Opposite.op { len := n })).obj x))

theorem CategoryTheory.cechComplexFunctor_delta_π {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] [Limits.HasFiniteProducts C] {ι : Type w} (U : ι → C) (P : Functor Cᵒᵖ A) {n : ℕ} (j : Fin (n + 2)) (x : ToType { len := n + 1 } → ι) : CategoryStruct.comp ((cechCosimplicial U P).δ j) (Limits.Pi.π (cechTermFamily U P (n + 1)) x) = CategoryStruct.comp (Limits.Pi.π (cechTermFamily U P n) (((cechNerve U).map (SimplexCategory.δ j).op).f x)) (P.map (((cechNerve U).map (SimplexCategory.δ j).op).φ x).op)

The j-th coface, projected at the index x, is the projection at the face index (cech.map (δ j).op).f x = x ∘ j.succAbove followed by the presheaf on the face inclusion.

Preadditivity plays no part here — only the alternating sum in cechComplexFunctor_d_π needs it.

theorem CategoryTheory.cechComplexFunctor_map_f_π {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] [Limits.HasFiniteProducts C] [Preadditive A] {ι : Type w} (U : ι → C) {F G : Functor Cᵒᵖ A} (φ : F ⟶ G) (n : ℕ) (x : ToType { len := n } → ι) : CategoryStruct.comp (((cechComplexFunctor U).map φ).f n) (Limits.Pi.π (cechTermFamily U G n) x) = CategoryStruct.comp (Limits.Pi.π (cechTermFamily U F n) x) (φ.app (Opposite.op (((cechNerve U).obj (Opposite.op { len := n })).obj x)))

The map a morphism of presheaves induces on Čech cochains, projected at the index x, is the projection at x followed by the morphism on that intersection.

evalOp sends a morphism to Pi.map componentwise, so once the two sides are recognised as a Pi.map and its projection this is Pi.map_π. The recognition is rfl rather than a rewrite: cechComplexFunctor reaches evalOp through two functor compositions, and only definitional unfolding crosses them.

Unlike cechComplexFunctor_delta_π this cannot omit Preadditive A: it names cechComplexFunctor itself, whose target CochainComplex A ℕ needs the zero morphisms.

theorem CategoryTheory.cechComplexFunctor_d_π {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [Limits.HasProducts A] [Limits.HasFiniteProducts C] [Preadditive A] {ι : Type w} (U : ι → C) (P : Functor Cᵒᵖ A) {n : ℕ} (x : ToType { len := n + 1 } → ι) : CategoryStruct.comp (((cechComplexFunctor U).obj P).d n (n + 1)) (Limits.Pi.π (cechTermFamily U P (n + 1)) x) = ∑ j : Fin (n + 2), (-1) ^ ↑j • CategoryStruct.comp (Limits.Pi.π (cechTermFamily U P n) (((cechNerve U).map (SimplexCategory.δ j).op).f x)) (P.map (((cechNerve U).map (SimplexCategory.δ j).op).φ x).op)

The Čech differential, projected at the index x, is the alternating sum of the face restrictions. This is the formula a concrete computation of Hⁱ consumes.