pullback_mem_iff_of_isIso — Mathlib

English

If i: X → Y is an isomorphism and S is a sieve on Y, then S.pullback i ∈ J X if and only if S ∈ J Y.

Русский

Если i: X → Y — изоморфизм, и S — решёт на Y, то S.pullback i ∈ J X, если и только если S ∈ J Y.

LaTeX

$$S.pullback i ∈ J X ⇔ S ∈ J Y$$

Lean4

@[simp]
theorem pullback_mem_iff_of_isIso {i : X ⟶ Y} [IsIso i] {S : Sieve Y} : S.pullback i ∈ J _ ↔ S ∈ J _ :=
  by
  refine ⟨fun H ↦ ?_, J.pullback_stable i⟩
  convert J.pullback_stable (inv i) H
  rw [← Sieve.pullback_comp, IsIso.inv_hom_id, Sieve.pullback_id]

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