Star subdivisions of regular cones and regular fans

Let τ be a regular cone with primitive ray generators u_ρ, and let A be a finite set of rays of τ, spanning the face σ of τ. The star subdivision of the fan of faces of τ along σ uses the ray through u_A = ∑ ρ ∈ A, u_ρ, which is a new ray when A contains at least two rays; for A = {ρ} it is ρ itself, since then u_A = u_ρ. Indexing the generators u_ρ by some ρ and u_A by none, its cones are the cones spanned by the generators indexed by a set S of indices which omits some ρ for some ρ ∈ A. Equivalently, they are the faces of τ not containing σ, and the cones spanned by such a face together with u_A.

Replacing a generator u_ρ with ρ ∈ A by u_A is a unimodular change of an integral basis extending the primitive generators of τ, so every cone of the star subdivision is regular. The only linear relations between the generators come from u_A = ∑ ρ ∈ A, u_ρ. So the conical coefficients of a point of two cones of the star subdivision agree, up to adding a common multiple of that relation, which must vanish since each cone omits a generator indexed by A. Hence two cones meet in the cone of the intersection of their index sets, a face of both. When A is nonempty, the star subdivision covers τ: subtracting from the coefficients of a point of τ the least coefficient at a ray of A, and putting it on u_A, writes the point as a conical combination omitting a generator indexed by A. So it subdivides the fan of faces of τ.

The construction of the fan and its face arguments are adapted from those of TauCeti.Toric.Fan.projectiveSpace in TauCeti.Geometry.Toric.Algebraic.Fan.ProjectiveSpace.Basic.

Classically, the toric variety of the star subdivision is the blow-up of the affine toric variety of τ along the orbit closure of σ.

The star subdivision of a regular fan Φ along one of its cones σ is glued from these local pieces. It keeps the cones of Φ not containing σ, and replaces each cone τ of Φ containing σ by the star subdivision of τ along the rays of σ. These local pieces are compatible: on a face τ₀ of τ containing σ, the star subdivision of τ restricts to that of τ₀, and a face of τ not containing σ is already a cone of the star subdivision of τ. So two cones of the glued family meet in a face of each, inside the intersection of the cones of Φ containing them. When σ is nonzero, every cone τ containing σ is covered by its local piece, so the result subdivides Φ.

A cone of the star subdivision contains the ray through u_σ exactly when the least cone of Φ containing it contains σ. Indeed, a face of σ containing u_σ contains every u_ρ, so is σ; and a cone omitting u_σ is a cone of Φ not containing σ. This identifies the cones of the star subdivision lying over the cones containing σ, which describes the exceptional divisor of the blow-down. Dually, the cones of the star subdivision lying over the cones of Φ not containing σ are exactly those cones themselves, so away from the exceptional divisor the blow-down changes nothing.

Main declarations

• TauCeti.Toric.starSubdivisionGenerator: the ray generators of the star subdivision.
• TauCeti.Toric.starSubdivisionCone: the cone spanned by the generators indexed by a set.
• TauCeti.Toric.starSubdivisionCone_inf: two cones of the star subdivision meet in the cone of the intersection of their index sets.
• TauCeti.Toric.isRegularCone_starSubdivisionCone: every cone of the star subdivision is regular.
• TauCeti.Toric.starSubdivisionCone_eq_faceOrderIso_symm: a cone of the star subdivision whose index set omits none is a face of the cone.
• TauCeti.Toric.Fan.starSubdivision: the star subdivision of the fan of faces of a regular cone.
• TauCeti.Toric.Fan.isRegular_starSubdivision: it is regular.
• TauCeti.Toric.Fan.starSubdivision_isSubdivision: for nonempty A it subdivides the fan of faces of the cone.
• TauCeti.Toric.Fan.inf_mem_starSubdivision_cones: the star subdivision of a regular cone along rays of a face restricts to the star subdivision of that face.
• TauCeti.Toric.Fan.starSubdivisionAlong: the star subdivision of a regular fan along one of its cones, with TauCeti.Toric.Fan.mem_starSubdivisionAlong_cones describing its cones.
• TauCeti.Toric.Fan.isRegular_starSubdivisionAlong and TauCeti.Toric.Fan.starSubdivisionAlong_isSubdivision: it is regular, and for a nonzero cone it subdivides the fan.
• TauCeti.Toric.Fan.starSubdivisionAlong_ofCone: on the fan of faces of a regular cone it is the star subdivision of the cone along the rays of the face.
• TauCeti.Toric.Fan.starSubdivisionAlongRay: for nonzero σ, the ray of the star subdivision through u_σ.
• TauCeti.Toric.Fan.starSubdivisionAlongRay_le_starSubdivisionCone: a cone of the star subdivision of a cone τ ⊇ σ whose generators include u_σ contains the ray through u_σ.
• TauCeti.Toric.Fan.starSubdivisionAlongRay_le_iff_le_leastCone: a cone of the star subdivision contains this ray exactly when the least cone of Φ containing it contains σ.
• TauCeti.Toric.Fan.not_le_leastCone_starSubdivisionAlong_iff: the cones of the star subdivision lying over the cones of Φ not containing σ are those cones themselves.

