Lie

Results named in Tau Ceti's TauCeti.Geometry.Lie modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe closed-subgroup theorem, with its model space#

A closed subgroup of a finite-dimensional real Lie group carries embedded-Lie-subgroup data whose model vector space is the Lie algebra TauCeti.Lie.lieSubalgebraOfSubgroup of the subgroup.

TauCeti.Lie.nonempty_embeddedLieSubgroupData_lieSubalgebraOfSubgroup_of_isClosed.{u, v, w}
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type v} [TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {G : Type w} [TopologicalSpace G] [ChartedSpace H G] [Group G]
  [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G] {K : Subgroup G} (hK : IsClosed ↑K) :
  have x := ⋯;
  Nonempty
    (TauCeti.Lie.EmbeddedLieSubgroupData I K ↥(TauCeti.Lie.lieSubalgebraOfSubgroup K).toSubmodule)

Lean

Formalized in Tau Ceti as TauCeti.Lie.nonempty_embeddedLieSubgroupData_lieSubalgebraOfSubgroup_of_isClosed.

Sources

• Tau Ceti documentation: TauCeti.Lie.nonempty_embeddedLieSubgroupData_lieSubalgebraOfSubgroup_of_isClosed
• Source of TauCeti.Lie.nonempty_embeddedLieSubgroupData_lieSubalgebraOfSubgroup_of_isClosed in TauCeti/Geometry/Lie/Subgroup/Embedded.lean

LeanTauCeti.Lie.nonempty_embeddedLieSubgroupData_lieSubalgebraOfSubgroup_of_isClosed

Uses 3

Proof usesHadamard's identity in the algebra of smooth functions · Hadamard's lemma in coordinates · The inverse function theorem for manifolds

TheoremHunt's lemma#

For X and Y in the Lie algebra of a compact Lie group, some adjoint translate of X brackets to zero with Y.

LeftInvariantDerivation.exists_Ad_lie_eq_zero.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3}
  [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G]
  [T2Space G] [CompactSpace G] (X Y : LeftInvariantDerivation I G) :
  ∃ g, ⁅(TauCeti.Lie.Ad g) X, Y⁆ = 0

Lean

Formalized in Tau Ceti as LeftInvariantDerivation.exists_Ad_lie_eq_zero.

Sources

• Tau Ceti documentation: LeftInvariantDerivation.exists_Ad_lie_eq_zero
• Source of LeftInvariantDerivation.exists_Ad_lie_eq_zero in TauCeti/Geometry/Lie/Adjoint/InvariantForm.lean

LeanLeftInvariantDerivation.exists_Ad_lie_eq_zero

Uses 2

Proof usesHadamard's identity in the algebra of smooth functions · Hadamard's lemma in coordinates

TheoremKronecker's criterion#

lieExp X is a topological generator of a connected commutative Lie group if and only if Λ + ℤ X is dense in the Lie algebra, Λ the kernel of the exponential.

TauCeti.closedZpowers_lieExp_eq_top_iff.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {G : Type u_3}
  [TopologicalSpace G] [ChartedSpace H G] [Group G] [FiniteDimensional ℝ E] [LieGroup I (↑⊤) G]
  [T2Space G] [IsMulCommutative G] [IsTopologicalGroup G] [PreconnectedSpace G]
  (X : LeftInvariantDerivation I G) :
  TauCeti.closedZpowers (lieExp X) = ⊤ ↔
    Dense ↑(TauCeti.lieExpAddMonoidHom.ker ⊔ AddSubgroup.zmultiples X)

Lean

Formalized in Tau Ceti as TauCeti.closedZpowers_lieExp_eq_top_iff.

Sources

• Tau Ceti documentation: TauCeti.closedZpowers_lieExp_eq_top_iff
• Source of TauCeti.closedZpowers_lieExp_eq_top_iff in TauCeti/Geometry/Lie/Exponential/CommutativeGroup/Kronecker.lean

LeanTauCeti.closedZpowers_lieExp_eq_top_iff

Uses 2

Proof usesHadamard's identity in the algebra of smooth functions · Hadamard's lemma in coordinates

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.