English
For an isomorphism X ≅ Y and a morphism between presheaves, the pushforward along the isomorphism gives a coherent description of the app on an open.
Русский
Для изоморфизма X ≅ Y и морфизма между пресшефами pushforward по изоморфизму даёт когерентное описание применения на открытом.
LaTeX
$$toPushforwardOfIso H₁ H₂ .app U = ℱ.map (eqToHom ...) ≫ H₂.app (op ((Opens.map H₁.inv).obj (unop U)))$$
Lean4
@[simp]
theorem pushforwardToOfIso_app {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : Y.Presheaf C} {𝒢 : X.Presheaf C} (H₂ : ℱ ⟶ H₁.hom _* 𝒢)
(U : (Opens X)ᵒᵖ) :
(pushforwardToOfIso H₁ H₂).app U =
H₂.app (op ((Opens.map H₁.inv).obj (unop U))) ≫ 𝒢.map (eqToHom (by simp [Opens.map, Set.preimage_preimage])) :=
by simp [pushforwardToOfIso, Equivalence.toAdjunction, Adjunction.homEquiv_counit]
