isSheafForIsSheafFor' — Mathlib

English

An auxiliary equivalence for IsSheafForIsSheafFor' connecting Symmetric limits with Discrete functors, under HasPullbacks and HasProducts assumptions.

Русский

Вспомогательное соответствие IsSheafForIsSheafFor', связывающее симметричные пределы с дискретными функторами при наличии HasPullbacks и HasProducts.

LaTeX

$$IsSheafForIsSheafFor' (P) (s) (U) (R) : Equiv (IsLimit (s.mapCone (Fork.ofι (Presheaf.forkMap R P) ⋯))) (IsLimit (Fork.ofι (Equalizer.forkMap (P.comp s) R) ⋯)).$$

Lean4

/-- (Implementation). An auxiliary lemma to convert between sheaf conditions. -/
def isSheafForIsSheafFor' (P : Cᵒᵖ ⥤ A) (s : A ⥤ Type max v₁ u₁)
    [∀ J, PreservesLimitsOfShape (Discrete.{max v₁ u₁} J) s] (U : C) (R : Presieve U) :
    IsLimit (s.mapCone (Fork.ofι _ (w R P))) ≃ IsLimit (Fork.ofι _ (Equalizer.Presieve.w (P ⋙ s) R)) :=
  by
  let e :
    parallelPair (s.map (firstMap R P)) (s.map (secondMap R P)) ≅
      parallelPair (Equalizer.Presieve.firstMap (P ⋙ s) R) (Equalizer.Presieve.secondMap (P ⋙ s) R) :=
    by
    refine
      parallelPair.ext (PreservesProduct.iso s _) ((PreservesProduct.iso s _)) (limit.hom_ext (fun j => ?_))
        (limit.hom_ext (fun j => ?_))
    · dsimp [Equalizer.Presieve.firstMap, firstMap]
      simp only [map_lift_piComparison, Functor.map_comp, limit.lift_π, Fan.mk_pt, Fan.mk_π_app, assoc,
        piComparison_comp_π_assoc]
    · dsimp [Equalizer.Presieve.secondMap, secondMap]
      simp only [map_lift_piComparison, Functor.map_comp, limit.lift_π, Fan.mk_pt, Fan.mk_π_app, assoc,
        piComparison_comp_π_assoc]
  refine Equiv.trans (isLimitMapConeForkEquiv _ _) ?_
  refine (IsLimit.postcomposeHomEquiv e _).symm.trans (IsLimit.equivIsoLimit (Fork.ext (Iso.refl _) ?_))
  dsimp [Equalizer.forkMap, forkMap, e, Fork.ι]
  simp only [id_comp, map_lift_piComparison]
    -- Remark : this lemma uses `A'` not `A`; `A'` is `A` but with a universe
    -- restriction. Can it be generalised?

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