Documentation

LeanPool.LocalComplexGeometry.FiniteProjection.Main

Finite projection for analytic hypersurface germs #

This module exposes the frozen algebraic predicate and combines the prepared quotient power basis with the genuine local proper finite-projection theorem.

source
noncomputable def LocalComplexGeometry.baseInclusion (n : ℕ) :
↥(HolomorphicGerm n) →+* ↥(HolomorphicGerm (n + 1))

Include a lower-dimensional germ as a germ independent of the last coordinate.

Equations
Instances For
    source
    noncomputable def LocalComplexGeometry.hypersurfaceIdeal {n : ℕ} (f : ↥(HolomorphicGerm (n + 1))) :
    Ideal ↥(HolomorphicGerm (n + 1))

    The principal ideal of a hypersurface germ.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev LocalComplexGeometry.HypersurfaceQuotient {n : ℕ} (f : ↥(HolomorphicGerm (n + 1))) :
      Type

      The local ring of the hypersurface germ.

      Equations
      Instances For
        source
        noncomputable def LocalComplexGeometry.hypersurfaceBaseRingHom {n : ℕ} (f : ↥(HolomorphicGerm (n + 1))) :
        ↥(HolomorphicGerm n) →+* HypersurfaceQuotient f

        The base-ring map on a hypersurface quotient.

        Equations
        Instances For
          source
          def LocalComplexGeometry.IsFiniteFreeOfRankOverBase {n : ℕ} (f : ↥(HolomorphicGerm (n + 1))) (d : ℕ) :
          Prop

          A noncircular finite-free rank-d predicate with the explicit power basis 1,w,...,w^(d-1).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem LocalComplexGeometry.hypersurfaceIdeal_eq_of_associated {n : ℕ} {f g : ↥(HolomorphicGerm (n + 1))} (hfg : Associated f g) :
            hypersurfaceIdeal f = hypersurfaceIdeal g

            Associated hypersurface equations have the same principal ideal.

            source
            theorem LocalComplexGeometry.isFiniteFreeOfRankOverBase_of_associated_prepared {n d : ℕ} (g : ↥(HolomorphicGerm (n + 1))) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hassoc : Associated g (WPTBridge.preparedPolynomialGerm a ha)) :
            IsFiniteFreeOfRankOverBase g d

            The prepared power basis transfers across multiplication by a unit.

            source
            theorem LocalComplexGeometry.hypersurface_finiteProjection_core {n : ℕ} {f : ↥(HolomorphicGerm (n + 1))} (hf_ne : f ≠ 0) (hf_zero : (evalAtOriginHom (n + 1)) f = 0) :
            ∃ (L : ComplexEuclidean (n + 1) ≃L[ℂ] ComplexEuclidean (n + 1)) (d : ℕ), 0 < d ∧ IsFiniteFreeOfRankOverBase ((coordinatePullback L) f) d ∧ ∃ (F : ComplexEuclidean (n + 1) → ℂ), AnalyticAt ℂ F 0 ∧ ↑F = ↑((coordinatePullback L) f) ∧ HasGeometricFiniteProjection F d

            Finite projection for a nontrivial analytic hypersurface germ.

            After an invertible complex-linear coordinate change, the hypersurface local ring is finite free over the lower-dimensional base with power basis 1,w,...,w^(d-1). The same coordinate change admits an analytic representative whose local zero locus projects properly and surjectively, with finite fibers of cardinality at most d and explicit vertical-boundary control.