mono_g — Mathlib

English

Let S be a short complex in a preadditive category which is exact, and suppose the first map is zero. Then the middle map is mono.

Русский

Пусть S — краткий комплекс в прекардовой категории, он экзактен, и предположим, что первый морфизм равен нулю. Тогда средний морфизм моно.

LaTeX

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

Lean4

theorem mono_g (hS : S.Exact) (hf : S.f = 0) : Mono S.g :=
  by
  have := hS.hasHomology
  have := hS.epi_toCycles
  have : S.iCycles = 0 := by rw [← cancel_epi S.toCycles, comp_zero, toCycles_i, hf]
  apply Preadditive.mono_of_cancel_zero
  intro A x₂ hx₂
  rw [← S.liftCycles_i x₂ hx₂, this, comp_zero]

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