congrArg_cast_hom_right — Mathlib

English

If p: X ⟶ Y and q: Z = Y, then transporting along q gives a map X ⟶ Z; composing with eqToHom q.symm yields p ≫ eqToHom q.symm.

Русский

Если p: X ⟶ Y и q: Z = Y, то перенос по q даёт отображение X ⟶ Z; это равно p ≫ eqToHom q.symm.

LaTeX

$$$ (\\mathrm{congrArg}(\\lambda W: X \\to W) q).mpr p = p \\circ eqToHom(q^{\\mathrm{symm}}) $$$

Lean4

/-- Reducible form of `congrArg_mpr_hom_right` -/
@[simp]
theorem congrArg_cast_hom_right {X Y Z : C} (p : X ⟶ Y) (q : Z = Y) :
    cast (congrArg (fun W : C => X ⟶ W) q.symm) p = p ≫ eqToHom q.symm :=
  by
  cases q
  simp

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