liftHom_fac — Mathlib

English

There is a constructed object in the SqFunctor at index j, whose f' is liftHom and which satisfies the necessary compatibility conditions w₁ and w₂ with the colimit cocone.

Русский

Сконструировано соответствующее объекту в SqFunctor на индексе j, у которого первый компонент f' равен liftHom и которое удовлетворяет требуемым совместимостям w₁ и w₂ с коконом колимита.

LaTeX

$$$$ lift : (sqFunctor\ c\ p\ f\ g).obj\ (Opposite.op\ j) $$ with\ f' := liftHom\ hj\ s, w_1, w_2\text{ как в определении} $$$$

Lean4

@[reassoc]
theorem liftHom_fac (i : J) (hi : i < j) : F.map (homOfLE hi.le) ≫ liftHom hj s = (s.1 ⟨⟨i, hi⟩⟩).f' :=
  (F.isColimitOfIsWellOrderContinuous j hj).fac _ ⟨i, hi⟩

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