golf request: `PushoutCocone ≌ BinaryCofan`

Stream: new members

[Michał Mrugała]

Hiya, there has to be a cleaner way of doing this, but I'm not familiar enough with the category theory API to spot it:

import Mathlib

open CategoryTheory Opposite Limits

section

variable {C : Type*} [Category C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}

@[simp]
def pushoutCocone.toBinaryCofan : PushoutCocone f g ⥤ BinaryCofan (Under.mk f) (Under.mk g) where
  obj c := BinaryCofan.mk (Under.homMk (U := Under.mk f) c.inl rfl)
      (Under.homMk (U := Under.mk g) (V := Under.mk (f ≫ c.inl)) c.inr c.condition.symm)
  map {c1 c2} a := {
    hom := Under.homMk a.hom
    w := by
      rintro (_|_)
      repeat
        ext
        exact a.w _
  }

@[simp]
def binaryCofanUnder.toPushoutCocone :
    BinaryCofan (Under.mk f) (Under.mk g) ⥤ PushoutCocone f g where
  obj c := PushoutCocone.mk c.inl.right c.inr.right (c.inl.w.symm.trans c.inr.w)
  map {c1 c2} a := {
    hom := a.hom.right
    w := by rintro (_|_|_) <;> simp [← Under.comp_right]
  }

def aux_unit :
    𝟭 (PushoutCocone f g) ≅ pushoutCocone.toBinaryCofan ⋙ binaryCofanUnder.toPushoutCocone where
  hom.app c := c.eta.hom
  inv.app c := c.eta.inv
  inv.naturality {c1 c2} a := by ext; simp

@[simp]
def aux_hom :
    binaryCofanUnder.toPushoutCocone ⋙ pushoutCocone.toBinaryCofan
    ⟶ 𝟭 (BinaryCofan (Under.mk f) (Under.mk g)) where
  app c := {
    hom := {
      left := 𝟙 c.pt.left
      right := 𝟙 c.pt.right
      w := by simpa using c.inl.w
    }
    w := by rintro (_|_) <;> { ext; simp }
  }

@[simp]
def aux_inv :
    𝟭 (BinaryCofan (Under.mk f) (Under.mk g))
    ⟶ binaryCofanUnder.toPushoutCocone ⋙ pushoutCocone.toBinaryCofan where
      app c := {
        hom := {
          left := 𝟙 c.pt.left
          right := 𝟙 c.pt.right
          w := by simpa using c.inl.w.symm
        }
        w := by rintro (_|_) <;> { ext; simp }
      }

def aux_counit :
    binaryCofanUnder.toPushoutCocone ⋙ pushoutCocone.toBinaryCofan
    ≅ 𝟭 (BinaryCofan (Under.mk f) (Under.mk g)) where
  hom := aux_hom
  inv := aux_inv
  hom_inv_id := by ext; simp
  inv_hom_id := by ext; simp

def pushoutCoconeEquivBinaryCofan : PushoutCocone f g ≌ BinaryCofan (Under.mk f) (Under.mk g) :=
  .mk pushoutCocone.toBinaryCofan binaryCofanUnder.toPushoutCocone aux_unit aux_counit

end

[Andrew Yang]

The unit is NatIso.ofComponents (fun c ↦ c.eta) (by aesop_cat), and the counit is

  NatIso.ofComponents (fun X ↦ Limits.BinaryCofan.ext (Under.isoMk (Iso.refl _)
    (by simpa using X.inl.w.symm)) (by aesop_cat) (by aesop_cat))
    (by intros; ext; simp [BinaryCofan.ext])

And you should use mk' instead of mk in the final construction of equivalences.

[Michał Mrugała]

Is there a reason to use mk' instead of mk here? It just requires strictly more information.

[Andrew Yang]

mk' gives better defeqs. You can see how mk is done.

[Michał Mrugała]

I know that it adjoinifies, but @Bhavik Mehta seemed to think mk is preferable to use here, unless we care about the half-adjunction.

[Bhavik Mehta]

I don't know that the defeqs actually matter here? The other benefit of mk here was that it's faster (particularly because the version of this code I saw was very close to timing out), but now that it's split up, perhaps that's no longer a factor.

[Joël Riou]

Michał Mrugała said:

I know that it adjoinifies, but Bhavik Mehta seemed to think mk is preferable to use here, unless we care about the half-adjunction.

I think it is better not to bet that nobody will ever need reasonably good definitional properties for unit/counit isomorphisms. In order to make #12728 work, I had to fix unnecessary uses of Equivalence.mk in #15919. When there is no difficulty showing functor_unitIso_comp, we should always use Equivalence.mk'.

[Bhavik Mehta]

Perhaps it would be sensible to add this to the docstrings

[Michał Mrugała]

I'll add this to the golf request as well (goes after the first code block)

def pushoutCocone.IsColimit.toBinaryCofanIsColimit (c : PushoutCocone f g)  (hc : IsColimit c) :
    IsColimit <| pushoutCocone.toBinaryCofan.obj c :=
  BinaryCofan.isColimitMk (fun s ↦
      Under.homMk (hc.desc <| binaryCofanUnder.toPushoutCocone.obj s) (by simpa using s.inl.w.symm))
      (by aesop_cat) (by aesop_cat) (fun s m h₁ h₂ ↦
      (by
        ext
        simp
        apply hc.uniq (binaryCofanUnder.toPushoutCocone.obj s) m.right
        rintro (_|_|_)
        · simp [← h₁]
        · simp [← h₁]
        simp [← h₂]
        ))

[Michał Mrugała]

It feels like I'm doing something wrong since I'm reusing the same arguments I used for the equivalence

[Andrew Yang]

You should use docs#CategoryTheory.Limits.IsColimit.ofCoconeEquiv

[Michał Mrugała]

Much better, though it still feels like I'm missing a way to simplify the end

def pushoutCocone.IsColimit.toBinaryCofanIsColimit (c : PushoutCocone f g)  (hc : IsColimit c) :
    IsColimit <| pushoutCocone.toBinaryCofan.obj c :=
  .ofCoconeEquiv pushoutCoconeEquivBinaryCofan.symm (.ofIsoColimit hc (by simp; exact c.eta))