Theorems · Theorem · category theory

CategoryTheory.Arrow.square_from_iso_invert

∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : T} (i : X ≅ Y) (p : CategoryTheory.Arrow T)
  (sq : CategoryTheory.Arrow.mk i.hom ⟶ p),
  CategoryTheory.CategoryStruct.comp i.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) p.hom) =
    CategoryTheory.Arrow.Hom.right sq

Given a square from an isomorphism i to an arrow p, express the target part of sq in terms of the inverse of i.

Defined in

Mathlib.CategoryTheory.Comma.Arrow

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.Category