Rays of a finite toric fan

A ray of a fan is a one-dimensional cone belonging to the fan. This intrinsic indexing type is finite and agrees, below any cone of the fan, with the rays of that cone. Every nonzero cone of a fan contains a ray; this follows from the generation of a toric cone by its rays.

The global ray type is the natural index for invariant boundary components of a toric variety. Containment of cones is detected by their rays, and any set of rays lying in a simplicial cone is the ray set of one of its faces. These facts determine which boundary components intersect. Fan equivalences transport rays functorially, and the rays of an open subfan embed as exactly the ambient rays whose cones belong to the subfan. These comparisons identify the indices of boundary components under toric isomorphisms and restriction to invariant open subspaces.

Main declarations

• TauCeti.Toric.Fan.Ray: the one-dimensional cones of a fan.
• TauCeti.Toric.Fan.Ray.ofToricRay: a ray of a cone of the fan, viewed as a fan ray.
• TauCeti.Toric.Fan.Ray.toToricRay: a fan ray contained in a cone, viewed as a ray of that cone.
• TauCeti.Toric.Fan.rayEquiv: the equivalence between rays below a cone and its toric rays.
• TauCeti.Toric.Fan.exists_ray_le_of_ne_bot: every nonzero cone of a fan contains a ray.
• TauCeti.Toric.Fan.le_iff_forall_ray_le: containment of cones is detected by their rays.
• TauCeti.Toric.Fan.exists_cone_rays_eq: a collection of rays in a simplicial cone is exactly the ray set of a face.
• TauCeti.Toric.Fan.subfanRayEmbedding: the ambient inclusion of the rays of an open subfan.
• TauCeti.Toric.FanEquiv.rayEquiv: the ray equivalence induced by a fan equivalence.

References

• W. Fulton, Introduction to Toric Varieties, §§1.2 and 3.1.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §§1.2 and 3.2.

@[reducible, inline]

abbrev TauCeti.Toric.Fan.Ray {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) : Type u_2

A ray of a fan is a one-dimensional cone belonging to the fan.

@[reducible, inline]

