FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013)

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 6 definitions, 12 theorems, 9 propositions, 2 lemmas, 2 corollaries, 9 examples and 2 conventions.

Of the 42 statements checked against Lean, 7 are formalized somewhere and 35 are not.

Status	Statements	Share	What it means
not formalized	35	83%	A documented search found no Lean statement of it anywhere.
in Mathlib	7	17%	Mathlib states and proves it.
checked in total	42

Which versions of Lean and Mathlib were searched

Canonical block: FC08-C21-U001–FC08-C21-U042, exactly 42 unique contiguous rows.
Search order: project A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0; Lean 4.33.0), current H=5315eef9e4ffb98e0f89f278b765c50a149f66ca (Apache-2.0; Lean 4.34.0-rc2), then indexed/current/external Lean search.
Result: 7 pinned mathlib rows and 35 dated unmatched rows. Positives: U001, U002, U005, U006, U021, U029, U030.
The topological action layer is strong: MulAction.orbitRel gives orbit equivalence/classes; the orbit quotient has the quotient topology and an open quotient map; ProperSMul is exactly Lee’s proper-action definition; and proper actions have Hausdorff orbit quotient. These own U001, U002, U005, U006.
U021 is the exact underlying coset-space convention: G ⧸ H is the left-coset quotient, leftRel_apply gives g₁⁻¹g₂ ∈ H, and the topology is quotient topology.
U029–U030 are exact abstract group theory: quotient by a normal subgroup, canonical surjection/kernel, and the first isomorphism theorem.
Mathlib also contains useful proper-action compact-set results and topological quotient-covering machinery, but not Lee’s smooth quotient-manifold theorem/unique smooth structure/submersion. These are not promoted into U007–U018.
No homogeneous-space quotient-manifold construction, Lie-group quotient theorem/first-isomorphism theorem, or Lie-correspondence classification was found. Connectivity searches likewise did not locate the bundled SO/U/SU/GL component results.
N=2026-09-07 marks negative decisions; strict whole-row semantics apply uniformly.

Convention/notation — orbit space of the action

FC08-C21-U001 · Ch. 21, § Quotients of Manifolds by Group Actions; source L16299 · in Mathlib

are given an action of a group G on a topological space M; which we write either as \(\theta \colon G \times M \to M\) or as \(( g , p ) \mapsto g \cdot p\) . (For definiteness, let us assume that \(G\) acts on the left; similar considerations apply to right actions.) Recall that the orbit of a point \(p \in M\) is the set of images of \(p\) under all elements of the group: \[ G \cdot p = \{g \cdot p: g \in G \}. \] Define a relation on M by setting \(p \sim q\) if there exists \(g \in G\) such that \(g \cdot p = q\) This is an equivalence relation, whose equivalence classes are exactly the orbits of G in M . The set of orbits is denoted by \(M / G\) ; with the quotient topology it is called the orbit space of the action. It is of great importance to determine conditions under which an orbit space is a smooth manifold. It is important to be aware that some authors use the notation \(G \backslash M\) for an orbit space determined by a left action of G on M; reserving \(M / G\) for one determined by a right action. We use only the latter notation, relying on the context, not the notation, to distinguish between the two cases.

Formalized. Mathlib/GroupTheory/GroupAction/Defs.lean::MulAction.orbitRel, MulAction.orbitRel_apply, MulAction.orbitRel.Quotient, MulAction.orbitRel.Quotient.orbit_mk; Mathlib/Topology/Algebra/ConstMulAction.lean::MulAction.isOpenQuotientMap_quotientMk — orbitRel is exactly the equivalence relation generated by lying in the same orbit; its quotient is the orbit set, orbit_mk identifies a class with the corresponding orbit, and isOpenQuotientMap_quotientMk supplies the quotient topology/map.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Lemma 21.1

FC08-C21-U002 · Ch. 21, § Quotients of Manifolds by Group Actions; source L16311 · in Mathlib

Lemma 21.1. For any continuous action of a topological group G on a topological space M; the quotient map \(\pi \colon M \to M / G\) is an open map.

Formalized. Mathlib/Topology/Algebra/ConstMulAction.lean::MulAction.isOpenMap_quotient_mk'_mul — For a continuous group action, Mathlib proves directly that the quotient map to the orbit-relation quotient is open.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Example 21.2

