Face localizations of affine complex points

A face τ of a cone σ has the larger dual semigroup, so a complex point of the affine chart of τ restricts to a complex point of the affine chart of σ. This restriction TauCeti.Toric.faceAffinePointMap is the map on complex points induced by the algebraic face restriction TauCeti.Toric.faceAffineCoordinateRingMap; it is functorial in face inclusions and equivariant for the coordinate-free complex torus.

When σ is finitely generated and τ = σ ⊓ ker m is cut out by a character m of the dual semigroup of σ, the coordinate ring of τ is the localization of that of σ away from the monomial of m. On complex points this becomes the analytic statement that the face map is an open embedding onto the locus where the monomial of m does not vanish: a point of τ is recovered from its restriction because every character nonnegative on τ becomes nonnegative on σ after adding a multiple of m, and the monomial of m is invertible on τ. The topologies are the monomial-embedding topologies of arbitrary finite generating families, so the statement involves no choice of coordinates.

Every face of a lattice-rational cone is cut out in this way. Its face-map image is therefore described intrinsically, as the locus where every monomial of a character vanishing on the face is nonzero, and the image of the intersection of two faces is the intersection of their images. These open embeddings and their overlaps are the topological input for gluing the affine charts of a fan.

The same recovery formula makes the face map holomorphic in both directions. Give the charts of σ and of τ the complex structures of extending bases. Every monomial of σ pulls back to a monomial of τ, so the face map is holomorphic. Conversely, every monomial of τ is a quotient of two monomials of σ whose denominator does not vanish on the image. Hence a map into the chart of τ is holomorphic exactly when its composite with the face map is. For a regular cone the face map is therefore a holomorphic local diffeomorphism, and with the open embedding property it identifies the chart of the face biholomorphically with an open subset of the chart of σ.

Main declarations

• TauCeti.Toric.faceAffinePointMap: restriction of complex points along a face inclusion, with TauCeti.Toric.faceAffinePointMap_eq_comp identifying it with the complex points of the algebraic face restriction, and TauCeti.Toric.faceAffinePointMap_id, TauCeti.Toric.faceAffinePointMap_comp and TauCeti.Toric.faceAffinePointMap_smul its functoriality and torus equivariance.
• TauCeti.Toric.continuous_faceAffinePointMap: the face map is continuous.
• TauCeti.Toric.faceAffinePointMap_apply_single_ne_zero: a restricted point does not vanish on the monomial of a character vanishing on the face.
• TauCeti.Toric.injective_faceAffinePointMap_of_inf_ker_eq, TauCeti.Toric.range_faceAffinePointMap_of_inf_ker_eq and TauCeti.Toric.isOpenEmbedding_faceAffinePointMap_of_inf_ker_eq: for a face cut out by a character m of a finitely generated cone, the face map is an open embedding onto the locus where the monomial of m does not vanish.
• TauCeti.Toric.IsLatticeRational.range_faceAffinePointMap, TauCeti.Toric.IsLatticeRational.isOpenEmbedding_faceAffinePointMap and TauCeti.Toric.IsLatticeRational.range_faceAffinePointMap_inf: the same for every face of a lattice-rational cone, with an intrinsic description of the image and its behaviour on intersections of faces.
• TauCeti.Toric.contMDiff_faceAffinePointMap: the face map is holomorphic for the complex structures of regular cone coordinates.
• TauCeti.Toric.contMDiffOn_faceAffinePointMap_comp_iff_of_inf_ker_eq and TauCeti.Toric.IsRegularCone.contMDiffOn_faceAffinePointMap_comp_iff: a map into the chart of the face is holomorphic exactly when its composite with the face map is.
• TauCeti.Toric.IsRegularCone.faceAffinePointPartialDiffeomorph: the biholomorphism from a face chart onto the open range of its localization map.
• TauCeti.Toric.IsRegularCone.isLocalDiffeomorph_faceAffinePointMap: for a face of a regular cone, the face map is a holomorphic local diffeomorphism.

References

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

