Commit 2023-10-09 13:35 4f086f94

feat: structure sheaf of a manifold (#7332) In https://github.com/leanprover-community/mathlib/pull/19146, we defined StructureGroupoid.LocalInvariantProp.sheaf, the sheaf-of-types of functions f : M → M' (for charted spaces M, M') satisfying some local property in the sense of StructureGroupoid.LocalInvariantProp (for example continuity, differentiability, smoothness). In this PR, in the case of smoothness, we upgrade this to a sheaf of groups if M' is a Lie group, a sheaf of abelian groups if M' is an abelian Lie group, and a sheaf of rings if M' is a "smooth ring".