The even ring acting on the odd part, and ℂ-points

The ordinary commutative ℂ-algebra structure of the even component of a RS.SuperCommAlgebra, and the nilness of the odd-generated ideal, are established in SuperRealize.lean (instCommRingEven, instAlgebraEven, oddIdeal_le_nilradical, oddIdeal_ne_top). This module adds the two things Deligne's §4.5 ending consumes on top of them.

• The odd component is a module over the even ring (instModuleEvenOdd), the action being the even-odd multiplication block, compatibly with the ambient ℂ-action (instIsScalarTowerComplexEvenOdd, instSMulCommClassComplexEvenOdd); the odd-odd block is bilinear for that action (mulOO_smul_left, mulOO_smul_right), which is what makes oddIdeal the image of the odd part under multiplication rather than merely its span.

• RS.SuperPoint — a super-algebra map to ℂ concentrated in even degree: a ℂ-algebra map off the even component killing every product of two odd elements. Such a map is exactly a ℂ-algebra map off the odd-nil quotient (SuperPoint.toQuotient, SuperPoint.ofQuotient), so on a nonzero algebra of finite type one exists (nonempty_superPoint), by the Nullstellensatz input RS.exists_algHom_complex of NullPoint.lean.

The odd component as a module over the even ring

@[instance_reducible]

instance RS.SuperCommAlgebra.instModuleEvenOdd (S : SuperCommAlgebra) : Module S.even S.odd

The odd component is a module over the even ring, the action being the even-odd multiplication block: the module axioms are the unit law one_mul_o, the associativity pattern assoc_eeo and the ℂ-bilinearity of the block.

Equations

• S.instModuleEvenOdd = { smul := fun (x : S.even) (u : S.odd) => (S.mulEO x) u, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

instance RS.SuperCommAlgebra.instIsScalarTowerComplexEvenOdd (S : SuperCommAlgebra) : IsScalarTower ℂ S.even S.odd

The scalar actions of ℂ and of the even ring on the odd component are compatible: the even-odd block is ℂ-linear in its even argument.

instance RS.SuperCommAlgebra.instSMulCommClassComplexEvenOdd (S : SuperCommAlgebra) : SMulCommClass ℂ S.even S.odd

The two scalar actions on the odd component commute: the even-odd block is ℂ-linear in its odd argument.

theorem RS.SuperCommAlgebra.mulOO_smul_left (S : SuperCommAlgebra) (x : S.even) (u v : S.odd) : (S.mulOO (x • u)) v = x * (S.mulOO u) v

The odd-odd block is linear over the even ring in its left argument.

theorem RS.SuperCommAlgebra.mulOO_smul_right (S : SuperCommAlgebra) (x : S.even) (u v : S.odd) : (S.mulOO u) (x • v) = x * (S.mulOO u) v

The odd-odd block is linear over the even ring in its right argument.

Nilness of the odd products, in ring form

theorem RS.SuperCommAlgebra.mulOO_mem_oddIdeal (S : SuperCommAlgebra) (u v : S.odd) : (S.mulOO u) v ∈ S.oddIdeal

Each generator of the odd-generated ideal lies in it.

ℂ-points concentrated in even degree

structure RS.SuperPoint (S : SuperCommAlgebra) : Type u

A ℂ-point of a super-commutative ℂ-algebra: a map of super-algebras to ℂ, which carries no odd component, so it is a ℂ-algebra map off the even part annihilating every product of two odd elements.

• chi : S.even →ₐ[ℂ] ℂ

  The ℂ-algebra map on the even component.

• vanishing (u v : S.odd) : self.chi ((S.mulOO u) v) = 0

  The odd degree is killed: products of odd elements go to zero.

theorem RS.SuperPoint.apply_eq_zero_of_mem_oddIdeal {S : SuperCommAlgebra} (P : SuperPoint S) {x : S.even} (hx : x ∈ S.oddIdeal) : P.chi x = 0

A point annihilates the whole odd-generated ideal, not only its generators.

noncomputable def RS.SuperPoint.toQuotient {S : SuperCommAlgebra} (P : SuperPoint S) : S.even ⧸ S.oddIdeal →ₐ[ℂ] ℂ

A point factors through the odd-nil quotient.

Equations

• P.toQuotient = Ideal.Quotient.liftₐ S.oddIdeal P.chi ⋯

noncomputable def RS.SuperPoint.ofQuotient (S : SuperCommAlgebra) (f : S.even ⧸ S.oddIdeal →ₐ[ℂ] ℂ) : SuperPoint S

A ℂ-algebra map off the odd-nil quotient is a point.

Equations

• RS.SuperPoint.ofQuotient S f = { chi := f.comp (Ideal.Quotient.mkₐ ℂ S.oddIdeal), vanishing := ⋯ }

theorem RS.nonempty_superPoint (S : SuperCommAlgebra) [Nontrivial S.even] [Algebra.FiniteType ℂ (S.even ⧸ S.oddIdeal)] : Nonempty (SuperPoint S)

Existence of a ℂ-point (Deligne §4.5, step (ii)): a super-commutative ℂ-algebra with nonzero even part whose odd-nil quotient is of finite type admits a ℂ-point. The quotient is a nonzero ordinary commutative ℂ-algebra of finite type (SuperCommAlgebra.nontrivial_quotient_oddIdeal), so the Nullstellensatz gives it a ℂ-algebra map to ℂ, which pulls back along the quotient map.