sheafAdjunctionCocontinuous_homEquiv_apply_val

English

A variant of the compatibility between toSheafify and pullback in a different setting.

Русский

Вариант совместимости toSheafify и pullback в другой конфигурации.

LaTeX

$$$toSheafify J (G.op \\cdot F) = \\dots$$$

Lean4

theorem sheafAdjunctionCocontinuous_homEquiv_apply_val {F : Sheaf K A} {H : Sheaf J A}
    (f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H) :
    ((G.sheafAdjunctionCocontinuous A J K).homEquiv F H f).val = (G.op.ranAdjunction A).homEquiv F.val H.val f.val :=
  ((sheafToPresheaf K A).congr_map
        (((G.op.ranAdjunction A).restrictFullyFaithful_homEquiv_apply (fullyFaithfulSheafToPresheaf K A)
          (fullyFaithfulSheafToPresheaf J A) (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm
          (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm f))).trans
    (by
      dsimp
      erw [Functor.map_id, Category.comp_id, Category.id_comp, Adjunction.homEquiv_unit])

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