English
Let f and g be homotopic morphisms between pre-one-hypercovers E and F over S. For any diagram P into a category A, the induced maps on the multiforks are equal; i.e., the refinements along any limit cone agree.
Русский
Пусть f и g — гомотопные морфизмы между пред-одиночными гиперковер-объектами E и F над S. Для любой диаграммы P в категорию A индуцируемые отображения на multifork совпадают; то есть refinements по конусу предельной системы совпадают.
LaTeX
$$$f.mapMultiforkOfIsLimit P\\;hc\\;d = g.mapMultiforkOfIsLimit P\\;hc\\;d$$$
Lean4
/-- Homotopic refinements induce the same map on multiequalizers. -/
theorem mapMultiforkOfIsLimit_eq {A : Type*} [Category A] {E F : PreOneHypercover.{w} S} {f g : E.Hom F}
(H : Homotopy f g) (P : Cᵒᵖ ⥤ A) {c : Multifork (E.multicospanIndex P)} (hc : IsLimit c)
(d : Multifork (F.multicospanIndex P)) : f.mapMultiforkOfIsLimit P hc d = g.mapMultiforkOfIsLimit P hc d :=
by
refine Multifork.IsLimit.hom_ext hc fun a ↦ ?_
have heq := d.condition ⟨⟨(f.s₀ a), (g.s₀ a)⟩, H.H a⟩
simp only [multicospanIndex_right, multicospanShape_fst, multicospanIndex_left, multicospanIndex_fst,
multicospanShape_snd, multicospanIndex_snd] at heq
simp [-Homotopy.wl, -Homotopy.wr, ← H.wl, ← H.wr, reassoc_of% heq]
