Refinements

This file contains lemmas about "refinements" that are specific to the study of the homology of HomologicalComplex. General lemmas about refinements and the case of ShortComplex appear in the file Mathlib/CategoryTheory/Abelian/Refinements.lean.

theorem HomologicalComplex.exactAt_iff_exact_up_to_refinements {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) : K.ExactAt j ↔ ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j), CategoryTheory.CategoryStruct.comp x₂ (K.d j k) = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : CategoryTheory.Epi π) (x₁ : A' ⟶ K.X i), CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ (K.d i j)

theorem HomologicalComplex.eq_liftCycles_homologyπ_up_to_refinements {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (K : HomologicalComplex C c) {A : C} {i : ι} (γ : A ⟶ K.homology i) (j : ι) (hj : c.next i = j) : ∃ (A' : C) (π : A' ⟶ A) (_ : CategoryTheory.Epi π) (z : A' ⟶ K.X i) (hz : CategoryTheory.CategoryStruct.comp z (K.d i j) = 0), CategoryTheory.CategoryStruct.comp π γ = CategoryTheory.CategoryStruct.comp (K.liftCycles z j hj hz) (K.homologyπ i)

theorem HomologicalComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) {A : C} (x₂ : A ⟶ K.X j) (hx₂ : CategoryTheory.CategoryStruct.comp x₂ (K.d j k) = 0) : CategoryTheory.CategoryStruct.comp (K.liftCycles x₂ k hk hx₂) (K.homologyπ j) = 0 ↔ ∃ (A' : C) (π : A' ⟶ A) (_ : CategoryTheory.Epi π) (x₁ : A' ⟶ K.X i), CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ (K.d i j)

theorem HomologicalComplex.liftCycles_comp_homologyπ_eq_iff_up_to_refinements {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) {A : C} (x₂ x₂' : A ⟶ K.X j) (hx₂ : CategoryTheory.CategoryStruct.comp x₂ (K.d j k) = 0) (hx₂' : CategoryTheory.CategoryStruct.comp x₂' (K.d j k) = 0) : CategoryTheory.CategoryStruct.comp (K.liftCycles x₂ k hk hx₂) (K.homologyπ j) = CategoryTheory.CategoryStruct.comp (K.liftCycles x₂' k hk hx₂') (K.homologyπ j) ↔ ∃ (A' : C) (π : A' ⟶ A) (_ : CategoryTheory.Epi π) (x₁ : A' ⟶ K.X i), CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp π x₂' + CategoryTheory.CategoryStruct.comp x₁ (K.d i j)

theorem HomologicalComplex.comp_homologyπ_eq_zero_iff_up_to_refinements {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hi : c.prev j = i) {A : C} (z₂ : A ⟶ K.cycles j) : CategoryTheory.CategoryStruct.comp z₂ (K.homologyπ j) = 0 ↔ ∃ (A' : C) (π : A' ⟶ A) (_ : CategoryTheory.Epi π) (x₁ : A' ⟶ K.X i), CategoryTheory.CategoryStruct.comp π z₂ = CategoryTheory.CategoryStruct.comp x₁ (K.toCycles i j)

theorem HomologicalComplex.comp_homologyπ_eq_iff_up_to_refinements {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) (hi : c.prev j = i) {A : C} (z₂ z₂' : A ⟶ K.cycles j) : CategoryTheory.CategoryStruct.comp z₂ (K.homologyπ j) = CategoryTheory.CategoryStruct.comp z₂' (K.homologyπ j) ↔ ∃ (A' : C) (π : A' ⟶ A) (_ : CategoryTheory.Epi π) (x₁ : A' ⟶ K.X i), CategoryTheory.CategoryStruct.comp π z₂ = CategoryTheory.CategoryStruct.comp π z₂' + CategoryTheory.CategoryStruct.comp x₁ (K.toCycles i j)

theorem HomologicalComplex.comp_pOpcycles_eq_zero_iff_up_to_refinements {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (K : HomologicalComplex C c) {A : C} {i : ι} (z : A ⟶ K.X i) (j : ι) (hj : c.prev i = j) : CategoryTheory.CategoryStruct.comp z (K.pOpcycles i) = 0 ↔ ∃ (A' : C) (π : A' ⟶ A) (_ : CategoryTheory.Epi π) (x : A' ⟶ K.X j), CategoryTheory.CategoryStruct.comp π z = CategoryTheory.CategoryStruct.comp x (K.d j i)

theorem HomologicalComplex.mono_homologyMap_iff_up_to_refinements {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) : CategoryTheory.Mono (homologyMap φ j) ↔ ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j), CategoryTheory.CategoryStruct.comp x₂ (K.d j k) = 0 → ∀ (y₁ : A ⟶ L.X i), CategoryTheory.CategoryStruct.comp x₂ (φ.f j) = CategoryTheory.CategoryStruct.comp y₁ (L.d i j) → ∃ (A' : C) (π : A' ⟶ A) (_ : CategoryTheory.Epi π) (x₁ : A' ⟶ K.X i), CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ (K.d i j)

theorem HomologicalComplex.epi_homologyMap_iff_up_to_refinements {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) : CategoryTheory.Epi (homologyMap φ j) ↔ ∀ ⦃A : C⦄ (y₂ : A ⟶ L.X j), CategoryTheory.CategoryStruct.comp y₂ (L.d j k) = 0 → ∃ (A' : C) (π : A' ⟶ A) (_ : CategoryTheory.Epi π) (x₂ : A' ⟶ K.X j) (_ : CategoryTheory.CategoryStruct.comp x₂ (K.d j k) = 0) (y₁ : A' ⟶ L.X i), CategoryTheory.CategoryStruct.comp π y₂ = CategoryTheory.CategoryStruct.comp x₂ (φ.f j) + CategoryTheory.CategoryStruct.comp y₁ (L.d i j)