The free–forgetful adjunction for module objects

The free module freeMod A X on an object X of a monoidal category D carries A ⊗ X with the action obtained by multiplying on the left factor. Maps of A-modules out of it are the same thing as maps out of X in D: the bijection sends a module map to its restriction along the unit (λ_ X).inv ≫ η[A] ▷ X and a bare map g to its extension A ◁ g ≫ actLeft A M.X.

• freeModHomEquiv: the bijection, with both round trips.
• freeModHom_eq_zero_iff: a map out of a free module vanishes exactly when its restriction along the unit does. This is the additive shadow of the adjunction, available even though the hom-sets of Mod D A carry no additive structure here.
• hom_eq_zero_of_generators: a module map out of N vanishes as soon as it is killed by a family of free modules whose retracts sum to the identity of N.
• freeModAdjunction: the bijection bundled as an adjunction between freeModFunctor A and Mod.forget A.

All the intermediate statements are phrased in the ambient language of A ⊗ X and a bare action morphism, and are transported into the category of module objects by definitional unfolding.

theorem RS.freeMod_unit_mul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X))) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj A X)

The unit of the free module is cancelled by the free action.

theorem RS.unit_whiskerLeft_act {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) (act : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ Y) (hone : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one Y) act = (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) (g : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g) act)) = g

Restricting an extended map along the unit recovers the map.

theorem RS.whiskerLeft_unit_cancel {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) (act : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ Y) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj A X ⟶ Y) (hlin : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A h) act) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) h))) act = h

Extending the restriction of a module map along the unit recovers the module map.

theorem RS.whiskerLeft_act_lin {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) (act : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ Y) (hassoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A act) act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul Y) act)) (g : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g) act) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g) act)) act

The extension of a map along the free module intertwines the free action with the given action.

theorem RS.freeModHom_lin {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) (M : CategoryTheory.Mod D A) (f : freeMod A X ⟶ M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X)) f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f.hom) (actLeft A M.X)

The module law of a map out of a free module, in tensor form.

noncomputable def RS.freeModHomEquiv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) (M : CategoryTheory.Mod D A) : (freeMod A X ⟶ M) ≃ (X ⟶ M.X)

The free–forgetful adjunction bijection for module objects: module maps out of the free module on X are maps out of X, by restriction along the unit.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.freeModHomEquiv_apply {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) (M : CategoryTheory.Mod D A) (f : freeMod A X ⟶ M) : (freeModHomEquiv A X M) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) f.hom)

@[simp]

theorem RS.freeModHomEquiv_symm_apply_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) (M : CategoryTheory.Mod D A) (g : X ⟶ M.X) : ((freeModHomEquiv A X M).symm g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g) (actLeft A M.X)

theorem RS.unit_eq_zero_iff {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (A : D) [CategoryTheory.MonObj A] (X Y : D) (act : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ Y) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj A X ⟶ Y) (hlin : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A h) act) : h = 0 ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) h) = 0

An equivariant map out of a free module vanishes exactly when its restriction along the unit does.

theorem RS.freeModHom_eq_zero_iff {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (A : D) [CategoryTheory.MonObj A] (X : D) (M : CategoryTheory.Mod D A) (f : freeMod A X ⟶ M) : f.hom = 0 ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) f.hom) = 0

A map out of a free module vanishes exactly when its restriction along the unit does. This replaces the linearity of the adjunction bijection, which is unavailable because the hom-sets of Mod D A carry no additive structure.

theorem RS.hom_eq_zero_of_generators {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] (A : D) [CategoryTheory.MonObj A] {N M : CategoryTheory.Mod D A} {J : Type} [Fintype J] {f : J → D} (s : (i : J) → freeMod A (f i) ⟶ N) (r : (i : J) → N ⟶ freeMod A (f i)) (htot : ∑ i : J, CategoryTheory.CategoryStruct.comp (r i).hom (s i).hom = CategoryTheory.CategoryStruct.id N.X) (g : N ⟶ M) (hg : ∀ (i : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (f i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (f i)) (CategoryTheory.CategoryStruct.comp (s i).hom g.hom)) = 0) : g.hom = 0

Generation by a finite family of free modules: a module map out of N vanishes as soon as its restrictions along the units of a family of free modules whose retracts sum to the identity of N all vanish.

theorem RS.unit_comp_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y Z : D) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj A X ⟶ Y) (k : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) (CategoryTheory.CategoryStruct.comp h k)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X) h)) k

Restriction along the unit is compatible with postcomposition in the target.

noncomputable def RS.freeModAdjunction {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] : freeModFunctor A ⊣ CategoryTheory.Mod.forget A

The free–forgetful adjunction for module objects.

Equations

• One or more equations did not get rendered due to their size.