The stalk map of an analytic map on germs of sections

The stalk map germMapOn φ hφ hb hc : 𝒪_{M,c} →+* 𝒪_{N,b} of an analytic map φ (with φ b = c), s ↦ s ∘ φ, is characterized by composition of function germs through the embedding stalkToGerm (stalkToGerm_germMapOn, stalkToGerm_germMap for a global analytic map germMap). This module reads it on sections:

• a function C^ω on an open set W is a section of 𝒪_N over W (sectionOfContMDiffOn), and the stalk map sends the germ of a section f to the germ of the section f ∘ φ (germMapOn_germ); for a global analytic map, f ∘ φ is the section comapSection φ hφ f over the preimage preimageOpens φ hφ U (germMap_germ);
• the stalk map is local, ev_b (s ∘ φ) = ev_{φ b} s (eval_germMapOn, through eval_eq_value), hence a local homomorphism (isLocalHom_germMapOn, isLocalHom_germMap);
• the stalk map of the identity is the identity (germMap_id).

These are the facts behind the pullback of ideal sheaves (IdealSheaf.pullback, whose stalks are generated by the germs of the f ∘ φ).

def Manifold.sectionOfContMDiffOn {𝕜 : Type} [NontriviallyNormedField 𝕜] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (h : N → 𝕜) (W : TopologicalSpace.Opens N) (hW : ContMDiffOn (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 𝕜) ⊤ h ↑W) : ↑((structureSheaf 𝕜 E' N).presheaf.obj (Opposite.op W))

A C^ω function on an open set W, as a section of 𝒪_N over W.

Equations

• Manifold.sectionOfContMDiffOn h W hW = ⟨h ∘ Subtype.val, ⋯⟩

theorem Manifold.sectionOfContMDiffOn_apply {𝕜 : Type} [NontriviallyNormedField 𝕜] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (h : N → 𝕜) (W : TopologicalSpace.Opens N) (hW : ContMDiffOn (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 𝕜) ⊤ h ↑W) (x : ↥W) : ↑(sectionOfContMDiffOn h W hW) x = h ↑x

theorem Manifold.stalkToGerm_germ_sectionOfContMDiffOn {𝕜 : Type} [NontriviallyNormedField 𝕜] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (h : N → 𝕜) (W : TopologicalSpace.Opens N) (hW : ContMDiffOn (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 𝕜) ⊤ h ↑W) {b : N} (hb : b ∈ W) : (stalkToGerm (modelWithCornersSelf 𝕜 E') ⊤ N b) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E' N).presheaf.germ W b hb)) (sectionOfContMDiffOn h W hW)) = ↑h

theorem Manifold.eval_eq_value {𝕜 : Type} [NontriviallyNormedField 𝕜] {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)) : (eval 𝕜 E M a) s = ((stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M a) s).value

The evaluation at a is the value of the germ.

theorem Manifold.stalkToGerm_stalkEquivRange_symm {𝕜 : Type} [NontriviallyNormedField 𝕜] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type v} [TopologicalSpace N] [ChartedSpace E' N] (b : N) (g : ↥(stalkToGerm (modelWithCornersSelf 𝕜 E') ⊤ N b).range) : (stalkToGerm (modelWithCornersSelf 𝕜 E') ⊤ N b) ((stalkEquivRange b).symm g) = ↑g

theorem Manifold.stalkToGerm_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) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk c)) : (stalkToGerm (modelWithCornersSelf 𝕜 E') ⊤ N b) ((germMapOn φ hφ hb hc) s) = ((stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M c) s).compTendsto φ ⋯

The stalk map is characterized by composition of germs.

theorem Manifold.germMapOn_germ {𝕜 : 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) {U : TopologicalSpace.Opens M} (hcU : c ∈ U) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) {W : TopologicalSpace.Opens N} (hbW : b ∈ W) (hW : ContMDiffOn (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 𝕜) ⊤ (extendSection 𝕜 E f ∘ φ) ↑W) : (germMapOn φ hφ hb hc) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U c hcU)) f) = (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E' N).presheaf.germ W b hbW)) (sectionOfContMDiffOn (extendSection 𝕜 E f ∘ φ) W hW)

The stalk map sends the germ of a section f to the germ of f ∘ φ.

theorem Manifold.eval_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) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk c)) : (eval 𝕜 E' N b) ((germMapOn φ hφ hb hc) s) = (eval 𝕜 E M c) s

The stalk map is local: ev_b (s ∘ φ) = ev_{φ b} s.

instance Manifold.isLocalHom_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) : IsLocalHom (germMapOn φ hφ hb hc)

theorem Manifold.stalkToGerm_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) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk (φ b))) : (stalkToGerm (modelWithCornersSelf 𝕜 E') ⊤ N b) ((germMap φ hφ b) s) = ((stalkToGerm (modelWithCornersSelf 𝕜 E) ⊤ M (φ b)) s).compTendsto φ ⋯

instance Manifold.isLocalHom_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) : IsLocalHom (germMap φ hφ b)

def Manifold.preimageOpens {𝕜 : 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) ⊤ φ) (U : TopologicalSpace.Opens M) : TopologicalSpace.Opens N

The preimage of an open set under φ.

Equations

• Manifold.preimageOpens φ hφ U = { carrier := φ ⁻¹' ↑U, is_open' := ⋯ }

theorem Manifold.mem_preimageOpens {𝕜 : 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) ⊤ φ) {U : TopologicalSpace.Opens M} {x : N} : x ∈ preimageOpens φ hφ U ↔ φ x ∈ U

theorem Manifold.contMDiffOn_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))) : ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 𝕜) ⊤ (extendSection 𝕜 E f) ↑U

The extension by zero of a section is C^ω on its domain.

noncomputable def Manifold.comapSection {𝕜 : 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) ⊤ φ) {U : TopologicalSpace.Opens M} (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) : ↑((structureSheaf 𝕜 E' N).presheaf.obj (Opposite.op (preimageOpens φ hφ U)))

f ∘ φ as a section of 𝒪_N over φ⁻¹ U.

Equations

• Manifold.comapSection φ hφ f = Manifold.sectionOfContMDiffOn (Manifold.extendSection 𝕜 E f ∘ φ) (Manifold.preimageOpens φ hφ U) ⋯

theorem Manifold.comapSection_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) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) {U : TopologicalSpace.Opens M} (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) (x : ↥(preimageOpens φ hφ U)) : ↑(comapSection φ hφ f) x = ↑f ⟨φ ↑x, ⋯⟩

theorem Manifold.germMap_germ {𝕜 : 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) ⊤ φ) {U : TopologicalSpace.Opens M} {b : N} (hU : φ b ∈ U) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) : (germMap φ hφ b) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U (φ b) hU)) f) = (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E' N).presheaf.germ (preimageOpens φ hφ U) b ⋯)) (comapSection φ hφ f)

The stalk map sends the germ of f to the germ of f ∘ φ.

theorem Manifold.germMap_id {𝕜 : Type} [NontriviallyNormedField 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (x : M) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk x)) : (germMap id ⋯ x) s = s

The germ map of the identity is the identity of the stalk.