Transitions between the overlap loci of analytic toric charts

The two overlap loci of a pair of cones are open subspaces of the two affine charts, and the overlap homeomorphisms of TauCeti.Toric.Fan.analyticOverlapHomeomorph are homeomorphisms between them. This file views each transition as a morphism of the overlap loci, so that the TopCat.GlueData of the analytic fan can be built from the same transitions that are already recorded on the analytic charts. A transition acts as the overlap homeomorphism it is built from, and its identity and inverse laws are recorded here as equations of morphisms.

References

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

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

The transition between the two overlap loci of two cones, as a morphism of spaces.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapTransition_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) (x : ↑((TopologicalSpace.Opens.toTopCat (Φ.analyticAffineChartDiagram.obj σ)).obj (Φ.analyticOverlapOpens hΦ σ τ))) : (CategoryTheory.ConcreteCategory.hom (Φ.analyticOverlapTransition hΦ σ τ)) x = (Φ.analyticOverlapHomeomorph hΦ σ τ) x

A transition applies as the overlap homeomorphism it is built from.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapTransition_self {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ : ↑Φ.cones) : Φ.analyticOverlapTransition hΦ σ σ = CategoryTheory.CategoryStruct.id ((TopologicalSpace.Opens.toTopCat (Φ.analyticAffineChartDiagram.obj σ)).obj (Φ.analyticOverlapOpens hΦ σ σ))

The transition across the overlap of a cone with itself is the identity.

@[simp]

theorem TauCeti.Toric.Fan.analyticOverlapTransition_trans_symm {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (σ τ : ↑Φ.cones) : CategoryTheory.CategoryStruct.comp (Φ.analyticOverlapTransition hΦ σ τ) (Φ.analyticOverlapTransition hΦ τ σ) = CategoryTheory.CategoryStruct.id ((TopologicalSpace.Opens.toTopCat (Φ.analyticAffineChartDiagram.obj σ)).obj (Φ.analyticOverlapOpens hΦ σ τ))

A transition followed by the reverse transition is the identity on the first overlap locus.