Documentation

TauCeti.Geometry.Toric.Algebraic.Fan.TorusAction.Basic

The torus action on the toric scheme of a fan #

The dense torus T = Spec ℂ[M] of the integral character lattice M acts on every affine toric chart U_σ = Spec ℂ[σ^∨ ∩ M] through the character-grading coaction, and these affine actions commute with restriction to faces (TauCeti.Toric.affineToricSchemeActionFaceMap_comp_action). This file glues them to an action T ×_{Spec ℂ} X_Φ ⟶ X_Φ on the toric scheme X_Φ of a finite fan Φ. No regularity is required.

The fibre product T ×_{Spec ℂ} X_Φ is covered by the open subschemes T ×_{Spec ℂ} U_σ. The affine toric open cover of X_Φ is locally directed, so its pullback along the projection T ×_{Spec ℂ} X_Φ ⟶ X_Φ is a locally directed open cover as well, and morphisms out of T ×_{Spec ℂ} X_Φ glue as soon as they are compatible with the face maps (AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOfLocallyDirected).

Main declarations #

TauCeti.Toric.Fan.algebraicRealizationAction: the torus action on the toric scheme of a fan.
TauCeti.Toric.Fan.algebraicRealizationActionChartMap_comp_algebraicRealizationAction: on T ×_{Spec ℂ} U_σ, it is the affine torus action followed by the chart inclusion.
TauCeti.Toric.Fan.algebraicRealizationActionChartMap_hom_ext: morphisms out of T ×_{Spec ℂ} X_Φ are determined on the charts T ×_{Spec ℂ} U_σ.
TauCeti.Toric.Fan.algebraicRealizationAction_comp_algebraicRealizationStructureMap: the action is a morphism over Spec ℂ.
TauCeti.Toric.Fan.algebraicRealizationUnitSection_comp_algebraicRealizationAction: the identity of the torus acts trivially.
TauCeti.Toric.Fan.algebraicRealizationActionChartMap_comp_algebraicRealizationAction_bot: on the dense torus itself, the action is the multiplication of the torus.

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.

The global torus action #

noncomputable def TauCeti.Toric.Fan.algebraicRealizationActionChartMap {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) :

The product of the dense torus with the affine chart of a cone maps into the product of the dense torus with the toric scheme, by the identity on the torus factor and the chart inclusion on the other factor.

Instances For

@[simp]

theorem TauCeti.Toric.Fan.algebraicRealizationActionChartMap_comp_fst {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) :

The product chart map is the identity on the torus factor.

@[simp]

theorem TauCeti.Toric.Fan.algebraicRealizationActionChartMap_comp_fst_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(affineCoordinateRing ⋯ ⊥) ⟶ Z) :

The product chart map is the identity on the torus factor.

@[simp]

theorem TauCeti.Toric.Fan.algebraicRealizationActionChartMap_comp_snd {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) :

The product chart map is the chart inclusion on the toric-scheme factor.

@[simp]

theorem TauCeti.Toric.Fan.algebraicRealizationActionChartMap_comp_snd_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) {Z : AlgebraicGeometry.Scheme} (h : Φ.algebraicRealization ⟶ Z) :

The product chart map is the chart inclusion on the toric-scheme factor.

noncomputable def TauCeti.Toric.Fan.algebraicRealizationAction {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) :

CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing ⋯ ⊥)))) Φ.algebraicRealizationStructureMap ⟶ Φ.algebraicRealization

The action of the dense torus on the toric scheme of a fan, glued from the affine torus actions on the affine toric charts.

Instances For

@[simp]

theorem TauCeti.Toric.Fan.algebraicRealizationActionChartMap_comp_algebraicRealizationAction {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) :

CategoryTheory.CategoryStruct.comp (algebraicRealizationActionChartMap σ) Φ.algebraicRealizationAction = CategoryTheory.CategoryStruct.comp (affineToricSchemeAction ⋯ ↑σ) (Φ.affineToricChartι σ)

On the product of the dense torus with an affine chart, the torus action on the toric scheme of a fan is the affine torus action followed by the chart inclusion.

@[simp]

