Holomorphic function germs at the origin

This file defines the local analytic ring as the subring of Mathlib's neighbourhood-function germs which have an analytic representative. It uses the same Filter.Germ model and AnalyticAt predicate as the pinned WPT project.

@[reducible, inline]

abbrev LocalComplexGeometry.ComplexEuclidean (n : ℕ) : Type

The complex vector space ℂⁿ.

Equations

• LocalComplexGeometry.ComplexEuclidean n = (Fin n → ℂ)

@[reducible, inline]

abbrev LocalComplexGeometry.FunctionGerm (n : ℕ) : Type

The ambient ring of all function germs at the origin of ℂⁿ.

Equations

• LocalComplexGeometry.FunctionGerm n = (nhds 0).Germ ℂ

def LocalComplexGeometry.holomorphicGermSubring (n : ℕ) : Subring (FunctionGerm n)

Function germs which have a representative analytic at the origin.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LocalComplexGeometry.HolomorphicGerm (n : ℕ) : Subring (FunctionGerm n)

The commutative ring 𝒪_{ℂⁿ,0} of holomorphic germs at the origin.

Equations

• LocalComplexGeometry.HolomorphicGerm n = LocalComplexGeometry.holomorphicGermSubring n

noncomputable def LocalComplexGeometry.HolomorphicGerm.ofFunction {n : ℕ} (f : ComplexEuclidean n → ℂ) (hf : AnalyticAt ℂ f 0) : ↥(HolomorphicGerm n)

Pass from an analytic representative to its holomorphic germ.

Equations

• LocalComplexGeometry.HolomorphicGerm.ofFunction f hf = ⟨↑f, ⋯⟩

@[simp]

theorem LocalComplexGeometry.HolomorphicGerm.coe_ofFunction {n : ℕ} (f : ComplexEuclidean n → ℂ) (hf : AnalyticAt ℂ f 0) : ↑(ofFunction f hf) = ↑f

theorem LocalComplexGeometry.HolomorphicGerm.exists_rep {n : ℕ} (φ : ↥(HolomorphicGerm n)) : ∃ (f : ComplexEuclidean n → ℂ), AnalyticAt ℂ f 0 ∧ ↑f = ↑φ

Every holomorphic germ has an analytic representative.

noncomputable def LocalComplexGeometry.evalAtOriginHom (n : ℕ) : ↥(HolomorphicGerm n) →+* ℂ

Evaluation at the origin, as a ring homomorphism.

Equations

• LocalComplexGeometry.evalAtOriginHom n = Filter.Germ.valueRingHom.comp (LocalComplexGeometry.holomorphicGermSubring n).subtype

@[reducible, inline]

noncomputable abbrev LocalComplexGeometry.evalAtOrigin {n : ℕ} (φ : ↥(HolomorphicGerm n)) : ℂ

Evaluation of a holomorphic germ at the origin.

Equations

• LocalComplexGeometry.evalAtOrigin φ = (LocalComplexGeometry.evalAtOriginHom n) φ

@[simp]

theorem LocalComplexGeometry.evalAtOrigin_ofFunction {n : ℕ} (f : ComplexEuclidean n → ℂ) (hf : AnalyticAt ℂ f 0) : evalAtOrigin (HolomorphicGerm.ofFunction f hf) = f 0

instance LocalComplexGeometry.holomorphicGerm_nontrivial (n : ℕ) : Nontrivial ↥(HolomorphicGerm n)

theorem LocalComplexGeometry.holomorphicGerm_isUnit_iff {n : ℕ} (φ : ↥(HolomorphicGerm n)) : IsUnit φ ↔ evalAtOrigin φ ≠ 0

A holomorphic germ is a unit exactly when its value at the origin is nonzero.

theorem LocalComplexGeometry.holomorphicGerm_isLocalRing (n : ℕ) : IsLocalRing ↥(HolomorphicGerm n)

The holomorphic germ ring is local.

instance LocalComplexGeometry.holomorphicGerm_instIsLocalRing (n : ℕ) : IsLocalRing ↥(HolomorphicGerm n)

theorem LocalComplexGeometry.holomorphicGerm_maximalIdeal (n : ℕ) : IsLocalRing.maximalIdeal ↥(HolomorphicGerm n) = Ideal.comap (evalAtOriginHom n) ⊥

The maximal ideal consists exactly of germs vanishing at the origin.