The affine analytic chart of a regular cone

An integral basis of the lattice whose vectors at the ray indices are the primitive ray generators of a cone σ splits the dual semigroup of σ as (ToricRay σ →₀ ℕ) × (ι →₀ ℤ), so the complex points of the affine toric scheme of σ become the mixed chart ℂ ^ k × (ℂ ^ *) ^ l, with k the number of rays of σ and l the number of complementary basis vectors. This file names that chart, computes its coordinate functions, and compares the charts of two extending bases.

The coordinates are values of the point on monomials: the coordinate indexed by a ray is the value on the monomial of the dual basis character of that ray, and the coordinates indexed by the complementary basis vectors are the invertible values on their dual basis characters. They are therefore characters, not choices, once the basis is fixed, and the chart is a homeomorphism for the monomial-embedding topology of an arbitrary finite generating family of the dual semigroup, which was defined without reference to any splitting.

Two extending bases cannot differ at the ray indices, since a ray of a toric cone in an integral lattice has a single primitive generator. The comparison of their charts is therefore a mixed monomial map of the restricted shape that TauCeti.Toric.MixedExponent permits: each boundary coordinate is kept and multiplied by a monomial in the torus coordinates, and the torus coordinates are transformed among themselves by the complementary block of the transition matrix. No boundary coordinate contributes to a torus coordinate. Read in the ambient coordinates ℂ ^ k × ℂ ^ l attached to a numbering of the rays, the comparison is the map TauCeti.Toric.basisChangeOpenPartialHomeomorph of the transition block, whose torus block is unimodular; that map is holomorphic in both directions, which is the compatibility an atlas assembled from these charts needs.

Main declarations

• TauCeti.Toric.coneChartEquiv: the affine analytic chart of a cone with an extending basis, with TauCeti.Toric.coneChartEquiv_fst_apply and TauCeti.Toric.val_coneChartEquiv_snd_apply identifying its coordinate functions with the dual basis characters and TauCeti.Toric.coneChartEquiv_symm_apply_single and TauCeti.Toric.apply_single_ne_zero_iff_coneChartEquiv_fst_ne_zero describing the value and nonvanishing of a point on an arbitrary monomial.
• TauCeti.Toric.coneChartHomeomorph: the chart is a homeomorphism for the monomial-embedding topology of any finite generating family of the dual semigroup.
• TauCeti.Toric.coneChartEquiv_fst_apply_basisChange and TauCeti.Toric.coneChartEquiv_snd_apply_basisChange: changing the extending basis multiplies each boundary coordinate by a monomial in the torus coordinates and transforms the torus coordinates by the complementary block of the transition matrix.
• TauCeti.Toric.coneChartAmbient: the chart in the ambient mixed coordinates attached to a numbering of the rays, which lands in TauCeti.Toric.mixedChartDomain.
• TauCeti.Toric.coneChartAmbientHomeomorph: the ambient chart as a homeomorphism onto TauCeti.Toric.mixedChartDomain.
• TauCeti.Toric.mixedMonomialMap_ofTorusBlock_coneChartAmbient and TauCeti.Toric.basisChangeOpenPartialHomeomorph_coneChartAmbient: in those coordinates the change of extending basis is the mixed monomial biholomorphism of the transition block.

References

• W. Fulton, Introduction to Toric Varieties, §§1.2 and 2.1.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §§1.2 and 3.1.

The chart of an extending basis

noncomputable def TauCeti.Toric.coneChartEquiv {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ) ≃ (ToricRay σ → ℂ) × (ι → ℂˣ)

The affine analytic chart of a cone with an extending basis: the complex points of its affine toric scheme in the mixed coordinates supplied by the basis. The coordinates indexed by the rays of the cone may vanish, while the coordinates indexed by the complementary basis vectors are invertible.

@[simp]

