piComparison_comp_π — Mathlib

English

Let f: I → C be a family with has-products and G: C ⥤ D a functor. Then for each b, the map piComparison G f composed with the b-th projection equals the image under G of the b-th projection: piComparison G f ∘ π_b^f = G(π_f(b)).

Русский

Пусть f: I → C задаёт семейство объектов и G: C ⥤ D — Функтор. Тогда для каждого b верно, что композиция piComparison G f с b-й проекцией равна отображению по G б-й проекции: piComparison G f ∘ π_b^f = G(π_f(b)).

LaTeX

$$$\\pi\\text{-Comparison } G f \\;\\circ\\; \\pi_b = G\\big(\\pi_f b\\big).$$$

Lean4

@[reassoc (attr := simp)]
theorem piComparison_comp_π [HasProduct f] [HasProduct fun b => G.obj (f b)] (b : β) :
    piComparison G f ≫ Pi.π _ b = G.map (Pi.π f b) :=
  limit.lift_π _ (Discrete.mk b)

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