Transport a monoidal structure along an equivalence. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
When C and D are equivalent as categories,
we can transport a monoidal structure on C along the equivalence,
obtaining a monoidal structure on D.
We then upgrade the original functor and its inverse to monoidal functors
with respect to the new monoidal structure on D.
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) :
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) :
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) :
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) :
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' := _}
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) :
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) :
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) :
@[protected, 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) :
@[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
Instances for category_theory.monoidal.transported
@[protected, instance]
def
category_theory.monoidal.transported.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) :
@[protected, instance]
def
category_theory.monoidal.transported.inhabited
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
@[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) :
@[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) :
@[simp]
theorem
category_theory.monoidal.lax_to_transported_to_functor
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
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) :
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 := e.functor, ε := 𝟙 (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' := _}
@[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) :
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) :
We can upgrade e.functor to a monoidal functor from C to D with the transported structure.
Equations
@[protected, instance]
def
category_theory.monoidal.to_functor.category_theory.is_equivalence
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
noncomputable
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) :
We can upgrade e.inverse to a monoidal functor from D with the transported structure to C.
@[simp]
theorem
category_theory.monoidal.from_transported_to_lax_monoidal_functor_to_functor
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
@[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)
(X Y : category_theory.monoidal.transported e) :
(category_theory.monoidal.from_transported e).to_lax_monoidal_functor.μ X Y = (e.unit_iso.hom.app (e.inverse.obj X) ⊗ e.unit_iso.hom.app (e.inverse.obj Y)) ≫ e.unit_iso.hom.app (e.inverse.obj (e.functor.obj (e.inverse.obj X)) ⊗ e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app X ⊗ e.counit.app Y)
@[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.ε = e.unit.app (𝟙_ C) ≫ category_theory.inv (e.inverse.map (𝟙 (e.functor.obj (𝟙_ C))))
@[simp]
theorem
category_theory.monoidal.transported_monoidal_unit_iso_inv
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
@[simp]
theorem
category_theory.monoidal.transported_monoidal_unit_iso_hom_to_nat_trans
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
noncomputable
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) :
The unit isomorphism upgrades to a monoidal isomorphism.
@[simp]
theorem
category_theory.monoidal.transported_monoidal_counit_iso_inv
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
noncomputable
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) :
The counit isomorphism upgrades to a monoidal isomorphism.
@[simp]
theorem
category_theory.monoidal.transported_monoidal_counit_iso_hom_to_nat_trans
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :