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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 16 definitions, 6 theorems, 10 propositions, 1 lemma, 1 corollary, 13 examples, 2 constructions and 2 conventions.

Of the 51 statements checked against Lean, 10 are formalized somewhere and 41 are not.

Status	Statements	Share	What it means
not formalized	41	80%	A documented search found no Lean statement of it anywhere.
in Mathlib	10	20%	Mathlib states and proves it.
checked in total	51

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 7, FC08-C07-U001–FC08-C07-U051, exactly 51 unique contiguous rows retrieved from FC08 — John M. Lee, Introduction to Smooth Manifolds through agent-memory.
Search order followed the Sweep-II plan: project source first at A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean 4.33.0), current upstream Mathlib H=5315eef9e4ffb98e0f89f278b765c50a149f66ca (Apache-2.0, Lean 4.34.0-rc2), then targeted indexed/current/external Lean searches. No project-existing, package-import, or reference-port C07 owner survived strict whole-row checking.
C07 has 10 pinned mathlib rows and 41 dated unmatched rows. Positive rows are: U001, U005, U016, U018, U025, U026, U029, U030, U034, U037.
/tmp/fc08-c07-witness.lean compiled through the project toolchain. It checks every positive interface and, for U037, proves definitionally that MulAction.orbit G p is the range of the orbit map g ↦ g • p and that MulAction.stabilizer G p is exactly the preimage of p. The witness is audit evidence only, not project source.
U001 is directly Mathlib’s LieGroup: LieGroup I ∞ G extends ContMDiffMul, which extends IsManifold, and adds smooth inversion. Mathlib is more general about models with corners; Lee’s finite-dimensional real boundaryless convention is obtained by specializing the model, not by changing the operational definition.
U005 is directly represented by ContMDiffMonoidMorphism in the group case, plus Diffeomorph for the isomorphism condition; generic MonoidHom.inverse proves the inverse of a bijective group homomorphism is again a homomorphism. U009 is nevertheless unmatched because the nontrivial theorem that a bijective smooth homomorphism has smooth inverse is not present.
U016 and U018 are generic group/topological-group interfaces: Subgroup.closure is the subgroup generated by a set and Subgroup.connectedComponentOfOne is the identity component. The stronger Lie-group neighborhood-generation and identity-component structure theorems U017/U019 were not inferred from these primitives.
U025, U026, U029, U030, U034, and U037 are direct action-theory interfaces: MulAction, ContinuousSMul/ContMDiffSMul, IsPretransitive, IsCancelSMul, MulActionHom, and orbit/stabilizer. Right actions/equivariance are represented equivalently as left actions of the opposite group. U027 remains unmatched because it is a source-specific left/right notation convention rather than this semantic interface.
The decisive missing geometric layer begins with U008 and U013. P/H have no Lie-group constant-rank theorem, LieSubgroup/embedded-Lie-subgroup object, closed-subgroup theorem, or universal-covering-Lie-group construction. This matches the C05 finding that Mathlib still lacks a general embedded/immersed-submanifold package. Consequently U008–U015 and U019–U024 cannot be promoted from their algebraic/topological ingredients.
The same boundary controls U036/U038: equivariance and orbit/stabilizer are formalized, but the Equivariant Rank Theorem and its constant-rank/Lie-subgroup/immersed-orbit consequences are not. Algebraic matrix groups exist for U039–U042, but their complete smooth Lie-subgroup examples and stated manifold properties are not bundled.
Mathlib/GroupTheory/SemidirectProduct.lean exactly supplies the algebraic semidirect-product carrier, multiplication, inclusions, projection, and complementary-subgroup isomorphisms. No checked P/H interface upgrades a smooth automorphism action to Lee’s semidirect-product Lie group or proves the closed Lie-subgroup/internal-product assertions, so U043–U047 remain unmatched under whole-row semantics.
Mathlib’s Representation and project-local representation code are algebraic. P/H have no ContMDiffRepresentation/Lie-group-representation bundle or theorem relating smooth linear actions and smooth homomorphisms into GL(V), and U048 additionally depends on the missing Lie-subgroup image theorem. Thus U048–U051 remain unmatched.
Current upstream H was inspected without changing the pinned worktree. Targeted searches found no LieSubgroup, IsEmbeddedLieSubgroup, universal-covering-group, smooth Lie representation, Lie-group semidirect-product instance, or replacement for the missing rank/subgroup results. A current TauCeti Lie-groups roadmap independently lists the closed-subgroup theorem, simply-connected Lie-group covers, and related Lie-group structure as missing/upcoming; this was used only as secondary indexed evidence, not as a substitute for revision inspection.
Project-first search found specialized complex-torus Lie-group work and algebraic action/representation code, but no general C07 interface closing an otherwise unmatched row. The project and pinned Mathlib worktrees remained unmodified.
N=2026-09-07 marks a dated unmatched decision after the prescribed search layers. Strict whole-row semantics apply uniformly.

Definition/convention — Lie group

FC08-C07-U001 · Ch. 7, § Basic Definitions; source L4100 · in Mathlib

A Lie group is a smooth manifold $G$ (without boundary) that is also a group in the algebraic sense, such that the multiplication map $m \colon G \times G \to G$ and the inversion map $i \colon G \to G$, given by \[ m(g,h) = gh, \qquad i(g) = g^{-1}, \] are both smooth. A Lie group is in particular a topological group.

Formalized. Mathlib/Geometry/Manifold/Algebra/LieGroup.lean::LieGroup — LieGroup I ∞ G extends ContMDiffMul, which itself extends IsManifold, and adds smooth inversion; together with Group G this is exactly Lee’s group-plus-smooth-manifold compatibility. Mathlib permits models with corners, so Lee’s boundaryless finite-dimensional real convention is the corresponding specialization rather than an extra theorem.

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

Convention/notation — arbitrary Lie group

FC08-C07-U002 · Ch. 7, § Basic Definitions; source L4108 · not formalized

The group operation in an arbitrary Lie group is denoted by juxtaposition, except in certain abelian groups such as $\mathbb { R } ^ { n }$ in which the operation is usually written additively. It is traditional to denote the identity element of an arbitrary Lie group by the symbol e (for German Einselement, “unit element”), and we follow this convention, except in specific examples in which there are more common notations (such as $I _ { n }$ for the identity matrix in a matrix group, or 0 for the identity element in $\mathbb{R}^{n}$).

Not formalized. none; no complete checked declaration under strict bundle semantics — This row is a source notation convention (e, juxtaposition) rather than a mathematical interface. Mathlib uses 1 and *; no declaration owns Lee’s notation convention as a formal object. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Proposition 7.1

FC08-C07-U003 · Ch. 7, § Basic Definitions; source L4112 · not formalized

Proposition 7.1. If G is a smooth manifold with a group structure such that the map $G \times G \to G$ given by $( g , h ) \mapsto g h ^ { - 1 }$ is smooth, then G is a Lie group.

