Moving a CategoryTheory.Equivalence across a Hom

Stream: Is there code for X?

[Eric Wieser]

Do we have something like

def Equivalence.homEquiv {C D : Type u} [Category.{v, u} C] [Category.{v, u} D]
    (e : C ≌ D) (c : C) (d : D) :
    (e.functor.obj c ⟶ d) ≃ (c ⟶ e.inverse.obj d) where
  toFun fd := e.unit.app _ ≫ e.inverse.map fd
  invFun fc := e.functor.map fc ≫ e.counit.app _
  left_inv fd := by
    dsimp only
    simp_rw [Functor.map_comp, Equivalence.fun_inv_map, Functor.id_obj, Category.assoc,
      Equivalence.counit_app_functor, ←Functor.map_comp_assoc, Iso.inv_hom_id_app,
      Functor.id_obj, Functor.comp_obj, Category.comp_id, Iso.hom_inv_id_app, Functor.id_obj,
      Functor.map_id, Category.id_comp]
  right_inv fc := by
    simp_rw [Functor.map_comp, Equivalence.inv_fun_map, Functor.id_obj, Category.assoc,
      Equivalence.unit_inverse_comp, Iso.hom_inv_id_app_assoc, Category.comp_id]

for docs#CategoryTheory.Equivalence ?

[Eric Wieser]

(I'm sure the second sorry is easy enough, but I suspect my approach is suboptimal so didn't want to waste time on it)

[Kevin Buzzard]

@loogle Equivalence, adjoint

[loogle]

:exclamation: unknown identifier 'adjoint'

[Kevin Buzzard]

You're asking why an equivalence is an adjunction

[Adam Topaz]

:magnifying_glass: docs#CategoryTheory.Equivalence.toAdjunction

[Adam Topaz]

That plus docs#CategoryTheory.Adjunction.homEquiv

[Eric Wieser]

Darn, I didn't think of looking in a different file!

[Eric Wieser]

As a follow up, is this proof sensible?

/-- Transport `Limits.IsZero` along an equivalence. -/
theorem Limits.IsZero.transport (e : C ≌ D) {x : C} (hx : IsZero x) : IsZero (e.functor.obj x) where
  unique_to X := hx.unique_to (e.inverse.obj X) |>.map <|
    fun u => @Equiv.unique _ _ u (e.toAdjunction.homEquiv _ _)
  unique_from X := hx.unique_from (e.inverse.obj X) |>.map <|
    fun u => @Equiv.unique _ _ u (e.symm.toAdjunction.homEquiv _ _).symm

[Eric Wieser]

Or am I missing some more obvious API

[Adam Topaz]

We may have this already?

[Adam Topaz]

My loogle-foo is subpar… I’ll have to look the old-fashioned way

[Arend Mellendijk]

(deleted)

[Arend Mellendijk]

@loogle CategoryTheory.Limits.IsZero, CategoryTheory.Equivalence

[loogle]

:shrug: nothing found

[Eric Wieser]

@loogle CategoryTheory.Limits.IsZero, CategoryTheory.IsEquivalence

[loogle]

:shrug: nothing found

[Adam Topaz]

Yeah, I couldn't find it either... Here's how I would do it:

import Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
import Mathlib.CategoryTheory.Adjunction.Limits

open CategoryTheory Limits

variable {C D : Type*} [Category C] [Category D] (e : C ≌ D)
  {X : C} (hX : IsZero X)

def IsZero.ofIinitialOfTerminal (Y : C) (h1 : IsInitial Y) (h2 : IsTerminal Y) :
    IsZero Y where
  unique_to _ := .intro <| .mk (.mk <| h1.to _) fun _ => h1.hom_ext _ _
  unique_from _ := .intro <| .mk (.mk <| h2.from _) fun _ => h2.hom_ext _ _

example : IsZero (e.functor.obj X) :=
  IsZero.ofIinitialOfTerminal _
    (hX.isInitial.isInitialObj e.functor)
    (hX.isTerminal.isTerminalObj e.functor)

[Adam Topaz]

I'm surprised we don't have IsZero.ofIinitialOfTerminal... maybe I missed it?

[Arend Mellendijk]

@loogle |- CategoryTheory.Limits.IsZero _

[loogle]

:search: CategoryTheory.Functor.isZero, CategoryTheory.Limits.isZero_zero, and 20 more

[Eric Wieser]

Note IsZero carries no data so that naming is wrong

[Adam Topaz]

Yeah, I was also careless with making the correct variables implicit.

[Arend Mellendijk]

Isn't it that way to avoid clashes with docs#Zero? I'd assumed that's why docs#Nat.ArithmeticFunction.IsMultiplicative is like that.

[Eric Wieser]

I'm talking about the names in Adam's message not the ones in the docs