instIsIsoSheafAppCounitSheafAdjunctionCocontinuous

English

The induced topology (G.inducedTopology K) is cocontinuous with respect to K, encoding the dual (colimit-like) behavior of coverings under G.

Русский

Вводимая топология (G.inducedTopology K) когонтинуальная по отношению к K, отражая колимитную—подобную поведение покрытий при G.

LaTeX

$$$G.\\mathrm{IsCocontinuous} (G.\\mathrm{inducedTopology } K)\\ K$$$

Lean4

instance (Y : Sheaf J A) : IsIso ((G.sheafAdjunctionCocontinuous A J K).counit.app Y) :=
  by
  apply (config := { allowSynthFailures := true }) ReflectsIsomorphisms.reflects (sheafToPresheaf J A)
  rw [NatTrans.isIso_iff_isIso_app]
  intro ⟨U⟩
  apply (config := { allowSynthFailures := true }) ReflectsIsomorphisms.reflects yoneda
  rw [NatTrans.isIso_iff_isIso_app]
  intro ⟨X⟩
  simp only [comp_obj, sheafToPresheaf_obj, sheafPushforwardContinuous_obj_val_obj, yoneda_obj_obj, id_obj,
    sheafToPresheaf_map, sheafAdjunctionCocontinuous_counit_app_val, ranAdjunction_counit]
  exact isIso_ranCounit_app_of_isDenseSubsite G J K Y U X

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