FormalConjecturesForMathlib.Geometry.Manifold.LieGroupPresentation

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import Mathlib.Geometry.Manifold.Algebra.LieGroup
public import Mathlib.Geometry.Manifold.Instances.Real
public import Mathlib.Topology.Algebra.ContinuousMonoidHom

Topological groups admitting a Lie group structure

A topological group G admits a Lie group structure if it is continuously isomorphic to a finite-dimensional real-analytic Lie group. Lie groups are Hausdorff but not assumed to be second countable: every discrete group is a 0-dimensional Lie group.

Main definitions

LieGroupPresentation G n: a continuous group isomorphism from G to an n-dimensional real-analytic Lie group.

AdmitsLieGroupStructure G: G has a LieGroupPresentation in some finite dimension.

Main results

admitsLieGroupStructure_of_lieGroup: a Hausdorff real-analytic Lie group admits a Lie group structure.

admitsLieGroupStructure_of_discreteTopology: a discrete group admits a Lie group structure.

AdmitsLieGroupStructure.locallyCompactSpace: a group admitting a Lie group structure is locally compact.

@[expose] public sectionopen scoped Manifold ContDiffuniverse uvariable {G : Type*} [Group G] [TopologicalSpace G]

A continuous group isomorphism from G to an n-dimensional real-analytic Lie group. The Lie group is not assumed to be second countable.

structure LieGroupPresentation (G : Type u) [TopologicalSpace G] [Group G] (n : ℕ) where
  carrier : Type u
  [topologicalSpace : TopologicalSpace carrier]
  [group : Group carrier]
  [t2Space : T2Space carrier]
  [chartedSpace : ChartedSpace (EuclideanSpace ℝ (Fin n)) carrier]
  [isManifold : IsManifold (𝓡 n) ω carrier]
  [lieGroup : LieGroup (𝓡 n) ω carrier]
  equiv : G ≃ₜ* carrier

A topological group admits a Lie group structure if it has a LieGroupPresentation in some finite dimension.

def AdmitsLieGroupStructure (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
  ∃ n, Nonempty (LieGroupPresentation G n)

Every Hausdorff finite-dimensional real-analytic Lie group admits a Lie group structure.

theorem admitsLieGroupStructure_of_lieGroup {n : ℕ} [T2Space G]
    [ChartedSpace (EuclideanSpace ℝ (Fin n)) G] [LieGroup (𝓡 n) ω G] :
    AdmitsLieGroupStructure G :=
  ⟨n, ⟨{ carrier := G, equiv := ContinuousMulEquiv.refl G }⟩⟩

Every discrete group is a 0-dimensional Lie group.

theorem admitsLieGroupStructure_of_discreteTopology [DiscreteTopology G] :
    AdmitsLieGroupStructure G := byG:Type u_1inst✝²:Group Ginst✝¹:TopologicalSpace Ginst✝:DiscreteTopology G⊢ AdmitsLieGroupStructure G
  let := ChartedSpace.ofDiscreteTopology (M := G) (H := EuclideanSpace ℝ (Fin 0))G:Type u_1inst✝²:Group Ginst✝¹:TopologicalSpace Ginst✝:DiscreteTopology Gthis:ChartedSpace (EuclideanSpace ℝ (Fin 0)) G := ChartedSpace.ofDiscreteTopology⊢ AdmitsLieGroupStructure G
  have := IsManifold.of_discreteTopology (𝕜 := ℝ) (M := G) (E := EuclideanSpace ℝ (Fin 0)) ωG:Type u_1inst✝²:Group Ginst✝¹:TopologicalSpace Ginst✝:DiscreteTopology Gthis✝:ChartedSpace (EuclideanSpace ℝ (Fin 0)) G := ChartedSpace.ofDiscreteTopologythis:IsManifold (𝓡 0) ω G⊢ AdmitsLieGroupStructure G
  have : LieGroup (𝓡 0) ω G :=
    { contMDiff_mul := contMDiff_of_discreteTopology
      contMDiff_inv := contMDiff_of_discreteTopology }G:Type u_1inst✝²:Group Ginst✝¹:TopologicalSpace Ginst✝:DiscreteTopology Gthis✝¹:ChartedSpace (EuclideanSpace ℝ (Fin 0)) G := ChartedSpace.ofDiscreteTopologythis✝:IsManifold (𝓡 0) ω Gthis:LieGroup (𝓡 0) ω G⊢ AdmitsLieGroupStructure G
  exact admitsLieGroupStructure_of_lieGroup (n := 0)All goals completed! 🐙

A group admitting a Lie group structure is locally compact.

theorem AdmitsLieGroupStructure.locallyCompactSpace (h : AdmitsLieGroupStructure G) :
    LocallyCompactSpace G := byG:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gh:AdmitsLieGroupStructure G⊢ LocallyCompactSpace G
  obtain ⟨k, ⟨p⟩⟩ := hG:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕp:LieGroupPresentation G k⊢ LocallyCompactSpace G
  let := p.topologicalSpaceG:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕp:LieGroupPresentation G kthis:TopologicalSpace p.carrier := p.topologicalSpace⊢ LocallyCompactSpace G
  let := p.groupG:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕp:LieGroupPresentation G kthis✝:TopologicalSpace p.carrier := p.topologicalSpacethis:Group p.carrier := p.group⊢ LocallyCompactSpace G
  let := p.chartedSpaceG:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕp:LieGroupPresentation G kthis✝¹:TopologicalSpace p.carrier := p.topologicalSpacethis✝:Group p.carrier := p.groupthis:ChartedSpace (EuclideanSpace ℝ (Fin k)) p.carrier := p.chartedSpace⊢ LocallyCompactSpace G
  have := (𝓡 k).locallyCompactSpaceG:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕp:LieGroupPresentation G kthis✝²:TopologicalSpace p.carrier := p.topologicalSpacethis✝¹:Group p.carrier := p.groupthis✝:ChartedSpace (EuclideanSpace ℝ (Fin k)) p.carrier := p.chartedSpacethis:LocallyCompactSpace (EuclideanSpace ℝ (Fin k))⊢ LocallyCompactSpace G
  have : LocallyCompactSpace p.carrier :=
    ChartedSpace.locallyCompactSpace (EuclideanSpace ℝ (Fin k)) p.carrierG:Type u_1inst✝¹:Group Ginst✝:TopologicalSpace Gk:ℕp:LieGroupPresentation G kthis✝³:TopologicalSpace p.carrier := p.topologicalSpacethis✝²:Group p.carrier := p.groupthis✝¹:ChartedSpace (EuclideanSpace ℝ (Fin k)) p.carrier := p.chartedSpacethis✝:LocallyCompactSpace (EuclideanSpace ℝ (Fin k))this:LocallyCompactSpace p.carrier⊢ LocallyCompactSpace G
  exact p.equiv.toHomeomorph.locallyCompactSpace_iff.mpr inferInstanceAll goals completed! 🐙