Mixed monomial maps between mixed charts

A mixed chart is a product ℂ ^ k × (ℂ ^ *) ^ l, the model on which the affine analytic chart of a regular k-dimensional cone in a rank-(k + l) lattice is built. The transition maps between two such charts, and the maps induced by a morphism of fans, are mixed monomial maps: each target coordinate is a product of integral powers of the source coordinates.

The exponents cannot be arbitrary. A source coordinate that is allowed to vanish may only be raised to a natural power, and it may only contribute to a target coordinate that is itself allowed to vanish: a monomial containing a boundary coordinate takes the value 0, so it can never be one of the invertible coordinates of the target. MixedExponent records exactly the three admissible blocks and, by omitting a fourth field, makes the forbidden contribution untypeable.

The ambient formula mixedMonomialMap is defined on all of ℂ ^ k × ℂ ^ l, using the junk value (0 : ℂ) ^ (n : ℤ) = 0 for n < 0. Every theorem about composing two of these maps is stated on mixedChartDomain, the open locus where the torus coordinates are invertible: exponent arithmetic needs y ^ (m + n) = y ^ m * y ^ n, which fails at y = 0, and the composite of two mixed monomial maps really is a different function off that locus.

Main declarations

• TauCeti.Toric.MixedExponent: the exponent data of a mixed monomial map.
• TauCeti.Toric.mixedChartDomain: the open locus where all torus coordinates are invertible.
• TauCeti.Toric.mixedMonomialMap: the ambient coordinate formula.
• TauCeti.Toric.mapsTo_mixedMonomialMap: a mixed monomial map preserves the mixed-chart locus.
• TauCeti.Toric.contDiffAt_mixedMonomialMap and TauCeti.Toric.differentiableOn_mixedMonomialMap: a mixed monomial map is holomorphic on the mixed-chart locus.
• TauCeti.Toric.MixedExponent.comp and TauCeti.Toric.mixedMonomialMap_comp: composition of exponent data is a product of block matrices, and it computes the composite map on the mixed-chart locus. TauCeti.Toric.MixedExponent.id_comp, TauCeti.Toric.MixedExponent.comp_id and TauCeti.Toric.MixedExponent.comp_assoc are the associated category laws.
• TauCeti.Toric.MixedExponent.prod, TauCeti.Toric.mixedChartProdHomeomorph, and TauCeti.Toric.mixedMonomialMap_prod: products of exponent data act componentwise on products of mixed charts.
• TauCeti.Toric.hasDerivAt_mixedMonomialMap_fst_boundary, TauCeti.Toric.hasDerivAt_mixedMonomialMap_fst_torus, TauCeti.Toric.hasDerivAt_mixedMonomialMap_snd_boundary, and TauCeti.Toric.hasDerivAt_mixedMonomialMap_snd_torus: the four blocks of the Jacobian in mixed coordinates.
• TauCeti.Toric.mixedMonomialOpenPartialHomeomorph: a two-sided inverse pair of exponent data gives a biholomorphism between the two mixed-chart loci, holomorphic in both directions by TauCeti.Toric.contDiffOn_mixedMonomialOpenPartialHomeomorph and TauCeti.Toric.contDiffOn_mixedMonomialOpenPartialHomeomorph_symm.
• TauCeti.Toric.MixedExponent.ofTorusBlock and TauCeti.Toric.basisChangeOpenPartialHomeomorph: the exponent data that keeps the boundary coordinates and acts on the torus coordinates by an integral matrix, and the biholomorphism it induces when that matrix is unimodular, holomorphic in both directions by TauCeti.Toric.contDiffOn_basisChangeOpenPartialHomeomorph and TauCeti.Toric.contDiffOn_basisChangeOpenPartialHomeomorph_symm. This is the shape of a change of the basis extending the primitive ray generators of a regular cone.

References

The mathematics is §§1.1--1.3 and §3.1 of D. Cox, J. Little and H. Schenck, Toric Varieties, and §§1.2--1.3 of W. Fulton, Introduction to Toric Varieties.

