The dual of a module object

Substrate for Deligne (2002), §2.8: over a monoidal category D, an exact pairing (X, Y) transports a module structure on X (for a monoid object A) to its dual Y.

• actCoev: the coevaluation twisted by the action, A ⟶ X ⊗ Y, with unit and multiplication laws one_actCoev/mul_actCoev.
• dualActRight: the contragredient right action Y ⊗ A ⟶ Y, the mate of the action under the pairing; right-module laws are dualActRight_one and dualActRight_dualActRight. No braiding is needed at this stage.
• dualActRight_evaluation/coevaluation_dualActRight: the mate calculus carrying the dual action across the evaluation and the coevaluation of the pairing.
• dualActLeft: in a braided category, (β_ Y A).inv ≫ dualActRight; for a commutative monoid this is a left module structure, bundled as dualModObj/dualMod. The inverse braiding is chosen so that the braided right action actRight derived on the dual is exactly dualActRight (actRight_dualMod), which makes the pairing descend through the module-tensor coequalizer on the nose.
• modPairing : modTensor A (dualMod A X Y) (asMod A X) ⟶ A, the descent of ε_ X Y ≫ η[A]. It is balanced but is not a morphism of A-modules for a general module; the equivariance that does hold is whiskerLeft_modTensorπ_act_modPairing.
• modCopairing : A ⟶ modTensor A (asMod A X) (dualMod A X Y), the twisted coevaluation followed by the projection. It is a morphism of modules (mul_modCopairing), bundled as modCopairingHom.

Zigzag identities at the modTensor level, and nonvanishing of the copairing, need the multi-tensor coherence layer and are outside this module's scope.

def RS.actCoev {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X Y

The coevaluation twisted by the action: informally a ↦ (a • xᵢ) ⊗ yᵢ in dual-basis notation.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.actCoev_def {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : actCoev A X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (η_ X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X Y).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A X) Y)))

The twisted coevaluation, unfolded.

theorem RS.actCoev_uncurry {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actCoev A X Y) X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (ε_ X Y)) (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)) = actLeft A X

Uncurrying the twisted coevaluation recovers the action.

theorem RS.actCoev_uncurry_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] {Z : D} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actCoev A X Y) X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (ε_ X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom h))) = CategoryTheory.CategoryStruct.comp (actLeft A X) h

Uncurrying the twisted coevaluation recovers the action.

theorem RS.one_actCoev {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (actCoev A X Y) = η_ X Y

Unit law of the twisted coevaluation.

theorem RS.one_actCoev_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp (actCoev A X Y) h) = CategoryTheory.CategoryStruct.comp (η_ X Y) h

Unit law of the twisted coevaluation.

theorem RS.mul_actCoev {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (actCoev A X Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (actCoev A X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X Y).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A X) Y))

Multiplication law of the twisted coevaluation.

theorem RS.mul_actCoev_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.CategoryStruct.comp (actCoev A X Y) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (actCoev A X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A X Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actLeft A X) Y) h))

Multiplication law of the twisted coevaluation.

def RS.dualActRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : CategoryTheory.MonoidalCategoryStruct.tensorObj Y A ⟶ Y

The contragredient right action on the dual: informally f ⊗ a ↦ f (a • ·), that is, f ⊗ a ↦ f (a • xᵢ) yᵢ in dual-basis notation.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.dualActRight_def {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : dualActRight A X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (actCoev A X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ε_ X Y) Y) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom))

The contragredient right action, unfolded.

theorem RS.dualActRight_evaluation {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (dualActRight A X Y) X) (ε_ X Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y A X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (actLeft A X)) (ε_ X Y))

Evaluation compatibility: the contragredient action against the evaluation is the original action across the pairing. This is the workhorse identity of the mate calculus.

theorem RS.dualActRight_evaluation_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (dualActRight A X Y) X) (CategoryTheory.CategoryStruct.comp (ε_ X Y) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y A X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (actLeft A X)) (CategoryTheory.CategoryStruct.comp (ε_ X Y) h))

Evaluation compatibility: the contragredient action against the evaluation is the original action across the pairing. This is the workhorse identity of the mate calculus.

