The affine toric scheme action map

The grading coaction of an affine toric coordinate ring gives a morphism from the product of the dense torus and the affine toric scheme to the affine toric scheme. The product is the fibre product over Spec ℂ, identified with the spectrum of the tensor product of coordinate rings. This is the affine action map that the global fan-scheme action glues along face opens. Compatible maps of lattice cones induce maps between the two action domains and intertwine the affine actions.

The defining equation on the tensor-product affine chart keeps the construction tied to the coordinate-ring coaction, whose counit, coassociativity, and face-compatibility laws are proved in Coaction.

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.

noncomputable def TauCeti.Toric.affineToricSchemeAction {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ)))) ⟶ affineToricScheme hi σ

The affine toric scheme action induced by the character-grading coaction. The dense torus acts on the affine chart via the common base Spec ℂ.

@[simp]

theorem TauCeti.Toric.pullbackSpecIso_inv_comp_affineToricSchemeAction {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso ℂ (affineCoordinateRing hi ⊥) (affineCoordinateRing hi σ)).inv (affineToricSchemeAction hi σ) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (affineCoordinateRingCoaction hi σ).toRingHom)

On the tensor-product affine chart, the scheme action is Spec of the toric coaction.

@[simp]

theorem TauCeti.Toric.pullbackSpecIso_inv_comp_affineToricSchemeAction_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {Z : AlgebraicGeometry.Scheme} (h : affineToricScheme hi σ ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso ℂ (affineCoordinateRing hi ⊥) (affineCoordinateRing hi σ)).inv (CategoryTheory.CategoryStruct.comp (affineToricSchemeAction hi σ) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (affineCoordinateRingCoaction hi σ).toRingHom)) h

On the tensor-product affine chart, the scheme action is Spec of the toric coaction.

theorem TauCeti.Toric.affineToricSchemeAction_comp_specMap_algebraMap {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : CategoryTheory.CategoryStruct.comp (affineToricSchemeAction hi σ) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))

The affine torus action is a morphism over Spec ℂ: it commutes with the projections of its source and target to Spec ℂ.

theorem TauCeti.Toric.affineToricSchemeAction_comp_specMap_algebraMap_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧ℂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineToricSchemeAction hi σ) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ)))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ)))) h)

The affine torus action is a morphism over Spec ℂ: it commutes with the projections of its source and target to Spec ℂ.

Naturality

noncomputable def TauCeti.Toric.affineToricSchemeActionMap {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {N' : Type} {V' : Type u_2} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} (hi' : IsIntegralLattice i') {τ : PointedCone ℝ V'} (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) : CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ)))) ⟶ CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' τ))))

A compatible map of lattice cones induces the product map from the source torus action domain to the target torus action domain. Its two factors are the induced dense-torus map and the induced affine toric morphism.

@[simp]

theorem TauCeti.Toric.affineToricSchemeActionMap_comp_fst {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {N' : Type} {V' : Type u_2} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} (hi' : IsIntegralLattice i') {τ : PointedCone ℝ V'} (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionMap hi σ hi' f g hfg hστ) (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' τ))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) (affineToricSchemeMap hi hi' f g hfg ⋯)

The product map on action domains has the induced dense-torus map as its first projection.

@[simp]

