Multiplicative version of CategoryTheory.equivOfFullyFaithfu

Stream: Is there code for X?

[Christian Merten]

Is there a multiplicative version of CategoryTheory.equivOfFullyFaithful? I.e.

import Mathlib

open CategoryTheory Functor

def equivMulOfFullyFaithful {C : Type u} [Category.{v, u} C] {D : Type u₁}
    [Category.{v₁, u₁} D] (F : C ⥤ D)
    [Full F] [Faithful F] {X : C } :
    End X ≃* End (F.obj X) := by
  apply MulEquiv.mk'
  intro f g
  erw [equivOfFullyFaithful_apply, equivOfFullyFaithful_apply,
    equivOfFullyFaithful_apply]
  simp only [End.mul_def, map_comp]

This is essentially the equivalence version of CategoryTheory.Functor.mapEnd. Same question for Aut.

[Yury G. Kudryashov]

loogle doesn't find any: @loogle CategoryTheory.Full, MulEquiv

[loogle]

:shrug: nothing found

[Yury G. Kudryashov]

def mulEquivOfFullyFaithful {C : Type u} [Category.{v, u} C] {D : Type u₁}
    [Category.{v₁, u₁} D] (F : C ⥤ D)
    [Full F] [Faithful F] {X : C} :
    End X ≃* End (F.obj X) where
  toEquiv := equivOfFullyFaithful F
  __ := mapEnd X F

[Christian Merten]

I added @[simps!] (! because lean complained about @[simps] alone). How do I see which simp lemmas are generated?

[Kevin Buzzard]

You can write whatsnew in before your declaration, or perhaps append a ? after simps! (not sure if this works)

[Christian Merten]

Adding ? worked. Thanks! @[simps!?] looks quite funny.

[Christian Merten]

Even @[simps?!] works :D

[Christian Merten]

#9566