Theorems · Definition · category theory

CategoryTheory.Subobject.isoOfEq

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B : C} →
      (X Y : CategoryTheory.Subobject B) →
        X = Y → (CategoryTheory.Subobject.underlying.obj X ≅ CategoryTheory.Subobject.underlying.obj Y)

An equality of subobjects gives an isomorphism of the corresponding objects. (One could use underlying.mapIso (eqToIso h)) here, but this is more readable.)

Defined in

Mathlib.CategoryTheory.Subobject.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category