Theorems · Theorem · category theory

CategoryTheory.Quiv.homOfEq_map_homOfEq

∀ {V W : Type u} [inst : Quiver V] [inst_1 : Quiver W] (e : V ≃ W) (he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)) {X Y : V}
  (f : X ⟶ Y) {X' Y' : V} (hX : X = X') (hY : Y = Y') {X'' Y'' : W} (hX' : e X' = X'') (hY' : e Y' = Y''),
  Quiver.homOfEq ((he X' Y') (Quiver.homOfEq f hX hY)) hX' hY' = Quiver.homOfEq ((he X Y) f) ⋯ ⋯

Defined in

Mathlib.CategoryTheory.Category.Quiv

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound

Assumes

QuiverQuiver