Documentation

TauCeti.Geometry.Toric.Analytic.Fan.Boundary.Basic

Boundary components of an analytic toric fan realization #

For a nonempty regular fan, the orbit of the zero cone is the dense torus. Each ray of the fan determines a closed invariant boundary component: the closure of its torus orbit. The orbit--cone correspondence identifies this component with the union of the orbits indexed by cones containing the ray.

These ray-indexed components form a finite family, and their union is exactly the complement of the dense torus. On an affine chart, the component of a ray contained in the chart's cone is the closure of the corresponding affine orbit; a ray not contained in the chart has empty preimage. This is the intrinsic topological description underlying the later coordinate-hyperplane and simple-normal-crossings descriptions.

Main declarations #

References #

source
noncomputable def TauCeti.Toric.Fan.analyticBoundaryComponent {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (rho : Phi.Ray) :
Set ↑(Phi.analyticRealization hPhi)

The boundary component indexed by a ray is the closure of the corresponding torus orbit.

Instances For
    source
    theorem TauCeti.Toric.Fan.analyticBoundaryComponent_def {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (rho : Phi.Ray) :
    Phi.analyticBoundaryComponent hPhi rho = closure (Phi.analyticConeOrbit hPhi (Ray.toCone Phi rho))

    A boundary component is the closure of the orbit indexed by its ray.

    source
    theorem TauCeti.Toric.Fan.isClosed_analyticBoundaryComponent {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (rho : Phi.Ray) :
    IsClosed (Phi.analyticBoundaryComponent hPhi rho)

    Every analytic boundary component is closed.

    source
    theorem TauCeti.Toric.Fan.mem_analyticBoundaryComponent_iff {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) {rho : Phi.Ray} {sigma : ↑Phi.cones} {x : ↑(Phi.analyticRealization hPhi)} (hx : x ∈ Phi.analyticConeOrbit hPhi sigma) :
    x ∈ Phi.analyticBoundaryComponent hPhi rho ↔ Ray.toCone Phi rho ≤ sigma

    A point in the orbit of sigma belongs to the component indexed by rho exactly when the ray is a face of sigma.

    source
    @[simp]
    theorem TauCeti.Toric.Fan.smul_mem_analyticBoundaryComponent_iff {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (rho : Phi.Ray) (t : ComplexTorus N) (x : ↑(Phi.analyticRealization hPhi)) :
    t • x ∈ Phi.analyticBoundaryComponent hPhi rho ↔ x ∈ Phi.analyticBoundaryComponent hPhi rho

    Torus translation preserves every analytic boundary component.

    source
    theorem TauCeti.Toric.Fan.analyticBoundaryComponent_eq_iUnion {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (rho : Phi.Ray) :
    Phi.analyticBoundaryComponent hPhi rho = ⋃ sigma ∈ Set.Ici (Ray.toCone Phi rho), Phi.analyticConeOrbit hPhi sigma

    The component of a ray is the union of the orbits indexed by cones containing that ray.

    source
    theorem TauCeti.Toric.Fan.preimage_analyticAffineChartι_analyticBoundaryComponent {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) {rho : Phi.Ray} {sigma : ↑Phi.cones} (h : Ray.toCone Phi rho ≤ sigma) :
    ⇑(CategoryTheory.ConcreteCategory.hom (Phi.analyticAffineChartι hPhi sigma)) ⁻¹' Phi.analyticBoundaryComponent hPhi rho = closure (affineConeOrbit ⋯ (Phi.orbitFace h))

    In a chart whose cone contains rho, the preimage of the boundary component is the closure of the affine orbit of rho, viewed as a face of the chart cone.

    source
    theorem TauCeti.Toric.Fan.preimage_analyticAffineChartι_analyticBoundaryComponent_of_not_le {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) {rho : Phi.Ray} {sigma : ↑Phi.cones} (h : ¬Ray.toCone Phi rho ≤ sigma) :
    ⇑(CategoryTheory.ConcreteCategory.hom (Phi.analyticAffineChartι hPhi sigma)) ⁻¹' Phi.analyticBoundaryComponent hPhi rho = ∅

    A boundary component has empty preimage in a chart whose cone does not contain its ray.

    source
    theorem TauCeti.Toric.Fan.iUnion_analyticBoundaryComponent {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (hPhi : Phi.IsRegular) (hPhi0 : Nonempty ↑Phi.cones) :
    ⋃ (rho : Phi.Ray), Phi.analyticBoundaryComponent hPhi rho = (Phi.analyticDenseTorus hPhi hPhi0)ᶜ

    The union of the ray-indexed boundary components is exactly the complement of the dense torus.