Documentation

TauCeti.Geometry.Toric.Analytic.Fan.Map.Subdivision

Proper analytic maps from fan subdivisions #

A subdivision of finite fans induces a toric map in the direction from the subdividing fan to the original fan. When both fans are regular, the corresponding analytic map is proper. Indeed, the real-linear map is the identity and each cone of the original fan is covered by the cones of the subdivision which it contains, so the cone-by-cone properness criterion applies.

In particular, the star subdivision of a regular cone along a nonempty set of its rays induces a proper analytic map to the realization of the fan of faces of the cone, the blow-down map, and so does the star subdivision of a regular fan along a nonzero cone of the fan. The preimage of the orbit closure of that cone under the blow-down map, the exceptional divisor, is the boundary component of the ray through the sum of the primitive generators of its rays.

Main declarations #

References #

source
theorem TauCeti.Toric.Fan.IsSubdivision.isProperMap_analyticMap {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ Ψ : Fan i} (h : Φ.IsSubdivision Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) :
IsProperMap ⇑(CategoryTheory.ConcreteCategory.hom (h.toFanHom.analyticMap hΦ hΨ))

The analytic toric map induced by a subdivision of regular fans is proper. No nonemptiness hypothesis is needed: for empty fans the properness conclusion follows from the sufficient half of the cone-by-cone criterion.

source
theorem TauCeti.Toric.Fan.isProperMap_analyticMap_starSubdivision {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτ : IsRegularCone i τ) {A : Finset (ToricRay τ)} (hA : A.Nonempty) :
IsProperMap ⇑(CategoryTheory.ConcreteCategory.hom (⋯.toFanHom.analyticMap ⋯ ⋯))

The star subdivision of a regular cone τ along a nonempty set A of its rays induces a proper analytic map to the realization of the fan of faces of τ, because the two fans have the same support.

source
theorem TauCeti.Toric.Fan.isProperMap_analyticMap_starSubdivisionAlong {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) (hσ0 : σ ≠ ⊥) :
IsProperMap ⇑(CategoryTheory.ConcreteCategory.hom (⋯.toFanHom.analyticMap ⋯ hΦ))

The star subdivision of a regular fan Φ along a nonzero cone σ of Φ induces a proper analytic map to the realization of Φ, because the two fans have the same support.

source
theorem TauCeti.Toric.Fan.preimage_analyticMap_closure_analyticConeOrbit_starSubdivisionAlong {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) (hσ0 : σ ≠ ⊥) :
⇑(CategoryTheory.ConcreteCategory.hom (⋯.toFanHom.analyticMap ⋯ hΦ)) ⁻¹' closure (Φ.analyticConeOrbit hΦ ⟨σ, hσ⟩) = (Φ.starSubdivisionAlong hΦ hσ).analyticBoundaryComponent ⋯ (Φ.starSubdivisionAlongRay hΦ hσ hσ0)

The exceptional divisor of the blow-down map of the star subdivision of a regular fan Φ along a nonzero cone σ: the preimage of the orbit closure of σ is the boundary component of the ray through the sum of the primitive generators of the rays of σ.