References

• W. Fulton, Introduction to Toric Varieties, §§1.4 and 2.4.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §3.3, Definition 3.3.13 and Proposition 3.3.15.

The ray generators and cones

noncomputable def TauCeti.Toric.starSubdivisionGenerator {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsToricCone i τ) (k : Option (ToricRay τ)) : N

The ray generators of the star subdivision of a toric cone τ along the rays in A: the primitive generator of ρ at some ρ, and the sum of the primitive generators of the rays in A at none.

@[simp]

theorem TauCeti.Toric.starSubdivisionGenerator_none {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsToricCone i τ) : starSubdivisionGenerator hi A hτ none = ∑ ρ ∈ A, primitiveGenerator hi hτ ρ

@[simp]

theorem TauCeti.Toric.starSubdivisionGenerator_some {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsToricCone i τ) (ρ : ToricRay τ) : starSubdivisionGenerator hi A hτ (some ρ) = primitiveGenerator hi hτ ρ

noncomputable def TauCeti.Toric.starSubdivisionCone {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsToricCone i τ) (S : Set (Option (ToricRay τ))) : PointedCone ℝ V

The cone of the star subdivision of τ along the rays in A spanned by the generators indexed by S. It is a cone of the star subdivision when S omits some ρ for some ρ ∈ A.

theorem TauCeti.Toric.starSubdivisionCone_def {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsToricCone i τ) (S : Set (Option (ToricRay τ))) : starSubdivisionCone hi A hτ S = PointedCone.hull ℝ (⇑i '' starSubdivisionGenerator hi A hτ '' S)

theorem TauCeti.Toric.mem_starSubdivisionCone_iff {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsToricCone i τ) [Fintype (ToricRay τ)] {S : Set (Option (ToricRay τ))} {x : V} : x ∈ starSubdivisionCone hi A hτ S ↔ ∃ (c : Option (ToricRay τ) → ℝ), (∀ k ∉ S, c k = 0) ∧ (∀ (k : Option (ToricRay τ)), 0 ≤ c k) ∧ ∑ k : Option (ToricRay τ), c k • i (starSubdivisionGenerator hi A hτ k) = x

A point lies in the cone of the star subdivision indexed by S exactly when it is a nonnegative combination of the ray generators with coefficients vanishing outside S.

theorem TauCeti.Toric.starSubdivisionCone_mono {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsToricCone i τ) {S T : Set (Option (ToricRay τ))} (h : S ⊆ T) : starSubdivisionCone hi A hτ S ≤ starSubdivisionCone hi A hτ T

theorem TauCeti.Toric.starSubdivisionGenerator_mem {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsToricCone i τ) (k : Option (ToricRay τ)) : i (starSubdivisionGenerator hi A hτ k) ∈ τ

Every ray generator of the star subdivision of τ lies in τ.

theorem TauCeti.Toric.starSubdivisionCone_le {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsToricCone i τ) (S : Set (Option (ToricRay τ))) : starSubdivisionCone hi A hτ S ≤ τ

Every cone of the star subdivision of τ lies in τ.

@[simp]

theorem TauCeti.Toric.starSubdivisionGenerator_map_faceEmbedding {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτ : IsToricCone i τ) {τ₀ : PointedCone ℝ V} (h : τ₀.IsFaceOf τ) (B : Finset (ToricRay τ₀)) (k : Option (ToricRay τ₀)) : starSubdivisionGenerator hi (Finset.map (ToricRay.faceEmbedding h) B) hτ (Option.map (⇑(ToricRay.faceEmbedding h)) k) = starSubdivisionGenerator hi B ⋯ k

Viewing a set B of rays of a face τ₀ of τ as rays of τ does not change the ray generators of the star subdivision along B.

