widePullbackι_mono — Mathlib

English

The inclusion widePullbackι(s) is a monomorphism.

Русский

Включение widePullbackι(s) моно.

LaTeX

$$Mono (widePullbackι s)$$

Lean4

instance widePullbackι_mono {A : C} (s : Set (Subobject A)) : Mono (widePullbackι s) :=
  ⟨fun u v h =>
    limit.hom_ext fun j => by
      cases j
      · exact h
      · apply (cancel_mono ((equivShrink (Subobject A)).symm _).arrow).1
        rw [assoc, assoc]
        erw [limit.w (wideCospan s) (WidePullbackShape.Hom.term _)]
        exact h⟩

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