lift_π — Mathlib

English

There exists a unique map from X to the wide pullback whose compositions with each projection π arrows j equal the prescribed maps fs j, and whose composition with the base equals f.

Русский

Существует единственный морфизм из X в широкий вытягивающий предел, чьи композитиции с проекциями π arrows j равны заданным fs j, и чья композиция с базой равна f.

LaTeX

$$$\\mathrm{lift}(f,fs,w) \\;:\\; X \\to \\mathrm{widePullback}\\;B\,objs\,arrows$ satisfies $\\mathrm{lift}(f,fs,w) \\;\\circ\\; \\pi arrows j = fs j$ for all j, and $\\mathrm{lift}(f,fs,w) \\;\\circ\\; \\text{base arrows} = f$.$$

Lean4

@[reassoc]
theorem lift_π (j : J) : lift f fs w ≫ π arrows j = fs _ := by
  simp only [limit.lift_π, WidePullbackShape.mkCone_pt, WidePullbackShape.mkCone_π_app]

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