homOfEq_map_homOfEq — Mathlib

English

A compatibility lemma stating that applying a map-compatibility function to a homomorphism preserves the expected equality under related equalities.

Русский

Лемма совместимости: отображение через гомоморфизм сохраняет равенство под соответствующими парами равенств.

LaTeX

$$$\text{homOfEq}(f, hX, hY)$ respects equalities after transporting along equivalences: $$$$

Lean4

@[simp]
theorem homOfEq_map_homOfEq {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 _ _ (Quiver.homOfEq f hX hY)) hX' hY' =
      Quiver.homOfEq (he _ _ f) (by rw [hX, hX']) (by rw [hY, hY']) :=
  by
  subst hX hY hX' hY'
  rfl

Похожие утверждения