ofArrows_eq_ofObjects — Mathlib

English

If all components p1_i, p2_i form pullbacks with g and f_i, then the pullback sieve of arrows is the pullback of arrows and X's sieve generated from Y's arrows.

Русский

Если все пары p1_i, p2_i образуют пуллбэки с g и f_i, тогда пуллбэк сито стрел является пуллбэком стрел и сито X, полученное из Y-стрел.

LaTeX

$$$\forall i, IsPullback(p1_i, p2_i, g, f_i) \Rightarrow Sieve.ofArrows P p1 = Sieve.pullback g (Sieve.ofArrows X f)$$$

Lean4

theorem ofArrows_eq_ofObjects {X : C} (hX : IsTerminal X) {I : Type*} (Y : I → C) (f : ∀ i, Y i ⟶ X) :
    ofArrows Y f = ofObjects Y X :=
  by
  refine le_antisymm (ofArrows_le_ofObjects Y f) (fun W g => ?_)
  rw [mem_ofArrows_iff, mem_ofObjects_iff]
  rintro ⟨i, ⟨h⟩⟩
  exact ⟨i, h, hX.hom_ext _ _⟩

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