Čech complexes under a change of coefficients

Let F : A ⥤ B be an additive functor between preadditive categories with products, and let U : ι → C be a family in a category with finite products. The degree n term of the Čech complex Č(U, P) of a presheaf P : Cᵒᵖ ⥤ A is a product indexed by Fin (n + 1) → ι. If F preserves these products, then applying F termwise to Č(U, P) gives the Čech complex Č(U, P ⋙ F), naturally in P (TauCeti.CategoryTheory.cechComplexFunctorMapIso).

Typical uses are the forgetful functor from modules over a ring to abelian groups, which preserves all products, and an additive functor such as extension of scalars, which preserves finite products, for a finite family U. For instance, the Čech complex of a presheaf of modules is a complex of modules whose underlying complex of abelian groups is the Čech complex of the underlying presheaf of abelian groups.

When A is linear over a ring R, the Čech complex functor is R-linear (TauCeti.CategoryTheory.cechComplexFunctor_linear): multiplying a morphism of presheaves by a scalar multiplies the induced map of Čech complexes by that scalar.

Main definitions

• TauCeti.CategoryTheory.cechComplexFunctorMapIso: the natural isomorphism between F applied to the Čech complex of P and the Čech complex of P ⋙ F.

Main results

• TauCeti.CategoryTheory.cechComplexFunctorMapIso_hom_app_f_π: its factors are the images under F of the projections of the products.
• TauCeti.CategoryTheory.cechComplexFunctorMapIso_hom_app_comp_cechComplexMap: it commutes with the maps induced by morphisms of families.
• TauCeti.CategoryTheory.cechComplexFunctor_linear: the Čech complex functor is linear.

noncomputable def TauCeti.CategoryTheory.cechComplexFunctorMapIso {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] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Preadditive B] [CategoryTheory.Limits.HasProducts B] {ι : Type w} (U : ι → C) (F : CategoryTheory.Functor A B) [∀ (n : ℕ), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete (Fin (n + 1) → ι)) F] [F.Additive] : (CategoryTheory.cechComplexFunctor U).comp (F.mapHomologicalComplex (ComplexShape.up ℕ)) ≅ ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.cechComplexFunctor U)

Čech complexes under a change of coefficients. For an additive functor F : A ⥤ B preserving the products indexed by Fin (n + 1) → ι for every n, applying F to the Čech complex of a presheaf P for the family U gives the Čech complex of P ⋙ F, naturally in P. Its factors are the images under F of the projections of the products (cechComplexFunctorMapIso_hom_app_f_π).

theorem TauCeti.CategoryTheory.cechComplexFunctorMapIso_hom_app_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] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Preadditive B] [CategoryTheory.Limits.HasProducts B] {ι : Type w} (U : ι → C) (F : CategoryTheory.Functor A B) [∀ (n : ℕ), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete (Fin (n + 1) → ι)) F] [F.Additive] (P : CategoryTheory.Functor Cᵒᵖ A) (n : ℕ) (a : Fin (n + 1) → ι) : CategoryTheory.CategoryStruct.comp (((cechComplexFunctorMapIso U F).hom.app P).f n) (CategoryTheory.Limits.Pi.π (fun (i : (Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := n })).I) => (((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).obj P).obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := n })).obj i))) a) = F.map (CategoryTheory.Limits.Pi.π (fun (a : Fin (n + 1) → ι) => P.obj (Opposite.op (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) a)

The factor indexed by a of the degree n component of cechComplexFunctorMapIso is the image under F of the projection onto the factor indexed by a.

theorem TauCeti.CategoryTheory.cechComplexFunctorMapIso_hom_app_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] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Preadditive B] [CategoryTheory.Limits.HasProducts B] {ι : Type w} (U : ι → C) (F : CategoryTheory.Functor A B) [∀ (n : ℕ), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete (Fin (n + 1) → ι)) F] [F.Additive] (P : CategoryTheory.Functor Cᵒᵖ A) (n : ℕ) (a : Fin (n + 1) → ι) {Z : B} (h : (((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).obj P).obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := n })).obj a)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (((cechComplexFunctorMapIso U F).hom.app P).f n) (CategoryTheory.Limits.Pi.π (fun (i : (Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := n })).I) => (((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).obj P).obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := n })).obj i))) a)) h = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.Pi.π (fun (a : Fin (n + 1) → ι) => P.obj (Opposite.op (∏ᶜ fun (j : Fin (n + 1)) => U (a j)))) a)) h

The factor indexed by a of the degree n component of cechComplexFunctorMapIso is the image under F of the projection onto the factor indexed by a.

theorem TauCeti.CategoryTheory.cechComplexFunctorMapIso_hom_app_comp_cechComplexMap {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] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Preadditive B] [CategoryTheory.Limits.HasProducts B] {ι : Type w} (U : ι → C) (F : CategoryTheory.Functor A B) [∀ (n : ℕ), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete (Fin (n + 1) → ι)) F] [F.Additive] {κ : Type w} {V : κ → C} [∀ (n : ℕ), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete (Fin (n + 1) → κ)) F] (P : CategoryTheory.Functor Cᵒᵖ A) (φ : { I := ι, obj := U } ⟶ { I := κ, obj := V }) : CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (cechComplexMap P φ)) ((cechComplexFunctorMapIso U F).hom.app P) = CategoryTheory.CategoryStruct.comp ((cechComplexFunctorMapIso V F).hom.app P) (cechComplexMap (P.comp F) φ)

cechComplexFunctorMapIso commutes with refinement maps. For a morphism φ from the family U to a family V, applying F to the map Č(V, P) ⟶ Č(U, P) induced by φ and then identifying with Č(U, P ⋙ F) is identifying with Č(V, P ⋙ F) and then applying the map induced by φ.

theorem TauCeti.CategoryTheory.cechComplexFunctorMapIso_hom_app_comp_cechComplexMap_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] {B : Type u''} [CategoryTheory.Category.{v'', u''} B] [CategoryTheory.Preadditive B] [CategoryTheory.Limits.HasProducts B] {ι : Type w} (U : ι → C) (F : CategoryTheory.Functor A B) [∀ (n : ℕ), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete (Fin (n + 1) → ι)) F] [F.Additive] {κ : Type w} {V : κ → C} [∀ (n : ℕ), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete (Fin (n + 1) → κ)) F] (P : CategoryTheory.Functor Cᵒᵖ A) (φ : { I := ι, obj := U } ⟶ { I := κ, obj := V }) {Z : HomologicalComplex B (ComplexShape.up ℕ)} (h : (CategoryTheory.cechComplexFunctor U).obj (((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).obj P) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (cechComplexMap P φ)) (CategoryTheory.CategoryStruct.comp ((cechComplexFunctorMapIso U F).hom.app P) h) = CategoryTheory.CategoryStruct.comp ((cechComplexFunctorMapIso V F).hom.app P) (CategoryTheory.CategoryStruct.comp (cechComplexMap (P.comp F) φ) h)

cechComplexFunctorMapIso commutes with refinement maps. For a morphism φ from the family U to a family V, applying F to the map Č(V, P) ⟶ Č(U, P) induced by φ and then identifying with Č(U, P ⋙ F) is identifying with Č(V, P ⋙ F) and then applying the map induced by φ.

instance TauCeti.CategoryTheory.cechComplexFunctor_linear {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} (U : ι → C) (R : Type u_1) [Semiring R] [CategoryTheory.Linear R A] : CategoryTheory.Functor.Linear R (CategoryTheory.cechComplexFunctor U)

The Čech complex functor of a family is linear when the coefficient category is.