The face map on complex points

noncomputable def TauCeti.Toric.faceAffinePointMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτσ : τ.IsFaceOf σ) : AffineSemigroupComplexPoint ↥(dualSemigroup hi τ) → AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)

The map on complex points induced by a face inclusion τ ≼ σ: the dual semigroup of σ is contained in that of τ, so a complex point of the affine chart of τ restricts to a complex point of the affine chart of σ.

theorem TauCeti.Toric.faceAffinePointMap_def {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτσ : τ.IsFaceOf σ) : faceAffinePointMap hi hτσ = AffineSemigroupComplexPoint.comap (AddSubmonoid.inclusion ⋯)

The face map is the pullback of complex points along the inclusion of dual semigroups.

@[simp]

theorem TauCeti.Toric.faceAffinePointMap_apply_single {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτσ : τ.IsFaceOf σ) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi τ)) (m : ↥(dualSemigroup hi σ)) : (faceAffinePointMap hi hτσ x) (MonoidAlgebra.single (Multiplicative.ofAdd m) 1) = x (MonoidAlgebra.single (Multiplicative.ofAdd ⟨↑m, ⋯⟩) 1)

The restriction of a point takes the same value on the monomial of a character.

theorem TauCeti.Toric.faceAffinePointMap_eq_comp {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτσ : τ.IsFaceOf σ) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi τ)) : faceAffinePointMap hi hτσ x = AlgHom.comp x (faceAffineCoordinateRingMap hi hτσ)

The face map on complex points is precomposition with the algebraic restriction of coordinate rings along the face inclusion.

@[simp]

theorem TauCeti.Toric.faceAffinePointMap_id {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ : PointedCone ℝ V} (hi : IsIntegralLattice i) : faceAffinePointMap hi ⋯ = id

The face map of a cone viewed as its own face is the identity.

@[simp]

theorem TauCeti.Toric.faceAffinePointMap_faceAffinePointMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ υ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hυτ : υ.IsFaceOf τ) (hτσ : τ.IsFaceOf σ) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi υ)) : faceAffinePointMap hi hτσ (faceAffinePointMap hi hυτ x) = faceAffinePointMap hi ⋯ x

Restricting along two successive face inclusions is restricting along the composite face inclusion.

theorem TauCeti.Toric.faceAffinePointMap_comp {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ υ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hυτ : υ.IsFaceOf τ) (hτσ : τ.IsFaceOf σ) : faceAffinePointMap hi hτσ ∘ faceAffinePointMap hi hυτ = faceAffinePointMap hi ⋯

The face maps compose along composite face inclusions.

@[simp]

theorem TauCeti.Toric.faceAffinePointMap_smul {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτσ : τ.IsFaceOf σ) (t : ComplexTorus N) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi τ)) : faceAffinePointMap hi hτσ (t • x) = t • faceAffinePointMap hi hτσ x

The face map is equivariant for the coordinate-free complex torus.

theorem TauCeti.Toric.continuous_faceAffinePointMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} {r r' : ℕ} (hi : IsIntegralLattice i) (hτσ : τ.IsFaceOf σ) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) r) (h : AddGeneratingFamily (↥(dualSemigroup hi τ)) r') : Continuous (faceAffinePointMap hi hτσ)

The face map is continuous for the monomial-embedding topologies of arbitrary finite generating families.

Nonvanishing and recovery from the restriction

theorem TauCeti.Toric.faceAffinePointMap_apply_single_ne_zero {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hτσ : τ.IsFaceOf σ) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi τ)) {m : ↥(dualSemigroup hi σ)} (hm : ∀ v ∈ τ, (hi.realCharacter ↑m) v = 0) : (faceAffinePointMap hi hτσ x) (MonoidAlgebra.single (Multiplicative.ofAdd m) 1) ≠ 0

A restricted point does not vanish on the monomial of a character of the dual semigroup of σ that vanishes on the face τ: the negative of such a character is nonnegative on τ, so its monomial is invertible on the chart of τ.

Faces cut out by a character

