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.

Inferring models with corners supports all current ModelWithCorners instances in mathlib. This will need to be updated as new instances are added.

For products of manifolds, we explicitly track if the resulting space is a product of normed spaces: that case is ambiguous, and the elaborators 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). If we encounter such an ambiguity, we warn about it and do not infer a model with corners.

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

TODO

• try an opinionated strategy on products of normed spaces: is one guess correct more often than the other?
• alternatively, can the elaborator generate two Try this suggestions, corresponding to the possible options?
• not all those elaborators have corresponding delaborators yet, this should be fixed
• add elaborators for more notation
• make the model finding extensible, by converting it to an environment extension

If you would like to work on any of these, please coordinate with Michael Rothgang (@grunweg) to avoid duplicating or conflicting work.

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

structure Manifold.Elab.NormedSpaceInfo : Type

Captures information when a model with corners is the trivial model on a normed space (or on an inner product space, which is also a normed space): contains the expressions describing the normed space and its base field.

Searching for a model with corners will return an Option NormedSpaceInfo, which is some if and only if the trivial model on a normed space was found.

• normedSpace : Lean.Expr

  The expression for the normed space itself.

• baseField : Lean.Expr

  The expression for the normed space's base field.

def Manifold.Elab.instInhabitedNormedSpaceInfo.default : NormedSpaceInfo

Equations

• Manifold.Elab.instInhabitedNormedSpaceInfo.default = { normedSpace := default, baseField := default }

@[implicit_reducible]

instance Manifold.Elab.instInhabitedNormedSpaceInfo : Inhabited NormedSpaceInfo

Equations

• Manifold.Elab.instInhabitedNormedSpaceInfo = { default := Manifold.Elab.instInhabitedNormedSpaceInfo.default }

structure Manifold.Elab.FindModelResult : Type

Information about a model with corners found through findModelInner. It includes the model with corners found, and, if this model is the trivial model with corners on a normed space, information about that normed space. (Knowing this is important for forming products of models.)

Most search results are not a model with corners for a normed space, so an Expr representing the model with corners may be coerced directly to this type.

• model : Lean.Expr

  Expression describing the model with corners found.

• normedSpaceInfo? : Option NormedSpaceInfo

  Information on the underlying normed space, if this model is the trivial model with corners on a normed space.

def Manifold.Elab.instInhabitedFindModelResult.default : FindModelResult

Equations

• Manifold.Elab.instInhabitedFindModelResult.default = { model := default, normedSpaceInfo? := default }

@[implicit_reducible]

instance Manifold.Elab.instInhabitedFindModelResult : Inhabited FindModelResult

Equations

• Manifold.Elab.instInhabitedFindModelResult = { default := Manifold.Elab.instInhabitedFindModelResult.default }

@[implicit_reducible]

instance Manifold.Elab.instCoeExprFindModelResult : Coe Lean.Expr FindModelResult

Equations

• Manifold.Elab.instCoeExprFindModelResult = { coe := fun (model : Lean.Expr) => { model := model } }

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

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. This method intentionally handles neither sums (disjoint unions) nor products of spaces, nor an open subset of an existing manifold. These are handled in findModel.

Return an expression describing the found model with corners, together with information about whether the model is the trivial model with corners on a normed space. (This is important for forming products of models.)

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.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 all ModelWithCorners instances that are currently defined in mathlib. 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.

Delaborators

In this section we make sure the info view also uses those notations. Not all notations are supported so far.

def delabTotalSpace_mk : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for Bundle.TotalSpace.mk using anonymous constructor notation.

Equations

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

def delabTotalSpace_mk' : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for Bundle.TotalSpace.mk' using anonymous constructor notation.

Equations

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

def delab_mfderiv : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for mfderiv using the custom elaborator, and special-casing arguments that can use the T% elaborator.

Equations

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

def delabMDifferentiableAt : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for MDifferentiableAt using the custom elaborator, and special-casing arguments that can use the T% elaborator.

Equations

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

def delabMDifferentiableWithinAt : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for MDifferentiableWithinAt using the custom elaborator, and special-casing arguments that can use the T% elaborator.

Equations

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