Lifting a linear functor through a fully faithful realization #
noncomputable def
MagnitudeConjecture.CategoryTheory.fullyFaithfulObjectLift
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v, u₃} E]
(F : CategoryTheory.Functor D E)
[F.Full]
[F.Faithful]
(G : CategoryTheory.Functor C E)
(obj : C → D)
(e : (X : C) → F.obj (obj X) ≅ G.obj X)
:
CategoryTheory.Functor C D
Lift the maps of a functor to specified objects in a fully faithful realization.
Instances For
instance
MagnitudeConjecture.CategoryTheory.fullyFaithfulObjectLift_additive
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
[CategoryTheory.Preadditive C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
[CategoryTheory.Preadditive D]
{E : Type u₃}
[CategoryTheory.Category.{v, u₃} E]
[CategoryTheory.Preadditive E]
(F : CategoryTheory.Functor D E)
[F.Full]
[F.Faithful]
[F.Additive]
(G : CategoryTheory.Functor C E)
[G.Additive]
(obj : C → D)
(e : (X : C) → F.obj (obj X) ≅ G.obj X)
:
(fullyFaithfulObjectLift F G obj e).Additive
instance
MagnitudeConjecture.CategoryTheory.fullyFaithfulObjectLift_linear
{k : Type v}
[Field k]
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k D]
{E : Type u₃}
[CategoryTheory.Category.{v, u₃} E]
[CategoryTheory.Preadditive E]
[CategoryTheory.Linear k E]
(F : CategoryTheory.Functor D E)
[F.Full]
[F.Faithful]
[CategoryTheory.Functor.Linear k F]
(G : CategoryTheory.Functor C E)
[CategoryTheory.Functor.Linear k G]
(obj : C → D)
(e : (X : C) → F.obj (obj X) ≅ G.obj X)
:
CategoryTheory.Functor.Linear k (fullyFaithfulObjectLift F G obj e)
instance
MagnitudeConjecture.CategoryTheory.fullyFaithfulObjectLift_faithful
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v, u₃} E]
(F : CategoryTheory.Functor D E)
[F.Full]
[F.Faithful]
(G : CategoryTheory.Functor C E)
(obj : C → D)
(e : (X : C) → F.obj (obj X) ≅ G.obj X)
[G.Faithful]
:
(fullyFaithfulObjectLift F G obj e).Faithful
instance
MagnitudeConjecture.CategoryTheory.fullyFaithfulObjectLift_full
{C : Type u₁}
[CategoryTheory.Category.{v, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v, u₃} E]
(F : CategoryTheory.Functor D E)
[F.Full]
[F.Faithful]
(G : CategoryTheory.Functor C E)
(obj : C → D)
(e : (X : C) → F.obj (obj X) ≅ G.obj X)
[G.Full]
:
(fullyFaithfulObjectLift F G obj e).Full