The left unitor of a bifunctor on complexes

Let F : C ⥤ D ⥤ D be a bifunctor and X an object of C with e : F.obj X ≅ 𝟭 D. Then the complex X[0] acts as the identity through the totalized bifunctor: for every complex shape c with tensor signs (ComplexShape.TensorSigns) and every complex K, there is an isomorphism mapBifunctor X[0] K F c ≅ K, natural in K.

Main definitions

• CategoryTheory.Functor.mapBifunctorLeftUnitor: the isomorphism mapBifunctor X[0] K F c ≅ K attached to e : F.obj X ≅ 𝟭 D.

This adapts Mathlib's CategoryTheory.GradedObject.mapBifunctorLeftUnitor and the left unitor HomologicalComplex.leftUnitor of the monoidal structure on homological complexes, both due to Joël Riou, from tensor products to arbitrary bifunctors on complexes.

noncomputable def CategoryTheory.Functor.mapBifunctorLeftUnitor {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] [Preadditive D] (F : Functor C (Functor D D)) [F.PreservesZeroMorphisms] [∀ (X : C), (F.obj X).PreservesZeroMorphisms] (X : C) (e : F.obj X ≅ Functor.id D) {I : Type u_1} [AddMonoid I] [DecidableEq I] {c : ComplexShape I} [c.TensorSigns] (K : HomologicalComplex D c) [((HomologicalComplex.single C c 0).obj X).HasMapBifunctor K F c] : ((HomologicalComplex.single C c 0).obj X).mapBifunctor K F c ≅ K

The left unitor mapBifunctor X[0] K F c ≅ K attached to an isomorphism e : F.obj X ≅ 𝟭 D.

@[simp]

theorem CategoryTheory.Functor.ι_mapBifunctorLeftUnitor_hom_f {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] [Preadditive D] (F : Functor C (Functor D D)) [F.PreservesZeroMorphisms] [∀ (X : C), (F.obj X).PreservesZeroMorphisms] (X : C) (e : F.obj X ≅ Functor.id D) {I : Type u_1} [AddMonoid I] [DecidableEq I] {c : ComplexShape I} [c.TensorSigns] (K : HomologicalComplex D c) [((HomologicalComplex.single C c 0).obj X).HasMapBifunctor K F c] (j : I) : CategoryStruct.comp (((HomologicalComplex.single C c 0).obj X).ιMapBifunctor K F c 0 j j ⋯) ((F.mapBifunctorLeftUnitor X e K).hom.f j) = CategoryStruct.comp ((F.map (HomologicalComplex.singleObjXSelf c 0 X).hom).app (K.X j)) (e.hom.app (K.X j))

@[simp]

theorem CategoryTheory.Functor.ι_mapBifunctorLeftUnitor_hom_f_assoc {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] [Preadditive D] (F : Functor C (Functor D D)) [F.PreservesZeroMorphisms] [∀ (X : C), (F.obj X).PreservesZeroMorphisms] (X : C) (e : F.obj X ≅ Functor.id D) {I : Type u_1} [AddMonoid I] [DecidableEq I] {c : ComplexShape I} [c.TensorSigns] (K : HomologicalComplex D c) [((HomologicalComplex.single C c 0).obj X).HasMapBifunctor K F c] (j : I) {Z : D} (h : K.X j ⟶ Z) : CategoryStruct.comp (((HomologicalComplex.single C c 0).obj X).ιMapBifunctor K F c 0 j j ⋯) (CategoryStruct.comp ((F.mapBifunctorLeftUnitor X e K).hom.f j) h) = CategoryStruct.comp ((F.map (HomologicalComplex.singleObjXSelf c 0 X).hom).app (K.X j)) (CategoryStruct.comp (e.hom.app (K.X j)) h)

@[simp]

theorem CategoryTheory.Functor.mapBifunctorLeftUnitor_inv_f {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] [Preadditive D] (F : Functor C (Functor D D)) [F.PreservesZeroMorphisms] [∀ (X : C), (F.obj X).PreservesZeroMorphisms] (X : C) (e : F.obj X ≅ Functor.id D) {I : Type u_1} [AddMonoid I] [DecidableEq I] {c : ComplexShape I} [c.TensorSigns] (K : HomologicalComplex D c) [((HomologicalComplex.single C c 0).obj X).HasMapBifunctor K F c] (j : I) : (F.mapBifunctorLeftUnitor X e K).inv.f j = CategoryStruct.comp (e.inv.app (K.X j)) (CategoryStruct.comp ((F.map (HomologicalComplex.singleObjXSelf c 0 X).inv).app (K.X j)) (((HomologicalComplex.single C c 0).obj X).ιMapBifunctor K F c 0 j j ⋯))

