The structure sheaf of analytic functions: evaluation, constants, charts

The stalk 𝒪_{M,a} of the structure sheaf structureSheaf 𝕜 E M of an analytic manifold (the n = ω case of contMDiffSheafCommRing, the sheaf of "regular functions" of Bierstone–Milman's regular coordinate charts [BM97, (0.3)], which for an analytic manifold is the sheaf of analytic functions [BM97, §3, "Regular coordinate charts"]) is a local ring with the evaluation eval 𝕜 E M a : 𝒪_{M,a} →+* 𝕜. This module provides, besides eval:

• analyticGermsAt 𝕜 E b, the ring 𝒪_{E,b} of germs at b ∈ E of functions analytic at b, as a subring of (𝓝 b).Germ 𝕜, and the specification IsChartTransport φ a e of the chart transport e : 𝒪_{M,a} ≃+* 𝒪_{E,φ(a)}, f ↦ f ∘ φ⁻¹, in a chart φ at a (any chart of the maximal atlas whose source contains a; the transport is chartTransport);
• the constants const 𝕜 E M a : 𝕜 →+* 𝒪_{M,a}, the germs at a of the constant sections constHom, and the extension by zero extendSection of a section to a function on M;
• for 𝕜 ∈ {ℝ, ℂ} and coordinates ψ : E ≃L[𝕜] (Fin n → 𝕜): the specification IsTaylorHom ψ φ a T of the Taylor homomorphism T_a : 𝒪_{M,a} →+* 𝕜[[X₁, …, Xₙ]] of [BM97, (0.3)] (T_a f is the convergent power series of f ∘ φ⁻¹ ∘ ψ⁻¹ at ψ(φ(a))), the formal partial derivatives pderivGerm on analytic germs (on power series they are Mathlib's MvPowerSeries.pderiv), and the values of the coordinate germs coord ψ φ hφ ha i (the germs x_i = ψ_i ∘ φ ∈ 𝒪_{M,a} of a chart) and of the constants (eval_const, eval_coord), the maximal ideal 𝔪_a = ker (ev_a) (mem_maximalIdeal_iff_eval) and x_i − x_i(a) ∈ 𝔪_a (coord_sub_mem_maximalIdeal).

The field lives in Type and the manifold in Type u: Mathlib's stalk API needs the sheaf of rings in CommRingCat.{u} over TopCat.of M. The Taylor homomorphism, its injectivity and its description of the powers of the maximal ideal are constructed in Hironaka/Manifold/Germ/; the ideal sheaves of 𝒪_M, the objects of the analytic main theorems, are built on this sheaf (Hironaka/Manifold/IdealSheaf/).

noncomputable def Manifold.eval (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u) [TopologicalSpace M] [ChartedSpace E M] (a : M) : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →+* 𝕜

The evaluation ev_a : 𝒪_{M,a} →+* 𝕜 at the point a.

Equations

• Manifold.eval 𝕜 E M a = Manifold.contMDiffSheafCommRing.eval (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 𝕜) ⊤ M 𝕜 a

instance Manifold.structureSheaf.instLocalRing_stalk (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u) [TopologicalSpace M] [ChartedSpace E M] (a : M) : IsLocalRing ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The stalk 𝒪_{M,a} is a local ring (Hironaka/Manifold/Sheaf/LocalRing.lean, as an instance for the structure sheaf).

def Manifold.analyticGermsAt (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (b : E) : Subring ((nhds b).Germ 𝕜)

The ring 𝒪_{E,b} of analytic germs at b ∈ E: the subring of Filter.Germ (𝓝 b) 𝕜 of germs of functions analytic at b.

Equations

• Manifold.analyticGermsAt 𝕜 E b = { carrier := {g : (nhds b).Germ 𝕜 | ∃ (f : E → 𝕜), g = ↑f ∧ AnalyticAt 𝕜 f b}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[reducible, inline]

noncomputable abbrev Manifold.extendSection (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {U : TopologicalSpace.Opens M} (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) : M → 𝕜

The extension by zero of a section of 𝒪_M over U to a function on M (extendBy0 for the structure sheaf).

Equations

• Manifold.extendSection 𝕜 E f = Manifold.extendBy0 (modelWithCornersSelf 𝕜 E) ⊤ M f

@[simp]

theorem Manifold.extendSection_of_mem (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {U : TopologicalSpace.Opens M} (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) {x : M} (hx : x ∈ U) : extendSection 𝕜 E f x = ↑f ⟨x, hx⟩

def Manifold.IsChartTransport (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) (a : M) (e : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ≃+* ↥(analyticGermsAt 𝕜 E (↑φ a))) : Prop

The specification of the chart transport of germs in a chart φ at a: a ring isomorphism e : 𝒪_{M,a} ≃+* 𝒪_{E, φ(a)} is the chart transport when it sends the germ of every section f to the germ at φ(a) of f ∘ φ⁻¹ (f extended by zero off its domain). Any chart of the maximal atlas whose source contains a is admitted; chartAt E a is the special case.

Equations

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

noncomputable def Manifold.const (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u) [TopologicalSpace M] [ChartedSpace E M] (a : M) : 𝕜 →+* ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The constants: the germ at a of the constant section c, as a ring homomorphism 𝕜 →+* 𝒪_{M,a} — the composite of constHom with the germ at a.

Equations

• Manifold.const 𝕜 E M a = (CommRingCat.Hom.hom ((Manifold.structureSheaf 𝕜 E M).presheaf.germ ⊤ a trivial)).comp (Manifold.constHom 𝕜 E M)

theorem Manifold.const_apply (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (a : M) (c : 𝕜) : (const 𝕜 E M a) c = (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ ⊤ a trivial)) (constSection 𝕜 E M c)

def Manifold.IsTaylorHom {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (a : M) (T : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →+* MvPowerSeries (Fin n) 𝕜) : Prop

The specification of the Taylor homomorphism T_a : 𝒪_{M,a} →+* 𝕜[[X₁, …, Xₙ]] in a chart φ at a with coordinates ψ [BM97, (0.3)]: every value is a convergent power series (Analytic.Conv 𝕜 n), and T_a f is the power series of f ∘ φ⁻¹ ∘ ψ⁻¹ at ψ(φ(a)), i.e. that function agrees near ψ(φ(a)) with y ↦ (T_a f)(y - ψ(φ(a))) (Analytic.evalSeries).

Equations

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

noncomputable def Manifold.pderivGerm {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (i : Fin n) (b : E) (g : ↥(analyticGermsAt 𝕜 E b)) : ↥(analyticGermsAt 𝕜 E b)

The partial derivative ∂_i g of an analytic germ g at b ∈ E in the direction of the i-th coordinate vector ψ⁻¹(e_i): the germ of y ↦ Dg(y)(ψ⁻¹ e_i).

Equations

• Manifold.pderivGerm E ψ i b g = ⟨Quotient.liftOn' (↑g) (fun (f : E → 𝕜) => ↑fun (y : E) => (fderiv 𝕜 f y) (ψ.symm (Pi.single i 1))) ⋯, ⋯⟩

Evaluation of the constants and of the coordinate germs

@[simp]

theorem Manifold.eval_const {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {a : M} (c : 𝕜) : (eval 𝕜 E M a) ((const 𝕜 E M a) c) = c

A constant germ evaluates to the constant.

@[simp]

theorem Manifold.eval_coord {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (i : Fin n) : (eval 𝕜 E M a) (coord E ψ φ hφ ha i) = ψ (↑φ a) i

The coordinate germ x_i evaluates to x_i(a).

theorem Manifold.mem_maximalIdeal_iff_eval {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {a : M} (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : s ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ↔ (eval 𝕜 E M a) s = 0

For the structure sheaf: 𝔪_a = ker (ev_a).

theorem Manifold.coord_sub_mem_maximalIdeal {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (i : Fin n) : coord E ψ φ hφ ha i - (const 𝕜 E M a) ((eval 𝕜 E M a) (coord E ψ φ hφ ha i)) ∈ IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

x_i − x_i(a) ∈ 𝔪_a.