adjunction_counit_map_functor — Mathlib

English

Let i: U ↪ X be an open embedding. The counit of the adjunction between the Open-map functor and restriction to U evaluated at V is equal to the canonical equality coming from map_functor_eq V.

Русский

Пусть i: U ↪ X — открытое вложение. Сопровождающее преобразование adjunction между отображением открытых множеств и ограничением к U, применённое к V, равно канонической равенству, получаемой из map_functor_eq V.

LaTeX

$$$ \\varepsilon_V = \\operatorname{eqToHom}(\\text{map\\_functor\\_eq}(V)). $$$

Lean4

@[simp]
theorem adjunction_counit_map_functor {X : TopCat} {U : Opens X} (V : Opens U) :
    U.isOpenEmbedding.isOpenMap.adjunction.counit.app (U.isOpenEmbedding.isOpenMap.functor.obj V) =
      eqToHom (by dsimp; rw [map_functor_eq V]) :=
  by subsingleton

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