English
There is a counit isomorphism between the identity on cones over diagram F and the composition of the forward and inverse cone equivalences.
Русский
Существует изоморфизм counit между тождественным каноном над диаграммой F и композицией эквивалентностей конусов.
LaTeX
$$$\mathrm{coneEquivCounitIso}(F,U) : \mathrm{Id}_{\mathrm{Cone}((\mathrm{diagram}\ U)^{op} \circ F)} \cong (\mathrm{coneEquivFunctor}(F,U) \circ \mathrm{coneEquivInverse}(F,U))$$$
Lean4
/-- Implementation of `SheafConditionPairwiseIntersections.coneEquiv`. -/
@[simps]
def coneEquivInverseObj (c : Limits.Cone (SheafConditionEqualizerProducts.diagram F U)) :
Limits.Cone ((diagram U).op ⋙ F) where
pt := c.pt
π :=
{ app := by
intro x
induction x with
| op x => ?_
rcases x with (⟨i⟩ | ⟨i, j⟩)
· exact c.π.app WalkingParallelPair.zero ≫ Pi.π _ i
· exact c.π.app WalkingParallelPair.one ≫ Pi.π _ (i, j)
naturality := by
intro x y f
induction x with
| op x => ?_
induction y with
| op y => ?_
have ef : f = f.unop.op := rfl
revert ef
generalize f.unop = f'
rintro rfl
rcases x with (⟨i⟩ | ⟨⟩) <;> rcases y with (⟨⟩ | ⟨j, j⟩) <;> rcases f' with ⟨⟩
· dsimp
rw [F.map_id]
simp
· dsimp
simp only [Category.id_comp, Category.assoc]
have h := c.π.naturality WalkingParallelPairHom.left
dsimp [SheafConditionEqualizerProducts.leftRes] at h
simp only [Category.id_comp] at h
have h' := h =≫ Pi.π _ (i, j)
rw [h']
simp only [Category.assoc, limit.lift_π, Fan.mk_π_app]
rfl
· dsimp
simp only [Category.id_comp, Category.assoc]
have h := c.π.naturality WalkingParallelPairHom.right
dsimp [SheafConditionEqualizerProducts.rightRes] at h
simp only [Category.id_comp] at h
have h' := h =≫ Pi.π _ (j, i)
rw [h']
simp
rfl
· dsimp
rw [F.map_id]
simp }
