coneEquivInverse — Mathlib

English

There is a unit isomorphism for the equivalence between cones over the pairwise diagram and cones over the equalizer diagram.

Русский

Существует модуль единичного изоморфизма для эквивалентности конусов между диаграммой Pairwise и диаграммой равносилки.

LaTeX

$$$\mathrm{coneEquivUnitIso}(F,U) : \mathbf{1} \to (\mathrm{coneEquivFunctor}(F,U) \circ \mathrm{coneEquivInverse}(F,U))$$$

Lean4

/-- Implementation of `SheafConditionPairwiseIntersections.coneEquiv`. -/
@[simps!]
def coneEquivInverse : Limits.Cone (SheafConditionEqualizerProducts.diagram F U) ⥤ Limits.Cone ((diagram U).op ⋙ F)
    where
  obj c := coneEquivInverseObj F U c
  map {c c'}
    f :=
    { hom := f.hom
      w := by
        intro x
        induction x with
        | op x => ?_
        rcases x with (⟨i⟩ | ⟨i, j⟩)
        · dsimp
          dsimp only [Fork.ι]
          rw [← f.w WalkingParallelPair.zero, Category.assoc]
        · dsimp
          rw [← f.w WalkingParallelPair.one, Category.assoc] }

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