English
For any functor F from WalkingParallelPair to CommRingCat, the projection from the limit (equalizer) to the left object is a local hom.
Русский
Для любой функторной композиции F из WalkingParallelPair в CommRingCat проекция из предела (равняющего) в левый объект является локальным гомоморфизмом.
LaTeX
$$$\\text{IsLocalHom}(\\lim.π\\,F\\;\\text{WalkingParallelPair.zero}.hom)$$$
Lean4
@[instance]
theorem equalizer_ι_isLocalHom (F : WalkingParallelPair ⥤ CommRingCat.{u}) :
IsLocalHom (limit.π F WalkingParallelPair.zero).hom :=
by
have := limMap_π (diagramIsoParallelPair F).hom WalkingParallelPair.zero
rw [← IsIso.comp_inv_eq] at this
rw [← this]
rw [←
limit.isoLimitCone_hom_π
⟨_, equalizerForkIsLimit (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)⟩
WalkingParallelPair.zero]
change IsLocalHom ((lim.map _ ≫ _ ≫ (equalizerFork _ _).ι) ≫ _).hom
infer_instance
