Theorems · Definition · category theory

CategoryTheory.MonoOver.isoMk

{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.hom g.arrow = f.arrow) CategoryTheory.MonoOver.isoMk._auto_1 →
            (f ≅ g)

Convenience constructor for an isomorphism in monomorphisms over X.

Defined in

Mathlib.CategoryTheory.Subobject.MonoOver

Cited by

9 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category