imageSubobject_le — Mathlib

English

If f: A → B factors through a subobject X of B via h: A → X, then the imageSubobject of f is contained in X.

Русский

Если $f: A\to B$ факторизуется через подобъект $X$ из $B$ как $f = h; X.arrow$, то образ подобъекта $f$ вложен в $X$.

LaTeX

$$$f : A \to B$, $X \subseteq B$ with arrow $X.arrow$, and $h : A \to X$ such that $h \circ X.arrow = f$ implies $\mathrm{imageSubobject}(f) \le X$.$$

Lean4

theorem imageSubobject_le {A B : C} {X : Subobject B} (f : A ⟶ B) [HasImage f] (h : A ⟶ X) (w : h ≫ X.arrow = f) :
    imageSubobject f ≤ X :=
  Subobject.le_of_comm
    ((imageSubobjectIso f).hom ≫
      image.lift
        { I := (X : C)
          e := h
          m := X.arrow })
    (by rw [assoc, image.lift_fac, imageSubobject_arrow])

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