Not formalized. none; no complete checked declaration under strict bundle semantics — The checked Lie-group API proves smooth multiplication and inversion separately but has no theorem giving Lee’s one-map criterion from smoothness of (g,h) ↦ g*h⁻¹. Reconstructing inversion and multiplication from that map would be new proof work. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Example 7.3

FC08-C07-U004 · Ch. 7, § Basic Definitions; source L4130 · after FC08-C01-U038 · not formalized

(Lie Groups). Each of the following is a Lie group with the indicated operation. (a) The general linear group $\mathrm{GL}(n,\mathbb{R})$, the invertible real $n \times n$ matrices: multiplication is smooth because the entries of $AB$ are polynomials in those of $A$ and $B$. (b) $\mathrm{GL}^{+}(n,\mathbb{R})$, the matrices of positive determinant: since $\det(AB) = (\det A)(\det B)$ and $\det(A^{-1}) = 1/\det A$ it is a subgroup, and as the preimage of $(0,\infty)$ under $\det$ it is open, hence an $n^{2}$-dimensional manifold. (c) Any open subgroup $H \subseteq G$ of a Lie group, by the argument of (b). (d) The complex general linear group $\mathrm{GL}(n,\mathbb{C})$, an open submanifold of $M(n,\mathbb{C})$ and so a $2n^{2}$-dimensional manifold, since products and inverses are smooth in the real and imaginary parts of the entries. (e) $\mathrm{GL}(V)$, the invertible linear maps of a real or complex vector space $V$ to itself; its smooth structure is independent of the choice of basis. (f) $\mathbb{R}$ and $\mathbb{R}^{n}$ under addition, the coordinates of $x - y$ being linear in $(x,y)$. (g) Likewise $\mathbb{C}$ and $\mathbb{C}^{n}$ under addition. (h) $\mathbb{R}^{*}$, the nonzero reals under multiplication, a 1-dimensional Lie group — indeed $\mathrm{GL}(1,\mathbb{R})$ — with $\mathbb{R}^{+}$ an open subgroup. (i) $\mathbb{C}^{*}$, the nonzero complex numbers, 2-dimensional, identified with $\mathrm{GL}(1,\mathbb{C})$. (j) The circle $\mathbb{S}^{1} \subseteq \mathbb{C}^{*}$ under complex multiplication: in angle coordinates multiplication and inversion read $(\theta_{1},\theta_{2}) \mapsto \theta_{1} + \theta_{2}$ and $\theta \mapsto -\theta$, so $\mathbb{S}^{1}$ is a Lie group, the circle group. (k) The direct product $G_{1} \times \cdots \times G_{k}$ of Lie groups, with componentwise multiplication $(g_{1},\dots,g_{k})(g'_{1},\dots,g'_{k}) = (g_{1}g'_{1},\dots,g_{k}g'_{k})$. (l) The $n$-torus $\mathbb{T}^{n} = \mathbb{S}^{1} \times \cdots \times \mathbb{S}^{1}$, an $n$-dimensional abelian Lie group. (m) Any group with the discrete topology is a topological group, and if finite or countable it is a zero-dimensional Lie group, a discrete Lie group.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has many individual group/manifold instances (products, normed spaces, units of normed algebras, matrix groups), and the project has complex tori as additive Lie groups, but no checked declaration owns this large multi-example bundle in full. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Definition/convention — Lie group isomorphism

FC08-C07-U005 · Ch. 7, § Lie Group Homomorphisms; source L4166 · in Mathlib

If G and H are Lie groups, a Lie group homomorphism from G to H is a smooth map $F \colon G \to H$ that is also a group homomorphism. It is called a Lie group isomorphism if it is also a diffeomorphism, which implies that it has an inverse that is also a Lie group homomorphism. In this case we say that G and H are isomorphic Lie groups. ##

Formalized. Mathlib/Geometry/Manifold/Algebra/Monoid.lean::ContMDiffMonoidMorphism; Mathlib/Geometry/Manifold/Diffeomorph.lean::Diffeomorph; Mathlib/Algebra/Group/Hom/Defs.lean::MonoidHom.inverse — For groups, ContMDiffMonoidMorphism I I′ ∞ G H is precisely a group homomorphism whose underlying map is smooth. Requiring the same underlying map to be a Diffeomorph is Lee’s Lie-group-isomorphism condition; MonoidHom.inverse records that the inverse of the resulting bijective group homomorphism is again a homomorphism.

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

Example 7.4

FC08-C07-U006 · Ch. 7, § Lie Group Homomorphisms; source L4168 · not formalized

Example 7.4 (Lie Group Homomorphisms). (a) The inclusion map $\mathbb { S } ^ { 1 } \hookrightarrow \mathbb { C } ^ { * }$ is a Lie group homomorphism. (b) Considering R as a Lie group under addition, and $\mathbb { R } ^ { * }$ as a Lie group under multiplication, the map exp $\mathbb { R } \to \mathbb { R } ^ { * }$ given by $\exp ( t ) = e ^ { t }$ is smooth, and is a Lie group homomorphism because $\overline { { e ^ { ( s + t ) } = e ^ { s } e ^ { t } } }$ The image of exp is the open subgroup $\mathbb { R } ^ { + }$ consisting of positive real numbers, and exp $\mathbb { R } \to \mathbb { R } ^ { + }$ is a Lie group isomorphism with inverse log $\mathbb { R } ^ { + } \to \mathbb { R }$ (c) Similarly, exp $\mathbb { C } \to \mathbb { C } ^ { * }$ given by $\exp ( z ) = e ^ { z }$ is a Lie group homomorphism. It is surjective but not injective, because its kernel consists of the complex numbers of the form $2 \pi i k$ , where k is an integer. (d) The map $\varepsilon \colon \mathbb { R } \to | \mathbb { S } ^ { 1 }$ defined by $\varepsilon ( t ) = e ^ { 2 \pi i t }$ is a Lie group homomorphism whose kernel is the set Z of integers. Similarly, the map $\varepsilon ^ { n } \colon \mathbb { R } ^ { n } \to \mathbb { T } ^ { n }$ defined by $\varepsilon ^ { n } ( x ^ { 1 } , \ldots , x ^ { n } ) = \left( e ^ { 2 \pi i x ^ { 1 } } , \ldots , e ^ { 2 \pi i x ^ { n } } \right)$ is a Lie group homomorphism whose kernel is $\mathbb { Z } ^ { n }$ (e) The determinant function det $\mathrm { G L } ( n , \mathbb { R } ) \to \mathbb { R } ^ { * }$ is smooth because det A is a polynomial in the matrix entries of A. It is a Lie group homomorphism because det $( A B ) = ( \operatorname* { d e t } A )$ .det B/. Similarly, det ${ \mathrm { G L } } ( n , \mathbb { C } ) \to \mathbb { C } ^ { * }$ is a Lie group homomorphism. (f) If G is a Lie group and $g \in G$ conjugation by g is the map $C _ { g } \colon G \to G$ given by $C _ { g } ( h ) = g h g ^ { - 1 }$ . Because group multiplication and inversion are smooth, $C _ { g }$ is smooth, and a simple computation shows that it is a group homomorphism.

