coneEquiv — Mathlib

English

There is an equivalence between the diagram of a presheaf and the equalizer-based diagram describing the sheaf condition for a cover U.

Русский

Существует эквивалентность между диаграммой преп presheaf и диаграммой равносилок, описывающей условиеSheaf для покрытия U.

LaTeX

$$$\mathrm{diagram}(F,U) \simeq \mathrm{SheafConditionEqualizerProducts.diagram}(F,U)$$$

Lean4

/-- Cones over `diagram U ⋙ F` are the same as a cones over the usual sheaf condition equalizer diagram.
-/
@[simps]
def coneEquiv : Limits.Cone ((diagram U).op ⋙ F) ≌ Limits.Cone (SheafConditionEqualizerProducts.diagram F U)
    where
  functor := coneEquivFunctor F U
  inverse := coneEquivInverse F U
  unitIso := coneEquivUnitIso F U
  counitIso := coneEquivCounitIso F U

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