def DerivedFunctorsDefs.CohomDeltaFunctor.IsEffaceable {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 : CohomDeltaFunctor C D) : Prop

A cohomological δ-functor F is effaceable when every object X admits a mono into an I killed by F^{n+1} for every n.

def DerivedFunctorsDefs.CohomDeltaFunctor.IsEffaceableMorphism {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 : CohomDeltaFunctor C D) : Prop

A weaker form of effaceability: every X admits a mono into some I such that F^{n+1} sends i to zero, without requiring F^{n+1}(I) itself to vanish.

def DerivedFunctorsDefs.CohomDeltaFunctor.IsEffaceablePointwise {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 : CohomDeltaFunctor C D) : Prop

Pointwise effaceability: for any test morphism into F^{n+1}(X), we can find a mono φ : X ⟶ N after composition with which the morphism becomes zero.

theorem DerivedFunctorsDefs.CohomDeltaFunctor.IsEffaceable.toIsEffaceableMorphism {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 : CohomDeltaFunctor C D} (hF : F.IsEffaceable) : F.IsEffaceableMorphism

Effaceable implies effaceable-morphism: if F^{n+1}(I) is zero then so is any map into it.

theorem DerivedFunctorsDefs.CohomDeltaFunctor.IsEffaceableMorphism.toPointwise {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 : CohomDeltaFunctor C D} (hF : F.IsEffaceableMorphism) : F.IsEffaceablePointwise

Effaceable-morphism implies pointwise effaceable: precompose by the test morphism.

theorem DerivedFunctorsDefs.CohomDeltaFunctor.IsEffaceablePointwise.toMorphism {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 : CohomDeltaFunctor C D} (hF : F.IsEffaceablePointwise) : F.IsEffaceableMorphism

Converse: pointwise effaceability specialized to the identity recovers effaceable-morphism.

theorem DerivedFunctorsDefs.CohomDeltaFunctor.IsEffaceable.toPointwise {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 : CohomDeltaFunctor C D} (hF : F.IsEffaceable) : F.IsEffaceablePointwise

Effaceable implies pointwise effaceable via the morphism formulation.

theorem DerivedFunctorsDefs.CohomDeltaFunctor.isEffaceableMorphism_iff_pointwise {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 : CohomDeltaFunctor C D) : F.IsEffaceableMorphism ↔ F.IsEffaceablePointwise

The two intermediate effaceability notions are equivalent.

theorem DerivedFunctorsDefs.delta_epi_of_map_zero {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 : CohomDeltaFunctor C D} (n : ℕ) (S : CategoryTheory.ShortComplex C) (hS : S.ShortExact) (hf : (F.T (n + 1)).map S.f = 0) : CategoryTheory.Epi (F.δ n S hS)

If F^{n+1} kills the monomorphism S.f, then the connecting morphism δ_n is an epimorphism, by exactness of the long exact sequence.

theorem DerivedFunctorsDefs.delta_epi_of_vanishing {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 : CohomDeltaFunctor C D} (n : ℕ) (S : CategoryTheory.ShortComplex C) (hS : S.ShortExact) (hI : CategoryTheory.Limits.IsZero ((F.T (n + 1)).obj S.X₂)) : CategoryTheory.Epi (F.δ n S hS)

If F^{n+1} vanishes on the middle term S.X₂, the connecting morphism δ_n is an epimorphism.

theorem DerivedFunctorsDefs.effaceable_morphism_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] (F G : CohomDeltaFunctor C D) (hF : F.IsEffaceable) (m₁ m₂ : F.Morphism G) (h₀ : m₁.η 0 = m₂.η 0) (n : ℕ) : m₁.η n = m₂.η n

Uniqueness for effaceable δ-functors: a morphism F → G of δ-functors out of an effaceable F is determined by its degree-zero component.

