Documentation

LeanPool.LocalComplexGeometry.Nullstellensatz.IdealRepresentatives

Representatives of a finite ideal generating family #

Noetherianity supplies a chosen finite generating set for every ideal. This file chooses analytic representatives of those generators and records the exact pointwise predicate representing the ideal's local zero-set germ.

source
@[reducible, inline]
noncomputable abbrev LocalComplexGeometry.IdealGeneratorIndex {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) :
Finset ↥(HolomorphicGerm n)

The finite type indexing the chosen generators of an ideal.

Equations
Instances For
    source
    noncomputable def LocalComplexGeometry.idealGeneratorRepresentatives {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) :
    ↥(IdealGeneratorIndex I) → ComplexEuclidean n → ℂ

    Chosen analytic representatives of the chosen generators of an ideal.

    Equations
    Instances For
      source
      theorem LocalComplexGeometry.analyticAt_idealGeneratorRepresentatives {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) (f : ↥(IdealGeneratorIndex I)) :
      AnalyticAt ℂ (idealGeneratorRepresentatives I f) 0
      source
      theorem LocalComplexGeometry.ofFunction_idealGeneratorRepresentatives {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) (f : ↥(IdealGeneratorIndex I)) :
      HolomorphicGerm.ofFunction (idealGeneratorRepresentatives I f) ⋯ = ↑f
      source
      theorem LocalComplexGeometry.idealGenerator_mem {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) (f : ↥(IdealGeneratorIndex I)) :
      ↑f ∈ I

      Every member of the chosen generating finset belongs to the ideal it generates.

      source
      def LocalComplexGeometry.idealGeneratorZeroPredicate {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) (z : ComplexEuclidean n) :
      Prop

      Pointwise representative of the ideal zero-set germ furnished by the chosen finite generating family.

      Equations
      Instances For
        source
        theorem LocalComplexGeometry.idealZeroSetGerm_eq_generatorZeroPredicate {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) :
        idealZeroSetGerm I = ↑(idealGeneratorZeroPredicate I)

        The canonical finite-generator predicate represents the abstract local zero-set germ of the ideal.

        source
        theorem LocalComplexGeometry.eventually_representative_eq_zero_of_mem_ideal {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) (f : ↥(HolomorphicGerm n)) (hf : f ∈ I) :
        ∀ᶠ (z : ComplexEuclidean n) in nhds 0, idealGeneratorZeroPredicate I z → HolomorphicGerm.representative f z = 0

        A chosen representative of any ideal member vanishes on the pointwise finite-generator predicate, on one neighborhood of the origin.

        source
        theorem LocalComplexGeometry.eventually_representatives_eq_of_quotient_eq {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) (f g : ↥(HolomorphicGerm n)) (hfg : (Ideal.Quotient.mk I) f = (Ideal.Quotient.mk I) g) :
        ∀ᶠ (z : ComplexEuclidean n) in nhds 0, idealGeneratorZeroPredicate I z → HolomorphicGerm.representative f z = HolomorphicGerm.representative g z

        Equality modulo an ideal makes chosen representatives equal on that ideal's local zero set, after shrinking once.