map_functorObj — Mathlib

English

For an inducing map f, the image under Opens.map of the object hf.functorObj(U) equals U.

Русский

Для индукцирующего отображения f образ объекта hf.functorObj(U) через Opens.map равен U.

LaTeX

$$$ (Opens.map f).obj (hf.functorObj U)=U.$$$

Lean4

theorem map_functorObj {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) (U : Opens X) :
    (Opens.map f).obj (hf.functorObj U) = U := by
  apply le_antisymm
  · rintro x ⟨_, ⟨s, rfl⟩, _, ⟨rfl : _ = U, rfl⟩, hx : f x ∈ s⟩; exact hx
  · intro x hx
    obtain ⟨U, hU⟩ := U
    obtain ⟨t, ht, rfl⟩ := hf.isOpen_iff.mp hU
    exact Opens.mem_sSup.mpr ⟨⟨_, ht⟩, rfl, hx⟩

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