instIsStableUnderCompositionToPrecoverage

English

The pre-coverage associated to a Grothendieck topology is stable under composition of coverings.

Русский

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

LaTeX

$$$$ J.toPrecoverage.IsStableUnderComposition $$$$

Lean4

instance (J : GrothendieckTopology C) : (toPrecoverage J).IsStableUnderComposition where
  comp_mem_coverings {ι} S X f hf σ Y g
    hg := by
    rw [mem_toPrecoverage_iff, ← Presieve.bindOfArrows_ofArrows]
    exact J.bindOfArrows hf hg

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