base_eqToHom — Mathlib

English

Let X and Y be objects in CatEnrichedOrdinary C, and f, g : X ⟶ Y with α : f = g. Then the base of the equality eqToHom α agrees with the equality obtained by applying the underlying functor to α, i.e. base(eqToHom α) = eqToHom(congrArg _ α).

Русский

Пусть X и Y — объекты в CatEnrichedOrdinary C, и f, g : X ⟶ Y такие, что α : f = g. Тогда основание равенства eqToHom α совпадает с равенством, полученным применением соответствующей базовой конструкции к α, то есть base(eqToHom α) = eqToHom(congrArg _ α).

LaTeX

$$$\\operatorname{base}(\\operatorname{eqToHom}(\\alpha)) = \\operatorname{eqToHom}(\\operatorname{congrArg}(\\;\\_, \\alpha))$$$

Lean4

@[simp]
theorem base_eqToHom {X Y : CatEnrichedOrdinary C} {f g : X ⟶ Y} (α : f = g) :
    Hom.base (eqToHom α) = eqToHom (congrArg _ α) := by cases α; rfl

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