Not formalized. none; no complete checked declaration under strict bundle semantics — The library contains individual exponential/determinant/conjugation maps and algebraic homomorphisms, but no one checked declaration or existing bundle establishes every homomorphism and smoothness claim in Lee’s multi-part example. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Definition/convention — normal subgroup

FC08-C07-U007 · Ch. 7, § Lie Group Homomorphisms; source L4180 · not formalized

If $G$ is a Lie group and $g \in G$, conjugation by $g$ is the map $C_{g} \colon G \to G$ given by $C_{g}(h) = ghg^{-1}$. It is smooth because multiplication and inversion are, it is a group homomorphism, and it is an isomorphism with inverse $C_{g^{-1}}$. A subgroup $H \subseteq G$ is normal if $C_{g}(H) = H$ for every $g \in G$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Subgroup.Normal and algebraic conjugation are formalized, and conjugation is constructibly smooth from Lie-group operations, but there is no existing bundled smooth conjugation Lie-group isomorphism owning the whole row. Strict mapping does not replace that missing interface by a new assembly proof. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Theorem 7.5

FC08-C07-U008 · Ch. 7, § Lie Group Homomorphisms; source L4184 · not formalized

homomorphisms. ## Theorem 7.5. Every Lie group homomorphism has constant rank.

Not formalized. none; no complete checked declaration under strict bundle semantics — No pinned/current theorem states that a smooth Lie-group homomorphism has constant manifold rank. This depends on the finite-dimensional equivariant/rank machinery that is absent from the checked manifold interface. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Corollary 7.6

FC08-C07-U009 · Ch. 7, § Lie Group Homomorphisms; source L4200 · not formalized

A Lie group homomorphism is a Lie group isomorphism if and only if it is bijective.

Not formalized. none; no complete checked declaration under strict bundle semantics — MonoidHom.inverse gives the inverse homomorphism algebraically for a bijection, but no pinned/current theorem proves that every bijective smooth Lie-group homomorphism has smooth inverse. The missing analytic half is the substance of the row. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Theorem 7.7

FC08-C07-U010 · Ch. 7, § The Universal Covering Group; source L4208 · not formalized

Theorem 7.7 (Existence of a Universal Covering Group). Let G be a connected Lie group. There exists a simply connected Lie group $\widetilde { G }$ , called the universal covering group of G , that admits a smooth covering map $\pi \colon { \tilde { G } } \to G$ that is also a Lie group homomorphism.

Not formalized. none; no complete checked declaration under strict bundle semantics — Topology has covering-space and lifting machinery, but no checked construction of a universal covering Lie group, lifted group law, or uniqueness as a Lie-group isomorphism. Current indexed Lie-group roadmaps explicitly list simply-connected covers as missing; the examples therefore lack their required Lie-group owner. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Theorem 7.9

FC08-C07-U011 · Ch. 7, § The Universal Covering Group; source L4256 · not formalized

Theorem 7.9 (Uniqueness of the Universal Covering Group). For any connected Lie group $G$ , the universal covering group is unique in the following sense: $i f { \widetilde { G } }$ and $\widetilde { G } ^ { \prime }$ are simply connected Lie groups that admit smooth covering maps $\pi \colon { \tilde { G } } \to G$ and $\pi ^ { \prime } \colon \widetilde { G } ^ { \prime } \to G$ that are also Lie group homomorphisms, then there exists a Lie group isomorphism $\phi \colon { \tilde { G } } { \tilde { G } } ^ { \prime }$ such that $\pi ^ { \prime } \circ \phi = \pi$

Example 7.10

FC08-C07-U012 · Ch. 7, § The Universal Covering Group; source L4260 · after FC08-C07-U006 · not formalized

(Universal Covering Groups). (a) For each $n$ the map $\varepsilon^{n} \colon \mathbb{R}^{n} \to \mathbb{T}^{n}$ given by $\varepsilon^{n}(x^{1},\dots,x^{n}) = (e^{2\pi i x^{1}},\dots,e^{2\pi i x^{n}})$ is a Lie group homomorphism and a smooth covering map; since $\mathbb{R}^{n}$ is simply connected, the universal covering group of $\mathbb{T}^{n}$ is the additive Lie group $\mathbb{R}^{n}$. (b) The homomorphism $\exp \colon \mathbb{C} \to \mathbb{C}^{*}$ is also a smooth covering map, so $\mathbb{C}$ is the universal covering group of $\mathbb{C}^{*}$.

Definition/convention — Lie subgroup of G

FC08-C07-U013 · Ch. 7, § Lie Subgroups; source L4274 · not formalized

Suppose G is a Lie group. A Lie subgroup of G is a subgroup of G endowed with a topology and smooth structure making it into a Lie group and an immersed submanifold of G. The following proposition shows that embedded subgroups are automatically Lie subgroups.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has Subgroup, LieGroup, and IsSmoothEmbedding predicates but no general Lie-subgroup object because the embedded/immersed-submanifold layer is absent. Hence the topology/smooth-structure and open/embedded Lie-subgroup claims cannot be stated as Lee does. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Proposition 7.11

FC08-C07-U014 · Ch. 7, § Lie Subgroups; source L4276 · not formalized

Proposition 7.11. Let G be a Lie group, and suppose $H \subseteq G$ is a subgroup that is also an embedded submanifold. Then H is a Lie subgroup.

Lemma 7.12

FC08-C07-U015 · Ch. 7, § Lie Subgroups; source L4282 · not formalized

Lemma 7.12. Suppose G is a Lie group and $H \subseteq G$ is an open subgroup. Then H is an embedded Lie subgroup. In addition, H is closed, so it is a union of connected components of G.

Definition/convention — source terminology/construction

FC08-C07-U016 · Ch. 7, § Lie Subgroups; source L4286 · in Mathlib

If G is a group and $S \subseteq G$ , the subgroup generated by S is the smallest subgroup containing S (i.e., the intersection of all subgroups containing S).

Formalized. Mathlib/Algebra/Group/Subgroup/Lattice.lean::Subgroup.closure, Subgroup.mem_closure, Subgroup.subset_closure — Subgroup.closure S is documented and defined as the subgroup generated by S, namely the infimum/intersection of all subgroups containing S; mem_closure gives exactly the universal characterization Lee states.

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

Proposition 7.14

FC08-C07-U017 · Ch. 7, § Lie Subgroups; source L4290 · not formalized

