Documentation

Mathlib.Algebra.Category.ModuleCat.Ulift

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 preserves projective and injective objects.

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

Universe lift functor for R-module.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem ModuleCat.uliftFunctor_obj (R : Type u) [Ring R] (X : ModuleCat R) :
    (uliftFunctor.{v', v, u} R).obj X = ↧(ULift.{v', v} ↑X)
    source
    @[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)
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      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.

      Equations
      Instances For
        source
        @[simp]
        theorem ModuleCat.uliftFunctorForgetIso_inv_app_hom_apply (R : Type u) [Ring R] (X : ModuleCat R) (a : ((uliftFunctor.{v', u_1, u} R).comp (CategoryTheory.forget (ModuleCat R))).obj X) :
        (CategoryTheory.ConcreteCategory.hom ((uliftFunctorForgetIso R).inv.app X)) a = a
        source
        @[simp]
        theorem ModuleCat.uliftFunctorForgetIso_hom_app_hom_apply (R : Type u) [Ring R] (X : ModuleCat R) (a : ((uliftFunctor.{v', u_1, u} R).comp (CategoryTheory.forget (ModuleCat R))).obj X) :
        (CategoryTheory.ConcreteCategory.hom ((uliftFunctorForgetIso R).hom.app X)) a = a
        source
        instance ModuleCat.instFullUliftFunctor (R : Type u) [Ring R] :
        (uliftFunctor.{v', v, u} R).Full
        source
        instance ModuleCat.instFaithfulUliftFunctor (R : Type u) [Ring R] :
        (uliftFunctor.{v', v, u} R).Faithful
        source
        instance ModuleCat.instAdditiveUliftFunctor (R : Type u) [Ring R] :
        (uliftFunctor.{u_2, u_1, u} R).Additive
        source
        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)
        source
        instance ModuleCat.instPreservesFiniteLimitsUliftFunctor (R : Type u) [Ring R] :
        CategoryTheory.Limits.PreservesFiniteLimits (uliftFunctor.{v', v, u} R)
        source
        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
        source
        instance ModuleCat.instPreservesFiniteColimitsUliftFunctor (R : Type u) [Ring R] :
        CategoryTheory.Limits.PreservesFiniteColimits (uliftFunctor.{v', v, u} R)
        source
        instance ModuleCat.instPreservesProjectiveObjectsUliftFunctorOfSmall (R : Type u) [Ring R] [Small.{v, u} R] :
        (uliftFunctor.{v', v, u} R).PreservesProjectiveObjects
        source
        instance ModuleCat.instPreservesInjectiveObjectsUliftFunctorOfSmall (R : Type u) [Ring R] [Small.{v, u} R] :
        (uliftFunctor.{v', v, u} R).PreservesInjectiveObjects
        source
        instance ModuleCat.instLinearUliftFunctor (R : Type u) [CommRing R] :
        CategoryTheory.Functor.Linear R (uliftFunctor.{v', v, u} R)