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.lean. 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 GrpCat, RingCat, CommRingCat;
this is just boilerplate and can be added as needed.
Similarly, there are variants of smoothSheafCommRing.forgetStalk and smoothSheafCommRing.eval
for GrpCat, CommGrpCat 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.
Instances For
@[implicit_reducible]
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) => ↥(Opposite.unop U) → N
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 (↥(Opposite.unop U)) 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!
noncomputable 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.
Instances For
noncomputable 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))
:
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.
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))
:
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.
Instances For
@[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).obj) U)
(evalHom IM I N x) = evalAt IM I N x (Opposite.unop U)
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).obj) U)
(CategoryTheory.CategoryStruct.comp (evalHom IM I N x) h) = CategoryTheory.CategoryStruct.comp (evalAt IM I N x (Opposite.unop U)) 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).obj).obj U)
:
evalHom IM I N x
(CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M N).obj) U
x✝) = evalAt IM I N x (Opposite.unop U) x✝
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 (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)
@[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 : M)
(hx : x ∈ U)
(f : (smoothSheaf IM I M N).presheaf.obj (Opposite.op U))
:
eval IM I N x ((smoothSheaf IM I M N).presheaf.germ U x hx f) = ↑f ⟨x, hx⟩
theorem
smoothSheaf.contMDiff_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)
:
@[implicit_reducible]
noncomputable instance
instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf
{𝕜 : 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)
@[implicit_reducible]
noncomputable instance
instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf
{𝕜 : 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)
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.
Instances For
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.
Instances For
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.
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.
Instances For
@[implicit_reducible]
noncomputable instance
instCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf
{𝕜 : 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)
@[implicit_reducible]
noncomputable instance
instAddCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf
{𝕜 : 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)
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.
Instances For
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.
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.
Instances For
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.
Instances For
noncomputable 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 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φ : ContMDiff I I' ↑⊤ ⇑φ)
:
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'.
Instances For
noncomputable 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 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φ : ContMDiff I I' ↑⊤ ⇑φ)
:
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'.
Instances For
@[implicit_reducible]
noncomputable instance
instRingObjOppositeOpensCarrierOfPresheafSmoothSheaf
{𝕜 : 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]
[ContMDiffRing I (↑⊤) R]
(U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ)
:
Ring ((smoothSheaf IM I M R).presheaf.obj U)
noncomputable 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]
[ContMDiffRing I (↑⊤) R]
:
The presheaf of smooth functions from M to R, for R a smooth ring, as a presheaf
of rings.
Instances For
noncomputable 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]
[ContMDiffRing I (↑⊤) R]
:
The sheaf of smooth functions from M to R, for R a smooth ring, as a sheaf of
rings.
Instances For
@[implicit_reducible]
noncomputable instance
instCommRingObjOppositeOpensCarrierOfPresheafSmoothSheaf
{𝕜 : 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]
[ContMDiffRing I (↑⊤) R]
(U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ)
:
CommRing ((smoothSheaf IM I M R).presheaf.obj U)
noncomputable 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]
[ContMDiffRing I (↑⊤) R]
:
The presheaf of smooth functions from M to R, for R a smooth commutative ring, as a
presheaf of commutative rings.
Instances For
noncomputable 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]
[ContMDiffRing I (↑⊤) R]
:
The sheaf of smooth functions from M to R, for R a smooth commutative ring, as a sheaf of
commutative rings.
Instances For
@[implicit_reducible]
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]
[ContMDiffRing 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)) =>
↥(Opposite.unop U) → R
noncomputable 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]
[ContMDiffRing I (↑⊤) R]
(x : ↑(TopCat.of M))
:
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.
Instances For
@[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]
[ContMDiffRing I (↑⊤) R]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
:
CategoryTheory.CategoryStruct.comp
(⇑(CommRingCat.Hom.hom
(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U)))
(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_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]
[ContMDiffRing 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
(⇑(CommRingCat.Hom.hom
(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U)))
(CategoryTheory.CategoryStruct.comp (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]
[ContMDiffRing I (↑⊤) R]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
(x✝ :
↑((smoothSheafCommRing IM I M R).presheaf.obj
(Opposite.op ((TopologicalSpace.OpenNhds.inclusion x).obj (Opposite.unop U)))))
:
(forgetStalk IM I M R x).hom
((CommRingCat.Hom.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 (smoothSheaf 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]
[ContMDiffRing 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)
(forgetStalk IM I M R x).inv = ⇑(CategoryTheory.ConcreteCategory.hom
(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing 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]
[ContMDiffRing I (↑⊤) R]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
{Z : Type u}
(h : ↑((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 (forgetStalk IM I M R x).inv h) = CategoryTheory.CategoryStruct.comp
(⇑(CategoryTheory.ConcreteCategory.hom
(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]
[ContMDiffRing 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)
:
(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.ConcreteCategory.hom
(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U))
x✝
noncomputable 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]
[ContMDiffRing I (↑⊤) R]
(x : ↑(TopCat.of M))
(U : TopologicalSpace.OpenNhds x)
:
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.
Instances For
noncomputable 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]
[ContMDiffRing I (↑⊤) R]
(x : ↑(TopCat.of M))
:
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.
Instances For
noncomputable 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]
[ContMDiffRing I (↑⊤) R]
(x : M)
:
Canonical ring homomorphism from the stalk of smoothSheafCommRing IM I M R at x to R,
given by evaluating sections at x.
Instances For
@[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]
[ContMDiffRing 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)
(evalHom IM I M R x) = evalAt IM I M R x (Opposite.unop U)
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]
[ContMDiffRing 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 (evalHom IM I M R x) h) = CategoryTheory.CategoryStruct.comp (evalAt IM I M R x (Opposite.unop U)) 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]
[ContMDiffRing I (↑⊤) R]
(x : ↑(TopCat.of M))
(U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
(x✝ : ↑(((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf).obj U))
:
(CategoryTheory.ConcreteCategory.hom (evalHom IM I M R x))
((CategoryTheory.ConcreteCategory.hom
(CategoryTheory.Limits.colimit.ι
((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U))
x✝) = (CategoryTheory.ConcreteCategory.hom (evalAt IM I M R x (Opposite.unop U))) x✝
@[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]
[ContMDiffRing I (↑⊤) R]
(U : TopologicalSpace.Opens ↑(TopCat.of M))
(x : M)
(hx : x ∈ U)
(f : ↑((smoothSheafCommRing IM I M R).presheaf.obj (Opposite.op U)))
:
(CategoryTheory.ConcreteCategory.hom (evalHom IM I M R x))
((CategoryTheory.ConcreteCategory.hom ((smoothSheafCommRing IM I M R).presheaf.germ U x hx)) f) = ↑f ⟨x, hx⟩
@[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]
[ContMDiffRing I (↑⊤) R]
(x : ↑(TopCat.of M))
:
CategoryTheory.CategoryStruct.comp (forgetStalk IM I M R x).inv ⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) = smoothSheaf.evalHom IM I R 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]
[ContMDiffRing I (↑⊤) R]
(x : ↑(TopCat.of M))
{Z : Type u}
(h : R ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (forgetStalk IM I M R x).inv
(CategoryTheory.CategoryStruct.comp (⇑(CommRingCat.Hom.hom (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]
[ContMDiffRing I (↑⊤) R]
(x : ↑(TopCat.of M))
(x✝ : (smoothSheaf IM I M R).presheaf.stalk x)
:
(CommRingCat.Hom.hom (evalHom IM I M R x)) ((forgetStalk IM I M R x).inv x✝) = smoothSheaf.evalHom IM I 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]
[ContMDiffRing I (↑⊤) R]
(x : ↑(TopCat.of M))
:
CategoryTheory.CategoryStruct.comp (forgetStalk IM I M R x).hom (smoothSheaf.evalHom IM I R x) = ⇑(CategoryTheory.ConcreteCategory.hom (evalHom IM I M 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]
[ContMDiffRing I (↑⊤) R]
(x : ↑(TopCat.of M))
{Z : Type u}
(h : R ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (forgetStalk IM I M R x).hom
(CategoryTheory.CategoryStruct.comp (smoothSheaf.evalHom IM I R x) h) = CategoryTheory.CategoryStruct.comp (⇑(CategoryTheory.ConcreteCategory.hom (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]
[ContMDiffRing I (↑⊤) R]
(x : ↑(TopCat.of M))
(x✝ : ↑((smoothSheafCommRing IM I M R).presheaf.stalk x))
:
smoothSheaf.evalHom IM I R x ((forgetStalk IM I M R x).hom x✝) = (CategoryTheory.ConcreteCategory.hom (evalHom IM I M R x)) 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]
[ContMDiffRing I (↑⊤) R]
(x : M)
:
Function.Surjective ⇑(eval IM I M R x)
instance
instNontrivialCarrierStalkCommRingCatPresheafSmoothSheafCommRing
{𝕜 : 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]
[ContMDiffRing I (↑⊤) R]
[Nontrivial R]
(x : M)
:
Nontrivial ↑((smoothSheafCommRing IM I M R).presheaf.stalk x)
@[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]
[ContMDiffRing I (↑⊤) R]
(U : TopologicalSpace.Opens M)
(x : M)
(hx : x ∈ U)
(f : ↑((smoothSheafCommRing IM I M R).presheaf.obj (Opposite.op U)))
:
(eval IM I M R x) ((CategoryTheory.ConcreteCategory.hom ((smoothSheafCommRing IM I M R).presheaf.germ U x hx)) f) = ↑f ⟨x, hx⟩