sheafAdjunctionCocontinuous_unit_app_val

English

Compatibility statement relating to toSheafify and pullback along F and G.

Русский

Согласованность между toSheafify и обратным тягом вдоль F и G.

LaTeX

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

Lean4

theorem sheafAdjunctionCocontinuous_unit_app_val (F : Sheaf K A) :
    ((G.sheafAdjunctionCocontinuous A J K).unit.app F).val = (G.op.ranAdjunction A).unit.app F.val :=
  by
  apply
    ((G.op.ranAdjunction A).map_restrictFullyFaithful_unit_app (fullyFaithfulSheafToPresheaf K A)
        (fullyFaithfulSheafToPresheaf J A) (G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).symm
        (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).symm F).trans
  dsimp
  erw [Functor.map_id]
  change _ ≫ 𝟙 _ ≫ 𝟙 _ = _
  simp only [Category.comp_id]

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