mathlib documentation

category_theory.monoidal.rigid.of_equivalence

Transport rigid structures over a monoidal equivalence. #

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

category_theory.exact_pairing_of_faithful F eval coeval map_eval map_coeval = {coevaluation := coeval, evaluation := eval, coevaluation_evaluation' := _, evaluation_coevaluation' := _}

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

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

category_theory.has_left_dual_of_equivalence F X = category_theory.has_left_dual.mk (F.to_lax_monoidal_functor.to_functor.inv.obj ᘁ(F.to_lax_monoidal_functor.to_functor.obj X))

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

category_theory.has_right_dual_of_equivalence F X = category_theory.has_right_dual.mk (F.to_lax_monoidal_functor.to_functor.inv.obj (F.to_lax_monoidal_functor.to_functor.obj X)ᘁ)

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

category_theory.left_rigid_category_of_equivalence F = category_theory.left_rigid_category.mk

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

category_theory.right_rigid_category_of_equivalence F = category_theory.right_rigid_category.mk

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

category_theory.rigid_category_of_equivalence F = category_theory.rigid_category.mk