The analytic realization of a regular fan

The affine analytic charts of a regular fan, their pairwise overlap loci and the transitions between them form gluing data for topological spaces in the sense of TopCat.GlueData. This file assembles that gluing data and defines the analytic realization of the fan as the glued space TopCat.GlueData.glued. Every affine chart is an open subspace of the realization, the charts cover it, and points of two charts are identified exactly when they come from a common point of the chart of the intersection cone.

Main declarations

• TauCeti.Toric.Fan.analyticGlueData: the gluing data of the affine analytic charts of a regular fan along their overlap transitions.
• TauCeti.Toric.Fan.analyticRealization: the analytic realization of a regular fan, the glued space of this gluing data.
• TauCeti.Toric.Fan.analyticAffineChartι: the inclusion of an affine analytic chart into the realization, an open embedding by TauCeti.Toric.Fan.isOpenEmbedding_analyticAffineChartι.
• TauCeti.Toric.Fan.analyticAffineChartι_faceAffinePointMap: face-localization maps commute with the chart inclusions into the realization.
• TauCeti.Toric.Fan.exists_analyticAffineChartι_apply_eq: the affine charts cover the realization.
• TauCeti.Toric.Fan.isEmpty_analyticRealization_iff: the realization is empty exactly when the fan has no cones.
• TauCeti.Toric.Fan.analyticAffineChartι_eq_analyticAffineChartι_iff: points of two charts are identified exactly along the chart of the intersection cone.
• TauCeti.Toric.Fan.isOpen_iff_forall_preimage_analyticAffineChartι: a subset of the realization is open exactly when its preimage in every chart is open.

Implementation notes

The gluing data is built with TopCat.GlueData.mk', whose index type and spaces live in one universe, so the lattice N and the real vector space V are taken in a common universe here. The gluing data is exposed so that its index type and charts are definitionally the cones and the affine analytic charts, which is what lets the chart inclusions be stated on the objects of TauCeti.Toric.Fan.analyticAffineChartDiagram and lets the TopCat.GlueData API be applied at a cone.

References

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

The gluing data

noncomputable def TauCeti.Toric.Fan.analyticGlueData {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) : TopCat.GlueData

The gluing data of the affine analytic charts of a regular fan along their overlap transitions: the charts, their overlap loci and the overlap transitions, together with the identity, triple-overlap and cocycle laws.

@[simp]

theorem TauCeti.Toric.Fan.analyticGlueData_J {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) : (Φ.analyticGlueData hΦ).J = ↑Φ.cones

The gluing data is indexed by the cones of the fan.

@[simp]