FC08-C21-U003 · Ch. 21, § Quotients of Manifolds by Group Actions; source L16323 · after FC08-C05-U043 · not formalized

(Orbit Spaces of Smooth Lie Group Actions). (a) For the trivial action of a group \(G\) on a smooth manifold \(M\), the orbits are points and \(M/G = M\). (b) \(\mathbb{R}^{k}\) acts on \(\mathbb{R}^{k} \times \mathbb{R}^{n}\) by translation in the first factor, \(v \cdot (x,y) = (v+x,\ y)\), and the quotient map \(\pi \colon \mathbb{R}^{k} \times \mathbb{R}^{n} \to \mathbb{R}^{n}\) is a smooth submersion. (c) The circle group \(\mathbb{S}^{1}\) acts on \(\mathbb{C}\) by complex multiplication, \(z \cdot w = zw\); the orbits are the circles centered at the origin together with \(\{0\}\), and the orbit space is not a manifold. (d) The natural action of \(\mathrm{GL}(n,\mathbb{R})\) on \(\mathbb{R}^{n}\) has an orbit space that is not even Hausdorff. (e) Restricting that action gives a smooth action of \(\mathrm{O}(n)\) on \(\mathbb{R}^{n}\) whose orbit space is homeomorphic to \([0,\infty)\): for nonzero \(v, v'\) of equal norm, completing \(v/|v|\) and \(v'/|v'|\) to orthonormal bases and taking the orthogonal matrices \(A\), \(A'\) with those columns, \(A'A^{-1}\) carries \(v\) to \(v'\). (f) Deleting the origin makes all three orbit spaces manifolds: \((\mathbb{C} \setminus \{0\})/\mathbb{S}^{1}\) and \((\mathbb{R}^{n} \setminus \{0\})/\mathrm{O}(n)\) are homeomorphic to \(\mathbb{R}^{+}\), and \((\mathbb{R}^{n} \setminus \{0\})/\mathrm{GL}(n,\mathbb{R})\) is a point. (g) Restricting further gives an action of \(\mathrm{O}(n)\) on \(\mathbb{S}^{n-1}\), smooth by Corollary 5.30 since \(\mathbb{S}^{n-1}\) is an embedded submanifold of \(\mathbb{R}^{n}\).

Not formalized. none; no complete checked declaration under strict bundle semantics — The source row is a bundled family of concrete orbit-space examples/pathologies; no single checked declaration owns all examples and identifications. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Example 21.3

FC08-C21-U004 · Ch. 21, § Quotients of Manifolds by Group Actions; source L16341 · after FC08-C04-U020 · not formalized

Let \(\alpha\) be irrational and let \(\mathbb{R}\) act on \(\mathbb{T}^{2} = \mathbb{S}^{1} \times \mathbb{S}^{1}\) by \(t \cdot (w,z) = (e^{2\pi i t}w,\ e^{2\pi i \alpha t}z)\). This action is smooth, and the arguments of Example 4.20 adapt to show it is free with dense orbits. Hence the only saturated open subsets of \(\mathbb{T}^{2}\) are \(\emptyset\) and \(\mathbb{T}^{2}\), so \(\mathbb{T}^{2}/\mathbb{R}\) has the trivial topology: not Hausdorff, and not a manifold.

Definition/convention — a proper action

FC08-C21-U005 · Ch. 21, § Quotients of Manifolds by Group Actions; source L16349 · in Mathlib

To avoid pathological cases such as these, we need to introduce one more restriction on our group actions. A continuous left action of a Lie group G on a manifold M is said to be a proper action if the map \(G \times M \to M \times M\) given by \(( g , p ) \mapsto ( g \cdot p , p )\) is a proper map. Note that this is generally a weaker condition than requiring that the map \(G \times M \to M\) defining the action be a proper map (see Problem 21-1).

Formalized. Mathlib/Topology/Algebra/ProperAction/Basic.lean::ProperSMul, ProperSMul.isProperMap_smul_pair — ProperSMul G X is defined exactly by properness of (g,x) ↦ (g • x,x), Lee’s definition of a proper action.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Proposition 21.4

FC08-C21-U006 · Ch. 21, § Quotients of Manifolds by Group Actions; source L16351 · in Mathlib

Proposition 21.4. If a Lie group acts continuously and properly on a manifold, then the orbit space is Hausdorff. P

