Theorems · Definition · category theory

CategoryTheory.Under.isoMk

{T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} →
      {f g : CategoryTheory.Under X} →
        (hr : f.right ≅ g.right) →
          autoParam (CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom) CategoryTheory.Under.isoMk._auto_1 →
            (f ≅ g)

Construct an isomorphism in the over category given isomorphisms of the objects whose forward direction gives a commutative triangle.

Defined in

Mathlib.CategoryTheory.Comma.Over.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category