Documentation

TauCeti.Geometry.Toric.Analytic.AffinePoint.Product

Complex points of a product semigroup #

A splitting of an additive commutative monoid as a product identifies its complex points with pairs of complex points of the factors. Restriction to each factor gives the forward map; the inverse multiplies the two monomial values. This is a homeomorphism for arbitrary finite monomial generating families, and supplies the affine charts of products of toric fans.

References #

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

A splitting of a semigroup identifies its complex points with pairs of points of the two factors, by restriction of multiplicative characters.

Instances For
    source
    @[simp]
    theorem TauCeti.Toric.AffineSemigroupComplexPoint.prodEquiv_symm_apply_single {S : Type u_1} {T : Type u_2} {U : Type u_3} [AddCommMonoid S] [AddCommMonoid T] [AddCommMonoid U] (e : S ≃+ T × U) (p : AffineSemigroupComplexPoint T × AffineSemigroupComplexPoint U) (s : S) :
    ((prodEquiv e).symm p) (MonoidAlgebra.single (Multiplicative.ofAdd s) 1) = p.1 (MonoidAlgebra.single (Multiplicative.ofAdd (e s).1) 1) * p.2 (MonoidAlgebra.single (Multiplicative.ofAdd (e s).2) 1)

    The inverse product identification multiplies the values on the factor monomials.

    source
    @[simp]
    theorem TauCeti.Toric.AffineSemigroupComplexPoint.prodEquiv_fst_apply_single {S : Type u_1} {T : Type u_2} {U : Type u_3} [AddCommMonoid S] [AddCommMonoid T] [AddCommMonoid U] (e : S ≃+ T × U) (x : AffineSemigroupComplexPoint S) (t : T) :
    ((prodEquiv e) x).1 (MonoidAlgebra.single (Multiplicative.ofAdd t) 1) = x (MonoidAlgebra.single (Multiplicative.ofAdd (e.symm (t, 0))) 1)

    Restriction to the first factor reads its monomial values.

    source
    @[simp]
    theorem TauCeti.Toric.AffineSemigroupComplexPoint.prodEquiv_snd_apply_single {S : Type u_1} {T : Type u_2} {U : Type u_3} [AddCommMonoid S] [AddCommMonoid T] [AddCommMonoid U] (e : S ≃+ T × U) (x : AffineSemigroupComplexPoint S) (u : U) :
    ((prodEquiv e) x).2 (MonoidAlgebra.single (Multiplicative.ofAdd u) 1) = x (MonoidAlgebra.single (Multiplicative.ofAdd (e.symm (0, u))) 1)

    Restriction to the second factor reads its monomial values.

    source
    noncomputable def TauCeti.Toric.AffineSemigroupComplexPoint.prodHomeomorph {S : Type u_1} {T : Type u_2} {U : Type u_3} [AddCommMonoid S] [AddCommMonoid T] [AddCommMonoid U] (e : S ≃+ T × U) {r rT rU : ℕ} (g : AddGeneratingFamily S r) (gT : AddGeneratingFamily T rT) (gU : AddGeneratingFamily U rU) :
    AffineSemigroupComplexPoint S ≃ₜ AffineSemigroupComplexPoint T × AffineSemigroupComplexPoint U

    The product identification is a homeomorphism for any finite monomial generating families on the three semigroups.

    Instances For
      source
      @[simp]
      theorem TauCeti.Toric.AffineSemigroupComplexPoint.coe_prodHomeomorph {S : Type u_1} {T : Type u_2} {U : Type u_3} [AddCommMonoid S] [AddCommMonoid T] [AddCommMonoid U] (e : S ≃+ T × U) {r rT rU : ℕ} (g : AddGeneratingFamily S r) (gT : AddGeneratingFamily T rT) (gU : AddGeneratingFamily U rU) :
      ⇑(prodHomeomorph e g gT gU) = ⇑(prodEquiv e)
      source
      @[simp]
      theorem TauCeti.Toric.AffineSemigroupComplexPoint.coe_prodHomeomorph_symm {S : Type u_1} {T : Type u_2} {U : Type u_3} [AddCommMonoid S] [AddCommMonoid T] [AddCommMonoid U] (e : S ≃+ T × U) {r rT rU : ℕ} (g : AddGeneratingFamily S r) (gT : AddGeneratingFamily T rT) (gU : AddGeneratingFamily U rU) :
      ⇑(prodHomeomorph e g gT gU).symm = ⇑(prodEquiv e).symm