The affine toric coaction on complex points

Evaluating the affine coordinate-ring coaction at a complex torus point and an affine complex point recovers the existing character action on the latter. The torus point is represented on the zero-cone coordinate ring by translating its distinguished point. Thus the algebraic coaction and the analytic action use the same characters, without choosing a lattice basis.

References

• W. Fulton, Introduction to Toric Varieties, §2.1.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §3.1.

@[simp]

theorem TauCeti.Toric.affineCoordinateRingCoaction_eval {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) (t : ComplexTorus N) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) : (Algebra.TensorProduct.lift (t • default) x ⋯).comp (affineCoordinateRingCoaction hi σ) = t • x

Evaluating the affine toric coaction against the torus point t and the chart point x gives the existing action t • x on complex points. The torus point is realized in the zero-cone chart as t • default.

theorem TauCeti.Toric.specMap_smul_eq_lift_comp_affineToricSchemeAction {N : Type} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) (t : ComplexTorus N) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) : AlgebraicGeometry.Spec.map (CommRingCat.ofHom (t • x).toRingHom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (t • default).toRingHom)) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom x.toRingHom)) ⋯) (affineToricSchemeAction hi σ)

On complex points, the affine scheme action is the character action. The two points of the action domain are paired by the fibre-product universal property over Spec ℂ.

The comparison is intended for explicit rewrites: applying it again to the translated torus point in the pairing would produce an infinite expansion.

theorem TauCeti.Toric.specMap_smul_eq_lift_comp_affineToricSchemeAction_assoc {N : Type} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) (t : ComplexTorus N) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(MonoidAlgebra ℂ (Multiplicative ↥(dualSemigroup hi σ))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (t • x).toRingHom)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (t • default).toRingHom)) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom x.toRingHom)) ⋯) (CategoryTheory.CategoryStruct.comp (affineToricSchemeAction hi σ) h)

On complex points, the affine scheme action is the character action. The two points of the action domain are paired by the fibre-product universal property over Spec ℂ.

The comparison is intended for explicit rewrites: applying it again to the translated torus point in the pairing would produce an infinite expansion.