Toric maps of analytic realizations

A morphism of fans f : FanHom Φ Ψ carries every cone σ of Φ into a cone υ of Ψ. Precomposition of characters with the lattice map of f sends the dual semigroup of υ to the dual semigroup of σ, and pulling complex points back along this map of semigroups gives a continuous map from the affine analytic chart of σ to the affine analytic chart of υ. Viewed in the analytic realization of Ψ, these chart maps do not depend on the target cone υ, and they commute with the face maps of the source fan. They therefore glue to a continuous map FanHom.analyticMap between the analytic realizations of two regular fans, the analytic counterpart of the morphism of toric schemes TauCeti.Toric.FanHom.algebraicMap.

On the chart of a cone σ the glued map is the chart map into the chart of the least target cone TauCeti.Toric.FanHom.leastCone, or equivalently into the chart of any target cone containing the image of σ. The construction is functorial: the identity morphism of a fan induces the identity, and a composite of fan morphisms induces the composite map. The inclusion of an open subfan induces the open-subfan map TauCeti.Toric.Fan.subfanAnalyticMap, so the open-subfan maps inherit this functoriality: on all the cones of a fan the open-subfan map is the identity, and for nested open subfans the open-subfan maps compose.

Main declarations

• TauCeti.Toric.FanHom.analyticChartMap: the map of affine analytic charts induced by a fan morphism and a target cone containing the image of the source cone.
• TauCeti.Toric.FanHom.analyticMap: the continuous map of analytic realizations induced by a morphism of regular fans.
• TauCeti.Toric.FanHom.analyticMap_analyticAffineChartι: its chart formula.
• TauCeti.Toric.FanHom.analyticMap_id and TauCeti.Toric.FanHom.analyticMap_comp: its functoriality.
• TauCeti.Toric.FanHom.analyticMap_subfanInclusion: the inclusion of an open subfan induces the open-subfan map.
• TauCeti.Toric.Fan.subfanAnalyticMap_self and TauCeti.Toric.Fan.subfanAnalyticMap_comp: the functoriality of the open-subfan maps for nested open subfans.

References

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

Chart maps

noncomputable def TauCeti.Toric.FanHom.analyticChartMap {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) {σ : ↑Φ.cones} {υ : ↑Ψ.cones} (h : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑υ) : Φ.analyticAffineChartDiagram.obj σ ⟶ Ψ.analyticAffineChartDiagram.obj υ

The map from the affine analytic chart of a cone σ of Φ to the affine analytic chart of a cone υ of Ψ into which the fan morphism carries σ: complex points are pulled back along the map of dual semigroups induced by the fan morphism.

@[simp]

theorem TauCeti.Toric.FanHom.analyticChartMap_apply {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) {σ : ↑Φ.cones} {υ : ↑Ψ.cones} (h : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑υ) (x : ↑(Φ.analyticAffineChartDiagram.obj σ)) : (CategoryTheory.ConcreteCategory.hom (f.analyticChartMap h)) x = AffineSemigroupComplexPoint.comap (dualSemigroupMap ⋯ ⋯ f.latticeMap f.realMap ⋯ h) x

The chart map pulls a complex point back along the map of dual semigroups.

theorem TauCeti.Toric.FanHom.map_comp_analyticChartMap {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) {τ σ : ↑Φ.cones} {υ : ↑Ψ.cones} (hτσ : τ ⟶ σ) (h : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑υ) : CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartDiagram.map hτσ) (f.analyticChartMap h) = f.analyticChartMap ⋯

Restricting to a face of the source cone and then mapping is mapping from the face.

theorem TauCeti.Toric.FanHom.map_comp_analyticChartMap_assoc {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) {τ σ : ↑Φ.cones} {υ : ↑Ψ.cones} (hτσ : τ ⟶ σ) (h : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑υ) {Z : TopCat} (h✝ : Ψ.analyticAffineChartDiagram.obj υ ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartDiagram.map hτσ) (CategoryTheory.CategoryStruct.comp (f.analyticChartMap h) h✝) = CategoryTheory.CategoryStruct.comp (f.analyticChartMap ⋯) h✝

Restricting to a face of the source cone and then mapping is mapping from the face.

theorem TauCeti.Toric.FanHom.analyticChartMap_comp_map {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) {σ : ↑Φ.cones} {κ υ : ↑Ψ.cones} (h : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑κ) (hκυ : κ ⟶ υ) : CategoryTheory.CategoryStruct.comp (f.analyticChartMap h) (Ψ.analyticAffineChartDiagram.map hκυ) = f.analyticChartMap ⋯

Mapping into a target cone and then restricting to a larger target cone is mapping into the larger cone.