theorem TauCeti.Toric.linearIndepOn_starSubdivisionGenerator {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsToricCone i τ) (hli : LinearIndependent ℝ fun (ρ : ToricRay τ) => i (primitiveGenerator hi hτ ρ)) {S : Set (Option (ToricRay τ))} (hS : ∃ ρ ∈ A, some ρ ∉ S) : LinearIndepOn ℝ (fun (k : Option (ToricRay τ)) => i (starSubdivisionGenerator hi A hτ k)) S

If the primitive ray generators of a toric cone are linearly independent, then any family of ray generators of its star subdivision omitting a generator indexed by A is linearly independent over the reals.

theorem TauCeti.Toric.starSubdivisionCone_inf {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsToricCone i τ) (hli : LinearIndependent ℝ fun (ρ : ToricRay τ) => i (primitiveGenerator hi hτ ρ)) {S T : Set (Option (ToricRay τ))} (hS : ∃ ρ ∈ A, some ρ ∉ S) (hT : ∃ ρ ∈ A, some ρ ∉ T) : starSubdivisionCone hi A hτ S ⊓ starSubdivisionCone hi A hτ T = starSubdivisionCone hi A hτ (S ∩ T)

If the primitive ray generators of a toric cone are linearly independent, then two cones of its star subdivision, each omitting a generator indexed by A, meet in the cone of the intersection of their index sets.

theorem TauCeti.Toric.isRegularCone_starSubdivisionCone {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsRegularCone i τ) {S : Set (Option (ToricRay τ))} (hS : ∃ ρ ∈ A, some ρ ∉ S) : IsRegularCone i (starSubdivisionCone hi A ⋯ S)

A cone of the star subdivision of a regular cone omitting a generator indexed by A is regular: replacing that generator by the sum of the generators of A in an integral basis extending the primitive generators of τ gives another integral basis.

theorem TauCeti.Toric.starSubdivisionCone_eq_faceOrderIso_symm {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsRegularCone i τ) {S : Set (Option (ToricRay τ))} (hS : none ∉ S) : starSubdivisionCone hi A ⋯ S = ↑((IsRegularCone.faceOrderIso hi hτ).symm {ρ : ToricRay τ | some ρ ∈ S})

A cone of the star subdivision of a regular cone τ whose index set omits none is the face of τ spanned by the rays it indexes.

theorem TauCeti.Toric.isFaceOf_starSubdivisionCone {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsRegularCone i τ) {S : Set (Option (ToricRay τ))} (hS : none ∉ S) : (starSubdivisionCone hi A ⋯ S).IsFaceOf τ

A cone of the star subdivision of a regular cone τ whose index set omits none is a face of τ.

The fan

noncomputable def TauCeti.Toric.Fan.starSubdivision {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsRegularCone i τ) : Fan i

The star subdivision of the fan of faces of a regular cone τ along the face spanned by the rays in A: its cones are spanned by the families of ray generators starSubdivisionGenerator, indexed by the sets omitting some ρ for some ρ ∈ A. It subdivides the fan of faces of τ when A is nonempty, and its toric variety is the blow-up of the affine toric variety of τ along the orbit closure of that face.

@[simp]

theorem TauCeti.Toric.Fan.mem_starSubdivision_cones {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsRegularCone i τ) {σ : PointedCone ℝ V} : σ ∈ (starSubdivision hi A hτ).cones ↔ ∃ (S : Set (Option (ToricRay τ))), (∃ ρ ∈ A, some ρ ∉ S) ∧ starSubdivisionCone hi A ⋯ S = σ

The cones of the star subdivision of a regular cone along the rays in A are the cones spanned by the families of ray generators omitting a generator indexed by A.

theorem TauCeti.Toric.Fan.isRegular_starSubdivision {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsRegularCone i τ) : (starSubdivision hi A hτ).IsRegular

The star subdivision of a regular cone is regular.

theorem TauCeti.Toric.Fan.hull_singleton_mem_starSubdivision_cones {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsRegularCone i τ) (hA : A.Nonempty) : ℝ ∙₊ i (∑ ρ ∈ A, primitiveGenerator hi ⋯ ρ) ∈ (starSubdivision hi A hτ).cones

For nonempty A, the ray through the sum of the primitive generators of the rays in A is a cone of the star subdivision. When A contains at least two rays, this is the new ray of the star subdivision; for A = {ρ} it is the ray ρ itself.

@[simp]

theorem TauCeti.Toric.Fan.support_starSubdivision {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsRegularCone i τ) (hA : A.Nonempty) : (starSubdivision hi A hτ).support = ↑τ

For nonempty A, the star subdivision of a regular cone τ covers τ.

