instIsStableUnderBaseChangeToPrecoverage

English

The pre-coverage associated to a Grothendieck topology is stable under base change.

Русский

Связаноe предпокрытие топологии Гротендика устойчиво к базовым изменениям.

LaTeX

$$$$ J.toPrecoverage.IsStableUnderBaseChange $$$$

Lean4

instance (J : GrothendieckTopology C) : (toPrecoverage J).IsStableUnderBaseChange where
  mem_coverings_of_isPullback {ι} S X f hf Y g P p₁ p₂
    h := by
    rw [mem_toPrecoverage_iff, ← Sieve.ofArrows, Sieve.ofArrows_eq_pullback_of_isPullback _ h]
    exact J.pullback_stable _ hf

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