theorem RS.coevaluation_dualActRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (η_ X Y) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y A).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (dualActRight A X Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor A).hom (actCoev A X Y)

Coevaluation compatibility, the mirror of dualActRight_evaluation: inserting the coevaluation and applying the contragredient action is the twisted coevaluation.

theorem RS.coevaluation_dualActRight_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (η_ X Y) A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (dualActRight A X Y)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor A).hom (CategoryTheory.CategoryStruct.comp (actCoev A X Y) h)

Coevaluation compatibility, the mirror of dualActRight_evaluation: inserting the coevaluation and applying the contragredient action is the twisted coevaluation.

theorem RS.dualActRight_one {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y CategoryTheory.MonObj.one) (dualActRight A X Y) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom

Unitality of the contragredient right action.

theorem RS.dualActRight_one_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] {Z : D} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y CategoryTheory.MonObj.one) (CategoryTheory.CategoryStruct.comp (dualActRight A X Y) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom h

Unitality of the contragredient right action.

theorem RS.dualActRight_dualActRight {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (dualActRight A X Y) A) (dualActRight A X Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y A A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y CategoryTheory.MonObj.mul) (dualActRight A X Y))

Associativity of the contragredient right action.

theorem RS.dualActRight_dualActRight_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] {Z : D} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (dualActRight A X Y) A) (CategoryTheory.CategoryStruct.comp (dualActRight A X Y) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y A A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y CategoryTheory.MonObj.mul) (CategoryTheory.CategoryStruct.comp (dualActRight A X Y) h))

Associativity of the contragredient right action.

def RS.dualActLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ Y

The dual left action: the contragredient right action pulled back along the inverse braiding. The inverse braiding (rather than the braiding β_ A Y) is chosen so that the braided right action actRight derived from it is exactly dualActRight; see actRight_dualMod.

Equations

• RS.dualActLeft A X Y = CategoryTheory.CategoryStruct.comp (β_ Y A).inv (RS.dualActRight A X Y)

theorem RS.dualActLeft_def {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : dualActLeft A X Y = CategoryTheory.CategoryStruct.comp (β_ Y A).inv (dualActRight A X Y)

The dual left action, unfolded.

theorem RS.one_dualActLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one Y) (dualActLeft A X Y) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom

Unitality of the dual left action.

theorem RS.one_dualActLeft_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] {Z : D} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one Y) (CategoryTheory.CategoryStruct.comp (dualActLeft A X Y) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom h

Unitality of the dual left action.

theorem RS.dualActLeft_evaluation {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (dualActLeft A X Y) X) (ε_ X Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ Y A).inv X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y A X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (actLeft A X)) (ε_ X Y)))

Evaluation compatibility for the dual left action.

theorem RS.dualActLeft_evaluation_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (dualActLeft A X Y) X) (CategoryTheory.CategoryStruct.comp (ε_ X Y) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ Y A).inv X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y A X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (actLeft A X)) (CategoryTheory.CategoryStruct.comp (ε_ X Y) h)))

Evaluation compatibility for the dual left action.

theorem RS.mul_dualActLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.IsCommMonObj A] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul Y) (dualActLeft A X Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (dualActLeft A X Y)) (dualActLeft A X Y))

Associativity of the dual left action, for a commutative monoid.

theorem RS.mul_dualActLeft_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.IsCommMonObj A] {Z : D} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul Y) (CategoryTheory.CategoryStruct.comp (dualActLeft A X Y) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (dualActLeft A X Y)) (CategoryTheory.CategoryStruct.comp (dualActLeft A X Y) h))

Associativity of the dual left action, for a commutative monoid.

@[implicit_reducible]

def RS.dualModObj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.IsCommMonObj A] : CategoryTheory.ModObj A Y

The dual module structure on Y, for a commutative monoid.

Equations

• RS.dualModObj A X Y = { smul := RS.dualActLeft A X Y, one_smul := ⋯, mul_smul := ⋯ }

@[reducible]

def RS.dualMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.IsCommMonObj A] : CategoryTheory.Mod D A

The dual of a module, bundled: Y with the transported action.

Equations