theorem DerivedFunctorsDefs.effaceable_morphism_unique_of_effaceableMorphism {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 : CohomDeltaFunctor C D) (hF : F.IsEffaceableMorphism) (m₁ m₂ : F.Morphism G) (h₀ : m₁.η 0 = m₂.η 0) (n : ℕ) : m₁.η n = m₂.η n

Uniqueness under the weaker effaceable-morphism hypothesis: the degree-zero component still pins down the entire morphism of δ-functors.

theorem DerivedFunctorsDefs.effaceable_morphism_unique_of_pointwise {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 : CohomDeltaFunctor C D) (hF : F.IsEffaceablePointwise) (m₁ m₂ : F.Morphism G) (h₀ : m₁.η 0 = m₂.η 0) (n : ℕ) : m₁.η n = m₂.η n

Uniqueness in the pointwise formulation, deduced from the morphism version.

theorem DerivedFunctorsDefs.effaceable_step_zero_condition {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 : CohomDeltaFunctor C D} (n : ℕ) (X : C) {I : C} (i : X ⟶ I) [CategoryTheory.Mono i] (_hI_map : (F.T (n + 1)).map i = 0) (η_n : F.T n ⟶ G.T n) : let S := CategoryTheory.ShortComplex.cokernelSequence i; have hSE := ⋯; CategoryTheory.CategoryStruct.comp ((F.T n).map S.g) (CategoryTheory.CategoryStruct.comp (η_n.app S.X₃) (G.δ n S hSE)) = 0

Compatibility condition needed to inductively define the next component of a morphism of δ-functors: the composite (F^n)(g) ; η_n ; δ_n^G vanishes.

theorem DerivedFunctorsDefs.effaceable_morphism_exists_family {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 : CohomDeltaFunctor C D) (hF : F.IsEffaceableMorphism) (η₀ : F.T 0 ⟶ G.T 0) : ∃ (η : (n : ℕ) → F.T n ⟶ G.T n), η 0 = η₀ ∧ ∀ (n : ℕ) (S : CategoryTheory.ShortComplex C) (hS : S.ShortExact), CategoryTheory.CategoryStruct.comp ((η n).app S.X₃) (G.δ n S hS) = CategoryTheory.CategoryStruct.comp (F.δ n S hS) ((η (n + 1)).app S.X₁)

Inductive construction (as a raw family of natural transformations) of a morphism of δ-functors extending a given degree-zero component.

theorem DerivedFunctorsDefs.effaceable_morphism_exists {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 : CohomDeltaFunctor C D) (hF : F.IsEffaceableMorphism) (η₀ : F.T 0 ⟶ G.T 0) : ∃ (m : F.Morphism G), m.η 0 = η₀

Existence: any degree-zero natural transformation η₀ : F^0 → G^0 extends to a morphism of δ-functors.

theorem DerivedFunctorsDefs.effaceable_morphism_exists_of_pointwise {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 : CohomDeltaFunctor C D) (hF : F.IsEffaceablePointwise) (η₀ : F.T 0 ⟶ G.T 0) : ∃ (m : F.Morphism G), m.η 0 = η₀

Existence in the pointwise effaceability formulation.

theorem DerivedFunctorsDefs.effaceable_is_universal {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 : CohomDeltaFunctor C D) (hF : F.IsEffaceableMorphism) : F.IsUniversal

An effaceable-morphism δ-functor is universal: this is the existence-plus- uniqueness statement underlying Prop 41 of Lec 23 (F^i universal ⟺ effaceable).

theorem DerivedFunctorsDefs.effaceable_is_universal_of_pointwise {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 : CohomDeltaFunctor C D) (hF : F.IsEffaceablePointwise) : F.IsUniversal

Universality under the pointwise effaceability hypothesis.

theorem DerivedFunctorsDefs.effaceable_is_universal_of_isEffaceable {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 : CohomDeltaFunctor C D) (hF : F.IsEffaceable) : F.IsUniversal

Universality under the strongest effaceability hypothesis (objects, not just morphisms).