Torus action and character naturality of the algebraic–analytic toric comparison

The coordinate-free complex torus ComplexTorus N acts on the affine complex points of each cone through the algebraic coordinate-ring coaction (TauCeti.Toric.affineCoordinateRingCoaction_eval). Because face localizations are equivariant for this coaction, the affine actions glue to a continuous torus action on the complex points Φ.AlgebraicComplexPoint of the toric scheme of any finite fan Φ, without assuming regularity.

For a regular fan, the chartwise algebraic–analytic comparison algebraicAnalyticEquiv is the identity on every affine chart, so it is torus-equivariant. Moreover:

• toric maps of algebraic complex points are equivariant for the torus homomorphism induced by the lattice map, and on the canonical dense torus inclusion they agree with that homomorphism;
• global character functions on algebraic complex points agree with analyticCharacter through the comparison, transform by their character under torus translation, and pull back along fan morphisms by precomposing with the lattice map;
• for a nonempty regular fan, compactness of Φ.AlgebraicComplexPoint is equivalent to completeness of Φ.

Main declarations

• TauCeti.Toric.Fan.AlgebraicComplexPoint.instMulActionComplexTorus: the glued torus action on the complex points of the toric scheme of a fan.
• TauCeti.Toric.Fan.AlgebraicComplexPoint.coe_smul: this action on complex points is induced by the scheme-level torus action algebraicRealizationAction.
• TauCeti.Toric.Fan.continuousSMul_algebraicComplexPoint and TauCeti.Toric.Fan.contMDiffSMul_complexTorus_algebraicComplexPoint: joint continuity and holomorphy of the torus action on algebraic complex points of a regular fan.
• TauCeti.Toric.Fan.algebraicAnalyticEquiv_smul and TauCeti.Toric.Fan.algebraicAnalyticEquiv_symm_smul: torus equivariance of the algebraic–analytic comparison.
• TauCeti.Toric.Fan.AlgebraicComplexPoint.torusι: the canonical dense-torus inclusion into the complex points of a nonempty fan scheme, intertwined with analyticTorusι by TauCeti.Toric.Fan.algebraicAnalyticEquiv_torusι.
• TauCeti.Toric.Fan.AlgebraicComplexPoint.character: the global character function on algebraic complex points, holomorphic on regular fans and intertwined with analyticCharacter by TauCeti.Toric.Fan.analyticCharacter_algebraicAnalyticEquiv.
• TauCeti.Toric.Fan.AlgebraicComplexPoint.coneOrbit and TauCeti.Toric.Fan.AlgebraicComplexPoint.boundaryComponent: the orbit strata and ray-indexed boundary components on algebraic complex points, matched with their analytic counterparts by TauCeti.Toric.Fan.image_algebraicAnalyticEquiv_coneOrbit and TauCeti.Toric.Fan.image_algebraicAnalyticEquiv_boundaryComponent.
• TauCeti.Toric.Fan.compactSpace_algebraicComplexPoint_iff_isComplete: for a nonempty regular fan, compactness of Φ.AlgebraicComplexPoint is equivalent to completeness of Φ.

References

• W. Fulton, Introduction to Toric Varieties, §§1.3–1.4, 2.1 and 2.4.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §§1.1, 3.1 and 3.4.

@[instance_reducible]

noncomputable instance TauCeti.Toric.Fan.AlgebraicComplexPoint.instSMulComplexTorus {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} : SMul (ComplexTorus N) Φ.AlgebraicComplexPoint

The coordinate-free complex torus acts on the complex points of the toric scheme of a fan by translating affine chart representatives.

@[simp]

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.smul_ofAffinePoint {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (t : ComplexTorus N) (σ : ↑Φ.cones) (x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ)) : t • ofAffinePoint σ x = ofAffinePoint σ (t • x)

Every affine chart inclusion into the complex points of the toric scheme is equivariant for the coordinate-free complex torus.

