bindOfArrows — Mathlib

English

If S = Sieve.ofArrows Z f is in J X and each generated sieve from R_i on Z_i lies in J(Z_i), then the generated sieve from Presieve.bindOfArrows Z f R lies in J X.

Русский

Если S = Sieve.ofArrows Z f и каждое порождающее решётку R_i на Z_i лежит в J(Z_i), то Sieve.generate(Presieve.bindOfArrows Z f R) лежит в J X.

LaTeX

$$Sieve.ofArrows Z f ∈ J X ∧ (∀ i, Sieve.generate (R i) ∈ J (Z i)) ⇒ Sieve.generate (Presieve.bindOfArrows Z f R) ∈ J X$$

Lean4

theorem bindOfArrows {ι : Type*} {X : C} {Z : ι → C} {f : ∀ i, Z i ⟶ X} {R : ∀ i, Presieve (Z i)}
    (h : Sieve.ofArrows Z f ∈ J X) (hR : ∀ i, Sieve.generate (R i) ∈ J _) :
    Sieve.generate (Presieve.bindOfArrows Z f R) ∈ J X :=
  by
  refine J.superset_covering (Presieve.bind_ofArrows_le_bindOfArrows _ _ _) ?_
  exact J.bind_covering h fun _ _ _ ↦ J.pullback_stable _ (hR _)

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