Elaborators for differential geometry

This file defines custom elaborators for differential geometry to allow for more compact notation. We introduce a class of elaborators for handling differentiability on manifolds, and the elaborator T% for converting dependent sections of fibre bundles into non-dependent functions into the total space.

All of these elaborators are scoped to the Manifold namespace.

Differentiability on manifolds

We provide compact notation for differentiability and continuous differentiability on manifolds, including inference of the model with corners.

Notation	Elaborates to
MDiff f	MDifferentiable I J f
MDiffAt f x	MDifferentiableAt I J f x
MDiff[u] f	MDifferentiableOn I J f u
MDiffAt[u] f x	MDifferentiableWithinAt I J f u x
CMDiff n f	ContMDiff I J n f
CMDiffAt n f x	ContMDiffAt I J n f x
CMDiff[u] n f	ContMDiffOn I J n f u
CMDiffAt[u] n f x	ContMDiffWithinAt I J n f u x
mfderiv[u] f x	mfderivWithin I J f u x
mfderiv% f x	mfderiv I J f x

In each of these cases, the models with corners are inferred from the domain and codomain of f. The search for models with corners uses the local context and is (almost) only based on expression structure, hence hopefully fast enough to always run.

This has no dedicated support for product manifolds (or product vector spaces) yet; adding this is left for future changes. (It would need to make a choice between e.g. the trivial model with corners on a product E × F and the product of the trivial models on E and F). In these settings, the elaborators should be avoided (for now).

T%

Secondly, this file adds an elaborator T% to ease working with sections in a fibre bundle, which converts a section s : Π x : M, V x to a non-dependent function into the total space of the bundle.

-- omitted: let `V` be a fibre bundle over `M`

variable {σ : Π x : M, V x} in
#check T% σ -- `(fun x ↦ TotalSpace.mk' F x (σ x)) : M → TotalSpace F V`

-- Note how the name of the bound variable `x` is preserved.
variable {σ : (x : E) → Trivial E E' x} in
#check T% σ -- `(fun x ↦ TotalSpace.mk' E' x (σ x)) : E → TotalSpace E' (Trivial E E')`

variable {s : E → E'} in
#check T% s -- `(fun a ↦ TotalSpace.mk' E' a (s a)) : E → TotalSpace E' (Trivial E E')`

---

These elaborators can be combined: CMDiffAt[u] n (T% s) x

Warning. These elaborators are a proof of concept; the implementation should be considered a prototype. Don't rewrite all of mathlib to use it just yet. Notable bugs and limitations include the following.

TODO

• extend the elaborators to guess models with corners on product manifolds (this has to make a guess, hence cannot always be correct: but it could make the guess that is correct 90% of the time). For products of vector spaces E × F, this could print a warning about making a choice between the model in E × F and the product of the models on E and F.
• extend the elaborators to support OpenPartialHomeomorphs and PartialEquivs
• better error messages (as needed)
• further testing and fixing of edge cases
• add tests for all of the above
• add delaborators for these elaborators

def Manifold.«termT%_» : Lean.ParserDescr

Elaborator for sections in a fibre bundle: converts a section s : Π x : M, V x as a dependent function to a non-dependent function into the total space. This handles the cases of

• sections of a trivial bundle
• vector fields on a manifold (i.e., sections of the tangent bundle)
• sections of an explicit fibre bundle
• turning a bare function E → E' into a section of the trivial bundle Bundle.Trivial E E'

This elaborator searches the local context for suitable hypotheses for the above cases by matching on the expression structure, avoiding isDefEq. Therefore, it is (hopefully) fast enough to always run.

Equations

• Manifold.«termT%_» = Lean.ParserDescr.node `Manifold.«termT%_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "T% ") (Lean.ParserDescr.cat `term 1023))

def Manifold.Elab.findModel (e : Lean.Expr) (baseInfo : Option (Lean.Expr × Lean.Expr) := none) : Lean.Elab.TermElabM Lean.Expr

Try to find a ModelWithCorners instance on a type (represented by an expression e), using the local context to infer the appropriate instance. This supports the following cases:

• the model with corners on the total space of a vector bundle
• a model with corners on a manifold
• the trivial model 𝓘(𝕜, E) on a normed space
• if the above are not found, try to find a NontriviallyNormedField instance on the type of e, and if successful, return 𝓘(𝕜).

Further cases can be added as necessary.

Return an expression describing the found model with corners.

