English
Cones over diagram U ⋙ F are equivalent to cones over the standard equalizer diagram for F and U.
Русский
Знаменитые конусы над диаграммой U ⋙ F эквивалентны конусам над стандартной диаграммой равносилок для F и U.
LaTeX
$$$\mathrm{coneEquiv}(F,U): \text{Cone}((\mathrm{diagram}\ U)^{op} \circ F) \simeq \text{Cone}(\mathrm{SheafConditionEqualizerProducts.diagram}(F,U))$$$
Lean4
/-- Implementation of `SheafConditionPairwiseIntersections.coneEquiv`. -/
@[simps]
def coneEquivFunctorObj (c : Cone ((diagram U).op ⋙ F)) : Cone (SheafConditionEqualizerProducts.diagram F U)
where
pt := c.pt
π :=
{ app := fun Z =>
WalkingParallelPair.casesOn Z (Pi.lift fun i : ι => c.π.app (op (single i)))
(Pi.lift fun b : ι × ι => c.π.app (op (pair b.1 b.2)))
naturality := fun Y Z f => by
cases Y <;> cases Z <;> cases f
· dsimp
ext
simp
· dsimp
ext ij
rcases ij with ⟨i, j⟩
simpa [SheafConditionEqualizerProducts.leftRes] using c.π.naturality (Quiver.Hom.op (Hom.left i j))
· dsimp
ext ij
rcases ij with ⟨i, j⟩
simpa [SheafConditionEqualizerProducts.rightRes] using c.π.naturality (Quiver.Hom.op (Hom.right i j))
· dsimp
ext
simp }
