Čech complexes along a functor into a thin category

Let G : C ⥤ D be a functor between categories with finite products, where D is thin, for instance a monotone map between posets of open subsets. For a family U : ι → C and a presheaf Q : Dᵒᵖ ⥤ A, the Čech complex of the pulled-back presheaf G.op ⋙ Q for U has terms Q(G(U (a 0) × ⋯ × U (a n))), while the Čech complex of Q for the family G ∘ U has terms Q(G (U (a 0)) × ⋯ × G (U (a n))). There is always a map G(U (a 0) × ⋯ × U (a n)) ⟶ G (U (a 0)) × ⋯ × G (U (a n)); when there is also a map in the reverse direction G (U (a 0)) × ⋯ × G (U (a n)) ⟶ G(U (a 0) × ⋯ × U (a n)), the two objects are isomorphic in the thin category D, and the two Čech complexes are isomorphic (cechComplexCompIso). If moreover G sends the terminal object T of C to a terminal object of D, this isomorphism is compatible with the augmentations, so one augmented Čech complex is exact if and only if the other is.

For open covers this compares the restriction of a cover to an open with a cover in a smaller poset: for an open Y ⊆ W, the presheaf F(Y ∩ -) on the opens contained in W is pulled back from the opens contained in Y along V ↦ Y ∩ V, which preserves intersections.

Main definitions

• TauCeti.CategoryTheory.cechComplexCompIso: the isomorphism between the Čech complex of Q for G ∘ U and the Čech complex of G.op ⋙ Q for U.

Main results

• TauCeti.CategoryTheory.cechComplexFunctor_map_comp_cechComplexCompIso_hom: this isomorphism is natural in the presheaf.
• TauCeti.CategoryTheory.cechComplexMap_comp_cechComplexCompIso_hom: this isomorphism commutes with refinement maps, retaining their actual index functions.
• TauCeti.CategoryTheory.cechComplexMapHomotopy_hom_comp_cechComplexCompIso_hom: this isomorphism carries the homotopy between the maps induced by two refinement maps to the corresponding homotopy.
• TauCeti.CategoryTheory.cechAugmentation_comp_cechComplexCompIso_hom: this isomorphism is compatible with the augmentations.
• TauCeti.CategoryTheory.quasiIso_cechAugmentation_op_comp_iff: the augmented Čech complex of G.op ⋙ Q for U is exact if and only if the one of Q for G ∘ U is.

The two Čech complexes are isomorphic

The degree n term of a Čech complex is, up to unfolding, a product indexed by a : Fin (n + 1) → ι (cechXIso); the differential is the alternating sum of the restrictions along the coface maps (cechComplexFunctor_obj_d_comp_π). The isomorphism of Čech complexes acts on the factor indexed by a through Q applied to the comparison isomorphism G(U (a 0) × ⋯ × U (a n)) ≅ G (U (a 0)) × ⋯ × G (U (a n)) (prodIso); it commutes with the differentials because all the morphisms of D with the same ends agree.

noncomputable def TauCeti.CategoryTheory.cechComplexCompIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasFiniteProducts D] [Quiver.IsThin D] (G : CategoryTheory.Functor C D) (U : ι → C) (Q : CategoryTheory.Functor Dᵒᵖ A) (hG : ∀ (n : ℕ) (a : Fin (n + 1) → ι), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (U (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) : (CategoryTheory.cechComplexFunctor fun (i : ι) => G.obj (U i)).obj Q ≅ (CategoryTheory.cechComplexFunctor U).obj (G.op.comp Q)

The Čech complex of Q for the family G ∘ U is isomorphic to the Čech complex of G.op ⋙ Q for U, provided each product G (U (a 0)) × ⋯ × G (U (a n)) maps to G(U (a 0) × ⋯ × U (a n)). In degree n it acts on the factor indexed by a through Q applied to the canonical map G(U (a 0) × ⋯ × U (a n)) ⟶ G (U (a 0)) × ⋯ × G (U (a n)) (cechComplexCompIso_hom_f_π).

theorem TauCeti.CategoryTheory.cechComplexCompIso_hom_f_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasFiniteProducts D] [Quiver.IsThin D] (G : CategoryTheory.Functor C D) (U : ι → C) (Q : CategoryTheory.Functor Dᵒᵖ A) (hG : ∀ (n : ℕ) (a : Fin (n + 1) → ι), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (U (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) (n : ℕ) (a : Fin (n + 1) → ι) : CategoryTheory.CategoryStruct.comp ((cechComplexCompIso G U Q hG).hom.f n) (CategoryTheory.Limits.Pi.π (fun (i : (Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := n })).I) => (G.op.comp Q).obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := n })).obj i))) a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun (i : (Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := fun (i : ι) => G.obj (U i) }.cech).obj { len := n })).I) => Q.obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := fun (i : ι) => G.obj (U i) }.cech).obj { len := n })).obj i))) a) (Q.map (CategoryTheory.Limits.Pi.lift fun (j : Fin (n + 1)) => G.map (CategoryTheory.Limits.Pi.π (fun (j : Fin (n + 1)) => U (a j)) j)).op)

