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 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 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) { carrier := M, str := inst✝ }

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

Equations

• smoothSheaf IM I M N = StructureGroupoid.LocalInvariantProp.sheaf M N ⋯

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 ↑{ carrier := M, str := inst✝ })ᵒᵖ) : CoeFun ((smoothSheaf IM I M N).presheaf.obj U) fun (x : (smoothSheaf IM I M N).presheaf.obj U) => ↥(Opposite.unop U) → N

Equations

• smoothSheaf.coeFun IM I N U = StructureGroupoid.LocalInvariantProp.sheafHasCoeToFun M N ⋯ U

theorem smoothSheaf.obj_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EM : Type u_2} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_3} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u} [TopologicalSpace M] [ChartedSpace HM M] (N : Type u) [TopologicalSpace N] [ChartedSpace H N] (U : (TopologicalSpace.Opens ↑{ carrier := M, str := inst✝ })ᵒᵖ) : (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 x → N

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

Equations

• smoothSheaf.eval IM I N x = TopCat.stalkToFiber (StructureGroupoid.LocalInvariantProp.localPredicate M N ⋯) x

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 : ↑{ carrier := M, str := inst✝ }) : (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

• smoothSheaf.evalHom IM I N x = TopCat.stalkToFiber (StructureGroupoid.LocalInvariantProp.localPredicate M N ⋯) x

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 : ↑{ carrier := M, str := inst✝ }) (U : TopologicalSpace.OpenNhds x) (i : (smoothSheaf IM I M N).presheaf.obj (Opposite.op U.obj)) : N

Given manifolds M, N and an open neighbourhood U of a point x : M, the evaluation-at-x map to N from smooth functions from U to N.

Equations

• smoothSheaf.evalAt IM I N x U i = ↑i ⟨x, ⋯⟩

@[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 : ↑{ carrier := M, str := inst✝ }) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M N).val) 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 : ↑{ carrier := M, str := inst✝ }) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ) {Z : Type u} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M N).val) U) (CategoryTheory.CategoryStruct.comp (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 : ↑{ carrier := M, str := inst✝ }) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ) (x✝ : ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M N).val).obj U) : (evalHom IM I N x) (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M N).val) 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 ↑{ carrier := M, str := inst✝ })ᵒᵖ} (f : (smoothSheaf IM I M N).presheaf.obj U) : ContMDiff IM I ↑⊤ ↑f

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 ↑{ carrier := M, str := inst✝ })ᵒᵖ) : Group ((smoothSheaf IM I M G).presheaf.obj U)

Equations

• instGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf IM I M G U = ContMDiffMap.group

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 ↑{ carrier := M, str := inst✝ })ᵒᵖ) : AddGroup ((smoothSheaf IM I M G).presheaf.obj U)

Equations

• instAddGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf IM I M G U = ContMDiffMap.addGroup

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] : TopCat.Presheaf GrpCat { carrier := M, str := inst✝ }

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.

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] : TopCat.Presheaf AddGrpCat { carrier := M, str := inst✝ }

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.

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] : TopCat.Sheaf GrpCat { carrier := M, str := inst✝ }

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

Equations

• smoothSheafGroup IM I M G = { val := smoothPresheafGroup IM I M G, cond := ⋯ }

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] : TopCat.Sheaf AddGrpCat { carrier := M, str := inst✝ }

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

Equations

• smoothSheafAddGroup IM I M G = { val := smoothPresheafAddGroup IM I M G, cond := ⋯ }

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 ↑{ carrier := M, str := inst✝ })ᵒᵖ) : CommGroup ((smoothSheaf IM I M A).presheaf.obj U)

Equations

• instCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf IM I M A U = ContMDiffMap.commGroup

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 ↑{ carrier := M, str := inst✝ })ᵒᵖ) : AddCommGroup ((smoothSheaf IM I M A).presheaf.obj U)

Equations

• instAddCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf IM I M A U = ContMDiffMap.addCommGroup

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] : TopCat.Presheaf CommGrpCat { carrier := M, str := inst✝ }

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.

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] : TopCat.Presheaf AddCommGrpCat { carrier := M, str := inst✝ }

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.

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] : TopCat.Sheaf CommGrpCat { carrier := M, str := inst✝ }

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

Equations

• smoothSheafCommGroup IM I M A = { val := smoothPresheafCommGroup IM I M A, cond := ⋯ }

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] : TopCat.Sheaf AddCommGrpCat { carrier := M, str := inst✝ }

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

Equations

• smoothSheafAddCommGroup IM I M A = { val := smoothPresheafAddCommGroup IM I M A, cond := ⋯ }

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' ↑⊤ ⇑φ) : smoothSheafCommGroup IM I M A ⟶ smoothSheafCommGroup IM I' M A'

For a manifold M and a smooth homomorphism φ between abelian Lie groups A, A', the 'left-composition-by-φ' morphism of sheaves from smoothSheafCommGroup IM I M A to smoothSheafCommGroup IM I' M A'.

Equations

• One or more equations did not get rendered due to their size.

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' ↑⊤ ⇑φ) : smoothSheafAddCommGroup IM I M A ⟶ smoothSheafAddCommGroup IM I' M A'

