The complex torus action on a fan realization

The coordinate-free complex torus acts on each affine chart by multiplication of monomial values. Restriction to a face commutes with this action, so the chart actions glue to an action on the analytic realization. The chart inclusions are equivariant, and the action is jointly continuous for the monomial-embedding topology.

References

• W. Fulton, Introduction to Toric Varieties, §§1.2 and 2.1.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §§3.1–3.2.

@[instance_reducible]

noncomputable instance TauCeti.Toric.Fan.analyticAffineChartMulAction {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : MulAction (ComplexTorus N) ↑(Φ.analyticAffineChartDiagram.obj σ)

The affine chart of a fan inherits the coordinate-free torus action on its complex points.

theorem TauCeti.Toric.Fan.analyticAffineChartDiagram_map_smul {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {τ σ : ↑Φ.cones} (f : τ ⟶ σ) (t : ComplexTorus N) (x : ↑(Φ.analyticAffineChartDiagram.obj τ)) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartDiagram.map f)) (t • x) = t • (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartDiagram.map f)) x

The map between affine charts associated to a face inclusion is equivariant for the coordinate-free complex torus.

@[instance_reducible]

noncomputable instance TauCeti.Toric.Fan.instSMulComplexTorusCarrierAnalyticRealization {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) : SMul (ComplexTorus N) ↑(Φ.analyticRealization hΦ)

The analytic realization carries the torus action obtained by translating chart points.

@[simp]

theorem TauCeti.Toric.Fan.smul_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (t : ComplexTorus N) (σ : ↑Φ.cones) (x : ↑(Φ.analyticAffineChartDiagram.obj σ)) : t • (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) (t • x)

The global action agrees with the affine action in every chart.

@[instance_reducible]

noncomputable instance TauCeti.Toric.Fan.instMulActionComplexTorusCarrierAnalyticRealization {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) : MulAction (ComplexTorus N) ↑(Φ.analyticRealization hΦ)

The glued translations satisfy the group action laws.

instance TauCeti.Toric.Fan.instContinuousSMulComplexTorusCarrierObjElemPointedConeRealConesTopCatAnalyticAffineChartDiagram {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : ContinuousSMul (ComplexTorus N) ↑(Φ.analyticAffineChartDiagram.obj σ)

The coordinate-free torus acts jointly continuously on each analytic affine chart.

instance TauCeti.Toric.Fan.instContinuousSMulComplexTorusCarrierAnalyticRealization {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) : ContinuousSMul (ComplexTorus N) ↑(Φ.analyticRealization hΦ)

The analytic realization carries the continuous action of its complex torus.