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

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 19 definitions, 15 theorems, 6 propositions, 4 lemmas, 10 corollaries, 1 example and 1 convention.

Of the 56 statements checked against Lean, 9 are formalized somewhere and 47 are not.

Status	Statements	Share	What it means
not formalized	47	84%	A documented search found no Lean statement of it anywhere.
in Mathlib	9	16%	Mathlib states and proves it.
checked in total	56

Which versions of Lean and Mathlib were searched

Canonical source block: FC08 Lee, Chapter 17, FC08-C17-U001–FC08-C17-U056, exactly 56 unique contiguous rows retrieved from FC08 — John M. Lee, Introduction to Smooth Manifolds through agent-memory.
Search order: project at 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 targeted indexed/current/external Lean searches.
C17 has 9 pinned mathlib rows and 47 dated unmatched rows. Positive rows are: U017, U026, U027, U047, U049, U052, U053, U054, U055.
The geometric de Rham layer is absent at P/H. Current Mathlib documentation exposes manifold vector fields, Riemannian geometry, smooth sections, and algebraic homological/cohomological complexes but no manifold de Rham cohomology module. A targeted current GitHub search likewise did not identify a compatible Mathlib-based de Rham implementation meeting the evidence floor.
U017 is independent of differential forms: contractible_iff_id_nullhomotopic is exactly Lee’s definition of contractibility as identity homotopic to a constant map.
U026–U027 are algebraic exactness and are owned directly by Function.Exact / moduleCat_exact_iff_range_eq_ker.
U047, U049, U052–U055 are generic homological algebra. Mathlib explicitly distinguishes CochainComplex (differentials increase degree) from ChainComplex (decrease degree), defines homology/cohomology as cycles modulo boundaries, gives induced homology maps, characterizes short exact complexes degreewise, and constructs the connecting morphism and long exact homology sequence. These rows therefore map without any de Rham bridge.
U048 remains unmatched despite adjacent exactness/complex APIs because its complete source bundle includes the strict non-converse “complex need not be exact”; no checked single owner packages that assertion, and a new counterexample would be reconstruction rather than reuse.
U046 was checked separately. P/H/current Mathlib contains Banach contraction fixed-point theory and one-dimensional interval fixed-point results, but no arbitrary-dimensional Brouwer closed-ball fixed-point theorem.
All remaining geometric rows depend essentially on the missing manifold de Rham complex, integration layer, or orientation-covering/degree machinery established absent in C14–C16; generic topological homotopy or algebraic complex infrastructure is not promoted through that gap.
N=2026-09-07 marks dated unmatched decisions. Strict whole-row semantics apply uniformly.

Definition/convention — de Rham cohomology groups

FC08-C17-U001 · Ch. 17; source L13307 · after FC08-C11-U064 · not formalized

Cohomology In Chapter 14 we defined closed and exact forms: a smooth differential form ! is closed if $d \omega = 0$ , and exact if it can be written $\omega = d \eta$ . Because d $\circ d = 0 .$ every exact form is closed. In this chapter, we explore the implications of the converse question: Is every closed form exact? The answer, in general, is no: in Example 11.48, for instance, we saw a 1-form on the punctured plane that is closed but not exact; the failure of exactness seemed to be a consequence of the “hole” in the center of the domain. For higher-degree forms, the question of which closed forms are exact depends on subtle topological properties of the manifold, connected with the existence of “holes” of higher dimensions. Making this dependence quantitative leads to a new set of invariants of smooth manifolds, called the de Rham cohomology groups, which are the subject of this chapter.

Not formalized. none; no complete checked declaration under strict bundle semantics — Pinned/current Mathlib has generic homological algebra and manifold smooth-map infrastructure, but no checked smooth-manifold de Rham complex: no manifold differential-form exterior derivative, closed/exact form quotient, pullback-induced de Rham functor, homotopy operator, Mayer–Vietoris de Rham sequence, compactly supported de Rham theory, integration degree theory, or the stated de Rham computations. Algebraic/topological ingredients alone do not own this geometric row. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing clauses, and substantive reconstruction from generic ingredients.

