sheafAdjunctionCocontinuous_counit_app_val

English

Explicit compatibility of toSheafify with pullback and sheafification under G.op.

Русский

Явная совместимость toSheafify с вытягиванием и подшивкой под G.op.

LaTeX

$$$toSheafify J (G.op \\cdot F) \\Rightarrow \\text{compatibility with pullback}$$$

Lean4

theorem sheafAdjunctionCocontinuous_counit_app_val (F : Sheaf J A) :
    ((G.sheafAdjunctionCocontinuous A J K).counit.app F).val = (G.op.ranAdjunction A).counit.app F.val :=
  ((G.op.ranAdjunction A).map_restrictFullyFaithful_counit_app (fullyFaithfulSheafToPresheaf K A)
        (fullyFaithfulSheafToPresheaf J A) (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm
        (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm F).trans
    (by cat_disch)

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