closedUnderLimitsOfShape_isMono — Mathlib

English

For X in C, the property Over X isMono is closed under limits of shape J.

Русский

Для $X$ в $C$ свойство Over X being mono замкнуто относительно пределов формы $J$.

LaTeX

$$ClosedUnderLimitsOfShape J (Over.isMono X)$$

Lean4

theorem closedUnderLimitsOfShape_isMono : ClosedUnderLimitsOfShape J (Over.isMono X) :=
  by
  refine fun F _ hc p ↦ ⟨fun g h e ↦ ?_⟩
  apply IsLimit.hom_ext <| WithTerminal.isLimitEquiv.invFun hc
  intro j;
  cases j with
  | of j => have := p j; rw [← cancel_mono ((F.obj j).hom)]; simpa
  | star => exact e

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