The parity shift of a super module

Exchanging the two components of a super module and relabelling the four action blocks accordingly again gives a super module: the module parity is only a label, so the eight associativities permute among themselves and no sign appears. This is the module underlying a twist by the odd line.

def RS.SuperCommAlgebra.Mod.shift {S : SuperCommAlgebra} (M : S.Mod) : S.Mod

The parity shift of a super module.

Equations

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

theorem RS.SuperCommAlgebra.Mod.shift_even {S : SuperCommAlgebra} (M : S.Mod) : M.shift.even = M.odd

The even component of the shift is the odd component. This is definitional, and is stated for use by name: as a simp rule it would rewrite the type arguments of every application of the shifted module's interface and so stop that interface firing.