Internal actions from the toric coaction

The coordinate-ring coaction is an internal action in the opposite category of complex algebras. Its unit and associativity laws are the counit and coassociativity identities of the coaction. Face restrictions are equivariant morphisms of these internal actions.

This packaging allows a lax monoidal functor, in particular the spectrum functor, to transport the action and its laws together. No regularity or finite-generation assumption on the cone is needed.

References

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

@[instance_reducible]

noncomputable def TauCeti.Toric.affineCoordinateRingCoactionModObj {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : CategoryTheory.ModObj (Opposite.op ↧(affineCoordinateRing hi ⊥)) (Opposite.op ↧(affineCoordinateRing hi σ))

The toric coaction as an internal action of the zero-cone monoid object on the cone algebra, in the opposite category of complex algebras.

@[simp]

theorem TauCeti.Toric.affineCoordinateRingCoactionModObj_smul {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : CategoryTheory.ModObj.smul = (CommAlgCat.ofHom (affineCoordinateRingCoaction hi σ)).op

The internal action has precisely the toric coaction as its comorphism.

theorem TauCeti.Toric.isModHom_faceAffineCoordinateRingMap {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) {σ τ : PointedCone ℝ V} (hτσ : τ.IsFaceOf σ) : CategoryTheory.IsModHom (Opposite.op ↧(affineCoordinateRing hi ⊥)) (CommAlgCat.ofHom (faceAffineCoordinateRingMap hi hτσ)).op

Restriction to a face is a morphism of internal torus actions.

@[simp]

theorem TauCeti.Toric.affineCoordinateRingCoactionModObj_bot {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) : affineCoordinateRingCoactionModObj hi ⊥ = CategoryTheory.ModObj.regular (Opposite.op ↧(affineCoordinateRing hi ⊥))

On the zero cone, the internal torus action is the regular action on itself.