lift_map — Mathlib

English

Equivalently, for any X and f, f' : X ⟶ limit F, equality on all π_j implies equality of the arrows; i.e., the limit is a universal receiver for morphisms from X.

Русский

Эквивалентно: если у f, f' : X ⟶ limit F равны после композиции с всеми π_j, то f = f'; предел является универсальным получателем морфизмов из X.

LaTeX

$$$\\forall j, f \\circ (limit.π F j) = f' \\circ (limit.π F j) \\Rightarrow f = f'$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_map {F G : J ⥤ C} [HasLimit F] [HasLimit G] (c : Cone F) (α : F ⟶ G) :
    limit.lift F c ≫ limMap α = limit.lift G ((Cones.postcompose α).obj c) :=
  by
  ext
  rw [assoc, limMap_π, limit.lift_π_assoc, limit.lift_π]
  rfl

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