smoothSheaf.obj_eq
theorem smoothSheaf.obj_eq :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
[inst_2 : NormedSpace ๐ EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners ๐ EM HM)
{E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace ๐ E] {H : Type u_5}
[inst_6 : TopologicalSpace H] (I : ModelWithCorners ๐ E H) {M : Type u} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace HM M] (N : Type u) [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H N]
(U : (TopologicalSpace.Opens โ(TopCat.of M))แตแต),
(smoothSheaf IM I M N).presheaf.obj U = ContMDiffMap IM I (โฅU.unop) N โค
The theorem `smoothSheaf.obj_eq` states that for any non-trivial normed field `๐`, normed additive commutative group `EM` and `E` with their corresponding normed spaces, topological spaces `HM`, `H`, `M`, and `N` with `M` and `N` being a charted space, a model with corners (`IM` and `I`), and an open set `U` in `M`, the object of the smooth sheaf `smoothSheaf IM I M N` for the open set `U` in `M` is equal to the set of all `C^โโฎIM, (unop U : Opens M); I, Nโฏ`, the `(IM, I)`-smooth functions from `U` to `N`. This is not just a moral equality, but a literal and definitional equality.
More concisely: The smooth sheaf of `C^โ` functions from an open set in a manifold to a normed vector space is equal to the set of `(IM, I)`-smooth functions for a given model with corners and chart.
|
smoothSheaf.eval_surjective
theorem smoothSheaf.eval_surjective :
โ {๐ : Type u_1} [inst : NontriviallyNormedField ๐] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
[inst_2 : NormedSpace ๐ EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners ๐ EM HM)
{E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace ๐ E] {H : Type u_5}
[inst_6 : TopologicalSpace H] (I : ModelWithCorners ๐ E H) {M : Type u} [inst_7 : TopologicalSpace M]
[inst_8 : ChartedSpace HM M] (N : Type u) [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H N] (x : M),
Function.Surjective (smoothSheaf.eval IM I N x)
This theorem states that for any non-trivially normed field ๐, any normed additive commutative group EM, any normed space ๐ over EM, any topological space HM, any model with corners IM for ๐, EM, and HM, any normed additive commutative group E, any normed space ๐ over E, any topological space H, any model with corners I for ๐, E, and H, any topological space M, any charted space M over HM, any type N, any topological space N, any charted space N over H, and any element x of M, the evaluation function of the smooth sheaf at x is surjective. This means that for every element in the target type of the evaluation function, there is an element in its domain such that the evaluation function applied to this element of the domain produces the given element of the target type.
More concisely: For any charted spaces M over HM, N over H, and any element x in M, the evaluation function from the smooth sheaf over HM to the smooth sheaf over H at x is surjective.
|