theorem TauCeti.Toric.Fan.algebraicRealizationActionChartMap_comp_algebraicRealizationAction_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) {Z : AlgebraicGeometry.Scheme} (h : Φ.algebraicRealization ⟶ Z) :

CategoryTheory.CategoryStruct.comp (algebraicRealizationActionChartMap σ) (CategoryTheory.CategoryStruct.comp Φ.algebraicRealizationAction h) = CategoryTheory.CategoryStruct.comp (affineToricSchemeAction ⋯ ↑σ) (CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) h)

On the product of the dense torus with an affine chart, the torus action on the toric scheme of a fan is the affine torus action followed by the chart inclusion.

theorem TauCeti.Toric.Fan.algebraicRealizationActionChartMap_hom_ext {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} {Y : AlgebraicGeometry.Scheme} {g h : CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing ⋯ ⊥)))) Φ.algebraicRealizationStructureMap ⟶ Y} (H : ∀ (σ : ↑Φ.cones), CategoryTheory.CategoryStruct.comp (algebraicRealizationActionChartMap σ) g = CategoryTheory.CategoryStruct.comp (algebraicRealizationActionChartMap σ) h) :

g = h

Morphisms out of the product of the dense torus with the toric scheme of a fan are determined by their restrictions to the products of the dense torus with the affine charts.

@[simp]

theorem TauCeti.Toric.Fan.affineToricSchemeActionFaceMap_comp_algebraicRealizationActionChartMap {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} {τ σ : ↑Φ.cones} (h : (↑τ).IsFaceOf ↑σ) :

CategoryTheory.CategoryStruct.comp (affineToricSchemeActionFaceMap ⋯ (↑σ) h) (algebraicRealizationActionChartMap σ) = algebraicRealizationActionChartMap τ

Restricting the product of the dense torus with an affine chart to a face is compatible with the inclusions into the product of the dense torus with the toric scheme.

@[simp]

theorem TauCeti.Toric.Fan.affineToricSchemeActionFaceMap_comp_algebraicRealizationActionChartMap_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} {τ σ : ↑Φ.cones} (h : (↑τ).IsFaceOf ↑σ) {Z : AlgebraicGeometry.Scheme} (h✝ : CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing ⋯ ⊥)))) Φ.algebraicRealizationStructureMap ⟶ Z) :

CategoryTheory.CategoryStruct.comp (affineToricSchemeActionFaceMap ⋯ (↑σ) h) (CategoryTheory.CategoryStruct.comp (algebraicRealizationActionChartMap σ) h✝) = CategoryTheory.CategoryStruct.comp (algebraicRealizationActionChartMap τ) h✝

Restricting the product of the dense torus with an affine chart to a face is compatible with the inclusions into the product of the dense torus with the toric scheme.

The torus action on the toric scheme of a fan is a morphism over Spec ℂ.

The torus action on the toric scheme of a fan is a morphism over Spec ℂ.

noncomputable def TauCeti.Toric.Fan.algebraicRealizationActionOver {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) :

CategoryTheory.MonoidalCategoryStruct.tensorObj ((affineToricScheme ⋯ ⊥).asOver (AlgebraicGeometry.Spec ↧ℂ)) (Φ.algebraicRealization.asOver (AlgebraicGeometry.Spec ↧ℂ)) ⟶ Φ.algebraicRealization.asOver (AlgebraicGeometry.Spec ↧ℂ)

The glued torus action as a morphism of schemes over Spec ℂ.

Instances For

theorem TauCeti.Toric.Fan.algebraicRealizationActionOver_left {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) :

CategoryTheory.Over.Hom.left Φ.algebraicRealizationActionOver = Φ.algebraicRealizationAction

Forgetting the base from the action over Spec ℂ gives the glued action morphism.

theorem TauCeti.Toric.Fan.whiskerLeft_affineToricChartι_asOver_left {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) :

CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((affineToricScheme ⋯ ⊥).asOver (AlgebraicGeometry.Spec ↧ℂ)) (AlgebraicGeometry.Scheme.Hom.asOver (Φ.affineToricChartι σ) (AlgebraicGeometry.Spec ↧ℂ))) = algebraicRealizationActionChartMap σ

