isThin — Mathlib

English

The category of monomorphisms over X is thin.

Русский

Категория монообразов над $X$ тонкая (не более одно гомоморфизм между двумя объектами).

LaTeX

$$Quiver.IsThin (MonoOver X).$$

Lean4

/-- The category of monomorphisms over X is a thin category,s
which makes defining its skeleton easy. -/
instance isThin {X : C} : Quiver.IsThin (MonoOver X) := fun f g =>
  ⟨by
    intro h₁ h₂
    apply Over.OverMorphism.ext
    rw [← cancel_mono g.arrow]
    erw [Over.w h₁]
    erw [Over.w h₂]⟩

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