English
Let J be an index category and A, B : J → C such that each f j: A j ⟶ B j has the lifting property with respect to p: X → Y. Then the induced map on the product (Limits.Pi.map f) has the lifting property with respect to p.
Русский
Пусть J — индексированное множество; A, B : J → C; для каждого j ⟂ A_j ⟶ B_j имеет свойство подъёма относительно p: X → Y. Тогда отображение Limits.Pi.map f имеет свойство подъёма относительно p.
LaTeX
$$$\\forall j, HasLiftingProperty(p, f_j) \\Rightarrow HasLiftingProperty(p, \\mathrm{Limits.Pi.map}\, f).$$$
Lean4
instance {J : Type*} {A B : J → C} [HasProduct A] [HasProduct B] (f : (j : J) → A j ⟶ B j) {X Y : C} (p : X ⟶ Y)
[∀ j, HasLiftingProperty p (f j)] : HasLiftingProperty p (Limits.Pi.map f) where
sq_hasLift {t b}
sq :=
by
have sq' (j : J) : CommSq (t ≫ Pi.π _ j) p (f j) (b ≫ Pi.π _ j) := ⟨by rw [← Category.assoc, ← sq.w]; simp⟩
exact ⟨⟨{ l := Pi.lift (fun j ↦ (sq' j).lift) }⟩⟩
