English
Under certain hypotheses, the morphism homologyMap φ.τ₃ i is mono.
Русский
При некоторых условиях морфизм homologyMap φ.τ₃ i моно
LaTeX
$$homologyMap φ.τ₃ i is mono$$
Lean4
theorem mono_homologyMap_τ₃ (i : ι) (h₁ : Epi (homologyMap φ.τ₁ i)) (h₂ : Mono (homologyMap φ.τ₂ i))
(h₃ : ∀ j, c.Rel i j → Mono (homologyMap φ.τ₁ j)) : Mono (homologyMap φ.τ₃ i) :=
by
by_cases hi : ∃ j, c.Rel i j
· obtain ⟨j, hij⟩ := hi
apply mono_of_epi_of_mono_of_mono ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij))
· exact (composableArrows₅_exact hS₁ i j hij).δlast.δlast
· exact (composableArrows₅_exact hS₂ i j hij).δlast.δlast
· exact h₁
· exact h₂
· exact h₃ _ hij
· refine
mono_of_epi_of_epi_of_mono (mapComposableArrows₂ φ i) (composableArrows₂_exact hS₁ i)
(composableArrows₂_exact hS₂ i) ?_ h₁ h₂
have := hS₁.epi_g
apply epi_homologyMap_of_epi_of_not_rel
simpa using hi
