English
Under assumptions, homologyMap φ.τ₃ i is epi.
Русский
При предположениях отображение гомологии φ.τ₃ i эпиморфизм
LaTeX
$$homologyMap φ.τ₃ i is epi$$
Lean4
theorem epi_homologyMap_τ₃ (i : ι) (h₁ : Epi (homologyMap φ.τ₂ i)) (h₂ : ∀ j, c.Rel i j → Epi (homologyMap φ.τ₁ j))
(h₃ : ∀ j, c.Rel i j → Mono (homologyMap φ.τ₂ j)) : Epi (homologyMap φ.τ₃ i) :=
by
by_cases hi : ∃ j, c.Rel i j
· obtain ⟨j, hij⟩ := hi
apply epi_of_epi_of_epi_of_mono ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij))
· exact (composableArrows₅_exact hS₁ i j hij).δ₀.δlast
· exact (composableArrows₅_exact hS₂ i j hij).δ₀.δlast
· exact h₁
· exact h₂ j hij
· exact h₃ j hij
· have := hS₂.epi_g
have eq := (homologyFunctor C _ i).congr_map φ.comm₂₃
dsimp at eq
simp only [homologyMap_comp] at eq
have := epi_homologyMap_of_epi_of_not_rel S₂.g i (by simpa using hi)
exact epi_of_epi_fac eq.symm