theorem TauCeti.Toric.affineToricSchemeActionMap_comp_fst_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {N' : Type} {V' : Type u_2} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} (hi' : IsIntegralLattice i') {τ : PointedCone ℝ V'} (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(affineCoordinateRing hi' ⊥) ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionMap hi σ hi' f g hfg hστ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' τ))))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) (CategoryTheory.CategoryStruct.comp (affineToricSchemeMap hi hi' f g hfg ⋯) h)

The product map on action domains has the induced dense-torus map as its first projection.

@[simp]

theorem TauCeti.Toric.affineToricSchemeActionMap_comp_snd {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {N' : Type} {V' : Type u_2} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} (hi' : IsIntegralLattice i') {τ : PointedCone ℝ V'} (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionMap hi σ hi' f g hfg hστ) (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' τ))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) (affineToricSchemeMap hi hi' f g hfg hστ)

The product map on action domains has the induced affine toric morphism as its second projection.

@[simp]

theorem TauCeti.Toric.affineToricSchemeActionMap_comp_snd_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {N' : Type} {V' : Type u_2} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} (hi' : IsIntegralLattice i') {τ : PointedCone ℝ V'} (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(affineCoordinateRing hi' τ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionMap hi σ hi' f g hfg hστ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' τ))))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) (CategoryTheory.CategoryStruct.comp (affineToricSchemeMap hi hi' f g hfg hστ) h)

The product map on action domains has the induced affine toric morphism as its second projection.

theorem TauCeti.Toric.pullbackSpecIso_inv_comp_affineToricSchemeActionMap {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {N' : Type} {V' : Type u_2} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} (hi' : IsIntegralLattice i') {τ : PointedCone ℝ V'} (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso ℂ (affineCoordinateRing hi ⊥) (affineCoordinateRing hi σ)).inv (affineToricSchemeActionMap hi σ hi' f g hfg hστ) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.map (affineCoordinateRingMap hi hi' f g hfg ⋯) (affineCoordinateRingMap hi hi' f g hfg hστ)).toRingHom)) (AlgebraicGeometry.pullbackSpecIso ℂ (affineCoordinateRing hi' ⊥) (affineCoordinateRing hi' τ)).inv

In tensor-product coordinates, the product map on action domains is Spec of the tensor product of the two coordinate-ring maps.

theorem TauCeti.Toric.pullbackSpecIso_inv_comp_affineToricSchemeActionMap_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {N' : Type} {V' : Type u_2} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} (hi' : IsIntegralLattice i') {τ : PointedCone ℝ V'} (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) {Z : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi' τ)))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso ℂ (affineCoordinateRing hi ⊥) (affineCoordinateRing hi σ)).inv (CategoryTheory.CategoryStruct.comp (affineToricSchemeActionMap hi σ hi' f g hfg hστ) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.map (affineCoordinateRingMap hi hi' f g hfg ⋯) (affineCoordinateRingMap hi hi' f g hfg hστ)).toRingHom)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso ℂ (affineCoordinateRing hi' ⊥) (affineCoordinateRing hi' τ)).inv h)

In tensor-product coordinates, the product map on action domains is Spec of the tensor product of the two coordinate-ring maps.

theorem TauCeti.Toric.affineToricSchemeActionMap_comp_action {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {N' : Type} {V' : Type u_2} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} (hi' : IsIntegralLattice i') {τ : PointedCone ℝ V'} (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionMap hi σ hi' f g hfg hστ) (affineToricSchemeAction hi' τ) = CategoryTheory.CategoryStruct.comp (affineToricSchemeAction hi σ) (affineToricSchemeMap hi hi' f g hfg hστ)

Affine toric morphisms intertwine the dense-torus actions induced by their lattice maps.

theorem TauCeti.Toric.affineToricSchemeActionMap_comp_action_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {N' : Type} {V' : Type u_2} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} (hi' : IsIntegralLattice i') {τ : PointedCone ℝ V'} (f : N →+ N') (g : V →ₗ[ℝ] V') (hfg : ∀ (n : N), g (i n) = i' (f n)) (hστ : Set.MapsTo ⇑g ↑σ ↑τ) {Z : AlgebraicGeometry.Scheme} (h : affineToricScheme hi' τ ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionMap hi σ hi' f g hfg hστ) (CategoryTheory.CategoryStruct.comp (affineToricSchemeAction hi' τ) h) = CategoryTheory.CategoryStruct.comp (affineToricSchemeAction hi σ) (CategoryTheory.CategoryStruct.comp (affineToricSchemeMap hi hi' f g hfg hστ) h)

Affine toric morphisms intertwine the dense-torus actions induced by their lattice maps.

theorem TauCeti.Toric.affineToricSchemeAction_bot {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) : affineToricSchemeAction hi ⊥ = CategoryTheory.Over.Hom.left CategoryTheory.MonObj.mul

For the zero cone, the affine action is multiplication of the dense torus scheme.

noncomputable def TauCeti.Toric.affineToricSchemeUnitSection {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : affineToricScheme hi σ ⟶ CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))

