map_lift_piComparison — Mathlib

English

Let HasProduct f and HasProduct (G.obj (f b)) hold. Then for any P and g: ∀ j, P ⟶ f j, the equation G.map (Pi.lift g) ≫ piComparison G f = Pi.lift (j ↦ G.map (g j)) holds.

Русский

Пусть выполнено условие существования произведения для f и для каждого j — отображение g j: P ⟶ f j. Тогда выполняется тождество: G.map (Pi.lift g) ≫ piComparison G f = Pi.lift (j ↦ G.map (g j)).

LaTeX

$$$G\\,\\big(\\Pi\\_f g\\big) = \\Pi\\_f (G\\circ g).$$$

Lean4

@[reassoc (attr := simp)]
theorem map_lift_piComparison [HasProduct f] [HasProduct fun b => G.obj (f b)] (P : C) (g : ∀ j, P ⟶ f j) :
    G.map (Pi.lift g) ≫ piComparison G f = Pi.lift fun j => G.map (g j) :=
  by
  ext j
  simp only [Category.assoc, piComparison_comp_π, ← G.map_comp, limit.lift_π, Fan.mk_pt, Fan.mk_π_app]

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