isSheafFor_singleton_iso — Mathlib

English

If there is an isomorphism i: P ≅ P' then IsSheafFor P R implies IsSheafFor P' R.

Русский

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

LaTeX

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

Lean4

/-- Every presheaf is a sheaf for the family {𝟙 X}.

[Elephant] C2.1.5(i)
-/
theorem isSheafFor_singleton_iso (P : Cᵒᵖ ⥤ Type w) : IsSheafFor P (Presieve.singleton (𝟙 X)) :=
  by
  intro x _
  refine ⟨x _ (Presieve.singleton_self _), ?_, ?_⟩
  · rintro _ _ ⟨rfl, rfl⟩
    simp
  · intro t ht
    simpa using ht _ (Presieve.singleton_self _)

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