theorem TauCeti.Toric.injective_faceAffinePointMap_of_inf_ker_eq {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : Submodule.FG σ) (hτσ : τ.IsFaceOf σ) (m : ↥(dualSemigroup hi σ)) (hm : σ ⊓ ↑(LinearMap.ker (hi.realCharacter ↑m)) = τ) : Function.Injective (faceAffinePointMap hi hτσ)

For a face τ cut out by a character m of the dual semigroup of a finitely generated cone σ, a complex point of the chart of τ is determined by its restriction to the chart of σ.

theorem TauCeti.Toric.range_faceAffinePointMap_of_inf_ker_eq {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : Submodule.FG σ) (hτσ : τ.IsFaceOf σ) (m : ↥(dualSemigroup hi σ)) (hm : σ ⊓ ↑(LinearMap.ker (hi.realCharacter ↑m)) = τ) : Set.range (faceAffinePointMap hi hτσ) = {x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ) | x (MonoidAlgebra.single (Multiplicative.ofAdd m) 1) ≠ 0}

For a face τ cut out by a character m of the dual semigroup of a finitely generated cone σ, the image of the chart of τ in the chart of σ is the locus where the monomial of m does not vanish.

theorem TauCeti.Toric.isOpenEmbedding_faceAffinePointMap_of_inf_ker_eq {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} {r r' : ℕ} (hi : IsIntegralLattice i) (hσ : Submodule.FG σ) (hτσ : τ.IsFaceOf σ) (m : ↥(dualSemigroup hi σ)) (hm : σ ⊓ ↑(LinearMap.ker (hi.realCharacter ↑m)) = τ) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) r) (h : AddGeneratingFamily (↥(dualSemigroup hi τ)) r') : Topology.IsOpenEmbedding (faceAffinePointMap hi hτσ)

For a face τ cut out by a character m of the dual semigroup of a finitely generated cone σ, the face map is an open embedding of the chart of τ into the chart of σ, for the monomial-embedding topologies of arbitrary finite generating families.

theorem TauCeti.Toric.range_faceAffinePointMap_of_exists_inf_ker_eq {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : Submodule.FG σ) (hτσ : τ.IsFaceOf σ) (hτ : ∃ (m : ↥(dualSemigroup hi σ)), σ ⊓ ↑(LinearMap.ker (hi.realCharacter ↑m)) = τ) : Set.range (faceAffinePointMap hi hτσ) = {x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ) | ∀ (m : ↥(dualSemigroup hi σ)), (∀ v ∈ τ, (hi.realCharacter ↑m) v = 0) → x (MonoidAlgebra.single (Multiplicative.ofAdd m) 1) ≠ 0}

For a face τ of a finitely generated cone σ cut out by a character, the image of the chart of τ in the chart of σ is intrinsically the locus where every monomial of a character vanishing on τ is nonzero.

theorem TauCeti.Toric.range_faceAffinePointMap_inf_of_inf_ker_eq {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ υ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : Submodule.FG σ) (hτσ : τ.IsFaceOf σ) (hυσ : υ.IsFaceOf σ) (m₁ : ↥(dualSemigroup hi σ)) (h₁ : σ ⊓ ↑(LinearMap.ker (hi.realCharacter ↑m₁)) = τ) (m₂ : ↥(dualSemigroup hi σ)) (h₂ : σ ⊓ ↑(LinearMap.ker (hi.realCharacter ↑m₂)) = υ) : Set.range (faceAffinePointMap hi ⋯) = Set.range (faceAffinePointMap hi hτσ) ∩ Set.range (faceAffinePointMap hi hυσ)

If two faces of a finitely generated cone are cut out by characters, the image of their intersection is the intersection of their images.

Faces of lattice-rational cones