theorem TauCeti.Toric.coneChartEquiv_symm_apply_single {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (z : (ToricRay σ → ℂ) × (ι → ℂˣ)) (m : ↥(dualSemigroup hi σ)) : ((coneChartEquiv hi hσ hb).symm z) (MonoidAlgebra.single (Multiplicative.ofAdd m) 1) = (((regularDualSemigroupEquiv hi hσ hb) m).1.prod fun (ρ : ToricRay σ) (n : ℕ) => z.1 ρ ^ n) * ↑(((regularDualSemigroupEquiv hi hσ hb) m).2.prod fun (j : ι) (n : ℤ) => z.2 j ^ n)

The value on the monomial of a character of the dual semigroup of the complex point with prescribed mixed coordinates: it is the mixed monomial whose exponents are the regular coordinates of the character, natural at the ray indices and integral at the complementary ones.

theorem TauCeti.Toric.apply_single_ne_zero_iff_coneChartEquiv_fst_ne_zero {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) (m : ↥(dualSemigroup hi σ)) : x (MonoidAlgebra.single (Multiplicative.ofAdd m) 1) ≠ 0 ↔ ∀ ρ ∈ ((regularDualSemigroupEquiv hi hσ hb) m).1.support, ((coneChartEquiv hi hσ hb) x).1 ρ ≠ 0

A monomial is nonzero at a complex point exactly when every ray coordinate occurring in its support is nonzero. The complementary-coordinate factor is always a unit.

@[simp]

theorem TauCeti.Toric.coneChartEquiv_fst_apply {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) (ρ : ToricRay σ) : ((coneChartEquiv hi hσ hb) x).1 ρ = x (MonoidAlgebra.single (Multiplicative.ofAdd (dualSemigroupCoord hi hσ hb (Sum.inl ρ))) 1)

The coordinate of a complex point indexed by a ray is its value on the monomial of the dual basis character of that ray.

@[simp]

theorem TauCeti.Toric.val_coneChartEquiv_snd_apply {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) (j : ι) : ↑(((coneChartEquiv hi hσ hb) x).2 j) = x (MonoidAlgebra.single (Multiplicative.ofAdd (dualSemigroupCoord hi hσ hb (Sum.inr j))) 1)

The coordinate of a complex point indexed by a complementary basis vector is, as a complex number, its value on the monomial of the dual basis character of that vector.

noncomputable def TauCeti.Toric.coneChartHomeomorph {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ) ≃ₜ (ToricRay σ → ℂ) × (ι → ℂˣ)

The affine analytic chart is a homeomorphism for the monomial-embedding topology of any finite generating family of the dual semigroup: the complex points of the affine toric scheme of a cone with an extending basis are the mixed chart ℂ ^ k × (ℂ ^ *) ^ l, whatever generating family topologizes them.

@[simp]

theorem TauCeti.Toric.coe_coneChartHomeomorph {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : ⇑(coneChartHomeomorph hi hσ hb g) = ⇑(coneChartEquiv hi hσ hb)

@[simp]

theorem TauCeti.Toric.coe_coneChartHomeomorph_symm {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : ⇑(coneChartHomeomorph hi hσ hb g).symm = ⇑(coneChartEquiv hi hσ hb).symm

Changing the extending basis

theorem TauCeti.Toric.coneChartEquiv_fst_apply_basisChange {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) [Fintype ι] {b' : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb' : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b' (Sum.inl ρ))) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) (ρ : ToricRay σ) : ((coneChartEquiv hi hσ hb') x).1 ρ = ((coneChartEquiv hi hσ hb) x).1 ρ * ∏ j : ι, ↑(((coneChartEquiv hi hσ hb) x).2 j) ^ b'.toMatrix (⇑b) (Sum.inl ρ) (Sum.inr j)

Changing the extending basis multiplies the coordinate indexed by a ray by a monomial in the torus coordinates, whose exponents are the complementary entries of the ray row of the transition matrix. The coordinate itself occurs to the first power: both bases carry the primitive generator of a ray at the index of that ray, so the ray block of the transition matrix is the identity.

theorem TauCeti.Toric.coneChartEquiv_snd_apply_basisChange {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) [Fintype ι] {b' : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb' : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b' (Sum.inl ρ))) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) (j : ι) : ((coneChartEquiv hi hσ hb') x).2 j = ∏ j' : ι, ((coneChartEquiv hi hσ hb) x).2 j' ^ b'.toMatrix (⇑b) (Sum.inr j) (Sum.inr j')

Changing the extending basis transforms the invertible coordinates among themselves, by the complementary block of the transition matrix. No coordinate indexed by a ray contributes: the complementary rows of the ray columns of the transition matrix vanish, because both bases carry the primitive generator of a ray at the index of that ray.

theorem TauCeti.Toric.val_coneChartEquiv_snd_apply_basisChange {N : Type u_1} {V : Type u_2} {ι : Type u_3} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {b : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b (Sum.inl ρ))) [Fintype ι] {b' : Module.Basis (ToricRay σ ⊕ ι) ℤ N} (hb' : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (b' (Sum.inl ρ))) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) (j : ι) : ↑(((coneChartEquiv hi hσ hb') x).2 j) = ∏ j' : ι, ↑(((coneChartEquiv hi hσ hb) x).2 j') ^ b'.toMatrix (⇑b) (Sum.inr j) (Sum.inr j')

The complex value of a transformed invertible coordinate, as a monomial in the complex values of the invertible coordinates of the other chart.

The chart in ambient mixed coordinates

