Theorems · Definition · category theory

CategoryTheory.Dial.isoMk

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        {X Y : CategoryTheory.Dial C} →
          (e₁ : X.src ≅ Y.src) →
            (e₂ : X.tgt ≅ Y.tgt) →
              X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel →
                (X ≅ Y)

An isomorphism in Dial C can be induced by isomorphisms on the source and target, which respect the respective relations on X and Y.

Defined in

Mathlib.CategoryTheory.Dialectica.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasFiniteProductsCategoryTheory.Limits.HasPullbacks