Orbit and affine-chart preimages under toric maps

The analytic map of a morphism of regular fans sends the distinguished point of a source cone to that of its least target cone. Equivariance then sends the whole source orbit into the orbit of that cone. It need not map onto the target orbit: the induced torus homomorphism need not be surjective.

The orbit partition gives exact preimage formulas. The preimage of a target orbit is the union of the source orbits whose least target cone is that cone, and the preimage of its closure is the union of those whose least target cone contains that cone; the preimage of an affine chart is the union of the source orbits whose cones map into its cone. These formulas include empty fans and provide the cone-by-cone description needed for restrictions and properness.

References

• W. Fulton, Introduction to Toric Varieties, §2.1 and §2.4.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §3.3.

theorem TauCeti.Toric.FanHom.analyticChartMap_distinguishedPoint {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) {σ : ↑Φ.cones} {τ : ↑Ψ.cones} (h : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑τ) : (CategoryTheory.ConcreteCategory.hom (f.analyticChartMap h)) (distinguishedPoint ⋯ ⊤) = distinguishedPoint ⋯ (Ψ.orbitFace ⋯)

Mapping the distinguished point of a source cone into any containing target chart gives that of the least target cone, viewed as a face of the chosen target cone.

@[simp]

theorem TauCeti.Toric.FanHom.analyticMap_analyticDistinguishedPoint {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) (σ : ↑Φ.cones) : (CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) (Φ.analyticDistinguishedPoint hΦ σ) = Ψ.analyticDistinguishedPoint hΨ ⟨f.leastCone ⋯, ⋯⟩

Analytic toric maps send distinguished points to the distinguished points of the least target cones.

theorem TauCeti.Toric.FanHom.mapsTo_analyticConeOrbit {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) (σ : ↑Φ.cones) : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ))) (Φ.analyticConeOrbit hΦ σ) (Ψ.analyticConeOrbit hΨ ⟨f.leastCone ⋯, ⋯⟩)

The orbit of a source cone maps into the orbit of its least target cone. No surjectivity of the lattice map or its torus homomorphism is required.

theorem TauCeti.Toric.FanHom.analyticMap_mem_analyticConeOrbit_iff {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) {σ : ↑Φ.cones} {τ : ↑Ψ.cones} {x : ↑(Φ.analyticRealization hΦ)} (hx : x ∈ Φ.analyticConeOrbit hΦ σ) : (CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) x ∈ Ψ.analyticConeOrbit hΨ τ ↔ f.leastCone ⋯ = ↑τ

On the orbit of σ, membership of the image in the orbit of τ is equivalent to τ being the least target cone of σ.

theorem TauCeti.Toric.FanHom.preimage_analyticMap_analyticConeOrbit {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) (τ : ↑Ψ.cones) : ⇑(CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) ⁻¹' Ψ.analyticConeOrbit hΨ τ = ⋃ (σ : ↑Φ.cones), ⋃ (_ : f.leastCone ⋯ = ↑τ), Φ.analyticConeOrbit hΦ σ

The preimage of a target orbit is exactly the union of the source orbits with that least target cone.

theorem TauCeti.Toric.FanHom.preimage_analyticMap_closure_analyticConeOrbit {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) (τ : ↑Ψ.cones) : ⇑(CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) ⁻¹' closure (Ψ.analyticConeOrbit hΨ τ) = ⋃ (σ : ↑Φ.cones), ⋃ (_ : ↑τ ≤ f.leastCone ⋯), Φ.analyticConeOrbit hΦ σ

The preimage of the closure of a target orbit is exactly the union of the source orbits whose least target cone contains that cone.

theorem TauCeti.Toric.FanHom.analyticMap_mem_range_analyticAffineChartι_iff {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) {σ : ↑Φ.cones} {τ : ↑Ψ.cones} {x : ↑(Φ.analyticRealization hΦ)} (hx : x ∈ Φ.analyticConeOrbit hΦ σ) : (CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Ψ.analyticAffineChartι hΨ τ)) ↔ f.leastCone ⋯ ≤ ↑τ

On a source orbit, membership of the image in a target affine chart is precisely containment of the least target cone in the chart's cone.

theorem TauCeti.Toric.FanHom.preimage_analyticMap_range_analyticAffineChartι {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) (τ : ↑Ψ.cones) : ⇑(CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Ψ.analyticAffineChartι hΨ τ)) = ⋃ (σ : ↑Φ.cones), ⋃ (_ : PointedCone.map f.realMap ↑σ ≤ ↑τ), Φ.analyticConeOrbit hΦ σ

The preimage of an affine target chart is the union of the source orbits whose cones map into its cone.