Regular toric cones and regular fans

A toric cone is regular, or smooth, when its primitive ray generators can be completed to a single integral basis of the lattice. This is the combinatorial condition under which the affine chart of the cone is a mixed chart ℂ ^ k × (ℂ ^ *) ^ (n - k) rather than a singular affine toric variety, so it is the hypothesis carried by the downstream mixed-chart and complex-manifold constructions.

Regularity is defined here as the conjunction of TauCeti.Toric.IsToricCone with the existence of an extending basis: an integral basis b of the lattice together with an injection r of the rays of the cone into the basis indices such that b (r ρ) is the primitive generator of the ray ρ. The toric-cone hypothesis separately enforces lattice rationality, salience, and finite generation; the basis condition alone would be vacuous whenever the cone's ToricRay type is empty.

Two extending bases of the same cone cannot differ at the ray indices, because a ray of a toric cone in an integral lattice has only one primitive generator. This pins the block form of the transition matrix between two extending bases: every ray column is a standard column supported at the matching ray row, so splitting the index set of each basis into its rays and a common complement, compatibly with the two ray indexings, the matrix is [[1, B], [0, D]] with D unimodular. The analytic layer consumes exactly this shape: changing the extending basis keeps the boundary coordinates, twists them by B, and acts on the torus coordinates by D.

Main declarations

• TauCeti.Toric.IsExtendingBasis: an integral basis whose vectors at the ray indices are the primitive ray generators.
• TauCeti.Toric.IsRegularCone: a toric cone admitting an extending basis.
• TauCeti.Toric.isRegularCone_bot: the zero cone, whose affine chart is the dense torus, is regular.
• TauCeti.Toric.isRegularCone_hull_singleton: the cone spanned by a primitive lattice vector, whose affine chart is the mixed chart ℂ × (ℂ ^ *) ^ (n - 1) with a single boundary coordinate, is regular.
• TauCeti.Toric.IsRegularCone.of_isFaceOf and TauCeti.Toric.IsRegularCone.face: a face of a regular cone is regular. Since the pairwise intersections of the cones of a fan are faces, this also makes the overlaps of the affine charts of a regular fan regular.
• TauCeti.Toric.IsRegularCone.prod: a product of regular cones is regular for the product lattice map.
• TauCeti.Toric.IsRegularCone.card_toricRay_le_finrank: a regular cone has at most as many rays as the rank of the lattice, which is the count that gives the dimensions of its mixed chart.
• TauCeti.Toric.IsRegularCone.exists_basis_sum: an extending basis indexed by the rays followed by a finite complementary type, as required by regular affine coordinates.
• TauCeti.Toric.IsExtendingBasis.basis_apply_eq, TauCeti.Toric.IsExtendingBasis.repr_basis_apply and TauCeti.Toric.IsExtendingBasis.toMatrix_apply: the salient ray columns of the transition matrix relating two extending bases.
• TauCeti.Toric.isUnit_det_toMatrix_submatrix_inr: for two bases indexed by a splitting of the index set into the rays of the cone and a common complement, both extending the primitive ray generators, the complementary block of the transition matrix is unimodular.
• TauCeti.Toric.IsExtendingBasis.isUnit_det_toMatrix_compl and TauCeti.Toric.IsExtendingBasis.exists_isUnit_det_toMatrix_compl: the complementary block of that transition matrix is unimodular, for compatible splittings of the two index sets into the rays and a common complement, and such a splitting exists.
• TauCeti.Toric.Fan.IsRegular: a fan all of whose cones are regular, together with the regularity of the fan of a regular cone and of subfans.

Implementation notes

TauCeti.Toric.IsRegularCone extends TauCeti.Toric.IsToricCone, so lattice rationality, salience and finite generation of a regular cone are reached by dot notation through the parent structure rather than by forwarding lemmas.

The index type of an extending basis is Fin n for an unconstrained n rather than Fin (Module.finrank ℤ N). The two are interchangeable, since Module.finrank_eq_card_basis identifies n with the rank and TauCeti.Toric.IsRegularCone.exists_basis_finrank produces the second form on demand, but the unconstrained index avoids transporting a basis along an equality of natural numbers every time one is built.

References

The mathematics is §1.2 and Proposition 1.2.16 of W. Fulton, Introduction to Toric Varieties, and §§1.2 and 1.3 of D. Cox, J. Little and H. Schenck, Toric Varieties, where a regular cone is called smooth.

Extending bases

structure TauCeti.Toric.IsExtendingBasis {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] (i : N →+ V) {σ : PointedCone ℝ V} {n : ℕ} (b : Module.Basis (Fin n) ℤ N) (r : ToricRay σ ↪ Fin n) : Prop

An integral basis b of N extends the primitive ray generators of a cone σ along an injection r of the rays of σ into the basis indices when the basis vector b (r ρ) is the primitive generator of the ray ρ.

