sheafPushforwardCocontinuousCompSheafToPresheafIso

Lean4
/-- `G.sheafPushforwardCocontinuous A J K : Sheaf J A ⥤ Sheaf K A` is induced
by the right Kan extension functor `G.op.ran` on presheaves. -/
@[simps! hom inv]
def sheafPushforwardCocontinuousCompSheafToPresheafIso :
    G.sheafPushforwardCocontinuous A J K ⋙ sheafToPresheaf K A ≅ sheafToPresheaf J A ⋙ G.op.ran :=
  Iso.refl
    _
      /-

      Given a cocontinuous functor `G`, the precomposition with `G.op` induces a functor
      on presheaves with leads to a "pullback" functor `Sheaf K A ⥤ Sheaf J A` (TODO: formalize
      this as `G.sheafPullbackCocontinuous A J K`) using the associated sheaf functor.
      It is shown in SGA 4 III 2.3 that this pullback functor is
      left adjoint to `G.sheafPushforwardCocontinuous A J K`. This adjunction may replace
      `Functor.sheafAdjunctionCocontinuous` below, and then, it could be shown that if
      `G` is also continuous, then we have an isomorphism
      `G.sheafPullbackCocontinuous A J K ≅ G.sheafPushforwardContinuous A J K` (TODO).

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