Documentation

TauCeti.Geometry.Toric.Analytic.Fan.Manifold

The complex manifold of a regular fan #

The analytic realization TauCeti.Toric.Fan.analyticRealization of a regular fan is glued from the affine analytic charts of its cones along the face localizations. This file installs its complex atlas and proves that it is a complex manifold, modelled on ℂ ^ n for n the rank of the lattice.

The complex structure on the affine chart of a regular cone comes from an extending integral basis, which identifies the chart with the open subset ℂ ^ k × (ℂˣ) ^ l of ℂ ^ k × ℂ ^ l, where k is the number of rays and k + l = n. Choosing such a basis for every cone and identifying ℂ ^ k × ℂ ^ l linearly with ℂ ^ n makes every affine chart a manifold modelled on ℂ ^ n. A map into an affine chart is holomorphic for this structure exactly when its values on all monomials are, which lets every statement be transferred to the structure of any other extending basis.

Two affine charts are glued along the chart of the intersection cone, through the open face localizations into both. A face localization is a biholomorphism onto its open image, so the charts are glued along holomorphic maps, and TopCat.GlueData.chartedSpace gives the realization a complex atlas making it a complex manifold. For this atlas, the inclusion of every affine chart, with the complex structure of any extending basis, is a biholomorphism onto its open image.

Main declarations #

References #

The same structures, indexed by the index type of the gluing data. Instance search does not identify this index type with Φ.cones, so the gluing theorems need these forms.

The complex manifold #

source
@[instance_reducible]
noncomputable def TauCeti.Toric.Fan.analyticChartedSpace {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) :
ChartedSpace (Fin (Module.finrank ℤ N) → ℂ) ↑(Φ.analyticRealization hΦ)

The complex atlas of the analytic realization of a regular fan, modelled on ℂ ^ n for n the rank of the lattice. Its charts are regular affine charts of the cones, transported along the chart inclusions.

Instances For
    source
    theorem TauCeti.Toric.Fan.isManifold_analyticRealization {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (n : WithTop ℕ∞) :
    IsManifold (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) n ↑(Φ.analyticRealization hΦ)

    The analytic realization of a regular fan is a complex manifold.

    source
    noncomputable def TauCeti.Toric.Fan.analyticAffineChartPartialDiffeomorph {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) {k l s : ℕ} {B : Module.Basis (ToricRay ↑σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay ↑σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay ↑σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup ⋯ ↑σ)) s) (n : WithTop ℕ∞) :
    let x := affinePointTopology g; have x_1 := coneChartedSpace ⋯ ⋯ hB κ g; PartialDiffeomorph (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) (AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ)) (↑(Φ.analyticRealization hΦ)) n

    The inclusion of the affine analytic chart of a cone into the analytic realization, as a biholomorphism onto its open image. The chart carries the complex structure of any extending basis of the cone.

    Instances For
      source
      @[simp]
      theorem TauCeti.Toric.Fan.analyticAffineChartPartialDiffeomorph_source {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) {k l s : ℕ} {B : Module.Basis (ToricRay ↑σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay ↑σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay ↑σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup ⋯ ↑σ)) s) (n : WithTop ℕ∞) :
      (Φ.analyticAffineChartPartialDiffeomorph hΦ σ hB κ g n).source = Set.univ

      The chart-inclusion biholomorphism is defined on the whole affine analytic chart.

      source
      @[simp]
      theorem TauCeti.Toric.Fan.analyticAffineChartPartialDiffeomorph_target {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) {k l s : ℕ} {B : Module.Basis (ToricRay ↑σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay ↑σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay ↑σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup ⋯ ↑σ)) s) (n : WithTop ℕ∞) :
      (Φ.analyticAffineChartPartialDiffeomorph hΦ σ hB κ g n).target = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ))

      The target of the chart-inclusion biholomorphism is the image of the affine analytic chart.

      source
      @[simp]
      theorem TauCeti.Toric.Fan.analyticAffineChartPartialDiffeomorph_apply {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) {k l s : ℕ} {B : Module.Basis (ToricRay ↑σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay ↑σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay ↑σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup ⋯ ↑σ)) s) (n : WithTop ℕ∞) (x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ)) :
      ↑(Φ.analyticAffineChartPartialDiffeomorph hΦ σ hB κ g n).toPartialEquiv x = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x

      The chart-inclusion biholomorphism is the inclusion of the affine analytic chart.

      source
      @[simp]
      theorem TauCeti.Toric.Fan.analyticAffineChartPartialDiffeomorph_symm_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) {k l s : ℕ} {B : Module.Basis (ToricRay ↑σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay ↑σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay ↑σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup ⋯ ↑σ)) s) (n : WithTop ℕ∞) (x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ)) :
      have x_1 := affinePointTopology g; have x_2 := coneChartedSpace ⋯ ⋯ hB κ g; ↑(Φ.analyticAffineChartPartialDiffeomorph hΦ σ hB κ g n).symm ((CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x) = x

      The inverse chart-inclusion biholomorphism recovers each affine chart point from its image.

      source
      theorem TauCeti.Toric.Fan.contMDiff_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) {k l s : ℕ} {B : Module.Basis (ToricRay ↑σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay ↑σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay ↑σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup ⋯ ↑σ)) s) (n : WithTop ℕ∞) :
      let x := affinePointTopology g; have x_1 := coneChartedSpace ⋯ ⋯ hB κ g; ContMDiff (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) n fun (x : AffineSemigroupComplexPoint ↥(dualSemigroup ⋯ ↑σ)) => (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x

      The inclusion of the affine analytic chart of a cone into the analytic realization is holomorphic, for the complex structure of any extending basis of the cone.