theorem TauCeti.Toric.Fan.le_of_mem_starSubdivision_cones {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsRegularCone i τ) {C : PointedCone ℝ V} (hC : C ∈ (starSubdivision hi A hτ).cones) : C ≤ τ

Every cone of the star subdivision of a regular cone τ lies in τ.

theorem TauCeti.Toric.Fan.mem_starSubdivision_cones_of_isFaceOf {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsRegularCone i τ) {F : PointedCone ℝ V} (hF : F.IsFaceOf τ) (hA : ∃ ρ ∈ A, ¬ρ.toPointedCone ≤ F) : F ∈ (starSubdivision hi A hτ).cones

A face of a regular cone τ not containing some ray of A is a cone of the star subdivision of τ along A: it is spanned by the primitive generators of its rays.

theorem TauCeti.Toric.Fan.inf_mem_starSubdivision_cones {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτ : IsRegularCone i τ) {τ₀ C : PointedCone ℝ V} (h : τ₀.IsFaceOf τ) (B : Finset (ToricRay τ₀)) (hC : C ∈ (starSubdivision hi (Finset.map (ToricRay.faceEmbedding h) B) hτ).cones) : C ⊓ τ₀ ∈ (starSubdivision hi B ⋯).cones

Intersecting with a face τ₀ of a regular cone τ restricts the star subdivision of τ along a set B of rays of τ₀ to the star subdivision of τ₀ along B.

theorem TauCeti.Toric.Fan.mem_starSubdivision_cones_map_faceEmbedding {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτ : IsRegularCone i τ) {τ₀ C : PointedCone ℝ V} (h : τ₀.IsFaceOf τ) (B : Finset (ToricRay τ₀)) (hC : C ∈ (starSubdivision hi B ⋯).cones) : C ∈ (starSubdivision hi (Finset.map (ToricRay.faceEmbedding h) B) hτ).cones

The star subdivision of a face τ₀ of a regular cone τ along a set B of rays of τ₀ consists of cones of the star subdivision of τ along B.

