Basic facts about Lie groups

This file records lightweight consequences of the Lie-group regularity hierarchy.

Main results

• ModelWithCorners.t2Space_of_lieGroup: a Lie group modeled on a normed space is Hausdorff.
• LieGroup.minSmoothness_of_isRCLikeNormedField: over a field satisfying IsRCLikeNormedField, a Cⁿ Lie group is a C^(minSmoothness 𝕜 n) Lie group; Mathlib's tangent Lie algebra GroupLieAlgebra assumes regularity minSmoothness 𝕜 3.

theorem ModelWithCorners.t2Space_of_lieGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] (n : WithTop ℕ∞) [LieGroup I n G] : T2Space G

A Lie group modeled on a normed space is Hausdorff.

theorem LieGroup.minSmoothness_of_isRCLikeNormedField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4} [TopologicalSpace G] [ChartedSpace H G] [Group G] [IsRCLikeNormedField 𝕜] {n : WithTop ℕ∞} [LieGroup I n G] : LieGroup I (minSmoothness 𝕜 n) G

Over a field satisfying IsRCLikeNormedField, minSmoothness 𝕜 n = n, so a Cⁿ Lie group is a C^(minSmoothness 𝕜 n) Lie group. Mathlib's tangent Lie algebra GroupLieAlgebra assumes LieGroup I (minSmoothness 𝕜 3) G, which this supplies from LieGroup I 3 G. This theorem is deliberately not a global instance, so the downgrade applies only in files that opt in with attribute [local instance] LieGroup.minSmoothness_of_isRCLikeNormedField.