Ulift functor for ModuleCat

In this file, we define the obvious functor ModuleCat.{v} R ⥤ ModuleCat.{max v v'} R and prove it is exact, fully faithful and preverves projective and injective objects.

def ModuleCat.uliftFunctor (R : Type u) [Ring R] : CategoryTheory.Functor (ModuleCat R) (ModuleCat R)

Universe lift functor for R-module.

@[simp]

theorem ModuleCat.uliftFunctor_obj (R : Type u) [Ring R] (X : ModuleCat R) : (uliftFunctor.{v', v, u} R).obj X = of R (ULift.{v', v} ↑X)

@[simp]

theorem ModuleCat.uliftFunctor_map (R : Type u) [Ring R] {X✝ Y✝ : ModuleCat R} (f : X✝ ⟶ Y✝) : (uliftFunctor.{v', v, u} R).map f = ofHom (↑ULift.moduleEquiv.symm ∘ₗ Hom.hom f ∘ₗ ↑ULift.moduleEquiv)

def ModuleCat.fullyFaithfulUliftFunctor (R : Type u) [Ring R] : (uliftFunctor.{u_2, u_1, u} R).FullyFaithful

The universe lift functor for R-module is fully faithful.

def ModuleCat.uliftFunctorForgetIso (R : Type u) [Ring R] : (uliftFunctor.{v', u_1, u} R).comp (CategoryTheory.forget (ModuleCat R)) ≅ (CategoryTheory.forget (ModuleCat R)).comp CategoryTheory.uliftFunctor.{v', u_1}

The ULift functor on ModuleCat is compatible with the one defined on categories of types.

@[simp]

theorem ModuleCat.uliftFunctorForgetIso_inv_app (R : Type u) [Ring R] (X : ModuleCat R) (a✝ : ((uliftFunctor.{v', u_1, u} R).comp (CategoryTheory.forget (ModuleCat R))).obj X) : (uliftFunctorForgetIso R).inv.app X a✝ = a✝

@[simp]

theorem ModuleCat.uliftFunctorForgetIso_hom_app (R : Type u) [Ring R] (X : ModuleCat R) (a✝ : ((uliftFunctor.{v', u_1, u} R).comp (CategoryTheory.forget (ModuleCat R))).obj X) : (uliftFunctorForgetIso R).hom.app X a✝ = a✝

instance ModuleCat.instFullUliftFunctor (R : Type u) [Ring R] : (uliftFunctor.{v', v, u} R).Full

instance ModuleCat.instFaithfulUliftFunctor (R : Type u) [Ring R] : (uliftFunctor.{v', v, u} R).Faithful

instance ModuleCat.instAdditiveUliftFunctor (R : Type u) [Ring R] : (uliftFunctor.{u_2, u_1, u} R).Additive

instance ModuleCat.instPreservesLimitsOfSizeUliftFunctor (R : Type u) [Ring R] : CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, v, max v v', max u (v + 1), max (max u (v + 1)) (v' + 1)} (uliftFunctor.{v', v, u} R)

instance ModuleCat.instPreservesFiniteLimitsUliftFunctor (R : Type u) [Ring R] : CategoryTheory.Limits.PreservesFiniteLimits (uliftFunctor.{v', v, u} R)

theorem ModuleCat.uliftFunctor_map_exact (R : Type u) [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (h : S.Exact) : (S.map (uliftFunctor.{u_1, v, u} R)).Exact

instance ModuleCat.instPreservesFiniteColimitsUliftFunctor (R : Type u) [Ring R] : CategoryTheory.Limits.PreservesFiniteColimits (uliftFunctor.{v', v, u} R)

instance ModuleCat.instPreservesProjectiveObjectsUliftFunctorOfSmall (R : Type u) [Ring R] [Small.{v, u} R] : (uliftFunctor.{v', v, u} R).PreservesProjectiveObjects

instance ModuleCat.instPreservesInjectiveObjectsUliftFunctorOfSmall (R : Type u) [Ring R] [Small.{v, u} R] : (uliftFunctor.{v', v, u} R).PreservesInjectiveObjects

instance ModuleCat.instLinearUliftFunctor (R : Type u) [CommRing R] : CategoryTheory.Functor.Linear R (uliftFunctor.{v', v, u} R)