theorem TauCeti.Toric.Fan.analyticGlueData_U {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : (Φ.analyticGlueData hΦ).U σ = Φ.analyticAffineChartDiagram.obj σ

The space of the gluing data at a cone is its affine analytic chart.

@[simp]

theorem TauCeti.Toric.Fan.analyticGlueData_V {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : (Φ.analyticGlueData hΦ).V (σ, τ) = (TopologicalSpace.Opens.toTopCat (Φ.analyticAffineChartDiagram.obj σ)).obj (Φ.analyticOverlapOpens hΦ σ τ)

The overlap space of the gluing data at two cones is the overlap open set of the first chart with the second.

@[simp]

theorem TauCeti.Toric.Fan.analyticGlueData_f {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : (Φ.analyticGlueData hΦ).f σ τ = (Φ.analyticOverlapOpens hΦ σ τ).inclusion'

The overlap space of the gluing data embeds into the first chart as an open subset.

@[simp]

theorem TauCeti.Toric.Fan.analyticGlueData_t {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : (Φ.analyticGlueData hΦ).t σ τ = Φ.analyticOverlapTransition hΦ σ τ

The transition of the gluing data is the overlap transition of the two charts.

The analytic realization

@[reducible, inline]

noncomputable abbrev TauCeti.Toric.Fan.analyticRealization {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) : TopCat

The analytic realization of a regular fan: the space obtained by gluing its affine analytic charts along their overlap transitions.

noncomputable def TauCeti.Toric.Fan.analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : Φ.analyticAffineChartDiagram.obj σ ⟶ Φ.analyticRealization hΦ

The inclusion of the affine analytic chart of a cone into the analytic realization.

theorem TauCeti.Toric.Fan.analyticAffineChartι_def {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : Φ.analyticAffineChartι hΦ σ = (Φ.analyticGlueData hΦ).ι σ

The chart inclusion is the inclusion of the gluing data at the cone.

theorem TauCeti.Toric.Fan.isOpenEmbedding_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ))

Each affine analytic chart is an open subspace of the analytic realization.

theorem TauCeti.Toric.Fan.exists_analyticAffineChartι_apply_eq {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (x : ↑(Φ.analyticRealization hΦ)) : ∃ (σ : ↑Φ.cones) (y : ↑(Φ.analyticAffineChartDiagram.obj σ)), (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) y = x

Every point of the analytic realization lies in one of the affine analytic charts.

@[simp]

theorem TauCeti.Toric.Fan.isEmpty_analyticRealization_iff {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) : IsEmpty ↑(Φ.analyticRealization hΦ) ↔ IsEmpty ↑Φ.cones

The analytic realization is empty exactly when the fan has no cones: every affine chart is nonempty, and the charts cover the realization.

instance TauCeti.Toric.Fan.instIsEmptyCarrierAnalyticRealizationOfElemPointedConeRealCones {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) [IsEmpty ↑Φ.cones] : IsEmpty ↑(Φ.analyticRealization hΦ)

The analytic realization of a fan with no cones, such as the empty subfan of any fan, is empty.

theorem TauCeti.Toric.Fan.analyticRealization_hom_ext {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {Z : TopCat} {g g' : Φ.analyticRealization hΦ ⟶ Z} (h : ∀ (σ : ↑Φ.cones), CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartι hΦ σ) g = CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartι hΦ σ) g') : g = g'

Two maps out of the analytic realization agree when they agree on every affine analytic chart.

theorem TauCeti.Toric.Fan.isOpen_iff_forall_preimage_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (s : Set ↑(Φ.analyticRealization hΦ)) : IsOpen s ↔ ∀ (σ : ↑Φ.cones), IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) ⁻¹' s)

A subset of the analytic realization is open exactly when its preimage in every affine analytic chart is open.

theorem TauCeti.Toric.Fan.analyticAffineChartι_eq_analyticAffineChartι_iff {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {σ τ : ↑Φ.cones} (x : ↑(Φ.analyticAffineChartDiagram.obj σ)) (y : ↑(Φ.analyticAffineChartDiagram.obj τ)) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ τ)) y ↔ ∃ (z : ↑(Φ.analyticAffineChartDiagram.obj (σ ⊓ τ))), (CategoryTheory.ConcreteCategory.hom (Φ.analyticOverlapLeft σ τ)) z = x ∧ (CategoryTheory.ConcreteCategory.hom (Φ.analyticOverlapRight σ τ)) z = y

Points of the affine analytic charts of two cones σ and τ have the same image in the analytic realization exactly when they come from a common point of the chart of σ ⊓ τ.

theorem TauCeti.Toric.Fan.analyticAffineChartDiagram_map_comp_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {τ σ : ↑Φ.cones} (f : τ ⟶ σ) : CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartDiagram.map f) (Φ.analyticAffineChartι hΦ σ) = Φ.analyticAffineChartι hΦ τ

The inclusion of the chart of a face factors through the chart diagram map into the chart of the ambient cone.

theorem TauCeti.Toric.Fan.analyticAffineChartDiagram_map_comp_analyticAffineChartι_assoc {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {τ σ : ↑Φ.cones} (f : τ ⟶ σ) {Z : TopCat} (h : Φ.analyticRealization hΦ ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartDiagram.map f) (CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartι hΦ σ) h) = CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartι hΦ τ) h

The inclusion of the chart of a face factors through the chart diagram map into the chart of the ambient cone.

theorem TauCeti.Toric.Fan.analyticAffineChartι_faceAffinePointMap {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {τ σ : ↑Φ.cones} (h : τ ≤ σ) (x : ↑(Φ.analyticAffineChartDiagram.obj τ)) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) (faceAffinePointMap ⋯ ⋯ x) = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ τ)) x

