pushoutCoconeEquivBinaryCofan — Mathlib

Lean4
/-- Pushout cocones from `X` are the same thing as binary cofans in `Under X`. -/
@[simps]
def pushoutCoconeEquivBinaryCofan : PushoutCocone f g ≌ BinaryCofan (Under.mk f) (.mk g)
    where
  functor.obj
    c :=
    .mk (Under.homMk (U := .mk f) (V := .mk (f ≫ c.inl)) c.inl rfl)
      (Under.homMk (U := .mk g) (V := .mk (f ≫ c.inl)) c.inr c.condition.symm)
  functor.map {c₁ c₂} a := { hom := Under.homMk a.hom, w := by rintro (_ | _) <;> cat_disch }
  inverse.obj c := .mk c.inl.right c.inr.right (c.inl.w.symm.trans c.inr.w)
  inverse.map {c₁ c₂}
    a :=
    { hom := a.hom.right
      w := by rintro (_ | _ | _) <;> simp [← Under.comp_right] }
  unitIso := NatIso.ofComponents (fun c ↦ c.eta) (fun f ↦ by ext; simp)
  counitIso :=
    NatIso.ofComponents
      (fun X ↦
        BinaryCofan.ext (Under.isoMk (.refl _) (by dsimp; simpa using X.inl.w.symm)) (by ext; simp) (by ext; simp))
      (by intros; ext; simp)
  functor_unitIso_comp c := by ext; simp
Похожие утверждения