Orbit strata under face localization #
If τ is a face of σ, every face F of τ is also a face of σ, and the restriction of
complex points along the face inclusion maps the stratum of F in the affine chart of τ into
the stratum of F in the affine chart of σ. In particular it maps distinguished points to
distinguished points. These are the compatibilities that let the affine orbit strata of the cones
of a fan be glued into torus orbits of the fan realization.
Main declarations #
TauCeti.Toric.faceAffinePointMap_mem_affineConeOrbit: face localization preserves strata.TauCeti.Toric.faceAffinePointMap_distinguishedPoint: face localization preserves distinguished points.
References #
- W. Fulton, Introduction to Toric Varieties, §3.1.
- D. Cox, J. Little and H. Schenck, Toric Varieties, §3.2.
theorem
TauCeti.Toric.faceAffinePointMap_mem_affineConeOrbit
{N : Type u_1}
{V : Type u_2}
[AddCommGroup N]
[AddCommGroup V]
[Module ℝ V]
{i : N →+ V}
{σ τ : PointedCone ℝ V}
(hi : IsIntegralLattice i)
(hτσ : τ.IsFaceOf σ)
{F : τ.Face}
{G : σ.Face}
(hFG : ↑F = ↑G)
{x : AffineSemigroupComplexPoint ↥(dualSemigroup hi τ)}
(hx : x ∈ affineConeOrbit hi F)
:
Restriction along a face inclusion τ ≼ σ maps the stratum of a face F of τ into the
stratum of the same cone F, viewed as a face G of σ.
theorem
TauCeti.Toric.faceAffinePointMap_distinguishedPoint
{N : Type u_1}
{V : Type u_2}
[AddCommGroup N]
[AddCommGroup V]
[Module ℝ V]
{i : N →+ V}
{σ τ : PointedCone ℝ V}
(hi : IsIntegralLattice i)
(hτσ : τ.IsFaceOf σ)
{F : τ.Face}
{G : σ.Face}
(hFG : ↑F = ↑G)
:
Restriction along a face inclusion τ ≼ σ sends the distinguished point of a face F of τ
to the distinguished point of the same cone F, viewed as a face G of σ.