pullback_close — Mathlib

English

Closure under J is stable under pullback: for any f: Y → X and sieve S on X, close(S pulled back along f) equals (close S) pulled back along f.

Русский

Замыкание по J сохраняется при взятии обратного образа: для любого f: Y → X и расселения S на X, close(S pullback f) = close(S) pullback f.

LaTeX

$$$J_1.\\text{close}(S\\.\\text{pullback} f) = (J_1.\\text{close} S)\\.\\text{pullback} f$$$

Lean4

/-- Closing under `J` is stable under pullback. -/
theorem pullback_close {X Y : C} (f : Y ⟶ X) (S : Sieve X) : J₁.close (S.pullback f) = (J₁.close S).pullback f :=
  by
  apply le_antisymm
  · refine J₁.le_close_of_isClosed (Sieve.pullback_monotone _ (J₁.le_close S)) ?_
    apply J₁.isClosed_pullback _ _ (J₁.close_isClosed _)
  · intro Z g hg
    change _ ∈ J₁ _
    rw [← Sieve.pullback_comp]
    apply hg

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