The unit of the dense torus, paired with the identity of the affine chart, defines a section of the torus-times-chart projection.

@[simp]

theorem TauCeti.Toric.affineToricSchemeUnitSection_comp_snd {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : CategoryTheory.CategoryStruct.comp (affineToricSchemeUnitSection hi σ) (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) = CategoryTheory.CategoryStruct.id (affineToricScheme hi σ)

The unit section has the identity as its projection to the affine chart.

@[simp]

theorem TauCeti.Toric.affineToricSchemeUnitSection_comp_snd_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(affineCoordinateRing hi σ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineToricSchemeUnitSection hi σ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) h) = h

The unit section has the identity as its projection to the affine chart.

@[simp]

theorem TauCeti.Toric.affineToricSchemeUnitSection_comp_fst {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : CategoryTheory.CategoryStruct.comp (affineToricSchemeUnitSection hi σ) (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Bialgebra.counitAlgHom ℂ (affineCoordinateRing hi ⊥)).toRingHom))

The projection of the unit section to the dense torus is the identity section after the structure map to Spec ℂ.

@[simp]

theorem TauCeti.Toric.affineToricSchemeUnitSection_comp_fst_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(affineCoordinateRing hi ⊥) ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineToricSchemeUnitSection hi σ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ)))) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Bialgebra.counitAlgHom ℂ (affineCoordinateRing hi ⊥)).toRingHom)) h)

The projection of the unit section to the dense torus is the identity section after the structure map to Spec ℂ.

@[simp]

theorem TauCeti.Toric.affineToricSchemeUnitSection_comp_action {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : CategoryTheory.CategoryStruct.comp (affineToricSchemeUnitSection hi σ) (affineToricSchemeAction hi σ) = CategoryTheory.CategoryStruct.id (affineToricScheme hi σ)

The identity element of the dense torus acts trivially on an affine toric scheme.

@[simp]

theorem TauCeti.Toric.affineToricSchemeUnitSection_comp_action_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {Z : AlgebraicGeometry.Scheme} (h : affineToricScheme hi σ ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineToricSchemeUnitSection hi σ) (CategoryTheory.CategoryStruct.comp (affineToricSchemeAction hi σ) h) = h

The identity element of the dense torus acts trivially on an affine toric scheme.

noncomputable def TauCeti.Toric.affineToricSchemeActionFaceMap {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {τ : PointedCone ℝ V} (hτσ : τ.IsFaceOf σ) : CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi τ)))) ⟶ CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))

Restricting an affine toric chart to a face induces the corresponding map on its product with the dense torus. On tensor-product coordinate rings it is the identity on the torus factor and face restriction on the chart factor.

@[simp]

theorem TauCeti.Toric.affineToricSchemeActionFaceMap_comp_fst {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {τ : PointedCone ℝ V} (hτσ : τ.IsFaceOf σ) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionFaceMap hi σ hτσ) (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi τ))))

Face restriction leaves the dense-torus projection of the product unchanged.

@[simp]

theorem TauCeti.Toric.affineToricSchemeActionFaceMap_comp_fst_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {τ : PointedCone ℝ V} (hτσ : τ.IsFaceOf σ) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(affineCoordinateRing hi ⊥) ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionFaceMap hi σ hτσ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi τ))))) h

Face restriction leaves the dense-torus projection of the product unchanged.

@[simp]

theorem TauCeti.Toric.affineToricSchemeActionFaceMap_comp_snd {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {τ : PointedCone ℝ V} (hτσ : τ.IsFaceOf σ) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionFaceMap hi σ hτσ) (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi τ))))) (faceAffineToricSchemeMap hi hτσ)

On the affine-chart projection, the product map is face restriction.

@[simp]

