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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 13 definitions, 5 theorems, 3 propositions and 4 lemmas.

Of the 25 statements checked against Lean, 6 are formalized somewhere and 19 are not.

Status	Statements	Share	What it means
not formalized	19	76%	A documented search found no Lean statement of it anywhere.
in Mathlib	6	24%	Mathlib states and proves it.
checked in total	25

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 18, FC08-C18-U001–FC08-C18-U025, exactly 25 unique contiguous rows from the canonical FC08 unit catalogue.
Search order: project A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0; Lean 4.33.0), current upstream H=5315eef9e4ffb98e0f89f278b765c50a149f66ca (Apache-2.0; Lean 4.34.0-rc2), then indexed/current/external Lean searches.
C18 has 6 pinned mathlib rows and 19 dated unmatched rows. Positives: U003, U006, U007, U008, U009, U019.
U003 and U006–U009 are owned by Mathlib’s singular-simplicial-set/singular-chain-complex implementation: continuous standard-simplex maps, free chain objects, alternating face differential, square-zero boundary, cycles, and homology.
U001–U002 and U004–U005 were not promoted merely because adjacent standard-simplex/face APIs exist: Lee’s rows bundle explicit affine Euclidean simplex geometry and uniqueness/face data not owned by one checked interface.
U010 is deliberately not assembled from separate point-homology and homotopy-invariance results because its arbitrary coproduct clause lacks a checked complete theorem.
No singular-homology Mayer–Vietoris theorem or singular-cohomology functor matching Lee’s real-coefficient convention was found at P/H/current external search, so U011–U014 remain unmatched.
Smooth singular homology/smoothing of simplices (U015–U018) is not present. U019 is independent algebra and maps to Mathlib’s stronger categorical five lemma.
U020–U025 require the missing manifold differential-form integration/de Rham comparison infrastructure identified in C14–C17 and remain unmatched.
N=2026-09-07 marks negative decisions; strict whole-row semantics apply uniformly.

Definition/convention — dimension of the simplex

FC08-C18-U001 · Ch. 18, § Singular Homology; source L14127 · not formalized

We begin with a brief summary of singular homology theory. Suppose $v _ { 0 } , \ldots , v _ { p }$ They are said to be affinely independent (or in general position) if they are not contained in any .p 1/-dimensional affine subspace. A geometric p-simplex is a subset of $\mathbb { R } ^ { n }$ of the \[ \left\{\sum_ {i = 0} ^ {p} t _ {i} v _ {i}: 0 \leq t _ {i} \leq 1 \text { and } \sum_ {i = 0} ^ {p} t _ {i} = 1 \right\}, \] for some $p + 1$ affinely independent _ { 0 } , , v _ { p } }$ . The integer $p$ (one less than the number of vertices) is called the dimension of the simplex. The points $ _ { 0 } , , v _ { p }$ are called its vertices, and the geometric simplex with these vertices is denoted by $ _ { 0 } , , v _ { p } ]$ . It is a compact convex set, in fact the smallest convex set containing $ _ { 0 } , , v _ { p } }$ . The simplices whose vertices are nonempty subsets of $ _ { 0 } , , v _ { p } }$ are called the faces of the simplex. The $( p - 1 )$ -dimensional faces are called its boundary faces. There are precisely $p + 1$ boundary faces, obtained by omitting each of the vertices in turn; the ith boundary face $ , , v _ { p } ]$ (with $v _ { i }$ omitted) is denoted by $

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib’s singular-simplicial-set machinery uses a standard simplex and face maps, but no checked declaration owns the full Euclidean geometric-simplex bundle in this row (affine independence, convex-hull/minimality/face classification, Lee’s affine coordinates, or the unique affine-simplex construction as applicable). Strict whole-row semantics reject proper subsets, unbridged alternative models, missing clauses, and reconstruction from generic ingredients.

Definition/convention — source terminology/construction

FC08-C18-U002 · Ch. 18, § Singular Homology; source L14140 · not formalized

