Pairwise overlaps of analytic affine toric charts

For two cones of a regular fan, the affine chart of their intersection embeds openly in each cone chart. Its image is the overlap locus. Interchanging the cones gives a canonical homeomorphism between the two overlap loci, obtained by passing through the intersection chart. These are the open sets and transitions used in the gluing of the analytic fan.

The construction uses the diagram of affine complex points. In particular, the transition is induced by restriction of characters and does not depend on generators chosen to present the affine-point topologies.

References

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

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

The inclusion of the common chart into the first chart.

theorem TauCeti.Toric.Fan.analyticOverlapLeft_def {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : Φ.analyticOverlapLeft σ τ = Φ.analyticAffineChartDiagram.map (CategoryTheory.homOfLE ⋯)

The left overlap inclusion is the diagram map for the meet inequality.

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

The inclusion of the common chart into the second chart.

theorem TauCeti.Toric.Fan.analyticOverlapRight_def {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : Φ.analyticOverlapRight σ τ = Φ.analyticAffineChartDiagram.map (CategoryTheory.homOfLE ⋯)

The right overlap inclusion is the diagram map for the meet inequality.

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

The common chart embeds openly into the first chart.

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

The common chart embeds openly into the second chart.

noncomputable def TauCeti.Toric.Fan.analyticOverlapOpens {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : TopologicalSpace.Opens ↑(Φ.analyticAffineChartDiagram.obj σ)

The open overlap locus in the first affine chart.

@[simp]

theorem TauCeti.Toric.Fan.coe_analyticOverlapOpens {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : ↑(Φ.analyticOverlapOpens hΦ σ τ) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticOverlapLeft σ τ))

The carrier of the overlap open set is the image of the left inclusion.

@[simp]

theorem TauCeti.Toric.Fan.mem_analyticOverlapOpens {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) (x : ↑(Φ.analyticAffineChartDiagram.obj σ)) : x ∈ Φ.analyticOverlapOpens hΦ σ τ ↔ ∃ (y : ↑(Φ.analyticAffineChartDiagram.obj (σ ⊓ τ))), (CategoryTheory.ConcreteCategory.hom (Φ.analyticOverlapLeft σ τ)) y = x

Membership in the overlap means coming from a point of the intersection chart.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapOpens_self {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : Φ.analyticOverlapOpens hΦ σ σ = ⊤

A chart overlaps itself in the whole chart.

noncomputable def TauCeti.Toric.Fan.analyticOverlapSwapIso {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : Φ.analyticAffineChartDiagram.obj (σ ⊓ τ) ≅ Φ.analyticAffineChartDiagram.obj (τ ⊓ σ)

Interchanging the two cones gives an isomorphism of their intersection charts.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapSwapIso_hom {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : (Φ.analyticOverlapSwapIso σ τ).hom = Φ.analyticAffineChartDiagram.map (CategoryTheory.eqToHom ⋯)

The forward swap is the chart diagram applied to the equality σ ⊓ τ = τ ⊓ σ.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapSwapIso_inv {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : (Φ.analyticOverlapSwapIso σ τ).inv = Φ.analyticAffineChartDiagram.map (CategoryTheory.eqToHom ⋯)

The inverse swap is the chart diagram applied to the equality τ ⊓ σ = σ ⊓ τ.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapSwapIso_symm {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : (Φ.analyticOverlapSwapIso σ τ).symm = Φ.analyticOverlapSwapIso τ σ

Reversing the swap exchanges its two orientations.

theorem TauCeti.Toric.Fan.analyticOverlapRight_eq_swap_comp_left {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) : Φ.analyticOverlapRight σ τ = CategoryTheory.CategoryStruct.comp (Φ.analyticOverlapSwapIso σ τ).hom (Φ.analyticOverlapLeft τ σ)

The right overlap inclusion is the left inclusion after interchanging the cones.

theorem TauCeti.Toric.Fan.analyticOverlapRight_apply_eq_left_swapIso_hom_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ τ : ↑Φ.cones) (x : ↑(Φ.analyticAffineChartDiagram.obj (σ ⊓ τ))) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticOverlapRight σ τ)) x = (CategoryTheory.ConcreteCategory.hom (Φ.analyticOverlapLeft τ σ)) ((CategoryTheory.ConcreteCategory.hom (Φ.analyticOverlapSwapIso σ τ).hom) x)

Pointwise, the right inclusion factors through the swapped left inclusion.

theorem TauCeti.Toric.Fan.range_analyticOverlapRight {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (Φ.analyticOverlapRight σ τ)) = ↑(Φ.analyticOverlapOpens hΦ τ σ)

The two orientations of the overlap have the same image in the second chart.

theorem TauCeti.Toric.Fan.analyticOverlapLeft_mem {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) (x : ↑(Φ.analyticAffineChartDiagram.obj (σ ⊓ τ))) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticOverlapLeft σ τ)) x ∈ Φ.analyticOverlapOpens hΦ σ τ

A point of the common chart maps into the first overlap open set.

theorem TauCeti.Toric.Fan.analyticOverlapRight_mem {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) (x : ↑(Φ.analyticAffineChartDiagram.obj (σ ⊓ τ))) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticOverlapRight σ τ)) x ∈ Φ.analyticOverlapOpens hΦ τ σ

