app_isHomLift — Mathlib

English

For a BasedNatTrans α: F ⇒ G, each component α.app a is a lift over the corresponding identity in the base category.

Русский

Для BasedNatTrans α: F ⇒ G каждый компонент α.app a является подъемом над соответствующим тождественным элементом базовой категории.

LaTeX

$$$\\forall a:\\, 𝒳.obj,\; IsHomLift 𝒴.p (𝟙 (𝒳.p.obj a)) (α.toNatTrans.app a)$$$

Lean4

instance app_isHomLift (a : 𝒳.obj) : IsHomLift 𝒴.p (𝟙 (𝒳.p.obj a)) (α.toNatTrans.app a) :=
  α.isHomLift' a

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