The standard $p$-simplex is $\Delta_{p} = [e_{0},e_{1},\dots,e_{p}] \subseteq \mathbb{R}^{p}$, where $e_{0} = 0$ and $e_{i}$ is the $i$th standard basis vector. Thus $\Delta_{0} = \{0\}$, $\Delta_{1} = [0,1]$, $\Delta_{2}$ is the triangle with vertices $(0,0)$, $(1,0)$, $(0,1)$ together with its interior, and $\Delta_{3}$ is a solid tetrahedron.

Definition/convention — singular p-simplex in M

FC08-C18-U003 · Ch. 18, § Singular Homology; source L14142 · in Mathlib

18.1). Let M be a topological space. A continuous map $\sigma \colon \Delta _ { p } M$ is called a singular p-simplex in M . The singular chain group of M in degree p, denoted by $C _ { p } ( M )$ , is the free abelian group generated by all singular p-simplices in M . An element of this group, called a singular p-chain, is a finite formal linear combination of singular p-simplices in M with integer coefficients.

Formalized. Mathlib/AlgebraicTopology/SingularSet.lean::TopCat.toSSetObjEquiv; Mathlib/AlgebraicTopology/SimplicialSet/Homology/Basic.lean::SSet.chainComplex, SSet.ιChainComplex — The singular simplicial set has p-simplices exactly continuous maps from the standard p-simplex to M. With coefficients ℤ in Ab, its chain object is the coproduct/free abelian group on those simplices, exactly Lee’s singular p-chain group.

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

Definition/convention — affine singular simplex in M

FC08-C18-U004 · Ch. 18, § Singular Homology; source L14144 · not formalized

One special case that arises frequently is that in which the space M is a convex subset of some Euclidean space $\mathbb { R } ^ { m }$ . In that case, for any ordered $( p + 1 )$ /-tuple of points $( w _ { 0 } , \ldots , w _ { p } )$ in M; not necessarily affinely independent, there is a unique affine map from R to $\mathbb { R } ^ { m }$ that takes $e _ { i }$ to $w _ { i }$ for $i = 0 , \ldots , p$ . (The map is easily constructed by first finding a linear map that takes $e _ { i }$ to $w _ { i } - w _ { 0 }$ for $i = 1 , \ldots , p ,$ and then translating by $w _ { 0 } . )$ The restriction of this affine map to $\Delta _ { p }$ is denoted by $A ( w _ { 0 } , \ldots , w _ { p } )$ , and is called an affine singular simplex.

Definition/convention — i th face map in Delta

FC08-C18-U005 · Ch. 18, § Singular Homology; source L14149 · not formalized

each $i = 0 , \ldots , p$ , we define the i th face map in $\Delta _ { p }$ to be the affine singular $( p - 1 )$ /-simplex $F _ { i , p } \colon \Delta _ { p - 1 } \to \Delta _ { p }$ defined by \[ F _ {i, p} = A \left(e _ {0}, \dots , \widehat {e _ {i}}, \dots , e _ {p}\right). \]

Definition/convention — source terminology/construction

FC08-C18-U006 · Ch. 18, § Singular Homology; source L14157 · in Mathlib

The boundary of a singular p-simplex $\Delta _ { p } M$ is the singular $( p - 1 )$ -chain defined by \[ \partial \sigma = \sum_ {i = 0} ^ {p} (- 1) ^ {i} \sigma \circ F _ {i, p}. \]

Formalized. Mathlib/AlgebraicTopology/SimplicialSet/Homology/Basic.lean::SSet.ιChainComplex_d — ιChainComplex_d evaluates the differential on a simplex generator as the alternating sum of its face maps, exactly Lee’s formula for the boundary of a singular simplex under the singular-simplicial-set identification.

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

Definition/convention — singular boundary operator

FC08-C18-U007 · Ch. 18, § Singular Homology; source L14163 · in Mathlib

