Documentation

Mathlib.CategoryTheory.Sites.SheafCohomology.Cech

Cech cohomology #

Given a family of objects U : ι → C in a category C that has finite products, we define a Cech complex functor cechComplexFunctor : (Cᵒᵖ ⥤ A) ⥤ CochainComplex A ℕ which sends a presheaf P : Cᵒᵖ ⥤ A in a preadditive category (where products exist) to the cochain complex which in degree n consists of the product, indexed by i : Fin (n + 1) → ι, of the value of P on the product of the objects U (i a) for a : Fin (n + 1).

source
noncomputable def CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [HasProducts A] (E : SimplicialObject (FormalCoproduct C)) :
Functor (Functor Cᵒᵖ A) (CosimplicialObject A)

Given a simplicial object E in the category FormalCoproduct C, this is the functor (Cᵒᵖ ⥤ A) ⥤ CosimplicialObject A which sends P : Cᵒᵖ ⥤ A to the cosimplicial object which sends ⦋n⦌ to the "evaluation" of P on E _⦋n⦌.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_map {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [HasProducts A] (E : SimplicialObject (FormalCoproduct C)) (X : Functor Cᵒᵖ A) {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) :
    ((cosimplicialObjectFunctor E).obj X).map f = Pi.lift fun (i : (E.obj (Opposite.op Y✝)).I) => CategoryStruct.comp (Pi.π (fun (i : (E.obj (Opposite.op X✝)).I) => X.obj (Opposite.op ((E.obj (Opposite.op X✝)).obj i))) ((E.map f.op).f i)) (X.map ((E.map f.op).φ i).op)
    source
    @[simp]
    theorem CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_map_app {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [HasProducts A] (E : SimplicialObject (FormalCoproduct C)) {X✝ Y✝ : Functor Cᵒᵖ A} (f : X✝ ⟶ Y✝) (X : SimplexCategory) :
    ((cosimplicialObjectFunctor E).map f).app X = Pi.map fun (i : (E.obj (Opposite.op X)).I) => f.app (Opposite.op ((E.obj (Opposite.op X)).obj i))
    source
    @[simp]
    theorem CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_obj {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [HasProducts A] (E : SimplicialObject (FormalCoproduct C)) (X : Functor Cᵒᵖ A) (X✝ : SimplexCategory) :
    ((cosimplicialObjectFunctor E).obj X).obj X✝ = ∏ᶜ fun (i : (E.obj (Opposite.op X✝)).I) => X.obj (Opposite.op ((E.obj (Opposite.op X✝)).obj i))
    source
    noncomputable def CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [HasProducts A] (E : SimplicialObject (FormalCoproduct C)) [Preadditive A] :
    Functor (Functor Cᵒᵖ A) (CochainComplex A ℕ)

    Given a simplicial object E in the category FormalCoproduct C, this is the functor (Cᵒᵖ ⥤ A) ⥤ CochainComplex A ℕ which sends P : Cᵒᵖ ⥤ A to the cochain complex which in degree n consists of the "evaluation" of P on E _⦋n⦌.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [HasProducts A] (E : SimplicialObject (FormalCoproduct C)) [Preadditive A] (X : Functor Cᵒᵖ A) (i j : ℕ) :
      ((cochainComplexFunctor E).obj X).d i j = if h : i + 1 = j then CategoryStruct.comp (∑ i_1 : Fin (i + 2), (-1) ^ ↑i_1 • ((cosimplicialObjectFunctor E).obj X).δ i_1) (eqToHom ⋯) else 0
      source
      @[simp]
      theorem CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [HasProducts A] (E : SimplicialObject (FormalCoproduct C)) [Preadditive A] (X : Functor Cᵒᵖ A) (n : ℕ) :
      ((cochainComplexFunctor E).obj X).X n = ∏ᶜ fun (i : (E.obj (Opposite.op (SimplexCategory.mk n))).I) => X.obj (Opposite.op ((E.obj (Opposite.op (SimplexCategory.mk n))).obj i))
      source
      @[simp]
      theorem CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f {C : Type u} [Category.{v, u} C] {A : Type u'} [Category.{v', u'} A] [HasProducts A] (E : SimplicialObject (FormalCoproduct C)) [Preadditive A] {X✝ Y✝ : Functor Cᵒᵖ A} (f : X✝ ⟶ Y✝) (n : ℕ) :
      ((cochainComplexFunctor E).map f).f n = Pi.map fun (i : (E.obj (Opposite.op (SimplexCategory.mk n))).I) => f.app (Opposite.op ((E.obj (Opposite.op (SimplexCategory.mk n))).obj i))
      source
      noncomputable def CategoryTheory.cechComplexFunctor {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) :
      Functor (Functor Cᵒᵖ A) (CochainComplex A ℕ)

      Given a family of objects U : ι → C, this is the Cech complex functor (Cᵒᵖ ⥤ A) ⥤ CochainComplex A ℕ which sends a presheaf P : Cᵒᵖ ⥤ A to the cochain complex which in degree n consists of the product, indexed by x : Fin (n + 1) → ι, of the value of P on the product of the objects U (x i) for i : Fin (n + 1).

      Equations
      Instances For