English
Given maps p, q, r with q ∘ p = r, one can assemble cofans X.CofanMapObjFun p j into a cofan X.CofanMapObjFun r k with a compatible vertex k, forming a cocone that coherently combines the p- and q-structures.
Русский
При задании отображений p, q, r с условием согласованности q∘p=r можно собрать конус X.CofanMapObjFun p j в конус X.CofanMapObjFun r k, чтобы получить когонус, согласующий p- и q-структуры.
LaTeX
$$$X.CofanMapObjFun r k = CofanMapObjFun.mk \_ \_ _ c'.pt (fun i hi => (c (p i) (by rw [hpqr, hi])).inj ⟨i, rfl⟩ \gg c'.inj (⟨p i, by rw [Set.mem_preimage, Set.mem_singleton_iff, hpqr, hi]⟩))$$$
Lean4
/-- Given a map `p : I → J`, this is the functor `GradedObject I C ⥤ GradedObject J C` which
sends an `I`-object `X` to the graded object `X.mapObj p` which in degree `j : J` is given
by the coproduct of those `X i` such that `p i = j`. -/
@[simps]
noncomputable def map [∀ (j : J), HasColimitsOfShape (Discrete (p ⁻¹' { j })) C] : GradedObject I C ⥤ GradedObject J C
where
obj X := X.mapObj p
map φ := mapMap φ p
