# 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 #

• smoothSheaf: The sheaf of smooth functions from M to N, as a sheaf of types
• smoothSheaf.eval: Canonical map onto N from the stalk of smoothSheaf IM I M N at x, given by evaluating sections at x
• smoothSheafGroup, 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 from M to R (for R a smooth ring) with the stalk at that point of the corresponding sheaf of types.
• smoothSheafCommRing.eval: upgrade smoothSheaf.eval to a ring homomorphism when considering the sheaf of smooth functions into a smooth commutative ring
• smoothSheafCommGroup.compLeft: For a manifold M and a smooth homomorphism φ between abelian Lie groups A, A', the 'postcomposition-by-φ' morphism of sheaves from smoothSheafCommGroup IM I M A to smoothSheafCommGroup IM I' M A'

# Main results #

• smoothSheaf.eval_surjective: smoothSheaf.eval is surjective.
• smoothSheafCommRing.eval_surjective: smoothSheafCommRing.eval is 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} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (N : Type u) [] [] :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance smoothSheaf.coeFun {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) {M : Type u} [] [ChartedSpace HM M] (N : Type u) [] [] (U : ) :
CoeFun ((TopCat.Sheaf.presheaf (smoothSheaf IM I M N)).obj U) fun (x : (TopCat.Sheaf.presheaf (smoothSheaf IM I M N)).obj U) => U.unopN
Equations
• One or more equations did not get rendered due to their size.
theorem smoothSheaf.obj_eq {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) {M : Type u} [] [ChartedSpace HM M] (N : Type u) [] [] (U : ) :
(TopCat.Sheaf.presheaf (smoothSheaf IM I M N)).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} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) {M : Type u} [] [ChartedSpace HM M] (N : Type u) [] [] (x : M) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def smoothSheaf.evalHom {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) {M : Type u} [] [ChartedSpace HM M] (N : Type u) [] [] (x : ()) :

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
• One or more equations did not get rendered due to their size.
Instances For
def smoothSheaf.evalAt {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) {M : Type u} [] [ChartedSpace HM M] (N : Type u) [] [] (x : ()) (U : ) (i : (TopCat.Sheaf.presheaf (smoothSheaf IM I M N)).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_assoc {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) {M : Type u} [] [ChartedSpace HM M] (N : Type u) [] [] (x : ()) (U : ) {Z : Type u} (h : N Z) :
theorem smoothSheaf.ι_evalHom_apply {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) {M : Type u} [] [ChartedSpace HM M] (N : Type u) [] [] (x : ()) (U : ) (x : (CategoryTheory.Functor.comp (smoothSheaf IM I M N).val).obj U) :
x { val := x✝, property := (_ : x✝ U.unop.obj) } = (fun (f : { f : (.obj U.unop)N // TopCat.PrelocalPredicate.pred (StructureGroupoid.LocalInvariantProp.localPredicate M N (_ : )).toPrelocalPredicate f }) => f { val := x✝, property := (_ : x✝ U.unop.obj) }) x
@[simp]
theorem smoothSheaf.ι_evalHom {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) {M : Type u} [] [ChartedSpace HM M] (N : Type u) [] [] (x : ()) (U : ) :
theorem smoothSheaf.eval_surjective {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) {M : Type u} [] [ChartedSpace HM M] (N : Type u) [] [] (x : M) :

The eval map is surjective at x.

instance instNontrivialStalkTypeTypesInstHasColimitsTypeTypesOfPresheafSmoothSheaf {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) {M : Type u} [] [ChartedSpace HM M] (N : Type u) [] [] [] (x : M) :
Equations
@[simp]
theorem smoothSheaf.eval_germ {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] {IM : ModelWithCorners 𝕜 EM HM} {E : Type u_4} [] {H : Type u_5} [] {I : } {M : Type u} [] [ChartedSpace HM M] {N : Type u} [] [] (U : ) (x : U) (f : (TopCat.Sheaf.presheaf (smoothSheaf IM I M N)).obj ()) :
theorem smoothSheaf.smooth_section {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] {IM : ModelWithCorners 𝕜 EM HM} {E : Type u_4} [] {H : Type u_5} [] {I : } {M : Type u} [] [ChartedSpace HM M] {N : Type u} [] [] {U : } (f : (TopCat.Sheaf.presheaf (smoothSheaf IM I M N)).obj U) :
Smooth IM I f
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
theorem smoothPresheafAddGroup.proof_2 {𝕜 : Type u_6} {EM : Type u_5} [] [NormedSpace 𝕜 EM] {HM : Type u_4} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [] {H : Type u_2} [] (I : ) (M : Type u_1) [] [ChartedSpace HM M] (G : Type u_1) [] [] [] [] :
∀ (x : ), { obj := fun (U : ) => AddGroupCat.of ((TopCat.Sheaf.presheaf (smoothSheaf IM I M G)).obj U), map := fun {X Y : } (h : X Y) => AddGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I G (_ : Y.unop X.unop)) }.map = { obj := fun (U : ) => AddGroupCat.of ((TopCat.Sheaf.presheaf (smoothSheaf IM I M G)).obj U), map := fun {X Y : } (h : X Y) => AddGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I G (_ : Y.unop X.unop)) }.map
theorem smoothPresheafAddGroup.proof_3 {𝕜 : Type u_6} {EM : Type u_5} [] [NormedSpace 𝕜 EM] {HM : Type u_4} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [] {H : Type u_2} [] (I : ) (M : Type u_1) [] [ChartedSpace HM M] (G : Type u_1) [] [] [] [] :
∀ {X Y Z : } (x : X Y) (x_1 : Y Z), { obj := fun (U : ) => AddGroupCat.of ((TopCat.Sheaf.presheaf (smoothSheaf IM I M G)).obj U), map := fun {X Y : } (h : X Y) => AddGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I G (_ : Y.unop X.unop)) }.map = { obj := fun (U : ) => AddGroupCat.of ((TopCat.Sheaf.presheaf (smoothSheaf IM I M G)).obj U), map := fun {X Y : } (h : X Y) => AddGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I G (_ : Y.unop X.unop)) }.map
theorem smoothPresheafAddGroup.proof_1 (M : Type u_1) [] :
∀ {X Y : }, (X Y)Y.unop X.unop
noncomputable def smoothPresheafAddGroup {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (G : Type u) [] [] [] [] :

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
noncomputable def smoothPresheafGroup {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (G : Type u) [] [] [] [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} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (G : Type u) [] [] [] [] :

The sheaf of smooth functions from M to G, for G an additive Lie group, as a sheaf of additive groups.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem smoothSheafAddGroup.proof_1 {𝕜 : Type u_6} {EM : Type u_5} [] [NormedSpace 𝕜 EM] {HM : Type u_4} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [] {H : Type u_2} [] (I : ) (M : Type u_1) [] [ChartedSpace HM M] (G : Type u_1) [] [] [] [] :
noncomputable def smoothSheafGroup {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (G : Type u) [] [] [] [LieGroup I G] :

The sheaf of smooth functions from M to G, for G a Lie group, as a sheaf of groups.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
theorem smoothPresheafAddCommGroup.proof_2 (M : Type u_1) [] :
∀ {X Y : }, (X Y)Y.unop X.unop
noncomputable def smoothPresheafAddCommGroup {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (A : Type u) [] [] [] [] :

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_1 {𝕜 : Type u_4} {E : Type u_2} [] {H : Type u_3} [] (I : ) (A : Type u_1) [] [] [] [] :
theorem smoothPresheafAddCommGroup.proof_3 {𝕜 : Type u_6} {EM : Type u_5} [] [NormedSpace 𝕜 EM] {HM : Type u_4} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [] {H : Type u_2} [] (I : ) (M : Type u_1) [] [ChartedSpace HM M] (A : Type u_1) [] [] [] [] :
∀ (x : ), { obj := fun (U : ) => AddCommGroupCat.of ((TopCat.Sheaf.presheaf (smoothSheaf IM I M A)).obj U), map := fun {X Y : } (h : X Y) => AddCommGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I A (_ : Y.unop X.unop)) }.map = { obj := fun (U : ) => AddCommGroupCat.of ((TopCat.Sheaf.presheaf (smoothSheaf IM I M A)).obj U), map := fun {X Y : } (h : X Y) => AddCommGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I A (_ : Y.unop X.unop)) }.map
theorem smoothPresheafAddCommGroup.proof_4 {𝕜 : Type u_6} {EM : Type u_5} [] [NormedSpace 𝕜 EM] {HM : Type u_4} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [] {H : Type u_2} [] (I : ) (M : Type u_1) [] [ChartedSpace HM M] (A : Type u_1) [] [] [] [] :
∀ {X Y Z : } (x : X Y) (x_1 : Y Z), { obj := fun (U : ) => AddCommGroupCat.of ((TopCat.Sheaf.presheaf (smoothSheaf IM I M A)).obj U), map := fun {X Y : } (h : X Y) => AddCommGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I A (_ : Y.unop X.unop)) }.map = { obj := fun (U : ) => AddCommGroupCat.of ((TopCat.Sheaf.presheaf (smoothSheaf IM I M A)).obj U), map := fun {X Y : } (h : X Y) => AddCommGroupCat.ofHom (SmoothMap.restrictAddMonoidHom IM I A (_ : Y.unop X.unop)) }.map
noncomputable def smoothPresheafCommGroup {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (A : Type u) [] [] [] [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} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (A : Type u) [] [] [] [] :

The sheaf of smooth functions from M to A, for A an abelian additive Lie group, as a sheaf of abelian additive groups.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem smoothSheafAddCommGroup.proof_1 {𝕜 : Type u_6} {EM : Type u_5} [] [NormedSpace 𝕜 EM] {HM : Type u_4} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [] {H : Type u_2} [] (I : ) (M : Type u_1) [] [ChartedSpace HM M] (A : Type u_1) [] [] [] [] :
noncomputable def smoothSheafCommGroup {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (A : Type u) [] [] [] [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
• One or more equations did not get rendered due to their size.
Instances For
def smoothSheafAddCommGroup.compLeft {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E H') (M : Type u) [] [ChartedSpace HM M] (A : Type u) (A' : Type u) [] [] [] [ChartedSpace H' 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_3 {𝕜 : Type u_6} {EM : Type u_5} [] [NormedSpace 𝕜 EM] {HM : Type u_4} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_3} [] {H : Type u_2} [] (I : ) {H' : Type u_7} [] (I' : ModelWithCorners 𝕜 E H') (M : Type u_1) [] [ChartedSpace HM M] (A : Type u_1) (A' : Type u_1) [] [] [] [ChartedSpace H' A'] [] [] [] [LieAddGroup I' A'] (φ : A →+ A') (hφ : Smooth I I' φ) :
∀ (x x_1 : ) (x_2 : x x_1), CategoryTheory.CategoryStruct.comp (().val.map x_2) ((fun (x : ) => AddCommGroupCat.ofHom (SmoothMap.compLeftAddMonoidHom IM (x.unop) φ )) x_1) = CategoryTheory.CategoryStruct.comp (().val.map x_2) ((fun (x : ) => AddCommGroupCat.ofHom (SmoothMap.compLeftAddMonoidHom IM (x.unop) φ )) x_1)
theorem smoothSheafAddCommGroup.compLeft.proof_1 {𝕜 : Type u_4} {E : Type u_2} [] {H : Type u_3} [] (I : ) (A : Type u_1) [] [] [] [] :
theorem smoothSheafAddCommGroup.compLeft.proof_2 {𝕜 : Type u_4} {E : Type u_2} [] {H' : Type u_3} [] (I' : ModelWithCorners 𝕜 E H') (A' : Type u_1) [] [ChartedSpace H' A'] [] [LieAddGroup I' A'] :
SmoothAdd I' A'
def smoothSheafCommGroup.compLeft {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) {H' : Type u_6} [] (I' : ModelWithCorners 𝕜 E H') (M : Type u) [] [ChartedSpace HM M] (A : Type u) (A' : Type u) [] [] [] [ChartedSpace H' 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
Equations
• One or more equations did not get rendered due to their size.
def smoothPresheafRing {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [Ring 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} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [Ring R] [] :

The sheaf of smooth functions from M to R, for R a smooth ring, as a sheaf of rings.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
def smoothPresheafCommRing {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] :

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} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] :

The sheaf of smooth functions from M to R, for R a smooth commutative ring, as a sheaf of commutative rings.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance smoothSheafCommRing.coeFun {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (U : ) :
CoeFun ((TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)).obj U) fun (x : ((TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)).obj U)) => U.unopR
Equations
• One or more equations did not get rendered due to their size.
def smoothSheafCommRing.forgetStalk {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (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} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) (U : ) {Z : Type u} (h : TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) x Z) :
theorem smoothSheafCommRing.ι_forgetStalk_hom_apply {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) (U : ) (x : .obj (().obj U)) :
@[simp]
theorem smoothSheafCommRing.ι_forgetStalk_hom {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) (U : ) :
theorem smoothSheafCommRing.ι_forgetStalk_inv_assoc {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) (U : ) {Z : Type u} (h : .obj () Z) :
theorem smoothSheafCommRing.ι_forgetStalk_inv_apply {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) (U : ) (x : ().obj U) :
@[simp]
theorem smoothSheafCommRing.ι_forgetStalk_inv {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) (U : ) :
def smoothSheafCommRing.evalAt {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) (U : ) :

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} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) :

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} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : M) :
() →+* 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_assoc {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) (U : ) {Z : CommRingCat} (h : ) :
theorem smoothSheafCommRing.ι_evalHom_apply {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) (U : ) (x : .obj (().obj U)) :
(CategoryTheory.Limits.colimit.desc () { pt := , ι := CategoryTheory.NatTrans.mk fun (U : ) => smoothSheafCommRing.evalAt IM I M R x✝ U.unop }) ((CategoryTheory.Limits.colimit.ι () U) x) = (smoothSheafCommRing.evalAt IM I M R x✝ U.unop) x
@[simp]
theorem smoothSheafCommRing.ι_evalHom {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) (U : ) :
@[simp]
theorem smoothSheafCommRing.evalHom_germ {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (U : ) (x : U) (f : ((TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)).obj ())) :
theorem smoothSheafCommRing.forgetStalk_inv_comp_eval_assoc {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) {Z : Type u} (h : Z) :
theorem smoothSheafCommRing.forgetStalk_inv_comp_eval_apply {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) (x : TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) x✝) :
(smoothSheafCommRing.evalHom IM I M R x✝) (().inv x) = (smoothSheaf.evalHom IM I R x✝) x
@[simp]
theorem smoothSheafCommRing.forgetStalk_inv_comp_eval {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) :
theorem smoothSheafCommRing.forgetStalk_hom_comp_evalHom_assoc {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) {Z : Type u} (h : R Z) :
theorem smoothSheafCommRing.forgetStalk_hom_comp_evalHom_apply {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) (x : .obj (TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x✝)) :
smoothSheaf.evalHom IM I R x✝ (().hom x) = (smoothSheafCommRing.evalHom IM I M R x✝) x
@[simp]
theorem smoothSheafCommRing.forgetStalk_hom_comp_evalHom {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : ()) :
theorem smoothSheafCommRing.eval_surjective {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] (x : M) :
instance instNontrivialαCommRingStalkCommRingCatInstCommRingCatLargeCategoryHasColimits_commRingCatOfPresheafSmoothSheafCommRing {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u) [] [ChartedSpace HM M] (R : Type u) [] [] [] [] [] (x : M) :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem smoothSheafCommRing.eval_germ {𝕜 : Type u_1} {EM : Type u_2} [] [NormedSpace 𝕜 EM] {HM : Type u_3} [] {IM : ModelWithCorners 𝕜 EM HM} {E : Type u_4} [] {H : Type u_5} [] {I : } {M : Type u} [] [ChartedSpace HM M] {R : Type u} [] [] [] [] (U : ) (x : U) (f : ((TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)).obj ())) :