pullbackConeEquivBinaryFanFunctor

Lean4
/-- A binary fan in `Over X` is a limit if its corresponding pullback cone to `X` is a limit. -/
-- `IsLimit.ofConeEquiv` isn't used here because the lift it defines is `𝟙 _ ≫ pullback.lift`.
-- TODO: Define `IsLimit.copy`?

@[simps!]
def pullbackConeEquivBinaryFanFunctor {c : PullbackCone f g} (hc : IsLimit c) :
    IsLimit <| pullbackConeEquivBinaryFan.functor.obj c :=
  BinaryFan.isLimitMk
    (fun s ↦ Over.homMk (hc.lift <| pullbackConeEquivBinaryFan.inverse.obj s) <| by simpa using s.fst.w)
    (fun s ↦ Over.OverMorphism.ext (hc.fac _ _)) (fun s ↦ Over.OverMorphism.ext (hc.fac _ _)) fun s m e₁ e₂ ↦
    by
    ext1
    apply PullbackCone.IsLimit.hom_ext hc
    · simpa using congr(($e₁).left)
    · simpa using congr(($e₂).left)
Похожие утверждения