3 The Levi-Civita connection
Mathlib has the Levi-Civita connection as of September 2026: mathlib4 PR #36845 (Massot, Rothgang, Macbeth) added CovariantDerivative/LeviCivita.lean with the Koszul formula, uniqueness, a construction by the musical isomorphism, and the proof that the construction is compatible and torsion-free. This chapter records what that gives the road, and the one thing it does not give yet.
For a \(C^1\) Riemannian metric \(g\) on a \(C^2\) manifold there is a torsion-free covariant derivative on \(TM\) compatible with \(g\).
Mathlib’s leviCivitaConnection I M: the Koszul expression \((X, Z) \mapsto \langle \nabla _X Y, Z\rangle \) is tensorial in \(X\) and \(Z\) for differentiable \(Y\), so it is a \((2,0)\)-tensor at each point; the musical isomorphism turns it into an endomorphism \(\nabla Y\), and that is the connection. Compatibility and torsion-freeness are then computations with the Koszul formula. No local frames are involved.
Two torsion-free metric-compatible covariant derivatives agree on every vector field that is differentiable at the point.
The Koszul formula determines \(\langle \nabla _X Y, Z\rangle \) for differentiable \(X, Y, Z\) without reference to \(\nabla \), and a vector is determined by its inner products against differentiable sections.
This — not “there is exactly one” — is the fundamental theorem. A CovariantDerivative is unconstrained on sections that are not differentiable at the point: the Leibniz and additivity laws, compatibility and the torsion all quantify over differentiable sections only, so a Levi-Civita connection can be altered on non-differentiable sections and stay Levi-Civita. The \(\exists !\) statement this chapter carried until now, as its only sorry, was therefore not provable as stated. Nothing downstream needed it: every curvature computation evaluates \(\nabla \) on differentiable sections.
\(R(X,Y)Z\) at \(x\) depends only on \(Z(x)\), and hence \(\operatorname {Ric}(X,Y)(x)\) depends only on \(X(x)\) and \(Y(x)\). Consequently Ricci curvature is a genuine function of tangent vectors, \(\texttt{ricciAt}\ x : T_xM\to T_xM\to \mathbb {R}\), and positivity of Ricci can be stated pointwise:
Proved. Expand \(Z\) in a local frame, valid near \(x\) (OrthonormalFrame.lean); globalise the frame fields and the coefficient functions by Lemma 10; apply \(C^\infty (M)\)-linearity in the third slot (curvature_sum_smul_third, whose twelve side conditions are discharged from globally \(C^2\) data in curvature_smul_third); the coefficients at \(x\) are determined by \(Z(x)\). Locality in the third slot (Lemma 10) is what lets the frame expansion, which holds only near \(x\), be used at all.
Only pointwise regularity of the first two slots is needed, which is what makes the result applicable to FiberBundle.extend and hence to the trace defining \(\operatorname {Ric}\).
The same machinery gives the well-definedness of the sectional curvature on a general manifold (sectionalCurvature_congr’, whose hypothesis h3 was previously assumed), and, with the vanishing of \(\langle R(X,Y)Y, X\rangle \) on a linearly dependent pair (inner_curvature_eq_zero_of_dep, by the equality case of Cauchy–Schwarz and antisymmetry in the first two slots), the multiplied-out form of constant sectional curvature (hasConstSecLC_iff_mul):
with no division and no nondegeneracy hypothesis, which is how Chow–Liao–Qin state it.
This is the form Chow–Liao–Qin’s positiveRicciMetric takes (arXiv 2608.21502), where it comes from a tensor-bundle construction; here it is derived instead from the frame and a bump function. It closes the last statement-level divergence recorded in notes/hamilton-statement-comparison.md. Note the result is a congruence, not TensorialAt: that structure demands its identities for merely differentiable sections, which the third slot cannot satisfy.
On a Hausdorff manifold, every tangent vector \(v \in T_xM\) is the value at \(x\) of a globally \(C^k\) vector field. Consequently, quantifying a property of \(X(x)\) over globally \(C^2\) fields \(X\) is the same as quantifying it over tangent vectors.
Proved. Mathlib’s FiberBundle.extend produces a section through \(v\) that is \(C^k\) only on a neighbourhood of \(x\) (exists_contMDiffOn_extend). Multiplying by a smooth bump function whose closed support lies inside that neighbourhood (SmoothBumpFunction.nhds_basis_support) gives a global field, still equal to \(v\) at \(x\) because the bump is \(1\) at its centre. Hausdorffness is needed for the bump function to be smooth and is exactly the hypothesis whose absence made the curvature predicates vacuously satisfiable; see notes/hamilton-statement-comparison.md.
The general form is exists_contMDiff_eventuallyEq: a section that is \(C^k\) on a neighbourhood of \(x\) agrees near \(x\) with a globally \(C^k\) section, with exists_contMDiff_eventuallyEq_fun the scalar companion for functions. This closes the long-standing gap "no global \(C^2\) extension of a tangent vector".
Alongside it, curvature_congr_third_of_eventuallyEq: \(R(X,Y)Z\) at \(x\) depends only on \(Z\) near \(x\), since \(\nabla \) is local on differentiable sections.
These two are what the pointwise statement below is built from.
Everything here is proved for an arbitrary \(C^k\) vector bundle (exists_contMDiff_eventuallyEq_of_bundle, exists_contMDiff_extension_of_bundle, forall_contMDiff_iff_forall_fiber), the tangent-bundle statements above being corollaries. Nothing in the bump-function argument is about \(TM\): mathlib’s FiberBundle.exists_contMDiffOn_extend and ContMDiffOn.smul_section_of_tsupport are already general. This is the form Lemma 90 needs — Hamilton’s curvature operator is a section of \(\mathrm{Sym}^2(\Lambda ^2 TM)\), not a vector field, so the maximum principle for it cannot quantify over a constant direction vector and must spread one into a section of that bundle instead (Lemma 80).
One statement does not survive verbatim: the conclusion is \(\forall ^f y \in \mathcal{N}(x),\ \tau (y) = \sigma (y)\) rather than \(\tau =^f_{\mathcal{N}(x)} \sigma \), because Lean’s Filter.EventuallyEq wants a non-dependent codomain and \(\prod _y V_y\) is non-dependent only for the tangent bundle, where \(V_y\) reduces to the model space.
Any two \(C^1\) Levi-Civita connections have the same Riemann tensor on fields \(X, Y\) differentiable at the point and \(C^2\) field \(Z\), hence the same Ricci tensor and the same sectional curvature on \(C^2\) fields.
\(R(X,Y)Z = \nabla _X \nabla _Y Z - \nabla _Y \nabla _X Z - \nabla _{[X,Y]} Z\). The inner derivatives agree as sections by uniqueness, since \(Z\) is differentiable everywhere; the outer derivatives then agree by uniqueness again, since \(\nabla _Y Z\) is differentiable at \(x\) when \(\nabla \) is \(C^1\) and \(Z\) is \(C^2\). For \(\operatorname {Ric}\), the trace is over the endomorphism produced by TensorialAt.mkHom, whose value on a vector is \(R\) evaluated on a differentiable extension of it. Sectional curvature is a quotient of inner products of \(R\).
This is what makes the existential quantification over connections in Chapters 6 and 7 well-posed: the predicates there are statements about the metric, not about a choice of connection.
On a \(C^\omega \) manifold with a \(C^{k+1}\) Riemannian metric, Mathlib’s leviCivitaConnection is a \(C^k\) covariant derivative: for every \(C^{k+1}\) vector field \(Y\), the section \(x \mapsto \nabla Y(x)\) of \(\operatorname {End}(TM)\) is \(C^k\).
This is the result Mathlib’s LeviCivita.lean defers to “future PRs”. Work in a trivialisation \(e\) of \(TM\) at \(x_0\) with the local frame \(s_i = e^{-1}(\cdot , b_i)\) for a basis \(b\) of the model space. Three criteria, each proved separately:
A map into \(\operatorname {Hom}(E, F)\) is \(C^k\) iff its values on a basis of \(E\) are (contMDiffAt_clm_of_basis).
A section \(w\) of a Riemannian bundle with \(C^k\) metric is \(C^k\) at \(x_0\) if the scalar functions \(\langle w, s_j\rangle \) are (contMDiffAt_section_of_inner_localFrame): the coordinates of \(w\) are \(G^{-1}(\langle w, s_j\rangle )_j\) for the Gram operator \(G\) of the frame, \(G\) is smooth and invertible on the base set, and ContinuousLinearMap.inverse is smooth at invertible points.
The Koszul expression for \(\langle \nabla _{s_i} Y, s_j\rangle \) is \(C^k\): derivatives of \(C^{k+1}\) inner products along \(C^{k}\) fields (contMDiffAt_mvfderiv_apply) and inner products of \(C^{k+1}\) fields with brackets of \(C^{k+1}\) fields, which are \(C^k\).
Then \(\nabla _{s_i} Y\) is \(C^k\) by (2) and (3), and \(\nabla Y\) in coordinates is determined by the \(\nabla _{s_i} Y\) by (1). No orthonormal frames are needed; the Gram inversion replaces them.
For a \(C^2\) metric \(g\), \(\operatorname {Ric}(g)\) is the Ricci curvature of its Levi-Civita connection, and likewise \(K(g)\). By Theorem 12 the connection is \(C^1\), so these are genuine tensors and not the junk value that ricci returns on a connection not known to be \(C^1\). This is the function \(g\mapsto \operatorname {Ric}(g)\) that DeTurck’s trick and the curvature evolution equations need.
\(\operatorname {Ric}(X,Y) = \operatorname {tr}(Z \mapsto R(Z,X)Y)\) and \(\operatorname {scal}= \operatorname {tr}_g\operatorname {Ric}\).
Defined. The trace needs \(R\) to descend from vector fields to vectors, and the criterion is \(C^\infty (M)\)-linearity in each slot — Lemma 6, together with additivity (curvature_add_left/middle/right). Since the trace is taken in the first slot only, Mathlib’s one-slot TensorialAt.mkHom suffices and the mkHom\(_3\) this blueprint previously called for is not needed — and would not have worked: its hypotheses quantify over merely MDiffAt sections, whereas first-slot tensoriality of \(R\) needs the third-slot field to be \(C^2\).
For a torsion-free connection, \(\operatorname {Ric}(X,Y) - \operatorname {Ric}(Y,X) = -\operatorname {tr} R(X,Y)\).
Trace the cyclic sum \(R(X,Y)Z + R(Y,Z)X + R(Z,X)Y = 0\) in \(Z\): the first term contributes \(\operatorname {tr}R(X,Y)\), the second \(-\operatorname {Ric}(Y,X)\) by antisymmetry, the third \(\operatorname {Ric}(X,Y)\) by definition.
Note. \(\operatorname {Ric}\) is not symmetric for a general torsion-free connection; symmetry is the corollary (ricci_symm_of_traceless) obtained when \(\operatorname {tr}R(X,Y) = 0\), which holds for a metric connection because \(R(X,Y)\) is then skew-adjoint. An earlier plan for this blueprint asserted symmetry from torsion-freeness alone. That is false.
\(\operatorname {Ric}\) as an honest continuous bilinear form \(\operatorname {Ric}_x : T_xM\times T_xM\to \mathbb {R}\) on a general manifold.
Proved (RicciForm.lean). Lemma 9 makes \(\operatorname {Ric}(X,Y)(x)\) depend on \(X_x\) and \(Y_x\) alone, so \(\operatorname {Ric}_x\) is a well-defined function of two tangent vectors (ricciAt); each of its four linearity laws is the corresponding field-level law (ricci_add_left and friends) applied to global \(C^2\) extensions, which exist by Lemma 10. Continuity is automatic in finite dimension. Two years’ worth of the “\(\operatorname {Ric}\) is not a tensor here” caveats in this blueprint dissolve at this node.
Write \(\operatorname {Rm}(X,Y,Z,W) = \langle R(X,Y)Z, W\rangle \) for a metric torsion-free connection. Then
Proved (CurvatureSymm.lean). The first three were already here: antisymmetry in the first pair needs no hypothesis at all (curvature_antisymm), antisymmetry in the second pair is metric compatibility (inner_curvature_right_skew), and the cyclic identity is Lemma 3 paired against a vector — note the fourth slot needs no regularity, the identity being a vector identity.
Pair symmetry is the new one, and it is what makes \(R\) a symmetric operator on \(\Lambda ^2 T_xM\) — the form Hamilton’s pinching estimates and Uhlenbeck’s trick are stated in — and what the second contraction of the second Bianchi identity will need.
\(\operatorname {Rm}_x(v_1,v_2,v_3,v_4) = \langle R(v_1,v_2)v_3, v_4\rangle \) is a well-defined \(4\)-linear form on \(T_xM\), additive and homogeneous in each slot, and carries all four symmetries of Lemma 17 pointwise.
Proved (CurvatureOperator.lean). What was missing was a genuinely pointwise tensor. The curvature was packaged only in pieces — curvatureEndoAt fixes the two field slots and varies a tangent vector in the third, curvatureBilinFst fixes the last two fields and varies the first — and nothing took four tangent vectors at once, which is what factoring through \(\Lambda ^2\) requires.
Three slots cost an extension; the fourth is free. The first three vectors are globalised to \(C^2\) fields (Lemma 10) and the fourth is paired against directly, so no regularity is asked of it at all — the same observation inner_bianchi_first already rested on. Slots 1 and 2 are then tensorialAt_curvature_fst/_snd cashed in through TensorialAt.pointwise, and slot 3 is curvature_congr_third with curvature_add_right/curvature_smul_const_right — the curvatureEndoAt pattern one slot wider.
Antisymmetry in the second pair is not proved from metric compatibility here, but deduced from pair symmetry and antisymmetry in the first pair, which is shorter: two applications of \(\operatorname {Rm}(a,b,c,d) = \operatorname {Rm}(c,d,a,b)\) around one sign flip.
This is the object Lemma 17 says pair symmetry is for. What remains before the curvature operator on \(\Lambda ^2 T_xM\) itself is the alternating factorisation. Mathlib supplies the target — \(\bigwedge ^2 E\) carries an inner product by the Gram determinant, and an orthonormal basis of \(E\) induces one of \(\bigwedge ^2 E\) — and exteriorPower.alternatingMapLinearEquiv is the universal property; what it does not supply is a constructor building a rank-\(2\) alternating map from a bilinear one, so the underlying MultilinearMap over Fin 2 has to be built by hand.
The classical octahedron argument. In the six unknowns
the four cyclic identities on \((X,Y,Z;W)\), \((Y,Z,W;X)\), \((Z,W,X;Y)\) and \((W,X,Y;Z)\), after every term has been brought to one of these six by the two antisymmetries, read
Adding the first two and the last two gives \(p - q + s + t = 0\) and \(q - p + s + t = 0\); subtracting, \(2(p-q) = 0\). In Lean the six links are supplied as hypotheses and linarith does the elimination.
For fixed \(c,d \in T_xM\), the map \((a,b) \mapsto \operatorname {Rm}_x(a,b,c,d)\) is alternating, hence factors through \(\Lambda ^2 T_xM\) as a linear functional \(\Phi _{c,d} \colon \Lambda ^2 T_xM\to \mathbb {R}\) with \(\Phi _{c,d}(a \wedge b) = \operatorname {Rm}_x(a,b,c,d)\); and \((c,d) \mapsto \Phi _{c,d}\) is itself additive, homogeneous and alternating in each of its two slots.
Proved (CurvatureLambda.lean). Mathlib has no constructor for a rank-\(2\) alternating map from a bilinear one, so the underlying MultilinearMap over Fin 2 is built by hand (altOfBilin): map_update_add’ and map_update_smul’ each split on whether the updated index is \(0\) or \(1\), and the alternating condition reduces to \(\operatorname {Rm}_x(a,a,c,d) = 0\). The factorisation itself is then exteriorPower.alternatingMapLinearEquiv, the universal property.
The factorisation is characterised, not merely defined. curvatureFunctional_apply_\(\iota \)Multi evaluates it on a wedge, which is what makes the object usable; the ten laws in the second pair of slots are each proved at the alternating-map level and carried across by alternatingMapLinearEquiv being a linear equivalence. No induction over \(\Lambda ^2\) is used, and none is available — Mathlib has exteriorPower.\(\iota \)Multi_span but no span-induction eliminator.
Everything is stated over \(E\), never over \(T_xM\). The two are definitionally equal, but forming \(\Lambda ^2 T_xM\) and unifying it against \(\Lambda ^2 E\) sends isDefEq through the exterior algebra — a quotient of a tensor algebra — and it does not return, even at four times the heartbeat budget. This is the \(E\) versus TangentSpace wall one type former up, and the same remedy applies. No metric is used, so nothing is lost by it.
The second factorisation is built, abstractly (sndAux, sndForm, sndForm_apply): for any family \(\Phi _{c,d} \colon \Lambda ^2 V \to \mathbb {R}\) bilinear and alternating in \((c,d)\), the induced bilinear form on \(\Lambda ^2 V\), defined and applied and characterised. Linearity in the \(\Lambda ^2\) slot is carried by hand, so the universal property is used only at codomain \(\mathbb {R}\), never at a linear-map-valued one.
Where this stops — and the diagnosis, corrected. The curvature form itself is still absent: instantiating the above at \(\Phi = \Phi _{c,d}\) puts the metric back into the term and every application times out. An earlier version of this node blamed the nested codomain \(\Lambda ^2 E \to _\ell (\Lambda ^2 E \to _\ell \mathbb {R})\). That was wrong, and three checks refute it: a variable of exactly that type applies to two wedges by rfl under the full instance pile; Mathlib’s own LinearMap.BilinForm.exteriorPower has that type and a simp lemma applying it to two wedges; and a map whose codomain is a plain alternating map — not nested at all — fails identically. Nor is it \(\Lambda ^2\): the abstract sndForm works end to end.
What the profiler says. On the smallest failing application, set_option diagnostics true reports isDefEq unfolding RiemannianBundle.g \(202472\) times and RiemannianMetric.inner \(202476\) times, through innerSL and mkContinuousOfExistsBound, with the \(f\, a \overset {?}{=} f\, b\) heuristic firing on toFun \(286390\) times. The cost is the metric. \(\operatorname {Rm}_x(a,b,c,d)\) is by definition \(\langle R(a,b)c, d\rangle \), so every definitional comparison of a term built from it descends into the metric’s construction. Marking things irreducible — the inner definitions, the outer definition, or \(\operatorname {Rm}_x\) itself — does not stop it.
A definition whose only characterisation cannot be stated is precisely the hazard this blueprint guards against, so the curvature form is not landed unusable. The lead for the next attempt is a different one: keep the metric out of the term, not merely out of the construction — build the \((0,4)\) tensor once as a bundled \(E \to _L E \to _L E \to _L E \to _L \mathbb {R}\) so that \(\langle \cdot ,\cdot \rangle \) sits inside a single opaque continuous linear map, and factor that. It is the same lesson curvatureBilinFst and FlowKoszul.lean each paid for once.
If every sectional curvature at \(x\) equals \(k\), then for all four arguments
Proved (ConstantCurvature.lean). This is a strengthening, not a parity fix. Chow–Liao–Qin’s admitsConstantPositiveSectionalCurvature is the multiplied-out sectional identity \(\operatorname {Rm}(X,Y,Y,X) = c(g(X,X)g(Y,Y) - g(X,Y)^2)\), which hasConstSecLC_iff_mul already matches; the divergence recorded in notes/hamilton-statement-comparison.md was closed before this lemma existed. What the lemma adds is that the sectional identity pins down the whole \((0,4)\) tensor, so everything downstream of constant curvature — the spherical space form conclusion above all — can use \(\operatorname {Rm}\) directly instead of re-deriving it.
Corollaries, by tracing once and twice (ricci_eq_of_const_sec, scalarCurvatureAt_eq_of_const_sec):
Both are stated over an arbitrary orthonormal basis of \(T_xM\), with \(n\) its cardinality, so no identification of \(\operatorname {finrank}\) with the dimension of the model is needed. Tracing uses Parseval (OrthonormalBasis.sum_inner_mul_inner) exactly once, on \(\sum _i \langle X, e_i\rangle \langle e_i, Y\rangle = \langle X, Y\rangle \); the first slot of \(\operatorname {Ric}\) is fed the global \(C^2\) extensions of the basis vectors, which is what extendTwo is for.
Applied to the predicate. hasConstSecLC_tensor, hasConstSecLC_ricci and hasConstSecLC_scalar instantiate all three at HasConstSecLC I M k and the canonical Levi-Civita connection, via hasConstSecLC_iff_mul. So the conclusion of Theorem 93 delivers the full \((0,4)\) tensor, and the metric it produces is Einstein with \(\operatorname {scal}= n(n-1)k\) — which is what the spherical space form direction will want to consume.
Polarisation, twice. Let
(curvatureDefect). The model term has every symmetry the curvature has, so by Lemma 17 \(T\) is antisymmetric in each pair, symmetric under exchanging the pairs, and satisfies the first Bianchi identity; and the hypothesis says exactly \(T(A,B,B,A) = 0\).
Expanding \(T(A+C, B, B, A+C) = 0\) and using \(T(C,B,B,A) = T(A,B,B,C)\) — pair symmetry followed by the two antisymmetries — gives \(2T(A,B,B,C) = 0\), so \(T(A,B,B,C) = 0\) for all \(A,B,C\). Expanding \(T(A, B+C, B+C, D) = 0\) then gives \(T(A,B,C,D) + T(A,C,B,D) = 0\): \(T\) is antisymmetric in its middle two slots as well. A tensor antisymmetric in three consecutive slots has all three terms of the first Bianchi identity equal, so \(3T(X,Y,Z,W) = 0\).
For a metric torsion-free connection — in particular for the Levi-Civita connection — \(\operatorname {Ric}(X,Y) = \operatorname {Ric}(Y,X)\) at every point of a general manifold, with no further hypothesis.
Torsion-freeness alone is not enough. Lemma 15 says the antisymmetric part of \(\operatorname {Ric}\) is exactly \(-\operatorname {tr}(v \mapsto R(X,Y)v)\), and that trace vanishes because the connection is metric. Symmetry is a corollary of skew-adjointness, not of the first Bianchi identity.
Lemma 15 carried two hypotheses it could not then discharge: that global \(C^2\) fields realise every tangent vector, and that the endomorphism \(v \mapsto R(X,Y)v\) exists at all. Both are now theorems — Lemma 10 and Lemma 9 — so curvatureEndoAt is an unconditional linear endomorphism of \(T_xM\), its linearity being tensoriality of the curvature’s third slot on global extensions. Its trace over an orthonormal basis is \(\sum _i \langle e_i, R(X,Y)e_i \rangle \), and each term vanishes because \(R(X,Y)\) is skew-adjoint for a metric connection (inner_curvature_self_right). Transporting through Definition 16 gives symmetry of the Ricci form itself.
\(\operatorname {scal}= \operatorname {tr}_g\operatorname {Ric}\), the metric trace of the Ricci tensor: \(\operatorname {scal}(x) = \sum _i \operatorname {Ric}(e_i, e_i)\) over an orthonormal basis of \(T_xM\).
Now a genuine trace on a general manifold (scalarCurvatureAt), and frame-independence is free: \(\sum _i B(e_i,e_i)\) is basis-independent for any bilinear \(B\), and by Definition 16 \(\operatorname {Ric}_x\) is one (scalarCurvatureAt_eq_sum_basis, no hypotheses).
This supersedes the earlier architecture, which is kept for the correspondence: the frame-relative scalarCurvatureWith, whose frame-independence scalarCurvatureWith_congr had to assume pointwise dependence of the curvature’s third slot in a form (MDiffAt in the first slot) that Lemma 9 does not supply, and the hypothesis-free scalarCurvature on the model space. Going through the bilinear form discharges the hypothesis on any manifold (scalarCurvatureWith_congr’).
\(\operatorname {Ric}(X,Y)(x) = \sum _i \langle b_i, R(b_i, X)Y(x)\rangle \) for any orthonormal basis of the fibre — hypothesis-free, on a general manifold. Raising an index is never needed: the frame sum with Parseval replaces the musical isomorphisms entirely.
For a \(2\)-plane spanned by tangent vectors \(X, Y\) at a point,
and the metric has constant sectional curvature \(k\) if \(K\equiv k\) on every \(2\)-plane at every point.
Defined, together with its invariance under change of basis of the spanned \(2\)-plane (sectionalCurvature_basis_change), which is the actual content. Absent from Mathlib entirely — the string sectional does not occur anywhere in the library. This is the conclusion side of Hamilton’s theorem, and it is undefined for the same reason the hypothesis was: well-definedness on \(2\)-planes rather than on pairs of vector fields is exactly Lemma 6. Unlike \(\operatorname {Ric}\) it needs no trace, so it requires the pointwise tensor but not mkHom\(_3\).