imageSubobject_comp_le — Mathlib

English

Postcomposing by a morphism h: X' → X yields imageSubobject (h ≫ f) ≤ imageSubobject f.

Русский

После композиции через гомоморфизм h: X' → X получаем imageSubobject (h ≫ f) ≤ imageSubobject f.

LaTeX

$$$\operatorname{imageSubobject}(h \gg f) \leq \operatorname{imageSubobject}(f)$$$

Lean4

/-- The image of `h ≫ f` is always a smaller subobject than the image of `f`. -/
theorem imageSubobject_comp_le {X' : C} (h : X' ⟶ X) (f : X ⟶ Y) [HasImage f] [HasImage (h ≫ f)] :
    imageSubobject (h ≫ f) ≤ imageSubobject f :=
  Subobject.mk_le_mk_of_comm (image.preComp h f) (by simp)

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