Forgetting module-valued Čech complexes

The Čech complex of the underlying additive-group-valued presheaf is canonically the result of forgetting the module-valued Čech complex.

noncomputable def CategoryTheory.evalOpForget₂AddCommGrpIso {C : Type u} [Category.{u_1, u} C] [Limits.HasFiniteProducts C] {R : CommRingCat} (P : Functor Cᵒᵖ (ModuleCat ↑R)) : ((Limits.FormalCoproduct.evalOp C (ModuleCat ↑R)).obj P).comp (forget₂ (ModuleCat ↑R) AddCommGrpCat) ≅ (Limits.FormalCoproduct.evalOp C AddCommGrpCat).obj (P.comp (forget₂ (ModuleCat ↑R) AddCommGrpCat))

Evaluation on a formal coproduct commutes with forgetting a module to its underlying additive group. The components are the canonical product-comparison isomorphisms.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.map_alternatingCofaceMapComplex {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] : (AlgebraicTopology.alternatingCofaceMapComplex C).comp (F.mapHomologicalComplex (ComplexShape.up ℕ)) = ((CosimplicialObject.whiskering C D).obj F).comp (AlgebraicTopology.alternatingCofaceMapComplex D)

Additive functors commute with the alternating-coface-map complex.

noncomputable def CategoryTheory.cechComplexForget₂AddCommGrpIso {C : Type u} [Category.{u_1, u} C] [Limits.HasFiniteProducts C] {R : CommRingCat} {I : Type u} (U : I → C) (P : Functor Cᵒᵖ (ModuleCat ↑R)) : ((forget₂ (ModuleCat ↑R) AddCommGrpCat).mapHomologicalComplex (ComplexShape.up ℕ)).obj ((cechComplexFunctor U).obj P) ≅ (cechComplexFunctor U).obj (P.comp (forget₂ (ModuleCat ↑R) AddCommGrpCat))

The Čech complex of an underlying additive-group-valued presheaf is canonically the forgotten module-valued Čech complex.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.cechComplex_exactAt_forget₂AddCommGrp_of_exactAt {C : Type u} [Category.{u_1, u} C] [Limits.HasFiniteProducts C] {R : CommRingCat} {I : Type u} (U : I → C) (P : Functor Cᵒᵖ (ModuleCat ↑R)) (n : ℕ) (h : HomologicalComplex.ExactAt ((cechComplexFunctor U).obj P) n) : HomologicalComplex.ExactAt ((cechComplexFunctor U).obj (P.comp (forget₂ (ModuleCat ↑R) AddCommGrpCat))) n

Exactness of a module-valued Čech complex passes to the Čech complex of the underlying additive-group-valued presheaf.