Chart transport of germs

For a chart φ of the maximal atlas of an analytic manifold M over a complete field 𝕜, with a in its source, the stalk 𝒪_{M,a} of the structure sheaf is isomorphic to the ring 𝒪_{E,φ(a)} = analyticGermsAt 𝕜 E (φ a) of germs at φ(a) of functions analytic at φ(a), by f ↦ f ∘ φ⁻¹ (chartTransport, satisfying the specification IsChartTransport of Hironaka/Manifold/StructureSheaf.lean); the isomorphism respects the maximal ideals. This is the identification, in a regular coordinate chart, of the local ring of an analytic manifold with the ring of analytic function germs [BM97, §3, "Regular coordinate charts"].

The construction: the stalk embeds into the germs at a (stalkToGerm), composition with φ⁻¹ is a ring homomorphism of germs (germCompChart), and the composite stalkToChartGerm is injective with range the analytic germs (range_stalkToChartGerm): a C^ω germ on M composed with φ⁻¹ is analytic (ContMDiffAt in the chart at a), and an analytic germ g at φ(a) is C^ω near φ(a) (the field is complete), so g ∘ φ is a C^ω section on φ⁻¹(V) ∩ φ.source for a neighbourhood V on which g is analytic. The transport is the first step of the Taylor homomorphism (Hironaka/Manifold/Germ/TaylorHom.lean) and is used wherever a statement about the stalk is read in a chart.

theorem Manifold.germCompRingHom_coe {𝕜 : Type} [NontriviallyNormedField 𝕜] {α : Type u_2} {β : Type u_3} {l : Filter α} {l' : Filter β} (g : α → β) (hg : Filter.Tendsto g l l') (f : β → 𝕜) : (germCompRingHom g hg) ↑f = ↑(f ∘ g)

@[reducible, inline]

abbrev Manifold.germCompChart {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] {M : Type u} [TopologicalSpace M] (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) : (nhds a).Germ 𝕜 →+* (nhds (↑φ a)).Germ 𝕜

Composition with the inverse chart φ⁻¹ of a chart φ at a, as a ring homomorphism of germs Filter.Germ (𝓝 a) 𝕜 →+* Filter.Germ (𝓝 (φ a)) 𝕜.

Equations

• Manifold.germCompChart E φ ha = Manifold.germCompRingHom ↑φ.symm ⋯

theorem Manifold.germCompChart_coe {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] {M : Type u} [TopologicalSpace M] (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (f : M → 𝕜) : (germCompChart E φ ha) ↑f = ↑(f ∘ ↑φ.symm)

theorem Manifold.germCompChart_injective {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] {M : Type u} [TopologicalSpace M] (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) : Function.Injective ⇑(germCompChart E φ ha)

Composition with the inverse chart is injective on germs at a: compose back with φ.

noncomputable def Manifold.stalkToChartGerm {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →+* (nhds (↑φ a)).Germ 𝕜

The stalk 𝒪_{M,a} mapped to the germs at φ(a), f ↦ f ∘ φ⁻¹.

Equations

• Manifold.stalkToChartGerm E φ ha = (Manifold.germCompChart E φ ha).comp (Manifold.stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M a)

theorem Manifold.stalkToGerm_structureSheaf_germ {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {a : M} (U : TopologicalSpace.Opens M) (hU : a ∈ U) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) : (stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M a) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U a hU)) f) = ↑(extendSection 𝕜 E f)

theorem Manifold.stalkToChartGerm_germ {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (U : TopologicalSpace.Opens M) (hU : a ∈ U) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) : (stalkToChartGerm E φ ha) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U a hU)) f) = ↑(extendSection 𝕜 E f ∘ ↑φ.symm)

theorem Manifold.stalkToChartGerm_injective {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) : Function.Injective ⇑(stalkToChartGerm E φ ha)

theorem Manifold.contMDiffAt_chart_symm {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (↑φ.symm) (↑φ a)

A chart φ⁻¹ of the maximal atlas is an analytic map near φ(a).

theorem Manifold.range_stalkToChartGerm {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) [CompleteSpace 𝕜] : Set.range ⇑(stalkToChartGerm E φ ha) = ↑(analyticGermsAt 𝕜 E (↑φ a))

The range of f ↦ f ∘ φ⁻¹ on the stalk is exactly the ring of analytic germs at φ(a).

noncomputable def Manifold.chartTransport {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) [CompleteSpace 𝕜] : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ≃+* ↥(analyticGermsAt 𝕜 E (↑φ a))

The chart transport of germs: the ring isomorphism 𝒪_{M,a} ≃+* 𝒪_{E, φ(a)}, f ↦ f ∘ φ⁻¹, for a chart φ of the maximal atlas containing a [BM97, §3, "Regular coordinate charts"].

Equations

• Manifold.chartTransport E φ ha hφ = RingEquiv.ofBijective ((Manifold.stalkToChartGerm E φ ha).codRestrict (Manifold.analyticGermsAt 𝕜 E (↑φ a)) ⋯) ⋯

theorem Manifold.chartTransport_apply_coe {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) [CompleteSpace 𝕜] (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : ↑((chartTransport E φ ha hφ) s) = (stalkToChartGerm E φ ha) s

theorem Manifold.isChartTransport_chartTransport {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) [CompleteSpace 𝕜] : IsChartTransport 𝕜 E φ a (chartTransport E φ ha hφ)

chartTransport satisfies the specification IsChartTransport.

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

The chart transport is determined by its specification.

theorem Manifold.IsChartTransport.mem_nonunits_iff' {𝕜 : Type} [NontriviallyNormedField 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) {e : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ≃+* ↥(analyticGermsAt 𝕜 E (↑φ a))} (he : IsChartTransport 𝕜 E φ a e) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : s ∈ nonunits ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ↔ (↑(e s)).value = 0

The chart transport respects 𝔪_a: a germ is a non-unit iff its transport vanishes at φ(a).