diff --git a/TauCetiRoadmap/AnalyticToricGeometry/README.md b/TauCetiRoadmap/AnalyticToricGeometry/README.md new file mode 100644 index 00000000..90ac3449 --- /dev/null +++ b/TauCetiRoadmap/AnalyticToricGeometry/README.md @@ -0,0 +1,337 @@ +# Roadmap: analytic toric geometry + +This roadmap constructs algebraic and complex-analytic toric varieties from finite regular +rational fans. It supplies the algebraic cone-to-fan layer that is not yet exposed by the Toric +project, then builds complex points, analytic charts, gluing, torus actions, orbit strata, +normal-crossings boundary components, toric maps, properness, and the algebraic--analytic +comparison. + +The public API has one toric dialect. Cones are Mathlib `PointedCone`s with additional +predicates, affine charts are schemes built from monoid algebras, and gluing uses the common +scheme and `TopCat.GlueData` carriers. Basis-dependent coordinates are theorems, not definitions +of the global objects. + +Suggested homes: `TauCeti/Geometry/Toric/Algebraic/` for the common algebraic supplier and +`TauCeti/Geometry/Toric/Analytic/` for complex realization. + +## Scope and completion criterion + +The scope is smooth complex toric geometry for **finite regular rational fans**. Restricting to +finite fans makes all algebraic realizations quasi-compact and avoids an ambiguous notion of +local finiteness: every cone contains the origin, and every affine toric chart contains the dense +torus, so neither the cone family near the origin nor the affine-chart cover can be locally finite +in the naive sense. + +Singular toric analytic spaces, infinite fans, general analytification, coherent toric sheaves, +intersection theory, symplectic moment maps, and special deformation retractions are outside the +roadmap. + +The roadmap is complete when Tau Ceti supplies all of the following. + +1. A Toric-compatible algebraic API for rational salient polyhedral cones, primitive rays, + regularity, finite fans, fan morphisms, dual semigroups, affine toric schemes, face + localizations, fan gluing, torus actions, and algebraic toric maps. +2. Every regular cone has an analytic affine chart on the complex points of its algebraic affine + scheme. Its topology comes from a finite monomial embedding and is independent of the chosen + semigroup generators. A basis extending the primitive ray generators gives a biholomorphism + with `C^k x (C^*)^(n-k)`, independent of the extending basis. +3. Every finite regular fan has a Hausdorff second-countable complex manifold obtained by gluing + its affine analytic charts along face localizations. Character functions, chart inclusions, + and the torus action are holomorphic. +4. Cones correspond naturally to torus orbits. The complement of the dense torus is a finite + union of closed embedded complex hypersurfaces indexed by rays, with reduced multiplicity one + and the local coordinate-hyperplane simple-normal-crossings form. +5. A fan morphism induces a holomorphic toric map. Identity, composition, products, open subfans, + and restrictions agree definitionally or by named natural isomorphisms. For finite source and + target fans, the cone-by-cone support criterion characterizes properness. +6. The analytic realization is naturally biholomorphic, as a toric space, to the global complex + points `Hom(Spec C, X_Sigma)` of the algebraic fan scheme. This comparison commutes with + affine charts, characters, orbit strata, boundary components, and toric maps. +7. A finite regular fan is complete exactly when its analytic realization is compact. The + standard fans for affine space, the algebraic torus, projective space, products, and a star + subdivision satisfy the expected comparison and properness theorems. + +## Ownership and dependencies + +- **This roadmap owns the missing cone-to-fan algebraic supplier.** The public Toric project + supplies `AlgebraicGeometry.ToricVariety` in `Toric.ToricVariety.Defs`, the affine-monoid + construction in `Toric.ToricVariety.FromMonoid`, and the common torus and monoid-algebra + infrastructure. It does not supply rational toric cones, fans, fan schemes, or their morphisms. + Layer 0 below supplies those objects in the same vocabulary rather than treating a prospective + external API as a dependency. +- **Matching external declarations are consumed immediately.** Before implementing a Layer 0 + declaration, search Toric, Mathlib, and active pull requests. If the exact object and laws + exist, import them and delete the local target. Otherwise implement the target here with the + public shape below. Analytic work never pauses for external upstreaming, and this roadmap does + not assign work to another project. +- **Mathlib owns convex-cone vocabulary.** Use `PointedCone`, `PointedCone.FG`, + `PointedCone.DualFG`, `PointedCone.IsFaceOf`, `PointedCone.Face`, + `ConvexCone.Salient`, cone hulls, maps, duals, and the face lattice. A toric cone is a predicate + on that carrier, not a replacement carrier. +- **The Toric project owns its existing scheme-level vocabulary.** Consume its tori, + diagonalizable group schemes, monoid algebras, `ToricVariety` class, and affine-monoid + construction. Layer 0 connects fan combinatorics to those objects; it does not put analytic + fields into them. +- **The complex-manifolds roadmap owns analytic atlas transport, open gluing, compatible + structure-groupoid atlases, and biholomorphism vocabulary.** This roadmap supplies toric + affine charts and verifies the hypotheses of those generic theorems. +- **General scheme analytification is not claimed.** The comparison is toric and chartwise. It + identifies affine functor-of-points carriers, proves compatibility on face localizations, and + glues those comparisons. + +## Pinned conventions + +These conventions are acceptance conditions. + +- An integral lattice is a finite free `Z`-module `N`, a finite-dimensional real vector space + `N_R`, an additive map `i : N -> N_R`, and an `R`-linear equivalence + `R tensor[Z] N ≃ N_R` sending `1 tensor n` to `i(n)`. Injectivity, discreteness, spanning, and + equality of the integral and real ranks are consequences. An injective dense map with full + real span is not accepted as a lattice. +- A toric cone is a Mathlib `PointedCone R N_R` satisfying finite generation, generation by + finitely many lattice vectors, and `ConvexCone.Salient`. Salience is the condition + `sigma inter (-sigma) = {0}`; Mathlib's name `PointedCone` alone does not assert it. +- Rays are one-dimensional Mathlib faces. Their primitive lattice generators are derived by an + existence-and-uniqueness theorem. A cone record does not store an arbitrary generator list. +- Regularity includes the toric-cone hypothesis and says that all primitive ray generators occur + in one integral basis. It is never a standalone property of an irrational or nonsalient cone. + The analytic layer consumes such a basis and proves independence from its choice. +- A fan is a finite set of toric cones, closed under faces, whose pairwise intersections are + faces of both cones. A fan morphism is an integral lattice map, its compatible real-linear map, + and the theorem that each source cone maps into a target cone. +- The dual semigroup is the additive submonoid of integral characters nonnegative on the cone. + The affine chart is the spectrum of its complex monoid algebra. Face inclusions act through + localization and affine open immersions. +- The dense complex torus is represented coordinate-freely by multiplicative characters of the + integral character lattice. It becomes `(C^*)^n` only after choosing a basis. +- Affine complex points are algebra homomorphisms from the complex monoid algebra to `C`. Their + topology is induced by evaluation on a finite semigroup generating family. Independence from + that family is proved before any regular-coordinate homeomorphism. +- A mixed chart is `C^k x (C^*)^l`. A mixed monomial map has natural-number exponents from + noninvertible source coordinates and integer exponents from invertible source coordinates. + No noninvertible source coordinate may contribute to an invertible target coordinate. +- Gluing uses `TopCat.GlueData.glued`. The analytic realization is not a second tagged quotient. +- Global algebraic complex points mean scheme morphisms `Spec C -> X`, not the underlying + prime-ideal space of `X`. +- The toric boundary is a finite ray-indexed family of closed embedded complex hypersurfaces. + Its simple-normal-crossings conclusion is a complex local biholomorphism, represented by a + complex `PartialDiffeomorph`, under which the components are coordinate hyperplanes. A merely + topological `PartialHomeomorph` does not establish this conclusion. +- Properness is stated only for finite fans. For every target cone `tau`, the inverse image of + `tau` under the real-linear map equals the support of the source cones mapped into `tau`. + +## Existing foundations to consume + +At the dependency pin, the following anchors already exist. + +- Mathlib's ordered-cone hierarchy, including finite generation, dual finite generation, + simpliciality, salience, faces, maps, and the face lattice. +- Finite free modules, scalar extension, `Basis`, `Module.Dual`, `Finsupp`, matrices, additive + submonoids, monoid algebras, localizations, affine schemes, and scheme gluing. +- The Toric modules for diagonalizable group schemes, tori, monoid algebras, + `AlgebraicGeometry.ToricVariety`, and affine toric varieties from affine monoids. +- Complex differentiability, finite products, open subspaces, complex manifolds, local + diffeomorphisms, and structure groupoids. +- `TopCat.GlueData`, its canonical open embeddings, its open-set criterion, and its colimit + universal property. +- Proper maps, compactness, local compactness, quotient maps, and second-countability tools. + +## Layer 0: the Toric-compatible algebraic supplier + +This layer closes the algebraic prerequisite chain. Each item has an exact carrier and feeds the +representative declarations in `Suggested.lean`. + +1. Define the integral-lattice predicate by an `R`-linear equivalence + `R tensor[Z] N ≃ N_R` whose restriction to `1 tensor N` is the chosen lattice map. Derive + injectivity, discreteness, spanning, equality of integral and real ranks, and naturality under + integral linear maps. +2. Define `IsToricCone i sigma` on a Mathlib `PointedCone` by finite generation, lattice + rationality, and salience. Prove preservation under faces, intersections, products, injective + integral maps, and lattice equivalences. +3. Define rays as one-dimensional Mathlib faces. Prove existence and uniqueness of the primitive + generator of every ray, finiteness of the ray type, generation of the cone by its primitive + rays, and naturality under lattice equivalences. +4. Define regularity as the conjunction of `IsToricCone` with the existence of an integral basis + containing every primitive ray generator. Prove regular cones are simplicial and that faces + and products of regular cones are regular. Pin the block form relating two extending bases. +5. Define a finite fan as a finite set of toric cones closed under faces with pairwise + intersections a face of each. Define support, completeness, open subfans, products, + subdivisions, and fan morphisms. Prove identity, composition, and support functoriality. +6. Define the dual affine semigroup as the additive submonoid of integral characters + nonnegative on a cone. Prove finite generation, face-localization, functoriality, and the + regular-coordinate equivalence with `N^k x Z^(n-k)`. +7. Construct the affine toric scheme as the spectrum of the complex monoid algebra. Connect it + to the Toric project's affine-monoid `ToricVariety` instance, identify its dense torus, and + construct the torus action. +8. For every face inclusion, construct the localization map and prove it is an affine open + immersion. Prove identity, composition, pairwise-overlap, and cocycle laws. +9. Glue the affine schemes of a finite fan along these open immersions. Construct the global + dense torus, torus action, cone opens, and algebraic toric maps. Prove identity, composition, + products, open-subfan restriction, and naturality of the affine inclusions. + +**Source spine:** Cox--Little--Schenck, Chapters 1 and 3; Fulton, Chapter 1 and §2.1; the public +Toric modules named above. + +## Layer 1: characters and mixed monomial maps + +1. Define evaluation of an integral character on the complex torus without choosing a basis. + Prove its multiplicative laws, separation of points, compatibility with lattice maps, and its + Laurent-monomial formula after choosing a basis. +2. For a semigroup homomorphism, construct the contravariant map on affine complex points. Prove + compatibility with the monoid-algebra map, continuity for monomial-embedding topologies, and + independence from chosen generators. +3. Define typed mixed exponent data for maps + `C^k x (C^*)^l -> C^k' x (C^*)^l'`. Prove preservation of the invertible-coordinate locus, + holomorphy there, identity, composition **on that locus**, products, Jacobian formulas, and + biholomorphicity for the appropriate unimodular block matrices. No composition theorem is + stated on ambient points with a zero torus coordinate, where integer-power conventions break + exponent arithmetic. +4. Prove that localization along a face gives an open complex subspace and a biholomorphism onto + its image. Verify the cocycle equations for successive face inclusions. + +**Source spine:** Cox--Little--Schenck, §§1.1--1.3 and §3.1; Fulton, §§1.2--1.3. + +## Layer 2: affine analytic charts of regular cones + +1. Put the finite-monomial-embedding topology on the affine complex-point carrier. Prove + independence from the generating family, Hausdorffness, local compactness, and second + countability. +2. For a regular cone of dimension `k` in a rank-`n` lattice, use an extending basis to construct + a biholomorphism with `C^k x (C^*)^(n-k)`. Prove its coordinate functions are the expected + characters. +3. Install the named complex `ChartedSpace` and prove `IsManifold`. Show that changing the + extending basis preserves the complex structure through the corresponding mixed monomial + biholomorphism. +4. Identify the dense torus as an open submanifold and the orbit associated to every face as a + locally closed complex submanifold. Compute its dimension and closure relation. +5. Prove that face localization is an open holomorphic embedding and agrees on carriers with + complex points of the algebraic open immersion. + +**Source spine:** Fulton, §§1.2 and 2.1; Cox--Little--Schenck, §§1.2, 3.1, and 3.3. + +## Layer 3: finite-fan analytic gluing + +1. Form the `TopCat.GlueData` diagram of affine charts and face-localization overlaps. Derive its + symmetry and cocycle equations from the fan intersection axiom and Layer 0 localization laws. +2. Apply the complex-manifold gluing theorem to `TopCat.GlueData.glued`. Prove every affine chart + inclusion is an open holomorphic embedding and every cone-orbit chart agrees on overlaps. +3. Prove Hausdorffness from the fan intersection property and closedness of the generated gluing + relation. The proof must separate points in noncommon faces rather than store separation in a + fan record. +4. Prove second countability from finiteness of the chart family and second countability of each + affine chart. Prove local compactness and finite dimensionality. +5. Establish invariance under fan equivalence and functoriality for open subfans. A subdivision + produces a holomorphic map to the original realization, not an asserted isomorphism. + +**Source spine:** Fulton, §§1.4 and 2.4; Cox--Little--Schenck, §§3.1 and 3.4; Oda, Chapter I. + +## Layer 4: torus actions, strata, and the boundary + +1. Glue the affine torus actions and prove the group law, joint continuity, holomorphy, and + equivariance of chart inclusions and character functions. +2. Prove the orbit--cone correspondence as an order-reversing equivalence between cones and + torus orbits. Compute stabilizers and quotient tori using sublattices. +3. For each ray, construct the invariant closed embedded complex hypersurface. Prove that the + finite union of these components is exactly the complement of the dense torus and that every + component has reduced multiplicity one. +4. At every point, construct a regular affine chart, the finite set of boundary components + through the point, and an injection from those components to coordinate indices. Make this a + complex local biholomorphism and prove that a point of the chart lies in a component exactly + when the corresponding holomorphic coordinate vanishes. +5. Deduce transversality and the intersection formula indexed by cones. Prove naturality under + fan isomorphisms, products, and open subfans. + +**Source spine:** Fulton, §§2.1--2.2 and §3.1; Cox--Little--Schenck, §§3.2--3.3 and §4.1. + +## Layer 5: toric maps and properness + +1. Glue the affine mixed monomial maps attached to a fan morphism. Prove holomorphy, identity, + composition, product compatibility, and uniqueness from the dense torus. +2. Describe preimages of affine cone charts and orbit strata cone by cone. Prove restriction and + base-change results for open subfans. +3. For finite source and target fans, prove that the analytic map is proper exactly when, for + every target cone, its real-linear inverse image equals the support of the source cones mapped + into that cone. +4. Deduce that the realization of a complete finite fan is compact and that a star subdivision + induces a proper map because the supports agree. +5. Prove that a fan isomorphism induces a biholomorphism, with inverse induced by the inverse fan + morphism. + +**Source spine:** Fulton, §2.4; Cox--Little--Schenck, §3.3 and Theorem 3.4.11. + +## Layer 6: global algebraic--analytic comparison + +1. For every cone, compare algebra homomorphisms from its complex monoid algebra to `C` with + morphisms `Spec C -> U_sigma`. Prove compatibility with the independent monomial-embedding + topology. +2. Prove that complex points preserve the finite affine-open gluing used to construct the fan + scheme. Identify the resulting topological gluing with `TopCat.GlueData.glued` and show that + both overlap maps are the same face-localization maps. +3. Glue the affine comparisons to a torus-equivariant homeomorphism from + `Hom(Spec C, X_Sigma)` to the analytic realization. Prove it and its inverse are holomorphic. +4. Prove naturality for fan morphisms, characters, products, orbit inclusions, and boundary + components. The comparison identifies analytic compactness with algebraic completeness + through the common finite-fan support criterion. + +**Source spine:** Cox--Little--Schenck, Chapters 1 and 3; Fulton, Chapters 1--2; Gunning--Rossi, +Chapter I. + +## Dependency order + +| Track | Depends on | Feeds | +| --- | --- | --- | +| L0 algebraic supplier | Mathlib and the existing Toric modules | every later layer | +| L1 character and mixed-monomial calculus | L0, Mathlib complex analysis | L2, L5--L6 | +| L2 affine regular charts | L0--L1, complex manifolds | L3--L6 | +| L3 finite-fan gluing | L2, complex-manifold gluing | L4--L6 | +| L4 orbit and boundary theory | L2--L3 | L6 and downstream geometry | +| L5 maps and properness | L1--L3 | L6 and compactness applications | +| L6 global comparison | L0--L5 | reusable analytic realization | + +After L0 fixes the carriers, L1's character calculus and the generator-independence part of L2 +can proceed in parallel. L4 and L5 can proceed independently after L3. L6 joins those tracks. + +## Acceptance checks + +- The map `ℤ² -> ℝ`, `(a,b) |-> a + √2 b`, is rejected as an integral lattice even though it + is injective and has full real span. It cannot produce two competing primitive generators of + the same ray. +- The full line in a rank-one real lattice is a Mathlib `PointedCone` but fails the toric-cone + salience predicate. Its dual semigroup gives a point; it is never accepted as the cone of an + affine toric curve with a dense one-dimensional torus. +- The affine ray cone produces `C`, the zero cone produces `C^*`, and face localization is the + ordinary inclusion `C^* -> C`. +- A rank-`n` regular cone of dimension `k` produces a chart biholomorphic to + `C^k x (C^*)^(n-k)`. Two extending bases give the same atlas. +- A mixed monomial with a negative exponent in a noninvertible source coordinate is rejected by + its type. Identity and composition agree with matrix block composition on `mixedChartDomain`; + no equality is claimed at ambient points with zero torus coordinates. +- The fan with only the zero cone produces the coordinate-free complex torus. A basis identifies + it with `(C^*)^n`, and changing basis acts by the corresponding Laurent monomial map. +- The standard complete fan produces complex projective space with its standard affine charts; + the comparison respects homogeneous-coordinate monomials. +- Product fans realize as products of complex manifolds, with matching character and orbit + formulas. +- A star subdivision gives the expected proper toric map through the finite-fan support + criterion. +- The boundary is proved to be a finite ray-indexed family of closed embedded complex + hypersurfaces through a holomorphic coordinate-hyperplane local normal form. A + `PartialHomeomorph` or a stored SNC assertion is insufficient. +- The global comparison starts from `Hom(Spec C, X_Sigma)`, agrees on every affine chart and + overlap, and is natural for toric maps. An unrelated homeomorphism of final carriers is + insufficient. +- No public declaration introduces a competing convex-cone, semigroup-algebra, scheme, gluing + quotient, or biholomorphism carrier. + +## References + +- William Fulton, *Introduction to Toric Varieties*, Annals of Mathematics Studies 131, + Princeton University Press, 1993, especially Chapters 1--2. +- David Cox, John Little, and Henry Schenck, *Toric Varieties*, Graduate Studies in Mathematics + 124, American Mathematical Society, 2011, especially Chapters 1, 3, and 4. +- Tadao Oda, *Convex Bodies and Algebraic Geometry*, Ergebnisse der Mathematik 15, + Springer, 1988, Chapter I. +- Robert Gunning and Hugo Rossi, *Analytic Functions of Several Complex Variables*, Prentice-Hall, + 1965, Chapter I. +- Yaël Dillies et al., [*Toric varieties in Lean*](https://github.com/YaelDillies/Toric), for + the existing tori, monoid-algebra, affine-monoid, and `ToricVariety` interfaces consumed here. diff --git a/TauCetiRoadmap/AnalyticToricGeometry/Suggested.lean b/TauCetiRoadmap/AnalyticToricGeometry/Suggested.lean new file mode 100644 index 00000000..a4b76343 --- /dev/null +++ b/TauCetiRoadmap/AnalyticToricGeometry/Suggested.lean @@ -0,0 +1,395 @@ +import Mathlib + +/-! +# Analytic toric geometry: target signatures + +**This file is not the roadmap and is not exhaustive.** The definitive document is +`README.md`. These declarations pin representative interfaces for the algebraic supplier, +finite-fan analytic realization, mixed monomial calculus, boundary normal forms, properness, +and the comparison with algebraic complex points. + +The algebraic structures below are built on Mathlib carriers. In particular, a toric cone is a +predicate on `PointedCone`, and affine charts use monoid algebras and schemes. They are the +Toric-compatible prerequisites that this roadmap supplies until an identical external API can +be imported. +-/ + +namespace TauCetiRoadmap.AnalyticToricGeometry + +open AlgebraicGeometry CategoryTheory Topology +open scoped BigOperators +open scoped ContDiff Manifold +open scoped TensorProduct + +universe u + +/-! ## Integral lattices and toric cones -/ + +section AlgebraicSupplier + +variable {N V : Type u} [AddCommGroup N] [Module ℤ N] [Module.Free ℤ N] [Module.Finite ℤ N] + [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] + +/-- Full integral-lattice data in a real vector space. The scalar-extension equivalence rules out +dense injective images such as `ℤ² → ℝ`, `(a,b) ↦ a + √2 b`; cones remain Mathlib +`PointedCone`s in the ambient space. -/ +def IsIntegralLattice (i : N →+ V) : Prop := + ∃ scalarExtension : TensorProduct ℤ ℝ N ≃ₗ[ℝ] V, + ∀ n : N, scalarExtension ((1 : ℝ) ⊗ₜ[ℤ] n) = i n + +/-- Rationality of a cone means generation by finitely many lattice vectors. -/ +def IsLatticeRational (i : N →+ V) (sigma : PointedCone ℝ V) : Prop := + ∃ s : Finset N, sigma = PointedCone.hull ℝ (i '' (s : Set N)) + +/-- A toric cone is a finitely generated, lattice-rational, salient Mathlib pointed cone. -/ +structure IsToricCone (i : N →+ V) (sigma : PointedCone ℝ V) : Prop where + fg : sigma.FG + rational : IsLatticeRational i sigma + salient : (sigma : ConvexCone ℝ V).Salient + +/-- One-dimensional faces of a toric cone. -/ +def ToricRay (sigma : PointedCone ℝ V) := + {rho : sigma.Face // + Module.finrank ℝ (Submodule.span ℝ ((rho : PointedCone ℝ V) : Set V)) = 1} + +/-- A primitive lattice generator pointing along a ray. -/ +def IsPrimitiveGenerator (i : N →+ V) {sigma : PointedCone ℝ V} + (rho : ToricRay sigma) (v : N) : Prop := + i v ∈ (rho.1 : PointedCone ℝ V) ∧ v ≠ 0 ∧ + ∀ (m : ℕ), 0 < m → ∀ w : N, v = m • w → m = 1 + +/-- Rational salient rays have unique primitive generators. -/ +theorem IsToricCone.existsUnique_primitiveGenerator {i : N →+ V} + (hi : IsIntegralLattice i) {sigma : PointedCone ℝ V} (hsigma : IsToricCone i sigma) + (rho : ToricRay sigma) : + ∃! v : N, IsPrimitiveGenerator i rho v := by + sorry + +/-- A regular cone is a toric cone whose primitive ray generators occur in one integral basis. +Carrying the toric-cone hypothesis prevents regularity from holding vacuously for an irrational +or nonsalient cone. -/ +def IsRegularCone (i : N →+ V) (sigma : PointedCone ℝ V) : Prop := + IsToricCone i sigma ∧ + ∃ (basis : Module.Basis (Fin (Module.finrank ℤ N)) ℤ N) + (rayIndex : ToricRay sigma ↪ Fin (Module.finrank ℤ N)), + ∀ rho, IsPrimitiveGenerator i rho (basis (rayIndex rho)) + +/-- A finite fan on the shared Mathlib cone carrier. -/ +structure Fan (i : N →+ V) where + lattice : IsIntegralLattice i + cones : Set (PointedCone ℝ V) + finite_cones : cones.Finite + toric : ∀ {sigma}, sigma ∈ cones → IsToricCone i sigma + faces : ∀ {sigma}, sigma ∈ cones → ∀ rho : sigma.Face, + (rho : PointedCone ℝ V) ∈ cones + inter_face_left : ∀ {sigma}, sigma ∈ cones → ∀ {tau}, tau ∈ cones → + (sigma ⊓ tau).IsFaceOf sigma + inter_face_right : ∀ {sigma}, sigma ∈ cones → ∀ {tau}, tau ∈ cones → + (sigma ⊓ tau).IsFaceOf tau + +/-- A fan is regular when each of its cones is regular. -/ +def Fan.IsRegular {i : N →+ V} (Sigma : Fan i) : Prop := + ∀ sigma, sigma ∈ Sigma.cones → IsRegularCone i sigma + +/-- The support of a finite fan. -/ +def Fan.support {i : N →+ V} (Sigma : Fan i) : Set V := + ⋃ sigma ∈ Sigma.cones, (sigma : Set V) + +/-- Completeness means that the support fills the ambient real vector space. -/ +def Fan.IsComplete {i : N →+ V} (Sigma : Fan i) : Prop := Sigma.support = Set.univ + +variable {N' V' : Type u} [AddCommGroup N'] [Module ℤ N'] [Module.Free ℤ N'] + [Module.Finite ℤ N'] [AddCommGroup V'] [Module ℝ V'] [FiniteDimensional ℝ V'] + +/-- An integral map of lattices carrying each source cone into a target cone. -/ +structure FanHom {i : N →+ V} {i' : N' →+ V'} (Sigma : Fan i) (Delta : Fan i') where + latticeMap : N →+ N' + realMap : V →ₗ[ℝ] V' + map_lattice : ∀ n, realMap (i n) = i' (latticeMap n) + map_cone : ∀ sigma, sigma ∈ Sigma.cones → + ∃ tau, tau ∈ Delta.cones ∧ sigma.map realMap ≤ tau + +/-- The integral dual semigroup of a cone. -/ +noncomputable def dualSemigroup (i : N →+ V) (sigma : PointedCone ℝ V) : + AddSubmonoid (N →+ ℤ) := by + sorry + +/-- Coordinate ring of the affine toric chart of a cone. -/ +abbrev affineCoordinateRing (i : N →+ V) (sigma : PointedCone ℝ V) := + MonoidAlgebra ℂ (Multiplicative (dualSemigroup i sigma)) + +/-- Affine toric scheme supplied by a cone. -/ +noncomputable abbrev affineToricScheme (i : N →+ V) (sigma : PointedCone ℝ V) := + Spec (.of (affineCoordinateRing i sigma)) + +/-- A face inclusion induces the algebraic affine open immersion used for fan gluing. -/ +noncomputable def faceOpenImmersion {i : N →+ V} {sigma tau : PointedCone ℝ V} + (h : tau.IsFaceOf sigma) : affineToricScheme i tau ⟶ affineToricScheme i sigma := by + sorry + +/-- Algebraic realization obtained by gluing the affine cone schemes along face localizations. -/ +noncomputable def algebraicRealization {i : N →+ V} (Sigma : Fan i) : Scheme := by + sorry + +/-- A fan morphism induces the algebraic toric morphism. -/ +noncomputable def algebraicMap {i : N →+ V} {i' : N' →+ V'} + {Sigma : Fan i} {Delta : Fan i'} (f : FanHom Sigma Delta) : + algebraicRealization Sigma ⟶ algebraicRealization Delta := by + sorry + +end AlgebraicSupplier + +/-! ## Affine complex points and an independent topology -/ + +/-- The complex points of an affine semigroup scheme. -/ +abbrev AffineSemigroupComplexPoint (S : Type*) [AddCommMonoid S] := + MonoidAlgebra ℂ (Multiplicative S) →ₐ[ℂ] ℂ + +/-- A finite additive generating family. -/ +structure AddGeneratingFamily (S : Type*) [AddCommMonoid S] (r : ℕ) where + toFun : Fin r → S + spans : AddSubmonoid.closure (Set.range toFun) = ⊤ + +/-- Evaluation on finite semigroup generators gives a monomial embedding into affine space. -/ +noncomputable def monomialEmbedding {S : Type*} [AddCommMonoid S] {r : ℕ} + (g : AddGeneratingFamily S r) : AffineSemigroupComplexPoint S → Fin r → ℂ := + fun x j ↦ x (MonoidAlgebra.single (.ofAdd (g.toFun j)) 1) + +/-- The affine complex-point topology is induced by a finite monomial embedding. -/ +@[instance_reducible] +noncomputable def affinePointTopology {S : Type*} [AddCommMonoid S] {r : ℕ} + (g : AddGeneratingFamily S r) : TopologicalSpace (AffineSemigroupComplexPoint S) := + TopologicalSpace.induced (monomialEmbedding g) inferInstance + +/-- The monomial-embedding topology is independent of the finite generating family. -/ +theorem affinePointTopology_eq {S : Type*} [AddCommMonoid S] {r s : ℕ} + (g : AddGeneratingFamily S r) (h : AddGeneratingFamily S s) : + affinePointTopology g = affinePointTopology h := by + sorry + +/-- Coordinate model for the dual semigroup of a regular cone. -/ +abbrev RegularDualSemigroup (k l : ℕ) := (Fin k →₀ ℕ) × (Fin l →₀ ℤ) + +/-- Regularity identifies the affine functor-of-points carrier with its mixed affine-torus model. -/ +noncomputable def regularAffinePointEquiv {S : Type*} [AddCommMonoid S] {k l : ℕ} + (e : S ≃+ RegularDualSemigroup k l) : + AffineSemigroupComplexPoint S ≃ (Fin k → ℂ) × (Fin l → ℂˣ) := by + sorry + +/-- The regular coordinate map is a homeomorphism for the independently defined topology. -/ +noncomputable def regularAffinePointHomeomorph {S : Type*} [AddCommMonoid S] + {r k l : ℕ} (g : AddGeneratingFamily S r) (e : S ≃+ RegularDualSemigroup k l) : + @Homeomorph (AffineSemigroupComplexPoint S) ((Fin k → ℂ) × (Fin l → ℂˣ)) + (affinePointTopology g) inferInstance := by + sorry + +/-! ## Mixed monomial maps -/ + +/-- Exponent data for a map between regular charts. There is deliberately no block from +noninvertible source coordinates to invertible target coordinates. -/ +structure MixedExponent (k l k' l' : ℕ) where + boundaryBoundary : Matrix (Fin k') (Fin k) ℕ + boundaryTorus : Matrix (Fin k') (Fin l) ℤ + torusTorus : Matrix (Fin l') (Fin l) ℤ + +/-- Ambient coordinate formula for a mixed monomial map. -/ +noncomputable def mixedMonomialMap {k l k' l' : ℕ} (A : MixedExponent k l k' l') : + ((Fin k → ℂ) × (Fin l → ℂ)) → (Fin k' → ℂ) × (Fin l' → ℂ) := + fun z ↦ + (fun a ↦ (∏ b, z.1 b ^ A.boundaryBoundary a b) * + ∏ b, z.2 b ^ A.boundaryTorus a b, + fun a ↦ ∏ b, z.2 b ^ A.torusTorus a b) + +/-- The open locus where all torus coordinates are invertible. -/ +def mixedChartDomain (k l : ℕ) : Set ((Fin k → ℂ) × (Fin l → ℂ)) := + {z | ∀ j, z.2 j ≠ 0} + +/-- Mixed monomial maps preserve the mixed-chart locus. -/ +theorem mixedMonomialMap_mem {k l k' l' : ℕ} (A : MixedExponent k l k' l') + {z : (Fin k → ℂ) × (Fin l → ℂ)} (hz : z ∈ mixedChartDomain k l) : + mixedMonomialMap A z ∈ mixedChartDomain k' l' := by + sorry + +/-- Mixed monomial maps are holomorphic on their natural open domain. -/ +theorem mixedMonomialMap_differentiableOn {k l k' l' : ℕ} + (A : MixedExponent k l k' l') : + DifferentiableOn ℂ (mixedMonomialMap A) (mixedChartDomain k l) := by + sorry + +/-- Composition of typed mixed exponent data. -/ +noncomputable def 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'' := by + sorry + +theorem 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) := by + sorry + +/-! ## Finite-fan analytic realization and comparison -/ + +section AnalyticRealization + +variable {N V : Type u} [AddCommGroup N] [Module ℤ N] [Module.Free ℤ N] [Module.Finite ℤ N] + [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] +variable {i : N →+ V} + +/-- Topological gluing data built from affine complex-point charts and face localizations. -/ +noncomputable def fanGlueData (Sigma : Fan i) : TopCat.GlueData := by + sorry + +/-- The analytic realization uses `TopCat.GlueData.glued`, not a new quotient carrier. -/ +noncomputable abbrev AnalyticRealization (Sigma : Fan i) := (fanGlueData Sigma).glued + +/-- Model vector space determined by the lattice rank. -/ +abbrev ToricModel := Fin (Module.finrank ℤ N) → ℂ + +/-- The compatible regular affine charts install the complex atlas on the glued carrier. -/ +@[instance_reducible] +noncomputable def analyticChartedSpace (Sigma : Fan i) (hSigma : Sigma.IsRegular) : + ChartedSpace (ToricModel (N := N)) (AnalyticRealization Sigma) := by + sorry + +/-- The finite-fan realization is a complex manifold. -/ +theorem analyticRealization_isManifold (Sigma : Fan i) (hSigma : Sigma.IsRegular) : + letI := analyticChartedSpace Sigma hSigma + IsManifold 𝓘(ℂ, ToricModel (N := N)) ∞ (AnalyticRealization Sigma) := by + sorry + +/-- Coordinate-free dense complex torus with character lattice `N →+ ℤ`. -/ +abbrev ComplexTorus := Multiplicative (N →+ ℤ) →* ℂˣ + +/-- The affine torus actions glue to an action on the analytic realization. -/ +noncomputable def torusAction (Sigma : Fan i) : + ComplexTorus (N := N) →* Equiv.Perm (AnalyticRealization Sigma) := by + sorry + +/-- The torus orbit associated to a cone. -/ +noncomputable def orbit (Sigma : Fan i) (sigma : PointedCone ℝ V) + (hsigma : sigma ∈ Sigma.cones) : Set (AnalyticRealization Sigma) := by + sorry + +/-- Face inclusion is the closure order on torus orbits. -/ +theorem orbit_subset_closure_iff (Sigma : Fan i) {sigma tau : PointedCone ℝ V} + (hsigma : sigma ∈ Sigma.cones) (htau : tau ∈ Sigma.cones) : + orbit Sigma tau htau ⊆ closure (orbit Sigma sigma hsigma) ↔ sigma ≤ tau := by + sorry + +/-- Rays of a finite fan. -/ +def FanRay (Sigma : Fan i) := + {sigma : PointedCone ℝ V // sigma ∈ Sigma.cones ∧ + Module.finrank ℝ (Submodule.span ℝ (sigma : Set V)) = 1} + +/-- The invariant boundary component indexed by a ray. -/ +noncomputable def boundaryComponent (Sigma : Fan i) (rho : FanRay Sigma) : + Set (AnalyticRealization Sigma) := by + sorry + +/-- Every boundary component is closed. Its hypersurface property follows from the local normal +form below. -/ +theorem boundaryComponent_isClosed (Sigma : Fan i) (rho : FanRay Sigma) : + IsClosed (boundaryComponent Sigma rho) := by + sorry + +/-- The toric boundary has the holomorphic simple-normal-crossings coordinate-hyperplane normal +form. A complex `PartialDiffeomorph`, rather than a bare `PartialHomeomorph`, makes each component +a complex hypersurface and makes the displayed coordinates holomorphic. -/ +theorem boundary_local_normalForm (Sigma : Fan i) (hSigma : Sigma.IsRegular) + (x : AnalyticRealization Sigma) : + letI := analyticChartedSpace Sigma hSigma + ∃ (s : Set (FanRay Sigma)) (_hs : s.Finite) + (j : s ↪ Fin (Module.finrank ℤ N)) + (e : PartialDiffeomorph 𝓘(ℂ, ToricModel (N := N)) 𝓘(ℂ, ToricModel (N := N)) + (AnalyticRealization Sigma) (ToricModel (N := N)) ∞), + x ∈ e.source ∧ + ∀ y ∈ e.source, ∀ rho, + y ∈ boundaryComponent Sigma rho ↔ + ∃ hrho : rho ∈ s, e y (j ⟨rho, hrho⟩) = 0 := by + sorry + +variable {N' V' : Type u} [AddCommGroup N'] [Module ℤ N'] [Module.Free ℤ N'] + [Module.Finite ℤ N'] [AddCommGroup V'] [Module ℝ V'] [FiniteDimensional ℝ V'] +variable {i' : N' →+ V'} {Sigma : Fan i} {Delta : Fan i'} + +/-- A fan morphism glues to a continuous analytic map. -/ +noncomputable def analyticMap (f : FanHom Sigma Delta) : + AnalyticRealization Sigma → AnalyticRealization Delta := by + sorry + +theorem analyticMap_continuous (f : FanHom Sigma Delta) : Continuous (analyticMap f) := by + sorry + +/-- The glued map is holomorphic for regular source and target fans. -/ +theorem analyticMap_mdifferentiable (f : FanHom Sigma Delta) + (hSigma : Sigma.IsRegular) (hDelta : Delta.IsRegular) : + letI := analyticChartedSpace Sigma hSigma + letI := analyticChartedSpace Delta hDelta + ContMDiff 𝓘(ℂ, ToricModel (N := N)) 𝓘(ℂ, ToricModel (N := N')) ∞ + (analyticMap f) := by + sorry + +/-- The finite-fan support condition for properness. -/ +def FanHom.SupportCondition (f : FanHom Sigma Delta) : Prop := + ∀ tau, tau ∈ Delta.cones → + f.realMap ⁻¹' (tau : Set V') = + ⋃ sigma ∈ Sigma.cones, ⋃ (_h : sigma.map f.realMap ≤ tau), (sigma : Set V) + +/-- Properness is characterized by the cone-by-cone support condition for finite fans. -/ +theorem analyticMap_isProper_iff (f : FanHom Sigma Delta) : + IsProperMap (analyticMap f) ↔ f.SupportCondition := by + sorry + +/-- A finite regular fan has compact realization exactly when it is complete. -/ +theorem isCompact_univ_iff_isComplete (hSigma : Sigma.IsRegular) : + IsCompact (Set.univ : Set (AnalyticRealization Sigma)) ↔ Sigma.IsComplete := by + sorry + +/-- Global algebraic complex points mean morphisms from `Spec ℂ`, not prime ideals. -/ +abbrev AlgebraicComplexPoint (Sigma : Fan i) := Spec (.of ℂ) ⟶ algebraicRealization Sigma + +/-- The topology on global algebraic complex points is glued from the independently topologized +affine functor-of-points charts. -/ +@[instance_reducible] +noncomputable def algebraicComplexPointTopology (Sigma : Fan i) : + TopologicalSpace (AlgebraicComplexPoint Sigma) := by + sorry + +/-- The affine algebraic complex-point charts glue to their own named complex atlas. -/ +@[instance_reducible] +noncomputable def algebraicComplexPointChartedSpace (Sigma : Fan i) + (hSigma : Sigma.IsRegular) : + letI := algebraicComplexPointTopology Sigma + ChartedSpace (ToricModel (N := N)) (AlgebraicComplexPoint Sigma) := by + sorry + +/-- The affine comparisons glue to the global algebraic--analytic comparison. -/ +noncomputable def algebraicAnalyticHomeomorph (Sigma : Fan i) (hSigma : Sigma.IsRegular) : + @Homeomorph (AlgebraicComplexPoint Sigma) (AnalyticRealization Sigma) + (algebraicComplexPointTopology Sigma) inferInstance := by + sorry + +/-- The global comparison and its inverse are holomorphic. -/ +theorem algebraicAnalyticHomeomorph_mdifferentiable (Sigma : Fan i) + (hSigma : Sigma.IsRegular) : + letI := algebraicComplexPointTopology Sigma + letI := algebraicComplexPointChartedSpace Sigma hSigma + letI := analyticChartedSpace Sigma hSigma + ContMDiff 𝓘(ℂ, ToricModel (N := N)) 𝓘(ℂ, ToricModel (N := N)) ∞ + (algebraicAnalyticHomeomorph Sigma hSigma) ∧ + ContMDiff 𝓘(ℂ, ToricModel (N := N)) 𝓘(ℂ, ToricModel (N := N)) ∞ + (algebraicAnalyticHomeomorph Sigma hSigma).symm := by + sorry + +/-- The comparison is natural for fan morphisms. -/ +theorem algebraicAnalyticHomeomorph_naturality (f : FanHom Sigma Delta) + (hSigma : Sigma.IsRegular) (hDelta : Delta.IsRegular) + (x : AlgebraicComplexPoint Sigma) : + algebraicAnalyticHomeomorph Delta hDelta (x ≫ algebraicMap f) = + analyticMap f (algebraicAnalyticHomeomorph Sigma hSigma x) := by + sorry + +end AnalyticRealization + +end TauCetiRoadmap.AnalyticToricGeometry