Connections with torsion (moving from sage to lean)

Stream: new members

[Dominic Steinitz]

Some years ago I wrote an example of an affine connection with torsion in sage manifolds: Mercator projection and connection with torsion on S2. I am currently trying to write an example of an Ehresmann connection on a principal bundle and find myself frustrated by sage's lack of types. How feasible would it be to "port" my Mercator example to Lean? I can give more details of my sage implementation if that would help (in summary I have a 2-sphere with the usual metric but with a connection in which straight lines on the mercator projection are really straight lines - this respects the metric but clearly is not the Levi-Civita connection which has great circles as straight lines - the straight lines with the Mercator connection are called loxodromes).

[Johan Commelin]

Mathlib knows about manifolds, the two sphere, vector bundles, the tangent bundle. But not about connections. Differential forms are in progress.

[Johan Commelin]

That's the short version of what is available.

[Johan Commelin]

So I think your project is missing some prerequisites, but isn't out of reach.

[Dominic Steinitz]

I am happy to contribute. I hope my 30 years in Haskell will allow me to. I think contributing to sage manifolds (written in python) would for me be a much harder proposition.

[Dominic Steinitz]

Johan Commelin said:

Mathlib knows about manifolds, the two sphere, vector bundles, the tangent bundle. But not about connections. Differential forms are in progress.

Differential forms are essential for what I want to do: an Ehresmann connection is a Lie algebra-valued 1-form on the principal bundle over a manifold (subject to conditions of course not every 1-form is a connection)

[Dominic Steinitz]

So I will need fibre bundles not just vector bundles.

[Dean Young]

@Dominic @Johan Commelin . Do you think one could parallelize connections and derivations? (d/D) (actional/unitial)

[Johan Commelin]

@Dominic fibre bundles are also in mathlib

[Dominic Steinitz]

Dean Young said:

Dominic Johan Commelin . Do you think one could parallelize connections and derivations? (d/D) (actional/unitial)

I don't know what parallelise means

[Dean Young]

@Dominic I think that the connections have an additive action from the derivations, which form an additive group.

"ℝⁿ is a (unitial) group with an operation (acting) additively on n-dimensional affine space". (unitial/actional)