proj_eq — Mathlib

English

For any φ in fibre S, its image under ι S is a lift of the base map id_S.

Русский

Для любого φ в волокне S образ под ι_S является подъемом по базовому отображению id_S.

LaTeX

$$$\\text{homLift }{S}:{a,b\\in Fib p S} \\big(\\varphi\\big) : IsHomLift p (𝟙 S) ((\\iota S).map \\varphi)$$$

Lean4

@[simp]
theorem proj_eq {S : 𝒮} (a : Fib p S) : p.obj ((ι S).obj a) = S := by simp only [← comp_obj, comp_const, const_obj_obj]

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