For example, if $\sigma$ is a singular 2-simplex, its boundary is a formal sum of three singular 1-simplices with coefficients 1, as indicated in Fig. 18.2. This extends uniquely to a group homomorphism @ $C _ { p } ( M ) \to C _ { p - 1 } ( M )$ , called the singular boundary operator. The basic fact about the boundary operator is the next lemma.

Formalized. Mathlib/AlgebraicTopology/SingularHomology/Basic.lean::AlgebraicTopology.singularChainComplexFunctor; Mathlib/AlgebraicTopology/SimplicialSet/Homology/Basic.lean::SSet.ιChainComplex_d — singularChainComplexFunctor packages the degreewise free abelian groups and their boundary homomorphisms; ιChainComplex_d gives the alternating-face action on generators.

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

Lemma 18.2

FC08-C18-U008 · Ch. 18, § Singular Homology; source L14165 · in Mathlib

Lemma 18.2. If c is any singular chain, then $\partial ( \partial c ) = 0$

Formalized. Mathlib/AlgebraicTopology/SingularHomology/Basic.lean::AlgebraicTopology.singularChainComplexFunctor; Mathlib/Algebra/Homology/HomologicalComplex.lean::HomologicalComplex.d_comp_d — The singular chains are a HomologicalComplex, and d_comp_d states that two successive boundary maps compose to zero. Applied to a chain element this is precisely ∂(∂c)=0.

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

Definition/convention — cycle

FC08-C18-U009 · Ch. 18, § Singular Homology; source L14175 · in Mathlib

A singular p-chain c is called a cycle if $\partial c = 0$ , and a boundary if $c = \partial b$ for some singular $( p + 1 )$ /-chain b. Let $Z _ { p } ( M )$ denote the set of singular p-cycles in M; and $B _ { p } ( M )$ the set of singular p-boundaries. Because @ is a homomorphism, $Z _ { p } ( M )$ and $B _ { p } ( M )$ are subgroups of $C _ { p } ( M )$ , and because $\partial \circ \partial = 0$ , they satisfy $B _ { p } ( M ) \subseteq Z _ { p } ( M )$ . The pth singular homology group of M is the quotient group \[ H _ {p} (M) = \frac {Z _ {p} (M)}{B _ {p} (M)}. \] To put it another way, the sequence of abelian groups and homomorphisms \[ \dots \to C _ {p + 1} (M) \xrightarrow {\partial} C _ {p} (M) \xrightarrow {\partial} C _ {p - 1} (M) \to \dots \] Fig. 18.3 The homology homomorphism induced by a continuous map is a complex, called the singular chain complex, and $H _ { p } ( M )$ is the pth homology group of this complex. The equivalence class in $H _ { p } ( M )$ of a singular p-cycle c is called its homology class, and is denoted by Œc. We say that two p-cycles are homologous if they differ by a boundary.

Formalized. Mathlib/AlgebraicTopology/SingularHomology/Basic.lean::AlgebraicTopology.singularChainComplexFunctor, AlgebraicTopology.singularHomologyFunctor; Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean::HomologicalComplex.cycles, HomologicalComplex.homology — The singular chain complex is formalized directly; cycles is the kernel of the boundary and homology is cycles modulo boundaries. singularHomologyFunctor is exactly the homology of this complex, covering Lee’s cycle/boundary/homology-class package.

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

Proposition 18.3

FC08-C18-U010 · Ch. 18, § Singular Homology; source L14196 · not formalized

