Transporting categorical morphisms along object equalities

This file provides general lemmas for removing and rearranging the conjugations by eqToHom that arise when categorical objects are identified propositionally. They apply in an arbitrary category and avoid exposing the definitional equality of the objects being transported.

Main results

• TauCeti.eqToHom_conjugate_cancel: transporting a morphism and then transporting it back leaves it unchanged.
• TauCeti.eqToHom_conjugate_square: conjugating every edge preserves and reflects commutativity of a square.
• TauCeti.eq_of_eqToHom_conjugate: two morphisms with equal conjugates are equal.
• TauCeti.eqToHom_conjugate_vertical_square_of_horizontal_square: commutativity with conjugated horizontal edges gives commutativity after moving the conjugations to the vertical edges.

theorem TauCeti.eqToHom_conjugate_cancel {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X X' Y Y' : C} (hX : X = X') (hY : Y = Y') (f : X' ⟶ Y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hX) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))) (CategoryTheory.eqToHom hY)) = f

Transporting a morphism along object equalities and then back leaves it unchanged.

theorem TauCeti.eqToHom_conjugate_square {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X X' Y Y' Z Z' W W' : C} (hX : X = X') (hY : Y = Y') (hZ : Z = Z') (hW : W = W') (f : X' ⟶ Y') (g : Y' ⟶ Z') (f' : X' ⟶ W') (g' : W' ⟶ Z') : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hX) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hY) (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom ⋯))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hX) (CategoryTheory.CategoryStruct.comp f' (CategoryTheory.eqToHom ⋯))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hW) (CategoryTheory.CategoryStruct.comp g' (CategoryTheory.eqToHom ⋯))) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'

Conjugating a commuting square by object equalities leaves it commuting, and nothing else becomes commuting that way: the square of transported edges commutes exactly when the original one does.

theorem TauCeti.eq_of_eqToHom_conjugate {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {X X' Y Y' : C} (hX : X' = X) (hY : Y = Y') {f g : X ⟶ Y} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hX) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom hY)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hX) (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom hY))) : f = g

Two morphisms conjugated to the same morphism are equal: conjugating back cancels, by TauCeti.eqToHom_conjugate_cancel, on both sides at once.

theorem TauCeti.eqToHom_conjugate_vertical_square_of_horizontal_square {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A A' B B' D D' E E' : C} (hA : A = A') (hB : B = B') (hD : D = D') (hE : E = E') (p : A' ⟶ B') (q : E' ⟶ D') (f : B ⟶ D) (g : A ⟶ E) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hA) (CategoryTheory.CategoryStruct.comp p (CategoryTheory.eqToHom ⋯))) f = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hE) (CategoryTheory.CategoryStruct.comp q (CategoryTheory.eqToHom ⋯)))) : CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom hD))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom hE))) q

A square with conjugated horizontal edges yields a square with conjugated vertical edges. The horizontal conjugations cancel from the conclusion, while the vertical edges acquire the corresponding conjugations.