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