English
If the presheaf F map cone (cocone U)ᵒᵖ is a limit cone, then the equalizer fork SheafConditionEqualizerProducts.fork F U is a limit as well.
Русский
Если конус отображения F map cone (cocone U)ᵒᵖ является пределом, тогда равноселение SheafConditionEqualizerProducts.fork F U тоже является пределом.
LaTeX
$$$\text{IsLimit}\bigl(F.mapCone(\mathrm{cocone}\,U)^{op}\bigr) \Rightarrow \text{IsLimit}\bigl(\mathrm{SheafConditionEqualizerProducts.fork}\,F\,U\bigr).$$$
Lean4
/-- If `F.mapCone (cone U)` is a limit cone,
then `SheafConditionEqualizerProducts.fork` is an equalizer.
-/
def isLimitSheafConditionForkOfIsLimitMapCone (Q : IsLimit (F.mapCone (cocone U).op)) :
IsLimit (SheafConditionEqualizerProducts.fork F U) :=
IsLimit.ofIsoLimit ((IsLimit.ofConeEquiv (coneEquiv F U)).symm Q)
{ hom :=
{ hom := 𝟙 _
w := by
rintro ⟨⟩
· simp
rfl
· dsimp
ext
dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res, SheafConditionEqualizerProducts.leftRes]
simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app, Category.assoc]
rw [← F.map_comp]
rfl }
inv :=
{ hom := 𝟙 _
w := by
rintro ⟨⟩
· simp
rfl
· dsimp
ext
dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res, SheafConditionEqualizerProducts.leftRes]
simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app, Category.assoc]
rw [← F.map_comp]
rfl } }