Convention/notation — de Rham cohomology group in degree p (

FC08-C17-U002 · Ch. 17, § The de Rham Cohomology Groups; source L13327 · not formalized

Let M be a smooth manifold with or without boundary, and let $p$ be a nonnegative integer. Because d $\Omega ^ { p } ( M ) \to \Omega ^ { p + 1 } ( M )$ is linear, its kernel and image are linear subspaces. We define \[ \mathcal {Z} ^ {p} (M) = \operatorname{Ker} \left(d: \Omega^ {p} (M) \rightarrow \Omega^ {p + 1} (M)\right) = \{\text { closed } p \text {-forms on } M \}, \] \[ \mathcal {B} ^ {p} (M) = \operatorname{Im} \left(d: \Omega^ {p - 1} (M) \rightarrow \Omega^ {p} (M)\right) = \{\text { exact } p \text {-forms on } M \}. \] By convention, we consider $\Omega ^ { p } ( M )$ to be the zero vector space when $p < 0$ or $p > n = \dim M$ ; so that, for example, $\mathcal { B } ^ { 0 } ( M ) = 0$ and $\mathcal { Z } ^ { n } ( M ) = \Omega ^ { n } ( M )$ The fact that every exact form is closed implies that $\mathcal { B } ^ { p } ( M ) \subseteq \mathcal { Z } ^ { p } ( M )$ . Thus, it makes sense to define the de Rham cohomology group in degree $\pmb { p }$ (or the pth de Rham group) of M to be the quotient vector space \[ H _ {\mathrm{dR}} ^ {p} (M) = \frac {\mathcal {Z} ^ {p} (M)}{\mathcal {B} ^ {p} (M)}. \] (It is a real vector space, and thus in particular a group under vector addition. Perhaps “de Rham cohomology space” would be a more appropriate term, but because most other cohomology theories produce only groups it is traditional to use the term group in this context as well, bearing in mind that these “groups” are actually real vector spaces.) It is clear that $H _ { \mathrm { d R } } ^ { p } ( M ) = 0$ for $p < 0$ or p > dim M; because $\Omega ^ { p } ( M ) = 0$ in those cases.

Example 17.1

FC08-C17-U003 · Ch. 17, § The de Rham Cohomology Groups; source L13347 · after FC08-C11-U064, FC08-C11-U066 · not formalized

Example 17.1. The fact that there is a closed 1-form on $\mathbb { R } ^ { 2 } \setminus \{ 0 \}$ that is not exact means that $H _ { \mathrm { d R } } ^ { 1 } \left( \mathbb { R } ^ { 2 } \setminus \{ 0 \} \right) \neq 0$ (see Example 11.48). On the other hand, the Poincaré lemma for 1-forms (Theorem 11.49) implies that $H _ { \mathrm { d R } } ^ { 1 } ( U ) = 0$ for any star-shaped open subset $U \subseteq \mathbb{R}^{n}$.

Definition/convention — cohomology class of

FC08-C17-U004 · Ch. 17, § The de Rham Cohomology Groups; source L13349 · not formalized

for any star-shaped open subset $U \subseteq \mathbb { R } ^ { n }$ The first order of business is to show that the de Rham groups are diffeomorphism invariants. For any closed $p \mathrm { - f o r m } \ \omega$ on M; we let Œ! denote the equivalence class of ! in $H _ { \mathrm { d R } } ^ { p } ( M )$ , called the cohomology class of !. If $[ \omega ] = [ \omega ^ { \prime } ]$ (that is, if ! and $\omega ^ { \prime }$ differ by an exact form), we say that ! and $\omega ^ { \prime }$

Proposition 17.2

FC08-C17-U005 · Ch. 17, § The de Rham Cohomology Groups; source L13351 · not formalized

(Induced Cohomology Maps). For any smooth map $F \colon M \to N$ between smooth manifolds with or without boundary, the pullback $F^{*} \colon \Omega^{p}(N) \to \Omega^{p}(M)$ carries $\mathcal{Z}^{p}(N)$ into $\mathcal{Z}^{p}(M)$ and $\mathcal{B}^{p}(N)$ into $\mathcal{B}^{p}(M)$, so it descends to a linear map $F^{*} \colon H^{p}_{\mathrm{dR}}(N) \to H^{p}_{\mathrm{dR}}(M)$, the induced cohomology map. (a) If $G \colon N \to P$ is another smooth map, then $(G \circ F)^{*} = F^{*} \circ G^{*} \colon H^{p}_{\mathrm{dR}}(P) \to H^{p}_{\mathrm{dR}}(M)$. (b) $\operatorname{Id}^{*}$ is the identity map of $H^{p}_{\mathrm{dR}}(M)$.

Corollary 17.3

FC08-C17-U006 · Ch. 17, § The de Rham Cohomology Groups; source L13371 · not formalized

Corollary 17.3 (Functoriality). For any integer p, the assignment $M \mapsto H _ { \mathrm { d R } } ^ { p } ( M )$ $F \mapsto F ^ { * }$ is a contravariant functor from the category of smooth manifolds with boundary to the category of real vector space rves with fewer than m such points.

Corollary 17.4

FC08-C17-U007 · Ch. 17, § The de Rham Cohomology Groups; source L13373 · not formalized

Corollary 17.4 (Diffeomorphism Invariance of de Rham Cohomology). $D i f f e o -$ morphic smooth manifolds (with or without boundary) have isomorphic de Rham cohomology groups. ##

Proposition 17.5

FC08-C17-U008 · Ch. 17, § Elementary Computations; source L13379 · not formalized

Proposition 17.5 (Cohomology of Disjoint Unions). Let $\{ M _ { j } \}$ be a countable collection of smooth n-manifolds with or without boundary, and let $\begin{array} { r } { M = \coprod _ { j } M _ { j } } \end{array}$ . For each p, the inclusion maps $\iota _ { j } \colon M _ { j } \hookrightarrow M$ induce an isomorphism from $H _ { \mathrm { d R } } ^ { p } ( M )$ to the direct product space = (_ {} - _ { _ {0}} ) + (_ { _ {1}} - _ {} ) \ & = _ { _ {1}} - _ { _ {0}} .

Proposition 17.6

FC08-C17-U009 · Ch. 17, § Elementary Computations; source L13393 · not formalized

Proposition 17.6 (Cohomology in Degree Zero). If M is a connected smooth manifold with or without boundary, then $H _ { \mathrm { d R } } ^ { 0 } ( M )$ is equal to the space of constant functions and is therefore 1-dimensio Suppose $( M , g )$ is an oriented Riemannian manifold with or without boundary, and let $\omega _ { g }$ denote its Riemannian volume form.

Corollary 17.7

FC08-C17-U010 · Ch. 17, § Elementary Computations; source L13397 · not formalized

a n t s } }$ Corollary 17.7 (Cohomology of Zero-Manifolds). Suppose M is a manifold of dimension 0. Then $H _ { \mathrm { d R } } ^ { 0 } ( M )$ is a direct product of 1-dimensional vector spaces, one for each point of M; and all other de Rham cohomology groups of M are zero. Proof. The statement about $