abbrev TauCeti.Toric.Fan.Ray.toCone {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (rho : Phi.Ray) : ↑Phi.cones

The cone of the fan underlying a fan ray.

@[simp]

theorem TauCeti.Toric.Fan.Ray.finrank_span {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (rho : Phi.Ray) : Module.finrank ℝ ↥(Submodule.span ℝ ↑↑(toCone Phi rho)) = 1

The cone underlying a fan ray has one-dimensional linear span.

def TauCeti.Toric.Fan.Ray.ofToricRay {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (sigma : ↑Phi.cones) (rho : ToricRay ↑sigma) : Phi.Ray

A ray of a cone belonging to a fan is a ray of the fan.

@[simp]

theorem TauCeti.Toric.Fan.Ray.toCone_ofToricRay {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (sigma : ↑Phi.cones) (rho : ToricRay ↑sigma) : ↑(toCone Phi (ofToricRay Phi sigma rho)) = rho.toPointedCone

theorem TauCeti.Toric.Fan.Ray.toCone_ofToricRay_le {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (sigma : ↑Phi.cones) (rho : ToricRay ↑sigma) : toCone Phi (ofToricRay Phi sigma rho) ≤ sigma

A toric ray, viewed as a fan ray, is contained in its original cone.

def TauCeti.Toric.Fan.Ray.toToricRay {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (rho : Phi.Ray) (sigma : ↑Phi.cones) (h : toCone Phi rho ≤ sigma) : ToricRay ↑sigma

A fan ray contained in a cone is a ray of that cone.

@[simp]

theorem TauCeti.Toric.Fan.Ray.toPointedCone_toToricRay {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (rho : Phi.Ray) (sigma : ↑Phi.cones) (h : toCone Phi rho ≤ sigma) : (toToricRay Phi rho sigma h).toPointedCone = ↑(toCone Phi rho)

theorem TauCeti.Toric.Fan.Ray.toCone_ne_bot {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (rho : Phi.Ray) : ↑(toCone Phi rho) ≠ ⊥

A fan ray is not the zero cone.

def TauCeti.Toric.Fan.rayEquiv {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (sigma : ↑Phi.cones) : { rho : Phi.Ray // Ray.toCone Phi rho ≤ sigma } ≃ ToricRay ↑sigma

The fan rays contained in a cone are exactly the toric rays of that cone.

@[simp]

theorem TauCeti.Toric.Fan.rayEquiv_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (sigma : ↑Phi.cones) (rho : { rho : Phi.Ray // Ray.toCone Phi rho ≤ sigma }) : (Phi.rayEquiv sigma) rho = Ray.toToricRay Phi (↑rho) sigma ⋯

The equivalence from fan rays below a cone to its toric rays uses the same underlying cone.

@[simp]

theorem TauCeti.Toric.Fan.rayEquiv_symm_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (sigma : ↑Phi.cones) (rho : ToricRay ↑sigma) : (Phi.rayEquiv sigma).symm rho = ⟨Ray.ofToricRay Phi sigma rho, ⋯⟩

The inverse equivalence views a toric ray as a cone belonging to the fan.

theorem TauCeti.Toric.Fan.exists_ray_le_of_ne_bot {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (sigma : ↑Phi.cones) (hσ : ↑sigma ≠ ⊥) : ∃ (rho : Phi.Ray), Ray.toCone Phi rho ≤ sigma

Every nonzero cone of a fan contains a ray of the fan.

theorem TauCeti.Toric.Fan.le_iff_forall_ray_le {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) {sigma tau : ↑Phi.cones} : sigma ≤ tau ↔ ∀ (rho : Phi.Ray), Ray.toCone Phi rho ≤ sigma → Ray.toCone Phi rho ≤ tau

Containment of fan cones is detected by their rays. No regularity is needed.

theorem TauCeti.Toric.Fan.exists_cone_rays_eq {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) {S : Set Phi.Ray} {sigma : ↑Phi.cones} (hSigma : (↑sigma).IsSimplicial) (hS : ∀ rho ∈ S, Ray.toCone Phi rho ≤ sigma) : ∃ tau ≤ sigma, ∀ (rho : Phi.Ray), Ray.toCone Phi rho ≤ tau ↔ rho ∈ S

Any collection of rays contained in a simplicial cone of a fan is exactly the collection of rays of a face of that cone. This includes the empty collection, which gives the zero cone.

def TauCeti.Toric.Fan.subfanRayEmbedding {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Phi.cones) (hface : ∀ ⦃sigma tau : PointedCone ℝ V⦄, sigma ∈ S → tau.IsFaceOf sigma → tau ∈ S) : (Phi.subfan S hS hface).Ray ↪ Phi.Ray

The rays of an open subfan embed in the rays of the ambient fan without changing cones.

@[simp]

theorem TauCeti.Toric.Fan.toCone_subfanRayEmbedding {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Phi.cones) (hface : ∀ ⦃sigma tau : PointedCone ℝ V⦄, sigma ∈ S → tau.IsFaceOf sigma → tau ∈ S) (rho : (Phi.subfan S hS hface).Ray) : ↑(Ray.toCone Phi ((Phi.subfanRayEmbedding S hS hface) rho)) = ↑(Ray.toCone (Phi.subfan S hS hface) rho)

The ray embedding of a subfan leaves the underlying cone unchanged.

@[simp]

theorem TauCeti.Toric.Fan.range_subfanRayEmbedding {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Phi.cones) (hface : ∀ ⦃sigma tau : PointedCone ℝ V⦄, sigma ∈ S → tau.IsFaceOf sigma → tau ∈ S) : Set.range ⇑(Phi.subfanRayEmbedding S hS hface) = {rho : Phi.Ray | ↑(Ray.toCone Phi rho) ∈ S}

The rays coming from a subfan are exactly the ambient rays whose cones belong to it.

def TauCeti.Toric.FanEquiv.rayEquiv {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Phi : Fan i} {Psi : Fan i'} (e : FanEquiv Phi Psi) : Phi.Ray ≃ Psi.Ray

A fan equivalence identifies the rays of the two fans by transporting their cones.

@[simp]

theorem TauCeti.Toric.FanEquiv.toCone_rayEquiv {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Phi : Fan i} {Psi : Fan i'} (e : FanEquiv Phi Psi) (rho : Phi.Ray) : Fan.Ray.toCone Psi (e.rayEquiv rho) = e.coneEquiv (Fan.Ray.toCone Phi rho)

The ray equivalence transports the underlying cone by the cone equivalence.

@[simp]

theorem TauCeti.Toric.FanEquiv.rayEquiv_symm {N : Type u_1} {N' : Type u_2} {V : Type u_4} {V' : Type u_5} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Phi : Fan i} {Psi : Fan i'} (e : FanEquiv Phi Psi) : e.rayEquiv.symm = e.symm.rayEquiv

The inverse ray equivalence is induced by the inverse fan equivalence.

@[simp]

theorem TauCeti.Toric.FanEquiv.rayEquiv_refl {N : Type u_1} {V : Type u_4} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Phi : Fan i) : (FanEquiv.refl Phi).rayEquiv = Equiv.refl Phi.Ray

The identity fan equivalence induces the identity on rays.

@[simp]

theorem TauCeti.Toric.FanEquiv.rayEquiv_trans {N : Type u_1} {N' : Type u_2} {N'' : Type u_3} {V : Type u_4} {V' : Type u_5} {V'' : Type u_6} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [AddCommGroup V] [AddCommGroup V'] [AddCommGroup V''] [Module ℝ V] [Module ℝ V'] [Module ℝ V''] {i : N →+ V} {i' : N' →+ V'} {i'' : N'' →+ V''} {Phi : Fan i} {Psi : Fan i'} {Omega : Fan i''} (e : FanEquiv Phi Psi) (e' : FanEquiv Psi Omega) : (e.trans e').rayEquiv = e.rayEquiv.trans e'.rayEquiv

Ray transport respects composition of fan equivalences.