For a manifold M and a smooth homomorphism φ between abelian additive Lie groups A, A', the 'left-composition-by-φ' morphism of sheaves from smoothSheafAddCommGroup IM I M A to smoothSheafAddCommGroup IM I' M A'.

Equations

• One or more equations did not get rendered due to their size.

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 ↑{ carrier := M, str := inst✝ })ᵒᵖ) : Ring ((smoothSheaf IM I M R).presheaf.obj U)

Equations

• instRingObjOppositeOpensCarrierOfPresheafSmoothSheaf IM I M R U = ContMDiffMap.ring

def smoothPresheafRing {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EM : Type u_2} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_3} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (R : Type u) [TopologicalSpace R] [ChartedSpace H R] [Ring R] [ContMDiffRing I (↑⊤) R] : TopCat.Presheaf RingCat { carrier := M, str := inst✝ }

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.

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] : TopCat.Sheaf RingCat { carrier := M, str := inst✝ }

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

Equations

• smoothSheafRing IM I M R = { val := smoothPresheafRing IM I M R, cond := ⋯ }

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 ↑{ carrier := M, str := inst✝ })ᵒᵖ) : CommRing ((smoothSheaf IM I M R).presheaf.obj U)

Equations

• instCommRingObjOppositeOpensCarrierOfPresheafSmoothSheaf IM I M R U = ContMDiffMap.commRing

def smoothPresheafCommRing {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EM : Type u_2} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_3} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (R : Type u) [TopologicalSpace R] [ChartedSpace H R] [CommRing R] [ContMDiffRing I (↑⊤) R] : TopCat.Presheaf CommRingCat { carrier := M, str := inst✝ }

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.

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] : TopCat.Sheaf CommRingCat { carrier := M, str := inst✝ }

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

Equations

• smoothSheafCommRing IM I M R = { val := smoothPresheafCommRing IM I M R, cond := ⋯ }

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 ↑{ carrier := M, str := inst✝ })ᵒᵖ) : CoeFun ↑((smoothSheafCommRing IM I M R).presheaf.obj U) fun (x : ↑((smoothSheafCommRing IM I M R).presheaf.obj U)) => ↥(Opposite.unop U) → R

Equations

• smoothSheafCommRing.coeFun IM I M R U = StructureGroupoid.LocalInvariantProp.sheafHasCoeToFun M R ⋯ U

def smoothSheafCommRing.forgetStalk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EM : Type u_2} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_3} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (R : Type u) [TopologicalSpace R] [ChartedSpace H R] [CommRing R] [ContMDiffRing I (↑⊤) R] (x : ↑{ carrier := M, str := inst✝ }) : ↑((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.

@[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 : ↑{ carrier := M, str := inst✝ }) (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 : ↑{ carrier := M, str := inst✝ }) (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 : ↑{ carrier := M, str := inst✝ }) (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 : ↑{ carrier := M, str := inst✝ }) (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 : ↑{ carrier := M, str := inst✝ }) (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 : ↑{ carrier := M, str := inst✝ }) (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✝

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 : ↑{ carrier := M, str := inst✝ }) (U : TopologicalSpace.OpenNhds x) : (smoothSheafCommRing IM I M R).presheaf.obj (Opposite.op U.obj) ⟶ { carrier := R, commRing := inst✝¹ }

Given a smooth commutative ring R and a manifold M, and an open neighbourhood U of a point x : M, the evaluation-at-x map to R from smooth functions from U to R.

Equations

• smoothSheafCommRing.evalAt IM I M R x U = CommRingCat.ofHom (ContMDiffMap.evalRingHom ⟨x, ⋯⟩)

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 : ↑{ carrier := M, str := inst✝ }) : (smoothSheafCommRing IM I M R).presheaf.stalk x ⟶ { carrier := R, commRing := inst✝¹ }

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.

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) : ↑((smoothSheafCommRing IM I M R).presheaf.stalk x) →+* R

Canonical ring homomorphism from the stalk of smoothSheafCommRing IM I M R at x to R, given by evaluating sections at x.

Equations

• smoothSheafCommRing.eval IM I M R x = CommRingCat.Hom.hom (smoothSheafCommRing.evalHom IM I M R x)

@[simp]

theorem smoothSheafCommRing.ι_evalHom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EM : Type u_2} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_3} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) {E : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (R : Type u) [TopologicalSpace R] [ChartedSpace H R] [CommRing R] [ContMDiffRing I (↑⊤) R] (x : ↑{ carrier := M, str := inst✝ }) (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 : ↑{ carrier := M, str := inst✝ }) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ) {Z : CommRingCat} (h : { carrier := R, commRing := inst✝¹ } ⟶ 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 : ↑{ carrier := M, str := inst✝ }) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ) (x✝ : CategoryTheory.ToType (((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✝) = (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 ↑{ carrier := M, str := inst✝ }) (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 : ↑{ carrier := M, str := inst✝ }) : 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 : ↑{ carrier := M, str := inst✝ }) {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 : ↑{ carrier := M, str := inst✝ }) (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 : ↑{ carrier := M, str := inst✝ }) : 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 : ↑{ carrier := M, str := inst✝ }) {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 : ↑{ carrier := M, str := inst✝ }) (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⟩