this intuition more substance.) Proposition 18.3 (Properties of Singular Homology Groups). (a) For any one-point space $\{ q \} , H _ { 0 } ( \{ q \} )$ is the infinite cyclic group generated by the homology class of the unique singular 0-simplex mapping $\Delta _ { 0 }$ to $q _ { \cdot }$ , and $H _ { p } ( \{ q \} ) = 0 f o r a l l p \neq 0$ (b) Let $\{ M _ { j } \}$ be any collection of topological spaces, and let $\begin{array} { r } { M = \coprod _ { i } M _ { j } } \end{array}$ . The inclusion maps $\iota _ { j } \colon M _ { j } \hookrightarrow M$ induce an isomorphism $\bigoplus _ { j } H _ { p } ( M _ { j } ) \cong H _ { p } ( M )$ (c) Homotopy equivalent spaces have isomorphic singular homology note first that any orientation form on $\mathbb { S } ^ { 1 }$ has nonzero integral, so it is not exact by Corollary 16.13; thus dim $H _ { \mathrm { d R } } ^ { 1 } \big ( \mathbb { S } ^ { 1 } \big ) \geq 1$ .

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned Mathlib separately formalizes the point-space singular homology computation and homotopy invariance, but no checked theorem supplies the row’s arbitrary-disjoint-union homology isomorphism together with those clauses as one complete owner. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing clauses, and reconstruction from generic ingredients.

Theorem 18.4

FC08-C18-U011 · Ch. 18, § Singular Homology; source L14218 · not formalized