A point of the common chart maps into the opposite overlap open set.

noncomputable def TauCeti.Toric.Fan.analyticOverlapHomeomorph {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : ↥(Φ.analyticOverlapOpens hΦ σ τ) ≃ₜ ↥(Φ.analyticOverlapOpens hΦ τ σ)

The transition between the two open overlap loci, induced by their common chart.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapHomeomorph_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) (x : ↑(Φ.analyticAffineChartDiagram.obj (σ ⊓ τ))) : (Φ.analyticOverlapHomeomorph hΦ σ τ) ⟨(CategoryTheory.ConcreteCategory.hom (Φ.analyticOverlapLeft σ τ)) x, ⋯⟩ = ⟨(CategoryTheory.ConcreteCategory.hom (Φ.analyticOverlapRight σ τ)) x, ⋯⟩

On a point represented by the intersection chart, the transition is the other intersection-chart inclusion.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapHomeomorph_symm {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : (Φ.analyticOverlapHomeomorph hΦ σ τ).symm = Φ.analyticOverlapHomeomorph hΦ τ σ

Reversing an overlap transition is the transition in the opposite orientation.

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

The two overlap inclusions of a chart with itself coincide.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapHomeomorph_self {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : Φ.analyticOverlapHomeomorph hΦ σ σ = Homeomorph.refl ↥(Φ.analyticOverlapOpens hΦ σ σ)

The transition across the self-overlap is the identity.

theorem TauCeti.Toric.Fan.mem_analyticOverlapOpens_of_le {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {γ σ τ : ↑Φ.cones} (hγσ : γ ≤ σ) (hγτ : γ ≤ τ) (z : ↑(Φ.analyticAffineChartDiagram.obj γ)) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartDiagram.map (CategoryTheory.homOfLE hγσ))) z ∈ Φ.analyticOverlapOpens hΦ σ τ

A point coming from a common face belongs to the overlap of the two charts.

theorem TauCeti.Toric.Fan.analyticOverlapHomeomorph_apply_of_le {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) {γ σ τ : ↑Φ.cones} (hγσ : γ ≤ σ) (hγτ : γ ≤ τ) (z : ↑(Φ.analyticAffineChartDiagram.obj γ)) : ↑((Φ.analyticOverlapHomeomorph hΦ σ τ) ⟨(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartDiagram.map (CategoryTheory.homOfLE hγσ))) z, ⋯⟩) = (CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartDiagram.map (CategoryTheory.homOfLE hγτ))) z

On a point from a common face, an overlap transition is the chart map into the second cone.