isIso_toSheafify — Mathlib

English

If P is a sheaf for J, then the canonical map toSheafify J P is an isomorphism.

Русский

Если P является sheaf для J, то каноническое отображение toSheafify J P является изоморфизмом.

LaTeX

$$IsIso (toSheafify J P)$$

Lean4

theorem isIso_toSheafify {P : Cᵒᵖ ⥤ D} (hP : Presheaf.IsSheaf J P) : IsIso (toSheafify J P) :=
  by
  refine ⟨(sheafificationAdjunction J D |>.counit.app ⟨P, hP⟩).val, ?_, ?_⟩
  · change _ = (𝟙 (sheafToPresheaf J D ⋙ 𝟭 (Cᵒᵖ ⥤ D)) :).app ⟨P, hP⟩
    rw [← sheafificationAdjunction J D |>.right_triangle]
    rfl
  · change (sheafToPresheaf _ _).map _ ≫ _ = _
    change _ ≫ (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj ⟨P, hP⟩) = _
    rw [← (sheafificationAdjunction J D).inv_counit_map (X := ⟨P, hP⟩)]
    simp

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