Local zero-set germs and vanishing ideals

Zero sets are predicate-valued germs. This avoids evaluating an abstract function germ at points away from the base point. Only finite intersections are used; arbitrary intersections would not have a uniform neighborhood.

@[reducible, inline]

abbrev LocalComplexGeometry.LocalSetGerm (n : ℕ) : Type

Germs at the origin of predicates on ℂⁿ.

Equations

• LocalComplexGeometry.LocalSetGerm n = (nhds 0).Germ Prop

noncomputable def LocalComplexGeometry.germZeroLocus {n : ℕ} (f : ↥(HolomorphicGerm n)) : LocalSetGerm n

The local zero set of a holomorphic function germ.

Equations

• LocalComplexGeometry.germZeroLocus f = Filter.Germ.map (fun (z : ℂ) => z = 0) ↑f

@[simp]

theorem LocalComplexGeometry.germZeroLocus_zero (n : ℕ) : germZeroLocus 0 = ⊤

theorem LocalComplexGeometry.germZeroLocus_inf_le_add {n : ℕ} (f g : ↥(HolomorphicGerm n)) : germZeroLocus f ⊓ germZeroLocus g ≤ germZeroLocus (f + g)

A common zero of f and g is a zero of their sum.

theorem LocalComplexGeometry.germZeroLocus_le_mul {n : ℕ} (a f : ↥(HolomorphicGerm n)) : germZeroLocus f ≤ germZeroLocus (a * f)

Every zero of f is a zero of a left multiple of f.

theorem LocalComplexGeometry.germZeroLocus_pow {n : ℕ} (f : ↥(HolomorphicGerm n)) {k : ℕ} (hk : 0 < k) : germZeroLocus (f ^ k) = germZeroLocus f

A positive power has exactly the same local zero-set germ.

theorem LocalComplexGeometry.germZeroLocus_eq_top_iff {n : ℕ} (f : ↥(HolomorphicGerm n)) : germZeroLocus f = ⊤ ↔ f = 0

A holomorphic germ vanishes on a full neighborhood exactly when it is the zero germ.

def LocalComplexGeometry.vanishingIdeal {n : ℕ} (Z : LocalSetGerm n) : Ideal ↥(HolomorphicGerm n)

Holomorphic germs vanishing on a fixed local set germ form an ideal.

Equations

