Documentation

TauCeti.Geometry.Toric.Analytic.Fan.Character

Holomorphic characters on a toric fan realization #

An integral character nonnegative on every cone of a regular fan defines a holomorphic function on its analytic realization. The affine monomial functions agree under face localization, so they descend through the gluing. Their products correspond to sums of characters, and torus translation multiplies them by the corresponding character value. For a nonempty fan, these functions are the unique continuous extensions of the characters on its dense torus. Pullback along a toric map precomposes the character with the map of integral lattices.

References #

source
noncomputable def TauCeti.Toric.Fan.analyticCharacter {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) :
C(↑(Φ.analyticRealization hΦ), ℂ)

The holomorphic monomial function of an integral character nonnegative on every cone. Its restriction to each affine chart is evaluation on the corresponding monomial.

Instances For
    source
    @[simp]
    theorem TauCeti.Toric.Fan.analyticCharacter_analyticAffineChartι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) (σ : ↑Φ.cones) (x : ↑(Φ.analyticAffineChartDiagram.obj σ)) :
    (Φ.analyticCharacter hΦ m hm) ((CategoryTheory.ConcreteCategory.hom (Φ.analyticAffineChartι hΦ σ)) x) = x (MonoidAlgebra.single (Multiplicative.ofAdd ⟨m, ⋯⟩) 1)

    The character function is the expected monomial on every affine chart.

    source
    @[simp]
    theorem TauCeti.Toric.Fan.analyticCharacter_smul {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) (t : ComplexTorus N) (x : ↑(Φ.analyticRealization hΦ)) :
    (Φ.analyticCharacter hΦ m hm) (t • x) = ↑(t m) * (Φ.analyticCharacter hΦ m hm) x

    Character functions transform by their character under torus translation.

    source
    @[simp]
    theorem TauCeti.Toric.Fan.analyticCharacter_zero {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (x : ↑(Φ.analyticRealization hΦ)) :
    (Φ.analyticCharacter hΦ 0 ⋯) x = 1

    The zero character defines the constant function one.

    source
    @[simp]
    theorem TauCeti.Toric.Fan.analyticCharacter_add {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) (m' : IntegralCharacter N) (hm' : ∀ (σ : ↑Φ.cones), m' ∈ dualSemigroup ⋯ ↑σ) (x : ↑(Φ.analyticRealization hΦ)) :
    (Φ.analyticCharacter hΦ (m + m') ⋯) x = (Φ.analyticCharacter hΦ m hm) x * (Φ.analyticCharacter hΦ m' hm') x

    Addition of characters corresponds to multiplication of their holomorphic functions.

    source
    theorem TauCeti.Toric.Fan.contMDiff_analyticCharacter {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) (n : WithTop ℕ∞) :
    have x := Φ.analyticChartedSpace hΦ; ContMDiff (modelWithCornersSelf ℂ (Fin (Module.finrank ℤ N) → ℂ)) (modelWithCornersSelf ℂ ℂ) n ⇑(Φ.analyticCharacter hΦ m hm)

    The glued character function is holomorphic for the canonical complex structure.

    source
    @[simp]
    theorem TauCeti.Toric.Fan.analyticCharacter_analyticTorusι {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) (hΦ0 : Nonempty ↑Φ.cones) (t : ComplexTorus N) :
    (Φ.analyticCharacter hΦ m hm) (Φ.analyticTorusι hΦ hΦ0 t) = ↑(t m)

    The global function restricts to the original character on the dense torus.

    source
    theorem TauCeti.Toric.Fan.eq_analyticCharacter_iff {N V : Type u} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} (Φ : Fan i) (hΦ : Φ.IsRegular) (m : IntegralCharacter N) (hm : ∀ (σ : ↑Φ.cones), m ∈ dualSemigroup ⋯ ↑σ) (hΦ0 : Nonempty ↑Φ.cones) (f : C(↑(Φ.analyticRealization hΦ), ℂ)) :
    f = Φ.analyticCharacter hΦ m hm ↔ ∀ (t : ComplexTorus N), f (Φ.analyticTorusι hΦ hΦ0 t) = ↑(t m)

    A continuous extension of a character from the dense torus is the glued character function. The nonempty hypothesis supplies the dense torus; the construction itself also allows empty fans.

    source
    @[simp]
    theorem TauCeti.Toric.FanHom.analyticCharacter_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) (m : IntegralCharacter N') (hm : ∀ (τ : ↑Ψ.cones), m ∈ dualSemigroup ⋯ ↑τ) (x : ↑(Φ.analyticRealization hΦ)) :
    (Ψ.analyticCharacter hΨ m hm) ((CategoryTheory.ConcreteCategory.hom (f.analyticMap hΦ hΨ)) x) = (Φ.analyticCharacter hΦ (AddMonoidHom.comp m f.latticeMap) ⋯) x

    Pullback of a global holomorphic character along a toric map is the character obtained by precomposition with its integral lattice map. Nonnegativity on the source follows from nonnegativity on the target and the fan-morphism condition.