@[simp]

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.coe_smul {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (t : ComplexTorus N) (p : Φ.AlgebraicComplexPoint) : ↑(t • p) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (t • default).toRingHom)) ↑p ⋯) Φ.algebraicRealizationAction

The chartwise action on complex points is induced by the scheme-level torus action algebraicRealizationAction. The torus point and scheme point are paired by the fibre-product universal property over Spec ℂ.

@[instance_reducible]

noncomputable instance TauCeti.Toric.Fan.AlgebraicComplexPoint.instMulActionComplexTorus {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} : MulAction (ComplexTorus N) Φ.AlgebraicComplexPoint

The glued torus translations on algebraic complex points satisfy the group action laws.

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.continuous_const_smul {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (t : ComplexTorus N) : Continuous fun (p : Φ.AlgebraicComplexPoint) => t • p

Translation by a fixed torus element is continuous on algebraic complex points.

instance TauCeti.Toric.Fan.AlgebraicComplexPoint.instContinuousConstSMulComplexTorus {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} : ContinuousConstSMul (ComplexTorus N) Φ.AlgebraicComplexPoint

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

The distinguished complex point of a cone σ in the toric scheme: the image of the distinguished point of the top face of σ in the affine chart of σ.

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.distinguishedPoint_def {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) : distinguishedPoint σ = ofAffinePoint σ (Toric.distinguishedPoint ⋯ ⊤)

The distinguished point of a cone is the image of the distinguished point of its top face.

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.ofAffinePoint_distinguishedPoint {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} {τ σ : ↑Φ.cones} (h : τ ≤ σ) : ofAffinePoint σ (Toric.distinguishedPoint ⋯ (Φ.orbitFace h)) = distinguishedPoint τ

A face inclusion in the fan sends the distinguished point of the face to itself in the larger chart.

noncomputable def TauCeti.Toric.Fan.AlgebraicComplexPoint.torusι {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ0 : Nonempty ↑Φ.cones) (t : ComplexTorus N) : Φ.AlgebraicComplexPoint

The canonical inclusion of the coordinate-free complex torus into the complex points of the toric scheme of a nonempty fan, obtained by translating the distinguished point of the zero cone.

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.torusι_def {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ0 : Nonempty ↑Φ.cones) (t : ComplexTorus N) : torusι hΦ0 t = t • distinguishedPoint ⟨⊥, ⋯⟩

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.torusι_eq_ofAffinePoint {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ0 : Nonempty ↑Φ.cones) (σ : ↑Φ.cones) (t : ComplexTorus N) : torusι hΦ0 t = ofAffinePoint σ (t • default)

In every affine chart, the canonical torus inclusion is translation of the point default where every monomial takes the value 1.

@[simp]

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.torusι_one {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ0 : Nonempty ↑Φ.cones) : torusι hΦ0 1 = distinguishedPoint ⟨⊥, ⋯⟩

@[simp]

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.torusι_mul {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ0 : Nonempty ↑Φ.cones) (s t : ComplexTorus N) : torusι hΦ0 (s * t) = s • torusι hΦ0 t

Global character functions on algebraic complex points

noncomputable def TauCeti.Toric.Fan.AlgebraicComplexPoint.character {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) : C(Φ.AlgebraicComplexPoint, ℂ)

An integral character m nonnegative on every cone of a fan defines a continuous function on the complex points of the toric scheme, evaluating each affine chart point on the monomial of m.

@[simp]

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.character_ofAffinePoint {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) (σ : ↑Φ.cones) (x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ)) : (character Φ m hm) (ofAffinePoint σ x) = x (MonoidAlgebra.single (Multiplicative.ofAdd ⟨m, ⋯⟩) 1)

On every affine chart, the algebraic character function evaluates the point at the corresponding monomial.

@[simp]

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.character_smul {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) (t : ComplexTorus N) (p : Φ.AlgebraicComplexPoint) : (character Φ m hm) (t • p) = ↑(t m) * (character Φ m hm) p