(Mayer–Vietoris for Singular Homology). Let $M$ be a topological space and $U, V$ open subsets with $U \cup V = M$. For each $p$ there is a connecting homomorphism $\partial_{*} \colon H_{p}(M) \to H_{p-1}(U \cap V)$ for which \[ \cdots \xrightarrow{\ \partial_{*}\ } H_{p}(U \cap V) \xrightarrow{\ \alpha\ } H_{p}(U) \oplus H_{p}(V) \xrightarrow{\ \beta\ } H_{p}(M) \xrightarrow{\ \partial_{*}\ } H_{p-1}(U \cap V) \xrightarrow{\ \alpha\ } \cdots \tag{18.4} \] is exact, where $\alpha[c] = (i_{*}[c], -j_{*}[c])$ and $\beta([c],[c']) = k_{*}[c] + l_{*}[c']$, and $\partial_{*}[e] = [c]$ provided there are $f \in C_{p}(U)$ and $f' \in C_{p}(V)$ with $k_{\sharp}f + l_{\sharp}f'$ homologous to $e$ and $(i_{\sharp}c, -j_{\sharp}c) = (\partial f, \partial f')$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has generic long exact sequences of homological complexes but no singular-homology Mayer–Vietoris theorem for an open cover, nor the specific chain-level connecting map described here. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing clauses, and reconstruction from generic ingredients.

Definition/convention — singular cohomology groups

FC08-C18-U012 · Ch. 18, § Singular Cohomology; source L14244 · not formalized

For any topological space $M$ and abelian group $G$ one also defines the singular cohomology groups $H^{p}(M;G)$ with coefficients in $G$. Only $G = \mathbb{R}$ matters here, and then $H^{p}(M;\mathbb{R})$ is a real vector space naturally isomorphic to $\operatorname{Hom}(H_{p}(M),\mathbb{R})$, which may be taken as the definition. A continuous map $F \colon M \to N$ induces $F^{*} \colon H^{p}(N;\mathbb{R}) \to H^{p}(M;\mathbb{R})$ by $(F^{*}\gamma)[c] = \gamma(F_{*}[c])$, and the functorial properties carry over: $(G \circ F)^{*} = F^{*} \circ G^{*}$ and $(\operatorname{Id}_{M})^{*} = \operatorname{Id}$. So $p$th singular cohomology with real coefficients is a contravariant functor from the topological category to real vector spaces and linear maps.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has generic Hom/cochain-complex machinery, but no checked singular-cohomology functor with real coefficients identified naturally with Hom(H_p(M),ℝ) and no singular-cohomology Mayer–Vietoris theorem. The algebraic dual-complex ingredients do not supply Lee’s topological bridge. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing clauses, and reconstruction from generic ingredients.

Proposition 18.5

FC08-C18-U013 · Ch. 18, § Singular Cohomology; source L14248 · not formalized

groups, like the de Rham cohomology groups, define contravariant functors makes it much easier to compare the two. Proposition 18.5 (Properties of Singular Cohomology). (a) For any one-point space $\{ q \} , H ^ { p } ( \{ q \} ; \mathbb { R } )$ is trivial except when $p = 0$ , in which case it is 1-dimensional. (b) If $\{ M _ { j } \}$ is any collection of topological spaces and $\begin{array} { r } { M = \coprod _ { i } M _ { j } } \end{array}$ , then the inclusion maps $\iota _ { j } \colon M _ { j } \hookrightarrow M$ induce an isomorphism from $H ^ { p } ( M ; \mathbb { R } )$ to $\begin{array} { r } { \prod _ { i } H ^ { p } ( M _ { j } ; \mathbb { R } ) } \end{array}$ (c) Homotopy equivalent spaces have isomorphic singular cohomology groups.

Theorem 18.6

FC08-C18-U014 · Ch. 18, § Singular Cohomology; source L14260 · after FC08-C18-U011 · not formalized

Theorem 18.6 (Mayer–Vietoris for Singular Cohomology). Suppose M; U , and V satisfy the hypotheses of Theorem 18.4. The following sequence is exact: \[ \begin{array}{c} \dots \xrightarrow {\partial^ {*}} H ^ {p} (M; \mathbb {R}) \xrightarrow {k ^ {*} \oplus l ^ {*}} H ^ {p} (U; \mathbb {R}) \oplus H ^ {p} (V; \mathbb {R}) \xrightarrow {i ^ {*} - j ^ {*}} H ^ {p} (U \cap V; \mathbb {R}) \\ \xrightarrow {\partial^ {*}} H ^ {p + 1} (M; \mathbb {R}) \xrightarrow {k ^ {*} \oplus l ^ {*}} \dots , \end{array}\tag{18.5} \] where the maps $k ^ { * } \oplus l ^ { * }$ and $i ^ { * } - j ^ { * }$ are defined as in (17.8), and $\partial ^ { * }$ is defined by $\partial ^ { * } ( \gamma ) = \gamma \circ \partial _ { * }$

Definition/convention — smooth chain group in degree p

FC08-C18-U015 · Ch. 18, § Smooth Singular Homology; source L14274 · not formalized

If M is a smooth manifold, a smooth p-simplex in M is a map σ : Delta _p M that is smooth in the sense that it has a smooth extension to a neighborhood of each point. The subgroup of C _p ( M ) generated by smooth simplices is denoted by C _p ^∞ ( M ) and called the smooth chain group in degree p. Elements of this group, which are finite formal linear combinations of smooth simplices, are called smooth chains. Because the boundary of a smooth simplex is a smooth chain, we can define the pth smooth singular homology group of M to be the quotient group \[ H^{\infty}_{p}(M) = \frac{\operatorname{Ker}\big(\partial \colon C^{\infty}_{p}(M) \to C^{\infty}_{p-1}(M)\big)}{\operatorname{Im}\big(\partial \colon C^{\infty}_{p+1}(M) \to C^{\infty}_{p}(M)\big)}. \]

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib formalizes continuous singular chains but not Lee’s smooth-singular-chain subcomplex, smoothing homotopies compatible with all faces, or the smooth-vs-continuous singular homology isomorphism. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing clauses, and reconstruction from generic ingredients.

Theorem 18.7

FC08-C18-U016 · Ch. 18, § Smooth Singular Homology; source L14285 · not formalized

Theorem 18.7 (Smooth Singular vs. Singular Homology). For any smooth manifold M; the map $\iota _ { * } \colon H _ { p } ^ { \infty } ( M ) \to H _ { p } ( M )$ induced by inclusion is an isomorphi ere.

Lemma 18.8

FC08-C18-U017 · Ch. 18, § Smooth Singular Homology; source L14291 · not formalized

Lemma 18.8. Let M be a smooth manifold. For each integer $p \geq 0$ and each singular p-simplex $\sigma \colon \Delta _ { p } M$ ; there exists a continuous map $H _ { \sigma } \colon \Delta _ { p } \times I \to M$ such that the following properties hold: (i) $H _ { \sigma }$ is a homotopy from $\sigma ( x ) = H _ { \sigma } ( x , 0 )$ to a smooth p-simplex $\widetilde { \sigma } ( x ) =$ $H _ { \sigma } ( x , 1 )$ (ii) For each face map $F _ { i , p } \colon \Delta _ { p - 1 } \to \Delta _ { p }$ \[ H _ {\sigma \circ F _ {i, p}} = H _ {\sigma} \circ \big (F _ {i, p} \times \mathrm{Id} _ {I} \big),\tag{18.6} \] or more explicitly, \[ H _ {\sigma \circ F _ {i, p}} (x, t) = H _ {\sigma} \bigl (F _ {i, p} (x), t \bigr), \quad (x, t) \in \Delta_ {p - 1} \times I.\tag{18.7} \] (iii) If is a smooth p-simplex, then $H _ { \sigma }$ is the con rime}} d _ {0} = _ {B ^ {}} _ {0}.