theorem TauCeti.Toric.affineToricSchemeActionFaceMap_comp_snd_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {τ : PointedCone ℝ V} (hτσ : τ.IsFaceOf σ) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(affineCoordinateRing hi σ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionFaceMap hi σ hτσ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ))))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi τ))))) (CategoryTheory.CategoryStruct.comp (faceAffineToricSchemeMap hi hτσ) h)

On the affine-chart projection, the product map is face restriction.

@[simp]

theorem TauCeti.Toric.affineToricSchemeActionFaceMap_id {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) : affineToricSchemeActionFaceMap hi σ ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi ⊥)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing hi σ)))))

The product map of a reflexive face inclusion is the identity.

@[simp]

theorem TauCeti.Toric.affineToricSchemeActionFaceMap_comp {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {υ τ : PointedCone ℝ V} (hυτ : υ.IsFaceOf τ) (hτσ : τ.IsFaceOf σ) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionFaceMap hi τ hυτ) (affineToricSchemeActionFaceMap hi σ hτσ) = affineToricSchemeActionFaceMap hi σ ⋯

Product maps of face inclusions compose as the underlying face maps do.

theorem TauCeti.Toric.affineToricSchemeActionFaceMap_comp_pullbackSpecIso {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {τ : PointedCone ℝ V} (hτσ : τ.IsFaceOf σ) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionFaceMap hi σ hτσ) (AlgebraicGeometry.pullbackSpecIso ℂ (affineCoordinateRing hi ⊥) (affineCoordinateRing hi σ)).hom = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso ℂ (affineCoordinateRing hi ⊥) (affineCoordinateRing hi τ)).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.map (AlgHom.id ℂ (affineCoordinateRing hi ⊥)) (faceAffineCoordinateRingMap hi hτσ)).toRingHom))

In tensor-product coordinates, the product face map acts as the identity on the torus factor and as face restriction on the chart factor.

theorem TauCeti.Toric.affineToricSchemeActionFaceMap_comp_pullbackSpecIso_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {τ : PointedCone ℝ V} (hτσ : τ.IsFaceOf σ) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(TensorProduct ℂ (affineCoordinateRing hi ⊥) (affineCoordinateRing hi σ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionFaceMap hi σ hτσ) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso ℂ (affineCoordinateRing hi ⊥) (affineCoordinateRing hi σ)).hom h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso ℂ (affineCoordinateRing hi ⊥) (affineCoordinateRing hi τ)).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.map (AlgHom.id ℂ (affineCoordinateRing hi ⊥)) (faceAffineCoordinateRingMap hi hτσ)).toRingHom)) h)

In tensor-product coordinates, the product face map acts as the identity on the torus factor and as face restriction on the chart factor.

theorem TauCeti.Toric.affineToricSchemeActionFaceMap_comp_action {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {τ : PointedCone ℝ V} (hτσ : τ.IsFaceOf σ) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionFaceMap hi σ hτσ) (affineToricSchemeAction hi σ) = CategoryTheory.CategoryStruct.comp (affineToricSchemeAction hi τ) (faceAffineToricSchemeMap hi hτσ)

The affine torus action commutes with restriction to a face. This square is the scheme-level compatibility used to glue the affine actions across the fan's open overlaps.

theorem TauCeti.Toric.affineToricSchemeActionFaceMap_comp_action_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (σ : PointedCone ℝ V) {τ : PointedCone ℝ V} (hτσ : τ.IsFaceOf σ) {Z : AlgebraicGeometry.Scheme} (h : affineToricScheme hi σ ⟶ Z) : CategoryTheory.CategoryStruct.comp (affineToricSchemeActionFaceMap hi σ hτσ) (CategoryTheory.CategoryStruct.comp (affineToricSchemeAction hi σ) h) = CategoryTheory.CategoryStruct.comp (affineToricSchemeAction hi τ) (CategoryTheory.CategoryStruct.comp (faceAffineToricSchemeMap hi hτσ) h)

The affine torus action commutes with restriction to a face. This square is the scheme-level compatibility used to glue the affine actions across the fan's open overlaps.