The sheaf of C^n functions on a manifold: sections and evaluation #
For a manifold M modelled on (EM, HM) over a nontrivially normed field 𝕜, a manifold N
modelled on (E, H) and any smoothness n : ℕ∞ω, the sections of the sheaf of C^n functions
contMDiffSheaf IM I n M N over U are, definitionally, the bundled maps C^n⟮IM, U; I, N⟯
(contMDiffSheaf.obj_eq), and likewise for the sheaf of commutative rings
contMDiffSheafCommRing IM I n M R of C^n functions valued in a C^n commutative ring R, on
which restriction is restriction of functions (contMDiffSheafCommRing.map_apply).
The evaluation at a point, contMDiffSheafCommRing.eval IM I n M R x : stalk x →+* R, takes the
germ of a section to its value at x (eval_germ) and is surjective, every value being taken by a
constant section (eval_surjective); in particular the stalks are nontrivial when R is.
This is the sheaf of regular functions of Bierstone–Milman's regular coordinate charts
[BM97, (0.3)]: the coordinates of a chart are sections and the stalks are the local rings of germs
(contMDiffSheafCommRing.instLocalRing_stalk).
theorem
Manifold.contMDiffSheaf.obj_eq
{𝕜 : 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)ᵒᵖ)
:
The sections of contMDiffSheaf IM I n M N over U are, definitionally, the C^n functions
C^n⟮IM, U; I, N⟯.
theorem
Manifold.contMDiffSheaf.contMDiff_section
{𝕜 : 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)ᵒᵖ}
(f : (contMDiffSheaf IM I n M N).presheaf.obj U)
:
ContMDiff IM I n ↑f
theorem
Manifold.contMDiffSheafCommRing.obj_eq
{𝕜 : 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)ᵒᵖ)
:
The sections of contMDiffSheafCommRing IM I n M R over U are, definitionally, the C^n
functions C^n⟮IM, U; I, R⟯.
theorem
Manifold.contMDiffSheafCommRing.contMDiff_section
{𝕜 : 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)ᵒᵖ}
(f : ↑((contMDiffSheafCommRing IM I n M R).presheaf.obj U))
:
ContMDiff IM I n ↑f
@[simp]
theorem
Manifold.contMDiffSheafCommRing.map_apply
{𝕜 : 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 V : TopologicalSpace.Opens ↑↧M}
(h : U ≤ V)
(f : ↑((contMDiffSheafCommRing IM I n M R).presheaf.obj (Opposite.op V)))
(x : ↥U)
:
↑((CategoryTheory.ConcreteCategory.hom ((contMDiffSheafCommRing IM I n M R).presheaf.map (CategoryTheory.homOfLE h).op))
f)
x = ↑f (Set.inclusion h x)
Restriction is restriction of functions.
noncomputable def
Manifold.contMDiffSheafCommRing.evalAt
{𝕜 : 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]
(x : ↑↧M)
(U : TopologicalSpace.OpenNhds x)
:
Evaluation at x on the sections over an open neighbourhood U of x, valued in the lift of
R to the universe of M (so that it is a morphism of CommRingCat.{u}).
Equations
- Manifold.contMDiffSheafCommRing.evalAt IM I n M R x U = CommRingCat.ofHom (ULift.ringEquiv.symm.toRingHom.comp (ContMDiffMap.evalRingHom ⟨x, ⋯⟩))
Instances For
noncomputable def
Manifold.contMDiffSheafCommRing.evalHom
{𝕜 : 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]
(x : ↑↧M)
:
The evaluation at x, as a morphism from the stalk of C^n functions at x to the lift of
R in the category of commutative rings.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Manifold.contMDiffSheafCommRing.eval
{𝕜 : 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]
(x : M)
:
The evaluation ev_x : 𝒪_x →+* R at x on the stalk of C^n functions.
Equations
- Manifold.contMDiffSheafCommRing.eval IM I n M R x = ULift.ringEquiv.toRingHom.comp (CommRingCat.Hom.hom (Manifold.contMDiffSheafCommRing.evalHom IM I n M R x))
Instances For
@[simp]
theorem
Manifold.contMDiffSheafCommRing.ι_evalHom
{𝕜 : 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]
(x : ↑↧M)
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (contMDiffSheafCommRing IM I n M R).presheaf) U)
(evalHom IM I n M R x) = evalAt IM I n M R x (Opposite.unop U)
theorem
Manifold.contMDiffSheafCommRing.ι_evalHom_assoc
{𝕜 : 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]
(x : ↑↧M)
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
{Z : CommRingCat}
(h : ↧(ULift.{u, 0} R) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (contMDiffSheafCommRing IM I n M R).presheaf) U)
(evalHom IM I n M R x))
h = CategoryTheory.CategoryStruct.comp (evalAt IM I n M R x (Opposite.unop U)) h
theorem
Manifold.contMDiffSheafCommRing.ι_evalHom_apply
{𝕜 : 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]
(x : ↑↧M)
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
(x✝ : ↑(((TopologicalSpace.OpenNhds.inclusion x).op.comp (contMDiffSheafCommRing IM I n M R).presheaf).obj U))
:
(CategoryTheory.ConcreteCategory.hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (contMDiffSheafCommRing IM I n M R).presheaf) U)
(evalHom IM I n M R x)))
x✝ = (CategoryTheory.ConcreteCategory.hom (evalAt IM I n M R x (Opposite.unop U))) x✝
theorem
Manifold.contMDiffSheafCommRing.evalHom_germ
{𝕜 : 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)
(x : M)
(hx : x ∈ U)
(f : ↑((contMDiffSheafCommRing IM I n M R).presheaf.obj (Opposite.op U)))
:
(CategoryTheory.ConcreteCategory.hom (evalHom IM I n M R x))
((CategoryTheory.ConcreteCategory.hom ((contMDiffSheafCommRing IM I n M R).presheaf.germ U x hx)) f) = { down := ↑f ⟨x, hx⟩ }
@[simp]
theorem
Manifold.contMDiffSheafCommRing.eval_germ
{𝕜 : 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)
(x : M)
(hx : x ∈ U)
(f : ↑((contMDiffSheafCommRing IM I n M R).presheaf.obj (Opposite.op U)))
:
(eval IM I n M R x)
((CategoryTheory.ConcreteCategory.hom ((contMDiffSheafCommRing IM I n M R).presheaf.germ U x hx)) f) = ↑f ⟨x, hx⟩
The evaluation at x of the germ of a section is the value of the section at x.
theorem
Manifold.contMDiffSheafCommRing.eval_surjective
{𝕜 : 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]
(x : M)
:
Function.Surjective ⇑(eval IM I n M R x)
The evaluation at x is surjective: every value is taken by a constant section.
instance
Manifold.instNontrivialCarrierStalkCommRingCatPresheafContMDiffSheafCommRing
{𝕜 : 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]
[Nontrivial R]
(x : M)
:
Nontrivial ↑((contMDiffSheafCommRing IM I n M R).presheaf.stalk x)