English
For a contravariant diagram F: WalkingParallelPair^op → CommRingCat, the projection from the limit to the opposite zero/one corner is a local hom.
Русский
Для контравариантного диаграммного F: WalkingParallelPair^op → CommRingCat проекция из предела к противоположному нулю/единице угла — локальный гомоморфизм.
LaTeX
$$$\\text{IsLocalHom}(\\lim.π\\,F\\;(\\text{Opposite.op }\\mathrm{WalkingParallelPair.one}).hom)$$$
Lean4
instance equalizer_ι_isLocalHom' (F : WalkingParallelPairᵒᵖ ⥤ CommRingCat.{u}) :
IsLocalHom (limit.π F (Opposite.op WalkingParallelPair.one)).hom :=
by
have :=
limit.isoLimitCone_inv_π ⟨_, IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv⟩
WalkingParallelPair.zero
dsimp at this
rw [← this]
-- note: this was not needed before https://github.com/leanprover-community/mathlib4/pull/19757
have : IsLocalHom (limit.π (walkingParallelPairOp ⋙ F) zero).hom := by infer_instance
infer_instance
