Cocycle of analytic toric chart overlaps #
The transitions between affine charts of a regular fan preserve triple overlaps and satisfy the cocycle law there. These are the compatibility conditions for gluing the charts as open complex subspaces.
References #
- W. Fulton, Introduction to Toric Varieties, §1.4.
- D. Cox, J. Little and H. Schenck, Toric Varieties, §3.1.
theorem
TauCeti.Toric.Fan.exists_analyticTripleOverlap
{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 σ))
(hτ : x ∈ Φ.analyticOverlapOpens hΦ σ τ)
(hυ : x ∈ Φ.analyticOverlapOpens hΦ σ υ)
:
∃ (z : ↑(Φ.analyticAffineChartDiagram.obj (σ ⊓ τ ⊓ υ))),
(CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartDiagram.map (CategoryTheory.homOfLE ⋯))) z = x
A point in the intersection of two overlap loci comes from the chart of the triple intersection cone.
theorem
TauCeti.Toric.Fan.analyticOverlapHomeomorph_mem
{N : Type u_1}
{V : Type u_2}
[AddCommGroup N]
[AddCommGroup V]
[Module ℝ V]
{i : N →+ V}
(Φ : Fan i)
(hΦ : Φ.IsRegular)
(σ τ υ : ↑Φ.cones)
(x : ↥(Φ.analyticOverlapOpens hΦ σ τ))
(h : ↑x ∈ Φ.analyticOverlapOpens hΦ σ υ)
:
An overlap transition sends the triple overlap of the first and third charts into the overlap of the second and third charts.
theorem
TauCeti.Toric.Fan.analyticOverlapHomeomorph_cocycle
{N : Type u_1}
{V : Type u_2}
[AddCommGroup N]
[AddCommGroup V]
[Module ℝ V]
{i : N →+ V}
(Φ : Fan i)
(hΦ : Φ.IsRegular)
(σ τ υ : ↑Φ.cones)
(x : ↥(Φ.analyticOverlapOpens hΦ σ τ))
(h : ↑x ∈ Φ.analyticOverlapOpens hΦ σ υ)
:
↑((Φ.analyticOverlapHomeomorph hΦ τ υ) ⟨↑((Φ.analyticOverlapHomeomorph hΦ σ τ) x), ⋯⟩) = ↑((Φ.analyticOverlapHomeomorph hΦ σ υ) ⟨↑x, h⟩)
The overlap transitions obey the cocycle law on a triple overlap.