Formalized. Mathlib/Topology/Algebra/ProperAction/Basic.lean::t2Space_quotient_mulAction_of_properSMul — Mathlib proves directly that the orbit quotient of a proper action is T2/Hausdorff, exactly the proposition.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Proposition 21.5

FC08-C21-U007 · Ch. 21, § Quotients of Manifolds by Group Actions; source L16363 · not formalized

Proposition 21.5 (Characterizations of Proper Actions). Let M be a manifold, and let G be a Lie group acting continuously on M . The following are equivalent. (a) The action is proper. (b) \(I f ( p _ { i } )\) is a sequence in M and \(( g _ { i } )\) is a sequence in G such that both \(\left( { { p } _ { i } } \right)\) and \(( g _ { i } \cdot p _ { i } )\) converge, then a subsequence \(o f ( g _ { i } )\) converges. (c) For every compact subset \(K \subseteq M\) ; the set \(G _ { K } = \{ g \in G \colon ( g \cdot K ) \cap K \neq \emptyset \}\)

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has the exact proper-action predicate, Hausdorff quotient theorem, and compact-set consequences, but no one checked theorem packages Lee’s sequential characterization and all orbit/isotropy conclusions in this row; deriving the missing clauses would be reconstruction. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Corollary 21.6

FC08-C21-U008 · Ch. 21, § Quotients of Manifolds by Group Actions; source L16385 · not formalized

Corollary 21.6. Every continuous action by a compact Lie group on a manifold is proper.

Proposition 21.7

FC08-C21-U009 · Ch. 21, § Quotients of Manifolds by Group Actions; source L16389 · not formalized

Proposition 21.7 (Orbits of Proper Actions). Suppose is a proper smooth action of a Lie group G on a smooth manifold M . For any point \(p \in M\) ; the orbit map \(\theta ^ { ( p ) } \colon G \to M\) is a proper map, and thus the orbit \(G \cdot p = \theta ^ { ( p ) } ( G )\) is closed in M . If in addition \(G _ { p } = \{ e \}\) , then \(\theta ^ { ( p ) }\) is a smooth embedding, and the orbit is a properly embedded submanifold.

Corollary 21.8

FC08-C21-U010 · Ch. 21, § Quotients of Manifolds by Group Actions; source L16395 · not formalized

Corollary 21.8. If a Lie group G acts properly on a manifold M; then each orbit is a closed subset of M; and each isotropy group is compact. P

Example 21.9

FC08-C21-U011 · Ch. 21, § Quotients of Manifolds by Group Actions; source L16399 · not formalized

Example 21.9. We can see in two ways that the action of \(\mathbb { R } ^ { + }\) on \(\mathbb { R } ^ { n }\) given by \[ t \cdot (x ^ {1}, \ldots , x ^ {n}) = (t x ^ {1}, \ldots , t x ^ {n})\tag{21.1} \] is not proper: the isotropy group of the origin is all of \(\mathbb { R } ^ { + }\) , which is not compact; and the orbits of other points are open rays, which are not closed.

Theorem 21.10

FC08-C21-U012 · Ch. 21, § The Quotient Manifold Theorem; source L16411 · not formalized

Theorem 21.10 (Quotient Manifold Theorem). Suppose G is a Lie group acting smoothly, freely, and properly on a smooth manifold M . Then the orbit space \(M / G\) is a topological manifold of dimension equal to dim M dim G, and has a unique smooth structure with the property that the quotient map \(M \to M / G\) is a smooth submersion.

Not formalized. none; no complete checked declaration under strict bundle semantics — P/H have topological orbit quotients and quotient-covering machinery for properly discontinuous actions, but no smooth quotient-manifold theorem constructing the unique smooth structure/submersion or Lee’s complete smooth covering-manifold statements. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Proposition 4.40

FC08-C21-U013 · Ch. 21, § Covering Manifolds; source L16468 · after FC08-C07-U033 · not formalized

Thus we are back in the situation of the preceding paragraph, and the two charts are smoothly compatible. ## Covering Manifolds Proposition 4.40 showed that any covering space of a smooth manifold is itself a smooth manifold. It is often important to know when a space covered \(b y\) a smooth manifold is itself a smooth manifold. To understand the answer to this question, we need to study the action on a covering space by the automorphism group of the covering. We saw in Chapter 7 (Proposition 7.23) that for any smooth covering \(E \to M\) ; the automorphism group is a discrete Lie group acting smoothly and freely on the covering space E. Below, we will show that the action is also proper. Before proceeding, it is useful to have an alternative characterization of properness for free actions of discrete Lie groups.

