The internal torus action on a fan scheme

The glued torus morphism is an internal action in schemes over Spec ℂ. Its associativity is checked on the affine cone opens, where the coordinate-ring coaction supplies the action laws through the monoidal spectrum functor. The affine chart inclusions are equivariant. No regularity or nonemptiness assumption on the fan is needed.

The construction uses CategoryTheory.Functor.modObjObj and Mathlib's monoidal algSpec.

References

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

@[instance_reducible]

noncomputable instance TauCeti.Toric.Fan.algebraicRealizationModObj {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : CategoryTheory.ModObj ((affineToricScheme ⋯ ⊥).asOver (AlgebraicGeometry.Spec ↧ℂ)) (Φ.algebraicRealization.asOver (AlgebraicGeometry.Spec ↧ℂ))

The dense torus acts on the fan scheme over Spec ℂ by the glued affine torus actions.

theorem TauCeti.Toric.Fan.algebraicRealizationModObj_smul {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : CategoryTheory.ModObj.smul = Φ.algebraicRealizationActionOver

The internal action is the existing glued torus morphism over Spec ℂ.

theorem TauCeti.Toric.Fan.isModHom_affineToricChartι {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : CategoryTheory.IsModHom ((affineToricScheme ⋯ ⊥).asOver (AlgebraicGeometry.Spec ↧ℂ)) (AlgebraicGeometry.Scheme.Hom.asOver (Φ.affineToricChartι σ) (AlgebraicGeometry.Spec ↧ℂ))

The affine chart inclusions intertwine the coaction-induced affine action and the global torus action, as morphisms of schemes over Spec ℂ.