isHomLift — Mathlib

English

Given α: F ⇒ G between based functors and a, if 𝒳.p.obj a = S, then α.app a is a lift of id on S.

Русский

Пусть α: F ⇒ G между основанными функторaми и a, если 𝒳.p.obj a = S, тогда α.app a — подъем тождественного отображения на S.

LaTeX

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

Lean4

theorem isHomLift {a : 𝒳.obj} {S : 𝒮} (ha : 𝒳.p.obj a = S) : IsHomLift 𝒴.p (𝟙 S) (α.toNatTrans.app a) := by subst ha;
  infer_instance

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