Lemma 18.9

FC08-C18-U018 · Ch. 18, § Smooth Singular Homology; source L14373 · not formalized

Lemma 18.9. Let M be a smooth manifold, let be a geometric p-simplex in $\mathbb { R } ^ { n }$ and let $f \colon \partial \Delta \to M$ be a continuous map whose restriction to each individual boundary face of $\Delta$ is smooth. Then f is smooth when considered as a map from the entire boundary $\partial\Delta$.

Lemma 18.10

FC08-C18-U019 · Ch. 18, § The de Rham Theorem; source L14495 · in Mathlib

Lemma 18.10 (The Five Lemma). Consider the following commutative diagram of modules and linear maps: \[ \begin{array}{c} A _ {1} \xrightarrow {\alpha_ {1}} A _ {2} \xrightarrow {\alpha_ {2}} A _ {3} \xrightarrow {\alpha_ {3}} A _ {4} \xrightarrow {\alpha_ {4}} A _ {5} \\ \Big \downarrow f _ {1} \qquad \Big \downarrow f _ {2} \qquad \Big \downarrow f _ {3} \qquad \Big \downarrow f _ {4} \qquad \Big \downarrow f _ {5} \\ B _ {1} \xrightarrow {\beta_ {1}} B _ {2} \xrightarrow {\beta_ {2}} B _ {3} \xrightarrow {\beta_ {3}} B _ {4} \xrightarrow {\beta_ {4}} B _ {5}. \end{array} \] If the horizontal rows are exact and $f _ { 1 } , f _ { 2 } , f _ { 4 }$ , and $f _ { 5 }$ are isomorphisms, then $f _ { 3 }$

Formalized. Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean::ComposableArrows.isIso_of_epi_of_isIso_of_isIso_of_mono — Mathlib’s five lemma says that in a morphism between exact five-term diagrams in an abelian category, if the first vertical map is epi, the second and fourth are isomorphisms, and the fifth is mono, then the middle map is an isomorphism. Lee assumes the stronger first/fifth isomorphism hypotheses, so this directly implies his statement.

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

Definition/convention — integral of

FC08-C18-U020 · Ch. 18, § The de Rham Theorem; source L14505 · not formalized

Suppose M is a smooth manifold, ! is a closed p-form on M; and $\sigma$ is a smooth p-simplex in M . We define the integral of ! over to be \[ \int_ {\sigma} \omega = \int_ {\Delta_ {p}} \sigma^ {*} \omega . \] This makes sense because $\Delta _ { p }$ is a smooth p-submanifold with corners embedded in $\mathbb { R } ^ { p }$ , and it inherits the orientation of $\mathbb { R } ^ { p }$ . (Or we could just consider $\Delta _ { p }$ as a domain of integration in $\mathbb { R } ^ { p } .$ ) Observe that when $p = 1$ , this is the same as the line integral of ! over the smooth curve segment $\sigma \colon [ 0 , 1 ] \to M$ . If $\textstyle c = \sum _ { i = 1 } ^ { k } c _ { i } \sigma _ { i }$ is a smooth p-chain, the integral of ! over c is defined as \[ \int_ {c} \omega = \sum_ {i = 1} ^ {k} c _ {i} \int_ {\sigma_ {i}} \omega . \]

