English
For a presheaf P, the IsLimit of a fork built from P.map π.op and the equalizer condition is equivalent to the IsLimit of the mapped cocone over a sieve constructed from X and π.
Русский
Для префункторa P равносильны изоморфизмы Fork_ofι и IsLimit для диаграммы, полученной из P.map π.op и условия равнозначителя, и IsLimit сопоставленного кокона над решетом, построенном из X и π.
LaTeX
$$IsLimit (Fork.ofι (P.map π.op) (equalizerCondition_w P c)) ≃ IsLimit (P.mapCone (Sieve.ofArrows (fun x => X) (fun x => π)).arrows.cocone.op)$$
Lean4
/-- Given a limiting pullback cone, the fork in `SingleEqualizerCondition` is limiting iff the diagram
in `Presheaf.isSheaf_iff_isLimit_coverage` is limiting.
-/
noncomputable def isLimit_forkOfι_equiv (P : Cᵒᵖ ⥤ D) {X B : C} (π : X ⟶ B) (c : PullbackCone π π) (hc : IsLimit c) :
IsLimit (Fork.ofι (P.map π.op) (equalizerCondition_w P c)) ≃
IsLimit (P.mapCone (Sieve.ofArrows (fun (_ : Unit) ↦ X) fun _ ↦ π).arrows.cocone.op) :=
by
let S := (Sieve.ofArrows (fun (_ : Unit) => X) (fun _ => π)).arrows
let X' := S.categoryMk π ⟨_, 𝟙 _, π, ofArrows.mk (), Category.id_comp _⟩
let P' := S.categoryMk (c.fst ≫ π) ⟨_, c.fst, π, ofArrows.mk (), rfl⟩
let fst : P' ⟶ X' := Over.homMk c.fst
let snd : P' ⟶ X' := Over.homMk c.snd c.condition.symm
let F : S.categoryᵒᵖ ⥤ D := S.diagram.op ⋙ P
let G := parallelPair (P.map c.fst.op) (P.map c.snd.op)
let H := parallelPair fst.op snd.op
have : H.Initial := parallelPair_pullback_initial π c hc
let i : H ⋙ F ≅ G := parallelPair.ext (Iso.refl _) (Iso.refl _) (by aesop) (by aesop)
refine (IsLimit.equivOfNatIsoOfIso i.symm _ _ ?_).trans (Functor.Initial.isLimitWhiskerEquiv H _)
refine Cones.ext (Iso.refl _) ?_
rintro ⟨_ | _⟩
all_goals aesop
