toPushforwardOfIso_app — Mathlib

English

Given an isomorphism of topological spaces and a morphism of presheaves, the isomorphically transported pushforward acts by composing the maps as described by the isomorphism.

Русский

Приизложение изоморфизма пространств и морфизм пресшефа перемещает pushforward согласно изоморфизму.

LaTeX

$$(toPushforwardOfIso H₁ H₂).app U = F.map (eqToHom ...) ≫ H₂.app (op ((Opens.map H₁.inv).obj (unop U)))$$

Lean4

@[simp]
theorem toPushforwardOfIso_app {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : X.Presheaf C} {𝒢 : Y.Presheaf C} (H₂ : H₁.hom _* ℱ ⟶ 𝒢)
    (U : (Opens X)ᵒᵖ) :
    (toPushforwardOfIso H₁ H₂).app U =
      ℱ.map (eqToHom (by simp [Opens.map, Set.preimage_preimage])) ≫ H₂.app (op ((Opens.map H₁.inv).obj (unop U))) :=
  by simp [toPushforwardOfIso, Adjunction.homEquiv_unit]

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