over_map_coverPreserving — Mathlib

English

For a morphism f, there is compatibility-preserving behavior of the diagram under Over.map f with respect to J.

Русский

При отображении Over.map f соблюдается совместимость графиков и топологии J.

LaTeX

$$$\\forall f:\\,X\\to Y\\; \\mathrm{CompatiblePreserving}\\ (J.\\mathrm{over}\\,Y)\\ (\\mathrm{Over.map}\\ f)$$$

Lean4

theorem over_map_coverPreserving {X Y : C} (f : X ⟶ Y) : CoverPreserving (J.over X) (J.over Y) (Over.map f) where
  cover_preserve {U S}
    hS := by
    obtain ⟨S, rfl⟩ := (Sieve.overEquiv U).symm.surjective S
    rw [Sieve.functorPushforward_over_map]
    apply overEquiv_symm_mem_over
    simpa [mem_over_iff] using hS

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