noncomputable def TauCeti.Toric.coneChartAmbient {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {k l : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) : (Fin k → ℂ) × (Fin l → ℂ)

The affine analytic chart of a cone with an extending basis, in the ambient mixed coordinates ℂ ^ k × ℂ ^ l attached to a numbering κ of its rays: the coordinates indexed by the rays are reindexed along κ, and the invertible coordinates are viewed as complex numbers. This is the shape on which mixed monomial maps act.

@[simp]

theorem TauCeti.Toric.coneChartAmbient_fst_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {k l : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) (a : Fin k) : (coneChartAmbient hi hσ hB κ x).1 a = ((coneChartEquiv hi hσ hB) x).1 (κ.symm a)

@[simp]

theorem TauCeti.Toric.coneChartAmbient_snd_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {k l : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) (c : Fin l) : (coneChartAmbient hi hσ hB κ x).2 c = ↑(((coneChartEquiv hi hσ hB) x).2 c)

theorem TauCeti.Toric.coneChartAmbient_mem_mixedChartDomain {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {k l : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) : coneChartAmbient hi hσ hB κ x ∈ mixedChartDomain k l

The ambient coordinates of a complex point lie in the mixed-chart locus: the coordinates indexed by the complementary basis vectors are invertible.

noncomputable def TauCeti.Toric.coneChartAmbientHomeomorph {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {k l : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ) ≃ₜ { z : (Fin k → ℂ) × (Fin l → ℂ) // z ∈ mixedChartDomain k l }

The ambient coordinates give a homeomorphism from the complex points of the affine toric scheme onto the mixed-chart locus. It is obtained from coneChartHomeomorph by reindexing the ray coordinates and applying unitsHomeomorphNeZero coordinatewise to the torus coordinates.

@[simp]

theorem TauCeti.Toric.coneChartAmbientHomeomorph_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {k l : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) : ↑((coneChartAmbientHomeomorph hi hσ hB κ g) x) = coneChartAmbient hi hσ hB κ x

@[simp]

theorem TauCeti.Toric.range_coneChartAmbient {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {k l : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) : Set.range (coneChartAmbient hi hσ hB κ) = mixedChartDomain k l

The range of the ambient cone chart is exactly the mixed-chart locus.

@[simp]

theorem TauCeti.Toric.coneChartAmbientHomeomorph_symm_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} {s : ℕ} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {k l : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) s) (z : { z : (Fin k → ℂ) × (Fin l → ℂ) // z ∈ mixedChartDomain k l }) : (coneChartAmbientHomeomorph hi hσ hB κ g).symm z = (coneChartEquiv hi hσ hB).symm (fun (ρ : ToricRay σ) => (↑z).1 (κ ρ), fun (c : Fin l) => Units.mk0 ((↑z).2 c) ⋯)

theorem TauCeti.Toric.mixedMonomialMap_ofTorusBlock_coneChartAmbient {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {k l : ℕ} {B B' : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (hB' : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B' (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) : mixedMonomialMap (MixedExponent.ofTorusBlock (Matrix.of fun (a : Fin k) (c : Fin l) => B'.toMatrix (⇑B) (Sum.inl (κ.symm a)) (Sum.inr c)) ((B'.toMatrix ⇑B).submatrix Sum.inr Sum.inr)) (coneChartAmbient hi hσ hB κ x) = coneChartAmbient hi hσ hB' κ x

Changing the basis extending the primitive ray generators acts on the ambient mixed coordinates of the affine chart by the mixed monomial map of the transition block: each boundary coordinate is kept and twisted by the complementary entries of its ray row, and the torus coordinates are transformed by the complementary block of the transition matrix.

theorem TauCeti.Toric.basisChangeOpenPartialHomeomorph_coneChartAmbient {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsToricCone i σ) {k l : ℕ} {B B' : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (hB' : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B' (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) : ↑(basisChangeOpenPartialHomeomorph (Matrix.of fun (a : Fin k) (c : Fin l) => B'.toMatrix (⇑B) (Sum.inl (κ.symm a)) (Sum.inr c)) ((B'.toMatrix ⇑B).submatrix Sum.inr Sum.inr) ⋯) (coneChartAmbient hi hσ hB κ x) = coneChartAmbient hi hσ hB' κ x

The transition between the ambient mixed coordinates attached to two extending bases is the mixed monomial map of the transition block, whose torus block is unimodular: the boundary coordinates are kept and twisted. It is therefore a biholomorphism of the mixed-chart locus, by TauCeti.Toric.contDiffOn_basisChangeOpenPartialHomeomorph and TauCeti.Toric.contDiffOn_basisChangeOpenPartialHomeomorph_symm.