The structure sheaf of an analytic manifold

For a manifold M modelled on a normed space E over a field 𝕜 with analytic (C^ω) chart changes, the structure sheaf 𝒪_M is the sheaf of commutative rings U ↦ {f : U → 𝕜 : f is C^ω}, 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"].

• The sheaf of C^n functions. For a manifold M modelled on (EM, HM), a manifold N modelled on (E, H) and any smoothness n : ℕ∞ω, contMDiffSheaf IM I n M N is the sheaf of types of C^n functions M → N (the local predicate contMDiffLocalPredicate, Mathlib's LocalInvariantProp.localPredicate for contDiffWithinAt_localInvariantProp n), whose sections over U are definitionally the bundled maps C^n⟮IM, U; I, N⟯; for a C^n commutative ring R, contMDiffSheafCommRing IM I n M R is the sheaf of commutative rings of C^n functions M → R. Mathlib's smoothSheaf and smoothSheafCommRing are the case n = ∞ with M and N in one universe; here the target lives in Type and the manifold in Type u, so that the sheaf of rings is an object of CommRingCat.{u} over TopCat.of M and Mathlib's stalk API applies to manifolds whose carrier is in any universe. A section over U valued in 𝕜 extends by zero to a function on M (extendBy0).
• The structure sheaf structureSheaf 𝕜 E M is the case n = ω, R = 𝕜. Its global constants are the ring homomorphism constHom : 𝕜 →+* Γ(M, 𝒪_M); a chart φ of the maximal atlas with coordinates ψ : E ≃L[𝕜] (Fin n → 𝕜) has the coordinate sections ψ_i ∘ φ over its source (chartSection) and their germs x_i ∈ 𝒪_{M,a} (coord).
• The stalk as a ring of germs. The stalk 𝒪_{M,a} of the sheaf of C^n functions valued in 𝕜 embeds into Filter.Germ (𝓝 a) 𝕜: stalkToGerm sends the germ of a section f to the germ of its extension by zero (stalkToGerm_germ); it is injective (stalkToGerm_injective: two sections with the same germ agree on an open neighbourhood of a), and its range is the set of germs of functions C^n on a neighbourhood of a (mem_range_stalkToGerm_iff).
• The stalk map of an analytic map. For φ : N → M analytic on an open V ∋ b with φ b = c, germMapOn φ hφ hb hc : 𝒪_{M,c} →+* 𝒪_{N,b} is s ↦ s ∘ φ: the germ of s is composed with φ (stalkGermComp, through germCompRingHom, Mathlib's Filter.Germ.compTendsto as a ring homomorphism), the composite is again the germ of a section (stalkGermComp_mem_range, by the description of the range of stalkToGerm), and it is lifted back to the stalk along stalkEquivRange. The target point c is a parameter with hc : φ b = c, so that the stalk map of a local inverse at φ b lands in 𝒪_{N,b} without transport; germMap φ hφ b is the case of a global analytic map. It is the stalk map along which ideal sheaves are pulled back (IdealSheaf.pullback).

The sheaf of C^n functions

def Manifold.contMDiffLocalPredicate {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (N : Type) [TopologicalSpace N] [ChartedSpace H N] : TopCat.LocalPredicate fun (x : ↑↧M) => N

The local predicate "f : U → N is C^n" on the open sets of M: Mathlib's LocalInvariantProp.localPredicate for contDiffWithinAt_localInvariantProp n, with the target in Type (Mathlib's version needs M and N in one universe).

Equations

• Manifold.contMDiffLocalPredicate IM I n M N = { pred := fun {U : TopologicalSpace.Opens ↑↧M} (f : ↥U → N) => ChartedSpace.LiftProp (ContDiffWithinAtProp IM I n) f, res := ⋯, locality := ⋯ }

def Manifold.contMDiffSheaf {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (N : Type) [TopologicalSpace N] [ChartedSpace H N] : TopCat.Sheaf (Type u) ↧M

The sheaf of types of C^n functions from M to N.

Equations

• Manifold.contMDiffSheaf IM I n M N = TopCat.subsheafToTypes (Manifold.contMDiffLocalPredicate IM I n M N)

@[instance_reducible]

instance Manifold.contMDiffSheaf.coeFun {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) {M : Type u} [TopologicalSpace M] [ChartedSpace HM M] (N : Type) [TopologicalSpace N] [ChartedSpace H N] (U : (TopologicalSpace.Opens ↑↧M)ᵒᵖ) : CoeFun ((contMDiffSheaf IM I n M N).presheaf.obj U) fun (x : (contMDiffSheaf IM I n M N).presheaf.obj U) => ↥(Opposite.unop U) → N

Equations

• Manifold.contMDiffSheaf.coeFun IM I n N U = { coe := fun (a : (Manifold.contMDiffSheaf IM I n M N).presheaf.obj U) => ↑a }

@[instance_reducible]

noncomputable instance Manifold.instCommRingObjOppositeOpensCarrierOfPresheafContMDiffSheaf {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (R : Type) [CommRing R] [TopologicalSpace R] [ChartedSpace H R] [ContMDiffRing I n R] (U : (TopologicalSpace.Opens ↑↧M)ᵒᵖ) : CommRing ((contMDiffSheaf IM I n M R).presheaf.obj U)

Equations

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

noncomputable def Manifold.contMDiffPresheafCommRing {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (R : Type) [CommRing R] [TopologicalSpace R] [ChartedSpace H R] [ContMDiffRing I n R] : TopCat.Presheaf CommRingCat ↧M

The presheaf of C^n functions from M to a C^n commutative ring R, as a presheaf of commutative rings.

Equations

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

noncomputable def Manifold.contMDiffSheafCommRing {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (R : Type) [CommRing R] [TopologicalSpace R] [ChartedSpace H R] [ContMDiffRing I n R] : TopCat.Sheaf CommRingCat ↧M

The sheaf of C^n functions from M to a C^n commutative ring R, as a sheaf of commutative rings.

Equations

• Manifold.contMDiffSheafCommRing IM I n M R = { obj := Manifold.contMDiffPresheafCommRing IM I n M R, property := ⋯ }

@[instance_reducible]

instance Manifold.contMDiffSheafCommRing.coeFun {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (R : Type) [CommRing R] [TopologicalSpace R] [ChartedSpace H R] [ContMDiffRing I n R] (U : (TopologicalSpace.Opens ↑↧M)ᵒᵖ) : CoeFun ↑((contMDiffSheafCommRing IM I n M R).presheaf.obj U) fun (x : ↑((contMDiffSheafCommRing IM I n M R).presheaf.obj U)) => ↥(Opposite.unop U) → R

Equations

• Manifold.contMDiffSheafCommRing.coeFun IM I n M R U = { coe := fun (a : ↑((Manifold.contMDiffSheafCommRing IM I n M R).presheaf.obj U)) => ↑a }

noncomputable def Manifold.extendBy0 {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] {U : TopologicalSpace.Opens M} (f : ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.obj (Opposite.op U))) : M → 𝕜

The extension by zero of a C^n section over U (valued in 𝕜) to a function on M.

Equations

• Manifold.extendBy0 IM n M f x = if h : x ∈ U then ↑f ⟨x, h⟩ else 0

@[simp]

theorem Manifold.extendBy0_of_mem {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] {U : TopologicalSpace.Opens M} (f : ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.obj (Opposite.op U))) {x : M} (hx : x ∈ U) : extendBy0 IM n M f x = ↑f ⟨x, hx⟩

theorem Manifold.extendBy0_comp_val {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] {U : TopologicalSpace.Opens M} (f : ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.obj (Opposite.op U))) : extendBy0 IM n M f ∘ Subtype.val = ↑f

The structure sheaf

@[implicit_reducible]

noncomputable def Manifold.structureSheaf (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u) [TopologicalSpace M] [ChartedSpace E M] : TopCat.Sheaf CommRingCat ↧M

The structure sheaf 𝒪_M of analytic functions on the manifold M modelled on E over 𝕜: the sheaf of commutative rings U ↦ {f : U → 𝕜 : ContMDiff 𝓘(𝕜, E) 𝓘(𝕜) ω f}, the sheaf of regular functions of an analytic manifold [BM97, (0.3); §3, "Regular coordinate charts"].

Equations

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

@[instance_reducible]

instance Manifold.structureSheaf.coeFun (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u) [TopologicalSpace M] [ChartedSpace E M] (U : (TopologicalSpace.Opens ↑↧M)ᵒᵖ) : CoeFun ↑((structureSheaf 𝕜 E M).presheaf.obj U) fun (x : ↑((structureSheaf 𝕜 E M).presheaf.obj U)) => ↥(Opposite.unop U) → 𝕜

Equations

• Manifold.structureSheaf.coeFun 𝕜 E M U = { coe := fun (a : ↑((Manifold.structureSheaf 𝕜 E M).presheaf.obj U)) => ↑a }

def Manifold.constSection (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u) [TopologicalSpace M] [ChartedSpace E M] (c : 𝕜) : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op ⊤))

The constant section c over M.

Equations

• Manifold.constSection 𝕜 E M c = ⟨fun (x : ↥⊤) => c, ⋯⟩

def Manifold.constHom (𝕜 : Type) [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Type u) [TopologicalSpace M] [ChartedSpace E M] : 𝕜 →+* ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op ⊤))

