mathlib docs: category_theory.monoidal.transport

@[simp]

theorem category_theory.monoidal.transport_left_unitor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X : D) :

λ_ X = e.functor.map_iso (((e.unit_iso.app (𝟙_ C)).symm ⊗ category_theory.iso.refl (e.inverse.obj X)) ≪≫ λ_ (e.inverse.obj X)) ≪≫ e.counit_iso.app X

source

@[simp]

theorem category_theory.monoidal.transport_associator {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X Y Z : D) :

α_ X Y Z = e.functor.map_iso (((e.unit_iso.app (e.inverse.obj X ⊗ e.inverse.obj Y)).symm ⊗ category_theory.iso.refl (e.inverse.obj Z)) ≪≫ α_ (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z) ≪≫ (category_theory.iso.refl (e.inverse.obj X) ⊗ e.unit_iso.app (e.inverse.obj Y ⊗ e.inverse.obj Z)))

source

@[simp]

theorem category_theory.monoidal.transport_tensor_unit {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

𝟙_ D = e.functor.obj (𝟙_ C)

source

def category_theory.monoidal.transport {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

category_theory.monoidal_category D

Transport a monoidal structure along an equivalence of (plain) categories.

Equations

category_theory.monoidal.transport e = {tensor_obj := λ (X Y : D), e.functor.obj (e.inverse.obj X ⊗ e.inverse.obj Y), tensor_hom := λ (W X Y Z : D) (f : W ⟶ X) (g : Y ⟶ Z), e.functor.map (e.inverse.map f ⊗ e.inverse.map g), tensor_id' := _, tensor_comp' := _, tensor_unit := e.functor.obj (𝟙_ C), associator := λ (X Y Z : D), e.functor.map_iso (((e.unit_iso.app (e.inverse.obj X ⊗ e.inverse.obj Y)).symm ⊗ category_theory.iso.refl (e.inverse.obj Z)) ≪≫ α_ (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z) ≪≫ (category_theory.iso.refl (e.inverse.obj X) ⊗ e.unit_iso.app (e.inverse.obj Y ⊗ e.inverse.obj Z))), associator_naturality' := _, left_unitor := λ (X : D), e.functor.map_iso (((e.unit_iso.app (𝟙_ C)).symm ⊗ category_theory.iso.refl (e.inverse.obj X)) ≪≫ λ_ (e.inverse.obj X)) ≪≫ e.counit_iso.app X, left_unitor_naturality' := _, right_unitor := λ (X : D), e.functor.map_iso ((category_theory.iso.refl (e.inverse.obj X) ⊗ (e.unit_iso.app (𝟙_ C)).symm) ≪≫ ρ_ (e.inverse.obj X)) ≪≫ e.counit_iso.app X, right_unitor_naturality' := _, pentagon' := _, triangle' := _}

source

@[simp]

theorem category_theory.monoidal.transport_tensor_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (W X Y Z : D) (f : W ⟶ X) (g : Y ⟶ Z) :

f ⊗ g = e.functor.map (e.inverse.map f ⊗ e.inverse.map g)

source

@[simp]

theorem category_theory.monoidal.transport_tensor_obj {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X Y : D) :

X ⊗ Y = e.functor.obj (e.inverse.obj X ⊗ e.inverse.obj Y)

source

@[simp]

theorem category_theory.monoidal.transport_right_unitor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X : D) :

ρ_ X = e.functor.map_iso ((category_theory.iso.refl (e.inverse.obj X) ⊗ (e.unit_iso.app (𝟙_ C)).symm) ≪≫ ρ_ (e.inverse.obj X)) ≪≫ e.counit_iso.app X

source

@[instance]

def category_theory.monoidal.transported.category {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

category_theory.category (category_theory.monoidal.transported e)

source

@[nolint]

def category_theory.monoidal.transported {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

Type u₂

A type synonym for D, which will carry the transported monoidal structure.

Equations

category_theory.monoidal.transported e = D

source

@[instance]

def category_theory.monoidal.category_theory.monoidal_category {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

category_theory.monoidal_category (category_theory.monoidal.transported e)

Equations

category_theory.monoidal.category_theory.monoidal_category e = category_theory.monoidal.transport e

source

@[instance]

def category_theory.monoidal.inhabited {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

inhabited (category_theory.monoidal.transported e)

Equations

category_theory.monoidal.inhabited e = {default := 𝟙_ (category_theory.monoidal.transported e) (category_theory.monoidal.category_theory.monoidal_category e)}

source

@[simp]

theorem category_theory.monoidal.lax_to_transported_μ {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X Y : C) :

(category_theory.monoidal.lax_to_transported e).μ X Y = e.functor.map (e.unit_inv.app X ⊗ e.unit_inv.app Y)

source

@[simp]

theorem category_theory.monoidal.lax_to_transported_ε {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

(category_theory.monoidal.lax_to_transported e).ε = 𝟙 (e.functor.obj (𝟙_ C))

source

@[simp]

theorem category_theory.monoidal.lax_to_transported_to_functor_obj {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (a : C) :

(category_theory.monoidal.lax_to_transported e).to_functor.obj a = e.functor.obj a

source

def category_theory.monoidal.lax_to_transported {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

category_theory.lax_monoidal_functor C (category_theory.monoidal.transported e)

We can upgrade e.functor to a lax monoidal functor from C to D with the transported structure.

Equations

category_theory.monoidal.lax_to_transported e = {to_functor := {obj := e.functor.obj, map := e.functor.map, map_id' := _, map_comp' := _}, ε := 𝟙 (e.functor.obj (𝟙_ C)), μ := λ (X Y : C), e.functor.map (e.unit_inv.app X ⊗ e.unit_inv.app Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}

source

@[simp]

theorem category_theory.monoidal.lax_to_transported_to_functor_map {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) {X Y : C} (a : X ⟶ Y) :

(category_theory.monoidal.lax_to_transported e).to_functor.map a = e.functor.map a

source

@[simp]

theorem category_theory.monoidal.to_transported_ε_is_iso {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

(category_theory.monoidal.to_transported e).ε_is_iso = id (category_theory.is_iso.id (e.functor.obj (𝟙_ C)))

source

@[simp]

theorem category_theory.monoidal.to_transported_μ_is_iso {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X Y : C) :

(category_theory.monoidal.to_transported e).μ_is_iso X Y = id (e.functor.map_is_iso (e.unit_inv.app X ⊗ e.unit_inv.app Y))

source

@[simp]

theorem category_theory.monoidal.to_transported_to_lax_monoidal_functor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

(category_theory.monoidal.to_transported e).to_lax_monoidal_functor = category_theory.monoidal.lax_to_transported e

source

def category_theory.monoidal.to_transported {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

category_theory.monoidal_functor C (category_theory.monoidal.transported e)

We can upgrade e.functor to a monoidal functor from C to D with the transported structure.

Equations

category_theory.monoidal.to_transported e = {to_lax_monoidal_functor := {to_functor := (category_theory.monoidal.lax_to_transported e).to_functor, ε := (category_theory.monoidal.lax_to_transported e).ε, μ := (category_theory.monoidal.lax_to_transported e).μ, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := id (category_theory.is_iso.id (e.functor.obj (𝟙_ C))), μ_is_iso := λ (X Y : C), id (e.functor.map_is_iso (e.unit_inv.app X ⊗ e.unit_inv.app Y))}

source

@[simp]

theorem category_theory.monoidal.lax_from_transported_μ {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X Y : category_theory.monoidal.transported e) :

(category_theory.monoidal.lax_from_transported e).μ X Y = e.unit.app (e.inverse.obj X ⊗ e.inverse.obj Y)

source

@[simp]

theorem category_theory.monoidal.lax_from_transported_to_functor_obj {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (a : D) :

(category_theory.monoidal.lax_from_transported e).to_functor.obj a = e.inverse.obj a

source

@[simp]

theorem category_theory.monoidal.lax_from_transported_to_functor_map {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) {X Y : D} (a : X ⟶ Y) :

(category_theory.monoidal.lax_from_transported e).to_functor.map a = e.inverse.map a

source

@[simp]

theorem category_theory.monoidal.lax_from_transported_ε {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

(category_theory.monoidal.lax_from_transported e).ε = e.unit.app (𝟙_ C)

source

def category_theory.monoidal.lax_from_transported {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

category_theory.lax_monoidal_functor (category_theory.monoidal.transported e) C

We can upgrade e.inverse to a lax monoidal functor from D with the transported structure to C.

Equations

category_theory.monoidal.lax_from_transported e = {to_functor := {obj := e.inverse.obj, map := e.inverse.map, map_id' := _, map_comp' := _}, ε := e.unit.app (𝟙_ C), μ := λ (X Y : category_theory.monoidal.transported e), e.unit.app (e.inverse.obj X ⊗ e.inverse.obj Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}

source

@[simp]

theorem category_theory.monoidal.from_transported_to_lax_monoidal_functor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

(category_theory.monoidal.from_transported e).to_lax_monoidal_functor = category_theory.monoidal.lax_from_transported e

source

@[simp]

theorem category_theory.monoidal.from_transported_ε_is_iso {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

(category_theory.monoidal.from_transported e).ε_is_iso = id (category_theory.nat_iso.is_iso_app_of_is_iso e.unit (𝟙_ C))

source

def category_theory.monoidal.from_transported {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

category_theory.monoidal_functor (category_theory.monoidal.transported e) C

We can upgrade e.inverse to a monoidal functor from D with the transported structure to C.

Equations

category_theory.monoidal.from_transported e = {to_lax_monoidal_functor := {to_functor := (category_theory.monoidal.lax_from_transported e).to_functor, ε := (category_theory.monoidal.lax_from_transported e).ε, μ := (category_theory.monoidal.lax_from_transported e).μ, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := id (category_theory.nat_iso.is_iso_app_of_is_iso e.unit (𝟙_ C)), μ_is_iso := λ (X Y : category_theory.monoidal.transported e), id (category_theory.nat_iso.is_iso_app_of_is_iso e.unit (e.inverse.obj X ⊗ e.inverse.obj Y))}

source

@[simp]

theorem category_theory.monoidal.from_transported_μ_is_iso {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X Y : category_theory.monoidal.transported e) :

(category_theory.monoidal.from_transported e).μ_is_iso X Y = id (category_theory.nat_iso.is_iso_app_of_is_iso e.unit (e.inverse.obj X ⊗ e.inverse.obj Y))

source

@[simp]

theorem category_theory.monoidal.transported_monoidal_unit_iso_inv_to_nat_trans_app {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X : C) :

(category_theory.monoidal.transported_monoidal_unit_iso e).inv.to_nat_trans.app X = category_theory.is_iso.inv ({to_nat_trans := {app := λ (X : C), ((λ (X : C), e.unit_iso.app X) X).hom, naturality' := _}, unit' := _, tensor' := _}.to_nat_trans.app X)

source

def category_theory.monoidal.transported_monoidal_unit_iso {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

category_theory.lax_monoidal_functor.id C ≅ category_theory.monoidal.lax_to_transported e ⊗⋙ category_theory.monoidal.lax_from_transported e

The unit isomorphism upgrades to a monoidal isomorphism.

Equations

category_theory.monoidal.transported_monoidal_unit_iso e = category_theory.monoidal_nat_iso.of_components (λ (X : C), e.unit_iso.app X) _ _ _

source

@[simp]

theorem category_theory.monoidal.transported_monoidal_unit_iso_hom_to_nat_trans_app {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X : C) :

(category_theory.monoidal.transported_monoidal_unit_iso e).hom.to_nat_trans.app X = ((λ (X : C), e.unit_iso.app X) X).hom

source

@[simp]

theorem category_theory.monoidal.transported_monoidal_counit_iso_hom_to_nat_trans_app {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X : category_theory.monoidal.transported e) :

(category_theory.monoidal.transported_monoidal_counit_iso e).hom.to_nat_trans.app X = ((λ (X : category_theory.monoidal.transported e), e.counit_iso.app X) X).hom

source

@[simp]

theorem category_theory.monoidal.transported_monoidal_counit_iso_inv_to_nat_trans_app {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) (X : category_theory.monoidal.transported e) :

(category_theory.monoidal.transported_monoidal_counit_iso e).inv.to_nat_trans.app X = category_theory.is_iso.inv ({to_nat_trans := {app := λ (X : category_theory.monoidal.transported e), ((λ (X : category_theory.monoidal.transported e), e.counit_iso.app X) X).hom, naturality' := _}, unit' := _, tensor' := _}.to_nat_trans.app X)

source

def category_theory.monoidal.transported_monoidal_counit_iso {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] (e : C ≌ D) :

category_theory.monoidal.lax_from_transported e ⊗⋙ category_theory.monoidal.lax_to_transported e ≅ category_theory.lax_monoidal_functor.id (category_theory.monoidal.transported e)

The counit isomorphism upgrades to a monoidal isomorphism.

Equations

category_theory.monoidal.transported_monoidal_counit_iso e = category_theory.monoidal_nat_iso.of_components (λ (X : category_theory.monoidal.transported e), e.counit_iso.app X) _ _ _

mathlib documentation

Transport a monoidal structure along an equivalence.