objEqToHom_d — Mathlib

English

For any β-indexed graded object X, the map X.objEqToHom on refl i is the identity

Русский

Для любого индексового i в градации X.objEqToHom на refl i является тождественным отображением.

LaTeX

$$$\forall i,\; X.objEqToHom (refl i) = \mathrm{Id}_{X.obj i}$$$

Lean4

@[reassoc]
theorem objEqToHom_d {x y : β} (h : x = y) : X.objEqToHom h ≫ X.d y = X.d x ≫ X.objEqToHom (by cases h; rfl) := by
  cases h; simp

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