bind_ofArrows_le_bindOfArrows — Mathlib

English

The extension of a diagram along an index i yields a morphism that factors as required by the square's commutativity and intermediate arrows.

Русский

Расширение диаграммы по индексу i образует морфизм, который можно разложить согласно композиции квадрата и промежуточным стрелам.

LaTeX

$$Exists l with f_i ≫ l = t ≫ ιFunctorObj and l ≫ πFunctorObj = b$$

Lean4

theorem bind_ofArrows_le_bindOfArrows {ι : Type*} {X : C} (Z : ι → C) (f : ∀ i, Z i ⟶ X) (R : ∀ i, Presieve (Z i)) :
    Sieve.bind (Sieve.ofArrows Z f)
        (fun _ _ hg ↦ Sieve.pullback (Sieve.ofArrows.h hg) (.generate <| R (Sieve.ofArrows.i hg))) ≤
      Sieve.generate (Presieve.bindOfArrows Z f R) :=
  by
  rintro T g ⟨W, v, v', hv', ⟨S, u, u', h, hu⟩, rfl⟩
  rw [← Sieve.ofArrows.fac hv', ← reassoc_of% hu]
  exact ⟨S, u, u' ≫ f _, ⟨_, _, h⟩, rfl⟩

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