Not formalized. none; no complete checked declaration under strict bundle semantics — This row depends on the manifold differential-form integration/de Rham layer established absent in FC08 C14–C17. Mathlib’s continuous singular homology and generic homological algebra do not provide Stokes integration on smooth chains or the de Rham comparison map/theorem. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing clauses, and reconstruction from generic ingredients.

Theorem 18.12

FC08-C18-U021 · Ch. 18, § The de Rham Theorem; source L14517 · not formalized

Theorem 18.12 (Stokes’s Theorem for Chains). If c is a smooth p-chain in a smooth manifold M; and ! is a smooth $( p - 1 )$ -form on M; then \[ \int_ {\partial c} \omega = \int_ {c} d \omega . \]

Definition/convention — de Rham homomorphism

FC08-C18-U022 · Ch. 18, § The de Rham Theorem; source L14537 · after FC08-C18-U016 · not formalized

Using this theorem, we define a natural linear map J : H _d R ^p ( M ) → H ^p ( M ; ℝ ) called the de Rham homomorphism, as follows. For any [ ω ] ∈ H _d R ^p ( M ) and [ c ] ∈ H _p ( M ) ≅ H _p ^∞ ( M ) , we define I [ ω ] [ c ] = int_tilde(c) ω ,tag18.14 where tilde(c) is any smooth p-cycle representing the homology class Œc. This is well defined, because if tilde(c) , tilde(c) ^prime are smooth cycles representing the same homology class, then Theorem 18.7 guarantees that tilde(c) - tilde(c) ^prime = ∂ tilde(b) for some smooth ( p + 1 ) -chain tilde(b) , which implies $\int_{\widetilde{c}} \omega = \int_{\widetilde{c}'} \omega$ by Stokes’s theorem, so $\mathcal{I}[\omega][c] = \int_{\widetilde{c}} \omega$ is well defined.

Proposition 18.13

FC08-C18-U023 · Ch. 18, § The de Rham Theorem; source L14557 · not formalized

(Naturality of the de Rham Homomorphism). For a smooth manifold $M$ and $p \geq 0$, let $\mathcal{I} \colon H^{p}_{\mathrm{dR}}(M) \to H^{p}(M;\mathbb{R})$ be the de Rham homomorphism. (a) For a smooth map $F \colon M \to N$, the square with $F^{*} \colon H^{p}_{\mathrm{dR}}(N) \to H^{p}_{\mathrm{dR}}(M)$ on top, $F^{*} \colon H^{p}(N;\mathbb{R}) \to H^{p}(M;\mathbb{R})$ below and $\mathcal{I}$ down each side commutes. (b) If $U, V$ are open subsets of $M$ with $U \cup V = M$, the corresponding square with the connecting homomorphisms $\delta$ of the de Rham Mayer–Vietoris sequence on top and $\partial^{*}$ of the singular one below commutes.

Theorem 18.14

FC08-C18-U024 · Ch. 18, § The de Rham Theorem; source L14612 · not formalized

(de Rham). For every smooth manifold $M$ and every nonnegative integer $p$, the de Rham homomorphism $\mathcal{I} \colon H^{p}_{\mathrm{dR}}(M) \to H^{p}(M;\mathbb{R})$ is an isomorphism.

Definition/convention — de Rham basis for M

FC08-C18-U025 · Ch. 18, § The de Rham Theorem; source L14616 · not formalized

If M is any smooth manifold, let us call an open cover $\{ U _ { i } \}$ of M a de Rham cover if each subset $U _ { i }$ is a de Rham manifold, and every finite intersection $U _ { i _ { 1 } } \cap \cdots \cap U _ { i _ { k } }$ is de Rham. A de Rham cover that is also a basis for the topology of M is called a de Rham basis for M .