Documentation

Mathlib.Algebra.Category.FGModuleCat.Basic

The category of finitely generated modules over a ring #

This introduces FGModuleCat R, the category of finitely generated modules over a ring R. It is implemented as a full subcategory on a subtype of ModuleCat R.

When K is a field, FGModuleCatCat K is the category of finite dimensional vector spaces over K.

We first create the instance as a preadditive category. When R is commutative we then give the structure as an R-linear monoidal category. When R is a field we give it the structure of a closed monoidal category and then as a right-rigid monoidal category.

Future work #

def FGModuleCat (R : Type u) [Ring R] :
Type (u + 1)

Define FGModuleCat as the subtype of ModuleCat.{u} R of finitely generated modules.

Equations
Instances For
    def FGModuleCat.carrier {R : Type u} [Ring R] (M : FGModuleCat R) :

    A synonym for M.obj.carrier, which we can mark with @[coe].

    Equations
    • M = M.obj
    Instances For
      Equations
      • instCoeSortFGModuleCatType = { coe := FGModuleCat.carrier }
      @[simp]
      theorem obj_carrier {R : Type u} [Ring R] (M : FGModuleCat R) :
      M.obj = M
      instance instAddCommGroupCarrier {R : Type u} [Ring R] (M : FGModuleCat R) :
      Equations
      instance instModuleCarrier {R : Type u} [Ring R] (M : FGModuleCat R) :
      Module R M
      Equations
      Equations
      • instLargeCategoryFGModuleCat = id inferInstance
      instance instFunLikeHomFGModuleCatCarrier {R : Type u} [Ring R] {M : FGModuleCat R} {N : FGModuleCat R} :
      FunLike (M N) M N
      Equations
      • instFunLikeHomFGModuleCatCarrier = LinearMap.instFunLike
      instance instLinearMapClassHomFGModuleCatCarrier {R : Type u} [Ring R] {M : FGModuleCat R} {N : FGModuleCat R} :
      LinearMapClass (M N) R M N
      Equations
      • =
      Equations
      • instConcreteCategoryFGModuleCat = id inferInstance
      Equations
      • instPreadditiveFGModuleCat = id inferInstance
      instance FGModuleCat.finite (R : Type u) [Ring R] (V : FGModuleCat R) :
      Equations
      • =
      Equations
      def FGModuleCat.of (R : Type u) [Ring R] (V : Type u) [AddCommGroup V] [Module R V] [Module.Finite R V] :

      Lift an unbundled finitely generated module to FGModuleCat R.

      Equations
      Instances For
        instance FGModuleCat.instFiniteCarrier (R : Type u) [Ring R] (V : FGModuleCat R) :
        Equations
        • =
        def FGModuleCat.isoToLinearEquiv {R : Type u} [Ring R] {V : FGModuleCat R} {W : FGModuleCat R} (i : V W) :
        V ≃ₗ[R] W

        Converts and isomorphism in the category FGModuleCat R to a LinearEquiv between the underlying modules.

        Equations
        Instances For
          @[simp]
          theorem LinearEquiv.toFGModuleCatIso_inv {R : Type u} [Ring R] {V : Type u} {W : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] [AddCommGroup W] [Module R W] [Module.Finite R W] (e : V ≃ₗ[R] W) :
          e.toFGModuleCatIso.inv = e.symm
          @[simp]
          theorem LinearEquiv.toFGModuleCatIso_hom {R : Type u} [Ring R] {V : Type u} {W : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] [AddCommGroup W] [Module R W] [Module.Finite R W] (e : V ≃ₗ[R] W) :
          e.toFGModuleCatIso.hom = e
          def LinearEquiv.toFGModuleCatIso {R : Type u} [Ring R] {V : Type u} {W : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] [AddCommGroup W] [Module R W] [Module.Finite R W] (e : V ≃ₗ[R] W) :

          Converts a LinearEquiv to an isomorphism in the category FGModuleCat R.

          Equations
          • e.toFGModuleCatIso = { hom := e, inv := e.symm, hom_inv_id := , inv_hom_id := }
          Instances For
            @[simp]
            theorem FGModuleCat.tensorUnit_obj (R : Type u) [CommRing R] :
            (𝟙_ (FGModuleCat R)).obj = 𝟙_ (ModuleCat R)
            theorem FGModuleCat.Iso.conj_eq_conj (R : Type u) [CommRing R] {V : FGModuleCat R} {W : FGModuleCat R} (i : V W) (f : CategoryTheory.End V) :
            i.conj f = (FGModuleCat.isoToLinearEquiv i).conj f
            instance FGModuleCat.instFiniteHom (K : Type u) [Field K] (V : FGModuleCat K) (W : FGModuleCat K) :
            Equations
            • =
            @[simp]
            theorem FGModuleCat.ihom_obj (K : Type u) [Field K] (V : FGModuleCat K) (W : FGModuleCat K) :
            (CategoryTheory.ihom V).obj W = FGModuleCat.of K (V →ₗ[K] W)

            The dual module is the dual in the rigid monoidal category FGModuleCat K.

            Equations
            Instances For

              The evaluation morphism is given by the contraction map.

              Equations
              Instances For
                @[simp]
                Equations
                • One or more equations did not get rendered due to their size.

                @[simp] lemmas for LinearMap.comp and categorical identities.

                @[simp]
                theorem LinearMap.comp_id_fgModuleCat {R : Type u} [Ring R] {G : FGModuleCat R} {H : Type u} [AddCommGroup H] [Module R H] (f : G →ₗ[R] H) :
                @[simp]
                theorem LinearMap.id_fgModuleCat_comp {R : Type u} [Ring R] {G : Type u} [AddCommGroup G] [Module R G] {H : FGModuleCat R} (f : G →ₗ[R] H) :