Definition/convention — homotopy operator between F

FC08-C17-U011 · Ch. 17, § Homotopy Invariance; source L13425 · not formalized

general, if $F , G \colon M \to N$ are smooth maps, a collection of linear maps $h \colon \Omega ^ { p } ( N ) \to \Omega ^ { p - 1 } ( M )$ such that (17.3) is satisfied for all $\omega$ is called a homotopy operator between $F ^ { * }$ and $G ^ { * }$ . (The term cochain homotopy is used frequently in the algebraic topology literature.) The next proposition follows immediately from the argument in the preceding nian n-manifold (with or without boundary).

Proposition 17.8

FC08-C17-U012 · Ch. 17, § Homotopy Invariance; source L13427 · not formalized

Suppose $M$ and $N$ are smooth manifolds with or without boundary. If $F, G \colon M \to N$ are smooth maps and there exists a homotopy operator between the pullbacks $F^{*}$ and $G^{*}$, then the induced cohomology maps $F^{*}, G^{*} \colon H^{p}_{\mathrm{dR}}(N) \to H^{p}_{\mathrm{dR}}(M)$ are equal.

Lemma 17.9

FC08-C17-U013 · Ch. 17, § Homotopy Invariance; source L13437 · not formalized

Lemma 17.9 (Existence of a Homotopy Operator). For any smooth manifold M with or without boundary, there exists a homotopy operator between the two maps $i _ { 0 } ^ { * } , i _ { 1 } ^ { * } \colon \Omega ^ { * } ( M \times I ) \to \Omega ^ { * } ( M )$

Proposition 17.10

FC08-C17-U014 · Ch. 17, § Homotopy Invariance; source L13477 · not formalized

Proposition 17.10. Suppose M and N are smooth manifolds with or without boundary, and F; G $M N$ are homotopic smooth maps. For every p, the induced cohomology maps $F ^ { * } , G ^ { * } \colon H _ { \mathrm { d R } } ^ { p } ( N ) { \stackrel { - } { \to } } H _ { \mathrm { d R } } ^ { p } ( M )$

Theorem 17.11

FC08-C17-U015 · Ch. 17, § Homotopy Invariance; source L13487 · not formalized

Theorem 17.11 (Homotopy Invariance of de Rham Cohomology). If M and N are homotopy equivalent smooth manifolds with or without boundary, then $H _ { \mathrm { d R } } ^ { p } ( M ) \cong H _ { \mathrm { d R } } ^ { p } ( N )$ for each p. The isomorphisms are induced by any smooth homotopy equivalence F $M \to N$

Corollary 17.12

FC08-C17-U016 · Ch. 17, § Homotopy Invariance; source L13504 · not formalized

Corollary 17.12 (Topological Invariance of de Rham Cohomology). The de Rham cohomology groups are topological invariants: if M and N are homeomorphic smooth manifolds with or without boundary, then their de Rham cohomology groups are isomorphic. T

Definition/convention — contractible

FC08-C17-U017 · Ch. 17, § Computations Using Homotopy Invariance; source L13510 · in Mathlib

We can use homotopy invariance to compute a number of de Rham groups. We begin with the simplest case of homotopy equivalence. A topological space X is said to be contractible if the identity map of X is homotopic to a constant map.

Formalized. Mathlib/Topology/Homotopy/Contractible.lean::ContractibleSpace, contractible_iff_id_nullhomotopic — contractible_iff_id_nullhomotopic states exactly that a space is contractible iff its identity map is homotopic to a constant map (Nullhomotopic); ContractibleSpace packages the equivalent homotopy-equivalence-to-a-point formulation.

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

Theorem 17.13

FC08-C17-U018 · Ch. 17, § Computations Using Homotopy Invariance; source L13512 · not formalized

Theorem 17.13 (Cohomology of Contractible Manifolds). If M is a contractible smooth manifold with or without boundary, then $H _ { \mathrm { d R } } ^ { p } ( M ) = 0 f o r \ p \geq 1$

Definition/convention — star-shaped

FC08-C17-U019 · Ch. 17, § Computations Using Homotopy Invariance; source L13518 · after FC08-C11-U066 · not formalized

Theorem 11.49 showed that every closed 1-form on a star-shaped open subset of $\mathbb{R}^{n}$ is exact, where $U \subseteq \mathbb{R}^{n}$ is star-shaped if there is $c \in U$ such that the segment from $c$ to $x$ lies in $U$ for every $x \in U$. The next theorem generalizes this to forms of all degrees, and despite the apparent specialness of star-shaped domains it is one of the most important facts about de Rham cohomology.

Theorem 17.14

FC08-C17-U020 · Ch. 17, § Computations Using Homotopy Invariance; source L13520 · not formalized