Suppose $G$ is a Lie group and $W \subseteq G$ is any neighborhood of the identity. (a) $W$ generates an open subgroup of $G$. (b) If $W$ is connected, it generates a connected open subgroup of $G$. (c) If $G$ is connected, then $W$ generates $G$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Subgroup.closure supplies the algebraic subgroup generated by a neighborhood and topological-group APIs supply nearby ingredients, but no checked theorem packages Lee’s three conclusions: openness, connectedness under connected W, and generation of all connected G. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Definition/convention — identity component of G

FC08-C07-U018 · Ch. 7, § Lie Subgroups; source L4316 · in Mathlib

If G is a Lie group, the connected component of G containing the identity is called the identity component of G .

Formalized. Mathlib/Topology/Algebra/Group/Basic.lean::Subgroup.connectedComponentOfOne — Subgroup.connectedComponentOfOne G has carrier connectedComponent (1 : G), exactly Lee’s identity component (with Mathlib’s multiplicative identity 1 in place of e).

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

Proposition 7.15

FC08-C07-U019 · Ch. 7, § Lie Subgroups; source L4318 · not formalized

Proposition 7.15. Let G be a Lie group and let $G _ { 0 }$ be its identity component. Then G0 is a normal subgroup of G, and is the only connected open subgroup. Every connected component of G is diffeomorphic to $G _ { 0 }$

Not formalized. none; no complete checked declaration under strict bundle semantics — Subgroup.connectedComponentOfOne owns the identity component itself (U018), but no checked theorem owns this full bundle of normality, uniqueness as the connected open subgroup, and diffeomorphic connected components. In particular, the open-subgroup library still records identity-component openness as missing in its general setting. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Proposition 7.16

FC08-C07-U020 · Ch. 7, § Lie Subgroups; source L4324 · not formalized

Proposition 7.16. Let F G H be a Lie group homomorphism. The kernel of F is a properly embedded Lie subgroup of G, whose codimension is equal to the rank of F . P

Not formalized. none; no complete checked declaration under strict bundle semantics — These rows require the missing Lie-subgroup/submanifold theory (kernel/image as Lie subgroups, induced smooth structures, embeddedness, or closed-subgroup characterization), and several also rely on the absent constant-rank theorem. Algebraic subgroup and matrix-group ingredients are only proper subsets. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Proposition 7.17

FC08-C07-U021 · Ch. 7, § Lie Subgroups; source L4330 · not formalized

$F \colon G \to H$ is an injective Lie group homomorphism, the image of F has a unique smooth manifold structure such that F .G/ is a Lie subgroup of H and $F \colon G \to F ( G )$ is a Lie group isomorphism onto it.

Example 7.18

FC08-C07-U022 · Ch. 7, § Lie Subgroups; source L4336 · after FC08-C07-U004 · not formalized

(Embedded Lie Subgroups). (a) $\mathrm{GL}^{+}(n,\mathbb{R}) \subseteq \mathrm{GL}(n,\mathbb{R})$ is an open subgroup and so an embedded Lie subgroup. (b) The circle $\mathbb{S}^{1}$ is an embedded Lie subgroup of $\mathbb{C}^{*}$, being both a subgroup and an embedded submanifold. (c) The special linear group $\mathrm{SL}(n,\mathbb{R})$ of real $n \times n$ matrices of determinant $1$: the determinant is a surjective smooth submersion by the global rank theorem, so $\mathrm{SL}(n,\mathbb{R})$ has dimension $n^{2}-1$. (d) The map $\beta \colon \mathrm{GL}(n,\mathbb{C}) \to \mathrm{GL}(2n,\mathbb{R})$ replacing each entry $a + ib$ by the block $\begin{pmatrix} a & -b \\ b & a \end{pmatrix}$ is an injective Lie group homomorphism whose image is a properly embedded Lie subgroup of $\mathrm{GL}(2n,\mathbb{R})$. (e) The complex special linear group $\mathrm{SL}(n,\mathbb{C}) = \operatorname{Ker}(\det) \subseteq \mathrm{GL}(n,\mathbb{C})$ is a properly embedded Lie subgroup of codimension $\dim_{\mathbb{R}} \mathbb{C}^{*} = 2$, hence of dimension $2n^{2}-2$.

Example 7.19

FC08-C07-U023 · Ch. 7, § Lie Subgroups; source L4356 · after FC08-C04-U020, FC08-C07-U021 · not formalized

Example 7.19 (A Dense Lie Subgroup of the Torus). Let $H \subseteq \mathbb { T } ^ { 2 }$ be the dense submanifold of the torus that is the image of the immersion $\gamma \colon { \mathbb { R } } \to { \mathbb { T } } ^ { 2 }$ defined in Example 4.20. It is easy to check that $\gamma$ is an injective Lie group homomorphism, and thus H is an immersed Lie subgroup of $\mathbb { T } ^ { 2 }$ by Proposition 7.17. Exercise 7.20. Let $S \subseteq \mathbb { T } ^ { 3 }$ be the image of the subgroup H of the preceding ith the discrete topology is a topological group, called a discrete group.

Theorem 7.21

FC08-C07-U024 · Ch. 7, § Lie Subgroups; source L4367 · not formalized

Theorem 7.21. Suppose G is a Lie group and $H \subseteq G$ is a Lie subgroup. Then H is closed in G if and only if it is embedded.

Definition/convention — group

FC08-C07-U025 · Ch. 7, § Group Actions and Equivariant Maps; source L4410 · in Mathlib

The most important applications of Lie groups to smooth manifold theory involve actions by Lie groups on other manifolds. If G is a group and M is a set, a left action of G on M is a map $G \times M \to M$ ; often written as $( g , p ) \mapsto g \cdot p$ , that satisfies \[ \begin{array}{c c} g _ {1} \cdot (g _ {2} \cdot p) = (g _ {1} g _ {2}) \cdot p & \text { for all } g _ {1}, g _ {2} \in G \text { and } p \in M; \\ e \cdot p = p & \text { for all } p \in M. \end{array}\tag{7.6} \]

Formalized. Mathlib/Algebra/Group/Action/Defs.lean::MulAction — For a group G, MulAction G M is exactly a left action: its scalar multiplication satisfies identity and multiplication/associativity laws corresponding to e·p=p and g₁·(g₂·p)=(g₁g₂)·p.

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

Definition/convention — a continuous action

FC08-C07-U026 · Ch. 7, § Group Actions and Equivariant Maps; source L4422 · in Mathlib

If M is a topological space and G is a topological group, an action of G on M is said to be a continuous action if the defining map $G \times M \to M { \mathrm { ~ o r ~ } } M \times G \to M$ is continuous. In this case, M is said to be a (left or right) G -space. If in addition M is a smooth manifold with or without boundary, G is a Lie group, and the defining map is smooth, then the action is said to be a smooth action. We are primarily interested in smooth actions of Lie groups on smooth manifolds.