• RS.dualMod A X Y = { X := Y, mod := RS.dualModObj A X Y }

theorem RS.actLeft_dualMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.IsCommMonObj A] : actLeft A Y = dualActLeft A X Y

On the dual module the action is the dual left action.

theorem RS.actRight_dualMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.IsCommMonObj A] : actRight A Y = dualActRight A X Y

On the dual module the braided right action is exactly the contragredient right action.

@[reducible]

def RS.asMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.Mod D A

A module object, bundled as a module.

Equations

• RS.asMod A X = { X := X, mod := inst✝ }

theorem RS.modTensorLeg_pair {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (modTensorLegM A (dualMod A X Y) (asMod A X)) (CategoryTheory.CategoryStruct.comp (ε_ X Y) CategoryTheory.MonObj.one) = CategoryTheory.CategoryStruct.comp (modTensorLegN A (dualMod A X Y) (asMod A X)) (CategoryTheory.CategoryStruct.comp (ε_ X Y) CategoryTheory.MonObj.one)

The two coequalizer legs agree against the paired evaluation: this is exactly dualActRight_evaluation, thanks to the inverse braiding convention of dualActLeft.

noncomputable def RS.modPairing {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.Limits.HasCoequalizers D] : modTensor A (dualMod A X Y) (asMod A X) ⟶ A

The A-valued pairing on the module tensor of the dual with the module: the descent of ε_ X Y ≫ η[A] through the coequalizer. It is balanced but, for a general module, not a morphism of A-modules; see whiskerLeft_modTensorπ_act_modPairing for the equivariance it does satisfy.

Equations

• RS.modPairing A X Y = RS.modTensorDesc A (RS.dualMod A X Y) (RS.asMod A X) (CategoryTheory.CategoryStruct.comp (ε_ X Y) CategoryTheory.MonObj.one) ⋯

@[simp]

theorem RS.modTensorπ_modPairing {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.Limits.HasCoequalizers D] : CategoryTheory.CategoryStruct.comp (modTensorπ A (dualMod A X Y) (asMod A X)) (modPairing A X Y) = CategoryTheory.CategoryStruct.comp (ε_ X Y) CategoryTheory.MonObj.one

Defining equation of the pairing.

@[simp]

theorem RS.modTensorπ_modPairing_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.Limits.HasCoequalizers D] {Z : D} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A (dualMod A X Y) (asMod A X)) (CategoryTheory.CategoryStruct.comp (modPairing A X Y) h) = CategoryTheory.CategoryStruct.comp (ε_ X Y) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)

Defining equation of the pairing.

noncomputable def RS.modCopairing {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.Limits.HasCoequalizers D] : A ⟶ modTensor A (asMod A X) (dualMod A X Y)

The copairing into the module tensor of the module with its dual: the twisted coevaluation followed by the projection.

Equations

• RS.modCopairing A X Y = CategoryTheory.CategoryStruct.comp (RS.actCoev A X Y) (RS.modTensorπ A (RS.asMod A X) (RS.dualMod A X Y))

theorem RS.one_modCopairing {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.Limits.HasCoequalizers D] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (modCopairing A X Y) = CategoryTheory.CategoryStruct.comp (η_ X Y) (modTensorπ A (asMod A X) (dualMod A X Y))

The copairing carries the unit to the projected coevaluation.

theorem RS.one_modCopairing_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.Limits.HasCoequalizers D] {Z : D} (h : modTensor A (asMod A X) (dualMod A X Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp (modCopairing A X Y) h) = CategoryTheory.CategoryStruct.comp (η_ X Y) (CategoryTheory.CategoryStruct.comp (modTensorπ A (asMod A X) (dualMod A X Y)) h)

The copairing carries the unit to the projected coevaluation.

theorem RS.whiskerLeft_modTensorπ_act_modPairing {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorπ A (dualMod A X Y) (asMod A X))) (CategoryTheory.CategoryStruct.comp (modTensorAct A (dualMod A X Y) (asMod A X)) (modPairing A X Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A Y X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ Y A).inv X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y A X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (actLeft A X)) (CategoryTheory.CategoryStruct.comp (ε_ X Y) CategoryTheory.MonObj.one))))

