inclusion'_top_functor — Mathlib

English

The inclusion-induced functor is naturally isomorphic to a pullback via inclusionTopIso.

Русский

Функтор, порожденный включением, естественно изоморфен вытяжке через inclusionTopIso.

LaTeX

$$$ inclusion'_top\_functor(X)= map( inclusionTopIso(X) )^{-1} $$$

Lean4

theorem inclusion'_top_functor (X : TopCat) :
    (@Opens.isOpenEmbedding X ⊤).isOpenMap.functor = map (inclusionTopIso X).inv :=
  by
  refine CategoryTheory.Functor.ext ?_ ?_
  · intro U
    ext x
    exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨x, trivial⟩, h, rfl⟩⟩
  · subsingleton

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