pushforwardContinuousSheafificationCompatibility_hom_app_val

English

A variant form of the previous compatibility statement with a different F.

Русский

Вариант той же самой совместимости с иным F.

LaTeX

$$$(G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F$ ≡ \\text{something}$$$

Lean4

@[simp]
theorem pushforwardContinuousSheafificationCompatibility_hom_app_val (F : Dᵒᵖ ⥤ A) :
    ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val =
      sheafifyLift J (whiskerLeft G.op <| toSheafify K F)
        ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F).cond :=
  by
  apply sheafifyLift_unique
  apply toSheafify_pullbackSheafificationCompatibility

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