def DerivedFunctorsDefs.CohomDeltaFunctor.compMorphism {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] {F G H : CohomDeltaFunctor C D} (m₁ : F.Morphism G) (m₂ : G.Morphism H) : F.Morphism H

Composition of morphisms of cohomological delta functors.

@[simp]

theorem DerivedFunctorsDefs.CohomDeltaFunctor.compMorphism_η {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] {F G H : CohomDeltaFunctor C D} (m₁ : F.Morphism G) (m₂ : G.Morphism H) (n : ℕ) : (compMorphism m₁ m₂).η n = CategoryTheory.CategoryStruct.comp (m₁.η n) (m₂.η n)

The n-th component of a composition of delta-functor morphisms is the composition of the components.

theorem CechDerivedComparison.roundtrip_eq_id_of_effaceable {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] (F : DerivedFunctorsDefs.CohomDeltaFunctor C D) (hF : F.IsEffaceable) (m : F.Morphism F) (h₀ : m.η 0 = CategoryTheory.CategoryStruct.id (F.T 0)) (n : ℕ) : m.η n = CategoryTheory.CategoryStruct.id (F.T n)

An endomorphism of an effaceable delta functor that is the identity in degree zero is the identity in every degree, by the uniqueness of effaceable extensions.

structure CechDerivedIsomorphismProof.CechDerivedComparisonData {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₃)

Data witnessing a comparison between Čech and derived-functor cohomology as delta functors, with mutually inverse morphisms in degree zero and effaceability hypotheses to extend the inverse to all degrees.

• cech : DerivedFunctorsDefs.CohomDeltaFunctor C D
• derived : DerivedFunctorsDefs.CohomDeltaFunctor C D
• cech_effaceable : self.cech.IsEffaceable
• derived_effaceable : self.derived.IsEffaceable
• forward : self.cech.Morphism self.derived
• backward : self.derived.Morphism self.cech
• forward_backward_zero : CategoryTheory.CategoryStruct.comp (self.forward.η 0) (self.backward.η 0) = CategoryTheory.CategoryStruct.id (self.cech.T 0)
• backward_forward_zero : CategoryTheory.CategoryStruct.comp (self.backward.η 0) (self.forward.η 0) = CategoryTheory.CategoryStruct.id (self.derived.T 0)

theorem CechDerivedIsomorphismProof.CechDerivedComparisonData.forward_backward_eq_id {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 : CechDerivedComparisonData) (n : ℕ) : CategoryTheory.CategoryStruct.comp (data.forward.η n) (data.backward.η n) = CategoryTheory.CategoryStruct.id (data.cech.T n)

The composition forward ∘ backward is the identity in every degree.

theorem CechDerivedIsomorphismProof.CechDerivedComparisonData.backward_forward_eq_id {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 : CechDerivedComparisonData) (n : ℕ) : CategoryTheory.CategoryStruct.comp (data.backward.η n) (data.forward.η n) = CategoryTheory.CategoryStruct.id (data.derived.T n)

The composition backward ∘ forward is the identity in every degree.

theorem CechDerivedIsomorphismProof.CechDerivedComparisonData.forward_isIso {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 : CechDerivedComparisonData) (n : ℕ) : CategoryTheory.IsIso (data.forward.η n)

The forward comparison map is an isomorphism in every degree.

theorem CechDerivedIsomorphismProof.CechDerivedComparisonData.backward_isIso {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 : CechDerivedComparisonData) (n : ℕ) : CategoryTheory.IsIso (data.backward.η n)

The backward comparison map is an isomorphism in every degree.

theorem CechDerivedIsomorphismProof.CechDerivedComparisonData.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] (data : CechDerivedComparisonData) (m : data.cech.Morphism data.derived) (h₀ : m.η 0 = data.forward.η 0) (n : ℕ) : m.η n = data.forward.η n

Uniqueness: any morphism cech → derived agreeing with forward in degree zero agrees with it in every degree.

theorem CechDerivedIsomorphismProof.CechDerivedComparisonData.inverse_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 : CechDerivedComparisonData) (m : data.derived.Morphism data.cech) (h₀ : m.η 0 = data.backward.η 0) (n : ℕ) : m.η n = data.backward.η n

Uniqueness of the inverse: any morphism derived → cech agreeing with backward in degree zero agrees with it in every degree.

structure CechDerivedIsomorphismProof.CechDerivedFullComparison {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.CechDerivedIsomorphism : Type (max (max (max u_1 u_2) u₃) v₃)

A CechDerivedIsomorphism enriched with explicit degree-zero invertibility witnesses, suitable for promoting the comparison to all degrees.

• 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
• forward_backward_zero : CategoryTheory.CategoryStruct.comp (self.forward.η 0) (self.backward.η 0) = CategoryTheory.CategoryStruct.id (self.cech.T 0)
• backward_forward_zero : CategoryTheory.CategoryStruct.comp (self.backward.η 0) (self.forward.η 0) = CategoryTheory.CategoryStruct.id (self.derived.T 0)

def CechDerivedIsomorphismProof.CechDerivedFullComparison.toComparisonData {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 : CechDerivedFullComparison) : CechDerivedComparisonData

Repackage a CechDerivedFullComparison as CechDerivedComparisonData.

theorem CechDerivedIsomorphismProof.CechDerivedFullComparison.forward_isIso {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 : CechDerivedFullComparison) (n : ℕ) : CategoryTheory.IsIso (comp.forward.η n)

The forward comparison map from a CechDerivedFullComparison is an isomorphism in every degree.