The factor of (cechComplexCompIso G U Q hG).hom.f n indexed by a is Q applied to the canonical map G(U (a 0) × ⋯ × U (a n)) ⟶ G (U (a 0)) × ⋯ × G (U (a n)).

theorem TauCeti.CategoryTheory.cechComplexCompIso_hom_f_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasFiniteProducts D] [Quiver.IsThin D] (G : CategoryTheory.Functor C D) (U : ι → C) (Q : CategoryTheory.Functor Dᵒᵖ A) (hG : ∀ (n : ℕ) (a : Fin (n + 1) → ι), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (U (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) (n : ℕ) (a : Fin (n + 1) → ι) {Z : A} (h : Q.obj (G.op.obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := n })).obj a))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((cechComplexCompIso G U Q hG).hom.f n) (CategoryTheory.Limits.Pi.π (fun (i : (Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := n })).I) => Q.obj (G.op.obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := n })).obj i)))) a)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun (i : (Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := fun (i : ι) => G.obj (U i) }.cech).obj { len := n })).I) => Q.obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := fun (i : ι) => G.obj (U i) }.cech).obj { len := n })).obj i))) a) (Q.map (CategoryTheory.Limits.Pi.lift fun (j : Fin (n + 1)) => G.map (CategoryTheory.Limits.Pi.π (fun (j : Fin (n + 1)) => U (a j)) j)).op)) h

The factor of (cechComplexCompIso G U Q hG).hom.f n indexed by a is Q applied to the canonical map G(U (a 0) × ⋯ × U (a n)) ⟶ G (U (a 0)) × ⋯ × G (U (a n)).

