The sandwich retract legs

The insertion and contraction making a module a retract of its double-dual sandwich, built from bundled pieces: the unit collapses of the relative tensor as module isomorphisms, the bundled copairing and pairing, and the associator.

theorem RS.modTensorUnitLeft_act {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (N : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorAct A (regularMod A) N) (modTensorUnitLeft A N).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorUnitLeft A N).hom) (actLeft A N.X)

The left unit collapse intertwines the actions.

noncomputable def RS.modTensorUnitLeftMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (N : CategoryTheory.Mod D A) : modTensorMod A (regularMod A) N ≅ N

The left unit collapse, as a module isomorphism.

Equations

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

theorem RS.modTensorUnitRight_act {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (modTensorAct A M (regularMod A)) (modTensorUnitRight A M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorUnitRight A M).hom) (actLeft A M.X)

The right unit collapse intertwines the actions.

noncomputable def RS.modTensorUnitRightMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M : CategoryTheory.Mod D A) : modTensorMod A M (regularMod A) ≅ M

The right unit collapse, as a module isomorphism.

Equations

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

noncomputable def RS.sandwichIns {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') : M ⟶ modTensorMod A (modTensorMod A M M') M

The sandwich insertion: expand the unit and insert the copairing on the left.

Equations

• RS.sandwichIns A d = CategoryTheory.CategoryStruct.comp (RS.modTensorUnitLeftMod A M).symm.hom (RS.modTensorMapMod A (RS.ModDualityDatum.copairMod A d) (CategoryTheory.CategoryStruct.id M))

noncomputable def RS.sandwichCon {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') : modTensorMod A (modTensorMod A M M') M ⟶ M

The sandwich contraction: reassociate, contract the trailing pair, and collapse the unit.

Equations

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

noncomputable def RS.sandwichInsR {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') : M' ⟶ modTensorMod A M' (modTensorMod A M M')

The dual sandwich insertion: expand the unit and insert the copairing on the right.

Equations

• RS.sandwichInsR A d = CategoryTheory.CategoryStruct.comp (RS.modTensorUnitRightMod A M').symm.hom (RS.modTensorMapMod A (CategoryTheory.CategoryStruct.id M') (RS.ModDualityDatum.copairMod A d))

noncomputable def RS.sandwichConR {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {M M' : CategoryTheory.Mod D A} (d : ModDualityDatum A M M') : modTensorMod A M' (modTensorMod A M M') ⟶ M'

The dual sandwich contraction: reassociate backwards, contract the leading pair, and collapse the unit.

Equations

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