• isPrimitiveGenerator_apply (ρ : ToricRay σ) : IsPrimitiveGenerator i ρ (b (r ρ))

  The basis vector indexed by a ray is the primitive generator of that ray.

Regular cones

structure TauCeti.Toric.IsRegularCone {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] (i : N →+ V) (σ : PointedCone ℝ V) extends TauCeti.Toric.IsToricCone i σ : Prop

A toric cone is regular, or smooth, when some integral basis of the lattice extends its primitive ray generators. The toric-cone hypothesis is part of the definition: it enforces lattice rationality, salience, and finite generation, while the basis condition alone would be vacuous for any cone whose ToricRay type is empty.

• rational : IsLatticeRational i σ
• salient : (↑σ).Salient
• exists_basis : ∃ (n : ℕ) (b : Module.Basis (Fin n) ℤ N) (r : ToricRay σ ↪ Fin n), IsExtendingBasis i b r

  Some integral basis extends the primitive ray generators of the cone.

theorem TauCeti.Toric.IsRegularCone.exists_basis_finrank {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (h : IsRegularCone i σ) : ∃ (b : Module.Basis (Fin (Module.finrank ℤ N)) ℤ N) (r : ToricRay σ ↪ Fin (Module.finrank ℤ N)), IsExtendingBasis i b r

The rays of a regular cone can be indexed inside a basis of rank-many indices.

theorem TauCeti.Toric.IsRegularCone.card_toricRay_le_finrank {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (h : IsRegularCone i σ) : Nat.card (ToricRay σ) ≤ Module.finrank ℤ N

A regular cone has at most as many rays as the rank of the lattice: an extending basis indexes its rays injectively. This ray count is what fixes the two dimensions of the mixed chart ℂ ^ k × (ℂ ^ *) ^ (n - k); reading it as the dimension of the cone needs the simpliciality of a regular cone, which is not proved here.

Equivalences

theorem TauCeti.Toric.IsRegularCone.map_equiv {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {f : N ≃+ N'} {e : V ≃ₗ[ℝ] V'} (hfe : ∀ (n : N), e (i n) = i' (f n)) (h : IsRegularCone i σ) : IsRegularCone i' (PointedCone.map (↑e) σ)

Regularity is preserved when a cone is transported along compatible equivalences of its integral lattice and ambient real vector space.

theorem TauCeti.Toric.isRegularCone_map_equiv_iff {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {f : N ≃+ N'} {e : V ≃ₗ[ℝ] V'} (hfe : ∀ (n : N), e (i n) = i' (f n)) : IsRegularCone i' (PointedCone.map (↑e) σ) ↔ IsRegularCone i σ

Regularity of a cone is invariant under compatible equivalences of its integral lattice and ambient real vector space.

The zero cone and the cone of a ray

@[simp]

theorem TauCeti.Toric.isRegularCone_bot {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) : IsRegularCone i ⊥

The zero cone is regular. Its affine chart is the dense torus of the lattice, which is therefore a smooth chart of every toric variety built from a nonempty fan.

@[simp]

theorem TauCeti.Toric.isRegularCone_hull_singleton {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) {v : N} (hv : IsPrimitive v) : IsRegularCone i (ℝ ∙₊ i v)

The cone spanned by a primitive lattice vector is regular: a primitive vector belongs to an integral basis, and the cone it spans is its own only ray. Having a single ray, this cone has exactly one boundary coordinate: its affine chart is ℂ × (ℂ ^ *) ^ (n - 1) for n the rank of the lattice, into which the chart of the zero face is the inclusion of the dense torus.

Faces

theorem TauCeti.Toric.IsRegularCone.of_isFaceOf {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hσ : IsRegularCone i σ) (hτ : τ.IsFaceOf σ) : IsRegularCone i τ

A face of a regular cone is regular: its rays are rays of the ambient cone, with the same primitive generators, so an extending basis of the ambient cone restricts to one of the face.

theorem TauCeti.Toric.IsRegularCone.face {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hσ : IsRegularCone i σ) (F : σ.Face) : IsRegularCone i ↑F

Every element of Mathlib's face lattice of a regular cone is a regular cone. Since the pairwise intersection of two cones of a fan is a face of each of them, the overlaps of the affine charts of a regular fan are again charts of regular cones.

Products

theorem TauCeti.Toric.IsRegularCone.prod {N : Type u_1} {N' : Type u_2} {V : Type u_3} {V' : Type u_4} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {σ : PointedCone ℝ V} {τ' : PointedCone ℝ V'} (hσ : IsRegularCone i σ) (hτ' : IsRegularCone i' τ') : IsRegularCone (i.prodMap i') (Submodule.prod σ τ')

A product of regular cones is regular for the product lattice map. Every ray of the product is a ray of one of the two factors, so the product of two extending bases extends the primitive ray generators of the product cone.

Two extending bases

theorem TauCeti.Toric.isUnit_det_toMatrix_submatrix_inr {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {ι : Type u_5} [Fintype ι] [DecidableEq ι] (hi : IsIntegralLattice i) (hσ : (↑σ).Salient) {B B' : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (hB' : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B' (Sum.inl ρ))) : IsUnit ((B'.toMatrix ⇑B).submatrix Sum.inr Sum.inr).det

The complementary block of the transition matrix between two bases indexed by a splitting of the index set into the rays of a cone and a common complement, both carrying the primitive generator of a ray at the index of that ray, is unimodular: the matrix has the block form [[1, B], [0, D]], because a salient ray in an integral lattice has only one primitive generator. This is the unimodularity hypothesis used by the analytic change of chart.

theorem TauCeti.Toric.IsExtendingBasis.isPrimitiveGenerator_reindex {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {n : ℕ} {b : Module.Basis (Fin n) ℤ N} {r : ToricRay σ ↪ Fin n} {ι : Type u_5} (hb : IsExtendingBasis i b r) (e : ToricRay σ ⊕ ι ≃ Fin n) (he : ∀ (ρ : ToricRay σ), e (Sum.inl ρ) = r ρ) (ρ : ToricRay σ) : IsPrimitiveGenerator i ρ ((b.reindex e.symm) (Sum.inl ρ))

An extending basis, reindexed along a splitting of its index set into the rays of the cone and a complement compatibly with the ray indexing, carries the primitive generator of a ray at the index of that ray. This is the hypothesis shape consumed by TauCeti.Toric.regularDualSemigroupEquiv.

theorem TauCeti.Toric.IsExtendingBasis.basis_apply_eq {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {n n' : ℕ} {b : Module.Basis (Fin n) ℤ N} {b' : Module.Basis (Fin n') ℤ N} {r : ToricRay σ ↪ Fin n} {r' : ToricRay σ ↪ Fin n'} (hi : IsIntegralLattice i) (hb : IsExtendingBasis i b r) (hb' : IsExtendingBasis i b' r') (ρ : ToricRay σ) (hρ : (↑ρ.toPointedCone).Salient) : b (r ρ) = b' (r' ρ)

Two integral bases extending the primitive ray generators of a cone carry the same vector at the indices of a given salient ray: both are primitive generators of that ray, and a salient ray in an integral lattice has only one. Only the ray itself has to be salient; for a ray of a salient ambient cone this follows from ConvexCone.Salient.anti along the face inclusion.

theorem TauCeti.Toric.IsExtendingBasis.repr_basis_apply {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {n n' : ℕ} {b : Module.Basis (Fin n) ℤ N} {b' : Module.Basis (Fin n') ℤ N} {r : ToricRay σ ↪ Fin n} {r' : ToricRay σ ↪ Fin n'} (hi : IsIntegralLattice i) (hb : IsExtendingBasis i b r) (hb' : IsExtendingBasis i b' r') (ρ : ToricRay σ) (hρ : (↑ρ.toPointedCone).Salient) : b'.repr (b (r ρ)) = Finsupp.single (r' ρ) 1

The salient ray columns of the transition matrix between two extending bases are standard columns.

theorem TauCeti.Toric.IsExtendingBasis.toMatrix_apply {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {n n' : ℕ} {b : Module.Basis (Fin n) ℤ N} {b' : Module.Basis (Fin n') ℤ N} {r : ToricRay σ ↪ Fin n} {r' : ToricRay σ ↪ Fin n'} (hi : IsIntegralLattice i) (hb : IsExtendingBasis i b r) (hb' : IsExtendingBasis i b' r') (ρ : ToricRay σ) (hρ : (↑ρ.toPointedCone).Salient) (j : Fin n') : b'.toMatrix (⇑b) j (r ρ) = if j = r' ρ then 1 else 0

The entries of a ray column of the transition matrix between two extending bases: the column of the index that b assigns to a ray carries a single 1, in the row that b' assigns to that same ray, and zeroes elsewhere. Splitting both index sets into ray and nonray indices, this is the [[P, B], [0, C]] shape of the matrix, with P the comparison of the two ray indexings. When both splittings are indexed by the rays themselves, P is the identity and C is unimodular, by TauCeti.Toric.IsExtendingBasis.isUnit_det_toMatrix_compl.

theorem TauCeti.Toric.IsExtendingBasis.toMatrix_apply_eq_zero {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {n n' : ℕ} {b : Module.Basis (Fin n) ℤ N} {b' : Module.Basis (Fin n') ℤ N} {r : ToricRay σ ↪ Fin n} {r' : ToricRay σ ↪ Fin n'} (hi : IsIntegralLattice i) (hb : IsExtendingBasis i b r) (hb' : IsExtendingBasis i b' r') (ρ : ToricRay σ) (hρ : (↑ρ.toPointedCone).Salient) {j : Fin n'} (hj : j ≠ r' ρ) : b'.toMatrix (⇑b) j (r ρ) = 0

The nonray-row, ray-column block of the transition matrix between two extending bases vanishes at a salient ray.

theorem TauCeti.Toric.IsExtendingBasis.isUnit_det_toMatrix_compl {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {n n' : ℕ} {b : Module.Basis (Fin n) ℤ N} {b' : Module.Basis (Fin n') ℤ N} {r : ToricRay σ ↪ Fin n} {r' : ToricRay σ ↪ Fin n'} {ι : Type u_5} [Fintype ι] [DecidableEq ι] (hi : IsIntegralLattice i) (hσ : (↑σ).Salient) (hb : IsExtendingBasis i b r) (hb' : IsExtendingBasis i b' r') (e : ToricRay σ ⊕ ι ≃ Fin n) (e' : ToricRay σ ⊕ ι ≃ Fin n') (he : ∀ (ρ : ToricRay σ), e (Sum.inl ρ) = r ρ) (he' : ∀ (ρ : ToricRay σ), e' (Sum.inl ρ) = r' ρ) : IsUnit ((b'.toMatrix ⇑b).submatrix (fun (j : ι) => e' (Sum.inr j)) fun (k : ι) => e (Sum.inr k)).det

The complementary block of the transition matrix between two extending bases is unimodular. For compatible splittings of both index sets into the rays of the cone and a common complement ι, the transition matrix has the block form [[1, B], [0, D]], with D unimodular. This is the unimodularity hypothesis used by the analytic change of chart.

theorem TauCeti.Toric.IsExtendingBasis.exists_isUnit_det_toMatrix_compl {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {n n' : ℕ} {b : Module.Basis (Fin n) ℤ N} {b' : Module.Basis (Fin n') ℤ N} {r : ToricRay σ ↪ Fin n} {r' : ToricRay σ ↪ Fin n'} (hi : IsIntegralLattice i) (hσ : (↑σ).Salient) (hb : IsExtendingBasis i b r) (hb' : IsExtendingBasis i b' r') : ∃ (l : ℕ) (e : ToricRay σ ⊕ Fin l ≃ Fin n) (e' : ToricRay σ ⊕ Fin l ≃ Fin n'), (∀ (ρ : ToricRay σ), e (Sum.inl ρ) = r ρ) ∧ (∀ (ρ : ToricRay σ), e' (Sum.inl ρ) = r' ρ) ∧ IsUnit ((b'.toMatrix ⇑b).submatrix (fun (j : Fin l) => e' (Sum.inr j)) fun (k : Fin l) => e (Sum.inr k)).det

Two extending bases of the same cone admit compatible splittings of their index sets into the rays of the cone and a common complement Fin l, in which the transition matrix has the block form [[1, B], [0, D]] with D unimodular. The two index sets have the same size, both being the rank of the lattice, so the same l serves for both.

theorem TauCeti.Toric.IsRegularCone.exists_basis_sum {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (h : IsRegularCone i σ) : ∃ (l : ℕ) (b : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N), ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))

The primitive ray generators of a regular cone can be placed at the left summand of a basis indexed by the rays and a finite complementary type. This is the indexing shape used by the regular affine-coordinate equivalence.

Regular fans

def TauCeti.Toric.Fan.IsRegular {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : Prop

A fan is regular, or smooth, when every one of its cones is regular. This is the hypothesis under which the analytic realization of the fan is a complex manifold.

@[simp]

theorem TauCeti.Toric.Fan.isRegular_iff {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} : Φ.IsRegular ↔ ∀ σ ∈ Φ.cones, IsRegularCone i σ

The characteristic property of a regular fan.

theorem TauCeti.Toric.Fan.isRegular_ofCone {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsRegularCone i σ) : (ofCone hi ⋯).IsRegular

The fan of a regular cone is regular: its cones are the faces of that cone.

theorem TauCeti.Toric.Fan.isRegular_ofCones_iff {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (hi : IsIntegralLattice i) (S : Set (PointedCone ℝ V)) (hS : S.Finite) (hSt : ∀ ⦃σ : PointedCone ℝ V⦄, σ ∈ S → IsToricCone i σ) (hSinf : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ ∈ S → (σ ⊓ τ).IsFaceOf σ) : (ofCones hi S hS hSt hSinf).IsRegular ↔ ∀ σ ∈ S, IsRegularCone i σ

The fan generated by finitely many cones is regular exactly when the generating cones are.

theorem TauCeti.Toric.Fan.IsRegular.subfan {N : Type u_1} {V : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) : (Φ.subfan S hS hface).IsRegular

A subfan of a regular fan is regular.