theorem TauCeti.Toric.IsLatticeRational.range_faceAffinePointMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsLatticeRational i σ) (hτσ : τ.IsFaceOf σ) : Set.range (faceAffinePointMap hi hτσ) = {x : AffineSemigroupComplexPoint ↥(dualSemigroup hi σ) | ∀ (m : ↥(dualSemigroup hi σ)), (∀ v ∈ τ, (hi.realCharacter ↑m) v = 0) → x (MonoidAlgebra.single (Multiplicative.ofAdd m) 1) ≠ 0}

For a face τ of a lattice-rational cone σ, the image of its chart in the chart of σ is the locus where the monomial of every character of the dual semigroup of σ vanishing on τ is nonzero.

theorem TauCeti.Toric.IsLatticeRational.isOpenEmbedding_faceAffinePointMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} {r r' : ℕ} (hi : IsIntegralLattice i) (hσ : IsLatticeRational i σ) (hτσ : τ.IsFaceOf σ) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) r) (h : AddGeneratingFamily (↥(dualSemigroup hi τ)) r') : Topology.IsOpenEmbedding (faceAffinePointMap hi hτσ)

For a face τ of a lattice-rational cone σ, the face map is an open embedding of the chart of τ into the chart of σ, for the monomial-embedding topologies of arbitrary finite generating families.

theorem TauCeti.Toric.IsLatticeRational.range_faceAffinePointMap_inf {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ υ : PointedCone ℝ V} (hi : IsIntegralLattice i) (hσ : IsLatticeRational i σ) (hτσ : τ.IsFaceOf σ) (hυσ : υ.IsFaceOf σ) : Set.range (faceAffinePointMap hi ⋯) = Set.range (faceAffinePointMap hi hτσ) ∩ Set.range (faceAffinePointMap hi hυσ)

For two faces τ and υ of a lattice-rational cone σ, the image of the chart of τ ⊓ υ in the chart of σ is the intersection of the images of the charts of τ and of υ.

Holomorphy

