From cf0049ec812ebc91c7295af712a53f415308a142 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Sun, 20 Oct 2024 19:54:50 +0000 Subject: [PATCH] feat(CategoryTheory): natural version of `FullyFaithful.homEquiv` (#17450) --- Mathlib/CategoryTheory/Yoneda.lean | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean index 61b37dc22ad22..5116a9b934fd8 100644 --- a/Mathlib/CategoryTheory/Yoneda.lean +++ b/Mathlib/CategoryTheory/Yoneda.lean @@ -24,7 +24,7 @@ namespace CategoryTheory open Opposite -universe v v₁ u₁ u₂ +universe v v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [CategoryTheory universes]. variable {C : Type u₁} [Category.{v₁} C] @@ -767,4 +767,24 @@ lemma yonedaMap_app_apply {Y : C} {X : Cᵒᵖ} (f : X.unop ⟶ Y) : end +namespace Functor.FullyFaithful + +variable {C : Type u₁} [Category.{v₁} C] + +/-- `FullyFaithful.homEquiv` as a natural isomorphism. -/ +def homNatIso {D : Type u₂} [Category.{v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful) (X : C) : + F.op ⋙ yoneda.obj (F.obj X) ⋙ uliftFunctor.{v₁} ≅ yoneda.obj X ⋙ uliftFunctor.{v₂} := + NatIso.ofComponents + (fun Y => Equiv.toIso (Equiv.ulift.trans <| hF.homEquiv.symm.trans Equiv.ulift.symm)) + (fun f => by ext; exact Equiv.ulift.injective (hF.map_injective (by simp))) + +/-- `FullyFaithful.homEquiv` as a natural isomorphism. -/ +def homNatIsoMaxRight {D : Type u₂} [Category.{max v₁ v₂} D] {F : C ⥤ D} (hF : F.FullyFaithful) + (X : C) : F.op ⋙ yoneda.obj (F.obj X) ≅ yoneda.obj X ⋙ uliftFunctor.{v₂} := + NatIso.ofComponents + (fun Y => Equiv.toIso (hF.homEquiv.symm.trans Equiv.ulift.symm)) + (fun f => by ext; exact Equiv.ulift.injective (hF.map_injective (by simp))) + +end Functor.FullyFaithful + end CategoryTheory