isCofiltered_of_hasPullbacks — Mathlib

English

Compatibility of lift with projections, ensuring the universal property of IsLimit for multiforks.

Русский

Совместимость подъема с проекцииями, обеспечивающая универcальное свойство IsLimit для multifork.

LaTeX

$$$ lift\\ hP\\ hE\\ le\\ F \\mapsto F.ι\\ ⟨_, E.f i, le _ (Sieve.ofArrows_mk _ _ _)⟩$$$

Lean4

/-- If `C` has pullbacks, the category of `1`-hypercovers up to homotopy is cofiltered. -/
instance isCofiltered_of_hasPullbacks [HasPullbacks C] : IsCofiltered (J.HOneHypercover S)
    where
  cone_objs
    {E F} := ⟨⟨E.1.inter F.1⟩, Quot.mk _ (PreOneHypercover.interFst _ _), Quot.mk _ (PreOneHypercover.interSnd _ _), ⟨⟩⟩
  cone_maps {X Y} f
    g := by
    obtain ⟨(f : X.1 ⟶ Y.1), rfl⟩ := (toHOneHypercover J S).map_surjective f
    obtain ⟨(g : X.1 ⟶ Y.1), rfl⟩ := (toHOneHypercover J S).map_surjective g
    obtain ⟨W, h, ⟨H⟩⟩ := OneHypercover.exists_nonempty_homotopy f g
    use (toHOneHypercover J S).obj W, (toHOneHypercover J S).map h
    rw [← Functor.map_comp, ← Functor.map_comp]
    exact H.map_eq_map

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