Equivariant natural transformations as modifications

Let a monoid M act on categories C and D, and let F₁ F₂ : C ⥤ D be equivariant functors (left-linear for the actions of Discrete M). They correspond to the strong transformations strongTrans M F₁ and strongTrans M F₂ between the pseudofunctors pseudofunctor M C and pseudofunctor M D. This file shows that the equivariant natural transformations F₁ ⟶ F₂ (those satisfying NatTrans.IsLeftLinear) are exactly the modifications between these strong transformations.

• MonoidalLeftAction.modification M τ is the modification whose component at the unique object is τ. Its naturality condition at g is the commutation of τ with the oplax lineators δₗ F₁ ⟨g⟩ and δₗ F₂ ⟨g⟩.
• Conversely MonoidalLeftAction.natTransOfModification Γ is the component of a modification Γ at the unique object; it is equivariant.
• MonoidalLeftAction.modificationEquiv M F₁ F₂ packages these as an equivalence between the equivariant natural transformations F₁ ⟶ F₂ and the modifications. It sends identities to identities and vertical composites to vertical composites.
• MonoidalLeftAction.strongTransIso M e is the invertible modification attached to a natural isomorphism e : F₁ ≅ F₂ with equivariant forward map.
• MonoidalLeftAction.strongTransIdIso M and MonoidalLeftAction.strongTransCompIso M F G compare the strong transformations of the identity functor and of a composite F ⋙ G, with the left-linear structures of Functor.LeftLinear.id and Functor.LeftLinear.comp, with the identity strong transformation and with the vertical composite strongTrans M F ≫ strongTrans M G. Both are invertible modifications with identity components.

Since every strong transformation pseudofunctor M C ⟶ pseudofunctor M D is definitionally strongTrans M (functorOfStrongTrans η), these statements describe the modifications between arbitrary such strong transformations.

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.modification (M : Type u) [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] (τ : F₁ ⟶ F₂) [NatTrans.IsLeftLinear τ (Discrete M)] : (strongTrans M F₁).Modification (strongTrans M F₂)

An equivariant natural transformation τ : F₁ ⟶ F₂ between equivariant functors is a modification strongTrans M F₁ ⟶ strongTrans M F₂ with component τ at the unique object. Its naturality condition at g is τ.app (g ⊙ₗ X) ≫ δₗ F₂ g X = δₗ F₁ g X ≫ g ⊴ₗ τ.app X.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.modification_app_toNatTrans (M : Type u) [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] (τ : F₁ ⟶ F₂) [NatTrans.IsLeftLinear τ (Discrete M)] (a : LocallyDiscrete (SingleObj M)) : ((modification M τ).app a).toNatTrans = τ

The component of modification M τ at every object is τ.

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.natTransOfModification {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] (Γ : (strongTrans M F₁).Modification (strongTrans M F₂)) : F₁ ⟶ F₂

The natural transformation F₁ ⟶ F₂ underlying a modification Γ : strongTrans M F₁ ⟶ strongTrans M F₂: its component at the unique object.

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.natTransOfModification_app {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] (Γ : (strongTrans M F₁).Modification (strongTrans M F₂)) (X : C) : (natTransOfModification Γ).app X = (Γ.app { as := SingleObj.star M }).toNatTrans.app X

The components of the natural transformation underlying a modification.

instance CategoryTheory.MonoidalCategory.MonoidalLeftAction.isLeftLinear_natTransOfModification {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] (Γ : (strongTrans M F₁).Modification (strongTrans M F₂)) : NatTrans.IsLeftLinear (natTransOfModification Γ) (Discrete M)

The natural transformation underlying a modification between the strong transformations of equivariant functors is equivariant: the naturality condition of the modification at g is the commutation with the oplax lineators δₗ F₁ ⟨g⟩ and δₗ F₂ ⟨g⟩.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.natTransOfModification_modification {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] (τ : F₁ ⟶ F₂) [NatTrans.IsLeftLinear τ (Discrete M)] : natTransOfModification (modification M τ) = τ

The natural transformation underlying modification M τ is τ.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.modification_natTransOfModification {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] (Γ : (strongTrans M F₁).Modification (strongTrans M F₂)) : modification M (natTransOfModification Γ) = Γ

