The germ at a point of a section of the sheaf of C^n functions #
The stalk 𝒪_{M,a} of the sheaf of C^n functions valued in 𝕜 embeds into
Filter.Germ (𝓝 a) 𝕜 through the germs at a of the extensions by zero of the sections
(germAt, stalkToGerm). This module records that germAt is the germ of the extension by zero
(germAt_apply) and that the germ at a of a restriction is the germ of the section
(germAt_restrict).
theorem
Manifold.germAt_apply
{𝕜 : 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)))
:
theorem
Manifold.germAt_restrict
{𝕜 : 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.Opens M)
(i : U ⟶ V)
(ha : a ∈ U)
(f : ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.obj (Opposite.op V)))
:
(germAt IM n M a U ha)
((CategoryTheory.ConcreteCategory.hom
((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.map i.op))
f) = (germAt IM n M a V ⋯) f
The germs at a of restrictions are the germs of the sections.