Equivariance of the pairing: acting on the tensor product and pairing equals braiding the scalar through and pairing against the acted-on module. For a general module this is the strongest compatibility available; the pairing is not A-linear.

theorem RS.whiskerLeft_modTensorπ_act_modPairing_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] {Z : D} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorπ A (dualMod A X Y) (asMod A X))) (CategoryTheory.CategoryStruct.comp (modTensorAct A (dualMod A X Y) (asMod A X)) (CategoryTheory.CategoryStruct.comp (modPairing A X Y) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A Y X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ Y A).inv X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y A X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (actLeft A X)) (CategoryTheory.CategoryStruct.comp (ε_ X Y) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)))))

Equivariance of the pairing: acting on the tensor product and pairing equals braiding the scalar through and pairing against the acted-on module. For a general module this is the strongest compatibility available; the pairing is not A-linear.

theorem RS.mul_modCopairing {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (modCopairing A X Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modCopairing A X Y)) (modTensorAct A (asMod A X) (dualMod A X Y))

The copairing is a morphism of modules.

theorem RS.mul_modCopairing_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] {Z : D} (h : modTensor A (asMod A X) (dualMod A X Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.CategoryStruct.comp (modCopairing A X Y) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modCopairing A X Y)) (CategoryTheory.CategoryStruct.comp (modTensorAct A (asMod A X) (dualMod A X Y)) h)

The copairing is a morphism of modules.

noncomputable def RS.modCopairingHom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] [CategoryTheory.IsCommMonObj A] (X Y : D) [CategoryTheory.ExactPairing X Y] [CategoryTheory.ModObj A X] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] : regularMod A ⟶ modTensorMod A (asMod A X) (dualMod A X Y)

The copairing, bundled as a morphism of modules out of the regular module.

Equations

• RS.modCopairingHom A X Y = CategoryTheory.Mod.Hom.mk' (RS.modCopairing A X Y) ⋯

def RS.rightDualActLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X : D) [CategoryTheory.HasRightDual X] [CategoryTheory.ModObj A X] : CategoryTheory.MonoidalCategoryStruct.tensorObj A Xᘁ ⟶ Xᘁ

The dual left action, specialised to the right dual Xᘁ.

Equations

• RS.rightDualActLeft A X = RS.dualActLeft A X Xᘁ

theorem RS.one_rightDualActLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X : D) [CategoryTheory.HasRightDual X] [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one Xᘁ) (rightDualActLeft A X) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor Xᘁ).hom

Unitality of the dual left action at the right dual.

theorem RS.one_rightDualActLeft_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X : D) [CategoryTheory.HasRightDual X] [CategoryTheory.ModObj A X] {Z : D} (h : Xᘁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one Xᘁ) (CategoryTheory.CategoryStruct.comp (rightDualActLeft A X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Xᘁ).hom h

Unitality of the dual left action at the right dual.

theorem RS.mul_rightDualActLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X : D) [CategoryTheory.HasRightDual X] [CategoryTheory.ModObj A X] [CategoryTheory.IsCommMonObj A] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul Xᘁ) (rightDualActLeft A X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A Xᘁ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (rightDualActLeft A X)) (rightDualActLeft A X))

Associativity of the dual left action at the right dual.

theorem RS.mul_rightDualActLeft_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X : D) [CategoryTheory.HasRightDual X] [CategoryTheory.ModObj A X] [CategoryTheory.IsCommMonObj A] {Z : D} (h : Xᘁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul Xᘁ) (CategoryTheory.CategoryStruct.comp (rightDualActLeft A X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A Xᘁ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (rightDualActLeft A X)) (CategoryTheory.CategoryStruct.comp (rightDualActLeft A X) h))

Associativity of the dual left action at the right dual.

@[reducible]

def RS.rightDualMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.BraidedCategory D] (X : D) [CategoryTheory.HasRightDual X] [CategoryTheory.ModObj A X] [CategoryTheory.IsCommMonObj A] : CategoryTheory.Mod D A

The dual module, specialised to the right dual Xᘁ.

Equations

• RS.rightDualMod A X = RS.dualMod A X Xᘁ