conj_eqToHom_iff_heq — Mathlib

English

Two morphisms are conjugate via eqToHom iff they are heterogeneously equal.

Русский

Два морфизма сопряжены через eqToHom тогда и только тогда, когда они гетероэквивалентны.

LaTeX

$$$ \forall W X Y Z\, (f: W\to X) (g: Y\to Z) (h: W=Y) (h': X=Z),\; f = eqToHom(h)\, g \, eqToHom(h').symm \\Leftrightarrow\; f \≈ g.$$$

Lean4

/-- Two morphisms are conjugate via eqToHom if and only if they are heterogeneously equal.
Note this used to be in the Functor namespace, where it doesn't belong. -/
theorem conj_eqToHom_iff_heq {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) :
    f = eqToHom h ≫ g ≫ eqToHom h'.symm ↔ f ≍ g := by
  cases h
  cases h'
  simp

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