coneEquivUnitIsoApp — Mathlib

English

Cones over diagram U ⋙ F are equivalent to cones over the standard sheaf-condition diagram.

Русский

Коны диаграммы U ⋙ F эквивалентны конам стандартной диаграммы условияSheaf.

LaTeX

$$$\mathrm{coneEquiv}(F,U) : \mathrm{Cone}((\mathrm{diagram}\ U)^{op} \circ F) \simeq \mathrm{Cone}(\mathrm{SheafConditionEqualizerProducts.diagram}(F,U))$$$

Lean4

/-- Implementation of `SheafConditionPairwiseIntersections.coneEquiv`. -/
@[simps]
def coneEquivUnitIsoApp (c : Cone ((diagram U).op ⋙ F)) :
    (𝟭 (Cone ((diagram U).op ⋙ F))).obj c ≅ (coneEquivFunctor F U ⋙ coneEquivInverse F U).obj c
    where
  hom :=
    { hom := 𝟙 _
      w := fun j =>
        by
        induction j with
        | op j => ?_
        rcases j with ⟨⟩ <;>
          · dsimp [coneEquivInverse]
            simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π] }
  inv :=
    { hom := 𝟙 _
      w := fun j =>
        by
        induction j with
        | op j => ?_
        rcases j with ⟨⟩ <;>
          · dsimp [coneEquivInverse]
            simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π] }

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