Formalized. Mathlib/Topology/Algebra/MulAction.lean::ContinuousSMul; Mathlib/Geometry/Manifold/Algebra/SMul.lean::ContMDiffSMul, ContMDiffSMul.continuousSMul — ContinuousSMul requires joint continuity of the action map, while ContMDiffSMul I I′ ∞ G M requires that same map G × M → M to be smooth; the latter file explicitly presents this as a smooth Lie-group action when combined with LieGroup and IsManifold. Right actions are equivalently left actions of the opposite group.

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

Convention/notation — source terminology/construction

FC08-C07-U027 · Ch. 7, § Group Actions and Equivariant Maps; source L4438 · not formalized

For left actions, we generally use the notations $g \cdot p$ and $\theta _ { g } ( p )$ interchangeably. The latter notation contains a bit more information, and is useful when it is important to specify the particular action under consideration, while the former is often more convenient when the action is understood. For right actions, the notation $p \cdot g$ is generally preferred because of the way composition works.

Not formalized. none; no complete checked declaration under strict bundle semantics — The smooth-action API provides the fixed left-action diffeomorphism Diffeomorph.smul, but Lee’s row is specifically a left/right notation convention (g·p, θ_g(p), p·g). Mathlib has no matching right-action notation/interface, so the whole convention is not promoted. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Definition/convention — symmetry group of the structure) frequently turns out to be a Lie

FC08-C07-U028 · Ch. 7, § Group Actions and Equivariant Maps; source L4442 · not formalized

Lie group actions typically arise in situations involving some kind of symmetry. For example, if M is a vector space or smooth manifold endowed with a metric or other geometric structure, the set of diffeomorphisms of M that preserve the structure (called the symmetry group of the structure) frequently turns out to be a Lie group acting smoothly on M . T

Not formalized. none; no complete checked declaration under strict bundle semantics — This is explanatory terminology about symmetry groups of geometric structures. Smooth action/diffeomorphism primitives exist, but there is no generic checked “symmetry group of a structure” Lie-group construction matching the row. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Definition/convention — transitive

FC08-C07-U029 · Ch. 7, § Group Actions and Equivariant Maps; source L4460 · in Mathlib

The action is said to be transitive if for every pair of points $p , q \in M$ ; there exists $g \in G$ such that $g \cdot p = q$ , or equivalently if the only orbit is all of M .

Formalized. Mathlib/Algebra/Group/Action/Pretransitive.lean::MulAction.IsPretransitive; Mathlib/GroupTheory/GroupAction/Transitive.lean::MulAction.isPretransitive_iff_orbit_eq_univ — IsPretransitive G M says every pair of points is related by some group element, and isPretransitive_iff_orbit_eq_univ is exactly Lee’s equivalent “the only orbit is all of M” characterization.

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

Definition/convention — free

FC08-C07-U030 · Ch. 7, § Group Actions and Equivariant Maps; source L4462 · in Mathlib

The action is said to be free if the only element of G that fixes any element of M is the identity: $g \cdot p = p$ for some $p \in M$ implies $g = e$ , or equivalently if every isotropy group is trivial.

Formalized. Mathlib/Algebra/Group/Action/Defs.lean::IsCancelSMul; Mathlib/Algebra/Group/Action/Basic.lean::isCancelSMul_iff_eq_one_of_smul_eq; Mathlib/GroupTheory/GroupAction/Basic.lean::isCancelSMul_iff_stabilizer_eq_bot — For a group action, IsCancelSMul is equivalent to g • p = p → g = 1, and also to every stabilizer being the trivial subgroup. These are precisely Lee’s two equivalent definitions of a free action.

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

Example 7.22

FC08-C07-U031 · Ch. 7, § Group Actions and Equivariant Maps; source L4466 · not formalized

(Lie Group Actions). (a) For any Lie group $G$ and smooth manifold $M$, the trivial action $g \cdot p = p$ is smooth; each orbit is a point and each isotropy group is all of $G$. (b) The natural action of $\mathrm{GL}(n,\mathbb{R})$ on $\mathbb{R}^{n}$ is matrix multiplication $(A,x) \mapsto Ax$ on column vectors; since any nonzero vector goes to any other, there are exactly two orbits, $\{0\}$ and $\mathbb{R}^{n} \setminus \{0\}$. (c) Every Lie group acts smoothly on itself by left translation; more generally, restricting multiplication to $H \times G \to G$ for a Lie subgroup $H$ gives a smooth free — generally not transitive — left action. (d) Every Lie group acts smoothly on itself by conjugation, $g \cdot h = ghg^{-1}$. (e) An action of a discrete group $\Gamma$ on $M$ is smooth if and only if $p \mapsto g \cdot p$ is smooth for each $g \in \Gamma$. An automorphism of a covering $\pi$, also called a deck or covering transformation, is a homeomorphism $\varphi \colon E \to E$ with $\pi \circ \varphi = \pi$; the set $\operatorname{Aut}_{\pi}(E)$ of all of them is a group under composition, acting on $E$ on the left.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib owns many individual algebraic actions and some smooth scalar actions, but not the complete multi-example bundle, especially the Lie-subgroup restriction and covering-automorphism examples. Whole-row semantics reject the partial examples. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Definition/convention — normal covering map

FC08-C07-U032 · Ch. 7, § Group Actions and Equivariant Maps; source L4488 · not formalized

