Natural transformations at the monoidal unit

The monoidal unit gives graded natural transformations with ordinary components. This module relates their graded naturality to naturality after forgetting enrichment, and provides identity and composition for these transformations.

@[reducible, inline]

abbrev TauCeti.UnitGradedNatTrans {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C' : Type u₁} {D' : Type u₂} [CategoryTheory.EnrichedCategory V C'] [CategoryTheory.EnrichedCategory V D'] (F G : CategoryTheory.EnrichedFunctor V C' D') : Type (max u₁ w)

Graded natural transformations whose degree is the monoidal unit.

Equations

• TauCeti.UnitGradedNatTrans F G = CategoryTheory.GradedNatTrans ((CategoryTheory.Center.ofBraided V).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)) F G

noncomputable def TauCeti.UnitGradedNatTrans.toOrdinary {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C' : Type u₁} {D' : Type u₂} [CategoryTheory.EnrichedCategory V C'] [CategoryTheory.EnrichedCategory V D'] {F G : CategoryTheory.EnrichedFunctor V C' D'} (α : UnitGradedNatTrans F G) : F.forget ⟶ G.forget

Forget enrichment of a graded natural transformation at the monoidal unit.

Equations

• α.toOrdinary = { app := fun (X : CategoryTheory.ForgetEnrichment V C') => α.app (CategoryTheory.ForgetEnrichment.to V X), naturality := ⋯ }

@[simp]

theorem TauCeti.UnitGradedNatTrans.toOrdinary_app {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C' : Type u₁} {D' : Type u₂} [CategoryTheory.EnrichedCategory V C'] [CategoryTheory.EnrichedCategory V D'] {F G : CategoryTheory.EnrichedFunctor V C' D'} (α : UnitGradedNatTrans F G) (X : C') : α.toOrdinary.app (CategoryTheory.ForgetEnrichment.of V X) = CategoryTheory.ForgetEnrichment.homOf V (α.app X)

Forgetting enrichment leaves the component of a unit-graded transformation unchanged.

theorem TauCeti.composeNaturalSquares {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {E : Type u₂} [CategoryTheory.Category.{u_1, u₂} E] [CategoryTheory.EnrichedOrdinaryCategory V E] {FX GX HX FY GY HY : E} {M : V} (fMap : M ⟶ FX ⟶[V] FY) (gMap : M ⟶ GX ⟶[V] GY) (hMap : M ⟶ HX ⟶[V] HY) (aX : FX ⟶ GX) (aY : FY ⟶ GY) (bX : GX ⟶ HX) (bY : GY ⟶ HY) (ha : CategoryTheory.CategoryStruct.comp fMap (CategoryTheory.eHomWhiskerLeft V FX aY) = CategoryTheory.CategoryStruct.comp gMap (CategoryTheory.eHomWhiskerRight V aX GY)) (hb : CategoryTheory.CategoryStruct.comp gMap (CategoryTheory.eHomWhiskerLeft V GX bY) = CategoryTheory.CategoryStruct.comp hMap (CategoryTheory.eHomWhiskerRight V bX HY)) : CategoryTheory.CategoryStruct.comp fMap (CategoryTheory.eHomWhiskerLeft V FX (CategoryTheory.CategoryStruct.comp aY bY)) = CategoryTheory.CategoryStruct.comp hMap (CategoryTheory.eHomWhiskerRight V (CategoryTheory.CategoryStruct.comp aX bX) HY)

Two enriched whiskering squares compose along their ordinary components.

noncomputable def TauCeti.UnitGradedNatTrans.unitComp {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C' : Type u₁} {D' : Type u₂} [CategoryTheory.EnrichedCategory V C'] [CategoryTheory.EnrichedCategory V D'] {F G H : CategoryTheory.EnrichedFunctor V C' D'} (α : UnitGradedNatTrans F G) (γ : UnitGradedNatTrans G H) : UnitGradedNatTrans F H

Composition of graded natural transformations at the monoidal unit.

Equations

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

theorem TauCeti.UnitGradedNatTrans.unitComp_app {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C' : Type u₁} {D' : Type u₂} [CategoryTheory.EnrichedCategory V C'] [CategoryTheory.EnrichedCategory V D'] {F G H : CategoryTheory.EnrichedFunctor V C' D'} (α : UnitGradedNatTrans F G) (γ : UnitGradedNatTrans G H) (X : C') : (α.unitComp γ).app X = (CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ForgetEnrichment.homOf V (α.app X)) (CategoryTheory.ForgetEnrichment.homOf V (γ.app X)))

A component of the composite at the monoidal unit.

@[simp]

theorem TauCeti.UnitGradedNatTrans.unitComp_app_homOf {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C' : Type u₁} {D' : Type u₂} [CategoryTheory.EnrichedCategory V C'] [CategoryTheory.EnrichedCategory V D'] {F G H : CategoryTheory.EnrichedFunctor V C' D'} (α : UnitGradedNatTrans F G) (γ : UnitGradedNatTrans G H) (X : C') : CategoryTheory.ForgetEnrichment.homOf V ((α.unitComp γ).app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ForgetEnrichment.homOf V (α.app X)) (CategoryTheory.ForgetEnrichment.homOf V (γ.app X))

The ordinary component of a composite is the composite of ordinary components.

noncomputable def TauCeti.UnitGradedNatTrans.id {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C' : Type u₁} {D' : Type u₂} [CategoryTheory.EnrichedCategory V C'] [CategoryTheory.EnrichedCategory V D'] (F : CategoryTheory.EnrichedFunctor V C' D') : UnitGradedNatTrans F F

Identity graded natural transformation at the monoidal unit.

Equations

• TauCeti.UnitGradedNatTrans.id F = { app := fun (X : C') => CategoryTheory.eId V (F.obj X), naturality := ⋯ }

@[simp]

theorem TauCeti.UnitGradedNatTrans.id_app {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C' : Type u₁} {D' : Type u₂} [CategoryTheory.EnrichedCategory V C'] [CategoryTheory.EnrichedCategory V D'] (F : CategoryTheory.EnrichedFunctor V C' D') (X : C') : (id F).app X = CategoryTheory.eId V (F.obj X)

A component of the identity at the monoidal unit.