• LocalComplexGeometry.vanishingIdeal Z = { carrier := {f : ↥(LocalComplexGeometry.HolomorphicGerm n) | Z ≤ LocalComplexGeometry.germZeroLocus f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem LocalComplexGeometry.mem_vanishingIdeal {n : ℕ} {Z : LocalSetGerm n} {f : ↥(HolomorphicGerm n)} : f ∈ vanishingIdeal Z ↔ Z ≤ germZeroLocus f

@[simp]

theorem LocalComplexGeometry.vanishingIdeal_top (n : ℕ) : vanishingIdeal ⊤ = ⊥

The only holomorphic germ vanishing on a full neighborhood is zero.

noncomputable def LocalComplexGeometry.finiteCommonZeroSet {n : ℕ} (S : Finset ↥(HolomorphicGerm n)) : LocalSetGerm n

Common zero set of a finite family of germs.

Equations

• LocalComplexGeometry.finiteCommonZeroSet S = S.inf LocalComplexGeometry.germZeroLocus

noncomputable def LocalComplexGeometry.indexedCommonZeroSet {n s : ℕ} (f : Fin s → ↥(HolomorphicGerm n)) : LocalSetGerm n

Common zero-set germ of a finite indexed family. Unlike a Finset of germs, this retains the indices used by the comparator-facing certificate.

Equations

• LocalComplexGeometry.indexedCommonZeroSet f = Finset.univ.inf fun (i : Fin s) => LocalComplexGeometry.germZeroLocus (f i)

noncomputable def LocalComplexGeometry.fintypeCommonZeroSet {n : ℕ} {ι : Type u_1} [Fintype ι] (f : ι → ↥(HolomorphicGerm n)) : LocalSetGerm n

Common zero-set germ of a family indexed by an arbitrary finite type.

Equations

• LocalComplexGeometry.fintypeCommonZeroSet f = Finset.univ.inf fun (i : ι) => LocalComplexGeometry.germZeroLocus (f i)

theorem LocalComplexGeometry.indexedCommonZeroSet_ofFunction {n s : ℕ} (f : Fin s → ComplexEuclidean n → ℂ) (hf : ∀ (i : Fin s), AnalyticAt ℂ (f i) 0) : (indexedCommonZeroSet fun (i : Fin s) => HolomorphicGerm.ofFunction (f i) ⋯) = ↑fun (x : ComplexEuclidean n) => ∀ (i : Fin s), f i x = 0

The indexed set-germ definition has the expected eventual pointwise meaning for a concrete representative family.

theorem LocalComplexGeometry.fintypeCommonZeroSet_ofFunction {n : ℕ} {ι : Type u_1} [Fintype ι] (f : ι → ComplexEuclidean n → ℂ) (hf : ∀ (i : ι), AnalyticAt ℂ (f i) 0) : (fintypeCommonZeroSet fun (i : ι) => HolomorphicGerm.ofFunction (f i) ⋯) = ↑fun (x : ComplexEuclidean n) => ∀ (i : ι), f i x = 0

The finite-type common zero set has its expected pointwise meaning for concrete analytic representatives.

theorem LocalComplexGeometry.fintypeCommonZeroSet_le_iff_eventually {n : ℕ} {ι : Type u_1} [Fintype ι] (f : ι → ComplexEuclidean n → ℂ) (hf : ∀ (i : ι), AnalyticAt ℂ (f i) 0) (g : ComplexEuclidean n → ℂ) (hg : AnalyticAt ℂ g 0) : (fintypeCommonZeroSet fun (i : ι) => HolomorphicGerm.ofFunction (f i) ⋯) ≤ germZeroLocus (HolomorphicGerm.ofFunction g hg) ↔ ∀ᶠ (x : ComplexEuclidean n) in nhds 0, (∀ (i : ι), f i x = 0) → g x = 0

Translate a finite-type representative common-zero hypothesis into the order relation on local set germs.

theorem LocalComplexGeometry.finiteCommonZeroSet_eq_fintypeCommonZeroSet_subtype {n : ℕ} (S : Finset ↥(HolomorphicGerm n)) : finiteCommonZeroSet S = fintypeCommonZeroSet fun (f : ↥S) => ↑f

A finite set and the family indexed by its subtype define the same common zero-set germ.

theorem LocalComplexGeometry.indexedCommonZeroSet_le_iff_eventually {n s : ℕ} (f : Fin s → ComplexEuclidean n → ℂ) (hf : ∀ (i : Fin s), AnalyticAt ℂ (f i) 0) (g : ComplexEuclidean n → ℂ) (hg : AnalyticAt ℂ g 0) : (indexedCommonZeroSet fun (i : Fin s) => HolomorphicGerm.ofFunction (f i) ⋯) ≤ germZeroLocus (HolomorphicGerm.ofFunction g hg) ↔ ∀ᶠ (x : ComplexEuclidean n) in nhds 0, (∀ (i : Fin s), f i x = 0) → g x = 0

Translate the representative-level eventual common-zero hypothesis into the order relation on local set germs.

theorem LocalComplexGeometry.finiteCommonZeroSet_le_germZeroLocus {n : ℕ} (S : Finset ↥(HolomorphicGerm n)) {f : ↥(HolomorphicGerm n)} (hf : f ∈ S) : finiteCommonZeroSet S ≤ germZeroLocus f

theorem LocalComplexGeometry.finiteCommonZeroSet_le_germZeroLocus_of_mem_span {n : ℕ} (S : Finset ↥(HolomorphicGerm n)) {f : ↥(HolomorphicGerm n)} (hf : f ∈ Ideal.span ↑S) : finiteCommonZeroSet S ≤ germZeroLocus f

Every member of the ideal spanned by S vanishes on the common zero set of S.

theorem LocalComplexGeometry.finiteCommonZeroSet_antitone_span {n : ℕ} (S T : Finset ↥(HolomorphicGerm n)) (h : Ideal.span ↑S ≤ Ideal.span ↑T) : finiteCommonZeroSet T ≤ finiteCommonZeroSet S

Enlarging the generated ideal shrinks the corresponding finite zero set.

theorem LocalComplexGeometry.finiteCommonZeroSet_eq_of_span_eq {n : ℕ} (S T : Finset ↥(HolomorphicGerm n)) (h : Ideal.span ↑S = Ideal.span ↑T) : finiteCommonZeroSet S = finiteCommonZeroSet T

The finite common zero-set germ depends only on the generated ideal.

noncomputable def LocalComplexGeometry.idealGeneratorFinset {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) : Finset ↥(HolomorphicGerm n)

A fixed finite generating set selected from Noetherianity.

Equations

• LocalComplexGeometry.idealGeneratorFinset I = Classical.choose ⋯

theorem LocalComplexGeometry.span_idealGeneratorFinset {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) : Ideal.span ↑(idealGeneratorFinset I) = I

noncomputable def LocalComplexGeometry.idealZeroSetGerm {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) : LocalSetGerm n

The zero-set germ of an ideal, defined through a finite generating set.

Equations

• LocalComplexGeometry.idealZeroSetGerm I = LocalComplexGeometry.finiteCommonZeroSet (LocalComplexGeometry.idealGeneratorFinset I)

theorem LocalComplexGeometry.idealZeroSetGerm_eq_of_span_eq {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) (S : Finset ↥(HolomorphicGerm n)) (hS : Ideal.span ↑S = I) : idealZeroSetGerm I = finiteCommonZeroSet S

Generator independence for the ideal zero-set germ.

@[simp]

theorem LocalComplexGeometry.idealZeroSetGerm_bot {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] : idealZeroSetGerm ⊥ = ⊤

theorem LocalComplexGeometry.idealZeroSetGerm_le_germZeroLocus_of_mem {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] (I : Ideal ↥(HolomorphicGerm n)) {f : ↥(HolomorphicGerm n)} (hf : f ∈ I) : idealZeroSetGerm I ≤ germZeroLocus f

Every member of an ideal vanishes on its local zero-set germ.

theorem LocalComplexGeometry.idealZeroSetGerm_antitone {n : ℕ} [IsNoetherianRing ↥(HolomorphicGerm n)] {I J : Ideal ↥(HolomorphicGerm n)} (hIJ : I ≤ J) : idealZeroSetGerm J ≤ idealZeroSetGerm I

Inclusion of ideals reverses inclusion of their local zero-set germs.