theorem TauCeti.Toric.contMDiff_faceAffinePointMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} {r r' : ℕ} (hi : IsIntegralLattice i) {k l k' l' : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} {B' : Module.Basis (ToricRay τ ⊕ Fin l') ℤ N} (hτσ : τ.IsFaceOf σ) (hσ : IsToricCone i σ) (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) r) (hB' : ∀ (ρ : ToricRay τ), IsPrimitiveGenerator i ρ (B' (Sum.inl ρ))) (κ' : ToricRay τ ≃ Fin k') (h : AddGeneratingFamily (↥(dualSemigroup hi τ)) r') (n : WithTop ℕ∞) : let x := affinePointTopology g; let x_1 := affinePointTopology h; have x_2 := coneChartedSpace hi hσ hB κ g; have x_3 := coneChartedSpace hi ⋯ hB' κ' h; ContMDiff (modelWithCornersSelf ℂ ((Fin k' → ℂ) × (Fin l' → ℂ))) (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) n (faceAffinePointMap hi hτσ)

The face map is holomorphic for the complex structures of the regular affine charts of the cone and of its face.

theorem TauCeti.Toric.contMDiffOn_faceAffinePointMap_comp_iff_of_inf_ker_eq {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} {r r' : ℕ} (hi : IsIntegralLattice i) {k l k' l' : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} {B' : Module.Basis (ToricRay τ ⊕ Fin l') ℤ N} (hτσ : τ.IsFaceOf σ) (hσ : IsToricCone i σ) (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) r) (hB' : ∀ (ρ : ToricRay τ), IsPrimitiveGenerator i ρ (B' (Sum.inl ρ))) (κ' : ToricRay τ ≃ Fin k') (h : AddGeneratingFamily (↥(dualSemigroup hi τ)) r') (m : ↥(dualSemigroup hi σ)) (hm : σ ⊓ ↑(LinearMap.ker (hi.realCharacter ↑m)) = τ) {E : Type u_3} {H : Type u_4} {M : Type u_5} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [TopologicalSpace M] [ChartedSpace H M] {f : M → AffineSemigroupComplexPoint ↥(dualSemigroup hi τ)} {t : Set M} {n : WithTop ℕ∞} : let x := affinePointTopology g; let x_1 := affinePointTopology h; have x_2 := coneChartedSpace hi hσ hB κ g; have x_3 := coneChartedSpace hi ⋯ hB' κ' h; ContMDiffOn I (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) n (faceAffinePointMap hi hτσ ∘ f) t ↔ ContMDiffOn I (modelWithCornersSelf ℂ ((Fin k' → ℂ) × (Fin l' → ℂ))) n f t

For a face τ cut out by a character m of the dual semigroup of σ, a map into the chart of τ is holomorphic on a set exactly when its composite with the face map into the chart of σ is.

theorem TauCeti.Toric.IsRegularCone.contMDiffOn_faceAffinePointMap_comp_iff {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} {r r' : ℕ} (hi : IsIntegralLattice i) {k l k' l' : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} {B' : Module.Basis (ToricRay τ ⊕ Fin l') ℤ N} (hσ : IsRegularCone i σ) (hτσ : τ.IsFaceOf σ) (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) r) (hB' : ∀ (ρ : ToricRay τ), IsPrimitiveGenerator i ρ (B' (Sum.inl ρ))) (κ' : ToricRay τ ≃ Fin k') (h : AddGeneratingFamily (↥(dualSemigroup hi τ)) r') {E : Type u_3} {H : Type u_4} {M : Type u_5} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [TopologicalSpace M] [ChartedSpace H M] {f : M → AffineSemigroupComplexPoint ↥(dualSemigroup hi τ)} {t : Set M} {n : WithTop ℕ∞} : let x := affinePointTopology g; let x_1 := affinePointTopology h; have x_2 := coneChartedSpace hi ⋯ hB κ g; have x_3 := coneChartedSpace hi ⋯ hB' κ' h; ContMDiffOn I (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) n (faceAffinePointMap hi hτσ ∘ f) t ↔ ContMDiffOn I (modelWithCornersSelf ℂ ((Fin k' → ℂ) × (Fin l' → ℂ))) n f t

For a face τ of a regular cone σ, a map into the chart of τ is holomorphic on a set exactly when its composite with the face map into the chart of σ is.

noncomputable def TauCeti.Toric.IsRegularCone.faceAffinePointPartialDiffeomorph {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} {r r' : ℕ} (hi : IsIntegralLattice i) {k l k' l' : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} {B' : Module.Basis (ToricRay τ ⊕ Fin l') ℤ N} (hσ : IsRegularCone i σ) (hτσ : τ.IsFaceOf σ) (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) r) (hB' : ∀ (ρ : ToricRay τ), IsPrimitiveGenerator i ρ (B' (Sum.inl ρ))) (κ' : ToricRay τ ≃ Fin k') (h : AddGeneratingFamily (↥(dualSemigroup hi τ)) r') (n : WithTop ℕ∞) : let x := affinePointTopology g; let x_1 := affinePointTopology h; have x_2 := coneChartedSpace hi ⋯ hB κ g; have x_3 := coneChartedSpace hi ⋯ hB' κ' h; PartialDiffeomorph (modelWithCornersSelf ℂ ((Fin k' → ℂ) × (Fin l' → ℂ))) (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) (AffineSemigroupComplexPoint ↥(dualSemigroup hi τ)) (AffineSemigroupComplexPoint ↥(dualSemigroup hi σ)) n

The face localization as a biholomorphism from the affine chart of τ onto its open image in the affine chart of σ.

@[simp]

theorem TauCeti.Toric.IsRegularCone.faceAffinePointPartialDiffeomorph_source {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} {r r' : ℕ} (hi : IsIntegralLattice i) {k l k' l' : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} {B' : Module.Basis (ToricRay τ ⊕ Fin l') ℤ N} (hσ : IsRegularCone i σ) (hτσ : τ.IsFaceOf σ) (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) r) (hB' : ∀ (ρ : ToricRay τ), IsPrimitiveGenerator i ρ (B' (Sum.inl ρ))) (κ' : ToricRay τ ≃ Fin k') (h : AddGeneratingFamily (↥(dualSemigroup hi τ)) r') (n : WithTop ℕ∞) : (faceAffinePointPartialDiffeomorph hi hσ hτσ hB κ g hB' κ' h n).source = Set.univ

The face localization partial diffeomorphism has the whole face chart as its source.

@[simp]

theorem TauCeti.Toric.IsRegularCone.faceAffinePointPartialDiffeomorph_target {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} {r r' : ℕ} (hi : IsIntegralLattice i) {k l k' l' : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} {B' : Module.Basis (ToricRay τ ⊕ Fin l') ℤ N} (hσ : IsRegularCone i σ) (hτσ : τ.IsFaceOf σ) (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) r) (hB' : ∀ (ρ : ToricRay τ), IsPrimitiveGenerator i ρ (B' (Sum.inl ρ))) (κ' : ToricRay τ ≃ Fin k') (h : AddGeneratingFamily (↥(dualSemigroup hi τ)) r') (n : WithTop ℕ∞) : (faceAffinePointPartialDiffeomorph hi hσ hτσ hB κ g hB' κ' h n).target = Set.range (faceAffinePointMap hi hτσ)

The target of the face localization partial diffeomorphism is the range of the face map.

@[simp]

theorem TauCeti.Toric.IsRegularCone.faceAffinePointPartialDiffeomorph_apply {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} {r r' : ℕ} (hi : IsIntegralLattice i) {k l k' l' : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} {B' : Module.Basis (ToricRay τ ⊕ Fin l') ℤ N} (hσ : IsRegularCone i σ) (hτσ : τ.IsFaceOf σ) (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) r) (hB' : ∀ (ρ : ToricRay τ), IsPrimitiveGenerator i ρ (B' (Sum.inl ρ))) (κ' : ToricRay τ ≃ Fin k') (h : AddGeneratingFamily (↥(dualSemigroup hi τ)) r') (n : WithTop ℕ∞) (x : AffineSemigroupComplexPoint ↥(dualSemigroup hi τ)) : ↑(faceAffinePointPartialDiffeomorph hi hσ hτσ hB κ g hB' κ' h n).toPartialEquiv x = faceAffinePointMap hi hτσ x

The face localization partial diffeomorphism acts by restricting complex points.

theorem TauCeti.Toric.IsRegularCone.isLocalDiffeomorph_faceAffinePointMap {N : Type u_1} {V : Type u_2} [AddCommGroup N] [AddCommGroup V] [Module ℝ V] {i : N →+ V} {σ τ : PointedCone ℝ V} {r r' : ℕ} (hi : IsIntegralLattice i) {k l k' l' : ℕ} {B : Module.Basis (ToricRay σ ⊕ Fin l) ℤ N} {B' : Module.Basis (ToricRay τ ⊕ Fin l') ℤ N} (hσ : IsRegularCone i σ) (hτσ : τ.IsFaceOf σ) (hB : ∀ (ρ : ToricRay σ), IsPrimitiveGenerator i ρ (B (Sum.inl ρ))) (κ : ToricRay σ ≃ Fin k) (g : AddGeneratingFamily (↥(dualSemigroup hi σ)) r) (hB' : ∀ (ρ : ToricRay τ), IsPrimitiveGenerator i ρ (B' (Sum.inl ρ))) (κ' : ToricRay τ ≃ Fin k') (h : AddGeneratingFamily (↥(dualSemigroup hi τ)) r') (n : WithTop ℕ∞) : let x := affinePointTopology g; let x_1 := affinePointTopology h; have x_2 := coneChartedSpace hi ⋯ hB κ g; have x_3 := coneChartedSpace hi ⋯ hB' κ' h; IsLocalDiffeomorph (modelWithCornersSelf ℂ ((Fin k' → ℂ) × (Fin l' → ℂ))) (modelWithCornersSelf ℂ ((Fin k → ℂ) × (Fin l → ℂ))) n (faceAffinePointMap hi hτσ)

The face map is a holomorphic local diffeomorphism from the face chart to the cone chart.