Documentation

TauCeti.Geometry.Toric.Algebraic.Fan.Over

Toric fan schemes over the complex numbers #

The structure morphisms of the affine toric charts descend to a structure morphism from the scheme of a finite fan to Spec ℂ. The chart inclusions and the algebraic maps induced by fan morphisms commute with these structure morphisms. Thus these schemes and maps can be used in Mathlib's category of schemes over Spec ℂ, and their complex points can be expressed as morphisms over Spec ℂ.

The affine structures are Mathlib's AlgebraicGeometry.specOverSpec; the global structure is obtained from the existing colimit of affine toric charts. The construction also applies to the empty fan. The integral lattices are in Type, so their spectra and Spec ℂ are schemes in the same universe; the ambient real vector spaces need not be in Type.

Main declarations #

References #

source
noncomputable def TauCeti.Toric.Fan.algebraicRealizationStructureMap {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) :
Φ.algebraicRealization ⟶ AlgebraicGeometry.Spec ↧ℂ

The structure morphism to Spec ℂ of the scheme of a finite fan.

Instances For
    source
    @[instance_reducible]
    noncomputable instance TauCeti.Toric.Fan.algebraicRealizationOver {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) :
    Φ.algebraicRealization.Over (AlgebraicGeometry.Spec ↧ℂ)

    The canonical structure over Spec ℂ on the scheme of a finite fan, induced by the complex-algebra structures on its affine coordinate rings.

    source
    theorem TauCeti.Toric.Fan.algebraicRealization_over {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) :
    Φ.algebraicRealization ↘ AlgebraicGeometry.Spec ↧ℂ = Φ.algebraicRealizationStructureMap

    The canonical complex structure morphism is the descended structure morphism.

    source
    instance TauCeti.Toric.Fan.isOver_affineToricChartι {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) :
    AlgebraicGeometry.Scheme.Hom.IsOver (Φ.affineToricChartι σ) (AlgebraicGeometry.Spec ↧ℂ)

    Each affine toric chart inclusion respects the complex-scheme structures.

    source
    theorem TauCeti.Toric.Fan.affineToricChartι_comp_algebraicRealizationStructureMap {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) :
    CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) Φ.algebraicRealizationStructureMap = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing ⋯ ↑σ)))

    Composing an affine chart inclusion with the global structure morphism gives the structure morphism of the affine chart.

    source
    theorem TauCeti.Toric.Fan.affineToricChartι_comp_algebraicRealizationStructureMap_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (σ : ↑Φ.cones) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧ℂ ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (Φ.affineToricChartι σ) (CategoryTheory.CategoryStruct.comp Φ.algebraicRealizationStructureMap h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ℂ (affineCoordinateRing ⋯ ↑σ)))) h

    Composing an affine chart inclusion with the global structure morphism gives the structure morphism of the affine chart.

    source
    instance TauCeti.Toric.FanHom.isOver_algebraicMap {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {N' : Type} {V' : Type u_2} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) :
    AlgebraicGeometry.Scheme.Hom.IsOver f.algebraicMap (AlgebraicGeometry.Spec ↧ℂ)

    The algebraic morphism induced by a fan morphism respects the complex-scheme structures.

    source
    @[simp]
    theorem TauCeti.Toric.FanHom.algebraicMap_comp_algebraicRealizationStructureMap {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {N' : Type} {V' : Type u_2} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) :
    CategoryTheory.CategoryStruct.comp f.algebraicMap Ψ.algebraicRealizationStructureMap = Φ.algebraicRealizationStructureMap

    The algebraic morphism induced by a fan morphism commutes with the structure morphisms of the two fan schemes to Spec ℂ.

    source
    @[simp]
    theorem TauCeti.Toric.FanHom.algebraicMap_comp_algebraicRealizationStructureMap_assoc {N : Type} {V : Type u_1} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {N' : Type} {V' : Type u_2} [AddCommGroup N'] [AddCommGroup V'] [Module ℝ V'] {i' : N' →+ V'} {Φ : Fan i} {Ψ : Fan i'} (f : FanHom Φ Ψ) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧ℂ ⟶ Z) :
    CategoryTheory.CategoryStruct.comp f.algebraicMap (CategoryTheory.CategoryStruct.comp Ψ.algebraicRealizationStructureMap h) = CategoryTheory.CategoryStruct.comp Φ.algebraicRealizationStructureMap h

    The algebraic morphism induced by a fan morphism commutes with the structure morphisms of the two fan schemes to Spec ℂ.