The sheaf of smooth functions on a manifold #
The sheaf of 𝕜-smooth functions from a manifold M to a manifold N can be defined as a sheaf of
types using the construction StructureGroupoid.LocalInvariantProp.sheaf from the file
Mathlib.Geometry.Manifold.Sheaf.Basic. In this file we write that down (a one-liner), then do the
work of upgrading this to a sheaf of [groups]/[abelian groups]/[rings]/[commutative rings] when N
carries more algebraic structure. For example, if N is 𝕜 then the sheaf of smooth functions
from M to 𝕜 is a sheaf of commutative rings, the structure sheaf of M.
Main definitions #
smoothSheaf: The sheaf of smooth functions fromMtoN, as a sheaf of typessmoothSheaf.eval: Canonical map ontoNfrom the stalk ofsmoothSheaf IM I M Natx, given by evaluating sections atxsmoothSheafGroup,smoothSheafCommGroup,smoothSheafRing,smoothSheafCommRing: The sheaf of smooth functions into a [Lie group]/[abelian Lie group]/[smooth ring]/[smooth commutative ring], as a sheaf of [groups]/[abelian groups]/[rings]/[commutative rings]smoothSheafCommRing.forgetStalk: Identify the stalk at a point of the sheaf-of-commutative-rings of functions fromMtoR(forRa smooth ring) with the stalk at that point of the corresponding sheaf of types.smoothSheafCommRing.eval: upgradesmoothSheaf.evalto a ring homomorphism when considering the sheaf of smooth functions into a smooth commutative ringsmoothSheafCommGroup.compLeft: For a manifoldMand a smooth homomorphismφbetween abelian Lie groupsA,A', the 'postcomposition-by-φ' morphism of sheaves fromsmoothSheafCommGroup IM I M AtosmoothSheafCommGroup IM I' M A'
Main results #
smoothSheaf.eval_surjective:smoothSheaf.evalis surjective.smoothSheafCommRing.eval_surjective:smoothSheafCommRing.evalis surjective.
TODO #
There are variants of smoothSheafCommGroup.compLeft for GroupCat, RingCat, CommRingCat;
this is just boilerplate and can be added as needed.
Similarly, there are variants of smoothSheafCommRing.forgetStalk and smoothSheafCommRing.eval
for GroupCat, CommGroupCat and RingCat which can be added as needed.
Currently there is a universe restriction: one can consider the sheaf of smooth functions from M
to N only if M and N are in the same universe. For example, since ℂ is in Type, we can
only consider the structure sheaf of complex manifolds in Type, which is unsatisfactory. The
obstacle here is in the underlying category theory constructions, which are not sufficiently
universe polymorphic. A direct attempt to generalize the universes worked in Lean 3 but was
reverted because it was hard to port to Lean 4, see
https://github.com/leanprover-community/mathlib/pull/19230
The current (Oct 2023) proposal to permit these generalizations is to use the new UnivLE
typeclass, and some (but not all) of the underlying category theory constructions have now been
generalized by this method: see https://github.com/leanprover-community/mathlib4/pull/5724,
https://github.com/leanprover-community/mathlib4/pull/5726.
def
smoothSheaf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(N : Type u)
[TopologicalSpace N]
[ChartedSpace H N]
:
TopCat.Sheaf (Type u) (TopCat.of M)
The sheaf of smooth functions from M to N, as a sheaf of types.
Equations
- smoothSheaf IM I M N = StructureGroupoid.LocalInvariantProp.sheaf M N ⋯
Instances For
instance
smoothSheaf.coeFun
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(N : Type u)
[TopologicalSpace N]
[ChartedSpace H N]
(U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ)
:
CoeFun ((smoothSheaf IM I M N).presheaf.obj U) fun (x : (smoothSheaf IM I M N).presheaf.obj U) => ↥U.unop → N
Equations
- smoothSheaf.coeFun IM I N U = StructureGroupoid.LocalInvariantProp.sheafHasCoeToFun M N ⋯ U
theorem
smoothSheaf.obj_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(N : Type u)
[TopologicalSpace N]
[ChartedSpace H N]
(U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ)
:
(smoothSheaf IM I M N).presheaf.obj U = ContMDiffMap IM I (↥U.unop) N ⊤
The object of smoothSheaf IM I M N for the open set U in M is
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!
def
smoothSheaf.eval
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(N : Type u)
[TopologicalSpace N]
[ChartedSpace H N]
(x : M)
:
(smoothSheaf IM I M N).presheaf.stalk x → N
Canonical map from the stalk of smoothSheaf IM I M N at x to N, given by evaluating
sections at x.
Equations
- smoothSheaf.eval IM I N x = TopCat.stalkToFiber (StructureGroupoid.LocalInvariantProp.localPredicate M N ⋯) x
Instances For
def
smoothSheaf.evalHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(N : Type u)
[TopologicalSpace N]
[ChartedSpace H N]
(x : ↑(TopCat.of M))
:
(smoothSheaf IM I M N).presheaf.stalk x ⟶ N
Canonical map from the stalk of smoothSheaf IM I M N at x to N, given by evaluating
sections at x, considered as a morphism in the category of types.
Equations
Instances For
def
smoothSheaf.evalAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(N : Type u)
[TopologicalSpace N]
[ChartedSpace H N]
(x : ↑(TopCat.of M))
(U : TopologicalSpace.OpenNhds x)
(i : (smoothSheaf IM I M N).presheaf.obj (Opposite.op U.obj))
:
N
Given manifolds M, N and an open neighbourhood U of a point x : M, the evaluation-at-x
map to N from smooth functions from U to N.
Equations
- smoothSheaf.evalAt IM I N x U i = ↑i ⟨x, ⋯⟩
Instances For
theorem
smoothSheaf.ι_evalHom_assoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(N : Type u)
[TopologicalSpace N]
[ChartedSpace H N]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
{Z : Type u}
(h : N ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M N).val) U)
(CategoryTheory.CategoryStruct.comp (smoothSheaf.evalHom IM I N x) h) = CategoryTheory.CategoryStruct.comp (smoothSheaf.evalAt IM I N x U.unop) h
theorem
smoothSheaf.ι_evalHom_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(N : Type u)
[TopologicalSpace N]
[ChartedSpace H N]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x✝)ᵒᵖ)
(x : ((TopologicalSpace.OpenNhds.inclusion x✝).op.comp (smoothSheaf IM I M N).val).obj U)
:
↑x ⟨x✝, ⋯⟩ = (fun
(f :
{ f : ↥((TopologicalSpace.OpenNhds.inclusion x✝).obj U.unop) → N //
(StructureGroupoid.LocalInvariantProp.localPredicate M N ⋯).pred f }) =>
↑f ⟨x✝, ⋯⟩)
x
@[simp]
theorem
smoothSheaf.ι_evalHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(N : Type u)
[TopologicalSpace N]
[ChartedSpace H N]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M N).val) U)
(smoothSheaf.evalHom IM I N x) = smoothSheaf.evalAt IM I N x U.unop
theorem
smoothSheaf.eval_surjective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(N : Type u)
[TopologicalSpace N]
[ChartedSpace H N]
(x : M)
:
Function.Surjective (smoothSheaf.eval IM I N x)
The eval map is surjective at x.
instance
instNontrivialStalkPresheafSmoothSheaf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
(N : Type u)
[TopologicalSpace N]
[ChartedSpace H N]
[Nontrivial N]
(x : M)
:
Nontrivial ((smoothSheaf IM I M N).presheaf.stalk x)
Equations
- ⋯ = ⋯
@[simp]
theorem
smoothSheaf.eval_germ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace H N]
(U : TopologicalSpace.Opens M)
(x : ↥U)
(f : (smoothSheaf IM I M N).presheaf.obj (Opposite.op U))
:
smoothSheaf.eval IM I N (↑x) ((smoothSheaf IM I M N).presheaf.germ x f) = ↑f x
theorem
smoothSheaf.smooth_section
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
{N : Type u}
[TopologicalSpace N]
[ChartedSpace H N]
{U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ}
(f : (smoothSheaf IM I M N).presheaf.obj U)
:
Smooth IM I ↑f
noncomputable instance
instAddGroupObjOppositeOpensαTopologicalSpaceOfPresheafSmoothSheaf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(G : Type u)
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I G]
(U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ)
:
AddGroup ((smoothSheaf IM I M G).presheaf.obj U)
Equations
- instAddGroupObjOppositeOpensαTopologicalSpaceOfPresheafSmoothSheaf IM I M G U = SmoothMap.addGroup
noncomputable instance
instGroupObjOppositeOpensαTopologicalSpaceOfPresheafSmoothSheaf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(G : Type u)
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I G]
(U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ)
:
Group ((smoothSheaf IM I M G).presheaf.obj U)
Equations
- instGroupObjOppositeOpensαTopologicalSpaceOfPresheafSmoothSheaf IM I M G U = SmoothMap.group
theorem
smoothPresheafAddGroup.proof_1
(M : Type u_1)
[TopologicalSpace M]
:
∀ {X Y : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ}, (X ⟶ Y) → Y.unop ≤ X.unop
theorem
smoothPresheafAddGroup.proof_2
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
{EM : Type u_5}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_4}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_1)
[TopologicalSpace M]
[ChartedSpace HM M]
(G : Type u_1)
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I G]
:
∀ (x : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ),
{
obj := fun (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) =>
AddGroupCat.of ((smoothSheaf IM I M G).presheaf.obj U),
map := fun {X Y : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ} (h : X ⟶ Y) =>
AddGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I G ⋯) }.map
(CategoryTheory.CategoryStruct.id x) = {
obj := fun (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) =>
AddGroupCat.of ((smoothSheaf IM I M G).presheaf.obj U),
map := fun {X Y : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ} (h : X ⟶ Y) =>
AddGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I G ⋯) }.map
(CategoryTheory.CategoryStruct.id x)
noncomputable def
smoothPresheafAddGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(G : Type u)
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I G]
:
The presheaf of smooth functions from M to G, for G an additive Lie group, as a
presheaf of additive groups.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
smoothPresheafAddGroup.proof_3
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
{EM : Type u_5}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_4}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_1)
[TopologicalSpace M]
[ChartedSpace HM M]
(G : Type u_1)
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I G]
:
∀ {X Y Z : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ} (x : X ⟶ Y) (x_1 : Y ⟶ Z),
{
obj := fun (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) =>
AddGroupCat.of ((smoothSheaf IM I M G).presheaf.obj U),
map := fun {X Y : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ} (h : X ⟶ Y) =>
AddGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I G ⋯) }.map
(CategoryTheory.CategoryStruct.comp x x_1) = {
obj := fun (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) =>
AddGroupCat.of ((smoothSheaf IM I M G).presheaf.obj U),
map := fun {X Y : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ} (h : X ⟶ Y) =>
AddGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I G ⋯) }.map
(CategoryTheory.CategoryStruct.comp x x_1)
noncomputable def
smoothPresheafGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(G : Type u)
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I G]
:
The presheaf of smooth functions from M to G, for G a Lie group, as a presheaf of groups.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
smoothSheafAddGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(G : Type u)
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I G]
:
The sheaf of smooth functions from M to G, for G an additive Lie group, as a
sheaf of additive groups.
Equations
- smoothSheafAddGroup IM I M G = { val := smoothPresheafAddGroup IM I M G, cond := ⋯ }
Instances For
theorem
smoothSheafAddGroup.proof_1
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
{EM : Type u_5}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_4}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_1)
[TopologicalSpace M]
[ChartedSpace HM M]
(G : Type u_1)
[TopologicalSpace G]
[ChartedSpace H G]
[AddGroup G]
[LieAddGroup I G]
:
noncomputable def
smoothSheafGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(G : Type u)
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[LieGroup I G]
:
The sheaf of smooth functions from M to G, for G a Lie group, as a sheaf of
groups.
Equations
- smoothSheafGroup IM I M G = { val := smoothPresheafGroup IM I M G, cond := ⋯ }
Instances For
noncomputable instance
instAddCommGroupObjOppositeOpensαTopologicalSpaceOfPresheafSmoothSheaf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(A : Type u)
[TopologicalSpace A]
[ChartedSpace H A]
[AddCommGroup A]
[LieAddGroup I A]
(U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ)
:
AddCommGroup ((smoothSheaf IM I M A).presheaf.obj U)
Equations
- instAddCommGroupObjOppositeOpensαTopologicalSpaceOfPresheafSmoothSheaf IM I M A U = SmoothMap.addCommGroup
noncomputable instance
instCommGroupObjOppositeOpensαTopologicalSpaceOfPresheafSmoothSheaf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(A : Type u)
[TopologicalSpace A]
[ChartedSpace H A]
[CommGroup A]
[LieGroup I A]
(U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ)
:
CommGroup ((smoothSheaf IM I M A).presheaf.obj U)
Equations
- instCommGroupObjOppositeOpensαTopologicalSpaceOfPresheafSmoothSheaf IM I M A U = SmoothMap.commGroup
theorem
smoothPresheafAddCommGroup.proof_2
(M : Type u_1)
[TopologicalSpace M]
:
∀ {X Y : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ}, (X ⟶ Y) → Y.unop ≤ X.unop
noncomputable def
smoothPresheafAddCommGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(A : Type u)
[TopologicalSpace A]
[ChartedSpace H A]
[AddCommGroup A]
[LieAddGroup I A]
:
The presheaf of smooth functions from M to A, for A an additive abelian Lie
group, as a presheaf of additive abelian groups.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
smoothPresheafAddCommGroup.proof_3
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
{EM : Type u_5}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_4}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_1)
[TopologicalSpace M]
[ChartedSpace HM M]
(A : Type u_1)
[TopologicalSpace A]
[ChartedSpace H A]
[AddCommGroup A]
[LieAddGroup I A]
:
∀ (x : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ),
{
obj := fun (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) =>
AddCommGroupCat.of ((smoothSheaf IM I M A).presheaf.obj U),
map := fun {X Y : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ} (h : X ⟶ Y) =>
AddCommGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I A ⋯) }.map
(CategoryTheory.CategoryStruct.id x) = {
obj := fun (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) =>
AddCommGroupCat.of ((smoothSheaf IM I M A).presheaf.obj U),
map := fun {X Y : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ} (h : X ⟶ Y) =>
AddCommGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I A ⋯) }.map
(CategoryTheory.CategoryStruct.id x)
theorem
smoothPresheafAddCommGroup.proof_4
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
{EM : Type u_5}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_4}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_1)
[TopologicalSpace M]
[ChartedSpace HM M]
(A : Type u_1)
[TopologicalSpace A]
[ChartedSpace H A]
[AddCommGroup A]
[LieAddGroup I A]
:
∀ {X Y Z : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ} (x : X ⟶ Y) (x_1 : Y ⟶ Z),
{
obj := fun (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) =>
AddCommGroupCat.of ((smoothSheaf IM I M A).presheaf.obj U),
map := fun {X Y : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ} (h : X ⟶ Y) =>
AddCommGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I A ⋯) }.map
(CategoryTheory.CategoryStruct.comp x x_1) = {
obj := fun (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) =>
AddCommGroupCat.of ((smoothSheaf IM I M A).presheaf.obj U),
map := fun {X Y : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ} (h : X ⟶ Y) =>
AddCommGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I A ⋯) }.map
(CategoryTheory.CategoryStruct.comp x x_1)
theorem
smoothPresheafAddCommGroup.proof_1
{𝕜 : Type u_4}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(A : Type u_1)
[TopologicalSpace A]
[ChartedSpace H A]
[AddCommGroup A]
[LieAddGroup I A]
:
SmoothAdd I A
noncomputable def
smoothPresheafCommGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(A : Type u)
[TopologicalSpace A]
[ChartedSpace H A]
[CommGroup A]
[LieGroup I A]
:
The presheaf of smooth functions from M to A, for A an abelian Lie group, as a
presheaf of abelian groups.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
smoothSheafAddCommGroup.proof_1
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
{EM : Type u_5}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_4}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u_1)
[TopologicalSpace M]
[ChartedSpace HM M]
(A : Type u_1)
[TopologicalSpace A]
[ChartedSpace H A]
[AddCommGroup A]
[LieAddGroup I A]
:
noncomputable def
smoothSheafAddCommGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(A : Type u)
[TopologicalSpace A]
[ChartedSpace H A]
[AddCommGroup A]
[LieAddGroup I A]
:
The sheaf of smooth functions from M to
A, for A an abelian additive Lie group, as a sheaf of abelian additive groups.
Equations
- smoothSheafAddCommGroup IM I M A = { val := smoothPresheafAddCommGroup IM I M A, cond := ⋯ }
Instances For
noncomputable def
smoothSheafCommGroup
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(A : Type u)
[TopologicalSpace A]
[ChartedSpace H A]
[CommGroup A]
[LieGroup I A]
:
The sheaf of smooth functions from M to A, for A an abelian Lie group, as a
sheaf of abelian groups.
Equations
- smoothSheafCommGroup IM I M A = { val := smoothPresheafCommGroup IM I M A, cond := ⋯ }
Instances For
theorem
smoothSheafAddCommGroup.compLeft.proof_3
{𝕜 : Type u_6}
[NontriviallyNormedField 𝕜]
{EM : Type u_5}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_4}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_7}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E H')
(M : Type u_1)
[TopologicalSpace M]
[ChartedSpace HM M]
(A : Type u_1)
(A' : Type u_1)
[TopologicalSpace A]
[ChartedSpace H A]
[TopologicalSpace A']
[ChartedSpace H' A']
[AddCommGroup A]
[AddCommGroup A']
[LieAddGroup I A]
[LieAddGroup I' A']
(φ : A →+ A')
(hφ : Smooth I I' ⇑φ)
:
∀ (x x_1 : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) (x_2 : x ⟶ x_1),
CategoryTheory.CategoryStruct.comp ((smoothSheafAddCommGroup IM I M A).val.map x_2)
((fun (x : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) =>
AddCommGroupCat.ofHom (SmoothMap.compLeftAddMonoidHom IM (↥x.unop) φ hφ))
x_1) = CategoryTheory.CategoryStruct.comp ((smoothSheafAddCommGroup IM I M A).val.map x_2)
((fun (x : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) =>
AddCommGroupCat.ofHom (SmoothMap.compLeftAddMonoidHom IM (↥x.unop) φ hφ))
x_1)
theorem
smoothSheafAddCommGroup.compLeft.proof_1
{𝕜 : Type u_4}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(A : Type u_1)
[TopologicalSpace A]
[ChartedSpace H A]
[AddCommGroup A]
[LieAddGroup I A]
:
SmoothAdd I A
def
smoothSheafAddCommGroup.compLeft
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_6}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E H')
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(A : Type u)
(A' : Type u)
[TopologicalSpace A]
[ChartedSpace H A]
[TopologicalSpace A']
[ChartedSpace H' A']
[AddCommGroup A]
[AddCommGroup A']
[LieAddGroup I A]
[LieAddGroup I' A']
(φ : A →+ A')
(hφ : Smooth I I' ⇑φ)
:
smoothSheafAddCommGroup IM I M A ⟶ smoothSheafAddCommGroup IM I' M A'
For a manifold M and a smooth homomorphism φ between abelian additive Lie groups
A, A', the 'left-composition-by-φ' morphism of sheaves from smoothSheafAddCommGroup IM I M A
to smoothSheafAddCommGroup IM I' M A'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
smoothSheafAddCommGroup.compLeft.proof_2
{𝕜 : Type u_4}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H' : Type u_3}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E H')
(A' : Type u_1)
[TopologicalSpace A']
[ChartedSpace H' A']
[AddCommGroup A']
[LieAddGroup I' A']
:
SmoothAdd I' A'
def
smoothSheafCommGroup.compLeft
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{H' : Type u_6}
[TopologicalSpace H']
(I' : ModelWithCorners 𝕜 E H')
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(A : Type u)
(A' : Type u)
[TopologicalSpace A]
[ChartedSpace H A]
[TopologicalSpace A']
[ChartedSpace H' A']
[CommGroup A]
[CommGroup A']
[LieGroup I A]
[LieGroup I' A']
(φ : A →* A')
(hφ : Smooth I I' ⇑φ)
:
smoothSheafCommGroup IM I M A ⟶ smoothSheafCommGroup IM I' M A'
For a manifold M and a smooth homomorphism φ between abelian Lie groups A, A', the
'left-composition-by-φ' morphism of sheaves from smoothSheafCommGroup IM I M A to
smoothSheafCommGroup IM I' M A'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
instRingObjOppositeOpensαTopologicalSpaceOfPresheafSmoothSheaf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[Ring R]
[SmoothRing I R]
(U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ)
:
Ring ((smoothSheaf IM I M R).presheaf.obj U)
Equations
- instRingObjOppositeOpensαTopologicalSpaceOfPresheafSmoothSheaf IM I M R U = SmoothMap.ring
def
smoothPresheafRing
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[Ring R]
[SmoothRing I R]
:
The presheaf of smooth functions from M to R, for R a smooth ring, as a presheaf
of rings.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
smoothSheafRing
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[Ring R]
[SmoothRing I R]
:
The sheaf of smooth functions from M to R, for R a smooth ring, as a sheaf of
rings.
Equations
- smoothSheafRing IM I M R = { val := smoothPresheafRing IM I M R, cond := ⋯ }
Instances For
instance
instCommRingObjOppositeOpensαTopologicalSpaceOfPresheafSmoothSheaf
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ)
:
CommRing ((smoothSheaf IM I M R).presheaf.obj U)
Equations
- instCommRingObjOppositeOpensαTopologicalSpaceOfPresheafSmoothSheaf IM I M R U = SmoothMap.commRing
def
smoothPresheafCommRing
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
:
The presheaf of smooth functions from M to R, for R a smooth commutative ring, as a
presheaf of commutative rings.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
smoothSheafCommRing
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
:
The sheaf of smooth functions from M to R, for R a smooth commutative ring, as a sheaf of
commutative rings.
Equations
- smoothSheafCommRing IM I M R = { val := smoothPresheafCommRing IM I M R, cond := ⋯ }
Instances For
instance
smoothSheafCommRing.coeFun
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ)
:
CoeFun ↑((smoothSheafCommRing IM I M R).presheaf.obj U) fun (x : ↑((smoothSheafCommRing IM I M R).presheaf.obj U)) =>
↥U.unop → R
Equations
- smoothSheafCommRing.coeFun IM I M R U = StructureGroupoid.LocalInvariantProp.sheafHasCoeToFun M R ⋯ U
def
smoothSheafCommRing.forgetStalk
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
:
(CategoryTheory.forget CommRingCat).obj ((smoothSheafCommRing IM I M R).presheaf.stalk x) ≅ (smoothSheaf IM I M R).presheaf.stalk x
Identify the stalk at a point of the sheaf-of-commutative-rings of functions from M to R
(for R a smooth ring) with the stalk at that point of the corresponding sheaf of types.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
smoothSheafCommRing.ι_forgetStalk_hom_assoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
{Z : Type u}
(h : (smoothSheaf IM I M R).presheaf.stalk x ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(⇑(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U))
(CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).hom h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M R).presheaf)
U)
h
theorem
smoothSheafCommRing.ι_forgetStalk_hom_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x✝)ᵒᵖ)
(x : (CategoryTheory.forget CommRingCat).obj
(((TopologicalSpace.OpenNhds.inclusion x✝).op.comp (smoothSheafCommRing IM I M R).presheaf).obj U))
:
(CategoryTheory.preservesColimitIso (CategoryTheory.forget CommRingCat)
((TopologicalSpace.OpenNhds.inclusion x✝).op.comp (smoothSheafCommRing IM I M R).presheaf)).hom
((CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x✝).op.comp (smoothSheafCommRing IM I M R).presheaf) U)
x) = (CategoryTheory.Limits.colimit.ι
(((TopologicalSpace.OpenNhds.inclusion x✝).op.comp (smoothSheafCommRing IM I M R).presheaf).comp
(CategoryTheory.forget CommRingCat))
U)
x
@[simp]
theorem
smoothSheafCommRing.ι_forgetStalk_hom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
:
CategoryTheory.CategoryStruct.comp
(⇑(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U))
(smoothSheafCommRing.forgetStalk IM I M R x).hom = CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M R).presheaf) U
theorem
smoothSheafCommRing.ι_forgetStalk_inv_assoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
{Z : Type u}
(h : (CategoryTheory.forget CommRingCat).obj ((smoothSheafCommRing IM I M R).presheaf.stalk x) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M R).presheaf)
U)
(CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).inv h) = CategoryTheory.CategoryStruct.comp
((CategoryTheory.forget CommRingCat).map
(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U))
h
theorem
smoothSheafCommRing.ι_forgetStalk_inv_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x✝)ᵒᵖ)
(x : ((TopologicalSpace.OpenNhds.inclusion x✝).op.comp (smoothSheaf IM I M R).presheaf).obj U)
:
(smoothSheafCommRing.forgetStalk IM I M R x✝).inv
(CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x✝).op.comp (smoothSheaf IM I M R).presheaf)
U x) = ⇑(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x✝).op.comp (smoothSheafCommRing IM I M R).presheaf) U)
x
@[simp]
theorem
smoothSheafCommRing.ι_forgetStalk_inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M R).presheaf)
U)
(smoothSheafCommRing.forgetStalk IM I M R x).inv = (CategoryTheory.forget CommRingCat).map
(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U)
def
smoothSheafCommRing.evalAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
(U : TopologicalSpace.OpenNhds x)
:
(smoothSheafCommRing IM I M R).presheaf.obj (Opposite.op U.obj) ⟶ CommRingCat.of R
Given a smooth commutative ring R and a manifold M, and an open neighbourhood U of a point
x : M, the evaluation-at-x map to R from smooth functions from U to R.
Equations
- smoothSheafCommRing.evalAt IM I M R x U = SmoothMap.evalRingHom ⟨x, ⋯⟩
Instances For
def
smoothSheafCommRing.evalHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
:
(smoothSheafCommRing IM I M R).presheaf.stalk x ⟶ CommRingCat.of R
Canonical ring homomorphism from the stalk of smoothSheafCommRing IM I M R at x to R,
given by evaluating sections at x, considered as a morphism in the category of commutative rings.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
smoothSheafCommRing.eval
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : M)
:
↑((smoothSheafCommRing IM I M R).presheaf.stalk x) →+* R
Canonical ring homomorphism from the stalk of smoothSheafCommRing IM I M R at x to R,
given by evaluating sections at x.
Equations
- smoothSheafCommRing.eval IM I M R x = smoothSheafCommRing.evalHom IM I M R x
Instances For
theorem
smoothSheafCommRing.ι_evalHom_assoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
{Z : CommRingCat}
(h : CommRingCat.of R ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U)
(CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.evalHom IM I M R x) h) = CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.evalAt IM I M R x U.unop) h
theorem
smoothSheafCommRing.ι_evalHom_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x✝)ᵒᵖ)
(x : (CategoryTheory.forget CommRingCat).obj
(((TopologicalSpace.OpenNhds.inclusion x✝).op.comp (smoothSheafCommRing IM I M R).presheaf).obj U))
:
(CategoryTheory.Limits.colimit.desc
((TopologicalSpace.OpenNhds.inclusion x✝).op.comp (smoothSheafCommRing IM I M R).presheaf)
{ pt := { α := R, str := inst✝¹ },
ι :=
{ app := fun (U : (TopologicalSpace.OpenNhds x✝)ᵒᵖ) => smoothSheafCommRing.evalAt IM I M R x✝ U.unop,
naturality := ⋯ } })
((CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x✝).op.comp (smoothSheafCommRing IM I M R).presheaf) U)
x) = (smoothSheafCommRing.evalAt IM I M R x✝ U.unop) x
@[simp]
theorem
smoothSheafCommRing.ι_evalHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U)
(smoothSheafCommRing.evalHom IM I M R x) = smoothSheafCommRing.evalAt IM I M R x U.unop
@[simp]
theorem
smoothSheafCommRing.evalHom_germ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(U : TopologicalSpace.Opens ↑(TopCat.of M))
(x : ↥U)
(f : ↑((smoothSheafCommRing IM I M R).presheaf.obj (Opposite.op U)))
:
(smoothSheafCommRing.evalHom IM I M R ↑x) (((smoothSheafCommRing IM I M R).presheaf.germ x) f) = ↑f x
theorem
smoothSheafCommRing.forgetStalk_inv_comp_eval_assoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
{Z : Type u}
(h : R ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).inv
(CategoryTheory.CategoryStruct.comp (⇑(smoothSheafCommRing.evalHom IM I M R x)) h) = CategoryTheory.CategoryStruct.comp (smoothSheaf.evalHom IM I R x) h
theorem
smoothSheafCommRing.forgetStalk_inv_comp_eval_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
(x : (smoothSheaf IM I M R).presheaf.stalk x✝)
:
(smoothSheafCommRing.evalHom IM I M R x✝) ((smoothSheafCommRing.forgetStalk IM I M R x✝).inv x) = smoothSheaf.evalHom IM I R x✝ x
@[simp]
theorem
smoothSheafCommRing.forgetStalk_inv_comp_eval
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
:
CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).inv
⇑(smoothSheafCommRing.evalHom IM I M R x) = smoothSheaf.evalHom IM I R x
theorem
smoothSheafCommRing.forgetStalk_hom_comp_evalHom_assoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
{Z : Type u}
(h : R ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).hom
(CategoryTheory.CategoryStruct.comp (smoothSheaf.evalHom IM I R x) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget CommRingCat).map (smoothSheafCommRing.evalHom IM I M R x))
h
theorem
smoothSheafCommRing.forgetStalk_hom_comp_evalHom_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
(x : (CategoryTheory.forget CommRingCat).obj ((smoothSheafCommRing IM I M R).presheaf.stalk x✝))
:
smoothSheaf.evalHom IM I R x✝ ((smoothSheafCommRing.forgetStalk IM I M R x✝).hom x) = ⇑(smoothSheafCommRing.evalHom IM I M R x✝) x
@[simp]
theorem
smoothSheafCommRing.forgetStalk_hom_comp_evalHom
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : ↑(TopCat.of M))
:
CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).hom (smoothSheaf.evalHom IM I R x) = (CategoryTheory.forget CommRingCat).map (smoothSheafCommRing.evalHom IM I M R x)
theorem
smoothSheafCommRing.eval_surjective
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(x : M)
:
Function.Surjective ⇑(smoothSheafCommRing.eval IM I M R x)
instance
instNontrivialαCommRingStalkCommRingCatPresheafSmoothSheafCommRing
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
(IM : ModelWithCorners 𝕜 EM HM)
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
(M : Type u)
[TopologicalSpace M]
[ChartedSpace HM M]
(R : Type u)
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
[Nontrivial R]
(x : M)
:
Nontrivial ↑((smoothSheafCommRing IM I M R).presheaf.stalk x)
Equations
- ⋯ = ⋯
@[simp]
theorem
smoothSheafCommRing.eval_germ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{EM : Type u_2}
[NormedAddCommGroup EM]
[NormedSpace 𝕜 EM]
{HM : Type u_3}
[TopologicalSpace HM]
{IM : ModelWithCorners 𝕜 EM HM}
{E : Type u_4}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_5}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u}
[TopologicalSpace M]
[ChartedSpace HM M]
{R : Type u}
[TopologicalSpace R]
[ChartedSpace H R]
[CommRing R]
[SmoothRing I R]
(U : TopologicalSpace.Opens M)
(x : ↥U)
(f : ↑((smoothSheafCommRing IM I M R).presheaf.obj (Opposite.op U)))
:
(smoothSheafCommRing.eval IM I M R ↑x) (((smoothSheafCommRing IM I M R).presheaf.germ x) f) = ↑f x