Dinatural transformations

Dinatural transformations are special kinds of transformations between functors F G : Cᵒᵖ ⥤ C ⥤ D which depend both covariantly and contravariantly on the same category (also known as difunctors).

A dinatural transformation is a family of morphisms given only on the diagonal of the two functors, and is such that a certain naturality hexagon commutes. Note that dinatural transformations cannot be composed with each other (since the outer hexagon does not commute in general), but can still be "pre/post-composed" with ordinary natural transformations.

References

• https://ncatlab.org/nlab/show/dinatural+transformation

structure CategoryTheory.DinatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F G : Functor Cᵒᵖ (Functor C D)) : Type (max u₁ v₂)

Dinatural transformations between two difunctors.

• app (X : C) : (F.obj (Opposite.op X)).obj X ⟶ (G.obj (Opposite.op X)).obj X

  The component of a natural transformation.

• dinaturality {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp ((F.map f.op).app X) (CategoryStruct.comp (self.app X) ((G.obj (Opposite.op X)).map f)) = CategoryStruct.comp ((F.obj (Opposite.op Y)).map f) (CategoryStruct.comp (self.app Y) ((G.map f.op).app Y))

  The commutativity square for a given morphism.

@[simp]

theorem CategoryTheory.DinatTrans.dinaturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor Cᵒᵖ (Functor C D)} (self : DinatTrans F G) {X Y : C} (f : X ⟶ Y) {Z : D} (h : (G.obj (Opposite.op X)).obj Y ⟶ Z) : CategoryStruct.comp ((F.map f.op).app X) (CategoryStruct.comp (self.app X) (CategoryStruct.comp ((G.obj (Opposite.op X)).map f) h)) = CategoryStruct.comp ((F.obj (Opposite.op Y)).map f) (CategoryStruct.comp (self.app Y) (CategoryStruct.comp ((G.map f.op).app Y) h))

def CategoryTheory.DinatTrans.«term_⤞_» : Lean.TrailingParserDescr

Notation for dinatural transformations.

Equations

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

def CategoryTheory.DinatTrans.compNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor Cᵒᵖ (Functor C D)} (δ : DinatTrans F G) (α : G ⟶ H) : DinatTrans F H

Post-composition with a natural transformation.

Equations

• δ.compNatTrans α = { app := fun (X : C) => CategoryTheory.CategoryStruct.comp (δ.app X) ((α.app (Opposite.op X)).app X), dinaturality := ⋯ }

@[simp]

theorem CategoryTheory.DinatTrans.compNatTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor Cᵒᵖ (Functor C D)} (δ : DinatTrans F G) (α : G ⟶ H) (X : C) : (δ.compNatTrans α).app X = CategoryStruct.comp (δ.app X) ((α.app (Opposite.op X)).app X)

def CategoryTheory.DinatTrans.precompNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor Cᵒᵖ (Functor C D)} (δ : DinatTrans G H) (α : F ⟶ G) : DinatTrans F H

Pre-composition with a natural transformation.

Equations

• δ.precompNatTrans α = { app := fun (X : C) => CategoryTheory.CategoryStruct.comp ((α.app (Opposite.op X)).app X) (δ.app X), dinaturality := ⋯ }

@[simp]

theorem CategoryTheory.DinatTrans.precompNatTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor Cᵒᵖ (Functor C D)} (δ : DinatTrans G H) (α : F ⟶ G) (X : C) : (δ.precompNatTrans α).app X = CategoryStruct.comp ((α.app (Opposite.op X)).app X) (δ.app X)