mathlib3 documentation

category_theory.monoidal.rigid.of_equivalence

Transport rigid structures over a monoidal equivalence. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
def category_theory.exact_pairing_of_faithful {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.monoidal_category C] [category_theory.monoidal_category D] (F : category_theory.monoidal_functor C D) [category_theory.faithful F.to_lax_monoidal_functor.to_functor] {X Y : C} (eval : Y ⊗ X ⟶ 𝟙_ C) (coeval : 𝟙_ C ⟶ X ⊗ Y) [category_theory.exact_pairing (F.to_lax_monoidal_functor.to_functor.obj X) (F.to_lax_monoidal_functor.to_functor.obj Y)] (map_eval : F.to_lax_monoidal_functor.to_functor.map eval = category_theory.inv (F.to_lax_monoidal_functor.μ Y X) ≫ ε_ (F.to_lax_monoidal_functor.to_functor.obj X) (F.to_lax_monoidal_functor.to_functor.obj Y) ≫ F.to_lax_monoidal_functor.ε) (map_coeval : F.to_lax_monoidal_functor.to_functor.map coeval = category_theory.inv F.to_lax_monoidal_functor.ε ≫ η_ (F.to_lax_monoidal_functor.to_functor.obj X) (F.to_lax_monoidal_functor.to_functor.obj Y) ≫ F.to_lax_monoidal_functor.μ X Y) :
category_theory.exact_pairing X Y

Given candidate data for an exact pairing, which is sent by a faithful monoidal functor to an exact pairing, the equations holds automatically.

Equations
source
noncomputable def category_theory.exact_pairing_of_fully_faithful {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.monoidal_category C] [category_theory.monoidal_category D] (F : category_theory.monoidal_functor C D) [category_theory.full F.to_lax_monoidal_functor.to_functor] [category_theory.faithful F.to_lax_monoidal_functor.to_functor] (X Y : C) [category_theory.exact_pairing (F.to_lax_monoidal_functor.to_functor.obj X) (F.to_lax_monoidal_functor.to_functor.obj Y)] :
category_theory.exact_pairing X Y

Given a pair of objects which are sent by a fully faithful functor to a pair of objects with an exact pairing, we get an exact pairing.

Equations
source
noncomputable def category_theory.has_left_dual_of_equivalence {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.monoidal_category C] [category_theory.monoidal_category D] (F : category_theory.monoidal_functor C D) [category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor] (X : C) [category_theory.has_left_dual (F.to_lax_monoidal_functor.to_functor.obj X)] :
category_theory.has_left_dual X

Pull back a left dual along an equivalence.

Equations
source
noncomputable def category_theory.has_right_dual_of_equivalence {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.monoidal_category C] [category_theory.monoidal_category D] (F : category_theory.monoidal_functor C D) [category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor] (X : C) [category_theory.has_right_dual (F.to_lax_monoidal_functor.to_functor.obj X)] :
category_theory.has_right_dual X

Pull back a right dual along an equivalence.

Equations
source
noncomputable def category_theory.left_rigid_category_of_equivalence {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.monoidal_category C] [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.left_rigid_category D] :
category_theory.left_rigid_category C

Pull back a left rigid structure along an equivalence.

Equations
source
noncomputable def category_theory.right_rigid_category_of_equivalence {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.monoidal_category C] [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.right_rigid_category D] :
category_theory.right_rigid_category C

Pull back a right rigid structure along an equivalence.

Equations
source
noncomputable def category_theory.rigid_category_of_equivalence {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] [category_theory.monoidal_category C] [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.rigid_category D] :
category_theory.rigid_category C

Pull back a rigid structure along an equivalence.

Equations