Documentation

Mathlib.Geometry.Manifold.Sheaf.Smooth

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 #

Main results #

TODO #

There are variants of smoothSheafCommGroup.compLeft for Grp, RingCat, CommRingCat; this is just boilerplate and can be added as needed.

Similarly, there are variants of smoothSheafCommRing.forgetStalk and smoothSheafCommRing.eval for Grp, CommGrp 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] :

The sheaf of smooth functions from M to N, as a sheaf of types.

Equations
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) => (Opposite.unop U)N
    Equations
    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!

    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 xN

    Canonical map from the stalk of smoothSheaf IM I M N at x to N, given by evaluating sections at x.

    Equations
    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
        Instances For
          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) :
          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) :

          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
          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
          theorem smoothPresheafAddGroup.proof_2 {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {EM : Type u_3} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_4} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_6} [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))ᵒᵖ) => AddGrp.of ((smoothSheaf IM I M G).presheaf.obj U), map := fun {X Y : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ} (h : X Y) => AddGrp.ofHom (SmoothMap.restrictAddMonoidHom IM I G ) }.map (CategoryTheory.CategoryStruct.id x) = { obj := fun (U : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ) => AddGrp.of ((smoothSheaf IM I M G).presheaf.obj U), map := fun {X Y : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ} (h : X Y) => AddGrp.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_2} [NontriviallyNormedField 𝕜] {EM : Type u_3} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_4} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_6} [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))ᵒᵖ) => AddGrp.of ((smoothSheaf IM I M G).presheaf.obj U), map := fun {X Y : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ} (h : X Y) => AddGrp.ofHom (SmoothMap.restrictAddMonoidHom IM I G ) }.map (CategoryTheory.CategoryStruct.comp x x_1) = { obj := fun (U : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ) => AddGrp.of ((smoothSheaf IM I M G).presheaf.obj U), map := fun {X Y : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ} (h : X Y) => AddGrp.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
              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.

                Equations
                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
                  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
                  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_2} [NontriviallyNormedField 𝕜] {EM : Type u_3} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_4} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_6} [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))ᵒᵖ) => AddCommGrp.of ((smoothSheaf IM I M A).presheaf.obj U), map := fun {X Y : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ} (h : X Y) => AddCommGrp.ofHom (SmoothMap.restrictAddMonoidHom IM I A ) }.map (CategoryTheory.CategoryStruct.id x) = { obj := fun (U : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ) => AddCommGrp.of ((smoothSheaf IM I M A).presheaf.obj U), map := fun {X Y : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ} (h : X Y) => AddCommGrp.ofHom (SmoothMap.restrictAddMonoidHom IM I A ) }.map (CategoryTheory.CategoryStruct.id x)
                    theorem smoothPresheafAddCommGroup.proof_4 {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {EM : Type u_3} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_4} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_6} [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))ᵒᵖ) => AddCommGrp.of ((smoothSheaf IM I M A).presheaf.obj U), map := fun {X Y : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ} (h : X Y) => AddCommGrp.ofHom (SmoothMap.restrictAddMonoidHom IM I A ) }.map (CategoryTheory.CategoryStruct.comp x x_1) = { obj := fun (U : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ) => AddCommGrp.of ((smoothSheaf IM I M A).presheaf.obj U), map := fun {X Y : (TopologicalSpace.Opens (TopCat.of M))ᵒᵖ} (h : X Y) => AddCommGrp.ofHom (SmoothMap.restrictAddMonoidHom IM I A ) }.map (CategoryTheory.CategoryStruct.comp x x_1)
                    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
                      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
                      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
                        Instances For
                          theorem smoothSheafAddCommGroup.compLeft.proof_3 {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {EM : Type u_3} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_4} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_6} [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' φ) :
                          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' φ) :

                          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_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H' : Type u_2} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E H') (A' : Type u_4) [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' φ) :

                            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
                              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
                                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
                                  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
                                    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)) => (Opposite.unop U)R
                                      Equations
                                      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_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) :
                                        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
                                        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
                                            Instances For
                                              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)) :
                                              @[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_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
                                              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
                                              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) :
                                              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