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
HasMFDerivAt[s] f x f'	HasMFDerivWithinAt I J f s x f'
HasMFDerivAt% f x f'	HasMFDerivAt I J f x f'

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 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.
• better error messages (as needed), with tests
• further testing and fixing of edge cases (with tests)
• add delaborators for these elaborators

def Manifold.Elab.totalSpaceMk (e : Lean.Expr) : Lean.MetaM Lean.Expr

Utility for sections in a fibre bundle: if an expression e is a section s : Π x : M, V x as a dependent function, convert it 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 searches the local context for suitable hypotheses for the above cases by matching on the expression structure, avoiding isDefEq. Therefore, it should be fast enough to always run. This process can be traced with set_option Elab.DiffGeo.TotalSpaceMk true.

All applications of e in the resulting expression are beta-reduced. If none of the handled cases apply, we simply return e (after beta-reducing).

This function is used for implementing the T% elaborator.

Equations

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

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 should be fast enough to always run. The search can be traced with set_option Elab.DiffGeo.TotalSpaceMk true.

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.isCLMReduciblyDefeqCoefficients (e : Lean.Expr) : Lean.Elab.TermElabM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

Check if an expression e is (after instantiating metavariables and performing whnf), a ContinuousLinearMap over an identity ring homomorphism and the coefficients of domain and codomain are reducibly definitionally equal. If so, we return the coefficient field, the domain and the codomain of the continuous linear maps (otherwise none).

Equations

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

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
• the model with corners on the tangent space of a manifold
• a model with corners on a manifold, or on its underlying model space
• a closed interval of real numbers (including the unit interval)
• Euclidean space, Euclidean half-space and Euclidean quadrants
• a metric sphere in a real or complex inner product space
• the units of a normed algebra
• the complex upper half plane
• a space of continuous k-linear maps
• 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.

Note that the matching on e does not see through reducibility (e.g. we distinguish the abbrev TangentBundle from its definition), so whnfR should not be run on e prior to calling findModel on it.

This implementation is not maximally robust yet.

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.

def Manifold.«termHasMFDerivAt[_]______» : Lean.ParserDescr

HasMFDerivAt[s] f x f' elaborates to HasMFDerivWithinAt I J f s x 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.«termHasMFDerivAt%______» : Lean.ParserDescr

HasMFDerivAt% f x f' elaborates to HasMFDerivAt I J f x f', 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.