arrow_stable — Mathlib

English

If f: Y → X and S covers f, then for any g: Z → Y, S covers g; composed arrows also preserved.

Русский

Если f: Y → X и S покрывает f, то для любого g: Z → Y покрытие сохраняется для g; композиция сохраняет покрытие.

LaTeX

$$J.Covers S f → ∀ g, J.Covers S (g ≫ f)$$

Lean4

/-- The stability axiom in 'arrow' form: If `S` covers `f` then `S` covers `g ≫ f` for any `g`. -/
theorem arrow_stable (f : Y ⟶ X) (S : Sieve X) (h : J.Covers S f) {Z : C} (g : Z ⟶ Y) : J.Covers S (g ≫ f) :=
  by
  rw [covers_iff] at h ⊢
  simp [h, Sieve.pullback_comp]

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