English
Given a pullback cone π: X ← W → B and a morphism π, a canonical constructed parallel pair in a presieve is Initial.
Русский
У данного конуса pullback с π: X → B и морфизмом π каноническая конструкция параллельной пары в пресейве является Initial.
LaTeX
$$parallelPair_initial_mk$$
Lean4
theorem parallelPair_pullback_initial {X B : C} (π : X ⟶ B) (c : PullbackCone π π) (hc : IsLimit c) :
(parallelPair (C := (Sieve.ofArrows (fun (_ : Unit) => X) (fun _ => π)).arrows.categoryᵒᵖ) (Y :=
op ((Presieve.categoryMk _ (c.fst ≫ π) ⟨_, c.fst, π, ofArrows.mk (), rfl⟩))) (X :=
op ((Presieve.categoryMk _ π (Sieve.ofArrows_mk _ _ Unit.unit)))) (Quiver.Hom.op (Over.homMk c.fst))
(Quiver.Hom.op (Over.homMk c.snd c.condition.symm))).Initial :=
by
apply Limits.parallelPair_initial_mk
· intro ⟨Z⟩
obtain ⟨_, f, g, ⟨⟩, hh⟩ := Z.property
let X' : (Presieve.ofArrows (fun () ↦ X) (fun () ↦ π)).category := Presieve.categoryMk _ π (ofArrows.mk ())
let f' : Z.obj.left ⟶ X'.obj.left := f
exact ⟨(Over.homMk f').op⟩
· intro ⟨Z⟩ ⟨i⟩ ⟨j⟩
let ij := PullbackCone.IsLimit.lift hc i.left j.left (by erw [i.w, j.w]; rfl)
refine ⟨Quiver.Hom.op (Over.homMk ij (by simpa [ij] using i.w)), ?_, ?_⟩
all_goals congr
all_goals exact Comma.hom_ext _ _ (by erw [Over.comp_left]; simp [ij]) rfl
