parallelPairIsoParallelPairCompIndYoneda

Lean4

/-- Given an `IndParallelPairPresentation f g`, we can understand the parallel pair `(f, g)` as
the colimit of `(P.φ, P.ψ)` in `Ind C`. -/
noncomputable def parallelPairIsoParallelPairCompIndYoneda {A B : Ind C} {f g : A ⟶ B}
    (P : IndParallelPairPresentation ((Ind.inclusion _).map f) ((Ind.inclusion _).map g)) :
    parallelPair f g ≅ parallelPair P.φ P.ψ ⋙ Ind.lim P.I :=
  ((whiskeringRight WalkingParallelPair _ _).obj (Ind.inclusion C)).preimageIso <|
    diagramIsoParallelPair _ ≪≫
      P.parallelPairIsoParallelPairCompYoneda ≪≫ isoWhiskerLeft (parallelPair _ _) Ind.limCompInclusion.symm

Похожие утверждения