isSheaf_iff_of_nat_equiv — Mathlib

English

If P1 and P2 are naturally equivalent presheaves on C and compatible with maps, then P1 is a sheaf for J if and only if P2 is a sheaf for J.

Русский

Если P1 и P2 являются естественно эквивалентными преслещами на C и совместимы с отображениями, то P1 является sheaf для J тогда и только тогда, когда P2 является sheaf для J.

LaTeX

$$$\mathrm{IsSheaf}(J,P_1) \iff \mathrm{IsSheaf}(J,P_2)$$$

Lean4

theorem isSheaf_iff_of_nat_equiv : Presieve.IsSheaf J P₁ ↔ Presieve.IsSheaf J P₂ :=
  ⟨fun hP₁ ↦ isSheaf_of_nat_equiv e he hP₁, fun hP₂ ↦
    isSheaf_of_nat_equiv (fun _ ↦ (@e _).symm)
      (fun X Y f x ↦ by
        obtain ⟨y, rfl⟩ := e.surjective x
        refine e.injective ?_
        simp only [Equiv.apply_symm_apply, Equiv.symm_apply_apply, he])
      hP₂⟩

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