isoSheafify_inv — Mathlib

English

The inverse of isoSheafify is given by the simple lift of the identity morphism.

Русский

Обратное изоморфирования isoSheafify задаётся простым подъёмом тождества морфизма.

LaTeX

$$isoSheafify_inv {P} (hP) : (J.isoSheafify hP).inv = J.sheafifyLift (id) hP$$

Lean4

@[simp]
theorem isoSheafify_inv {P : Cᵒᵖ ⥤ D} (hP : Presheaf.IsSheaf J P) : (J.isoSheafify hP).inv = J.sheafifyLift (𝟙 _) hP :=
  by
  apply J.sheafifyLift_unique
  simp [Iso.comp_inv_eq]

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