preservesLimitsOfShape_presheafToSheaf

English

There is an isomorphism between the sheafified objects and the plus-plus functor’s image, realized by whiskering an isomorphism with presheaf-to-sheaf.

Русский

Существует изоморфизм между объektами шейфикаций и образом плюс-плюс функторa, реализованный при помощи преобразования к пресшефу и шейфайю.

LaTeX

$$$ J.plusButSheafIsoPresheafToSheaf J D : J.sheafify P \\cong sheafify J P $$$

Lean4

instance preservesLimitsOfShape_presheafToSheaf [PreservesLimits (forget D)]
    [∀ X : C, Small.{t, max u v} (J.Cover X)ᵒᵖ] : PreservesLimitsOfShape K (plusPlusSheaf J D) :=
  by
  let e := (FinCategory.equivAsType K).symm.trans (AsSmall.equiv.{0, 0, t})
  haveI : HasLimitsOfShape (AsSmall.{t} (FinCategory.AsType K)) D := Limits.hasLimitsOfShape_of_equivalence e
  haveI : FinCategory (AsSmall.{t} (FinCategory.AsType K)) :=
    by
    constructor
    · change Fintype (ULift _)
      infer_instance
    · intro j j'
      change Fintype (ULift _)
      infer_instance
  refine @preservesLimitsOfShape_of_equiv _ _ _ _ _ _ _ _ e.symm _ (show _ from ?_)
  constructor; intro F; constructor; intro S hS; constructor
  apply isLimitOfReflects (sheafToPresheaf J D)
  have : ReflectsLimitsOfShape (AsSmall.{t} (FinCategory.AsType K)) (forget D) :=
    reflectsLimitsOfShape_of_reflectsIsomorphisms
  apply isLimitOfPreserves (J.sheafification D) hS

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