The symmetric power duality datum

Duality data transfer along module maps, and its instance of record: the symmetric powers of a dual pair form a dual pair, by transferring the power datum along the symmetriser section and projection. The transfer needs no compatibility between the chosen maps — linearity is compositional; the zigzag laws of the transferred datum are where retraction and self-adjointness enter, and they live with the pairing calculus.

noncomputable def RS.ModDualityDatum.transfer {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] {P P' Q Q' : CategoryTheory.Mod D A} (d : ModDualityDatum A P P') (s : Q ⟶ P) (s' : Q' ⟶ P') (r : P ⟶ Q) (r' : P' ⟶ Q') : ModDualityDatum A Q Q'

Duality data transfer: a duality datum for a pair of modules induces one on any pair connected to it by module maps — the pairing pulls back along maps into the pair, the copairing pushes forward along maps out of it. Linearity is inherited compositionally.

Equations

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

noncomputable def RS.symPowπMod {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] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] {X : D} [CategoryTheory.ModObj A X] (n : ℕ) : modPowMod A X n ⟶ symPowMod A X n

The symmetriser projection, as a morphism of bundled modules; the mirror of symPowσMod.

Equations

• RS.symPowπMod A n = { hom := RS.symPowπ A X (n + 1), isModHom := ⋯ }

noncomputable def RS.symDualityDatum {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] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') (n : ℕ) : ModDualityDatum A (symPowMod A M.X n) (symPowMod A M'.X n)

The symmetric power duality datum: the symmetric powers of a dual pair form a dual pair, by transferring the power datum along the symmetriser section and projection.

Equations

• RS.symDualityDatum A M M' d n = RS.ModDualityDatum.transfer A (RS.powDualityDatum A M M' d n) (RS.symPowσMod A n) (RS.symPowσMod A n) (RS.symPowπMod A n) (RS.symPowπMod A n)