eqToHom_codomain_lift_id — Mathlib

English

If hab : a = b, then eqToHom hab : a ⟶ b and relation with domain/codomain hold for lifts.

Русский

Если hab : a = b, то eqToHom hab : a ⟶ b и связанные с доменом/кодоморфизмами условия выполняются.

LaTeX

$$$$ \mathrm{eqToHom}(hab) $$$$

Lean4

theorem eqToHom_codomain_lift_id {p : 𝒳 ⥤ 𝒮} {a b : 𝒳} (hab : a = b) {S : 𝒮} (hS : p.obj b = S) :
    p.IsHomLift (𝟙 S) (eqToHom hab) := by subst hS hab; simp

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