The residue module of a complex point

A complex point of a super-commutative algebra makes the complex numbers, concentrated in even degree, a module over that algebra: the even part acts through the point and the odd part acts by zero, which is consistent exactly because a point kills the products of two odd elements.

noncomputable def RS.SuperCommAlgebra.pointMod {S : SuperCommAlgebra} (P : SuperPoint S) : S.Mod

The residue module of a complex point: the complex numbers in even degree and zero in odd degree, with the even part of the algebra acting through the point.

Equations

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