theorem TauCeti.CategoryTheory.cechComplexFunctor_map_comp_cechComplexCompIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasFiniteProducts D] [Quiver.IsThin D] (G : CategoryTheory.Functor C D) (U : ι → C) (Q : CategoryTheory.Functor Dᵒᵖ A) (hG : ∀ (n : ℕ) (a : Fin (n + 1) → ι), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (U (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) {Q' : CategoryTheory.Functor Dᵒᵖ A} (β : Q ⟶ Q') : CategoryTheory.CategoryStruct.comp ((CategoryTheory.cechComplexFunctor fun (i : ι) => G.obj (U i)).map β) (cechComplexCompIso G U Q' hG).hom = CategoryTheory.CategoryStruct.comp (cechComplexCompIso G U Q hG).hom ((CategoryTheory.cechComplexFunctor U).map (G.op.whiskerLeft β))

The isomorphism of Čech complexes cechComplexCompIso is natural in the presheaf Q.

theorem TauCeti.CategoryTheory.cechComplexFunctor_map_comp_cechComplexCompIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasFiniteProducts D] [Quiver.IsThin D] (G : CategoryTheory.Functor C D) (U : ι → C) (Q : CategoryTheory.Functor Dᵒᵖ A) (hG : ∀ (n : ℕ) (a : Fin (n + 1) → ι), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (U (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) {Q' : CategoryTheory.Functor Dᵒᵖ A} (β : Q ⟶ Q') {Z : CochainComplex A ℕ} (h : (CategoryTheory.cechComplexFunctor U).obj (G.op.comp Q') ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.cechComplexFunctor fun (i : ι) => G.obj (U i)).map β) (CategoryTheory.CategoryStruct.comp (cechComplexCompIso G U Q' hG).hom h) = CategoryTheory.CategoryStruct.comp (cechComplexCompIso G U Q hG).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.cechComplexFunctor U).map (G.op.whiskerLeft β)) h)

The isomorphism of Čech complexes cechComplexCompIso is natural in the presheaf Q.

theorem TauCeti.CategoryTheory.cechComplexMap_comp_cechComplexCompIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasFiniteProducts D] [Quiver.IsThin D] (G : CategoryTheory.Functor C D) (U : ι → C) (Q : CategoryTheory.Functor Dᵒᵖ A) (hG : ∀ (n : ℕ) (a : Fin (n + 1) → ι), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (U (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) {κ : Type w} {V : κ → C} (φ : { I := ι, obj := U } ⟶ { I := κ, obj := V }) (hV : ∀ (n : ℕ) (a : Fin (n + 1) → κ), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (V (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => V (a j)))) : CategoryTheory.CategoryStruct.comp (cechComplexMap Q { f := φ.f, φ := fun (i : { I := ι, obj := fun (i : ι) => G.obj (U i) }.I) => G.map (φ.φ i) }) (cechComplexCompIso G U Q hG).hom = CategoryTheory.CategoryStruct.comp (cechComplexCompIso G V Q hV).hom (cechComplexMap (G.op.comp Q) φ)

The comparison along G commutes with actual refinement functions, including ones that repeat or identify indices.

theorem TauCeti.CategoryTheory.cechComplexMap_comp_cechComplexCompIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasFiniteProducts D] [Quiver.IsThin D] (G : CategoryTheory.Functor C D) (U : ι → C) (Q : CategoryTheory.Functor Dᵒᵖ A) (hG : ∀ (n : ℕ) (a : Fin (n + 1) → ι), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (U (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) {κ : Type w} {V : κ → C} (φ : { I := ι, obj := U } ⟶ { I := κ, obj := V }) (hV : ∀ (n : ℕ) (a : Fin (n + 1) → κ), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (V (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => V (a j)))) {Z : CochainComplex A ℕ} (h : (CategoryTheory.cechComplexFunctor U).obj (G.op.comp Q) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cechComplexMap Q { f := φ.f, φ := fun (i : ι) => G.map (φ.φ i) }) (CategoryTheory.CategoryStruct.comp (cechComplexCompIso G U Q hG).hom h) = CategoryTheory.CategoryStruct.comp (cechComplexCompIso G V Q hV).hom (CategoryTheory.CategoryStruct.comp (cechComplexMap (G.op.comp Q) φ) h)

The comparison along G commutes with actual refinement functions, including ones that repeat or identify indices.

theorem TauCeti.CategoryTheory.cechComplexMapHomotopy_hom_comp_cechComplexCompIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasFiniteProducts D] [Quiver.IsThin D] (G : CategoryTheory.Functor C D) (U : ι → C) (Q : CategoryTheory.Functor Dᵒᵖ A) (hG : ∀ (n : ℕ) (a : Fin (n + 1) → ι), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (U (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) {κ : Type w} {V : κ → C} (φ ψ : { I := ι, obj := U } ⟶ { I := κ, obj := V }) (hV : ∀ (n : ℕ) (a : Fin (n + 1) → κ), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (V (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => V (a j)))) (i j : ℕ) : CategoryTheory.CategoryStruct.comp ((cechComplexMapHomotopy Q { f := φ.f, φ := fun (i : { I := ι, obj := fun (i : ι) => G.obj (U i) }.I) => G.map (φ.φ i) } { f := ψ.f, φ := fun (i : { I := ι, obj := fun (i : ι) => G.obj (U i) }.I) => G.map (ψ.φ i) }).hom i j) ((cechComplexCompIso G U Q hG).hom.f j) = CategoryTheory.CategoryStruct.comp ((cechComplexCompIso G V Q hV).hom.f i) ((cechComplexMapHomotopy (G.op.comp Q) φ ψ).hom i j)

The comparison along G carries the homotopy between the maps induced by two refinement maps φ and ψ (cechComplexMapHomotopy) for Q and the family G ∘ U to the corresponding homotopy for G.op ⋙ Q and the family U.

theorem TauCeti.CategoryTheory.cechComplexMapHomotopy_hom_comp_cechComplexCompIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasFiniteProducts D] [Quiver.IsThin D] (G : CategoryTheory.Functor C D) (U : ι → C) (Q : CategoryTheory.Functor Dᵒᵖ A) (hG : ∀ (n : ℕ) (a : Fin (n + 1) → ι), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (U (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) {κ : Type w} {V : κ → C} (φ ψ : { I := ι, obj := U } ⟶ { I := κ, obj := V }) (hV : ∀ (n : ℕ) (a : Fin (n + 1) → κ), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (V (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => V (a j)))) (i j : ℕ) {Z : A} (h : ((CategoryTheory.cechComplexFunctor U).obj (G.op.comp Q)).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cechComplexMapHomotopy Q { f := φ.f, φ := fun (i : ι) => G.map (φ.φ i) } { f := ψ.f, φ := fun (i : ι) => G.map (ψ.φ i) }).hom i j) (CategoryTheory.CategoryStruct.comp ((cechComplexCompIso G U Q hG).hom.f j) h) = CategoryTheory.CategoryStruct.comp ((cechComplexCompIso G V Q hV).hom.f i) (CategoryTheory.CategoryStruct.comp ((cechComplexMapHomotopy (G.op.comp Q) φ ψ).hom i j) h)

The comparison along G carries the homotopy between the maps induced by two refinement maps φ and ψ (cechComplexMapHomotopy) for Q and the family G ∘ U to the corresponding homotopy for G.op ⋙ Q and the family U.

theorem TauCeti.CategoryTheory.cechAugmentation_comp_cechComplexCompIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasFiniteProducts D] [Quiver.IsThin D] (G : CategoryTheory.Functor C D) (U : ι → C) (Q : CategoryTheory.Functor Dᵒᵖ A) (hG : ∀ (n : ℕ) (a : Fin (n + 1) → ι), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (U (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) [CategoryTheory.Limits.HasZeroObject A] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (hGT : CategoryTheory.Limits.IsTerminal (G.obj T)) : CategoryTheory.CategoryStruct.comp (cechAugmentation (fun (i : ι) => G.obj (U i)) hGT Q) (cechComplexCompIso G U Q hG).hom = cechAugmentation U hT (G.op.comp Q)

If G sends the terminal object T of C to a terminal object, the isomorphism of Čech complexes cechComplexCompIso is compatible with the augmentations.

theorem TauCeti.CategoryTheory.cechAugmentation_comp_cechComplexCompIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasFiniteProducts D] [Quiver.IsThin D] (G : CategoryTheory.Functor C D) (U : ι → C) (Q : CategoryTheory.Functor Dᵒᵖ A) (hG : ∀ (n : ℕ) (a : Fin (n + 1) → ι), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (U (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) [CategoryTheory.Limits.HasZeroObject A] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (hGT : CategoryTheory.Limits.IsTerminal (G.obj T)) {Z : CochainComplex A ℕ} (h : (CategoryTheory.cechComplexFunctor U).obj (G.op.comp Q) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cechAugmentation (fun (i : ι) => G.obj (U i)) hGT Q) (CategoryTheory.CategoryStruct.comp (cechComplexCompIso G U Q hG).hom h) = CategoryTheory.CategoryStruct.comp (cechAugmentation U hT (G.op.comp Q)) h

If G sends the terminal object T of C to a terminal object, the isomorphism of Čech complexes cechComplexCompIso is compatible with the augmentations.

theorem TauCeti.CategoryTheory.quasiIso_cechAugmentation_op_comp_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.Limits.HasFiniteProducts D] [Quiver.IsThin D] (G : CategoryTheory.Functor C D) (U : ι → C) (Q : CategoryTheory.Functor Dᵒᵖ A) (hG : ∀ (n : ℕ) (a : Fin (n + 1) → ι), Nonempty ((∏ᶜ fun (j : Fin (n + 1)) => G.obj (U (a j))) ⟶ G.obj (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) [CategoryTheory.Limits.HasZeroObject A] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (hGT : CategoryTheory.Limits.IsTerminal (G.obj T)) [CategoryTheory.CategoryWithHomology A] : QuasiIso (cechAugmentation U hT (G.op.comp Q)) ↔ QuasiIso (cechAugmentation (fun (i : ι) => G.obj (U i)) hGT Q)

Čech complexes along a functor into a thin category. Let G : C ⥤ D be a functor between categories with finite products, with D thin, let U be a family in C and let Q be a presheaf on D with values in an abelian category. Suppose that G sends the terminal object T of C to a terminal object, and that each product G (U (a 0)) × ⋯ × G (U (a n)) maps to G(U (a 0) × ⋯ × U (a n)). Then the augmented Čech complex of G.op ⋙ Q for U is exact if and only if the augmented Čech complex of Q for the family G ∘ U is.