structure CohomologyConnection.CechToDerivedData {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] : Type (max (max (max u_1 u_2) u₁) v₁)

Bundle of data comparing a Čech-style δ-functor to a derived-functor δ-functor, with the Čech side being effaceable.

• cech : DerivedFunctorsDefs.CohomDeltaFunctor C D
• derived : DerivedFunctorsDefs.CohomDeltaFunctor C D
• cech_effaceable : self.cech.IsEffaceable

theorem CohomologyConnection.CechToDerivedData.morphisms_unique {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (data : CechToDerivedData) (m₁ m₂ : data.cech.Morphism data.derived) (h₀ : m₁.η 0 = m₂.η 0) (n : ℕ) : m₁.η n = m₂.η n

Two morphisms between the Čech and derived δ-functors agreeing in degree zero agree in every degree, by effaceability of the source.

structure CohomologyConnection.CechDerivedComparison {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] extends CohomologyConnection.CechToDerivedData : Type (max (max (max u_1 u_2) u₁) v₁)

Extension of CechToDerivedData packaging a chosen comparison morphism from the Čech δ-functor to the derived δ-functor.

• cech : DerivedFunctorsDefs.CohomDeltaFunctor C D
• derived : DerivedFunctorsDefs.CohomDeltaFunctor C D
• cech_effaceable : self.cech.IsEffaceable
• comparison : self.cech.Morphism self.derived

theorem CohomologyConnection.CechDerivedComparison.comparison_unique {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (comp : CechDerivedComparison) (m : comp.cech.Morphism comp.derived) (h₀ : m.η 0 = comp.comparison.η 0) (n : ℕ) : m.η n = comp.comparison.η n

The comparison morphism in a CechDerivedComparison is uniquely determined by its degree zero component.

structure CohomologyConnection.CechDerivedIsomorphism {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] extends CohomologyConnection.CechToDerivedData : Type (max (max (max u_1 u_2) u₁) v₁)

Extension of CechToDerivedData packaging both directions of an isomorphism between the Čech and derived δ-functors, plus effaceability of the derived side.

• cech : DerivedFunctorsDefs.CohomDeltaFunctor C D
• derived : DerivedFunctorsDefs.CohomDeltaFunctor C D
• cech_effaceable : self.cech.IsEffaceable
• forward : self.cech.Morphism self.derived
• backward : self.derived.Morphism self.cech
• derived_effaceable : self.derived.IsEffaceable

theorem CohomologyConnection.CechDerivedIsomorphism.forward_unique {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (iso : CechDerivedIsomorphism) (m : iso.cech.Morphism iso.derived) (h₀ : m.η 0 = iso.forward.η 0) (n : ℕ) : m.η n = iso.forward.η n

The forward isomorphism is uniquely determined by its degree zero component.

theorem CohomologyConnection.CechDerivedIsomorphism.backward_unique {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (iso : CechDerivedIsomorphism) (m : iso.derived.Morphism iso.cech) (h₀ : m.η 0 = iso.backward.η 0) (n : ℕ) : m.η n = iso.backward.η n

The backward isomorphism is uniquely determined by its degree zero component.