The carrier calculus of the power chain

The scalar-based copairing powers of a duality datum, and the two carrier-level operations the chain is built from: contraction against a pairing (RS.carrierContract) and insertion of a copairing (RS.zigCarrier), with their naturality in the module and their evaluation on scalars.

noncomputable def RS.powCopairA {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts 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') (n : ℕ) : A ⟶ powStage A M M' n

The scalar-based copairing power: the base acts on the chain unit.

Equations

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

theorem RS.powCopairA_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts 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') : powCopairA A M M' d 0 = CategoryTheory.CategoryStruct.comp d.copair (modTensorMap A (toModPowModZero A M) (toModPowModZero A M'))

The bottom copairing power is the copairing, through the singleton stages.

noncomputable def RS.carrierContract {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] {M M' : CategoryTheory.Mod D A} (p : modTensor A M' M ⟶ A) : CategoryTheory.MonoidalCategoryStruct.tensorObj M.X (modTensor A M' M) ⟶ M.X

The carrier contraction: the module crosses the relative tensor, pairs against it, and the scalar acts.

Equations

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

@[simp]

theorem RS.whiskerLeft_π_carrierContract {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] {M M' : CategoryTheory.Mod D A} (p : modTensor A M' M ⟶ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (modTensorπ A M' M)) (carrierContract A p) = CategoryTheory.CategoryStruct.comp (β_ M.X (CategoryTheory.MonoidalCategoryStruct.tensorObj M'.X M.X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p) M.X) (actLeft A M.X))

Defining equation of the carrier contraction.

@[simp]

theorem RS.whiskerLeft_π_carrierContract_assoc {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] {M M' : CategoryTheory.Mod D A} (p : modTensor A M' M ⟶ A) {Z : D} (h : M.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (modTensorπ A M' M)) (CategoryTheory.CategoryStruct.comp (carrierContract A p) h) = CategoryTheory.CategoryStruct.comp (β_ M.X (CategoryTheory.MonoidalCategoryStruct.tensorObj M'.X M.X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (modTensorπ A M' M) p) M.X) (CategoryTheory.CategoryStruct.comp (actLeft A M.X) h))

Defining equation of the carrier contraction.

noncomputable def RS.zigCarrier {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] {M M' : CategoryTheory.Mod D A} (c : A ⟶ modTensor A M' M) (p : modTensor A M' M ⟶ A) : M.X ⟶ M.X

The carrier zigzag of a copairing and a pairing: insert the copairing, cross, contract.

Equations

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

noncomputable def RS.fromModPowModZero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts 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) : modPowMod A M.X 0 ⟶ M

The singleton stage maps back onto the module.

Equations

• RS.fromModPowModZero A M = CategoryTheory.Mod.Hom.mk' (RS.modPowOne A M.X).hom ⋯

theorem RS.carrierContract_map {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] {M M' N N' : CategoryTheory.Mod D A} (e : M ⟶ N) (f : N ⟶ M) (f' : N' ⟶ M') (hfe : CategoryTheory.CategoryStruct.comp f e = CategoryTheory.CategoryStruct.id N) (p : modTensor A M' M ⟶ A) (p' : modTensor A N' N ⟶ A) (hp' : CategoryTheory.CategoryStruct.comp (modTensorMap A f' f) p = p') : carrierContract A p' = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom (modTensor A N' N)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (modTensorMap A f' f)) (CategoryTheory.CategoryStruct.comp (carrierContract A p) e.hom))

The carrier contraction transports along module maps of the dual pair.

theorem RS.zigCarrier_map {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] {M M' N N' : CategoryTheory.Mod D A} (e : M ⟶ N) (f : N ⟶ M) (e' : M' ⟶ N') (f' : N' ⟶ M') (hfe : CategoryTheory.CategoryStruct.comp f e = CategoryTheory.CategoryStruct.id N) (hef : CategoryTheory.CategoryStruct.comp e f = CategoryTheory.CategoryStruct.id M) (he'f' : CategoryTheory.CategoryStruct.comp e' f' = CategoryTheory.CategoryStruct.id M') (c : A ⟶ modTensor A M' M) (p : modTensor A M' M ⟶ A) (c' : A ⟶ modTensor A N' N) (p' : modTensor A N' N ⟶ A) (hc' : c' = CategoryTheory.CategoryStruct.comp c (modTensorMap A e' e)) (hp' : CategoryTheory.CategoryStruct.comp (modTensorMap A f' f) p = p') : zigCarrier A c' p' = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (zigCarrier A c p) e.hom)

The carrier zigzag transports along module isomorphisms of the dual pair.

theorem RS.carrierContract_eq {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] {M M' : CategoryTheory.Mod D A} (p : modTensor A M' M ⟶ A) : carrierContract A p = CategoryTheory.CategoryStruct.comp (β_ M.X (modTensor A M' M)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight p M.X) (actLeft A M.X))

The carrier contraction is the crossing, the pairing, and the action, already at the quotient.

theorem RS.zigCarrier_scalar {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] {M M' : CategoryTheory.Mod D A} (c : A ⟶ modTensor A M' M) (p : modTensor A M' M ⟶ A) : zigCarrier A c p = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.comp c p)) M.X) (actLeft A M.X))

The scalar form of the carrier zigzag: the zigzag is the action of the paired copairing scalar.