baseInfo is only used for the first case, a model with corners on the total space of the vector bundle. In this case, it contains a pair of expressions (e, i) describing the type of the base and the model with corners on the base: these are required to construct the right model with corners.

This implementation is not maximally robust yet.

Equations

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

def Manifold.Elab.findModel.fromTotalSpace (e : Lean.Expr) (baseInfo : Option (Lean.Expr × Lean.Expr)) : Lean.Elab.TermElabM Lean.Expr

Attempt to find a model from a TotalSpace first by attempting to use any provided baseInfo, then by seeing if it is the total space of a tangent bundle.

Equations

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

def Manifold.Elab.findModel.fromTotalSpace.fromBaseInfo (baseInfo : Option (Lean.Expr × Lean.Expr)) (F : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Attempt to use the provided baseInfo to find a model.

Equations

• One or more equations did not get rendered due to their size.
• Manifold.Elab.findModel.fromTotalSpace.fromBaseInfo baseInfo F = Lean.throwError (Lean.toMessageData "No `baseInfo` provided")

def Manifold.Elab.findModel.fromTotalSpace.tangentSpace (V : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Attempt to find a model from the total space of a tangent bundle.

Equations

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

def Manifold.Elab.findModel.fromNormedSpace (e : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Attempt to find the trivial model on a normed space.

Equations

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

def Manifold.Elab.findModel.fromChartedSpace (e : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Attempt to find a model with corners on a manifold.

Equations

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

def Manifold.Elab.findModel.fromNormedField (e : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Attempt to find a model with corners from a normed field. We attempt to find a global instance here.

Equations

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

def Manifold.Elab.findModels (e : Lean.Expr) (es : Option Lean.Expr) : Lean.Elab.TermElabM (Lean.Expr × Lean.Expr)

If the type of e is a non-dependent function between spaces src and tgt, try to find a model with corners on both src and tgt. If successful, return both models.

We pass e instead of just its type for better diagnostics.

If es is some, we verify that src and the type of es are definitionally equal.

Equations

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

def Manifold.«termMDiffAt[_]__» : Lean.ParserDescr

MDiffAt[s] f x elaborates to MDifferentiableWithinAt I J f s x, trying to determine I and J from the local context. The argument x can be omitted.

Equations

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

def Manifold.termMDiffAt__ : Lean.ParserDescr

MDiffAt f x elaborates to MDifferentiableAt I J f x, trying to determine I and J from the local context. The argument x can be omitted.

Equations

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

def Manifold.«termMDiff[_]__» : Lean.ParserDescr

MDiff[s] f elaborates to MDifferentiableOn I J f s, trying to determine I and J from the local context.

Equations

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

def Manifold.termMDiff__ : Lean.ParserDescr

MDiff f elaborates to MDifferentiable I J f, trying to determine I and J from the local context.

Equations

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

def Manifold.«termCMDiffAt[_]____» : Lean.ParserDescr

CMDiffAt[s] n f x elaborates to ContMDiffWithinAt I J n f s x, trying to determine I and J from the local context. n is coerced to WithTop ℕ∞ if necessary (so passing a ℕ, ∞ or ω are all supported). The argument x can be omitted.

Equations

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

def Manifold.termCMDiffAt____ : Lean.ParserDescr

CMDiffAt n f x elaborates to ContMDiffAt I J n f x trying to determine I and J from the local context. n is coerced to WithTop ℕ∞ if necessary (so passing a ℕ, ∞ or ω are all supported). The argument x can be omitted.

Equations

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

def Manifold.«termCMDiff[_]____» : Lean.ParserDescr

CMDiff[s] n f elaborates to ContMDiffOn I J n f s, trying to determine I and J from the local context. n is coerced to WithTop ℕ∞ if necessary (so passing a ℕ, ∞ or ω are all supported).

Equations

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

def Manifold.termCMDiff____ : Lean.ParserDescr

CMDiff n f elaborates to ContMDiff I J n f, trying to determine I and J from the local context. n is coerced to WithTop ℕ∞ if necessary (so passing a ℕ, ∞ or ω are all supported).

Equations

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

def Manifold.«termMfderiv[_]__» : Lean.ParserDescr

mfderiv[u] f x elaborates to mfderivWithin I J f u x, trying to determine I and J from the local context.

Equations

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

def Manifold.«termMfderiv%__» : Lean.ParserDescr

mfderiv% f x elaborates to mfderiv I J f x, trying to determine I and J from the local context.

Equations

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

Trace classes

Note that the overall Elab trace class does not inherit the trace classes defined in this section, since they provide verbose information.