Tensoring a chart inclusion with the identity on the torus gives the product chart map.

noncomputable def TauCeti.Toric.Fan.algebraicRealizationUnitSection {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) :

Φ.algebraicRealization ⟶ CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing ⋯ ⊥)))) Φ.algebraicRealizationStructureMap

The section of the projection from the product of the dense torus with the toric scheme of a fan, given by the identity point of the dense torus.

Instances For

@[simp]

The torus component of the unit section is the identity point of the dense torus.

@[simp]

theorem TauCeti.Toric.Fan.algebraicRealizationUnitSection_comp_fst_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(affineCoordinateRing ⋯ ⊥) ⟶ Z) :

The torus component of the unit section is the identity point of the dense torus.

@[simp]

theorem TauCeti.Toric.Fan.algebraicRealizationUnitSection_comp_snd {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) :

CategoryTheory.CategoryStruct.comp Φ.algebraicRealizationUnitSection (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing ⋯ ⊥)))) Φ.algebraicRealizationStructureMap) = CategoryTheory.CategoryStruct.id Φ.algebraicRealization

The unit section is a section of the projection to the toric scheme.

@[simp]

theorem TauCeti.Toric.Fan.algebraicRealizationUnitSection_comp_snd_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {Z : AlgebraicGeometry.Scheme} (h : Φ.algebraicRealization ⟶ Z) :

CategoryTheory.CategoryStruct.comp Φ.algebraicRealizationUnitSection (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing ⋯ ⊥)))) Φ.algebraicRealizationStructureMap) h) = h

The unit section is a section of the projection to the toric scheme.

@[simp]

theorem TauCeti.Toric.Fan.affineToricChartι_comp_algebraicRealizationUnitSection {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) :

CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) Φ.algebraicRealizationUnitSection = CategoryTheory.CategoryStruct.comp (affineToricSchemeUnitSection ⋯ ↑σ) (algebraicRealizationActionChartMap σ)

On an affine chart, the unit section of the toric scheme is the unit section of the chart.

@[simp]

theorem TauCeti.Toric.Fan.affineToricChartι_comp_algebraicRealizationUnitSection_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) {Z : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing ⋯ ⊥)))) Φ.algebraicRealizationStructureMap ⟶ Z) :

CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) (CategoryTheory.CategoryStruct.comp Φ.algebraicRealizationUnitSection h) = CategoryTheory.CategoryStruct.comp (affineToricSchemeUnitSection ⋯ ↑σ) (CategoryTheory.CategoryStruct.comp (algebraicRealizationActionChartMap σ) h)

On an affine chart, the unit section of the toric scheme is the unit section of the chart.

@[simp]

theorem TauCeti.Toric.Fan.algebraicRealizationUnitSection_comp_algebraicRealizationAction {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) :

CategoryTheory.CategoryStruct.comp Φ.algebraicRealizationUnitSection Φ.algebraicRealizationAction = CategoryTheory.CategoryStruct.id Φ.algebraicRealization

The identity element of the dense torus acts trivially on the toric scheme of a fan.

@[simp]

theorem TauCeti.Toric.Fan.algebraicRealizationUnitSection_comp_algebraicRealizationAction_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {Z : AlgebraicGeometry.Scheme} (h : Φ.algebraicRealization ⟶ Z) :

CategoryTheory.CategoryStruct.comp Φ.algebraicRealizationUnitSection (CategoryTheory.CategoryStruct.comp Φ.algebraicRealizationAction h) = h

The identity element of the dense torus acts trivially on the toric scheme of a fan.

theorem TauCeti.Toric.Fan.algebraicRealizationActionChartMap_comp_algebraicRealizationAction_bot {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (h : ⊥ ∈ Φ.cones) :

CategoryTheory.CategoryStruct.comp (algebraicRealizationActionChartMap ⟨⊥, h⟩) Φ.algebraicRealizationAction = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.MonObj.mul) (Φ.affineToricChartι ⟨⊥, h⟩)

On the chart of the zero cone, the dense torus, the torus action on the toric scheme of a fan is the multiplication of the dense torus.