theorem CategoryTheory.Functor.mapBifunctorLeftUnitor_inv_f_assoc {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] [Preadditive D] (F : Functor C (Functor D D)) [F.PreservesZeroMorphisms] [∀ (X : C), (F.obj X).PreservesZeroMorphisms] (X : C) (e : F.obj X ≅ Functor.id D) {I : Type u_1} [AddMonoid I] [DecidableEq I] {c : ComplexShape I} [c.TensorSigns] (K : HomologicalComplex D c) [((HomologicalComplex.single C c 0).obj X).HasMapBifunctor K F c] (j : I) {Z : D} (h : (((HomologicalComplex.single C c 0).obj X).mapBifunctor K F c).X j ⟶ Z) : CategoryStruct.comp ((F.mapBifunctorLeftUnitor X e K).inv.f j) h = CategoryStruct.comp (e.inv.app (K.X j)) (CategoryStruct.comp ((F.map (HomologicalComplex.singleObjXSelf c 0 X).inv).app (K.X j)) (CategoryStruct.comp (((HomologicalComplex.single C c 0).obj X).ιMapBifunctor K F c 0 j j ⋯) h))

theorem CategoryTheory.Functor.mapBifunctorLeftUnitor_inv_naturality {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] [Preadditive D] (F : Functor C (Functor D D)) [F.PreservesZeroMorphisms] [∀ (X : C), (F.obj X).PreservesZeroMorphisms] (X : C) (e : F.obj X ≅ Functor.id D) {I : Type u_1} [AddMonoid I] [DecidableEq I] {c : ComplexShape I} [c.TensorSigns] {K L : HomologicalComplex D c} (f : K ⟶ L) [((HomologicalComplex.single C c 0).obj X).HasMapBifunctor K F c] [((HomologicalComplex.single C c 0).obj X).HasMapBifunctor L F c] : CategoryStruct.comp f (F.mapBifunctorLeftUnitor X e L).inv = CategoryStruct.comp (F.mapBifunctorLeftUnitor X e K).inv (HomologicalComplex.mapBifunctorMap (CategoryStruct.id ((HomologicalComplex.single C c 0).obj X)) f F c)

theorem CategoryTheory.Functor.mapBifunctorLeftUnitor_inv_naturality_assoc {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] [Preadditive D] (F : Functor C (Functor D D)) [F.PreservesZeroMorphisms] [∀ (X : C), (F.obj X).PreservesZeroMorphisms] (X : C) (e : F.obj X ≅ Functor.id D) {I : Type u_1} [AddMonoid I] [DecidableEq I] {c : ComplexShape I} [c.TensorSigns] {K L : HomologicalComplex D c} (f : K ⟶ L) [((HomologicalComplex.single C c 0).obj X).HasMapBifunctor K F c] [((HomologicalComplex.single C c 0).obj X).HasMapBifunctor L F c] {Z : HomologicalComplex D c} (h : ((HomologicalComplex.single C c 0).obj X).mapBifunctor L F c ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (F.mapBifunctorLeftUnitor X e L).inv h) = CategoryStruct.comp (F.mapBifunctorLeftUnitor X e K).inv (CategoryStruct.comp (HomologicalComplex.mapBifunctorMap (CategoryStruct.id ((HomologicalComplex.single C c 0).obj X)) f F c) h)

theorem CategoryTheory.Functor.mapBifunctorLeftUnitor_naturality {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] [Preadditive D] (F : Functor C (Functor D D)) [F.PreservesZeroMorphisms] [∀ (X : C), (F.obj X).PreservesZeroMorphisms] (X : C) (e : F.obj X ≅ Functor.id D) {I : Type u_1} [AddMonoid I] [DecidableEq I] {c : ComplexShape I} [c.TensorSigns] {K L : HomologicalComplex D c} (f : K ⟶ L) [((HomologicalComplex.single C c 0).obj X).HasMapBifunctor K F c] [((HomologicalComplex.single C c 0).obj X).HasMapBifunctor L F c] : CategoryStruct.comp (HomologicalComplex.mapBifunctorMap (CategoryStruct.id ((HomologicalComplex.single C c 0).obj X)) f F c) (F.mapBifunctorLeftUnitor X e L).hom = CategoryStruct.comp (F.mapBifunctorLeftUnitor X e K).hom f

theorem CategoryTheory.Functor.mapBifunctorLeftUnitor_naturality_assoc {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] [Preadditive D] (F : Functor C (Functor D D)) [F.PreservesZeroMorphisms] [∀ (X : C), (F.obj X).PreservesZeroMorphisms] (X : C) (e : F.obj X ≅ Functor.id D) {I : Type u_1} [AddMonoid I] [DecidableEq I] {c : ComplexShape I} [c.TensorSigns] {K L : HomologicalComplex D c} (f : K ⟶ L) [((HomologicalComplex.single C c 0).obj X).HasMapBifunctor K F c] [((HomologicalComplex.single C c 0).obj X).HasMapBifunctor L F c] {Z : HomologicalComplex D c} (h : L ⟶ Z) : CategoryStruct.comp (HomologicalComplex.mapBifunctorMap (CategoryStruct.id ((HomologicalComplex.single C c 0).obj X)) f F c) (CategoryStruct.comp (F.mapBifunctorLeftUnitor X e L).hom h) = CategoryStruct.comp (F.mapBifunctorLeftUnitor X e K).hom (CategoryStruct.comp f h)