Theorem 17.14 (The Poincaré Lemma). If U is a star-shaped open subset of R or $\mathbb { H } ^ { n }$ , then $H _ { \mathrm { d R } } ^ { p } ( U ) = 0 f o r \ p \geq 1$ Proof.

Corollary 17.15

FC08-C17-U021 · Ch. 17, § Computations Using Homotopy Invariance; source L13528 · not formalized

Corollary 17.15 (Local Exactness of Closed Forms). Let M be a smooth manifold with or without boundary. Each point of M has a neighborhood on which every closed form is exact.

Corollary 17.16

FC08-C17-U022 · Ch. 17, § Computations Using Homotopy Invariance; source L13532 · not formalized

Corollary 17.16 (Cohomology of Euclidean Spaces and Half-Spaces). For any and $p \geq 1 , H _ { \mathrm { d R } } ^ { p } \left( \mathbb { R } ^ { n } \right) = 0$ and $H _ { \mathrm { d R } } ^ { \bar { p } } \left( \mathbb { H } ^ { n } \right) = 0$

Definition/convention — linear map Phi

FC08-C17-U023 · Ch. 17, § Computations Using Homotopy Invariance; source L13536 · not formalized

Both $\mathbb { R } ^ { n }$ and $\mathbb { H } ^ { n }$ are star-shaped. Another case in which we can say quite a lot about de Rham cohomology is in degree 1. Suppose M is a connected smooth manifold and $q$ is any point in $M$ Let Hom $\left( \pi _ { 1 } ( \boldsymbol { M } , \boldsymbol { q } ) , \mathbb { R } \right)$ denote the set of group homomorphisms from $\pi _ { 1 } ( M , q )$ to the additive group R; it is a vector space under pointwise addition of homomorphisms and multiplication by constants. We define a linear map $\Phi \colon H _ { \mathrm { d R } } ^ { 1 } ( M ) \to$ $\mathrm { H o m } \big ( \pi _ { 1 } ( M , q ) , \mathbb { R } \big )$ as follows: given a cohomology class $[ \omega ] \in H _ { \mathrm { d R } } ^ { 1 } ( \bar { M } )$ , define $\phi [ \omega ] \colon \pi _ { 1 } ( M , q ) \to \mathbb { R }$ by \[ \varPhi [ \omega ] [ \gamma ] = \int_ {\widetilde {\gamma}} \omega , \] where $[ \gamma ]$ is any path homotopy class in $\pi _ { 1 } ( M , q )$ , and $\widetilde { \gamma }$ is any piecewise smooth curve representing the same path class. Theorem 17.17 (First Cohomology and the Fundamental Group). Suppose M is a connected smooth manifold. For each $q \in M$ ; the linear map $\Phi \colon H _ { \mathrm { d R } } ^ { 1 } ( M ) \to$ Hom $\left( \pi _ { 1 } ( M , q ) , \mathbb { R } \right)$

Theorem 17.17

FC08-C17-U024 · Ch. 17, § Computations Using Homotopy Invariance; source L13544 · not formalized

Theorem 17.17 (First Cohomology and the Fundamental Group). Suppose M is a connected smooth manifold. For each $q \in M$ ; the linear map $\Phi \colon H _ { \mathrm { d R } } ^ { 1 } ( M ) \to$ Hom $\left( \pi _ { 1 } ( M , q ) , \mathbb { R } \right)$ is wel ]{} ^ {1} (M) ^ {2} (M) ^ {3} (M).

Corollary 17.18

FC08-C17-U025 · Ch. 17, § Computations Using Homotopy Invariance; source L13566 · not formalized

Corollary 17.18. If M is a connected smooth manifold with finite fundamental group, then $H _ { \mathrm { d R } } ^ { 1 } ( M ) = 0$

Definition/convention — exact

FC08-C17-U026 · Ch. 17, § The Mayer–Vietoris Theorem; source L13602 · in Mathlib

In the statement of the Mayer–Vietoris theorem, we will use the following standard algebraic terminology. Suppose we are given a sequence of vector spaces and linear maps: \[ \dots \rightarrow V ^ {p - 1} \xrightarrow {F _ {p - 1}} V ^ {p} \xrightarrow {F _ {p}} V ^ {p + 1} \xrightarrow {F _ {p + 1}} V ^ {p + 2} \rightarrow \dots .\tag{17.9} \] Such a sequence is said to be exact if the image of each map is equal to the kernel of the next: for each $p$ \[ \operatorname{Im} F _ {p - 1} = \operatorname{Ker} F _ {p}. \]

Formalized. Mathlib/Algebra/Exact/Basic.lean::Function.Exact; Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean::ShortComplex.moduleCat_exact_iff_range_eq_ker — Function.Exact f g is the exact-pair predicate, and for module/linear maps moduleCat_exact_iff_range_eq_ker identifies categorical exactness with range f = ker g, exactly Lee’s degreewise definition.

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

Definition/convention — exact

FC08-C17-U027 · Ch. 17, § The Mayer–Vietoris Theorem; source L13608 · in Mathlib

Such a sequence is said to be exact if the image of each map is equal to the kernel of the next: for each p

Formalized. Mathlib/Algebra/Exact/Basic.lean::Function.Exact; Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean::ShortComplex.moduleCat_exact_iff_range_eq_ker — This repeated source definition is literally Mathlib’s exact-pair condition: image/range of one linear map equals the kernel of the next.

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

