Theorems · Definition · category theory

CategoryTheory.MonoOver.homMk

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {f g : CategoryTheory.MonoOver X} →
        (h : f.obj.left ⟶ g.obj.left) →
          autoParam (CategoryTheory.CategoryStruct.comp h g.arrow = f.arrow) CategoryTheory.MonoOver.homMk._auto_1 →
            (f ⟶ g)

Convenience constructor for a morphism in monomorphisms over X.

Defined in

Mathlib.CategoryTheory.Subobject.MonoOver

Cited by

18 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category