snd_of_mono — Mathlib

English

Let HasPullback f g and Mono f. Then pullback.snd f g is mono.

Русский

Пусть существует pullback f g и моно-морфизм f. Тогда pullback.snd f g моно.

LaTeX

$$$Mono\; (pullback.snd\, f\, g).$$$

Lean4

/-- The pullback of a monomorphism is a monomorphism -/
instance snd_of_mono {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] [Mono f] : Mono (pullback.snd f g) :=
  PullbackCone.mono_snd_of_is_pullback_of_mono (limit.isLimit _)

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