hasPullbacks_of_inclusions — Mathlib

English

Another restatement of the initial-to-Sigma pullback property for finite index sets.

Русский

Еще одно изложение свойства пуллбека начальных к Sigma для конечного числа индексов.

LaTeX

$$$IsPullback( initial.to (X i), initial.to (X j), Sigma.ι X i, Sigma.ι X j )$$$

Lean4

instance hasPullbacks_of_inclusions [FinitaryPreExtensive C] {X Z : C} {α : Type*} (f : X ⟶ Z) {Y : (a : α) → C}
    (i : (a : α) → Y a ⟶ Z) [Finite α] [hi : IsIso (Sigma.desc i)] (a : α) : HasPullback f (i a) :=
  by
  apply FinitaryPreExtensive.hasPullbacks_of_is_coproduct (c := Cofan.mk Z i)
  exact @IsColimit.ofPointIso (t := Cofan.mk Z i) (P := _) (i := hi)

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