English
Equality of two cofan constructions is established by pointwise comparison with the proof carried through the universal property of the colimit.
Русский
Равенство двух конусов достигается покомпонентно через единство и универсуальность колимита.
LaTeX
$$$Eq (X.cofanMapObjComp p q r hpqr k c c') (CategoryTheory.GradedObject.CofanMapObjFun.mk X r k c'.pt (fun i hi => ...))$$$
Lean4
/-- Given maps `p : I → J`, `q : J → K` and `r : I → K` such that `q.comp p = r`,
`X : GradedObject I C`, `k : K`, the datum of cofans `X.CofanMapObjFun p j` for all
`j : J` and of a cofan for all the points of these cofans, this is a cofan of
type `X.CofanMapObjFun r k`, which is a colimit (see `isColimitCofanMapObjComp`) if the
given cofans are. -/
@[simp]
def cofanMapObjComp : X.CofanMapObjFun r k :=
CofanMapObjFun.mk _ _ _ c'.pt
(fun i hi =>
(c (p i) (by rw [hpqr, hi])).inj ⟨i, rfl⟩ ≫
c'.inj (⟨p i, by rw [Set.mem_preimage, Set.mem_singleton_iff, hpqr, hi]⟩))