structure TauCeti.Toric.MixedExponent (k l k' l' : ℕ) : Type

Exponent data for a mixed monomial map ℂ ^ k × (ℂ ^ *) ^ l → ℂ ^ k' × (ℂ ^ *) ^ l'.

The three blocks are the only admissible ones. A boundary coordinate of the source, which may vanish, carries a natural exponent and may only enter a boundary coordinate of the target; a torus coordinate of the source, which is invertible, carries an integral exponent and may enter either kind of target coordinate. There is deliberately no block from the boundary coordinates of the source to the torus coordinates of the target: such a monomial would vanish somewhere.

• boundaryBoundary : Matrix (Fin k') (Fin k) ℕ

  Exponents of the source boundary coordinates in the target boundary coordinates.

• boundaryTorus : Matrix (Fin k') (Fin l) ℤ

  Exponents of the source torus coordinates in the target boundary coordinates.

• torusTorus : Matrix (Fin l') (Fin l) ℤ

  Exponents of the source torus coordinates in the target torus coordinates.

theorem TauCeti.Toric.MixedExponent.ext_iff {k l k' l' : ℕ} {x y : MixedExponent k l k' l'} : x = y ↔ x.boundaryBoundary = y.boundaryBoundary ∧ x.boundaryTorus = y.boundaryTorus ∧ x.torusTorus = y.torusTorus

theorem TauCeti.Toric.MixedExponent.ext {k l k' l' : ℕ} {x y : MixedExponent k l k' l'} (boundaryBoundary : x.boundaryBoundary = y.boundaryBoundary) (boundaryTorus : x.boundaryTorus = y.boundaryTorus) (torusTorus : x.torusTorus = y.torusTorus) : x = y

def TauCeti.Toric.mixedChartDomain (k l : ℕ) : Set ((Fin k → ℂ) × (Fin l → ℂ))

The open locus of a mixed chart: the points whose torus coordinates are all invertible.

@[simp]

theorem TauCeti.Toric.mem_mixedChartDomain {k l : ℕ} {z : (Fin k → ℂ) × (Fin l → ℂ)} : z ∈ mixedChartDomain k l ↔ ∀ (j : Fin l), z.2 j ≠ 0

theorem TauCeti.Toric.isOpen_mixedChartDomain {k l : ℕ} : IsOpen (mixedChartDomain k l)

The mixed-chart domain is open in its ambient affine space.

noncomputable def TauCeti.Toric.mixedMonomialMap {k l k' l' : ℕ} (A : MixedExponent k l k' l') : (Fin k → ℂ) × (Fin l → ℂ) → (Fin k' → ℂ) × (Fin l' → ℂ)

The ambient coordinate formula of the mixed monomial map with exponent data A. Its composition laws hold on mixedChartDomain, not at ambient points with a vanishing torus coordinate.

@[simp]

theorem TauCeti.Toric.mixedMonomialMap_fst_apply {k l k' l' : ℕ} (A : MixedExponent k l k' l') (z : (Fin k → ℂ) × (Fin l → ℂ)) (a : Fin k') : (mixedMonomialMap A z).1 a = (∏ b : Fin k, z.1 b ^ A.boundaryBoundary a b) * ∏ b : Fin l, z.2 b ^ A.boundaryTorus a b

@[simp]

theorem TauCeti.Toric.mixedMonomialMap_snd_apply {k l k' l' : ℕ} (A : MixedExponent k l k' l') (z : (Fin k → ℂ) × (Fin l → ℂ)) (a : Fin l') : (mixedMonomialMap A z).2 a = ∏ b : Fin l, z.2 b ^ A.torusTorus a b

theorem TauCeti.Toric.mixedMonomialMap_snd_ne_zero {k l k' l' : ℕ} (A : MixedExponent k l k' l') {z : (Fin k → ℂ) × (Fin l → ℂ)} (hz : z ∈ mixedChartDomain k l) (a : Fin l') : (mixedMonomialMap A z).2 a ≠ 0

A torus coordinate of the image of a point of the mixed-chart locus is invertible.

theorem TauCeti.Toric.mapsTo_mixedMonomialMap {k l k' l' : ℕ} (A : MixedExponent k l k' l') : Set.MapsTo (mixedMonomialMap A) (mixedChartDomain k l) (mixedChartDomain k' l')

A mixed monomial map sends the mixed-chart locus of its source into the mixed-chart locus of its target.

theorem TauCeti.Toric.mixedMonomialMap_fst_eq_zero_iff {k l k' l' : ℕ} (A : MixedExponent k l k' l') {z : (Fin k → ℂ) × (Fin l → ℂ)} (hz : z ∈ mixedChartDomain k l) (a : Fin k') : (mixedMonomialMap A z).1 a = 0 ↔ ∃ (b : Fin k), z.1 b = 0 ∧ A.boundaryBoundary a b ≠ 0

On the mixed-chart locus a boundary coordinate of the image vanishes exactly when one of the source boundary coordinates occurring in it vanishes.

Composition of exponent data

def TauCeti.Toric.MixedExponent.id (k l : ℕ) : MixedExponent k l k l

The exponent data of the identity of a mixed chart.

@[simp]

theorem TauCeti.Toric.MixedExponent.id_boundaryBoundary {k l : ℕ} : (MixedExponent.id k l).boundaryBoundary = 1

@[simp]

theorem TauCeti.Toric.MixedExponent.id_boundaryTorus {k l : ℕ} : (MixedExponent.id k l).boundaryTorus = 0

@[simp]

theorem TauCeti.Toric.MixedExponent.id_torusTorus {k l : ℕ} : (MixedExponent.id k l).torusTorus = 1

def TauCeti.Toric.MixedExponent.comp {k l k' l' k'' l'' : ℕ} (B : MixedExponent k' l' k'' l'') (A : MixedExponent k l k' l') : MixedExponent k l k'' l''

Composition of exponent data. The exponents of the source torus coordinates in the target boundary coordinates receive a contribution from each of the two blocks of B that land in a boundary coordinate.

@[simp]

theorem TauCeti.Toric.MixedExponent.comp_boundaryBoundary {k l k' l' k'' l'' : ℕ} (B : MixedExponent k' l' k'' l'') (A : MixedExponent k l k' l') : (B.comp A).boundaryBoundary = B.boundaryBoundary * A.boundaryBoundary

@[simp]

theorem TauCeti.Toric.MixedExponent.comp_boundaryTorus {k l k' l' k'' l'' : ℕ} (B : MixedExponent k' l' k'' l'') (A : MixedExponent k l k' l') : (B.comp A).boundaryTorus = B.boundaryBoundary.map Nat.cast * A.boundaryTorus + B.boundaryTorus * A.torusTorus

@[simp]

theorem TauCeti.Toric.MixedExponent.comp_torusTorus {k l k' l' k'' l'' : ℕ} (B : MixedExponent k' l' k'' l'') (A : MixedExponent k l k' l') : (B.comp A).torusTorus = B.torusTorus * A.torusTorus

@[simp]

theorem TauCeti.Toric.MixedExponent.id_comp {k l k' l' : ℕ} (A : MixedExponent k l k' l') : (MixedExponent.id k' l').comp A = A

The identity exponent data is a left unit for composition.

@[simp]

theorem TauCeti.Toric.MixedExponent.comp_id {k l k' l' : ℕ} (A : MixedExponent k l k' l') : A.comp (MixedExponent.id k l) = A

The identity exponent data is a right unit for composition.

@[simp]

theorem TauCeti.Toric.MixedExponent.comp_assoc {k l k' l' k'' l'' k''' l''' : ℕ} (C : MixedExponent k'' l'' k''' l''') (B : MixedExponent k' l' k'' l'') (A : MixedExponent k l k' l') : (C.comp B).comp A = C.comp (B.comp A)

Composition of exponent data is associative.

def TauCeti.Toric.MixedExponent.prod {k₁ l₁ k₁' l₁' k₂ l₂ k₂' l₂' : ℕ} (A : MixedExponent k₁ l₁ k₁' l₁') (B : MixedExponent k₂ l₂ k₂' l₂') : MixedExponent (k₁ + k₂) (l₁ + l₂) (k₁' + k₂') (l₁' + l₂')

The product of mixed exponent data is the block diagonal exponent data.

@[simp]

theorem TauCeti.Toric.MixedExponent.prod_boundaryBoundary {k₁ l₁ k₁' l₁' k₂ l₂ k₂' l₂' : ℕ} (A : MixedExponent k₁ l₁ k₁' l₁') (B : MixedExponent k₂ l₂ k₂' l₂') : (A.prod B).boundaryBoundary = (Matrix.fromBlocks A.boundaryBoundary 0 0 B.boundaryBoundary).submatrix ⇑finSumFinEquiv.symm ⇑finSumFinEquiv.symm

@[simp]

theorem TauCeti.Toric.MixedExponent.prod_boundaryTorus {k₁ l₁ k₁' l₁' k₂ l₂ k₂' l₂' : ℕ} (A : MixedExponent k₁ l₁ k₁' l₁') (B : MixedExponent k₂ l₂ k₂' l₂') : (A.prod B).boundaryTorus = (Matrix.fromBlocks A.boundaryTorus 0 0 B.boundaryTorus).submatrix ⇑finSumFinEquiv.symm ⇑finSumFinEquiv.symm

@[simp]

theorem TauCeti.Toric.MixedExponent.prod_torusTorus {k₁ l₁ k₁' l₁' k₂ l₂ k₂' l₂' : ℕ} (A : MixedExponent k₁ l₁ k₁' l₁') (B : MixedExponent k₂ l₂ k₂' l₂') : (A.prod B).torusTorus = (Matrix.fromBlocks A.torusTorus 0 0 B.torusTorus).submatrix ⇑finSumFinEquiv.symm ⇑finSumFinEquiv.symm

Composition of mixed monomial maps

@[simp]

theorem TauCeti.Toric.mixedMonomialMap_id {k l : ℕ} : mixedMonomialMap (MixedExponent.id k l) = id

The identity exponent data induces the identity map, at every ambient point.

@[simp]

theorem TauCeti.Toric.mixedMonomialMap_comp {k l k' l' k'' l'' : ℕ} (B : MixedExponent k' l' k'' l'') (A : MixedExponent k l k' l') {z : (Fin k → ℂ) × (Fin l → ℂ)} (hz : z ∈ mixedChartDomain k l) : mixedMonomialMap (B.comp A) z = mixedMonomialMap B (mixedMonomialMap A z)

Composing two mixed monomial maps multiplies their exponent data, on the locus where the torus coordinates are invertible. No such formula is claimed at ambient points with a vanishing torus coordinate.

Products

noncomputable def TauCeti.Toric.mixedChartProdHomeomorph {k₁ l₁ k₂ l₂ : ℕ} : (Fin (k₁ + k₂) → ℂ) × (Fin (l₁ + l₂) → ℂ) ≃ₜ ((Fin k₁ → ℂ) × (Fin l₁ → ℂ)) × (Fin k₂ → ℂ) × (Fin l₂ → ℂ)

Splitting the boundary and torus coordinates identifies the mixed chart of the sum of two dimensions with the product of the two mixed charts.

@[simp]

theorem TauCeti.Toric.mixedChartProdHomeomorph_apply {k₁ l₁ k₂ l₂ : ℕ} (z : (Fin (k₁ + k₂) → ℂ) × (Fin (l₁ + l₂) → ℂ)) : mixedChartProdHomeomorph z = ((fun (i : Fin k₁) => z.1 (Fin.castAdd k₂ i), fun (i : Fin l₁) => z.2 (Fin.castAdd l₂ i)), fun (i : Fin k₂) => z.1 (Fin.natAdd k₁ i), fun (i : Fin l₂) => z.2 (Fin.natAdd l₁ i))

@[simp]

theorem TauCeti.Toric.mixedChartProdHomeomorph_symm_apply {k₁ l₁ k₂ l₂ : ℕ} (z : ((Fin k₁ → ℂ) × (Fin l₁ → ℂ)) × (Fin k₂ → ℂ) × (Fin l₂ → ℂ)) : mixedChartProdHomeomorph.symm z = (fun (i : Fin (k₁ + k₂)) => Fin.addCases z.1.1 z.2.1 i, fun (i : Fin (l₁ + l₂)) => Fin.addCases z.1.2 z.2.2 i)

@[simp]

theorem TauCeti.Toric.mixedChartProdHomeomorph_preimage_prod {k₁ l₁ k₂ l₂ : ℕ} : ⇑mixedChartProdHomeomorph ⁻¹' mixedChartDomain k₁ l₁ ×ˢ mixedChartDomain k₂ l₂ = mixedChartDomain (k₁ + k₂) (l₁ + l₂)

The canonical coordinate splitting identifies the mixed-chart domain of the summed dimensions with the product of the two mixed-chart domains.

theorem TauCeti.Toric.mixedMonomialMap_prod {k₁ l₁ k₁' l₁' k₂ l₂ k₂' l₂' : ℕ} (A : MixedExponent k₁ l₁ k₁' l₁') (B : MixedExponent k₂ l₂ k₂' l₂') (z : (Fin (k₁ + k₂) → ℂ) × (Fin (l₁ + l₂) → ℂ)) : mixedChartProdHomeomorph (mixedMonomialMap (A.prod B) z) = (mixedMonomialMap A (mixedChartProdHomeomorph z).1, mixedMonomialMap B (mixedChartProdHomeomorph z).2)

The mixed monomial map of block diagonal product exponent data is the product of the two mixed monomial maps, under the canonical splitting of mixed-chart coordinates.

Holomorphy

theorem TauCeti.Toric.contDiffAt_mixedMonomialMap {k l k' l' : ℕ} {n : WithTop ℕ∞} (A : MixedExponent k l k' l') {z : (Fin k → ℂ) × (Fin l → ℂ)} (hz : z ∈ mixedChartDomain k l) : ContDiffAt ℂ n (mixedMonomialMap A) z

A mixed monomial map is holomorphic at every point of the mixed-chart locus, to any order.

theorem TauCeti.Toric.contDiffOn_mixedMonomialMap {k l k' l' : ℕ} {n : WithTop ℕ∞} (A : MixedExponent k l k' l') : ContDiffOn ℂ n (mixedMonomialMap A) (mixedChartDomain k l)

A mixed monomial map is holomorphic on the mixed-chart locus, to any order.

theorem TauCeti.Toric.differentiableOn_mixedMonomialMap {k l k' l' : ℕ} (A : MixedExponent k l k' l') : DifferentiableOn ℂ (mixedMonomialMap A) (mixedChartDomain k l)

A mixed monomial map is complex differentiable on the mixed-chart locus.

Jacobian entries

theorem TauCeti.Toric.hasDerivAt_mixedMonomialMap_fst_boundary {k l k' l' : ℕ} (A : MixedExponent k l k' l') (z : (Fin k → ℂ) × (Fin l → ℂ)) (a : Fin k') (b : Fin k) : HasDerivAt (fun (t : ℂ) => (mixedMonomialMap A (Function.update z.1 b t, z.2)).1 a) (↑(A.boundaryBoundary a b) * z.1 b ^ (A.boundaryBoundary a b - 1) * ((∏ c ∈ Finset.univ \ {b}, z.1 c ^ A.boundaryBoundary a c) * ∏ c : Fin l, z.2 c ^ A.boundaryTorus a c)) (z.1 b)

The boundary-to-boundary block of the Jacobian of a mixed monomial map. The formula remains valid when the boundary coordinate vanishes.

theorem TauCeti.Toric.hasDerivAt_mixedMonomialMap_fst_torus {k l k' l' : ℕ} (A : MixedExponent k l k' l') {z : (Fin k → ℂ) × (Fin l → ℂ)} (hz : z ∈ mixedChartDomain k l) (a : Fin k') (b : Fin l) : HasDerivAt (fun (t : ℂ) => (mixedMonomialMap A (z.1, Function.update z.2 b t)).1 a) (↑(A.boundaryTorus a b) * z.2 b ^ (A.boundaryTorus a b - 1) * ((∏ c : Fin k, z.1 c ^ A.boundaryBoundary a c) * ∏ c ∈ Finset.univ \ {b}, z.2 c ^ A.boundaryTorus a c)) (z.2 b)

The torus-to-boundary block of the Jacobian of a mixed monomial map, on the mixed-chart domain.

theorem TauCeti.Toric.hasDerivAt_mixedMonomialMap_snd_boundary {k l k' l' : ℕ} (A : MixedExponent k l k' l') (z : (Fin k → ℂ) × (Fin l → ℂ)) (a : Fin l') (b : Fin k) : HasDerivAt (fun (t : ℂ) => (mixedMonomialMap A (Function.update z.1 b t, z.2)).2 a) 0 (z.1 b)

The boundary-to-torus block of the Jacobian of a mixed monomial map is zero.

theorem TauCeti.Toric.hasDerivAt_mixedMonomialMap_snd_torus {k l k' l' : ℕ} (A : MixedExponent k l k' l') {z : (Fin k → ℂ) × (Fin l → ℂ)} (hz : z ∈ mixedChartDomain k l) (a : Fin l') (b : Fin l) : HasDerivAt (fun (t : ℂ) => (mixedMonomialMap A (z.1, Function.update z.2 b t)).2 a) (↑(A.torusTorus a b) * z.2 b ^ (A.torusTorus a b - 1) * ∏ c ∈ Finset.univ \ {b}, z.2 c ^ A.torusTorus a c) (z.2 b)

The torus-to-torus block of the Jacobian of a mixed monomial map, on the mixed-chart domain.

Biholomorphisms between mixed charts

noncomputable def TauCeti.Toric.mixedMonomialOpenPartialHomeomorph {k l k' l' : ℕ} (A : MixedExponent k l k' l') (B : MixedExponent k' l' k l) (hBA : B.comp A = MixedExponent.id k l) (hAB : A.comp B = MixedExponent.id k' l') : OpenPartialHomeomorph ((Fin k → ℂ) × (Fin l → ℂ)) ((Fin k' → ℂ) × (Fin l' → ℂ))

A two-sided inverse pair of exponent data induces a homeomorphism between the two mixed-chart loci. It is a biholomorphism by contDiffOn_mixedMonomialOpenPartialHomeomorph and contDiffOn_mixedMonomialOpenPartialHomeomorph_symm.

@[simp]

theorem TauCeti.Toric.mixedMonomialOpenPartialHomeomorph_coe {k l k' l' : ℕ} (A : MixedExponent k l k' l') (B : MixedExponent k' l' k l) (hBA : B.comp A = MixedExponent.id k l) (hAB : A.comp B = MixedExponent.id k' l') : ↑(mixedMonomialOpenPartialHomeomorph A B hBA hAB) = mixedMonomialMap A

@[simp]

theorem TauCeti.Toric.mixedMonomialOpenPartialHomeomorph_symm_coe {k l k' l' : ℕ} (A : MixedExponent k l k' l') (B : MixedExponent k' l' k l) (hBA : B.comp A = MixedExponent.id k l) (hAB : A.comp B = MixedExponent.id k' l') : ↑(mixedMonomialOpenPartialHomeomorph A B hBA hAB).symm = mixedMonomialMap B

@[simp]

theorem TauCeti.Toric.mixedMonomialOpenPartialHomeomorph_source {k l k' l' : ℕ} (A : MixedExponent k l k' l') (B : MixedExponent k' l' k l) (hBA : B.comp A = MixedExponent.id k l) (hAB : A.comp B = MixedExponent.id k' l') : (mixedMonomialOpenPartialHomeomorph A B hBA hAB).source = mixedChartDomain k l

@[simp]

theorem TauCeti.Toric.mixedMonomialOpenPartialHomeomorph_target {k l k' l' : ℕ} (A : MixedExponent k l k' l') (B : MixedExponent k' l' k l) (hBA : B.comp A = MixedExponent.id k l) (hAB : A.comp B = MixedExponent.id k' l') : (mixedMonomialOpenPartialHomeomorph A B hBA hAB).target = mixedChartDomain k' l'

theorem TauCeti.Toric.contDiffOn_mixedMonomialOpenPartialHomeomorph {k l k' l' : ℕ} {n : WithTop ℕ∞} (A : MixedExponent k l k' l') (B : MixedExponent k' l' k l) (hBA : B.comp A = MixedExponent.id k l) (hAB : A.comp B = MixedExponent.id k' l') : ContDiffOn ℂ n (↑(mixedMonomialOpenPartialHomeomorph A B hBA hAB)) (mixedMonomialOpenPartialHomeomorph A B hBA hAB).source

An inverse pair of exponent data induces a biholomorphism: the induced homeomorphism is holomorphic, to any order.

theorem TauCeti.Toric.contDiffOn_mixedMonomialOpenPartialHomeomorph_symm {k l k' l' : ℕ} {n : WithTop ℕ∞} (A : MixedExponent k l k' l') (B : MixedExponent k' l' k l) (hBA : B.comp A = MixedExponent.id k l) (hAB : A.comp B = MixedExponent.id k' l') : ContDiffOn ℂ n (↑(mixedMonomialOpenPartialHomeomorph A B hBA hAB).symm) (mixedMonomialOpenPartialHomeomorph A B hBA hAB).target

An inverse pair of exponent data induces a biholomorphism: the inverse of the induced homeomorphism is holomorphic, to any order.

Changing the basis extending the primitive ray generators

def TauCeti.Toric.MixedExponent.ofTorusBlock {k l : ℕ} (C : Matrix (Fin k) (Fin l) ℤ) (D : Matrix (Fin l) (Fin l) ℤ) : MixedExponent k l k l

The exponent data of a self-map of a mixed chart that keeps the boundary coordinates, twists them by the integral matrix C, and acts on the torus coordinates by the integral matrix D. Two bases of the lattice extending the primitive ray generators of a regular cone differ by exactly such a block, with D unimodular.

@[simp]

theorem TauCeti.Toric.MixedExponent.ofTorusBlock_boundaryBoundary {k l : ℕ} (C : Matrix (Fin k) (Fin l) ℤ) (D : Matrix (Fin l) (Fin l) ℤ) : (ofTorusBlock C D).boundaryBoundary = 1

@[simp]

theorem TauCeti.Toric.MixedExponent.ofTorusBlock_boundaryTorus {k l : ℕ} (C : Matrix (Fin k) (Fin l) ℤ) (D : Matrix (Fin l) (Fin l) ℤ) : (ofTorusBlock C D).boundaryTorus = C

@[simp]

theorem TauCeti.Toric.MixedExponent.ofTorusBlock_torusTorus {k l : ℕ} (C : Matrix (Fin k) (Fin l) ℤ) (D : Matrix (Fin l) (Fin l) ℤ) : (ofTorusBlock C D).torusTorus = D

@[simp]

theorem TauCeti.Toric.MixedExponent.ofTorusBlock_zero_one {k l : ℕ} : ofTorusBlock 0 1 = MixedExponent.id k l

@[simp]

theorem TauCeti.Toric.MixedExponent.ofTorusBlock_comp_ofTorusBlock {k l : ℕ} (C C' : Matrix (Fin k) (Fin l) ℤ) (D D' : Matrix (Fin l) (Fin l) ℤ) : (ofTorusBlock C' D').comp (ofTorusBlock C D) = ofTorusBlock (C + C' * D) (D' * D)

Composing the torus-block data (C, D) followed by (C', D') gives boundary twist C + C' * D and torus block D' * D.

theorem TauCeti.Toric.MixedExponent.ofTorusBlock_comp_eq_id_of_mul_eq_one {k l : ℕ} (C : Matrix (Fin k) (Fin l) ℤ) {D D' : Matrix (Fin l) (Fin l) ℤ} (h : D' * D = 1) : (ofTorusBlock (-(C * D')) D').comp (ofTorusBlock C D) = MixedExponent.id k l

A unimodular torus block gives an inverse pair of exponent data.

noncomputable def TauCeti.Toric.basisChangeOpenPartialHomeomorph {k l : ℕ} (C : Matrix (Fin k) (Fin l) ℤ) (D : Matrix (Fin l) (Fin l) ℤ) (hD : IsUnit D.det) : OpenPartialHomeomorph ((Fin k → ℂ) × (Fin l → ℂ)) ((Fin k → ℂ) × (Fin l → ℂ))

The biholomorphism of a mixed chart induced by a unimodular change of the basis extending the primitive ray generators: the boundary coordinates are kept and twisted by C, and the torus coordinates are transformed by the unimodular matrix D.

@[simp]

theorem TauCeti.Toric.basisChangeOpenPartialHomeomorph_coe {k l : ℕ} (C : Matrix (Fin k) (Fin l) ℤ) (D : Matrix (Fin l) (Fin l) ℤ) (hD : IsUnit D.det) : ↑(basisChangeOpenPartialHomeomorph C D hD) = mixedMonomialMap (MixedExponent.ofTorusBlock C D)

@[simp]

theorem TauCeti.Toric.basisChangeOpenPartialHomeomorph_symm_coe {k l : ℕ} (C : Matrix (Fin k) (Fin l) ℤ) (D : Matrix (Fin l) (Fin l) ℤ) (hD : IsUnit D.det) : ↑(basisChangeOpenPartialHomeomorph C D hD).symm = mixedMonomialMap (MixedExponent.ofTorusBlock (-(C * D⁻¹)) D⁻¹)

@[simp]

theorem TauCeti.Toric.basisChangeOpenPartialHomeomorph_source {k l : ℕ} (C : Matrix (Fin k) (Fin l) ℤ) (D : Matrix (Fin l) (Fin l) ℤ) (hD : IsUnit D.det) : (basisChangeOpenPartialHomeomorph C D hD).source = mixedChartDomain k l

@[simp]

theorem TauCeti.Toric.basisChangeOpenPartialHomeomorph_target {k l : ℕ} (C : Matrix (Fin k) (Fin l) ℤ) (D : Matrix (Fin l) (Fin l) ℤ) (hD : IsUnit D.det) : (basisChangeOpenPartialHomeomorph C D hD).target = mixedChartDomain k l

theorem TauCeti.Toric.contDiffOn_basisChangeOpenPartialHomeomorph {k l : ℕ} {n : WithTop ℕ∞} (C : Matrix (Fin k) (Fin l) ℤ) (D : Matrix (Fin l) (Fin l) ℤ) (hD : IsUnit D.det) : ContDiffOn ℂ n (↑(basisChangeOpenPartialHomeomorph C D hD)) (basisChangeOpenPartialHomeomorph C D hD).source

A unimodular change of the extending basis induces a biholomorphism: the induced homeomorphism is holomorphic, to any order.

theorem TauCeti.Toric.contDiffOn_basisChangeOpenPartialHomeomorph_symm {k l : ℕ} {n : WithTop ℕ∞} (C : Matrix (Fin k) (Fin l) ℤ) (D : Matrix (Fin l) (Fin l) ℤ) (hD : IsUnit D.det) : ContDiffOn ℂ n (↑(basisChangeOpenPartialHomeomorph C D hD).symm) (basisChangeOpenPartialHomeomorph C D hD).target

A unimodular change of the extending basis induces a biholomorphism: the inverse of the induced homeomorphism is holomorphic, to any order.