The set $\operatorname { A u t } _ { \pi } ( E )$ of all automorphisms of $\pi$ , called the automorphism group of $\pi ,$ is a group under composition, acting on $E$ on the left. It can be shown that $\operatorname { A u t } _ { \pi } ( E )$ acts transitively on each fiber of if and only if is a normal covering map, which means that $\pi _ { * } ( \pi _ { 1 } ( E , q ) )$ is a normal subgroup of $\pi _ { 1 } ( M , \pi ( q ) )$ for every $q \in E$ (see, for example, [

Not formalized. none; no complete checked declaration under strict bundle semantics — The covering-space library has deck/lifting infrastructure, but no checked package makes the automorphism group of a smooth covering into the asserted discrete zero-dimensional Lie group with the full smooth/free action theorem, nor packages Lee’s normal-cover equivalence in this smooth setting. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Proposition 7.23

FC08-C07-U033 · Ch. 7, § Group Actions and Equivariant Maps; source L4490 · not formalized

Suppose $E$ and $M$ are smooth manifolds with or without boundary and $\pi \colon E \to M$ is a smooth covering map. With the discrete topology, the automorphism group $\operatorname{Aut}_{\pi}(E)$ is a zero-dimensional Lie group acting smoothly and freely on $E$.

Definition/convention — equivariant

FC08-C07-U034 · Ch. 7, § Equivariant Maps; source L4506 · in Mathlib

For some manifolds with group actions, there is an easily verified sufficient condition for a smooth map to have constant rank. Suppose $G$ is a Lie group, and M and N are both smooth manifolds endowed with smooth left or right G-actions. A map $F \colon M \to N$ is said to be equivariant with respect to the given G-actions if for each $g \in G ,$ \[ \begin{array}{l l} F (g \cdot p) = g \cdot F (p) & (\text { for left actions }), \\ F (p \cdot g) = F (p) \cdot g & (\text { for right actions }). \end{array} \] Equivalently, if and ’ are the given actions on M and $N _ { : }$ , respectively, $F$ is equivariant if the following diagram commutes for each $g \in G \colon$ \[ \begin{array}{c} M \xrightarrow {F} N \\ \theta_ {g} \Big \downarrow \qquad \qquad \qquad \qquad \Big \downarrow \varphi_ {g} \\ M \xrightarrow {F} N. \end{array} \] This condition is also expressed by sayi ${ \mathbb S } ^ { 1 }$ is an embedded Lie subgroup of $\mathbb { C } ^ { * }$ because it is a subgroup and an embedded submanifold.

Formalized. Mathlib/GroupTheory/GroupAction/Hom.lean::MulActionHom — MulActionHom φ X Y bundles exactly the equivariance equation F(g • p) = φ(g) • F(p); with the identity scalar map this is Lee’s intertwining condition for two actions of the same group. Right actions are encoded by passing to the opposite group.

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

Example 7.24

FC08-C07-U035 · Ch. 7, § Equivariant Maps; source L4520 · after FC08-C07-U008 · not formalized

Let $v = (v^{1},\dots,v^{n}) \in \mathbb{R}^{n}$ be a fixed nonzero vector. The formulas \[ t \cdot (x^{1},\dots,x^{n}) = (x^{1}+tv^{1},\dots,x^{n}+tv^{n}), \qquad t \cdot (z^{1},\dots,z^{n}) = (e^{2\pi i t v^{1}}z^{1},\dots,e^{2\pi i t v^{n}}z^{n}) \] define smooth left actions of $\mathbb{R}$ on $\mathbb{R}^{n}$ and on $\mathbb{T}^{n}$, and the smooth map $\varepsilon^{n}(x^{1},\dots,x^{n}) = (e^{2\pi i x^{1}},\dots,e^{2\pi i x^{n}})$ is equivariant with respect to them.

Not formalized. none; no complete checked declaration under strict bundle semantics — Circle/additive-quotient covering maps and equivariance ingredients exist, but no checked declaration owns Lee’s specific real-to-torus action example and all of its stated equivariance identities as one existing formalization. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Theorem 7.25

FC08-C07-U036 · Ch. 7, § Equivariant Maps; source L4537 · not formalized

Theorem 7.5 is an extremely useful tool for proving that certain maps have constant rank. Theorem 7.25 (Equivariant Rank Theorem). Let M and N be smooth manifolds and let G be a Lie group. Suppose $F \colon M \to N$ is a smooth map that is equivariant with respect to a transitive smooth G-action on M and any smooth G-action on N . Then F has constant rank. Thus, if F is surjective, it is a smooth submersion; if it is injective, it is a smooth immersion; and if it is bijective, it is a diffeomorphi ight).

Not formalized. none; no complete checked declaration under strict bundle semantics — No pinned/current manifold Equivariant Rank Theorem was found. The generic algebraic MulActionHom owns equivariance (U034), but the constant-rank, submersion, immersion, and diffeomorphism consequences require missing finite-dimensional rank theory. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Definition/convention — orbit map

FC08-C07-U037 · Ch. 7, § Equivariant Maps; source L4547 · in Mathlib

Here is an important application of the equivariant rank theorem. Suppose G is a Lie group, M is a smooth manifold, and $\theta \colon G \times M \to M$ is a smooth left action. (The definitions for right actions are analogous.) For each $p \in M ,$ ; define a map G M by \[ \theta^ {(p)} (g) = g \cdot p.\tag{7.9} \] This is often called the orbit map, because its image is the orbit $G \cdot p$ . In addition, the preimage $( \theta ^ { ( p ) } ) ^ { - 1 } ( p )$ is the isotropy of the Torus).

Formalized. Mathlib/GroupTheory/GroupAction/Defs.lean::MulAction.orbit, MulAction.stabilizer; Mathlib/Algebra/Group/Action/Basic.lean::MulAction.toFun — The fixed-point action map is literally g ↦ g • p; MulAction.orbit G p is its range and MulAction.stabilizer G p is the preimage of p. Both source equalities were compiled in /tmp/fc08-c07-witness.lean.

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

Proposition 7.26

FC08-C07-U038 · Ch. 7, § Equivariant Maps; source L4557 · not formalized

Proposition 7.26 (Properties of the Orbit Map). Suppose is a smooth left action of a Lie group G on a smooth manifold M . For each $p \in M ,$ ; the $o r \mathrm { - }$ bit map $\theta ^ { ( p ) } \colon G \to M$ is smooth and has constant rank, so the isotropy group $G _ { p } = { \left( { \theta ^ { ( p ) } } \right) ^ { - 1 } } ( p )$ is a properly embedded Lie subgroup of G. If $G _ { p } = \{ e \}$ , then $\theta ^ { ( p ) }$ is an injective smooth immersion, so the orbit G p is an immersed ample under the obvious embedding $\mathbb { T } ^ { 2 } \hookrightarrow \mathbb { T } ^ { 3 }$ .

Not formalized. none; no complete checked declaration under strict bundle semantics — Orbit and stabilizer definitions are formalized (U037), but the asserted smooth constant rank, properly embedded isotropy Lie subgroup, and immersed-orbit conclusions require the missing rank and Lie-subgroup/submanifold layers. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Example 7.27

FC08-C07-U039 · Ch. 7, § Equivariant Maps; source L4585 · not formalized

(The Orthogonal Group). A real $n \times n$ matrix $A$ is orthogonal if, as a linear map $A \colon \mathbb{R}^{n} \to \mathbb{R}^{n}$, it preserves the Euclidean dot product: $(Ax) \cdot (Ay) = x \cdot y$ for all $x, y \in \mathbb{R}^{n}$; equivalently, if its columns are orthonormal. The set $\mathrm{O}(n)$ of such matrices is a subgroup of $\mathrm{GL}(n,\mathbb{R})$, the orthogonal group of degree $n$. It is compact, being closed — a level set of $\Phi(A) = A^{T}A$ — and bounded in $M(n,\mathbb{R}) \cong \mathbb{R}^{n^{2}}$, since every $A \in \mathrm{O}(n)$ has columns of norm $1$ and so $|A| = \sqrt{n}$. Equivariance of $\Phi$ under suitable right actions of $\mathrm{GL}(n,\mathbb{R})$ shows $\Phi$ has constant rank; computing $d\Phi_{I_{n}}(B)$ along the curve $\gamma(t) = I_{n} + tB$ shows its image is exactly the symmetric matrices, a subspace of dimension $n(n+1)/2$. Hence $\mathrm{O}(n)$ is an embedded Lie subgroup of dimension $n^{2} - n(n+1)/2 = n(n-1)/2$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has the corresponding algebraic matrix groups and substantial linear algebra, but the complete Lee examples additionally assert smooth Lie-subgroup structures, dimensions/connectedness and related manifold facts not packaged at P or H. No whole-row owner was found. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Example 7.28

