category_theory.monoidal.natural_transformation

source

theorem category_theory.monoidal_nat_trans.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.monoidal_category C} {D : Type u₂} {_inst_3 : category_theory.category D} {_inst_4 : category_theory.monoidal_category D} {F G : category_theory.lax_monoidal_functor C D} (x y : category_theory.monoidal_nat_trans F G) :

x = y ↔ x.to_nat_trans = y.to_nat_trans

source

theorem category_theory.monoidal_nat_trans.ext {C : Type u₁} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.monoidal_category C} {D : Type u₂} {_inst_3 : category_theory.category D} {_inst_4 : category_theory.monoidal_category D} {F G : category_theory.lax_monoidal_functor C D} (x y : category_theory.monoidal_nat_trans F G) (h : x.to_nat_trans = y.to_nat_trans) :

x = y

source

@[ext]

structure category_theory.monoidal_nat_trans {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F G : category_theory.lax_monoidal_functor C D) :

Type (max u₁ v₂)

to_nat_trans : category_theory.nat_trans F.to_functor G.to_functor
unit' : F.ε ≫ self.to_nat_trans.app (𝟙_ C) = G.ε . "obviously"
tensor' : (∀ (X Y : C), F.μ X Y ≫ self.to_nat_trans.app (X ⊗ Y) = (self.to_nat_trans.app X ⊗ self.to_nat_trans.app Y) ≫ G.μ X Y) . "obviously"

A monoidal natural transformation is a natural transformation between (lax) monoidal functors additionally satisfying: F.μ X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ G.μ X Y

Instances for category_theory.monoidal_nat_trans

category_theory.monoidal_nat_trans.has_sizeof_inst
category_theory.monoidal_nat_trans.inhabited

source

@[simp]

theorem category_theory.monoidal_nat_trans.tensor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G : category_theory.lax_monoidal_functor C D} (self : category_theory.monoidal_nat_trans F G) (X Y : C) :

F.μ X Y ≫ self.to_nat_trans.app (X ⊗ Y) = (self.to_nat_trans.app X ⊗ self.to_nat_trans.app Y) ≫ G.μ X Y

source

@[simp]

