pullbackIso — Mathlib

English

Equivalence between the inverse image under the isomorphism and component-wise equalities in the product diagram.

Русский

Эквивалентность между образом через обратное изображение по изоморфизму и равенствами компонентов в диаграмме произведения.

LaTeX

$$$F.1.map (homOfLE e).op ((F.objSupIsoProdEqLocus U V).inv x) = y \\Longleftrightarrow (\\ldots)$$$

Lean4

/-- The pullback of a sheaf is isomorphic (actually definitionally equal) to the sheafification
of the pullback as a presheaf.
-/
def pullbackIso (f : X ⟶ Y) : pullback A f ≅ forget A Y ⋙ Presheaf.pullback A f ⋙ presheafToSheaf _ _ :=
  Functor.sheafPullbackConstruction.sheafPullbackIso _ _ _ _

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