Analytic toric geometry

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremTauCeti.Toric.Fan.exists_partialDiffeomorph_analyticBoundaryComponent_normalForm#

The toric boundary has the holomorphic coordinate-hyperplane normal form near every point x of the realization. There are a biholomorphism e from an open neighbourhood of x onto an open subset of ℂ ^ n, for n the rank of the lattice, and an injection j from the set s of boundary components through x to the coordinate indices, such that a point of the neighbourhood lies in a boundary component exactly when that component passes through x and the coordinate it is assigned vanishes.

TauCeti.Toric.Fan.exists_partialDiffeomorph_analyticBoundaryComponent_normalForm.{u} {N V : Type u}
  [AddCommGroup N] [AddCommGroup V] [_root_.Module ℝ V] {i : N →+ V} (Φ : TauCeti.Toric.Fan i)
  (hΦ : Φ.IsRegular) (x : ↑(Φ.analyticRealization hΦ)) (n : WithTop ℕ∞) :
  ∃ s j e,
    x ∈ e.source ∧
      (∀ (ρ : Φ.Ray), x ∈ Φ.analyticBoundaryComponent hΦ ρ ↔ ρ ∈ s) ∧
        ∀ y ∈ e.source,
          ∀ (ρ : Φ.Ray),
            y ∈ Φ.analyticBoundaryComponent hΦ ρ ↔
              ∃ (hρ : ρ ∈ s), ↑e.toPartialEquiv y (j ⟨ρ, hρ⟩) = 0
Lean

Formalized in Tau Ceti as TauCeti.Toric.Fan.exists_partialDiffeomorph_analyticBoundaryComponent_normalForm.

Sources
LeanTauCeti.Toric.Fan.exists_partialDiffeomorph_analyticBoundaryComponent_normalForm
Uses 2
Proof usesGordan's lemma · Tucker's theorem

TheoremThe cone-by-cone properness criterion#

The analytic map of a morphism of regular fans with nonempty source is proper exactly when, for every target cone τ, the inverse image of τ under the real-linear map is the union of the source cones mapped into τ. The nonemptiness hypothesis is necessary: the inclusion of the empty subfan is proper, but 0 lies in the inverse image of every cone and in no cone of the empty fan. See TauCeti.Toric.FanHom.isProperMap_analyticMap_iff_isEmpty_or for the form without it.

