pullbackObjObjOfImageOpen — Mathlib

English

Let f: X → Y be continuous, and let F be a presheaf on Y. If the image f''U of an open set U ⊆ X is open in Y, then the pullback presheaf along f evaluated at U is canonically isomorphic to the original presheaf evaluated on the image open; i.e., (f^*F)(U) ≅ F(f(U)).

Русский

Пусть f: X → Y — непрерывное отображение, ℱ — пресsheaf на Y. Если образ f''U открытого множества U ⊆ X является открытым в Y, то вытянутый вдоль f пресsheaf на X, взятый на U, изотропен к ℱ на образе: (f^*ℱ)(U) ≅ ℱ(f(U)).

LaTeX

$$$\\bigl(f^{*}\\mathcal F\\bigr)(U) \\cong \\mathcal F\\bigl(f(U)\\bigr)\\quad\\text{whenever } f(U)\\text{ is open in } Y.$$$

Lean4

/-- If `f '' U` is open, then `f⁻¹ℱ U ≅ ℱ (f '' U)`. -/
def pullbackObjObjOfImageOpen {X Y : TopCat.{v}} (f : X ⟶ Y) (ℱ : Y.Presheaf C) (U : Opens X)
    (H : IsOpen (f '' SetLike.coe U)) : ((pullback C f).obj ℱ).obj (op U) ≅ ℱ.obj (op ⟨_, H⟩) :=
  by
  let x : CostructuredArrow (Opens.map f).op (op U) :=
    CostructuredArrow.mk (@homOfLE _ _ _ ((Opens.map f).obj ⟨_, H⟩) (Set.image_preimage.le_u_l _)).op
  have hx : IsTerminal x :=
    {
      lift := fun s ↦ by
        fapply CostructuredArrow.homMk
        · change op (unop _) ⟶ op (⟨_, H⟩ : Opens _)
          refine (homOfLE ?_).op
          apply (Set.image_mono s.pt.hom.unop.le).trans
          exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop)
        · simp [eq_iff_true_of_subsingleton] }
  exact
    IsColimit.coconePointUniqueUpToIso ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
      (colimitOfDiagramTerminal hx _)

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