Documentation

TauCeti.CategoryTheory.Monoidal.Mod.Free.Basic

Free modules over an internal monoid #

For a monoid object A in a monoidal category, A ⊗ X is the free left A-module on X. Restriction to the generators identifies module maps out of it with maps out of X, naturally in both variables. No braiding or colimit hypotheses are needed.

The construction uses Mathlib's Mod category. It supplies, in particular, the free sphere modules used to construct free symmetric spectra.

source
@[instance_reducible]
def TauCeti.freeModObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] (X : C) :
CategoryTheory.ModObj A (CategoryTheory.MonoidalCategoryStruct.tensorObj A X)

Multiplication on the first factor makes A ⊗ X a left A-module.

Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.freeMod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] :
    CategoryTheory.Functor C (CategoryTheory.Mod C A)

    The free left A-module functor. Its underlying object on X is A ⊗ X.

    Instances For
      source
      @[simp]
      theorem TauCeti.freeMod_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] (X : C) :
      CategoryTheory.ModObj.smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X)

      The free-module action is multiplication on its first tensor factor.

      source
      def TauCeti.freeModι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] (X : C) :
      X ⟶ ((freeMod A).obj X).X

      The generators of a free module are obtained by inserting the monoid unit.

      Instances For
        source
        theorem TauCeti.freeModι_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] (X : C) :
        freeModι A X = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one X)

        The inclusion of generators inserts the unit in the first tensor factor.

        source
        def TauCeti.freeModDesc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] {X : C} (M : CategoryTheory.Mod C A) (f : X ⟶ M.X) :
        (freeMod A).obj X ⟶ M

        Extending a map to a module by the module action.

        Instances For
          source
          @[simp]
          theorem TauCeti.freeModDesc_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] {X : C} (M : CategoryTheory.Mod C A) (f : X ⟶ M.X) :
          (freeModDesc A M f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) CategoryTheory.ModObj.smul

          The extension's underlying map applies the given map and then the action.

          source
          @[simp]
          theorem TauCeti.freeModι_desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] {X : C} (M : CategoryTheory.Mod C A) (f : X ⟶ M.X) :
          CategoryTheory.CategoryStruct.comp (freeModι A X) (freeModDesc A M f).hom = f

          An extension agrees with the given map on generators.

          source
          @[simp]
          theorem TauCeti.freeModι_desc_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] {X : C} (M : CategoryTheory.Mod C A) (f : X ⟶ M.X) {Z : C} (h : M.X ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (freeModι A X) (CategoryTheory.CategoryStruct.comp (freeModDesc A M f).hom h) = CategoryTheory.CategoryStruct.comp f h

          An extension agrees with the given map on generators.

          source
          @[simp]
          theorem TauCeti.freeModDesc_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] {X : C} (M : CategoryTheory.Mod C A) (f : (freeMod A).obj X ⟶ M) :
          freeModDesc A M (CategoryTheory.CategoryStruct.comp (freeModι A X) f.hom) = f

          Restriction followed by extension recovers every free-module map.

          source
          def TauCeti.freeModHomEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] (X : C) (M : CategoryTheory.Mod C A) :
          ((freeMod A).obj X ⟶ M) ≃ (X ⟶ M.X)

          The universal property of a free module.

          Instances For
            source
            @[simp]
            theorem TauCeti.freeModHomEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] (X : C) (M : CategoryTheory.Mod C A) (f : (freeMod A).obj X ⟶ M) :
            (freeModHomEquiv A X M) f = CategoryTheory.CategoryStruct.comp (freeModι A X) f.hom

            The universal bijection restricts a module map to the generators.

            source
            @[simp]
            theorem TauCeti.freeModHomEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] (X : C) (M : CategoryTheory.Mod C A) (f : X ⟶ M.X) :
            (freeModHomEquiv A X M).symm f = freeModDesc A M f

            The inverse universal bijection extends by the action.

            source
            theorem TauCeti.freeMod_hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] {X : C} {M : CategoryTheory.Mod C A} {f g : (freeMod A).obj X ⟶ M} (h : CategoryTheory.CategoryStruct.comp (freeModι A X) f.hom = CategoryTheory.CategoryStruct.comp (freeModι A X) g.hom) :
            f = g

            Maps out of a free module are determined by their restrictions to generators.

            source
            theorem TauCeti.freeMod_hom_ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A : C} [CategoryTheory.MonObj A] {X : C} {M : CategoryTheory.Mod C A} {f g : (freeMod A).obj X ⟶ M} :
            f = g ↔ CategoryTheory.CategoryStruct.comp (freeModι A X) f.hom = CategoryTheory.CategoryStruct.comp (freeModι A X) g.hom
            source
            def TauCeti.freeModAdjunction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] :
            freeMod A ⊣ CategoryTheory.Mod.forget A

            The free-module functor is left adjoint to the native forgetful functor.

            Instances For
              source
              @[simp]
              theorem TauCeti.freeModAdjunction_homEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] (X : C) (M : CategoryTheory.Mod C A) :
              (freeModAdjunction A).homEquiv X M = freeModHomEquiv A X M

              The adjunction uses restriction to the chosen generators as its hom-set bijection.

              source
              @[simp]
              theorem TauCeti.freeModAdjunction_unit_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] (X : C) :
              (freeModAdjunction A).unit.app X = freeModι A X

              The adjunction unit is the inclusion of generators.

              source
              @[simp]
              theorem TauCeti.freeModAdjunction_counit_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] (M : CategoryTheory.Mod C A) :
              (freeModAdjunction A).counit.app M = freeModDesc A M (CategoryTheory.CategoryStruct.id M.X)

              The adjunction counit extends the identity by the module action.

              source
              @[simp]
              theorem TauCeti.freeModι_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] {X Y : C} (f : X ⟶ Y) :
              CategoryTheory.CategoryStruct.comp f (freeModι A Y) = CategoryTheory.CategoryStruct.comp (freeModι A X) (CategoryTheory.Mod.Hom.mk' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) ⋯).hom

              Inclusion of generators is natural in the generating object.

              source
              @[simp]
              theorem TauCeti.freeModι_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] {X Y : C} (f : X ⟶ Y) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ Z) :
              CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (freeModι A Y) h) = CategoryTheory.CategoryStruct.comp (freeModι A X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Mod.Hom.mk' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) ⋯).hom h)

              Inclusion of generators is natural in the generating object.

              source
              @[simp]
              theorem TauCeti.freeModDesc_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] {X : C} {M N : CategoryTheory.Mod C A} (f : X ⟶ M.X) (g : M ⟶ N) :
              CategoryTheory.CategoryStruct.comp (freeModDesc A M f) g = freeModDesc A N (CategoryTheory.CategoryStruct.comp f g.hom)

              Extending a map commutes with post-composition by a module map.

              source
              theorem TauCeti.freeModDesc_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] {X : C} {M N : CategoryTheory.Mod C A} (f : X ⟶ M.X) (g : M ⟶ N) {Z : CategoryTheory.Mod C A} (h : N ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (freeModDesc A M f) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (freeModDesc A N (CategoryTheory.CategoryStruct.comp f g.hom)) h

              Extending a map commutes with post-composition by a module map.

              source
              @[simp]
              theorem TauCeti.freeMod_map_desc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] {X Y : C} (M : CategoryTheory.Mod C A) (f : X ⟶ Y) (g : Y ⟶ M.X) :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.Mod.Hom.mk' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) ⋯) (freeModDesc A M g) = freeModDesc A M (CategoryTheory.CategoryStruct.comp f g)

              Extending a map commutes with pre-composition on its generators.

              source
              theorem TauCeti.freeMod_map_desc_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] {X Y : C} (M : CategoryTheory.Mod C A) (f : X ⟶ Y) (g : Y ⟶ M.X) {Z : CategoryTheory.Mod C A} (h : M ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.Mod.Hom.mk' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) ⋯) (CategoryTheory.CategoryStruct.comp (freeModDesc A M g) h) = CategoryTheory.CategoryStruct.comp (freeModDesc A M (CategoryTheory.CategoryStruct.comp f g)) h

              Extending a map commutes with pre-composition on its generators.

              source
              @[simp]
              theorem TauCeti.freeModι_tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] (V K : C) :
              CategoryTheory.CategoryStruct.comp (freeModι A (CategoryTheory.MonoidalCategoryStruct.tensorObj V K)) (CategoryTheory.MonoidalCategoryStruct.associator A V K).inv = CategoryTheory.MonoidalCategoryStruct.whiskerRight (freeModι A V) K

              Inserting the free generators commutes with tensoring on the right.

              source
              @[simp]
              theorem TauCeti.freeModι_tensor_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.MonObj A] (V K : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj A V) K ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (freeModι A (CategoryTheory.MonoidalCategoryStruct.tensorObj V K)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A V K).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (freeModι A V) K) h

              Inserting the free generators commutes with tensoring on the right.