The free-module functor, and the factorisation of ω

Base change to an algebra is a functor to the module objects over that algebra, and Deligne's ω of 2.11 is that functor followed by realization. Recording the factorisation lets the two halves be treated separately: the free-module functor carries the monoidal comparison of the ambient category, and realization carries the comparison of (2.11.1).

theorem RS.freeModMap_id {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) : freeModMap A (CategoryTheory.CategoryStruct.id V) = CategoryTheory.CategoryStruct.id (freeMod A V)

Base change of a morphism is the identity on the identity.

theorem RS.freeModMap_comp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {V W X : D} (f : V ⟶ W) (g : W ⟶ X) : freeModMap A (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (freeModMap A f) (freeModMap A g)

Base change of a morphism respects composition.

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

Base change to an algebra, as a functor.

Equations

• RS.freeModFunctor A = { obj := fun (V : D) => RS.freeMod A V, map := fun {X Y : D} (f : X ⟶ Y) => RS.freeModMap A f, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem RS.freeModFunctor_obj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (V : D) : (freeModFunctor A).obj V = freeMod A V

@[simp]

theorem RS.freeModFunctor_map {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] {V W : D} (f : V ⟶ W) : (freeModFunctor A).map f = freeModMap A f