theorem TauCeti.Toric.FanHom.analyticChartMap_comp_map_assoc {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) {σ : ↑Φ.cones} {κ υ : ↑Ψ.cones} (h : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑κ) (hκυ : κ ⟶ υ) {Z : TopCat} (h✝ : Ψ.analyticAffineChartDiagram.obj υ ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.analyticChartMap h) (CategoryTheory.CategoryStruct.comp (Ψ.analyticAffineChartDiagram.map hκυ) h✝) = CategoryTheory.CategoryStruct.comp (f.analyticChartMap ⋯) h✝

Mapping into a target cone and then restricting to a larger target cone is mapping into the larger cone.

theorem TauCeti.Toric.FanHom.analyticChartMap_comp_analyticAffineChartι {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΨ : Ψ.IsRegular) {σ : ↑Φ.cones} {υ υ' : ↑Ψ.cones} (h : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑υ) (h' : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑υ') : CategoryTheory.CategoryStruct.comp (f.analyticChartMap h) (Ψ.analyticAffineChartι hΨ υ) = CategoryTheory.CategoryStruct.comp (f.analyticChartMap h') (Ψ.analyticAffineChartι hΨ υ')

In the analytic realization of the target fan, the chart map does not depend on the target cone into which the source cone is carried.

The glued map

noncomputable def TauCeti.Toric.FanHom.analyticMap {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) : Φ.analyticRealization hΦ ⟶ Ψ.analyticRealization hΨ

The continuous map between the analytic realizations of two regular fans induced by a fan morphism, glued from the chart maps into the charts of the least target cones.

theorem TauCeti.Toric.FanHom.analyticAffineChartι_comp_analyticMap {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) {σ : ↑Φ.cones} {υ : ↑Ψ.cones} (h : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑υ) : CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartι hΦ σ) (f.analyticMap hΦ hΨ) = CategoryTheory.CategoryStruct.comp (f.analyticChartMap h) (Ψ.analyticAffineChartι hΨ υ)

On the chart of a cone σ, the glued map is the chart map into the chart of any target cone υ into which the fan morphism carries σ.

theorem TauCeti.Toric.FanHom.analyticAffineChartι_comp_analyticMap_assoc {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) {σ : ↑Φ.cones} {υ : ↑Ψ.cones} (h : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑υ) {Z : TopCat} (h✝ : Ψ.analyticRealization hΨ ⟶ Z) : CategoryTheory.CategoryStruct.comp (Φ.analyticAffineChartι hΦ σ) (CategoryTheory.CategoryStruct.comp (f.analyticMap hΦ hΨ) h✝) = CategoryTheory.CategoryStruct.comp (f.analyticChartMap h) (CategoryTheory.CategoryStruct.comp (Ψ.analyticAffineChartι hΨ υ) h✝)

On the chart of a cone σ, the glued map is the chart map into the chart of any target cone υ into which the fan morphism carries σ.

