mono_shortComplex'_f — Mathlib

English

If h is a pullback, the arrow f on the short pullback is mono.

Русский

Если h является пуллбеком, то отображение f в коротком пуллбек-е моно.

LaTeX

$$IsPullback(f,g,inl,inr) ⇒ Mono(h.shortComplex'.f)$$

Lean4

theorem mono_shortComplex'_f (h : IsPullback fst snd f g) : Mono h.shortComplex'.f :=
  by
  rw [Preadditive.mono_iff_cancel_zero]
  intro _ b hb
  exact Fork.IsLimit.hom_ext h.isLimitKernelFork (by simpa using hb)

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