instHasPairwisePullbacksOfExtensive

English

For any extensive presieve on X in a category C, the presieve has pairwise pullbacks.

Русский

Для любого экстенсивного пресивса над X в категории C существует параллельные пулбек-последовательности.

LaTeX

$$$\forall S : Presieve X,\; S.\mathrm{HasPairwisePullbacks}$$$

Lean4

instance {X : C} (S : Presieve X) [S.Extensive] : S.HasPairwisePullbacks where
  has_pullbacks :=
    by
    obtain ⟨_, _, _, _, rfl, ⟨hc⟩⟩ := Presieve.Extensive.arrows_nonempty_isColimit (R := S)
    intro _ _ _ _ _ hg
    cases hg
    apply FinitaryPreExtensive.hasPullbacks_of_is_coproduct hc

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