Documentation

TauCeti.Geometry.Toric.Algebraic.TorusAction.Coaction

The affine toric coaction #

The coordinate ring of an affine toric chart is graded by the integral character lattice. Its grading gives the coaction of the dense torus: a monomial of character m maps to the monomial of m on the torus tensored with the original monomial. The torus factor is the coordinate ring of the zero cone, so this uses the same dense torus as the fan construction.

We prove the counit and coassociativity identities as equalities of algebra homomorphisms, and equivariance of face restriction. These identities are the coordinate-ring form of the unit and associativity laws for the affine torus action. Face equivariance allows the actions to descend along the affine open immersions used to glue a fan scheme.

The construction uses Mathlib's monoid-algebra comultiplication and tensor-product algebra maps. No rationality, salience, or regularity hypothesis on the cone is needed.

References #

source
noncomputable def TauCeti.Toric.affineCoordinateRingCoaction {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) :
affineCoordinateRing hi σ →ₐ[ℂ] TensorProduct ℂ (affineCoordinateRing hi ⊥) (affineCoordinateRing hi σ)

The coaction of the dense torus on the coordinate ring of an affine toric chart. The first factor is the coordinate ring of the zero cone, and the second is the coordinate ring of the chart.

Instances For
    source
    @[simp]
    theorem TauCeti.Toric.affineCoordinateRingCoaction_single {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) (m : ↥(dualSemigroup hi σ)) (z : ℂ) :
    (affineCoordinateRingCoaction hi σ) (MonoidAlgebra.single (Multiplicative.ofAdd m) z) = MonoidAlgebra.single (Multiplicative.ofAdd ⟨↑m, ⋯⟩) 1 ⊗ₜ[ℂ] MonoidAlgebra.single (Multiplicative.ofAdd m) z

    The torus coaction records the character of a monomial in its first factor and retains the monomial, including its coefficient, in its second factor.

    source
    @[simp]
    theorem TauCeti.Toric.affineCoordinateRingCoaction_counit {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) :
    ((↑(Algebra.TensorProduct.lid ℂ (affineCoordinateRing hi σ))).comp (Algebra.TensorProduct.map (Bialgebra.counitAlgHom ℂ (affineCoordinateRing hi ⊥)) (AlgHom.id ℂ (affineCoordinateRing hi σ)))).comp (affineCoordinateRingCoaction hi σ) = AlgHom.id ℂ (affineCoordinateRing hi σ)

    Evaluation at the identity of the dense torus recovers the original coordinate function.

    source
    theorem TauCeti.Toric.affineCoordinateRingCoaction_coassoc {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) :
    ((↑(Algebra.TensorProduct.assoc ℂ ℂ ℂ (affineCoordinateRing hi ⊥) (affineCoordinateRing hi ⊥) (affineCoordinateRing hi σ))).comp (Algebra.TensorProduct.map (Bialgebra.comulAlgHom ℂ (affineCoordinateRing hi ⊥)) (AlgHom.id ℂ (affineCoordinateRing hi σ)))).comp (affineCoordinateRingCoaction hi σ) = (Algebra.TensorProduct.map (AlgHom.id ℂ (affineCoordinateRing hi ⊥)) (affineCoordinateRingCoaction hi σ)).comp (affineCoordinateRingCoaction hi σ)

    The two ways of coacting twice agree, after the canonical reassociation of the tensor product. This is the coordinate-ring associativity law of the torus action.

    source
    @[simp]
    theorem TauCeti.Toric.affineCoordinateRingCoaction_comp_face {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) {σ τ : PointedCone ℝ V} (hτσ : τ.IsFaceOf σ) :
    (affineCoordinateRingCoaction hi τ).comp (faceAffineCoordinateRingMap hi hτσ) = (Algebra.TensorProduct.map (AlgHom.id ℂ (affineCoordinateRing hi ⊥)) (faceAffineCoordinateRingMap hi hτσ)).comp (affineCoordinateRingCoaction hi σ)

    Restriction to a face is equivariant for the affine torus coactions. In particular, the coactions agree on the coordinate rings of chart overlaps.

    source
    @[simp]
    theorem TauCeti.Toric.affineCoordinateRingCoaction_bot {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) :
    affineCoordinateRingCoaction hi ⊥ = Bialgebra.comulAlgHom ℂ (affineCoordinateRing hi ⊥)

    On the zero cone, the torus coaction is its own multiplication comorphism.

    source
    @[simp]
    theorem TauCeti.Toric.affineCoordinateRingCoaction_comp_map {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {N' : Type u_3} {V' : Type u_4} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} (hi : IsIntegralLattice i) (hi' : IsIntegralLattice i') {σ : PointedCone ℝ V} {τ : PointedCone ℝ V'} (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) :
    (affineCoordinateRingCoaction hi σ).comp (affineCoordinateRingMap hi hi' f g hfg hστ) = (Algebra.TensorProduct.map (affineCoordinateRingMap hi hi' f g hfg ⋯) (affineCoordinateRingMap hi hi' f g hfg hστ)).comp (affineCoordinateRingCoaction hi' τ)

    A map of lattice cones intertwines their coactions and the induced map of dense tori. This is the coordinate-ring equivariance law for affine toric morphisms.