Getting the manifold from a Lie group

Stream: maths

[Mr Proof]

Consider the equation

$$O(n+1)/O(n) \cong S^n$$

Here we are implicity treating O(n+1) as the manifold not the group. A lie group is a group as well as a manifold. But in Lean how might we cast from a Lie group to a manifold?

In everyday mathematics this notation is very ambiguous. e.g. O(5) can stand for a Lie group, a manifold, or a Lie algebra depending on context.

We need a "forgetful" operator which forgets that O(5) has group structure and treats it as a manifold. But there doesn't seem to be a notation for this in mathematics??? Do you know of a good notation for that?

[Yan Yablonovskiy 🇺🇦]

The reals are also an example of innumerably many structures, so you don't need to look this far. Generally this design consideration is covered here, including forgetfulness of functors:
https://leanprover-community.github.io/mathematics_in_lean/C08_Hierarchies.html

Partly sourced from : https://inria.hal.science/hal-02463336v2

[Michael Rothgang]

Short answer, I can say more next week: docs#LieGroup extends docs#IsManifold (transitively), so Lie groups are smooth manifolds by definition

[Mr Proof]

Michael Rothgang said:

Short answer, I can say more next week: docs#LieGroup extends docs#IsManifold (transitively), so Lie groups are smooth manifolds by definition

Yes, that's what it says in Wikipedia "A Lie group is a group that is also a differentiable manifold".

To me, this makes no sense. "A Lie group is a manifold equipped with a group structure" makes more sense.

To say a Lie Group "is" a manifold, seems to be extending the definition of manifold beyond it's original definition as a topological space.

True, we can say a cat wearing a hat is still a cat. But then is the cat wearing a different hat still the same cat? :smiley_cat:

I think that kind of language is a bit woolly. Even if it is the standard mathematical nomenclature.

Perhaps instead of "IsManifold", "HasManifoldStructure" is more apt. Which could be applied both to Lie groups and Manifolds.

[Jireh Loreaux]

No, we have a naming convention, to which we (attempt to) adhere. docs#IsManifold is a Prop-valued mixin, hence the Is prefix.

And besides, there's no reason for Mathlib to avoid standard mathematical nomenclature unnecessarily.

[Jireh Loreaux]

Mr Proof said:

Michael Rothgang said:

Short answer, I can say more next week: docs#LieGroup extends docs#IsManifold (transitively), so Lie groups are smooth manifolds by definition

True, we can say a cat wearing a hat is still a cat. But then is the cat wearing a different hat still the same cat? :smiley_cat:

Same cat, but a different cat-in-a-hat.