hasMap_comp — Mathlib

English

Let X be a graded object with maps p, q, r and hpqr as above. If X has a map along p and the object X.mapObj p has a map along q, with q(p(i)) = r(i) for all i, then X has a map along r.

Русский

Пусть X — градуированный объект с отображениями p, q, r и hpqr так, что q ∘ p = r. Если у X есть отображение вдоль p и у X.mapObj p есть отображение вдоль q при каждом i, удовлетворяющем q(p(i)) = r(i), тогда у X существует отображение вдоль r.

LaTeX

$$$X.HasMap\\; r$$$

Lean4

theorem hasMap_comp [(X.mapObj p).HasMap q] : X.HasMap r := fun k =>
  ⟨_,
    isColimitCofanMapObjComp X p q r hpqr k _ (fun j _ => X.isColimitCofanMapObj p j) _
      ((X.mapObj p).isColimitCofanMapObj q k)⟩

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