isClosed_pullback — Mathlib

English

If S is J-closed, then its pullback along any morphism f is J-closed.

Русский

Замкнутость S сохраняется под вытягиванием по любому морфизму f.

LaTeX

$$$J_1.\\text{IsClosed } S \\Rightarrow J_1.\\text{IsClosed}(S.\\mathrm{pullback} f)$$$

Lean4

/-- Being `J`-closed is stable under pullback. -/
theorem isClosed_pullback {X Y : C} (f : Y ⟶ X) (S : Sieve X) : J₁.IsClosed S → J₁.IsClosed (S.pullback f) :=
  fun hS Z g hg => hS (g ≫ f) (by rwa [J₁.covers_iff, Sieve.pullback_comp])

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