compatiblePreserving — Mathlib

English

As a consequence of the open-embedding property, the functor induced on opens preserves the Grothendieck topology's compatibility constraints.

Русский

Как следствие свойства открытого вложения, индуцованный функтор на открытые множества сохраняет ограничения совместимости для GrothendieckTopology.

LaTeX

$$$CompatiblePreserving\\,(Opens.grothendieckTopology Y) \\, hf.isOpenMap.functor$$$

Lean4

theorem compatiblePreserving (hf : IsOpenEmbedding f) :
    CompatiblePreserving (Opens.grothendieckTopology Y) hf.isOpenMap.functor :=
  by
  haveI : Mono f := (TopCat.mono_iff_injective f).mpr hf.injective
  apply compatiblePreservingOfDownwardsClosed
  intro U V i
  refine ⟨(Opens.map f).obj V, eqToIso <| Opens.ext <| Set.image_preimage_eq_of_subset fun x h ↦ ?_⟩
  obtain ⟨_, _, rfl⟩ := i.le h
  exact ⟨_, rfl⟩

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