isSheafFor_iso — Mathlib

English

If i : P ≅ P' is an isomorphism, IsSheafFor P R implies IsSheafFor P' R; dual version of isSheafFor_iso.

Русский

Если i : P ≅ P' изоморфизм, то IsSheafFor P R влечёт IsSheafFor P' R; симметрично.

LaTeX

$$isSheafFor_iso {P' : Cᵒᵖ ⥤ Type w} (i : CategoryTheory.Iso P P') (hP : IsSheafFor P R) : IsSheafFor P' R$$

Lean4

/-- If `P` is a sheaf for `S`, and it is iso to `P'`, then `P'` is a sheaf for `S`. This shows that
"being a sheaf for a presieve" is a mathematical or hygienic property.
-/
theorem isSheafFor_iso {P' : Cᵒᵖ ⥤ Type w} (i : P ≅ P') (hP : IsSheafFor P R) : IsSheafFor P' R :=
  isSheafFor_of_nat_equiv (fun X ↦ (i.app (op X)).toEquiv) (fun _ _ f x ↦ congr_fun (i.hom.naturality f.op) x) hP

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