The diagram of affine analytic charts of a fan

The complex points of the cones of any fan form a diagram of topological spaces. An inclusion of cones acts by restriction of characters along the corresponding face. For a regular fan, every map is an open embedding. When two points have the same image in a third chart, they come from the chart of the intersection cone. This is the overlap property needed to glue the analytic charts and to compare that gluing with the algebraic fan scheme.

The topology on each chart is the finite-monomial-embedding topology. Its definition chooses a finite generating family, but affinePointTopology_eq shows that the resulting topology is independent of this choice.

References

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

noncomputable def TauCeti.Toric.Fan.analyticChartGenerators {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : (r : ℕ) × AddGeneratingFamily (↥(dualSemigroup ⋯ ↑σ)) r

A finite generating family for the dual semigroup of any cone of a fan.

noncomputable def TauCeti.Toric.Fan.analyticAffineChart {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : TopCat

The affine complex-point chart of a cone, with its monomial-embedding topology.

theorem TauCeti.Toric.Fan.analyticAffineChart_str_eq {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) {r : ℕ} (g : AddGeneratingFamily (↥(dualSemigroup ⋯ ↑σ)) r) : (Φ.analyticAffineChart σ).str = affinePointTopology g

The chart topology agrees with the monomial-embedding topology of any finite generating family.

theorem TauCeti.Toric.Fan.t2Space_analyticAffineChart {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : T2Space ↑(Φ.analyticAffineChart σ)

Each analytic affine chart is Hausdorff.

theorem TauCeti.Toric.Fan.secondCountableTopology_analyticAffineChart {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : SecondCountableTopology ↑(Φ.analyticAffineChart σ)

Each analytic affine chart is second countable.

theorem TauCeti.Toric.Fan.locallyCompactSpace_analyticAffineChart {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : LocallyCompactSpace ↑(Φ.analyticAffineChart σ)

Each analytic affine chart is locally compact.

noncomputable def TauCeti.Toric.Fan.analyticFaceMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {τ σ : ↑Φ.cones} (f : τ ⟶ σ) : Φ.analyticAffineChart τ ⟶ Φ.analyticAffineChart σ

The analytic face map between two charts of a fan.

@[simp]

theorem TauCeti.Toric.Fan.analyticFaceMap_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {τ σ : ↑Φ.cones} (f : τ ⟶ σ) (x : ↑(Φ.analyticAffineChart τ)) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticFaceMap f)) x = faceAffinePointMap ⋯ ⋯ x

An analytic face map restricts the character of a point to the smaller dual semigroup.

noncomputable def TauCeti.Toric.Fan.analyticAffineChartDiagram {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) : CategoryTheory.Functor (↑Φ.cones) TopCat

The analytic affine charts of a fan, indexed by its cones.

@[simp]

theorem TauCeti.Toric.Fan.analyticAffineChartDiagram_obj {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) : Φ.analyticAffineChartDiagram.obj σ = Φ.analyticAffineChart σ

The diagram object at a cone is its affine analytic chart.

@[simp]

theorem TauCeti.Toric.Fan.analyticAffineChartDiagram_map {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {τ σ : ↑Φ.cones} (f : τ ⟶ σ) : Φ.analyticAffineChartDiagram.map f = Φ.analyticFaceMap f

The diagram map at a face inclusion is restriction of complex points.

theorem TauCeti.Toric.Fan.analyticAffineChartDiagram_map_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {τ σ : ↑Φ.cones} (f : τ ⟶ σ) (x : ↑(Φ.analyticAffineChartDiagram.obj τ)) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartDiagram.map f)) x = AffineSemigroupComplexPoint.comap (AddSubmonoid.inclusion ⋯) x

A map of the analytic affine chart diagram restricts a complex point along the inclusion of dual semigroups.

theorem TauCeti.Toric.Fan.analyticChartMap_comp {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) {α β γ : ↑Φ.cones} (f : α ⟶ β) (g : β ⟶ γ) (x : ↑(Φ.analyticAffineChartDiagram.obj α)) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartDiagram.map g)) ((CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartDiagram.map f)) x) = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartDiagram.map (CategoryTheory.CategoryStruct.comp f g))) x

Pointwise composition of maps in the analytic affine chart diagram.

theorem TauCeti.Toric.Fan.isOpenEmbedding_analyticAffineChartDiagram_map {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {τ σ : ↑Φ.cones} (f : τ ⟶ σ) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartDiagram.map f))

Every map in the analytic chart diagram is an open embedding.

theorem TauCeti.Toric.Fan.isLocallyDirected_analyticAffineChartDiagram {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) : (Φ.analyticAffineChartDiagram.comp (CategoryTheory.forget TopCat)).IsLocallyDirected

Two affine analytic charts mapping into a third chart meet in the chart of the intersection cone.