ofArrows_eq_pullback_of_isPullback

English

Equivalence between ofArrows and pullback along objects and arrows ensures the equalities of generated sieves under pullback.

Русский

Эквивалентность между ofArrows и пуллбэком обеспечивает равенство порожденных сито после тяготения.

LaTeX

$$(ofArrows Y f).arrows g ↔ ∃ i, ∃ a, g = a ≫ f_i$$

Lean4

theorem ofArrows_eq_pullback_of_isPullback {ι : Type*} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {Y : C} {g : Y ⟶ S}
    {P : ι → C} {p₁ : (i : ι) → P i ⟶ Y} {p₂ : (i : ι) → P i ⟶ X i} (h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)) :
    Sieve.ofArrows P p₁ = Sieve.pullback g (Sieve.ofArrows X f) :=
  by
  refine le_antisymm ?_ ?_
  · rw [Sieve.ofArrows, Sieve.generate_le_iff]
    rintro - - ⟨i⟩
    use X i, p₂ i, f i, ⟨i⟩
    exact (h i).w.symm
  · rintro W u ⟨Z, v, s, ⟨i⟩, heq⟩
    use P i, (h i).lift u v heq.symm, p₁ i, ⟨i⟩
    simp

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