Theorem 17.20

FC08-C17-U028 · Ch. 17, § The Mayer–Vietoris Theorem; source L13614 · not formalized

Theorem 17.20 (Mayer–Vietoris). Let M be a smooth manifold with or without boundary, and let U , V be open subsets of M whose union is M . For each $p _ { : }$ , there is a linear map ı $H _ { \mathrm { d R } } ^ { p } ( U \bar { \cap } V ) \to H _ { \mathrm { d R } } ^ { p + 1 } ( M )$ such that the following sequence, called the Mayer–Vietoris sequence for the open cover $\{ U , V \}$ , is exact: \[ \begin{array}{c} \dots \stackrel {{\delta}} {{\to}} H _ {\mathrm{dR}} ^ {p} (M) \xrightarrow {k ^ {*} \oplus l ^ {*}} H _ {\mathrm{dR}} ^ {p} (U) \oplus H _ {\mathrm{dR}} ^ {p} (V) \xrightarrow {i ^ {*} - j ^ {*}} H _ {\mathrm{dR}} ^ {p} (U \cap V) \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qend{array}\tag{17.10} \] Computations Using the Mayer–Vietoris Theorem Using the Mayer–Vietoris theorem, it is a simple matter to compute all of the de Rham cohomology groups of spheres. Theorem 17.21 (Cohomology

Theorem 17.21

FC08-C17-U029 · Ch. 17, § The Mayer–Vietoris Theorem; source L13624 · not formalized

(Cohomology of Spheres). For $n \geq 1$ the de Rham cohomology groups of $\mathbb{S}^{n}$ are \[ H^{p}_{\mathrm{dR}}(\mathbb{S}^{n}) \cong \begin{cases} \mathbb{R} & \text{if } p = 0 \text{ or } p = n, \\ 0 & \text{if } 0 < p < n, \end{cases} \tag{17.11} \] and the cohomology class of any smooth orientation form is a basis for $H^{n}_{\mathrm{dR}}(\mathbb{S}^{n})$.

Corollary 17.23

FC08-C17-U030 · Ch. 17, § The Mayer–Vietoris Theorem; source L13646 · not formalized

(Cohomology of Punctured Euclidean Space). Suppose $n \geq 2$, $x \in \mathbb{R}^{n}$ and $M = \mathbb{R}^{n} \setminus \{x\}$. The only nontrivial de Rham groups of $M$ are $H^{0}_{\mathrm{dR}}(M)$ and $H^{n-1}_{\mathrm{dR}}(M)$, both 1-dimensional. A closed $(n-1)$-form $\eta$ on $M$ is exact if and only if $\int_{S} \eta = 0$ for some, hence every, $(n-1)$-dimensional sphere $S \subseteq M$ centered at $x$.

Corollary 17.25

FC08-C17-U031 · Ch. 17, § The Mayer–Vietoris Theorem; source L13657 · not formalized

Suppose $n \geq 2$, $U \subseteq \mathbb{R}^{n}$ is open and $x \in U$. Then $H^{n-1}_{\mathrm{dR}}(U \setminus \{x\}) \neq 0$.

Theorem 17.26

FC08-C17-U032 · Ch. 17, § The Mayer–Vietoris Theorem; source L13663 · not formalized

Theorem 17.26 (Topological Invariance of Dimension). A nonempty n-dimensional topological manifold cannot be homeomorphic to an m-dimensional manifold unless $m = n$

Lemma 17.27

FC08-C17-U033 · Ch. 17, § The Mayer–Vietoris Theorem; source L13669 · not formalized

Lemma 17.27 (Poincaré Lemma with Compact Support). Let $n \geq p \geq 1$ , and suppose ! is a compactly supported closed p-form on $\mathbb { R } ^ { n }$ . If $p = n$ , suppose in addition that $\textstyle \int _ { \mathbb { R } ^ { n } } \omega = 0$ . Then there exists a compactly supported smooth $( p - 1 )$ form on $\mathbb { R } ^ { n }$ such that $\omega = d\eta$.

Definition/convention — generalization of the de Rham cohomology groups using only co

FC08-C17-U034 · Ch. 17, § The Mayer–Vietoris Theorem; source L13701 · not formalized

For some purposes it is useful to define a generalization of the de Rham cohomology groups using only compactly supported forms. Let M be a smooth manifold with or without boundary and let Omega _c ^p ( M ) denote the vector space of compactly supported smooth p-forms on M . The pth compactly supported de Rham cohomology group of M is the quotient space \[ H^{p}_{c}(M) = \frac{\operatorname{Ker}\big(d \colon \Omega^{p}_{c}(M) \to \Omega^{p+1}_{c}(M)\big)}{\operatorname{Im}\big(d \colon \Omega^{p-1}_{c}(M) \to \Omega^{p}_{c}(M)\big)}. \]

Theorem 17.28

FC08-C17-U035 · Ch. 17, § The Mayer–Vietoris Theorem; source L13709 · not formalized

Theorem 17.28 (Compactly Supported Cohomology of $\mathbb { R } ^ { n } )$ . For $n \geq 1$ , the compactly supported de Rham cohomology groups $o f \mathbb { R } ^ { n }$ are \[ H _ {c} ^ {p} \left(\mathbb {R} ^ {n}\right) \cong \left\{ \begin{array}{l l} 0 & \text { if } 0 \leq p < n, \\ \mathbb {R} & \text { if } p = n. \end{array} \right. \]

Definition/convention — source terminology/construction

FC08-C17-U036 · Ch. 17, § The Mayer–Vietoris Theorem; source L13717 · not formalized

In general, a smooth map need not pull back compactly supported forms to compactly supported ones, so it does not induce a map on compactly supported cohomology. However, a proper map does pull back compactly supported forms to compactly supported ones, so for a proper smooth map $F \colon M \to N$ there is an induced cohomology map $F ^ { * } \colon H _ { c } ^ { p } ( N ) \to H _ { c } ^ { p } ( M )$

Theorem 17.30

FC08-C17-U037 · Ch. 17, § The Mayer–Vietoris Theorem; source L13729 · not formalized

Theorem 17.30 (Top Cohomology, Orientable Compact Support Case). If M is a connected oriented smooth n-manifold, then the integration map $I \colon H _ { c } ^ { n } ( M ) \to \mathbb { R }$ is an isomorphism, so $H _ { c } ^ { n } ( M )$ is 1-dim integral of $f$ over M is defined to be $\textstyle { \int _ { M } f d V _ { g } }$ .

Theorem 17.31

FC08-C17-U038 · Ch. 17, § The Mayer–Vietoris Theorem; source L13756 · not formalized

Theorem 17.31 (Top Cohomology, Orientable Compact Case). If M is a compact connected orientable smooth n-manifold, then $H _ { \mathrm { d R } } ^ { n } ( M )$ is 1-dimensional, and is spanned by the cohomology class of any smooth orientation ## Problems 16-1.

Theorem 17.32

FC08-C17-U039 · Ch. 17, § The Mayer–Vietoris Theorem; source L13760 · not formalized

Theorem 17.32 (Top Cohomology, Orientable Noncompact Case). If M is a noncompact connected orientable smooth n-manifold, then $H _ { \mathrm { d R } } ^ { n } ( M ) = 0$

Lemma 17.33

FC08-C17-U040 · Ch. 17, § The Mayer–Vietoris Theorem; source L13768 · not formalized

Lemma 17.33. Suppose M is a connected nonorientable smooth manifold and $\widehat { \pi } \colon \widehat { M } \to M$ is its orientation covering. For each p, the induced cohomology maps $\widehat { \pi } ^ { * } \colon H _ { \mathrm { d R } } ^ { p } ( M ) \to H _ { \mathrm { d R } } ^ { p } \bigl ( \widehat { M } \bigr ) a n d \widehat { \pi } ^ { * } \colon \tilde { H _ { c } ^ { p } } ( M ) \to \tilde { H _ { c } ^ { p } } \bigl ( \widehat { M } \bigr )$ are injective. Proof. First, we prove the lemma for compactly supported cohomology.

Theorem 17.34

FC08-C17-U041 · Ch. 17, § The Mayer–Vietoris Theorem; source L13798 · not formalized

(Top Cohomology, Nonorientable Case). If $M$ is a connected nonorientable smooth $n$-manifold, then $H^{n}_{c}(M) = 0$ and $H^{n}_{\mathrm{dR}}(M) = 0$.

Theorem 17.35

FC08-C17-U042 · Ch. 17, § Degree Theory; source L13822 · not formalized

Theorem 17.35 (Degree of a Smooth Map). Suppose M and N are compact, connected, oriented, smooth manifolds of dimension n, and $F \colon M \to N$ is a smooth map. There exists a unique integer k, called the degree of F , that satisfies both of the following conditions. (a) For every smooth n-form ! on N , \[ \int_ {M} F ^ {*} \omega = k \int_ {N} \omega . \] (b) $H q \in N$ is a regular value of F , then \[ k = \sum_ {x \in F ^ {- 1} (q)} \operatorname{sgn} (x), \] where $\operatorname { s g n } ( x ) = + 1 i f d F _ { x }$ is orientation-preserving, and 1

Proposition 17.36

FC08-C17-U043 · Ch. 17, § Degree Theory; source L13854 · not formalized

Proposition 17.36 (Properties of the Degree). Suppose M; N , and P are compact, connected, oriented, smooth n-manifolds. (a) If $F \colon M \to N$ and $G \colon N \to P$ are both smooth maps, then deg $( G \circ F ) =$ $( \deg G ) ( \deg F )$ (b) If $F \colon M \to N$ is a diffeomorphism, then deg $F = + 1 \ i f \ F$ is orientationpreserving and 1 if it is orientation-reversing. (c) If two smooth maps $F _ { 0 } , F _ { 1 } \colon M \to N$ are homotopic, then they have the same degree.

Definition/convention — degree of a continuous map F

FC08-C17-U044 · Ch. 17, § Degree Theory; source L13864 · not formalized

This proposition allows us to define the degree of a continuous map $F \colon M \to N$ between compact, connected, oriented, smooth n-manifolds, by letting deg $F$ be the degree of any smooth map that is homotopic to $F$ . The Whitney approximation theorem guarantees that there is such a map, and the preceding proposition guarantees that the degree is the same for every map homotopic to $F$.

Theorem 17.38

FC08-C17-U045 · Ch. 17, § Degree Theory; source L13868 · not formalized

Theorem 17.38. Suppose N is a compact, connected, oriented, smooth n-manifold, and X is a compact, oriented, smooth $( n + 1 )$ -manifold with connected boundary. $I f ~ f \colon \partial X \to N$ is a continuous map that has a continuous extension to $X$ , then deg tain Riemannian metrics are not flat.

Theorem 17.39

FC08-C17-U046 · Ch. 17, § Degree Theory; source L13880 · not formalized

(Brouwer Fixed-Point Theorem). Every continuous map from $\overline{\mathbb{B}}^{n}$ to itself has a fixed point.

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted P/H/current searches find Banach fixed-point and one-dimensional interval fixed-point theorems, but no Brouwer fixed-point theorem for a closed Euclidean ball in arbitrary finite dimension. No complete owner was found. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing clauses, and substantive reconstruction from generic ingredients.

Definition/convention — a complex

FC08-C17-U047 · Ch. 17, § Proof of the Mayer–Vietoris Theorem; source L13908 · in Mathlib

(In all of our applications, the ring will be either $\mathbb { Z } .$ , in which case we are looking at abelian groups and homomorphisms, or R, in which case we have vector spaces and linear maps. The terminology of modules is just a convenient way to combine the two cases.) Such a sequence is said to be a complex if the composition of any two successive applications of d is the zero map: \[ d \circ d = 0 \colon A ^ {p} \to A ^ {p + 2} \quad \mathrm{foreach} p. \]

Formalized. Mathlib/Algebra/Homology/HomologicalComplex.lean::HomologicalComplex, CochainComplex, ChainComplex, HomologicalComplex.d_comp_d — HomologicalComplex is a graded sequence with differential satisfying d ≫ d = 0; CochainComplex specializes to increasing indices and ChainComplex to decreasing indices. This is exactly Lee’s abstract complex convention.

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

Definition/convention — exact sequence

FC08-C17-U048 · Ch. 17, § Proof of the Mayer–Vietoris Theorem; source L13914 · not formalized

Just as in the case of vector spaces, such a sequence of modules is called an exact sequence if the image of each d is equal to the kernel of the next. Clearly, every exact sequence is a complex, but the converse need not be true.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib formalizes exact pairs and complexes and proves exact pairs have zero composite, but this bundled row also asserts that the converse fails. No single checked declaration packages the definition together with that non-converse; supplying a counterexample here would be reconstruction rather than reuse. Strict whole-row semantics reject proper subsets, unbridged alternative models, missing clauses, and substantive reconstruction from generic ingredients.

Definition/convention — pth cohomology group of A to be the quotient module

FC08-C17-U049 · Ch. 17, § Proof of the Mayer–Vietoris Theorem; source L13916 · in Mathlib

Let us denote the sequence (17.12) by A * . If it is a complex, then the image of each map d is contained in the kernel of the next, so we define the pth cohomology group of A * to be the quotient module \[ H^{p}(A^{*}) = \frac{\operatorname{Ker}(d \colon A^{p} \to A^{p+1})}{\operatorname{Im}(d \colon A^{p-1} \to A^{p})}. \]

Formalized. Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean::HomologicalComplex.cycles, HomologicalComplex.homology — For a homological/cohomological complex in an abelian category, cycles is the kernel object and homology is its quotient by boundaries (implemented as the homology of the adjacent short complex), exactly ker d / im d.

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

Definition/convention — source terminology/construction

FC08-C17-U050 · Ch. 17, § Proof of the Mayer–Vietoris Theorem; source L13922 · not formalized

A complex is a sequence of vector spaces and linear maps whose consecutive composites vanish, and its cohomology measures the failure of exactness. The obvious example is the de Rham complex of a smooth $n$-manifold $M$, \[ 0 \to \Omega^{0}(M) \xrightarrow{\ d\ } \cdots \xrightarrow{\ d\ } \Omega^{p}(M) \xrightarrow{\ d\ } \Omega^{p+1}(M) \xrightarrow{\ d\ } \cdots \xrightarrow{\ d\ } \Omega^{n}(M) \to 0, \] whose cohomology groups are the de Rham groups of $M$. In algebraic topology such a complex is called a cochain complex, a chain complex being the same with maps of decreasing index, \[ \cdots \to A_{p+1} \xrightarrow{\ \partial\ } A_{p} \xrightarrow{\ \partial\ } A_{p-1} \to \cdots. \]

Definition/convention — cochain complex

FC08-C17-U051 · Ch. 17, § Proof of the Mayer–Vietoris Theorem; source L13928 · not formalized

whose cohomology groups are the de Rham groups of $M$ . (In algebraic topology, a complex as we have defined it is usually called a cochain complex, while a chain complex is defined similarly except that the maps go in the direction of decreasing indices: \[ \dots \to A _ {p + 1} \stackrel {\partial} {\to} A _ {p} \stackrel {\partial} {\to} A _ {p - 1} \to \dots . \] In that case, the term homology is used in place of cohomology.)

Definition/convention — cochain map

FC08-C17-U052 · Ch. 17, § Proof of the Mayer–Vietoris Theorem; source L13936 · in Mathlib

If $A ^ { * }$ and $B ^ { * }$ are complexes, a cochain map from $A ^ { * }$ to $B ^ { * }$ , denoted by $F \colon A ^ { * } \to B ^ { * }$ { p } B ^ { p }$ (it is easiest to use the same symbol for all of the maps) such that the following diagram commutes for each $p \colon$ \[ \begin{array}{c} \dots \longrightarrow A ^ {p} \xrightarrow {d} A ^ {p + 1} \longrightarrow \dots \\ F \Big \downarrow \qquad \qquad \qquad \Big \downarrow F \\ \dots \longrightarrow B ^ {p} \xrightarrow {d} B ^ {p + 1} \longrightarrow \dots . \end{array} \] The fact that $

Formalized. Mathlib/Algebra/Homology/HomologicalComplex.lean::HomologicalComplex.Hom, CochainComplex — A morphism of CochainComplex objects is a degreewise family of maps satisfying the differential-commuting condition, exactly Lee’s cochain map.

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

Definition/convention — chain map

FC08-C17-U053 · Ch. 17, § Proof of the Mayer–Vietoris Theorem; source L13942 · in Mathlib

Because $F \circ d = d \circ F$, any cochain map induces a linear map on cohomology $F^{*} \colon H^{p}(A^{*}) \to H^{p}(B^{*})$ for each $p$, as for de Rham cohomology. A map between chain complexes satisfying the analogous relations is a chain map, and the same argument shows it induces a linear map on homology.

Formalized. Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean::HomologicalComplex.homologyMap, HomologicalComplex.homologyFunctor, HomologicalComplex.homologyMap_comp, HomologicalComplex.homologyMap_id — Every chain/cochain-complex morphism induces homologyMap in each degree; homologyFunctor, homologyMap_comp, and homologyMap_id give the stated functoriality. The same HomologicalComplex interface covers both chain and cochain shapes.

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

Definition/convention — source terminology/construction

FC08-C17-U054 · Ch. 17, § Proof of the Mayer–Vietoris Theorem; source L13944 · in Mathlib

homology.) A short exact sequence of complexes consists of three complexes $A ^ { * } , B ^ { * } , C ^ { * }$ together with cochain maps {*} \[ such that each sequence \] 0 A ^ {p} B ^ {p} C {p} \[ is exact. This means that F is injective, G is surjective, and Im $F = \operatorname { K e r } G$ Lemma 17.40 (The Zigzag Lemma). Given a short exact sequence of complexes as above, for each p there is a linear map \]

Formalized. Mathlib/Algebra/Homology/HomologicalComplexAbelian.lean::HomologicalComplex.shortExact_iff_degreewise_shortExact; Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean::CategoryTheory.ShortComplex.ShortExact — A short complex of complexes is short exact iff it is short exact in every degree. In module categories ShortExact means the first map is injective, the second surjective, and the middle pair exact, matching Lee’s degreewise definition.

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

Lemma 17.40

FC08-C17-U055 · Ch. 17, § Proof of the Mayer–Vietoris Theorem; source L13958 · in Mathlib

(The Zigzag Lemma). Given a short exact sequence of complexes, for each $p$ there is a linear map $\delta \colon H^{p}(C^{*}) \to H^{p+1}(A^{*})$, the connecting homomorphism, for which the sequence \[ \cdots \xrightarrow{\ \delta\ } H^{p}(A^{*}) \xrightarrow{\ F^{*}\ } H^{p}(B^{*}) \xrightarrow{\ G^{*}\ } H^{p}(C^{*}) \xrightarrow{\ \delta\ } H^{p+1}(A^{*}) \xrightarrow{\ F^{*}\ } \cdots \tag{17.13} \] is exact.

Formalized. Mathlib/Algebra/Homology/HomologySequence.lean::CategoryTheory.ShortComplex.ShortExact.δ, CategoryTheory.ShortComplex.ShortExact.homology_exact₁, CategoryTheory.ShortComplex.ShortExact.homology_exact₂, CategoryTheory.ShortComplex.ShortExact.homology_exact₃ — For every short exact sequence of homological complexes, Mathlib constructs the connecting morphism δ; the three homology_exact theorems give the consecutive exact pieces of the resulting long exact homology/cohomology sequence. Applied to a cochain shape, this is Lee’s Zigzag Lemma.

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

Corollary 17.42

FC08-C17-U056 · Ch. 17, § Proof of the Mayer–Vietoris Theorem; source L14039 · not formalized

Corollary 17.42. The connecting homomorphism in the Mayer–Vietoris sequence, $\delta \colon H _ { \mathrm { d R } } ^ { p } ( \dot { U } \cap V ) \to H _ { \mathrm { d R } } ^ { p + 1 } ( M )$ , is defined as follows. For each $\omega \in \mathcal { Z } ^ { p } ( U \cap V )$ there are p-forms $\eta \in \Omega ^ { p } ( U )$ and $\eta ^ { \prime } \in \Omega ^ { p } ( V )$ / such that $\omega = \eta | _ { U \cap V } - \eta ^ { \prime } | _ { U \cap V } ;$ and then $\delta [ \omega ] = [ \sigma ]$ , where is the $( p + 1 )$ /-form on M that is equal to d on U and to d on $V . H \{ \varphi , \psi \}$ is a smooth partition of unity subordinate to $\{ U , V \}$ , we can take $\eta = \psi \omega$ and $\eta ^ { \prime } = - \varphi \omega$ , both extended by zero outside the supports of $\psi$ and $\varphi$.