hasSheafCompose — Mathlib

English

Transporting HasSheafify across an equivalence induces a HasSheafCompose structure for a functor F.

Русский

Перенос HasSheafify через эквивалентность порождает структуру HasSheafCompose для F.

LaTeX

$$hasSheafCompose: J.HasSheafCompose F$$

Lean4

theorem hasSheafCompose : J.HasSheafCompose F where
  isSheaf P
    hP :=
    by
    have hP' : Presheaf.IsSheaf K (e.inverse.op ⋙ P ⋙ F) :=
      by
      change Presheaf.IsSheaf K ((_ ⋙ _) ⋙ _)
      apply HasSheafCompose.isSheaf
      exact e.inverse.op_comp_isSheaf K J ⟨P, hP⟩
    replace hP' : Presheaf.IsSheaf J (e.functor.op ⋙ e.inverse.op ⋙ P ⋙ F) := e.functor.op_comp_isSheaf _ _ ⟨_, hP'⟩
    exact (Presheaf.isSheaf_of_iso_iff ((isoWhiskerRight e.op.unitIso.symm (P ⋙ F)))).mp hP'

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