Documentation

TauCeti.Geometry.Toric.Analytic.AffinePoint.Basic

Complex points of an affine semigroup and their monomial-embedding topology #

The complex points of the affine scheme of a commutative additive monoid S are the ℂ-algebra homomorphisms ℂ[S] →ₐ[ℂ] ℂ out of the monoid algebra, equivalently the multiplicative characters Multiplicative S →* ℂ. Evaluating such a point on a finite family g : Fin r → S that generates S as an additive monoid gives a map into ℂ^r, and the topology of the complex points is the one induced by that map.

This file constructs that topology and proves the facts a chart needs before any coordinates are chosen: the evaluation map is injective, its range is the closed subset of ℂ^r cut out by the binomial relations of the generating family, and the induced topology does not depend on which finite generating family is used. Consequently the complex points form a Hausdorff, second countable, locally compact space, and evaluation at every monomial is continuous.

Independence of the generating family is what makes the space, rather than one presentation of it, the object of study: a semigroup that arises as the dual of a cone has no preferred finite generating family, and later coordinate descriptions must be compared with a topology that was not defined using them.

The construction is contravariantly functorial in the semigroup: a homomorphism S →+ T pulls the complex points of T back to those of S through the induced map of monoid algebras, and the pulled-back map is continuous whichever generating families topologize the two sides. These are the maps by which face localizations and morphisms of fans act on affine charts, and an isomorphism of semigroups, such as a choice of coordinates on the dual semigroup of a regular cone, induces a homeomorphism.

Main declarations #

References #

source
@[reducible, inline]
abbrev TauCeti.Toric.AffineSemigroupComplexPoint (S : Type u_2) [AddCommMonoid S] :
Type u_2

The complex points of the affine scheme attached to a commutative additive monoid S: the ℂ-algebra homomorphisms out of the monoid algebra of S. This is the functor-of-points carrier; no topology is part of the data.

