Zulip Chat Archive

Stream: new members

Topic: Connections with torsion (moving from sage to lean)


Dominic Steinitz (Sep 12 2024 at 09:44):

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 (Sep 12 2024 at 09:46):

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

Johan Commelin (Sep 12 2024 at 09:46):

That's the short version of what is available.

Johan Commelin (Sep 12 2024 at 09:47):

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

Dominic Steinitz (Sep 12 2024 at 09:50):

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 (Sep 12 2024 at 09:58):

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 (Sep 12 2024 at 09:59):

So I will need fibre bundles not just vector bundles.

Dean Young (Sep 14 2024 at 00:17):

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

Johan Commelin (Sep 14 2024 at 04:39):

@Dominic fibre bundles are also in mathlib

Dominic Steinitz (Sep 14 2024 at 11:33):

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 (Sep 14 2024 at 23:46):

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


Last updated: May 02 2025 at 03:31 UTC