Theorems · Theorem · category theory

CategoryTheory.Functor.congr_inv_of_congr_hom

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F G : CategoryTheory.Functor C D) {X Y : C} (e : X ≅ Y) (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y),
  F.map e.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.CategoryStruct.comp (G.map e.hom) (CategoryTheory.eqToHom ⋯)) →
    F.map e.inv =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.CategoryStruct.comp (G.map e.inv) (CategoryTheory.eqToHom ⋯))

Defined in

Mathlib.CategoryTheory.EqToHom

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category