TauCeti.Toric.FanHom.isProperMap_analyticMap_iff.{u} {N N' V V' : Type u} [AddCommGroup N]
  [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [_root_.Module ℝ V] [_root_.Module ℝ V']
  {i : N →+ V} {i' : N' →+ V'} {Φ : TauCeti.Toric.Fan i} {Ψ : TauCeti.Toric.Fan i'}
  (f : TauCeti.Toric.FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) (hΦ0 : Nonempty ↑Φ.cones) :
  IsProperMap ⇑(CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) ↔
    ∀ (τ : ↑Ψ.cones), ⇑f.realMap ⁻¹' ↑↑τ = ⋃ σ, ⋃ (_ : PointedCone.map f.realMap ↑σ ≤ ↑τ), ↑↑σ
Lean

Formalized in Tau Ceti as TauCeti.Toric.FanHom.isProperMap_analyticMap_iff.

Sources
LeanTauCeti.Toric.FanHom.isProperMap_analyticMap_iff
Uses 3
Proof usesGordan's lemma · Hoffman's error bound for a polyhedral cone · Tucker's theorem

TheoremTauCeti.Toric.Fan.isProperMap_analyticMap_starSubdivisionAlong#

The star subdivision of a regular fan Φ along a nonzero cone σ of Φ induces a proper analytic map to the realization of Φ, because the two fans have the same support.

TauCeti.Toric.Fan.isProperMap_analyticMap_starSubdivisionAlong.{u} {N V : Type u} [AddCommGroup N]
  [AddCommGroup V] [_root_.Module ℝ V] {i : N →+ V} (Φ : TauCeti.Toric.Fan i) (hΦ : Φ.IsRegular)
  {σ : PointedCone ℝ V} (hσ : σ ∈ Φ.cones) (hσ0 : σ ≠ ⊥) :
  IsProperMap ⇑(CategoryTheory.ConcreteCategory.hom (⋯.toFanHom.analyticMap ⋯ hΦ))
Lean

Formalized in Tau Ceti as TauCeti.Toric.Fan.isProperMap_analyticMap_starSubdivisionAlong.

Sources
LeanTauCeti.Toric.Fan.isProperMap_analyticMap_starSubdivisionAlong
Uses 3
Proof usesGordan's lemma · Hoffman's error bound for a polyhedral cone · Tucker's theorem

TheoremTauCeti.Toric.Fan.compactSpace_analyticRealization_iff_isComplete#

A nonempty regular fan has compact analytic realization exactly when it is complete. The nonemptiness hypothesis is necessary: the realization of the empty fan is empty, hence compact, while the empty fan is not complete. See TauCeti.Toric.Fan.compactSpace_analyticRealization_iff_isEmpty_or_isComplete for the form without it.

TauCeti.Toric.Fan.compactSpace_analyticRealization_iff_isComplete.{u} {N V : Type u}
  [AddCommGroup N] [AddCommGroup V] [_root_.Module ℝ V] {i : N →+ V} (Φ : TauCeti.Toric.Fan i)
  (hΦ : Φ.IsRegular) (hΦ0 : Nonempty ↑Φ.cones) :
  CompactSpace ↑(Φ.analyticRealization hΦ) ↔ Φ.IsComplete
Lean

Formalized in Tau Ceti as TauCeti.Toric.Fan.compactSpace_analyticRealization_iff_isComplete.

Sources
LeanTauCeti.Toric.Fan.compactSpace_analyticRealization_iff_isComplete
Uses 2
Proof usesGordan's lemma · Tucker's theorem

TheoremTauCeti.Toric.Fan.algebraicAnalyticEquiv_smul#

The algebraic–analytic comparison is equivariant for the coordinate-free complex torus.

TauCeti.Toric.Fan.algebraicAnalyticEquiv_smul {N V : Type} [AddCommGroup N] [AddCommGroup V]
  [_root_.Module ℝ V] {i : N →+ V} {Φ : TauCeti.Toric.Fan i} (hΦ : Φ.IsRegular)
  (t : TauCeti.Toric.ComplexTorus N) (p : Φ.AlgebraicComplexPoint) :
  (TauCeti.Toric.Fan.algebraicAnalyticEquiv hΦ) (t • p) =
    t • (TauCeti.Toric.Fan.algebraicAnalyticEquiv hΦ) p
Lean

Formalized in Tau Ceti as TauCeti.Toric.Fan.algebraicAnalyticEquiv_smul.

Sources
LeanTauCeti.Toric.Fan.algebraicAnalyticEquiv_smul
Uses 2
Proof usesGordan's lemma · Tucker's theorem

InstanceTauCeti.Toric.Fan.algebraicRealizationModObj#

The dense torus acts on the fan scheme over Spec ℂ by the glued affine torus actions.

TauCeti.Toric.Fan.algebraicRealizationModObj.{u_1} {N : Type} {V : Type u_1} [AddCommGroup N]
  [AddCommGroup V] [_root_.Module ℝ V] {i : N →+ V} (Φ : TauCeti.Toric.Fan i) :
  CategoryTheory.ModObj ((TauCeti.Toric.affineToricScheme ⋯ ⊥).asOver (AlgebraicGeometry.Spec ↧ℂ))
    (Φ.algebraicRealization.asOver (AlgebraicGeometry.Spec ↧ℂ))
Lean

Formalized in Tau Ceti as TauCeti.Toric.Fan.algebraicRealizationModObj.

Sources
LeanTauCeti.Toric.Fan.algebraicRealizationModObj
Uses 1
Proof usesTucker's theorem

DefinitionTauCeti.Toric.Fan.projectiveSpace#

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.

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

Formalized in Tau Ceti as TauCeti.Toric.Fan.projectiveSpace.

Sources
LeanTauCeti.Toric.Fan.projectiveSpace
Used by 1
Used byTauCeti.Toric.projectiveSpaceDiffeomorph

DefinitionTauCeti.Toric.projectiveSpaceDiffeomorph#

Homogeneous coordinates identify the analytic realization of the standard projective-space fan biholomorphically with complex projective space, the circle quotient of the unit sphere with its standard homogeneous-ratio atlas.

TauCeti.Toric.projectiveSpaceDiffeomorph.{u} {N V : Type u} [AddCommGroup N] [AddCommGroup V]
  [_root_.Module ℝ V] {n : ℕ} (b : Module.Basis (Fin n) ℤ N) {i : N →+ V}
  (hi : TauCeti.Toric.IsIntegralLattice i) (r : WithTop ℕ∞) :
  have x := (TauCeti.Toric.Fan.projectiveSpace b hi).analyticChartedSpace ⋯;
  Diffeomorph (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ))
    (modelWithCornersSelf ℂ (Fin n → ℂ))
    (↑((TauCeti.Toric.Fan.projectiveSpace b hi).analyticRealization ⋯))
    (TauCeti.ComplexProjectiveSpace n) r
Lean

Formalized in Tau Ceti as TauCeti.Toric.projectiveSpaceDiffeomorph.

Sources
LeanTauCeti.Toric.projectiveSpaceDiffeomorph
Uses 3
Statement usesTauCeti.Toric.Fan.projectiveSpace
Proof usesGordan's lemma · Tucker's theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.