class CategoryTheory.IsInvertibleObject {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X : C) : Type (max u v)

An object X of a monoidal category C is invertible if there exists an object tensorInverse together with isomorphisms X ⊗ tensorInverse ≅ 𝟙_ C and tensorInverse ⊗ X ≅ 𝟙_ C (cf. Definition 1.11.1).

• tensorInverse : C
• compIso : MonoidalCategoryStruct.tensorObj X (tensorInverse X) ≅ MonoidalCategoryStruct.tensorUnit C
• invCompIso : MonoidalCategoryStruct.tensorObj (tensorInverse X) X ≅ MonoidalCategoryStruct.tensorUnit C

@[reducible]

def CategoryTheory.unit_invertible {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : IsInvertibleObject (MonoidalCategoryStruct.tensorUnit C)

The unit object 𝟙_ C is invertible, with itself as tensor inverse and the left unitor as both compositional isomorphisms.

def CategoryTheory.Definition_1_11_1_InvertibleObject {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) : Prop

Definition 1.11.1: in a rigid category, an object X is invertible iff both the evaluation ε_ X Xᘁ and the coevaluation η_ X Xᘁ are isomorphisms.

@[reducible]

def CategoryTheory.IsInvertibleObject.ofRightDual {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X : C) [HasRightDual X] (h1 : MonoidalCategoryStruct.tensorObj X Xᘁ ≅ MonoidalCategoryStruct.tensorUnit C) (h2 : MonoidalCategoryStruct.tensorObj Xᘁ X ≅ MonoidalCategoryStruct.tensorUnit C) : IsInvertibleObject X

Construct an IsInvertibleObject instance for X from its right dual Xᘁ together with isomorphisms X ⊗ Xᘁ ≅ 𝟙_ C and Xᘁ ⊗ X ≅ 𝟙_ C.

@[reducible]

def CategoryTheory.IsInvertibleObject.inverseInvertible {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X : C) [h : IsInvertibleObject X] : IsInvertibleObject (tensorInverse X)

The tensor inverse of an invertible object is itself invertible, with X as its inverse.

@[reducible]

def CategoryTheory.rightDual_invertible {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X : C) [HasRightDual X] (hX : IsInvertibleObject X) (h : IsInvertibleObject.tensorInverse X = Xᘁ) : IsInvertibleObject Xᘁ

If the tensor inverse of an invertible object X equals its right dual Xᘁ, then Xᘁ is itself invertible.

noncomputable def CategoryTheory.tensorCompIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y Xi Yi : C} (hX : MonoidalCategoryStruct.tensorObj X Xi ≅ MonoidalCategoryStruct.tensorUnit C) (hY : MonoidalCategoryStruct.tensorObj Y Yi ≅ MonoidalCategoryStruct.tensorUnit C) : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj X Y) (MonoidalCategoryStruct.tensorObj Yi Xi) ≅ MonoidalCategoryStruct.tensorUnit C

Given inverse isomorphisms X ⊗ Xi ≅ 𝟙_ C and Y ⊗ Yi ≅ 𝟙_ C, build the isomorphism (X ⊗ Y) ⊗ (Yi ⊗ Xi) ≅ 𝟙_ C via the associators and unitors.

noncomputable def CategoryTheory.tensorInvCompIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y Xi Yi : C} (hX : MonoidalCategoryStruct.tensorObj Xi X ≅ MonoidalCategoryStruct.tensorUnit C) (hY : MonoidalCategoryStruct.tensorObj Yi Y ≅ MonoidalCategoryStruct.tensorUnit C) : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj Yi Xi) (MonoidalCategoryStruct.tensorObj X Y) ≅ MonoidalCategoryStruct.tensorUnit C

Given inverse isomorphisms Xi ⊗ X ≅ 𝟙_ C and Yi ⊗ Y ≅ 𝟙_ C, build the isomorphism (Yi ⊗ Xi) ⊗ (X ⊗ Y) ≅ 𝟙_ C via the associators and unitors.

@[reducible]

noncomputable def CategoryTheory.tensor_invertible {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X Y : C) [hX : IsInvertibleObject X] [hY : IsInvertibleObject Y] : IsInvertibleObject (MonoidalCategoryStruct.tensorObj X Y)

The tensor product X ⊗ Y of two invertible objects is invertible, with tensor inverse Y⁻¹ ⊗ X⁻¹.

theorem CategoryTheory.zigzag_inv_eval_coeval {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X : C) [HasRightDual X] [IsIso (ε_ X Xᘁ)] [IsIso (η_ X Xᘁ)] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (inv (ε_ X Xᘁ)) Xᘁ) (CategoryStruct.comp (MonoidalCategoryStruct.associator Xᘁ X Xᘁ).hom (MonoidalCategoryStruct.whiskerLeft Xᘁ (inv (η_ X Xᘁ)))) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Xᘁ).hom (MonoidalCategoryStruct.rightUnitor Xᘁ).inv

Zigzag identity for the inverses of evaluation and coevaluation morphisms (one of the two compatibility laws used to upgrade Xᘁ to a left dual when ε, η are iso).

theorem CategoryTheory.zigzag_inv_coeval_eval {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X : C) [HasRightDual X] [IsIso (ε_ X Xᘁ)] [IsIso (η_ X Xᘁ)] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (inv (ε_ X Xᘁ))) (CategoryStruct.comp (MonoidalCategoryStruct.associator X Xᘁ X).inv (MonoidalCategoryStruct.whiskerRight (inv (η_ X Xᘁ)) X)) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).hom (MonoidalCategoryStruct.leftUnitor X).inv

Dual zigzag identity for the inverses of coevaluation and evaluation, completing the exact-pairing axioms for the pair (Xᘁ, X).

@[reducible]

noncomputable def CategoryTheory.exactPairingDualObj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X : C) [HasRightDual X] [IsIso (ε_ X Xᘁ)] [IsIso (η_ X Xᘁ)] : ExactPairing Xᘁ X

When the evaluation and coevaluation of X and Xᘁ are both isomorphisms, Xᘁ together with X forms an exact pairing using their inverses.

noncomputable def CategoryTheory.leftDualIsoRightDual_of_invertible {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) [HasRightDual X] [IsIso (ε_ X Xᘁ)] [IsIso (η_ X Xᘁ)] : ᘁX ≅ Xᘁ

For an invertible object X in a rigid category, the left dual is canonically isomorphic to the right dual.

noncomputable def CategoryTheory.Proposition_1_11_3 {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [RigidCategory C] (X : C) [IsIso (ε_ X Xᘁ)] [IsIso (η_ X Xᘁ)] : (ᘁX ≅ Xᘁ) × ([inst : IsInvertibleObject X] → IsInvertibleObject (IsInvertibleObject.tensorInverse X)) × ((Y : C) → [IsInvertibleObject X] → [IsInvertibleObject Y] → IsInvertibleObject (MonoidalCategoryStruct.tensorObj X Y))

Proposition 1.11.3: for an invertible object X in a rigid category, (i) the left dual is isomorphic to the right dual, (ii) the tensor inverse is invertible, and (iii) the tensor product of invertibles is invertible.

def CategoryTheory.IsInvertibleObjectProp {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : ObjectProperty C

The object property of being invertible, packaged as an ObjectProperty C for use when forming the monoidal subcategory of invertible objects.

instance CategoryTheory.instIsMonoidalIsInvertibleObjectProp {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : IsInvertibleObjectProp.IsMonoidal

The collection of invertible objects in a rigid monoidal category is closed under the monoidal unit and tensor product, hence forms a monoidal subcategory.