The fan of projective space

Let b be an integral basis of the lattice N, indexed by a finite type ι of size n. The fan of n-dimensional projective space has n + 1 ray generators: the basis vectors b j and the vector -∑ j, b j, which we index by Option ι, with none for the last one. Its cones are the cones spanned by the generators indexed by a proper subset S of Option ι.

Any n of the n + 1 generators form an integral basis, and the only linear relation among all of them is that they sum to zero. The first fact makes every cone regular. The second makes the conical coefficients of a point of two such cones agree up to a common constant, which must vanish since each cone omits a generator. Hence two cones meet in the cone of the intersection of their index sets, a face of both, and the cones form a fan. It is complete: subtracting from the coefficients of a point the least of them writes it as a conical combination omitting one generator.

The affine chart of the maximal cone omitting the generator indexed by k is the standard affine chart of projective space on which the k-th homogeneous coordinate does not vanish; this is proved in TauCeti.Geometry.Toric.Algebraic.Fan.ProjectiveSpace.Proj.

Main declarations

• TauCeti.Toric.projectiveSpaceGenerator: the ray generators of the fan of projective space.
• TauCeti.Toric.projectiveSpaceCone: the cone spanned by the generators indexed by a set.
• TauCeti.Toric.linearIndepOn_projectiveSpaceGenerator: any family of generators omitting one of them is linearly independent.
• TauCeti.Toric.projectiveSpaceCone_compl_none: the maximal cone omitting the extra generator is the positive orthant spanned by the basis.
• TauCeti.Toric.projectiveSpaceCone_inf: the intersection of two cones omitting a generator is the cone of the intersection of their index sets.
• TauCeti.Toric.projectiveSpaceCone_le_iff and TauCeti.Toric.projectiveSpaceCone_inj: a cone omitting a generator determines its index set.
• TauCeti.Toric.isRegularCone_projectiveSpaceCone: each cone omitting a generator is regular.
• TauCeti.Toric.Fan.projectiveSpace: the fan of projective space.
• TauCeti.Toric.Fan.isRegular_projectiveSpace and TauCeti.Toric.Fan.isComplete_projectiveSpace: it is regular and complete.

References

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

The ray generators