Lemma 21.11

FC08-C21-U014 · Ch. 21, § Covering Manifolds; source L16470 · not formalized

Lemma 21.11. Suppose a discrete Lie group acts continuously and freely on a manifold E. The action is proper if and only if the following conditions both hold: (i) Every point \(p \in E\) has a neighborhood U such that for each \(g \in T , ( g \cdot U ) \cap\) \(U = \varnothing\) unless \(g = e\) (ii) \(H p , p ^ { \prime } \in E\) are not in the same -orbit, there exist neighborhoods V of p and \(V ^ { \prime } o f p ^ { \prime }\) such that \(( g \cdot V ) \cap V ^ { \prime } = \emptyset\) for all \(g \in T\) Proof. First, suppose that the action is free and proper, and let \(\pi \colon E \to E / F\) denote the quotient map. By Proposition 21.4, \(E / { \cal { T } }\) is Hausdorff. If \(p , p ^ { \prime } \in E\)

Definition/convention — properly discontinuous

FC08-C21-U015 · Ch. 21, § Covering Manifolds; source L16488 · not formalized

By Proposition 21.5(b), the action is proper. In the literature, a continuous discrete group action satisfying condition (i) of this lemma (or conditions (i) and (ii), or something closely related to them) has traditionally been called properly discontinuous. We avoid this terminology, because its meaning is not universally agreed upon, and because it leads to such oxymoronic expressions as “continuous properly discontinuous actions.” Instead, following Allan Hatcher [Hat02], we call a continuous action satisfying (i) a covering space action, and simply refer to actions satisfying (i) and (ii) as “free and proper actions.” It can be shown that any covering space action on a topological space yields a covering map, though the quotient space need not be Hausdorff (see, e.g., [LeeTM, Chap. 12]). P

Proposition 21.12

FC08-C21-U016 · Ch. 21, § Covering Manifolds; source L16490 · not formalized

Let \(M\) be a smooth manifold and \(\pi \colon E \to M\) a smooth covering map. With the discrete topology, the automorphism group \(\operatorname{Aut}_{\pi}(E)\) acts smoothly, freely and properly on \(E\).

Theorem 21.13

FC08-C21-U017 · Ch. 21, § Covering Manifolds; source L16496 · not formalized

Theorem 21.13. Suppose E is a connected smooth manifold and is a discrete Lie group acting smoothly, freely, and properly on E. Then the orbit space \(E / { \cal { T } }\) is a topological manifold and has a unique smooth structure such that \(E \to E / { \cal { T } }\) is a smooth normal covering map.

Example 21.14

FC08-C21-U018 · Ch. 21, § Covering Manifolds; source L16514 · after FC08-C07-U031, FC08-C21-U007, FC08-C21-U017, FC08-C04-U033, FC08-C02-U015 · not formalized

(Proper Discrete Group Actions). (a) The discrete Lie group \(\mathbb{Z}^{n}\) acts smoothly and freely on \(\mathbb{R}^{n}\) by translations. The covering map \(\mathbb{R}^{n} \to \mathbb{T}^{n}\), \((x^{1},\dots,x^{n}) \mapsto (e^{2\pi i x^{1}},\dots,e^{2\pi i x^{n}})\), is a local diffeomorphism for the product smooth structure and makes the same identifications as \(\mathbb{R}^{n} \to \mathbb{R}^{n}/\mathbb{Z}^{n}\), so by Theorem 4.31 \(\mathbb{R}^{n}/\mathbb{Z}^{n}\) is diffeomorphic to \(\mathbb{T}^{n}\). (b) The two-element group \(\{\pm 1\}\) acts on \(\mathbb{S}^{n}\) by multiplication, and by Theorem 4.31 \(\mathbb{S}^{n}/\{\pm 1\}\) is diffeomorphic to \(\mathbb{RP}^{n}\).