The constants as the 𝕜-algebra structure of 𝒪_M: the ring homomorphism 𝕜 →+* Γ(M, 𝒪_M), c ↦ the constant section c (the structure used when M is regarded as an analytic space over 𝕜).

Equations

• Manifold.constHom 𝕜 E M = { toFun := Manifold.constSection 𝕜 E M, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def Manifold.chartSection {𝕜 : 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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (i : Fin n) : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op { carrier := φ.source, is_open' := ⋯ }))

A chart φ of the maximal atlas with coordinates ψ: the coordinate function ψ_i ∘ φ as a section of 𝒪_M over the source of φ.

Equations

• Manifold.chartSection E ψ φ hφ i = ⟨fun (x : ↥(Opposite.unop (Opposite.op { carrier := φ.source, is_open' := ⋯ }))) => ψ (↑φ ↑x) i, ⋯⟩

noncomputable def Manifold.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) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (i : Fin n) : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The coordinate germs x_i := ψ_i ∘ φ ∈ 𝒪_{M,a} of a chart φ of the maximal atlas containing a, with coordinates ψ.

Equations

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

The stalk as a ring of germs

noncomputable def Manifold.germAt {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (a : ↑↧M) (U : TopologicalSpace.Opens M) (ha : a ∈ U) : ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.obj (Opposite.op U)) →+* (nhds a).Germ 𝕜

The germ at a of the extension by zero, on the sections over an open neighbourhood U of a, as a ring homomorphism (on U ∈ 𝓝 a the extensions of sums and products are the pointwise sums and products).

Equations

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

theorem Manifold.germAt_naturality {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (a : ↑↧M) (U V : (TopologicalSpace.OpenNhds a)ᵒᵖ) (i : U ⟶ V) (f : ↑(((TopologicalSpace.OpenNhds.inclusion a).op.comp (contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf).obj U)) : (germAt IM n M a ((TopologicalSpace.OpenNhds.inclusion a).obj (Opposite.unop V)) ⋯) ((CategoryTheory.ConcreteCategory.hom (((TopologicalSpace.OpenNhds.inclusion a).op.comp (contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf).map i)) f) = (germAt IM n M a ((TopologicalSpace.OpenNhds.inclusion a).obj (Opposite.unop U)) ⋯) f

Naturality of the germs at a over the open neighbourhoods of a.

noncomputable def Manifold.stalkToGermCocone {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (a : ↑↧M) : CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion a).op.comp (contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf)

The cocone of the germs at a of the extensions by zero over the open neighbourhoods of a.

Equations

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

noncomputable def Manifold.stalkToGermHom {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (a : ↑↧M) : (contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.stalk a ⟶ ↧((nhds a).Germ 𝕜)

The stalk as germs: the ring homomorphism 𝒪_{M,a} →+* Filter.Germ (𝓝 a) 𝕜 sending the germ of a section to the germ of its extension by zero, as a morphism of CommRingCat (the germ ring Filter.Germ (𝓝 a) 𝕜 lives in the universe of M).

Equations

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

noncomputable def Manifold.stalkToGerm {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (a : M) : ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.stalk a) →+* (nhds a).Germ 𝕜

The stalk as germs, stalkToGerm : 𝒪_{M,a} →+* Filter.Germ (𝓝 a) 𝕜.

Equations

• Manifold.stalkToGerm IM n M a = CommRingCat.Hom.hom (Manifold.stalkToGermHom IM n M a)

@[simp]

theorem Manifold.stalkToGerm_germ {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (a : M) (U : TopologicalSpace.Opens M) (ha : a ∈ U) (f : ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.obj (Opposite.op U))) : (stalkToGerm IM n M a) ((CategoryTheory.ConcreteCategory.hom ((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.germ U a ha)) f) = ↑(extendBy0 IM n M f)

theorem Manifold.stalkToGerm_injective {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (a : M) : Function.Injective ⇑(stalkToGerm IM n M a)

Two sections with the same germ at a agree on an open neighbourhood of a, so the stalk embeds into the germs.

theorem Manifold.contMDiffOn_extendBy0 {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] {U : TopologicalSpace.Opens M} (f : ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.obj (Opposite.op U))) : ContMDiffOn IM (modelWithCornersSelf 𝕜 𝕜) n (extendBy0 IM n M f) ↑U

The extension by zero of a C^n section over U is C^n on U.

theorem Manifold.mem_range_stalkToGerm_iff {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (a : M) (g : (nhds a).Germ 𝕜) : g ∈ Set.range ⇑(stalkToGerm IM n M a) ↔ ∃ (h : M → 𝕜), g = ↑h ∧ ∃ (U : TopologicalSpace.Opens M), a ∈ U ∧ ContMDiffOn IM (modelWithCornersSelf 𝕜 𝕜) n h ↑U

The range of stalkToGerm is the set of germs of functions C^n on an open neighbourhood of a.

The stalk map of an analytic map

def Manifold.germCompRingHom {𝕜 : Type} [NontriviallyNormedField 𝕜] {α : Type u_1} {β : Type u_2} {l : Filter α} {l' : Filter β} (g : α → β) (hg : Filter.Tendsto g l l') : l'.Germ 𝕜 →+* l.Germ 𝕜

Composition of germs of 𝕜-valued functions with a map g tending to the base point, as a ring homomorphism Filter.Germ l' 𝕜 →+* Filter.Germ l 𝕜 (Mathlib's Filter.Germ.compTendsto bundled; the stalk maps below, the chart transport and the coordinate change are its instances).

Equations

• Manifold.germCompRingHom g hg = { toFun := fun (f : l'.Germ 𝕜) => f.compTendsto g hg, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem Manifold.tendsto_of_contMDiffOn_of_eq {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) {V : TopologicalSpace.Opens N} (hφ : ContMDiffOn (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ ↑V) {b : N} (hb : b ∈ V) {c : M} (hc : φ b = c) : Filter.Tendsto φ (nhds b) (nhds c)

noncomputable def Manifold.stalkGermComp {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) {V : TopologicalSpace.Opens N} (hφ : ContMDiffOn (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ ↑V) {b : N} (hb : b ∈ V) {c : M} (hc : φ b = c) : ↑((structureSheaf 𝕜 E M).presheaf.stalk c) →+* (nhds b).Germ 𝕜

The germ at c = φ b of a section of 𝒪_M, composed with φ, as a germ at b.

Equations

• Manifold.stalkGermComp φ hφ hb hc = (Manifold.germCompRingHom φ ⋯).comp (Manifold.stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M c)

theorem Manifold.stalkGermComp_apply {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) {V : TopologicalSpace.Opens N} (hφ : ContMDiffOn (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ ↑V) {b : N} (hb : b ∈ V) {c : M} (hc : φ b = c) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk c)) : (stalkGermComp φ hφ hb hc) s = ((stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M c) s).compTendsto φ ⋯

theorem Manifold.stalkGermComp_mem_range {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) {V : TopologicalSpace.Opens N} (hφ : ContMDiffOn (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ ↑V) {b : N} (hb : b ∈ V) {c : M} (hc : φ b = c) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk c)) : (stalkGermComp φ hφ hb hc) s ∈ (stalkToGerm (modelWithCornersSelf 𝕜 E') ⊤ N b).range

noncomputable def Manifold.stalkEquivRange {𝕜 : Type} [NontriviallyNormedField 𝕜] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (b : N) : ↑((structureSheaf 𝕜 E' N).presheaf.stalk b) ≃+* ↥(stalkToGerm (modelWithCornersSelf 𝕜 E') ⊤ N b).range

The stalk as its own image in the germs, a ring isomorphism.

Equations

• Manifold.stalkEquivRange b = RingEquiv.ofBijective (Manifold.stalkToGerm (modelWithCornersSelf 𝕜 E') ⊤ N b).rangeRestrict ⋯

noncomputable def Manifold.germMapOn {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) {V : TopologicalSpace.Opens N} (hφ : ContMDiffOn (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ ↑V) {b : N} (hb : b ∈ V) {c : M} (hc : φ b = c) : ↑((structureSheaf 𝕜 E M).presheaf.stalk c) →+* ↑((structureSheaf 𝕜 E' N).presheaf.stalk b)

The stalk map of an analytic map φ, analytic on the open V ∋ b, with φ b = c: the ring homomorphism 𝒪_{M,c} →+* 𝒪_{N,b}, s ↦ s ∘ φ.

Equations

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

@[reducible, inline]

noncomputable abbrev Manifold.germMap {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) (b : N) : ↑((structureSheaf 𝕜 E M).presheaf.stalk (φ b)) →+* ↑((structureSheaf 𝕜 E' N).presheaf.stalk b)

The stalk map 𝒪_{M, φ b} →+* 𝒪_{N, b} of a global analytic map.

Equations

• Manifold.germMap φ hφ b = Manifold.germMapOn φ ⋯ ⋯ ⋯