Instances For
    source
    @[instance_reducible]
    noncomputable instance TauCeti.Toric.instInhabitedAffineSemigroupComplexPoint {S : Type u_1} [AddCommMonoid S] :
    Inhabited (AffineSemigroupComplexPoint S)

    The complex points of every affine semigroup are inhabited: the distinguished point sends every monomial to 1.

    source
    theorem TauCeti.Toric.default_def {S : Type u_1} [AddCommMonoid S] :
    default = (MonoidAlgebra.lift ℂ ℂ (Multiplicative S)) 1

    The distinguished complex point is the algebra homomorphism induced by the trivial character.

    source
    @[simp]
    theorem TauCeti.Toric.default_apply_single {S : Type u_1} [AddCommMonoid S] (s : S) :
    default (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) = 1

    The distinguished complex point takes the value 1 on every monomial.

    source
    theorem TauCeti.Toric.AffineSemigroupComplexPoint.ext {S : Type u_1} [AddCommMonoid S] {x y : AffineSemigroupComplexPoint S} (h : ∀ (s : S), x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) = y (MonoidAlgebra.single (Multiplicative.ofAdd s) 1)) :
    x = y

    Two complex points of S that agree on every monomial are equal.

    source
    theorem TauCeti.Toric.AffineSemigroupComplexPoint.ext_iff {S : Type u_1} [AddCommMonoid S] {x y : AffineSemigroupComplexPoint S} :
    x = y ↔ ∀ (s : S), x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) = y (MonoidAlgebra.single (Multiplicative.ofAdd s) 1)
    source
    theorem TauCeti.Toric.AffineSemigroupComplexPoint.apply_single_add {S : Type u_1} [AddCommMonoid S] (x : AffineSemigroupComplexPoint S) (s t : S) :
    x (MonoidAlgebra.single (Multiplicative.ofAdd (s + t)) 1) = x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) * x (MonoidAlgebra.single (Multiplicative.ofAdd t) 1)

    A complex point is multiplicative on monomials: its value on the monomial of a sum is the product of its values on the monomials of the summands.

    source
    theorem TauCeti.Toric.AffineSemigroupComplexPoint.apply_single_nsmul {S : Type u_1} [AddCommMonoid S] (x : AffineSemigroupComplexPoint S) (n : ℕ) (s : S) :
    x (MonoidAlgebra.single (Multiplicative.ofAdd (n • s)) 1) = x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) ^ n

    The value of a complex point on the monomial of a multiple is the corresponding power of its value on the monomial.

    source
    structure TauCeti.Toric.AddGeneratingFamily (S : Type u_2) [AddCommMonoid S] (r : ℕ) :
    Type u_2

    A finite family generating a commutative additive monoid. The affine complex points of S are topologized through evaluation on such a family, so the chosen indexed family, and not just the finite generation of S, is part of the data.

    Instances For
      source
      theorem TauCeti.Toric.AddGeneratingFamily.ext_iff {S : Type u_2} {inst✝ : AddCommMonoid S} {r : ℕ} {x y : AddGeneratingFamily S r} :
      x = y ↔ x.toFun = y.toFun
      source
      theorem TauCeti.Toric.AddGeneratingFamily.ext {S : Type u_2} {inst✝ : AddCommMonoid S} {r : ℕ} {x y : AddGeneratingFamily S r} (toFun : x.toFun = y.toFun) :
      x = y
      source
      theorem TauCeti.Toric.AddGeneratingFamily.fg {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) :
      AddMonoid.FG S

      A monoid with a finite generating family is finitely generated.

      source
      theorem TauCeti.Toric.exists_addGeneratingFamily (S : Type u_2) [AddCommMonoid S] [AddMonoid.FG S] :
      ∃ (r : ℕ), Nonempty (AddGeneratingFamily S r)

      Conversely, a finitely generated additive monoid carries a finite generating family, so the constructions below apply to every finitely generated additive monoid.

      source
      theorem TauCeti.Toric.AddGeneratingFamily.exists_eq_sum {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) (s : S) :
      ∃ (a : Fin r → ℕ), s = ∑ j : Fin r, a j • g.toFun j

      Every element of the monoid is a combination of the generators with natural-number coefficients.

      source
      noncomputable def TauCeti.Toric.monomialEmbedding {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) :
      AffineSemigroupComplexPoint S → Fin r → ℂ

      Evaluation of the affine complex points of S on a finite generating family.

      Instances For
        source
        @[simp]
        theorem TauCeti.Toric.monomialEmbedding_apply {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) (x : AffineSemigroupComplexPoint S) (j : Fin r) :
        monomialEmbedding g x j = x (MonoidAlgebra.single (Multiplicative.ofAdd (g.toFun j)) 1)

        The j-th coordinate of the monomial embedding is evaluation at the monomial of the j-th generator.

        source
        theorem TauCeti.Toric.apply_single_eq_prod_monomialEmbedding {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) {s : S} {a : Fin r → ℕ} (ha : s = ∑ j : Fin r, a j • g.toFun j) (x : AffineSemigroupComplexPoint S) :
        x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) = ∏ j : Fin r, monomialEmbedding g x j ^ a j

        Evaluation at any monomial is a monomial in the coordinates of a monomial embedding, with exponents given by any expression of the monoid element through the generating family.

        source
        theorem TauCeti.Toric.monomialEmbedding_injective {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) :
        Function.Injective (monomialEmbedding g)

        An affine complex point is determined by its values on a finite generating family.

        source
        theorem TauCeti.Toric.range_monomialEmbedding {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) :
        Set.range (monomialEmbedding g) = {z : Fin r → ℂ | ∀ (a b : Fin r → ℕ), ∑ j : Fin r, a j • g.toFun j = ∑ j : Fin r, b j • g.toFun j → ∏ j : Fin r, z j ^ a j = ∏ j : Fin r, z j ^ b j}

        The range of a monomial embedding is the locus of the binomial relations of the generating family: a point of ℂ^r extends to an affine complex point exactly when every additive relation between the generators is matched by the corresponding multiplicative relation.

        source
        theorem TauCeti.Toric.isClosed_range_monomialEmbedding {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) :
        IsClosed (Set.range (monomialEmbedding g))

        The range of a monomial embedding is closed: it is the common zero locus of the differences of the binomials attached to the additive relations of the generating family.

        source
        @[instance_reducible]
        noncomputable def TauCeti.Toric.affinePointTopology {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) :
        TopologicalSpace (AffineSemigroupComplexPoint S)

        The topology on the affine complex points of S induced by evaluation on a finite generating family. It is independent of the family by affinePointTopology_eq.

        Instances For
          source
          theorem TauCeti.Toric.continuous_monomialEmbedding {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) :
          Continuous (monomialEmbedding g)

          The monomial embedding is continuous for the topology it induces.

          source
          theorem TauCeti.Toric.continuous_apply_single {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) (s : S) :
          Continuous fun (x : AffineSemigroupComplexPoint S) => x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1)

          Evaluation at a fixed monomial is continuous for the monomial-embedding topology: it is a monomial in the coordinates of the embedding.

          source
          theorem TauCeti.Toric.continuous_eval_const {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) (f : MonoidAlgebra ℂ (Multiplicative S)) :
          Continuous fun (x : AffineSemigroupComplexPoint S) => x f

          Evaluation at a fixed element of the coordinate ring is continuous for the monomial-embedding topology: such an element is a finite linear combination of monomials, and evaluation at each monomial is continuous.

          source
          theorem TauCeti.Toric.affinePointTopology_eq_iInf {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) :
          affinePointTopology g = ⨅ (s : S), TopologicalSpace.induced (fun (x : AffineSemigroupComplexPoint S) => x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1)) inferInstance

          The monomial-embedding topology is the coarsest one making evaluation at every monomial continuous. This description mentions no generating family, so it identifies the topologies induced by any two of them.

          source
          theorem TauCeti.Toric.continuous_iff_forall_continuous_apply_single {S : Type u_1} [AddCommMonoid S] {r : ℕ} {X : Type u_2} [TopologicalSpace X] (g : AddGeneratingFamily S r) (φ : X → AffineSemigroupComplexPoint S) :
          Continuous φ ↔ ∀ (s : S), Continuous fun (x : X) => (φ x) (MonoidAlgebra.single (Multiplicative.ofAdd s) 1)

          A map into the affine complex points is continuous for the monomial-embedding topology exactly when its composite with evaluation at every monomial is continuous.

          source
          theorem TauCeti.Toric.affinePointTopology_eq {S : Type u_1} [AddCommMonoid S] {r r' : ℕ} (g : AddGeneratingFamily S r) (h : AddGeneratingFamily S r') :
          affinePointTopology g = affinePointTopology h

          The monomial-embedding topology does not depend on the chosen finite generating family.

          source
          theorem TauCeti.Toric.isClosedEmbedding_monomialEmbedding {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) :
          Topology.IsClosedEmbedding (monomialEmbedding g)

          A monomial embedding is a closed embedding for the topology it induces.

          source
          theorem TauCeti.Toric.t2Space_affinePointTopology {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) :
          T2Space (AffineSemigroupComplexPoint S)

          The affine complex points of a finitely generated additive monoid are Hausdorff.

          source
          theorem TauCeti.Toric.secondCountableTopology_affinePointTopology {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) :
          SecondCountableTopology (AffineSemigroupComplexPoint S)

          The affine complex points of a finitely generated additive monoid are second countable.

          source
          theorem TauCeti.Toric.locallyCompactSpace_affinePointTopology {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) :
          LocallyCompactSpace (AffineSemigroupComplexPoint S)

          The affine complex points of a finitely generated additive monoid are locally compact: the monomial embedding realizes them as a closed subset of a complex affine space.

          source
          theorem TauCeti.Toric.isCompact_setOf_forall_norm_apply_single_toFun_le {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) (R : ℝ) :
          IsCompact {x : AffineSemigroupComplexPoint S | ∀ (j : Fin r), ‖x (MonoidAlgebra.single (Multiplicative.ofAdd (g.toFun j)) 1)‖ ≤ R}

          The complex points at which the monomials of a finite generating family have absolute value at most R form a compact set: it is the preimage of a closed polydisc under the monomial embedding, which is a closed embedding.

          source
          theorem TauCeti.Toric.isCompact_setOf_forall_norm_apply_single_le_one {S : Type u_1} [AddCommMonoid S] {r : ℕ} (g : AddGeneratingFamily S r) :
          IsCompact {x : AffineSemigroupComplexPoint S | ∀ (s : S), ‖x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1)‖ ≤ 1}

          The complex points at which every monomial has absolute value at most 1 form a compact set. For the dual semigroup of a cone, this is the part of the affine chart lying over the cone under the logarithm of absolute values; for a complete fan these parts of the charts cover the analytic realization.

          Functoriality in the semigroup #

          source
          noncomputable def TauCeti.Toric.AffineSemigroupComplexPoint.comap {S : Type u_1} [AddCommMonoid S] {T : Type u_2} [AddCommMonoid T] (f : S →+ T) :
          AffineSemigroupComplexPoint T → AffineSemigroupComplexPoint S

          The map on affine complex points induced by a homomorphism f : S →+ T of additive monoids: a point of T is pulled back to a point of S by precomposing it with the map ℂ[S] → ℂ[T] of monoid algebras induced by f. The construction is contravariant in the semigroup.

          Instances For
            source
            @[simp]
            theorem TauCeti.Toric.AffineSemigroupComplexPoint.comap_apply {S : Type u_1} [AddCommMonoid S] {T : Type u_2} [AddCommMonoid T] (f : S →+ T) (x : AffineSemigroupComplexPoint T) (a : MonoidAlgebra ℂ (Multiplicative S)) :
            (comap f x) a = x ((MonoidAlgebra.mapDomainAlgHom ℂ ℂ (AddMonoidHom.toMultiplicative f)) a)

            The pulled-back point is the original point composed with the induced map of monoid algebras.

            source
            theorem TauCeti.Toric.AffineSemigroupComplexPoint.comap_apply_single {S : Type u_1} [AddCommMonoid S] {T : Type u_2} [AddCommMonoid T] (f : S →+ T) (x : AffineSemigroupComplexPoint T) (s : S) :
            (comap f x) (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) = x (MonoidAlgebra.single (Multiplicative.ofAdd (f s)) 1)

            The pulled-back point takes the value of the original point on the image monomial.

            source
            @[simp]
            theorem TauCeti.Toric.AffineSemigroupComplexPoint.comap_default {S : Type u_1} [AddCommMonoid S] {T : Type u_2} [AddCommMonoid T] (f : S →+ T) :
            comap f default = default

            Pulling back preserves the distinguished point whose monomial values are all one.

            source
            @[simp]
            theorem TauCeti.Toric.AffineSemigroupComplexPoint.comap_id {S : Type u_1} [AddCommMonoid S] :
            comap (AddMonoidHom.id S) = id

            Pulling back along the identity does nothing.

            source
            @[simp]
            theorem TauCeti.Toric.AffineSemigroupComplexPoint.comap_comap {S : Type u_1} [AddCommMonoid S] {T : Type u_2} {U : Type u_3} [AddCommMonoid T] [AddCommMonoid U] (f : S →+ T) (f' : T →+ U) (x : AffineSemigroupComplexPoint U) :
            comap f (comap f' x) = comap (f'.comp f) x

            Pulling back along two homomorphisms in turn is pulling back along their composite.

            source
            theorem TauCeti.Toric.AffineSemigroupComplexPoint.comap_comp {S : Type u_1} [AddCommMonoid S] {T : Type u_2} {U : Type u_3} [AddCommMonoid T] [AddCommMonoid U] (f : S →+ T) (f' : T →+ U) :
            comap (f'.comp f) = comap f ∘ comap f'

            The pullback of complex points is contravariant for composition.

            source
            theorem TauCeti.Toric.AffineSemigroupComplexPoint.continuous_comap {S : Type u_1} [AddCommMonoid S] {r r' : ℕ} {T : Type u_2} [AddCommMonoid T] (g : AddGeneratingFamily S r) (h : AddGeneratingFamily T r') (f : S →+ T) :
            Continuous (comap f)

            The map induced by a homomorphism of additive monoids is continuous for the monomial-embedding topologies attached to any finite generating families of the source and the target.

            source
            noncomputable def TauCeti.Toric.AffineSemigroupComplexPoint.comapEquiv {S : Type u_1} [AddCommMonoid S] {T : Type u_2} [AddCommMonoid T] (e : S ≃+ T) :
            AffineSemigroupComplexPoint T ≃ AffineSemigroupComplexPoint S

            An isomorphism of additive monoids induces a bijection between their affine complex points.

            Instances For
              source
              @[simp]
              theorem TauCeti.Toric.AffineSemigroupComplexPoint.coe_comapEquiv {S : Type u_1} [AddCommMonoid S] {T : Type u_2} [AddCommMonoid T] (e : S ≃+ T) :
              ⇑(comapEquiv e) = comap ↑e
              source
              @[simp]
              theorem TauCeti.Toric.AffineSemigroupComplexPoint.comapEquiv_symm {S : Type u_1} [AddCommMonoid S] {T : Type u_2} [AddCommMonoid T] (e : S ≃+ T) :
              (comapEquiv e).symm = comapEquiv e.symm
              source
              noncomputable def TauCeti.Toric.AffineSemigroupComplexPoint.comapHomeomorph {S : Type u_1} [AddCommMonoid S] {r r' : ℕ} {T : Type u_2} [AddCommMonoid T] (e : S ≃+ T) (g : AddGeneratingFamily S r) (h : AddGeneratingFamily T r') :
              AffineSemigroupComplexPoint T ≃ₜ AffineSemigroupComplexPoint S

              An isomorphism of additive monoids induces a homeomorphism between their affine complex points, for the monomial-embedding topologies attached to any finite generating families.

              Instances For
                source
                @[simp]
                theorem TauCeti.Toric.AffineSemigroupComplexPoint.coe_comapHomeomorph {S : Type u_1} [AddCommMonoid S] {r r' : ℕ} {T : Type u_2} [AddCommMonoid T] (e : S ≃+ T) (g : AddGeneratingFamily S r) (h : AddGeneratingFamily T r') :
                ⇑(comapHomeomorph e g h) = comap ↑e
                source
                @[simp]
                theorem TauCeti.Toric.AffineSemigroupComplexPoint.comapHomeomorph_symm {S : Type u_1} [AddCommMonoid S] {r r' : ℕ} {T : Type u_2} [AddCommMonoid T] (e : S ≃+ T) (g : AddGeneratingFamily S r) (h : AddGeneratingFamily T r') :
                (comapHomeomorph e g h).symm = comapHomeomorph e.symm h g

                Points of a join of submonoids #

                source
                theorem TauCeti.Toric.AffineSemigroupComplexPoint.exists_comap_inclusion_eq_iff {M : Type u_2} [AddCommMonoid M] {S₁ S₂ S₃ : AddSubmonoid M} (h₁ : S₁ ≤ S₃) (h₂ : S₂ ≤ S₃) (h₃ : S₃ ≤ S₁ ⊔ S₂) (x : AffineSemigroupComplexPoint ↥S₁) (y : AffineSemigroupComplexPoint ↥S₂) :
                (∃ (z : AffineSemigroupComplexPoint ↥S₃), comap (AddSubmonoid.inclusion h₁) z = x ∧ comap (AddSubmonoid.inclusion h₂) z = y) ↔ ∀ (s s' : ↥S₁) (t t' : ↥S₂), ↑s + ↑t = ↑s' + ↑t' → x (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) * y (MonoidAlgebra.single (Multiplicative.ofAdd t) 1) = x (MonoidAlgebra.single (Multiplicative.ofAdd s') 1) * y (MonoidAlgebra.single (Multiplicative.ofAdd t') 1)

                Let S₃ be a submonoid generated by two submonoids S₁ and S₂ that it contains. A point of S₁ and a point of S₂ are the restrictions of a common point of S₃ exactly when they are compatible with every additive relation s + t = s' + t' between elements of S₁ and of S₂. For the dual semigroups of two cones meeting in a common face, this describes the chart of the common face inside the product of the two charts by binomial equations.

                source
                theorem TauCeti.Toric.AffineSemigroupComplexPoint.isClosed_setOf_exists_comap_inclusion_eq {r r' : ℕ} {M : Type u_2} [AddCommMonoid M] {S₁ S₂ S₃ : AddSubmonoid M} (h₁ : S₁ ≤ S₃) (h₂ : S₂ ≤ S₃) (h₃ : S₃ ≤ S₁ ⊔ S₂) (g : AddGeneratingFamily (↥S₁) r) (h : AddGeneratingFamily (↥S₂) r') :
                IsClosed {p : AffineSemigroupComplexPoint ↥S₁ × AffineSemigroupComplexPoint ↥S₂ | ∃ (z : AffineSemigroupComplexPoint ↥S₃), comap (AddSubmonoid.inclusion h₁) z = p.1 ∧ comap (AddSubmonoid.inclusion h₂) z = p.2}

                Let S₃ be a submonoid generated by two submonoids S₁ and S₂ that it contains. The pairs consisting of a point of S₁ and a point of S₂ that are restrictions of a common point of S₃ form a closed subset of the product of the two monomial-embedding topologies.