Character functions on algebraic complex points transform by their character under torus translation.

@[simp]

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.character_zero {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (p : Φ.AlgebraicComplexPoint) : (character Φ 0 ⋯) p = 1

The zero character defines the constant function 1 on algebraic complex points.

@[simp]

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.character_add {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (m m' : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) (hm' : ∀ (σ : ↑Φ.cones), m' ∈ dualSemigroup ⋯ ↑σ) (p : Φ.AlgebraicComplexPoint) : (character Φ (m + m') ⋯) p = (character Φ m hm) p * (character Φ m' hm') p

Addition of characters corresponds to multiplication of their functions on algebraic complex points.

@[simp]

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.character_torusι {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) (hΦ0 : Nonempty ↑Φ.cones) (t : ComplexTorus N) : (character Φ m hm) (torusι hΦ0 t) = ↑(t m)

On the canonical dense-torus inclusion, the global character function restricts to evaluation of the character.

Orbit strata and boundary components on algebraic complex points

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

The torus orbit of a cone σ in the complex points of the toric scheme: the image of the stratum of the top face of σ in the affine chart of σ.

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.coneOrbit_def {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) : coneOrbit Φ σ = ofAffinePoint σ '' affineConeOrbit ⋯ ⊤

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.distinguishedPoint_mem_coneOrbit {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (σ : ↑Φ.cones) : distinguishedPoint σ ∈ coneOrbit Φ σ

The distinguished point of a cone lies in its algebraic orbit.

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.smul_mem_coneOrbit {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} {σ : ↑Φ.cones} (t : ComplexTorus N) {p : Φ.AlgebraicComplexPoint} (hp : p ∈ coneOrbit Φ σ) : t • p ∈ coneOrbit Φ σ

The torus preserves the algebraic orbit of every cone.

noncomputable def TauCeti.Toric.Fan.AlgebraicComplexPoint.boundaryComponent {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (ρ : Φ.Ray) : Set Φ.AlgebraicComplexPoint

The boundary component indexed by a ray in the complex points of the toric scheme: the closure of the torus orbit of that ray.

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.boundaryComponent_def {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (ρ : Φ.Ray) : boundaryComponent Φ ρ = closure (coneOrbit Φ (Ray.toCone Φ ρ))

theorem TauCeti.Toric.Fan.AlgebraicComplexPoint.isClosed_boundaryComponent {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (ρ : Φ.Ray) : IsClosed (boundaryComponent Φ ρ)

Comparison with the analytic realization of a regular fan

@[simp]

theorem TauCeti.Toric.Fan.algebraicAnalyticEquiv_smul {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (t : ComplexTorus N) (p : Φ.AlgebraicComplexPoint) : (algebraicAnalyticEquiv hΦ) (t • p) = t • (algebraicAnalyticEquiv hΦ) p

The algebraic–analytic comparison is equivariant for the coordinate-free complex torus.

@[simp]

theorem TauCeti.Toric.Fan.algebraicAnalyticEquiv_symm_smul {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (t : ComplexTorus N) (x : ↑(Φ.analyticRealization hΦ)) : (algebraicAnalyticEquiv hΦ).symm (t • x) = t • (algebraicAnalyticEquiv hΦ).symm x

The inverse algebraic–analytic comparison is equivariant for the coordinate-free complex torus.

@[simp]

theorem TauCeti.Toric.Fan.algebraicAnalyticHomeomorph_smul {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (t : ComplexTorus N) (p : Φ.AlgebraicComplexPoint) : (algebraicAnalyticHomeomorph hΦ) (t • p) = t • (algebraicAnalyticHomeomorph hΦ) p

The algebraic–analytic homeomorphism is equivariant for the coordinate-free complex torus.

theorem TauCeti.Toric.Fan.continuousSMul_algebraicComplexPoint {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) : ContinuousSMul (ComplexTorus N) Φ.AlgebraicComplexPoint

For a regular fan, the complex torus acts jointly continuously on algebraic complex points.

@[simp]

theorem TauCeti.Toric.Fan.algebraicAnalyticEquiv_distinguishedPoint {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : (algebraicAnalyticEquiv hΦ) (AlgebraicComplexPoint.distinguishedPoint σ) = Φ.analyticDistinguishedPoint hΦ σ

The algebraic–analytic comparison carries the distinguished point of every cone to its analytic distinguished point.

@[simp]

theorem TauCeti.Toric.Fan.algebraicAnalyticEquiv_symm_analyticDistinguishedPoint {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : (algebraicAnalyticEquiv hΦ).symm (Φ.analyticDistinguishedPoint hΦ σ) = AlgebraicComplexPoint.distinguishedPoint σ

The inverse algebraic–analytic comparison carries the analytic distinguished point of every cone to its algebraic distinguished point.

@[simp]

theorem TauCeti.Toric.Fan.algebraicAnalyticEquiv_torusι {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (hΦ0 : Nonempty ↑Φ.cones) (t : ComplexTorus N) : (algebraicAnalyticEquiv hΦ) (AlgebraicComplexPoint.torusι hΦ0 t) = Φ.analyticTorusι hΦ hΦ0 t

The algebraic–analytic comparison intertwines the canonical dense-torus inclusions.

@[simp]

theorem TauCeti.Toric.Fan.algebraicAnalyticEquiv_symm_analyticTorusι {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (hΦ0 : Nonempty ↑Φ.cones) (t : ComplexTorus N) : (algebraicAnalyticEquiv hΦ).symm (Φ.analyticTorusι hΦ hΦ0 t) = AlgebraicComplexPoint.torusι hΦ0 t

The inverse algebraic–analytic comparison intertwines the canonical dense-torus inclusions.

@[simp]

theorem TauCeti.Toric.Fan.analyticCharacter_algebraicAnalyticEquiv {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) (p : Φ.AlgebraicComplexPoint) : (Φ.analyticCharacter hΦ m hm) ((algebraicAnalyticEquiv hΦ) p) = (AlgebraicComplexPoint.character Φ m hm) p

The global character function on algebraic complex points agrees with analyticCharacter through the algebraic–analytic comparison.

@[simp]

theorem TauCeti.Toric.Fan.character_algebraicAnalyticEquiv_symm {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) (x : ↑(Φ.analyticRealization hΦ)) : (AlgebraicComplexPoint.character Φ m hm) ((algebraicAnalyticEquiv hΦ).symm x) = (Φ.analyticCharacter hΦ m hm) x

Pulling back AlgebraicComplexPoint.character along the inverse comparison recovers analyticCharacter.

theorem TauCeti.Toric.Fan.contMDiff_character_algebraicComplexPoint {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) (n : WithTop ℕ∞) : ContMDiff (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) (modelWithCornersSelf ℂ ℂ) n ⇑(AlgebraicComplexPoint.character Φ m hm)

On a regular fan, the global character function on algebraic complex points is holomorphic.

theorem TauCeti.Toric.Fan.contMDiffSMul_complexTorus_algebraicComplexPoint {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) {ι : Type u_1} [Fintype ι] (e : IntegralCharacter N ≃+ (ι →₀ ℤ)) (n : WithTop ℕ∞) : have x := complexTorusChartedSpace e; ContMDiffSMul (modelWithCornersSelf ℂ (ι → ℂ)) (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) n (ComplexTorus N) Φ.AlgebraicComplexPoint

For a regular fan, the complex torus acts holomorphically on algebraic complex points.

@[simp]

theorem TauCeti.Toric.Fan.image_algebraicAnalyticEquiv_coneOrbit {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : ⇑(algebraicAnalyticEquiv hΦ) '' AlgebraicComplexPoint.coneOrbit Φ σ = Φ.analyticConeOrbit hΦ σ

The algebraic–analytic comparison carries the algebraic orbit of each cone onto its analytic cone orbit.

@[simp]

theorem TauCeti.Toric.Fan.preimage_algebraicAnalyticEquiv_analyticConeOrbit {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : ⇑(algebraicAnalyticEquiv hΦ) ⁻¹' Φ.analyticConeOrbit hΦ σ = AlgebraicComplexPoint.coneOrbit Φ σ

The preimage of the analytic orbit of a cone under the comparison is its algebraic orbit.

theorem TauCeti.Toric.Fan.coneOrbit_eq_orbit {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : AlgebraicComplexPoint.coneOrbit Φ σ = MulAction.orbit (ComplexTorus N) (AlgebraicComplexPoint.distinguishedPoint σ)

For a regular fan, the algebraic orbit of a cone σ is the torus orbit of its distinguished point.

@[simp]

theorem TauCeti.Toric.Fan.image_algebraicAnalyticEquiv_boundaryComponent {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (ρ : Φ.Ray) : ⇑(algebraicAnalyticEquiv hΦ) '' AlgebraicComplexPoint.boundaryComponent Φ ρ = Φ.analyticBoundaryComponent hΦ ρ

The algebraic–analytic comparison carries the algebraic boundary component of each ray onto its analytic boundary component.

@[simp]

theorem TauCeti.Toric.Fan.preimage_algebraicAnalyticEquiv_analyticBoundaryComponent {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (ρ : Φ.Ray) : ⇑(algebraicAnalyticEquiv hΦ) ⁻¹' Φ.analyticBoundaryComponent hΦ ρ = AlgebraicComplexPoint.boundaryComponent Φ ρ

The preimage of the analytic boundary component of a ray under the comparison is its algebraic boundary component.

theorem TauCeti.Toric.Fan.compactSpace_algebraicComplexPoint_iff_isComplete {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (hΦ0 : Nonempty ↑Φ.cones) : CompactSpace Φ.AlgebraicComplexPoint ↔ Φ.IsComplete

For a nonempty regular fan, the space of algebraic complex points is compact if and only if the fan is complete.

@[simp]

theorem TauCeti.Toric.FanHom.algebraicComplexPointMap_smul {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {N' V' : Type} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (t : ComplexTorus N) (p : Φ.AlgebraicComplexPoint) : f.algebraicComplexPointMap (t • p) = (complexTorusMap f.latticeMap) t • f.algebraicComplexPointMap p

The map on algebraic complex points induced by a fan morphism is equivariant for the torus homomorphism induced by its lattice map.

@[simp]

theorem TauCeti.Toric.FanHom.algebraicComplexPointMap_torusι {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {N' V' : Type} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ0 : Nonempty ↑Φ.cones) (t : ComplexTorus N) : f.algebraicComplexPointMap (Fan.AlgebraicComplexPoint.torusι hΦ0 t) = Fan.AlgebraicComplexPoint.torusι ⋯ ((complexTorusMap f.latticeMap) t)

On the canonical dense-torus inclusion, the map on algebraic complex points is the torus homomorphism induced by the lattice map.

@[simp]

theorem TauCeti.Toric.FanHom.character_algebraicComplexPointMap {N V : Type} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {N' V' : Type} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (m : IntegralCharacter N') (hm : ∀ (τ : ↑Ψ.cones), m ∈ dualSemigroup ⋯ ↑τ) (p : Φ.AlgebraicComplexPoint) : (Fan.AlgebraicComplexPoint.character Ψ m hm) (f.algebraicComplexPointMap p) = (Fan.AlgebraicComplexPoint.character Φ (AddMonoidHom.comp m f.latticeMap) ⋯) p

Pullback of a global character function on algebraic complex points along a fan morphism precomposes the character with the integral lattice map.