FC08-C07-U040 · Ch. 7, § Equivariant Maps; source L4615 · not formalized

Example 7.28 (The Special Orthogonal Group). The special orthogonal group of degree n is defined as $\operatorname { S O } ( n ) = \operatorname { O } ( n ) \cap \operatorname { S L } ( n , \mathbb { R } ) \subseteq \operatorname { G L } ( n , \mathbb { R } )$ . Because every matrix $A \in \mathrm { O } ( n )$ satisfies \[ 1 = \det I _ {n} = \det \left(A ^ {T} A\right) = (\det A) \left(\det A ^ {T}\right) = (\det A) ^ {2}, \] it follows that det $A = \pm 1$ for all $A \in \mathrm { O } ( n )$ . Therefore, SO.n/ is the open subgroup of ${ \mathrm { O } } ( n )$ consisting of matrices of positive determinant, and is therefore also an embedded Lie subgroup of dimension $n ( n - 1 ) / 2$ in GL.n; R/. It is a compact group because it is a closed subset of ${ \mathrm { O } } ( n )$ Example 7.29 (The Unitary Group). For any complex matrix $A ,$ , the adjoint of A is the matrix $A ^ { * }$ formed by conjugating the entries of A and taking the transpose: $\boldsymbol { A } ^ { * } = \overline { { \boldsymbol { A } } } ^ { T }$

Example 7.29

FC08-C07-U041 · Ch. 7, § Equivariant Maps; source L4623 · not formalized

Example 7.29 (The Unitary Group). For any complex matrix $A ,$ , the adjoint of A is the matrix $A ^ { * }$ formed by conjugating the entries of A and taking the transpose: $\boldsymbol { A } ^ { * } = \overline { { \boldsymbol { A } } } ^ { T }$ Observe that $( A B ) ^ { * } = \left( { \bar { A } } { \bar { B } } \right) ^ { T } = { \bar { B } } ^ { T } { \bar { A } } ^ { T } = B ^ { * } A ^ { * }$ . For any positive integer n, the unitary group of degree n is the subgroup $\mathrm { U } ( n ) \subseteq \mathrm { G L } ( n , \mathbb { C } )$ consisting of complex $n \times n$ matrices whose columns form an orthonormal basis for $\mathbb { C } ^ { n }$ with respect to the Hermitian dot product $\begin{array} { r } { z \cdot w = \sum _ { i } z ^ { i } \overline { { w ^ { i } } } } \end{array}$ . It is straightforward to check that U.n/ consists of those matrices A such that ${ \overline { { A ^ { * } } } } A = I _ { n }$ . Problem 7-13 shows that it is a properly embed explained at the beginning of the proof, the existence of such a neighborhood for one point of H implies that H is embedded.

Example 7.30

FC08-C07-U042 · Ch. 7, § Equivariant Maps; source L4625 · not formalized

embedded Lie subgroup of $\mathrm { G L } ( n , \mathbb { C } )$ of dimension $n ^ { 2 }$ Example 7.30 (The Special Unitary Group). The group $\mathrm { S U } ( n ) = \mathrm { U } ( n ) \ \cap$ SL.n; C/ is called the complex special unitary group of degree n. Problem 7-14 shows that it is a properly embedded $( n ^ { 2 } - 1 )$ /-dimensional Lie subgroup of U.n/. Since the composition of smooth embeddings $\operatorname { S U } ( n ) \hookrightarrow \operatorname { U } ( n ) \hookrightarrow \operatorname { G L } ( n , \mathbb { C } )$ is again a smooth embedding, this implies that SU.n/ is also embedded nvolve actions by Lie groups on other manifolds.

Construction/definition — semidirect product of H

FC08-C07-U043 · Ch. 7, § Semidirect Products; source L4629 · not formalized

also embedded in GL.n; C/. ## Semidirect Products Group actions give us a powerful new way to construct Lie groups. Suppose H and N are Lie groups, and $\theta \colon H \times N \to N$ is a smooth left action of H on N . is said to be an action by automorphisms if for each $h \in H$ , the map $\theta _ { h } \colon N \to N$ is a group automorphism of N (i.e., an isomorphism from N to itself). Given such an action, we define a new Lie group $N \rtimes _ { \theta }$ H , called a semidirect N , as follows. As a smooth manifold, H is just the Cartesian product $N \times H ;$ but the group multiplication is defined by \[ (n, h) (n ^ {\prime}, h ^ {\prime}) = \bigl (n \theta_ {h} (n ^ {\prime}), h h ^ {\prime} \bigr).\tag{7.10} \]

Not formalized. none; no complete checked declaration under strict bundle semantics — SemidirectProduct formalizes the algebraic product and multiplication formula, with canonical inclusions/projection and complementary-subgroup isomorphisms. There is no pinned/current Lie-group instance from a smooth automorphism action, nor the required closed Lie-subgroup/internal semidirect-product geometry, so the Lee rows are not owned in full. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Example 7.32

FC08-C07-U044 · Ch. 7, § Semidirect Products; source L4639 · not formalized

Example 7.32 (The Euclidean Group). If we consider $\mathbb { R } ^ { n }$ as a Lie group under addition, then the natural action of O.n/ on $\mathbb { R } ^ { n }$ is an action by automorphisms. The resulting semidirect product $\operatorname { E } ( n ) = \mathbb { R } ^ { n } \rtimes \mathbf { O } ( n )$ is called the Euclidean group; its multiplication is given by $( b , A ) ( b ^ { \prime } , A ^ { \prime } ) = ( b + A b ^ { \prime } , A A ^ { \prime } )$ acts on $\mathbb { R } ^ { n }$ via \[ (b, A) \cdot x = b + A x. \] This action preserves lines, distances, and angle measures, and thus consists of rigid motions of $\mathbb{R}^{n}$.

Proposition 7.33

FC08-C07-U045 · Ch. 7, § Semidirect Products; source L4649 · not formalized

Proposition 7.33 (Properties of Semidirect Products). Suppose N and H are Lie groups, and is a smooth action of H on N by automorphisms. Let $G = N \rtimes _ { \theta } H$ (a) The subsets $\widetilde { N } = N \times \{ e \}$ and $\tilde { H } = \{ e \} \times H$ are closed Lie subgroups of $G$ isomorphic to N and H , respectively. (b) $\widetilde { N }$ is a normal subgroup of Gz. (c) $\tilde { N } \cap \tilde { H } = \{ ( e , e ) \}$ and Nz Hz G. Exercise 7.34. Prove the preceding proposition. Thanks to the next theorem, many Lie groups can be realized as semidirect products , and a left action can similarly be converted to a right action.