Definition/convention — homogeneous G -space (

FC08-C21-U019 · Ch. 21, § Homogeneous Spaces; source L16522 · not formalized

diffeomorphic to \(\mathbb { R P } ^ { n }\) ## Homogeneous Spaces Some of the most interesting group action are transitive ones. A smooth manifold endowed with a transitive smooth action by a Lie group G is called a homogeneous G -space (or a homogeneous space or homogeneous manifold if it is not important to specify the group).

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has transitive actions, stabilizers, coset quotients, and Grassmannian algebraic/topological objects, but no homogeneous-space quotient-manifold theorem or smooth flag/Grassmannian construction matching the whole row. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Example 21.15

FC08-C21-U020 · Ch. 21, § Homogeneous Spaces; source L16528 · after FC08-C21-U003, FC08-C07-U044 · not formalized

(Homogeneous Spaces). (a) The natural action of \(\mathrm{O}(n)\) on \(\mathbb{S}^{n-1}\) is transitive, so \(\mathbb{S}^{n-1}\) is a homogeneous space of \(\mathrm{O}(n)\). (b) It restricts to a smooth action of \(\mathrm{SO}(n)\), so for \(n \geq 2\) the sphere is also a homogeneous space of \(\mathrm{SO}(n)\). (c) The Euclidean group \(\mathrm{E}(n)\) acts on \(\mathbb{R}^{n}\) by rigid motions, transitively since translations suffice, so \(\mathbb{R}^{n}\) is a homogeneous \(\mathrm{E}(n)\)-space. (d) \(\mathrm{SL}(2,\mathbb{R})\) acts smoothly and transitively on the upper half-plane \(\mathbb{U} = \{z \in \mathbb{C} : \operatorname{Im} z > 0\}\) by \[ \begin{pmatrix} a & b \\ c & d \end{pmatrix} \cdot z = \frac{az+b}{cz+d}, \] the resulting complex-analytic diffeomorphisms being the Möbius transformations. (e) For \(n \geq 1\) the natural action of \(\mathrm{GL}(n,\mathbb{C})\) on \(\mathbb{C}^{n}\) restricts to smooth actions of \(\mathrm{U}(n)\) and \(\mathrm{SU}(n)\) on \(\mathbb{S}^{2n-1}\), the unit vectors of \(\mathbb{C}^{n}\).

Convention/notation — left coset of H

FC08-C21-U021 · Ch. 21, § Homogeneous Spaces; source L16548 · in Mathlib

and that of \(\operatorname { S U } ( n )\) is transitive for all \(n \geq 2\) Next we describe a construction that can be used to generate a great number of homogeneous spaces, as quotients of Lie groups by closed subgroups. Let \(G\) be a Lie group and \(H \subseteq G\) be a Lie subgroup. A subset of \(G\) of the form \[ g H = \{g h: h \in H \} \] for some \(g \in G\) is called a left coset of H . The left cosets form a partition of \(G _ { : }\) and the quotient space determined by this partition (i.e., the set of left cosets with the quotient topology) is called the left coset space of G modulo H , and is denoted by \(G / H\) . Two elements \(g _ { 1 } , g _ { 2 } \in G\) are in the same left coset of H if and only if \(g _ { 1 } ^ { - 1 } g _ { 2 } \in H\) ; in this case we write \(g _ { 1 } \equiv g _ { 2 }\) .mod H / and say \(g _ { 1 }\) and \(g _ { 2 }\) are congruent modulo \(H\).

Formalized. Mathlib/GroupTheory/Coset/Defs.lean::QuotientGroup.leftRel_apply, instHasQuotientSubgroup; Mathlib/Topology/Algebra/Group/Quotient.lean::QuotientGroup.instTopologicalSpace, QuotientGroup.isQuotientMap_mk — G ⧸ H is the quotient by the left-coset relation, leftRel_apply is exactly g₁⁻¹g₂ ∈ H, and the quotient carries the quotient topology. This realizes Lee’s left-coset-space convention.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Theorem 21.17

FC08-C21-U022 · Ch. 21, § Homogeneous Spaces; source L16556 · not formalized

Theorem 21.17 (Homogeneous Space Construction Theorem). Let G be a Lie group and let H be a closed subgroup of G. The left coset space \(G / H\) is a topological manifold of dimension equal to dim G dim H , and has a unique smooth structure such that the quotient map \(G \to G / H\) is a smooth submersion. The left action of G on G=H given by \[ g _ {1} \cdot (g _ {2} H) = (g _ {1} g _ {2}) H\tag{21.3} \] turns \(G / H\) into a homogeneous G-space.

Theorem 21.18

FC08-C21-U023 · Ch. 21, § Homogeneous Spaces; source L16578 · not formalized

Theorem 21.18 (Homogeneous Space Characterization Theorem). Let G be a Lie group, let M be a homogeneous G-space, and let p be any point of M . The isotropy group \(G _ { p }\) is a closed subgroup of G, and the map \(F \colon G / G _ { p } \to M\) defined by \(F ( g G _ { p } ) = g \cdot p\) is an equivariant diffeomorphism.

Definition/convention — homogeneous space to be a quotient manifold of the form G / H

FC08-C21-U024 · Ch. 21, § Homogeneous Spaces; source L16600 · not formalized

Because of this identification, some authors define a homogeneous space to be a quotient manifold of the form \(G / H\) , where G is a Lie group and H is a closed subgroup of G. One advantage of that definition is that it makes explicit the intimate relationship between the homogeneous space and the Lie group that acts transitively on it. However, a disadvantage is that it suggests there is something special about the identity coset of H (the image of \(e \in G\) under the quotient map), while the essence of homogeneous spaces is that every point “looks the same” as every other.

Example 21.19

FC08-C21-U025 · Ch. 21, § Homogeneous Spaces; source L16604 · not formalized

(Homogeneous Spaces Revisited). (a) For the natural action of \(\mathrm{O}(n)\) on \(\mathbb{S}^{n-1}\), the sphere is diffeomorphic to \(\mathrm{O}(n)/\mathrm{O}(n-1)\). (b) For \(\mathrm{SO}(n)\) the isotropy group is \(\mathrm{SO}(n-1)\), so \(\mathbb{S}^{n-1} \approx \mathrm{SO}(n)/\mathrm{SO}(n-1)\) for \(n \geq 2\). (c) Since \(\mathrm{E}(n)\) acts smoothly and transitively on \(\mathbb{R}^{n}\) with isotropy group \(\mathrm{O}(n)\) at the origin, \(\mathbb{R}^{n} \approx \mathrm{E}(n)/\mathrm{O}(n)\). (d) For the transitive action of \(\mathrm{SL}(2,\mathbb{R})\) on the upper half-plane the isotropy group is \(\mathrm{SO}(2)\), so \(\mathbb{U} \approx \mathrm{SL}(2,\mathbb{R})/\mathrm{SO}(2)\). (e) By Exercise 21.16, \(\mathbb{S}^{2n-1} \approx \mathrm{U}(n)/\mathrm{U}(n-1)\) for \(n \geq 1\) and \(\mathbb{S}^{2n-1} \approx \mathrm{SU}(n)/\mathrm{SU}(n-1)\) for \(n \geq 2\).

Theorem 21.20

FC08-C21-U026 · Ch. 21, § Sets with Transitive Group Actions; source L16622 · not formalized

Theorem 21.20. Suppose X is a set, and we are given a transitive action of a Lie group \(G\) on X such that for some point \(p \in X\) , the isotropy group \(G _ { p }\) is closed in G. Then X has a unique smooth manifold structure with respect to which the given action is smooth. With this structure, dim \(X = \dim G - \dim G _ { p }\)

Example 21.21

FC08-C21-U027 · Ch. 21, § Sets with Transitive Group Actions; source L16628 · after FC08-C01-U048 · not formalized

(Grassmannians). Let \(G_{k}(\mathbb{R}^{n})\) denote the Grassmannian of \(k\)-dimensional subspaces of \(\mathbb{R}^{n}\), as in Example 1.36. It has a unique smooth manifold structure making the natural \(\mathrm{GL}(n,\mathbb{R})\) action smooth, and Problem 21-12 shows this is the structure defined in Example 1.36.

Example 21.22

FC08-C21-U028 · Ch. 21, § Sets with Transitive Group Actions; source L16636 · not formalized

Example 21.22 (Flag Manifolds). Let V be a real vector space of dimension \(n > 1\) and let \(K = ( k _ { 1 } , \ldots , k _ { m } )\) be a finite sequence of integers satisfying \(0 < k _ { 1 } < \cdots <\) \(k _ { m } < n\) . A flag in V of type K is a nested sequence of linear subspaces \(S _ { 1 } \subseteq S _ { 2 } \subseteq\) \(\cdots \subseteq S _ { m } \subseteq V\) , with dim \(S _ { i } = k _ { i }\) for each i. The set of all flags of type K in V is denoted by \(\operatorname { F } _ { K } ( V )\) . (For example, if \(K = ( k )\) , then \(\mathrm { F } _ { K } ( V )\) is the Grassmannian \(\mathrm { G } _ { k } ( V ) . )\) It is not hard to show that GL.V / acts transitively on \(\operatorname { F } _ { K } ( V )\) with a closed subgroup as isotropy group (see Problem 21-16), so \(\mathrm { F } _ { K } ( V )\) has a unique smooth manifold structure making it into a homogeneous GL.V /-space. With this structure, \(\mathrm { F } _ { K } ( V )\) is called a flag manifold. ## Applications to Lie Theory The quotient manifold theorem has a wealth of applications to the theory of Lie groups. In this section we describe a few of them. ## Quotient

Theorem 21.23

FC08-C21-U029 · Ch. 21, § Quotient Groups; source L16646 · in Mathlib

Theorem 21.23 (Quotient Theorem for Abstract Groups). Suppose G is any group and \(K \subseteq G\) is a normal subgroup. Then the set \(G / K\) of left cosets is a group with multiplication given by \(( g _ { 1 } K ) ( g _ { 2 } K ) = ( g _ { 1 } g _ { 2 } ) K\) , and the projection \(\pi \colon G \to G / K\) sending each element of G to its coset is a surjective homomorphism whose kernel like an ordinary action, except that \(g \cdot x \left( \operatorname { o r } x \cdot g \right)\) is required to be defined only for \(( g , x )\) in a neighborhood of \(\{ e \} \times W\) in \(U \times W\) .

Formalized. Mathlib/GroupTheory/QuotientGroup/Defs.lean::QuotientGroup.Quotient.group, QuotientGroup.mk', QuotientGroup.mk'_surjective, QuotientGroup.ker_mk' — For a normal subgroup, Mathlib gives the quotient group structure and the canonical surjective homomorphism with kernel exactly the subgroup, matching the abstract quotient-group theorem.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Theorem 21.24

FC08-C21-U030 · Ch. 21, § Quotient Groups; source L16648 · in Mathlib

Theorem 21.24 (First Isomorphism Theorem for Abstract Groups). If G and H are groups and \(F \colon G \to H\) is a group homomorphism, then the kernel of F is a normal subgroup of G, the image of F is a subgroup of H , and F descends to a group isomorphism \({ \widetilde { F } } \colon G / \operatorname { K e r } F \to \operatorname { I m } F\) . If F is surje a smooth manifold restricts to a local action on any sufficiently small coordinate neighborhood.

Formalized. Mathlib/GroupTheory/QuotientGroup/Basic.lean::QuotientGroup.quotientKerEquivRange, QuotientGroup.quotientKerEquivOfSurjective — quotientKerEquivRange is the first isomorphism theorem G/ker f ≃* range f; the surjective specialization identifies the quotient with the target.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0

Theorem 21.26

FC08-C21-U031 · Ch. 21, § Quotient Groups; source L16654 · not formalized

Theorem 21.26 (Quotient Theorem for Lie Groups). Suppose G is a Lie group and \(K \subseteq G\) is a closed normal subgroup. Then \(G / K\) is a Lie group, and the quotient map \(\pi \colon G \to G / K\) is a surjective Lie group homomorphism whose kernel o-one correspondence between smooth right actions of local Lie groups on W and finite-dimensional Lie subalgebras of X.W /.

Not formalized. none; no complete checked declaration under strict bundle semantics — The abstract quotient-group layer is present, but P/H have no Lie-group quotient-manifold/first-isomorphism theorem, discrete Lie-subgroup theorem, or Lie-correspondence classification required by this row. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Theorem 21.27

FC08-C21-U032 · Ch. 21, § Quotient Groups; source L16658 · not formalized

Theorem 21.27 (First Isomorphism Theorem for Lie Groups). If \(F \colon G \to H\) is a Lie group homomorphism, then the kernel of F is a closed normal Lie subgroup \(o f G\) , the image of F has a unique smooth manifold structure making it into a Lie subgroup of H , and F descends to a Lie group isomorphism \({ \tilde { F } } \colon G / \operatorname { K e r } F \to \operatorname { I m } F\) If F is surjective, then G= Ker

Definition/convention — subgroup that

FC08-C21-U033 · Ch. 21, § Quotient Groups; source L16662 · not formalized

These results are particularly significant when we apply them to a discrete subgroup, that is, a subgroup that is a discrete space in the subspace topology.

Proposition 21.28

FC08-C21-U034 · Ch. 21, § Quotient Groups; source L16664 · not formalized

Every discrete subgroup of a Lie group is a closed Lie subgroup of dimension zero.

Theorem 21.29

FC08-C21-U035 · Ch. 21, § Quotient Groups; source L16674 · not formalized

Theorem 21.29 (Quotients of Lie Groups by Discrete Subgroups). \(_ { I f G }\) is a connected Lie group and \(T \subseteq G\) is a discrete subgroup, then \(G / { \cal { T } }\) is a smooth manifold and the quotient map \(\pi \colon G \to G / { \cal {Gamma } }\) is a smooth normal covering oint Representation).