theorem TauCeti.Toric.Fan.starSubdivision_isSubdivision {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (A : Finset (ToricRay τ)) (hτ : IsRegularCone i τ) (hA : A.Nonempty) : (starSubdivision hi A hτ).IsSubdivision (ofCone hi ⋯)

For nonempty A, the star subdivision of a regular cone τ subdivides the fan of faces of τ.

The star subdivision of a regular fan along a cone

noncomputable def TauCeti.Toric.Fan.starSubdivisionAlong {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) : Fan i

The star subdivision of a regular fan Φ along one of its cones σ. It keeps the cones of Φ not containing σ, and replaces every cone τ of Φ containing σ by the cones of the star subdivision of τ along the rays of σ, TauCeti.Toric.Fan.starSubdivision. These cones use the ray through u_σ = ∑ ρ, u_ρ, the sum of the primitive generators of the rays of σ. For σ nonzero this subdivides Φ, and classically its toric variety is the blow-up of that of Φ along the orbit closure of σ. For σ = ⊥ the vector u_σ vanishes and the construction degenerates, so the subdivision theorems assume σ ≠ ⊥.

@[simp]

theorem TauCeti.Toric.Fan.mem_starSubdivisionAlong_cones {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) {C : PointedCone ℝ V} : C ∈ (Φ.starSubdivisionAlong hΦ hσ).cones ↔ C ∈ Φ.cones ∧ ¬σ ≤ C ∨ ∃ (τ : PointedCone ℝ V) (hτ : τ ∈ Φ.cones) (hστ : σ ≤ τ), C ∈ (starSubdivision ⋯ (ToricRay.faceFinset ⋯ ⋯) ⋯).cones

The cones of the star subdivision of a regular fan Φ along its cone σ are the cones of Φ not containing σ, and the cones of the star subdivisions of the cones τ of Φ containing σ along the rays of σ.

theorem TauCeti.Toric.Fan.mem_starSubdivisionAlong_cones_of_not_le {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) {C : PointedCone ℝ V} (hC : C ∈ Φ.cones) (hσC : ¬σ ≤ C) : C ∈ (Φ.starSubdivisionAlong hΦ hσ).cones

A cone of Φ not containing σ is a cone of the star subdivision of Φ along σ.

theorem TauCeti.Toric.Fan.exists_cone_le_of_mem_starSubdivisionAlong_cones {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) {C : PointedCone ℝ V} (hC : C ∈ (Φ.starSubdivisionAlong hΦ hσ).cones) : ∃ τ ∈ Φ.cones, C ≤ τ

Every cone of the star subdivision of Φ along σ lies in a cone of Φ.

theorem TauCeti.Toric.Fan.isRegular_starSubdivisionAlong {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) : (Φ.starSubdivisionAlong hΦ hσ).IsRegular

The star subdivision of a regular fan along one of its cones is regular.

@[simp]

theorem TauCeti.Toric.Fan.support_starSubdivisionAlong {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) (hσ0 : σ ≠ ⊥) : (Φ.starSubdivisionAlong hΦ hσ).support = Φ.support

The star subdivision of a regular fan Φ along a nonzero cone of Φ has the same support as Φ.

theorem TauCeti.Toric.Fan.starSubdivisionAlong_isSubdivision {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) (hσ0 : σ ≠ ⊥) : (Φ.starSubdivisionAlong hΦ hσ).IsSubdivision Φ

The star subdivision of a regular fan along a nonzero cone of the fan subdivides it.

theorem TauCeti.Toric.Fan.starSubdivisionAlong_ofCone {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) {τ : PointedCone ℝ V} (hτ : IsRegularCone i τ) (hσ : σ ∈ (ofCone hi ⋯).cones) : (ofCone hi ⋯).starSubdivisionAlong ⋯ hσ = starSubdivision hi (ToricRay.faceFinset ⋯ ⋯) hτ

On the fan of faces of a regular cone τ, the star subdivision along a face σ of τ is the star subdivision of τ along the rays of σ.

The ray through the sum of the primitive generators

noncomputable def TauCeti.Toric.Fan.starSubdivisionAlongRay {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) (hσ0 : σ ≠ ⊥) : (Φ.starSubdivisionAlong hΦ hσ).Ray

The ray of the star subdivision of Φ along a nonzero cone σ through the sum u_σ of the primitive generators of the rays of σ. When σ has at least two rays this is the ray added by the star subdivision; when σ is a ray it is σ itself.

@[simp]

theorem TauCeti.Toric.Fan.coe_toCone_starSubdivisionAlongRay {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) (hσ0 : σ ≠ ⊥) : ↑(Ray.toCone (Φ.starSubdivisionAlong hΦ hσ) (Φ.starSubdivisionAlongRay hΦ hσ hσ0)) = ℝ ∙₊ i (∑ ρ ∈ ToricRay.faceFinset ⋯ ⋯, primitiveGenerator ⋯ ⋯ ρ)

The cone of Fan.starSubdivisionAlongRay is the ray through the sum of the primitive generators of the rays of σ.

theorem TauCeti.Toric.Fan.starSubdivisionAlongRay_le_starSubdivisionCone {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) (hσ0 : σ ≠ ⊥) {τ : PointedCone ℝ V} (hτ : τ ∈ Φ.cones) (hστ : σ ≤ τ) {S : Set (Option (ToricRay τ))} (hS : none ∈ S) : ↑(Ray.toCone (Φ.starSubdivisionAlong hΦ hσ) (Φ.starSubdivisionAlongRay hΦ hσ hσ0)) ≤ starSubdivisionCone ⋯ (ToricRay.faceFinset ⋯ ⋯) ⋯ S

A cone of the star subdivision of a cone τ ⊇ σ of Φ along the rays of σ whose generators include u_σ contains the ray through u_σ.

theorem TauCeti.Toric.Fan.starSubdivisionAlongRay_le_iff_le_leastCone {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) (hσ0 : σ ≠ ⊥) (C : ↑(Φ.starSubdivisionAlong hΦ hσ).cones) : Ray.toCone (Φ.starSubdivisionAlong hΦ hσ) (Φ.starSubdivisionAlongRay hΦ hσ hσ0) ≤ C ↔ σ ≤ ⋯.toFanHom.leastCone ⋯

A cone of the star subdivision of Φ along a nonzero cone σ contains the ray through u_σ exactly when the least cone of Φ containing it contains σ.

theorem TauCeti.Toric.Fan.not_le_leastCone_starSubdivisionAlong_iff {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) (hσ0 : σ ≠ ⊥) {C : PointedCone ℝ V} (hC : C ∈ (Φ.starSubdivisionAlong hΦ hσ).cones) : ¬σ ≤ ⋯.toFanHom.leastCone hC ↔ C ∈ Φ.cones ∧ ¬σ ≤ C

Away from the cones containing σ the star subdivision of Φ along a nonzero cone σ changes nothing: a cone of the star subdivision has a least cone in Φ not containing σ exactly when it is a cone of Φ not containing σ.