coneEquivCounitIso — Mathlib

English

The counit isomorphism provides the inverse direction as a natural equivalence between the two cone categories.

Русский

Изоморфизм counit обеспечивает обратное направление как естественное равнообразие между двумя категориями конусов.

LaTeX

$$$\mathrm{coneEquivCounitIso}(F,U) : \mathrm{Cone}\!\left((\mathrm{diagram} U)^{op} \circ F\right) \cong \mathrm{Cone}(\mathrm{TopCatPresheafSheafConditionEqualizerProductsDiagram}(F,U))$$$

Lean4

/-- Implementation of `SheafConditionPairwiseIntersections.coneEquiv`. -/
@[simps!]
def coneEquivCounitIso :
    coneEquivInverse F U ⋙ coneEquivFunctor F U ≅ 𝟭 (Limits.Cone (SheafConditionEqualizerProducts.diagram F U)) :=
  NatIso.ofComponents
    (fun c =>
      { hom :=
          { hom := 𝟙 _
            w := by
              rintro ⟨_ | _⟩
              · dsimp
                ext
                simp
              · dsimp
                ext
                simp }
        inv :=
          { hom := 𝟙 _
            w := by
              rintro ⟨_ | _⟩
              · dsimp
                ext
                simp
              · dsimp
                ext
                simp } })
    fun {c d} f => by
    ext
    dsimp
    simp only [Category.comp_id, Category.id_comp]

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