The face-localization map followed by the ambient chart inclusion is the face chart inclusion, for any face inclusion in a regular fan.

theorem TauCeti.Toric.Fan.analyticAffineChartι_faceAffinePointMap_eq {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {υ σ τ : ↑Φ.cones} (hυσ : υ ≤ σ) (hυτ : υ ≤ τ) (x : ↑(Φ.analyticAffineChartDiagram.obj υ)) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) (faceAffinePointMap ⋯ ⋯ x) = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ τ)) (faceAffinePointMap ⋯ ⋯ x)

The face-localization images of a point of a common face have the same image in the analytic realization of the fan.

@[simp]

theorem TauCeti.Toric.Fan.analyticFaceMap_comp_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {τ σ : ↑Φ.cones} (f : τ ⟶ σ) : CategoryTheory.CategoryStruct.comp (Φ.analyticFaceMap f) (Φ.analyticAffineChartι hΦ σ) = Φ.analyticAffineChartι hΦ τ

The inclusion of the chart of a face factors through the analytic face map into the chart of the ambient cone.

@[simp]

theorem TauCeti.Toric.Fan.analyticFaceMap_comp_analyticAffineChartι_assoc {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {τ σ : ↑Φ.cones} (f : τ ⟶ σ) {Z : TopCat} (h : Φ.analyticRealization hΦ ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.analyticFaceMap f) (CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartι hΦ σ) h) = CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartι hΦ τ) h

The associated form of analyticFaceMap_comp_analyticAffineChartι.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapLeft_comp_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : CategoryTheory.CategoryStruct.comp (Φ.analyticOverlapLeft σ τ) (Φ.analyticAffineChartι hΦ σ) = Φ.analyticAffineChartι hΦ (σ ⊓ τ)

The left overlap inclusion followed by its chart inclusion is the inclusion of the chart of the intersection cone.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapLeft_comp_analyticAffineChartι_assoc {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) {Z : TopCat} (h : Φ.analyticRealization hΦ ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.analyticOverlapLeft σ τ) (CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartι hΦ σ) h) = CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartι hΦ (σ ⊓ τ)) h

The left overlap inclusion followed by its chart inclusion is the inclusion of the chart of the intersection cone.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapRight_comp_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : CategoryTheory.CategoryStruct.comp (Φ.analyticOverlapRight σ τ) (Φ.analyticAffineChartι hΦ τ) = Φ.analyticAffineChartι hΦ (σ ⊓ τ)

The right overlap inclusion followed by its chart inclusion is the inclusion of the chart of the intersection cone.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapRight_comp_analyticAffineChartι_assoc {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) {Z : TopCat} (h : Φ.analyticRealization hΦ ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.analyticOverlapRight σ τ) (CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartι hΦ τ) h) = CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartι hΦ (σ ⊓ τ)) h

The right overlap inclusion followed by its chart inclusion is the inclusion of the chart of the intersection cone.

@[simp]

theorem TauCeti.Toric.Fan.analyticAffineChartι_preimage_range {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ τ)) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) = ↑(Φ.analyticOverlapOpens hΦ τ σ)

The preimage in the chart of τ of the chart of σ is the overlap locus of τ with σ.

@[simp]

theorem TauCeti.Toric.Fan.range_analyticAffineChartι_inter_range_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) ∩ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ τ)) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ (σ ⊓ τ)))

Two affine analytic charts meet in the realization exactly in the image of the chart of the intersection cone.