Tensoring with the shifted unit is the parity shift #

For a super-commutative ℂ-algebra S and a module M over it, the parity shift of the unit module is invertible for the tensor product of RS.Classical.Deligne.SuperModTensor:

(shift S.unitMod) ⊗ M ≅ shift M.

The construction is the exact analogue of the left unitor of RS.Classical.Deligne.SuperModMonoidal, with the parity of the algebra factor reversed. Reversing that parity forces two of the four blocks to carry a sign: the shifted unit relabels the four multiplication blocks of S, and the eight balancing laws of the tensor product then hold only for the block pattern

fee = M.actOE, foo = -M.actEO, feo = -M.actOO, foe = M.actEE,

whose relative signs are pinned by the odd-odd relators (where the Koszul sign lives) and by the odd action laws; the overall sign is the one free choice, normalised here by taking the even-even block unsigned. The inverse carries the matching sign, −1 in even degree and +1 in odd degree.

Contents #

RS.SuperCommAlgebra.Mod.shiftUnitMod_actOO_one, shiftUnitMod_actEO_one: acting on the algebra unit inside the shifted unit module returns the scalar.
RS.SuperCommAlgebra.Mod.shiftUnitData: the four blocks with their eight balancing laws and eight action laws.
RS.SuperCommAlgebra.Mod.shiftUnitHom, shiftUnitInv: the two structure maps, with their computation rules.
RS.SuperCommAlgebra.Mod.shiftUnitTensor: the isomorphism.

The shifted unit module #

source

theorem RS.SuperCommAlgebra.Mod.shiftUnitMod_actOO_one {S : SuperCommAlgebra} (v : S.odd) :

(S.unitMod.shift.actOO v) S.one = v

Acting by an odd scalar on the algebra unit, viewed inside the shifted unit module, returns the scalar. In the shifted module the algebra unit is odd, so the relevant block is actOO.

source

theorem RS.SuperCommAlgebra.Mod.shiftUnitMod_actEO_one {S : SuperCommAlgebra} (x : S.even) :

(S.unitMod.shift.actEO x) S.one = x

Acting by an even scalar on the algebra unit, viewed inside the shifted unit module, returns the scalar.

The four blocks #

source

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

S.unitMod.shift.TensorData M M.shift

The data of the shift-unit isomorphism: the shifted unit factor acts on the module, with the parities of the algebra relabelled. The odd-odd and even-odd blocks carry a sign, forced by the four mixed balancing laws and by the four odd action laws.

Equations

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

Instances For

The structure maps #

source

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

S.unitMod.shift.tensor M ⟶ M.shift

The structure map of the shift-unit isomorphism.

Equations

M.shiftUnitHom = RS.SuperCommAlgebra.Mod.mkHom M.shiftUnitData

Instances For

source

@[simp]

theorem RS.SuperCommAlgebra.Mod.shiftUnitHom_evenMap_tmulEE {S : SuperCommAlgebra} (M : S.Mod) (v : S.odd) (m : M.even) :

M.shiftUnitHom.evenMap (((S.unitMod.shift.tmulEE M) v) m) = (M.actOE v) m

The structure map on an even-even generator.

source

@[simp]

theorem RS.SuperCommAlgebra.Mod.shiftUnitHom_evenMap_tmulOO {S : SuperCommAlgebra} (M : S.Mod) (x : S.even) (m : M.odd) :

M.shiftUnitHom.evenMap (((S.unitMod.shift.tmulOO M) x) m) = -(M.actEO x) m

The structure map on an odd-odd generator.

source

@[simp]

theorem RS.SuperCommAlgebra.Mod.shiftUnitHom_oddMap_tmulEO {S : SuperCommAlgebra} (M : S.Mod) (v : S.odd) (m : M.odd) :

M.shiftUnitHom.oddMap (((S.unitMod.shift.tmulEO M) v) m) = -(M.actOO v) m

The structure map on an even-odd generator.

source

@[simp]

theorem RS.SuperCommAlgebra.Mod.shiftUnitHom_oddMap_tmulOE {S : SuperCommAlgebra} (M : S.Mod) (x : S.even) (m : M.even) :

M.shiftUnitHom.oddMap (((S.unitMod.shift.tmulOE M) x) m) = (M.actEE x) m

The structure map on an odd-even generator.

source

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

M.shift ⟶ S.unitMod.shift.tensor M

The inverse of the shift-unit isomorphism: tensor with the algebra unit, which is odd in the shifted unit module. The even component carries a sign, forced by the odd-odd Koszul relator.

Equations

M.shiftUnitInv = { evenMap := -(S.unitMod.shift.tmulOO M) S.one, oddMap := (S.unitMod.shift.tmulOE M) S.one, map_actEE := ⋯, map_actEO := ⋯, map_actOE := ⋯, map_actOO := ⋯ }