Example 21.30

FC08-C21-U036 · Ch. 21, § Quotient Groups; source L16678 · not formalized

Let \(C\) be a cube centered at the origin in \(\mathbb{R}^{3}\). The orientation-preserving orthogonal transformations of \(\mathbb{R}^{3}\) taking \(C\) to itself form a finite subgroup \(\Gamma \subseteq \mathrm{SO}(3)\), and \(\mathrm{SO}(3)/\Gamma\) is a connected smooth 3-manifold with finite fundamental group whose universal covering space is \(\mathbb{S}^{3}\). The symmetry groups of the other regular polyhedra give similar examples.

Theorem 21.31

FC08-C21-U037 · Ch. 21, § Quotient Groups; source L16682 · not formalized

with discrete kernels. Theorem 21.31 (Homomorphisms with Discrete Kernels). Let G and H be connected Lie groups. For any Lie group homomorphism F \(G H\) , the following are equivalent: (a) F is surjective and has discrete kernel. (b) F is a smooth covering map. (c) F is a local diffeomorphism. (d) The induced homomorphism _ { * } \operatorname {

Theorem 21.32

FC08-C21-U038 · Ch. 21, § Quotient Groups; source L16700 · not formalized

Problem 21-22.) Theorem 21.32. Let g be a finite-dimensional Lie algebra. The connected Lie groups whose Lie algebras are isomorphic to g are (up to isomorphism) precisely those of the form \(G / { \cal { T } }\) , where G is the simply connected Lie group with Lie algebra g, and is a discrete normal subgroup of G.