Every modification strongTrans M F₁ ⟶ strongTrans M F₂ is the modification of its underlying natural transformation.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.modification_id (M : Type u) [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (F₁ : Functor C D) [F₁.LeftLinear (Discrete M)] : modification M (CategoryStruct.id F₁) = Pseudofunctor.StrongTrans.Modification.id (strongTrans M F₁)

The modification attached to the identity natural transformation is the identity modification.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.modification_comp (M : Type u) [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ F₃ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] [F₃.LeftLinear (Discrete M)] (τ : F₁ ⟶ F₂) (τ' : F₂ ⟶ F₃) [NatTrans.IsLeftLinear τ (Discrete M)] [NatTrans.IsLeftLinear τ' (Discrete M)] : modification M (CategoryStruct.comp τ τ') = (modification M τ).vcomp (modification M τ')

The modification attached to a vertical composite of equivariant natural transformations is the vertical composite of the modifications.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.natTransOfModification_id {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ : Functor C D} [F₁.LeftLinear (Discrete M)] : natTransOfModification (Pseudofunctor.StrongTrans.Modification.id (strongTrans M F₁)) = CategoryStruct.id F₁

The natural transformation underlying the identity modification is the identity.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.natTransOfModification_vcomp {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ F₃ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] [F₃.LeftLinear (Discrete M)] (Γ : (strongTrans M F₁).Modification (strongTrans M F₂)) (Δ : (strongTrans M F₂).Modification (strongTrans M F₃)) : natTransOfModification (Γ.vcomp Δ) = CategoryStruct.comp (natTransOfModification Γ) (natTransOfModification Δ)

The natural transformation underlying a vertical composite of modifications is the composite of the underlying natural transformations.

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.modificationEquiv (M : Type u) [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] (F₁ F₂ : Functor C D) [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] : { τ : F₁ ⟶ F₂ // NatTrans.IsLeftLinear τ (Discrete M) } ≃ (strongTrans M F₁).Modification (strongTrans M F₂)

Equivariant natural transformations F₁ ⟶ F₂ correspond to modifications strongTrans M F₁ ⟶ strongTrans M F₂.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.modificationEquiv_apply {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] (τ : { τ : F₁ ⟶ F₂ // NatTrans.IsLeftLinear τ (Discrete M) }) : (modificationEquiv M F₁ F₂) τ = modification M ↑τ

modificationEquiv sends an equivariant natural transformation to its modification.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.modificationEquiv_symm_apply_coe {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] (Γ : (strongTrans M F₁).Modification (strongTrans M F₂)) : ↑((modificationEquiv M F₁ F₂).symm Γ) = natTransOfModification Γ

The inverse of modificationEquiv sends a modification to its underlying natural transformation.

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransIso (M : Type u) [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] (e : F₁ ≅ F₂) [NatTrans.IsLeftLinear e.hom (Discrete M)] : strongTrans M F₁ ≅ strongTrans M F₂

A natural isomorphism e : F₁ ≅ F₂ between equivariant functors whose forward map is equivariant gives an invertible modification strongTrans M F₁ ≅ strongTrans M F₂, with components e.hom and e.inv at the unique object.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransIso_hom_as {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] (e : F₁ ≅ F₂) [NatTrans.IsLeftLinear e.hom (Discrete M)] : (strongTransIso M e).hom.as = modification M e.hom

The forward modification of strongTransIso M e is the modification of e.hom.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransIso_inv_as {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {F₁ F₂ : Functor C D} [F₁.LeftLinear (Discrete M)] [F₂.LeftLinear (Discrete M)] (e : F₁ ≅ F₂) [NatTrans.IsLeftLinear e.hom (Discrete M)] : (strongTransIso M e).inv.as = modification M e.inv

The inverse modification of strongTransIso M e is the modification of e.inv.

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransIdIso (M : Type u) [Monoid M] {C : Type w} [Category.{v, w} C] [MonoidalLeftAction (Discrete M) C] : strongTrans M (Functor.id C) ≅ CategoryStruct.id (pseudofunctor M C)

The strong transformation attached to the identity functor, with its identity lineators, is isomorphic to the identity strong transformation of pseudofunctor M C, through the invertible modification whose component at the unique object is the identity.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransIdIso_hom_as_app_toNatTrans {M : Type u} [Monoid M] {C : Type w} [Category.{v, w} C] [MonoidalLeftAction (Discrete M) C] (a : LocallyDiscrete (SingleObj M)) : ((strongTransIdIso M).hom.as.app a).toNatTrans = CategoryStruct.id (Functor.id C)

The components of the forward modification of strongTransIdIso M are identities.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransIdIso_inv_as_app_toNatTrans {M : Type u} [Monoid M] {C : Type w} [Category.{v, w} C] [MonoidalLeftAction (Discrete M) C] (a : LocallyDiscrete (SingleObj M)) : ((strongTransIdIso M).inv.as.app a).toNatTrans = CategoryStruct.id (Functor.id C)

The components of the inverse modification of strongTransIdIso M are identities.

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransCompIso (M : Type u) [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {E : Type w} [Category.{v, w} E] [MonoidalLeftAction (Discrete M) E] (F : Functor C D) (G : Functor D E) [F.LeftLinear (Discrete M)] [G.LeftLinear (Discrete M)] : strongTrans M (F.comp G) ≅ CategoryStruct.comp (strongTrans M F) (strongTrans M G)

The strong transformation attached to a composite F ⋙ G of equivariant functors, with the lineators of Functor.LeftLinear.comp, is isomorphic to the vertical composite of the strong transformations of F and G, through the invertible modification whose component at the unique object is the identity.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransCompIso_hom_as_app_toNatTrans {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {E : Type w} [Category.{v, w} E] [MonoidalLeftAction (Discrete M) E] (F : Functor C D) (G : Functor D E) [F.LeftLinear (Discrete M)] [G.LeftLinear (Discrete M)] (a : LocallyDiscrete (SingleObj M)) : ((strongTransCompIso M F G).hom.as.app a).toNatTrans = CategoryStruct.id (F.comp G)

The components of the forward modification of strongTransCompIso M F G are identities.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.strongTransCompIso_inv_as_app_toNatTrans {M : Type u} [Monoid M] {C D : Type w} [Category.{v, w} C] [Category.{v, w} D] [MonoidalLeftAction (Discrete M) C] [MonoidalLeftAction (Discrete M) D] {E : Type w} [Category.{v, w} E] [MonoidalLeftAction (Discrete M) E] (F : Functor C D) (G : Functor D E) [F.LeftLinear (Discrete M)] [G.LeftLinear (Discrete M)] (a : LocallyDiscrete (SingleObj M)) : ((strongTransCompIso M F G).inv.as.app a).toNatTrans = CategoryStruct.id (F.comp G)

The components of the inverse modification of strongTransCompIso M F G are identities.