epi_f — Mathlib

English

If S is exact and g is zero, then f is epi.

Русский

Если S экзактна и второй морфизм g равен 0, то первый морфизм f является эпиморфизмом.

LaTeX

$$$S\text{.Exact} \land S.g = 0 \Rightarrow \mathrm{Epi}(S.f)$$$

Lean4

theorem epi_f (hS : S.Exact) (hg : S.g = 0) : Epi S.f :=
  by
  have := hS.hasHomology
  have := hS.mono_fromOpcycles
  have : S.pOpcycles = 0 := by rw [← cancel_mono S.fromOpcycles, zero_comp, p_fromOpcycles, hg]
  apply Preadditive.epi_of_cancel_zero
  intro A x₂ hx₂
  rw [← S.p_descOpcycles x₂ hx₂, this, zero_comp]

Похожие утверждения