Proposition 21.33

FC08-C21-U039 · Ch. 21, § Connectivity of Lie Groups; source L16708 · not formalized

Proposition 21.33. Suppose a topological group G acts continuously, freely, and properly on a topological space M . If G and \(M / G\) are connected, then M is connected.

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted P/H/current search found no theorem packaging Lee’s connectivity statements for these Lie groups or the connected-component classification of real GL(n); nearby general connectedness results are insufficient. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Proposition 21.34

FC08-C21-U040 · Ch. 21, § Connectivity of Lie Groups; source L16714 · not formalized

Proposition 21.34. For each \(n \geq 1\) , the Lie groups SO.n/, U.n/, and SU.n/ are connected. The group O.n/ has exactly two components, one of which is SO.n/.

Definition/convention — source terminology/construction

FC08-C21-U041 · Ch. 21, § Connectivity of Lie Groups; source L16720 · not formalized

Therefore, the components of \({ \mathrm { O } } ( n )\) are \(\mathrm { O } ^ { + } ( n )\) and \(0 ^ { - } ( n )\) . Determining the components of the general linear groups is a bit more involved. Let \({ \mathrm { G L } } ^ { + } ( n , \mathbb { R } )\) and \({ \mathrm { G L } } ^ { - } ( n , \mathbb { R } )\) denote the open subsets of \({ \mathrm { G L } } ( n , \mathbb { R } )\) consisting of matrices with positive determinant and negative determinant, respectively.

Proposition 21.35

FC08-C21-U042 · Ch. 21, § Connectivity of Lie Groups; source L16725 · not formalized

The connected components of \(\mathrm{GL}(n,\mathbb{R})\) are \(\mathrm{GL}^{+}(n,\mathbb{R})\) and \(\mathrm{GL}^{-}(n,\mathbb{R})\).