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
      Equations
      • instConcreteCategoryFGModuleCat = id inferInstance
      Equations
      • instPreadditiveFGModuleCat = id inferInstance
      instance FGModuleCat.finite (R : Type u) [Ring R] (V : FGModuleCat R) :
      Equations
      @[reducible, inline]
      abbrev 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
        @[reducible, inline]
        abbrev FGModuleCat.ofHom {R : Type u} [Ring R] {V W : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] [AddCommGroup W] [Module R W] [Module.Finite R W] (f : V →ₗ[R] W) :

        Lift a linear map between finitely generated modules to FGModuleCat R.

        Equations
        Instances For
          theorem FGModuleCat.hom_ext {R : Type u} [Ring R] {V W : FGModuleCat R} {f g : V W} (h : f.hom = g.hom) :
          f = g
          def FGModuleCat.isoToLinearEquiv {R : Type u} [Ring R] {V 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

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

            Equations
            Instances For
              @[simp]
              theorem LinearEquiv.toFGModuleCatIso_hom_hom {R : Type u} [Ring R] {V 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.hom = e
              @[simp]
              theorem LinearEquiv.toFGModuleCatIso_inv_hom {R : Type u} [Ring R] {V 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.hom = e.symm
              @[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 W : FGModuleCat R} (i : V W) (f : CategoryTheory.End V) :
              theorem FGModuleCat.Iso.conj_hom_eq_conj (R : Type u) [CommRing R] {V W : FGModuleCat R} (i : V W) (f : CategoryTheory.End V) :
              (i.conj f).hom = (FGModuleCat.isoToLinearEquiv i).conj f.hom
              instance FGModuleCat.instFiniteHom (K : Type u) [Field K] (V W : FGModuleCat K) :
              @[simp]
              theorem FGModuleCat.ihom_obj (K : Type u) [Field K] (V W : FGModuleCat K) :

              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]
                  theorem FGModuleCat.FGModuleCatEvaluation_apply' (K : Type u) [Field K] (V : FGModuleCat K) (f : (FGModuleCat.FGModuleCatDual K V)) (x : V) :
                  (FGModuleCat.FGModuleCatEvaluation K V).hom (f ⊗ₜ[K] x) = f.toFun x

                  @[simp]-normal form of FGModuleCatEvaluation_apply, where the carriers have been unfolded.

                  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) :