theorem category_theory.monoidal_nat_trans.tensor_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G : category_theory.lax_monoidal_functor C D} (self : category_theory.monoidal_nat_trans F G) (X Y : C) {X' : D} (f' : G.to_functor.obj (X ⊗ Y) ⟶ X') :

F.μ X Y ≫ self.to_nat_trans.app (X ⊗ Y) ≫ f' = (self.to_nat_trans.app X ⊗ self.to_nat_trans.app Y) ≫ G.μ X Y ≫ f'

source

@[simp]

theorem category_theory.monoidal_nat_trans.unit {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G : category_theory.lax_monoidal_functor C D} (self : category_theory.monoidal_nat_trans F G) :

F.ε ≫ self.to_nat_trans.app (𝟙_ C) = G.ε

source

@[simp]

theorem category_theory.monoidal_nat_trans.unit_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G : category_theory.lax_monoidal_functor C D} (self : category_theory.monoidal_nat_trans F G) {X' : D} (f' : G.to_functor.obj (𝟙_ C) ⟶ X') :

F.ε ≫ self.to_nat_trans.app (𝟙_ C) ≫ f' = G.ε ≫ f'

source

@[simp]

theorem category_theory.monoidal_nat_trans.id_to_nat_trans {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.lax_monoidal_functor C D) :

(category_theory.monoidal_nat_trans.id F).to_nat_trans = 𝟙 F.to_functor

source

def category_theory.monoidal_nat_trans.id {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.lax_monoidal_functor C D) :

category_theory.monoidal_nat_trans F F

The identity monoidal natural transformation.

Equations

category_theory.monoidal_nat_trans.id F = {to_nat_trans := {app := (𝟙 F.to_functor).app, naturality' := _}, unit' := _, tensor' := _}

source

@[protected, instance]

def category_theory.monoidal_nat_trans.inhabited {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.lax_monoidal_functor C D) :

inhabited (category_theory.monoidal_nat_trans F F)

Equations

category_theory.monoidal_nat_trans.inhabited F = {default := category_theory.monoidal_nat_trans.id F}

source

@[simp]

theorem category_theory.monoidal_nat_trans.vcomp_to_nat_trans {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G H : category_theory.lax_monoidal_functor C D} (α : category_theory.monoidal_nat_trans F G) (β : category_theory.monoidal_nat_trans G H) :

(α.vcomp β).to_nat_trans = α.to_nat_trans.vcomp β.to_nat_trans

source

def category_theory.monoidal_nat_trans.vcomp {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G H : category_theory.lax_monoidal_functor C D} (α : category_theory.monoidal_nat_trans F G) (β : category_theory.monoidal_nat_trans G H) :

category_theory.monoidal_nat_trans F H

Vertical composition of monoidal natural transformations.

Equations

α.vcomp β = {to_nat_trans := {app := (α.to_nat_trans.vcomp β.to_nat_trans).app, naturality' := _}, unit' := _, tensor' := _}

source

@[protected, instance]

def category_theory.monoidal_nat_trans.category_lax_monoidal_functor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] :

category_theory.category (category_theory.lax_monoidal_functor C D)

Equations

category_theory.monoidal_nat_trans.category_lax_monoidal_functor = {to_category_struct := {to_quiver := {hom := category_theory.monoidal_nat_trans _inst_4}, id := category_theory.monoidal_nat_trans.id _inst_4, comp := λ (F G H : category_theory.lax_monoidal_functor C D) (α : F ⟶ G) (β : G ⟶ H), category_theory.monoidal_nat_trans.vcomp α β}, id_comp' := _, comp_id' := _, assoc' := _}

source

@[simp]

theorem category_theory.monoidal_nat_trans.comp_to_nat_trans_lax {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G H : category_theory.lax_monoidal_functor C D} {α : F ⟶ G} {β : G ⟶ H} :

(α ≫ β).to_nat_trans = α.to_nat_trans ≫ β.to_nat_trans

source

@[protected, instance]

def category_theory.monoidal_nat_trans.category_monoidal_functor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] :

category_theory.category (category_theory.monoidal_functor C D)

Equations

category_theory.monoidal_nat_trans.category_monoidal_functor = category_theory.induced_category.category category_theory.monoidal_functor.to_lax_monoidal_functor

source

@[simp]

theorem category_theory.monoidal_nat_trans.comp_to_nat_trans {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G H : category_theory.monoidal_functor C D} {α : F ⟶ G} {β : G ⟶ H} :

(α ≫ β).to_nat_trans = α.to_nat_trans ≫ β.to_nat_trans

source

@[simp]

theorem category_theory.monoidal_nat_trans.hcomp_to_nat_trans {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] {F G : category_theory.lax_monoidal_functor C D} {H K : category_theory.lax_monoidal_functor D E} (α : category_theory.monoidal_nat_trans F G) (β : category_theory.monoidal_nat_trans H K) :

(α.hcomp β).to_nat_trans = α.to_nat_trans ◫ β.to_nat_trans

source

def category_theory.monoidal_nat_trans.hcomp {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] {F G : category_theory.lax_monoidal_functor C D} {H K : category_theory.lax_monoidal_functor D E} (α : category_theory.monoidal_nat_trans F G) (β : category_theory.monoidal_nat_trans H K) :

category_theory.monoidal_nat_trans (F ⊗⋙ H) (G ⊗⋙ K)

Horizontal composition of monoidal natural transformations.

Equations

α.hcomp β = {to_nat_trans := {app := (α.to_nat_trans ◫ β.to_nat_trans).app, naturality' := _}, unit' := _, tensor' := _}

source

def category_theory.monoidal_nat_trans.prod {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] {F G : category_theory.lax_monoidal_functor C D} {H K : category_theory.lax_monoidal_functor C E} (α : category_theory.monoidal_nat_trans F G) (β : category_theory.monoidal_nat_trans H K) :

category_theory.monoidal_nat_trans (F.prod' H) (G.prod' K)

The cartesian product of two monoidal natural transformations is monoidal.

Equations

α.prod β = {to_nat_trans := {app := λ (X : C), (α.to_nat_trans.app X, β.to_nat_trans.app X), naturality' := _}, unit' := _, tensor' := _}

source

@[simp]

theorem category_theory.monoidal_nat_trans.prod_to_nat_trans_app {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] {F G : category_theory.lax_monoidal_functor C D} {H K : category_theory.lax_monoidal_functor C E} (α : category_theory.monoidal_nat_trans F G) (β : category_theory.monoidal_nat_trans H K) (X : C) :

(α.prod β).to_nat_trans.app X = (α.to_nat_trans.app X, β.to_nat_trans.app X)

source

def category_theory.monoidal_nat_iso.of_components {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G : category_theory.lax_monoidal_functor C D} (app : Π (X : C), F.to_functor.obj X ≅ G.to_functor.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), F.to_functor.map f ≫ (app Y).hom = (app X).hom ≫ G.to_functor.map f) (unit : F.ε ≫ (app (𝟙_ C)).hom = G.ε) (tensor : ∀ (X Y : C), F.μ X Y ≫ (app (X ⊗ Y)).hom = ((app X).hom ⊗ (app Y).hom) ≫ G.μ X Y) :

F ≅ G

Construct a monoidal natural isomorphism from object level isomorphisms, and the monoidal naturality in the forward direction.

Equations

category_theory.monoidal_nat_iso.of_components app naturality unit tensor = {hom := {to_nat_trans := {app := λ (X : C), (app X).hom, naturality' := naturality}, unit' := unit, tensor' := tensor}, inv := {to_nat_trans := {app := λ (X : C), (app X).inv, naturality' := _}, unit' := _, tensor' := _}, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.monoidal_nat_iso.of_components.hom_app {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G : category_theory.lax_monoidal_functor C D} (app : Π (X : C), F.to_functor.obj X ≅ G.to_functor.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), F.to_functor.map f ≫ (app Y).hom = (app X).hom ≫ G.to_functor.map f) (unit : F.ε ≫ (app (𝟙_ C)).hom = G.ε) (tensor : ∀ (X Y : C), F.μ X Y ≫ (app (X ⊗ Y)).hom = ((app X).hom ⊗ (app Y).hom) ≫ G.μ X Y) (X : C) :

(category_theory.monoidal_nat_iso.of_components app naturality unit tensor).hom.to_nat_trans.app X = (app X).hom

source

@[simp]

theorem category_theory.monoidal_nat_iso.of_components.inv_app {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G : category_theory.lax_monoidal_functor C D} (app : Π (X : C), F.to_functor.obj X ≅ G.to_functor.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), F.to_functor.map f ≫ (app Y).hom = (app X).hom ≫ G.to_functor.map f) (unit : F.ε ≫ (app (𝟙_ C)).hom = G.ε) (tensor : ∀ (X Y : C), F.μ X Y ≫ (app (X ⊗ Y)).hom = ((app X).hom ⊗ (app Y).hom) ≫ G.μ X Y) (X : C) :

(category_theory.monoidal_nat_iso.of_components app naturality unit tensor).inv.to_nat_trans.app X = (app X).inv

source

@[protected, instance]

def category_theory.monoidal_nat_iso.is_iso_of_is_iso_app {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G : category_theory.lax_monoidal_functor C D} (α : F ⟶ G) [∀ (X : C), category_theory.is_iso (α.to_nat_trans.app X)] :

category_theory.is_iso α

source

def category_theory.monoidal_unit {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.monoidal_functor C D) [category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor] :

category_theory.lax_monoidal_functor.id C ⟶ F.to_lax_monoidal_functor ⊗⋙ (category_theory.monoidal_inverse F).to_lax_monoidal_functor

The unit of a monoidal equivalence can be upgraded to a monoidal natural transformation.

Equations

category_theory.monoidal_unit F = let e : C ≌ D := F.to_lax_monoidal_functor.to_functor.as_equivalence in {to_nat_trans := e.unit, unit' := _, tensor' := _}

Instances for category_theory.monoidal_unit

category_theory.monoidal_unit.is_iso

source

@[simp]

theorem category_theory.monoidal_unit_to_nat_trans {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.monoidal_functor C D) [category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor] :

(category_theory.monoidal_unit F).to_nat_trans = F.to_lax_monoidal_functor.to_functor.as_equivalence.unit

source

@[protected, instance]

def category_theory.monoidal_unit.is_iso {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.monoidal_functor C D) [category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor] :

category_theory.is_iso (category_theory.monoidal_unit F)

source

def category_theory.monoidal_counit {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.monoidal_functor C D) [category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor] :

(category_theory.monoidal_inverse F).to_lax_monoidal_functor ⊗⋙ F.to_lax_monoidal_functor ⟶ category_theory.lax_monoidal_functor.id D

The counit of a monoidal equivalence can be upgraded to a monoidal natural transformation.

Equations

category_theory.monoidal_counit F = let e : C ≌ D := F.to_lax_monoidal_functor.to_functor.as_equivalence in {to_nat_trans := e.counit, unit' := _, tensor' := _}

Instances for category_theory.monoidal_counit

category_theory.monoidal_counit.is_iso

source

@[simp]

theorem category_theory.monoidal_counit_to_nat_trans {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.monoidal_functor C D) [category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor] :

(category_theory.monoidal_counit F).to_nat_trans = F.to_lax_monoidal_functor.to_functor.as_equivalence.counit

source

@[protected, instance]

def category_theory.monoidal_counit.is_iso {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F : category_theory.monoidal_functor C D) [category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor] :

category_theory.is_iso (category_theory.monoidal_counit F)

mathlib3 documentation

Monoidal natural transformations #