Theorem 7.35

FC08-C07-U046 · Ch. 7, § Semidirect Products; source L4661 · not formalized

Theorem 7.35 (Characterization of Semidirect Products). Suppose G is a Lie group, and $N , H \subseteq G$ are closed Lie subgroups such that N is normal, N H e , and $N H = G$ . Then the map .n; h/ nh is a Lie group isomorphism between N H and G, where $\theta \colon H \times N \to N$ is the action by conjugation: $\theta _ { h } ( n ) =$ hnh.

Construction/definition — source terminology/construction

FC08-C07-U047 · Ch. 7, § Semidirect Products; source L4665 · not formalized

Under the hypotheses of Theorem (7.35), we say that G is the internal semidirect product of N and H . Some examples are described in Problem

Definition/convention — faithful

FC08-C07-U048 · Ch. 7, § Representations; source L4673 · after FC08-C07-U021 · not formalized

a representation $\rho \colon G \to \mathbf { G } \mathbf { L } ( V )$ is injective, it is said to be faithful. In that case, it follows from Proposition 7.17 that the image of is a Lie subgroup of GL.V /, and gives a Lie group isomorphism between G and $\rho ( G ) \subseteq { \mathrm { G L } } ( V ) \cong$ GL.n; R/ or GL.n; C/. Thus, a Lie group admits a faithful representation if and only if it is isomorphic to a Lie subgroup of GL.n; R/ or GL.n; C/ for some n. Not every Lie group admits such a representation. We do not yet have the technology to construct a counterexample, but Problem 21-26 asks you to prove that the universal covering group of SL.2; R/ has no faithful representation and therefore is not isomorphic to any matrix manifolds.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has algebraic Representation, FaithfulSMul, linear actions, and smooth-action infrastructure, but no bundled smooth representation of a Lie group or bridge proving the associated GL(V) action smooth and conversely recovering a smooth representation. The Lie-subgroup consequences in U048 are also unavailable. Strict bundle semantics reject proper subsets, isolated ingredients, unbridged equivalent notions, stronger-hypothesis specializations, and reconstruction of the substantive source theorem.

Example 7.36

FC08-C07-U049 · Ch. 7, § Representations; source L4677 · after FC08-C07-U044 · not formalized

Example 7.36 (Lie Group Representations). (a) If G is any Lie subgroup of GL.n; R/, the inclusion G } ( n , ) = $ $\mathbf { G L } ( \mathbb { R } ^ { n } )$ is a faithful representation, called the defining representation of G . The defining representation of a Lie subgroup of $ ( n , $\mathbb { S } ^ { 1 } \hookrightarrow \mathbb { C } ^ { * } \cong { \mathrm { G L } } ( 1 , \mathbb { C } )$ representation of the circle group. More generally, the map ^ { n } ( n , (z ^ {1}, , z ^ {n}) = ( \[\begin{array}{c c c c} z ^ {1} & 0 & \ldots & 0 \\ 0 & z ^ {2} & \ldots 0 \\ \vdots & \vdots & \ddots & \vdots \\ 0 & 0 & z ^ {n} \end{array}\] ) \[ is a faithful representation of $\mathbb { T } ^ { n }$ (c) Let $\sigma \colon \mathbb { R } ^ { n } \to \mathbf { G L } ( n + 1 , \mathbb { R } )$ be the map that sends $x \in \mathbb { R } ^ { n }$ to the matrix $\sigma ( x )$ defined in block form by \] (x) = ( \[\begin{array}{c c} I _ {n} & x \\ 0 & 1 \end{array}\] ), \[ where $I _ { n }$ is the $n \times n$ identity matrix and x is regarded as an $n \times 1$ column matrix. A straightforward computation shows that is a faithful representation of the additive Lie $\operatorname { g r o u p } \mathbb { R } ^ { n }$ (d) Another faithful representation of $\mathbb { R } ^ { n }$ is the map $\mathbb { R } ^ { n } \to { \mathrm { G L } } ( n , \mathbb { R } )$ that sends $( { \overline { { x ^ { 1 } } } } , \ldots , x ^ { n } )$ to the diagonal matrix whose diagonal entries are $( e ^ { x ^ { 1 } } , \dots , e ^ { x ^ { n } } )$ (e) Yet another representation of $\mathbb { R } ^ { n }$ is the map $\mathbb { R } ^ { n } \to \mathbf { G L } ( n , \mathbb { C } )$ sending x to the diagonal matrix with diagonal entries $\left( e ^ { 2 \pi i x ^ { 1 } } , \dots , e ^ { 2 \pi i x ^ { n } } \right)$ This one is not faithful, because its kernel is the subgroup $\mathbb { Z } ^ { n } \subseteq \mathbb { R } ^ { n } .$ (f) Let E.n/ be the Euclidean group (Example 7.32). A faithful representation of E.n/ is given by the map $\rho \colon \operatorname { E } ( n ) \operatorname { G L } ( n + 1 , \mathbb { R } )$ defined in block form by \] \[\begin{array}{c c} A & b \\ 0 & 1 \end{array}\]

), \[ where b is considered as a column matrix. (g) For positive integers n and $d .$ , let $\mathcal P _ { d } ^ { n }$ denote the vector space of real-valued polynomial functions $p \colon { \mathbb { R } } ^ { n } \to { \mathbb { R } }$ of degree at most $d$ . For any matrix $A \in$ GL $\left( n , \mathbb { R } \right)$ define a linear map $\tau _ { d } ^ { n } ( A ) \colon { \mathcal { P } } _ { d } ^ { n } \to { \mathcal { P } } _ { d } ^ { n }$ by \]

Definition/convention — a linear action

FC08-C07-U050 · Ch. 7, § Representations; source L4717 · not formalized

There is a close connection between representations and group actions. Let G be a Lie group and V be a finite-dimensional vector space. An action of G on V is said to be a linear action if for each $g \in G$ , the map from V to itself given by $x \mapsto g \cdot x$ is linear. For example, if $\rho \colon G \to \mathbf { G } \mathbf { L } ( V )$ is a representation of G, there is an associated smooth linear action of G on V given by $g \cdot x = \rho ( g ) x$ . The next proposition shows that every linear action of this kind arises from a representation.

Proposition 7.37

FC08-C07-U051 · Ch. 7, § Representations; source L4719 · not formalized

Proposition 7.37. Let G be a Lie group and V be a finite-dimensional vector space. A smooth left action of G on V is linear if and only if it is of the form $g \cdot x = \rho ( g ) x$ for some representation