theorem TauCeti.Toric.FanHom.analyticMap_analyticAffineChartι_of_mapsTo {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) {σ : ↑Φ.cones} {υ : ↑Ψ.cones} (h : Set.MapsTo ⇑f.realMap ↑↑σ ↑↑υ) (x : ↑(Φ.analyticAffineChartDiagram.obj σ)) : (CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) ((CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x) = (CategoryTheory.ConcreteCategory.hom (Ψ.analyticAffineChartι hΨ υ)) ((CategoryTheory.ConcreteCategory.hom (f.analyticChartMap h)) x)

On a point of the chart of a cone σ, the glued map is the chart map into the chart of any target cone υ into which the fan morphism carries σ.

@[simp]

theorem TauCeti.Toric.FanHom.analyticMap_analyticAffineChartι {N N' V V' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup V] [AddCommGroup V'] [Module ℝ V] [Module ℝ V'] {i : N →+ V} {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) (σ : ↑Φ.cones) (x : ↑(Φ.analyticAffineChartDiagram.obj σ)) : (CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) ((CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x) = (CategoryTheory.ConcreteCategory.hom (Ψ.analyticAffineChartι hΨ ⟨f.leastCone ⋯, ⋯⟩)) ((CategoryTheory.ConcreteCategory.hom (f.analyticChartMap ⋯)) x)

On a point of the chart of a cone σ, the glued map is the chart map into the chart of the least target cone TauCeti.Toric.FanHom.leastCone. This is the analytic counterpart of TauCeti.Toric.FanHom.affineToricChartι_comp_algebraicMap.

Functoriality

@[simp]

theorem TauCeti.Toric.FanHom.analyticMap_id {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) : (FanHom.id Φ).analyticMap hΦ hΦ = CategoryTheory.CategoryStruct.id (Φ.analyticRealization hΦ)

The identity morphism of a regular fan induces the identity of its analytic realization.

theorem TauCeti.Toric.FanHom.analyticMap_comp {N N' N'' V V' V'' : Type u} [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [AddCommGroup V] [AddCommGroup V'] [AddCommGroup V''] [Module ℝ V] [Module ℝ V'] [Module ℝ V''] {i : N →+ V} {i' : N' →+ V'} {i'' : N'' →+ V''} {Φ : Fan i} {Ψ : Fan i'} {Ω : Fan i''} (f : FanHom Φ Ψ) (hΦ : Φ.IsRegular) (hΨ : Ψ.IsRegular) (g : FanHom Ψ Ω) (hΩ : Ω.IsRegular) : (g.comp f).analyticMap hΦ hΩ = CategoryTheory.CategoryStruct.comp (f.analyticMap hΦ hΨ) (g.analyticMap hΨ hΩ)

A composite of morphisms of regular fans induces the composite of the analytic maps.

theorem TauCeti.Toric.FanHom.analyticMap_subfanInclusion {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {Φ : Fan i} (hΦ : Φ.IsRegular) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) : (Φ.subfanInclusion S hS hface).analyticMap ⋯ hΦ = Φ.subfanAnalyticMap hΦ S hS hface

The inclusion of an open subfan induces the open-subfan map of analytic realizations.

Functoriality of open-subfan maps

@[simp]

theorem TauCeti.Toric.Fan.subfanAnalyticMap_self {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) : Φ.subfanAnalyticMap hΦ Φ.cones ⋯ ⋯ = CategoryTheory.CategoryStruct.id (Φ.analyticRealization hΦ)

The open-subfan map of a fan on all of its cones is the identity of its analytic realization.

theorem TauCeti.Toric.Fan.subfanAnalyticMap_comp {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) (T : Set (PointedCone ℝ V)) (hT : T ⊆ (Φ.subfan S hS hface).cones) (hfaceT : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ T → τ.IsFaceOf σ → τ ∈ T) : CategoryTheory.CategoryStruct.comp ((Φ.subfan S hS hface).subfanAnalyticMap ⋯ T hT hfaceT) (Φ.subfanAnalyticMap hΦ S hS hface) = Φ.subfanAnalyticMap hΦ T ⋯ hfaceT

The open-subfan maps are functorial for nested open subfans: mapping the realization of a subfan T of the subfan Φ.subfan S hS hface into the realization of Φ.subfan S hS hface, and then into the realization of Φ, is the open-subfan map of T as a subfan of Φ.

theorem TauCeti.Toric.Fan.subfanAnalyticMap_comp_assoc {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) (T : Set (PointedCone ℝ V)) (hT : T ⊆ (Φ.subfan S hS hface).cones) (hfaceT : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ T → τ.IsFaceOf σ → τ ∈ T) {Z : TopCat} (h : Φ.analyticRealization hΦ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((Φ.subfan S hS hface).subfanAnalyticMap ⋯ T hT hfaceT) (CategoryTheory.CategoryStruct.comp (Φ.subfanAnalyticMap hΦ S hS hface) h) = CategoryTheory.CategoryStruct.comp (Φ.subfanAnalyticMap hΦ T ⋯ hfaceT) h

The open-subfan maps are functorial for nested open subfans: mapping the realization of a subfan T of the subfan Φ.subfan S hS hface into the realization of Φ.subfan S hS hface, and then into the realization of Φ, is the open-subfan map of T as a subfan of Φ.

@[simp]

theorem TauCeti.Toric.Fan.subfanAnalyticMap_subfanAnalyticMap {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (S : Set (PointedCone ℝ V)) (hS : S ⊆ Φ.cones) (hface : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ S → τ.IsFaceOf σ → τ ∈ S) (T : Set (PointedCone ℝ V)) (hT : T ⊆ (Φ.subfan S hS hface).cones) (hfaceT : ∀ ⦃σ τ : PointedCone ℝ V⦄, σ ∈ T → τ.IsFaceOf σ → τ ∈ T) (x : ↑(((Φ.subfan S hS hface).subfan T hT hfaceT).analyticRealization ⋯)) : (CategoryTheory.ConcreteCategory.hom (Φ.subfanAnalyticMap hΦ S hS hface)) ((CategoryTheory.ConcreteCategory.hom ((Φ.subfan S hS hface).subfanAnalyticMap ⋯ T hT hfaceT)) x) = (CategoryTheory.ConcreteCategory.hom (Φ.subfanAnalyticMap hΦ T ⋯ hfaceT)) x

On points, the open-subfan maps are functorial for nested open subfans.