Characters on the least target cone #
For a fan morphism, a character nonnegative on the least target cone of a source cone vanishes on the image of the source cone exactly when it vanishes on the least target cone. Indeed, its zero locus cuts out a face of the least target cone, and this face must contain the least cone. This character criterion identifies the image of distinguished points and orbit strata under toric maps without choosing coordinates.
References #
- W. Fulton, Introduction to Toric Varieties, §2.1.
- D. Cox, J. Little and H. Schenck, Toric Varieties, §3.3.
theorem
TauCeti.Toric.FanHom.realCharacter_eq_zero_on_leastCone_iff
{N : Type u_1}
{N' : Type u_2}
{V : Type u_3}
{V' : Type u_4}
[AddCommGroup N]
[AddCommGroup N']
[AddCommGroup V]
[AddCommGroup V']
[Module ℝ V]
[Module ℝ V']
{i : N →+ V}
{i' : N' →+ V'}
{Φ : Fan i}
{Ψ : Fan i'}
(f : FanHom Φ Ψ)
{σ : PointedCone ℝ V}
(hσ : σ ∈ Φ.cones)
{m : N' →+ ℤ}
(hm : m ∈ dualSemigroup ⋯ (f.leastCone hσ))
:
(∀ y ∈ f.leastCone hσ, (⋯.realCharacter m) y = 0) ↔ ∀ x ∈ σ, (⋯.realCharacter (m.comp f.latticeMap)) x = 0
A character nonnegative on the least target cone of σ vanishes on that cone exactly when
its pullback vanishes on σ. Neither fan needs to be regular.