noncomputable def TauCeti.Toric.projectiveSpaceGenerator {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (b : Module.Basis ι ℤ N) (k : Option ι) : N

The ray generators of the fan of projective space attached to an integral basis b: the basis vector b j at some j, and the negative -∑ j, b j of their sum at none.

@[simp]

theorem TauCeti.Toric.projectiveSpaceGenerator_none {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (b : Module.Basis ι ℤ N) : projectiveSpaceGenerator b none = -∑ j : ι, b j

@[simp]

theorem TauCeti.Toric.projectiveSpaceGenerator_some {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (b : Module.Basis ι ℤ N) (j : ι) : projectiveSpaceGenerator b (some j) = b j

theorem TauCeti.Toric.sum_projectiveSpaceGenerator {N : Type u_1} {ι : Type u_3} [AddCommGroup N] [Fintype ι] (b : Module.Basis ι ℤ N) : ∑ k : Option ι, projectiveSpaceGenerator b k = 0

The ray generators of the fan of projective space sum to zero.

theorem TauCeti.Toric.linearIndepOn_projectiveSpaceGenerator {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) (hli : LinearIndependent ℝ fun (j : ι) => i (b j)) {S : Set (Option ι)} (hS : S ≠ Set.univ) : LinearIndepOn ℝ (fun (k : Option ι) => i (projectiveSpaceGenerator b k)) S

Any family of ray generators of the fan of projective space omitting one of them is linearly independent over the reals.

The cones

noncomputable def TauCeti.Toric.projectiveSpaceCone {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] [Fintype ι] (b : Module.Basis ι ℤ N) (i : N →+ V) (S : Set (Option ι)) : PointedCone ℝ V

The cone of the fan of projective space spanned by the ray generators indexed by S. It is a cone of the fan when S omits some generator.

theorem TauCeti.Toric.projectiveSpaceCone_def {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) (S : Set (Option ι)) : projectiveSpaceCone b i S = PointedCone.hull ℝ (⇑i '' projectiveSpaceGenerator b '' S)

theorem TauCeti.Toric.mem_projectiveSpaceCone_iff {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) {S : Set (Option ι)} {x : V} : x ∈ projectiveSpaceCone b i S ↔ ∃ (c : Option ι → ℝ), (∀ k ∉ S, c k = 0) ∧ (∀ (k : Option ι), 0 ≤ c k) ∧ ∑ k : Option ι, c k • i (projectiveSpaceGenerator b k) = x

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

@[simp]

theorem TauCeti.Toric.projectiveSpaceCone_empty {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) : projectiveSpaceCone b i ∅ = ⊥

theorem TauCeti.Toric.projectiveSpaceCone_mono {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) {S T : Set (Option ι)} (h : S ⊆ T) : projectiveSpaceCone b i S ≤ projectiveSpaceCone b i T

theorem TauCeti.Toric.projectiveSpaceCone_compl_none {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) : projectiveSpaceCone b i {none}ᶜ = PointedCone.hull ℝ (Set.range fun (j : ι) => i (b j))

The maximal cone of the fan of projective space omitting the extra ray is the positive orthant spanned by the basis vectors.

theorem TauCeti.Toric.projectiveSpaceCone_inf {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) (hli : LinearIndependent ℝ fun (j : ι) => i (b j)) {S T : Set (Option ι)} (hS : S ≠ Set.univ) (hT : T ≠ Set.univ) : projectiveSpaceCone b i S ⊓ projectiveSpaceCone b i T = projectiveSpaceCone b i (S ∩ T)

Two cones of the fan of projective space, each omitting some generator, meet in the cone of the intersection of their index sets.

theorem TauCeti.Toric.projectiveSpaceCone_le_iff {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) (hli : LinearIndependent ℝ fun (j : ι) => i (b j)) {S T : Set (Option ι)} (hS : S ≠ Set.univ) : projectiveSpaceCone b i S ≤ projectiveSpaceCone b i T ↔ S ⊆ T

The cone of the fan of projective space indexed by a set S omitting some generator lies in the cone indexed by T exactly when S ⊆ T.

@[simp]

theorem TauCeti.Toric.projectiveSpaceCone_inj {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) (hli : LinearIndependent ℝ fun (j : ι) => i (b j)) {S T : Set (Option ι)} (hS : S ≠ Set.univ) (hT : T ≠ Set.univ) : projectiveSpaceCone b i S = projectiveSpaceCone b i T ↔ S = T

Two cones of the fan of projective space, each omitting some generator, coincide exactly when their index sets do.

theorem TauCeti.Toric.isRegularCone_projectiveSpaceCone {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) (hi : IsIntegralLattice i) {S : Set (Option ι)} (hS : S ≠ Set.univ) : IsRegularCone i (projectiveSpaceCone b i S)

A cone of the fan of projective space omitting some generator is regular.

The fan

noncomputable def TauCeti.Toric.Fan.projectiveSpace {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) (hi : IsIntegralLattice i) : Fan i

The fan of projective space attached to an integral basis b of an integral lattice: its cones are spanned by the families of ray generators projectiveSpaceGenerator b omitting at least one of them. For a basis indexed by a type with n elements it is the fan of n-dimensional complex projective space.

@[simp]

theorem TauCeti.Toric.Fan.mem_projectiveSpace_cones {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) (hi : IsIntegralLattice i) {σ : PointedCone ℝ V} : σ ∈ (projectiveSpace b hi).cones ↔ ∃ (S : Set (Option ι)), S ≠ Set.univ ∧ projectiveSpaceCone b i S = σ

The cones of the fan of projective space are the cones spanned by the families of ray generators omitting at least one of them.

@[reducible, inline]

noncomputable abbrev TauCeti.Toric.Fan.projectiveSpaceMaximalCone {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) (hi : IsIntegralLattice i) (k : Option ι) : ↑(projectiveSpace b hi).cones

The maximal cone omitting the ray k, whose projective chart has X_k ≠ 0.

theorem TauCeti.Toric.Fan.exists_le_projectiveSpaceCone_compl {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) (hi : IsIntegralLattice i) {σ : PointedCone ℝ V} (hσ : σ ∈ (projectiveSpace b hi).cones) : ∃ (k : Option ι), σ ≤ projectiveSpaceCone b i {k}ᶜ

Every cone of the fan of projective space lies in the maximal cone omitting some ray.

theorem TauCeti.Toric.Fan.isRegular_projectiveSpace {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) (hi : IsIntegralLattice i) : (projectiveSpace b hi).IsRegular

The fan of projective space is regular.

theorem TauCeti.Toric.Fan.bot_mem_projectiveSpace_cones {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) (hi : IsIntegralLattice i) : ⊥ ∈ (projectiveSpace b hi).cones

The fan of projective space is nonempty: it contains the zero cone.

theorem TauCeti.Toric.Fan.isComplete_projectiveSpace {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} [Fintype ι] (b : Module.Basis ι ℤ N) (hi : IsIntegralLattice i) : (projectiveSpace b hi).IsComplete

The fan of projective space is complete.