III.24 The global projected connection
On this page · Permalink · Source line 1
Let \(M\) be a smooth real manifold without boundary, \(F\) a complete normed real vector space and \(P:M\to{\operatorname{End}}(F)\) a smooth family of bounded idempotents. For smooth range sections \(s\), define
The proof begins by constructing the range bundle from \(P\). Its local connection formulas glue, and the actual covariant commutator satisfies
The derivative and Lie bracket are Mathlib's actual manifold operators. No global coordinate chart is assumed. The result requires idempotence, not an additional orthogonality hypothesis.
III.25 Local products constructed from the projector
On this page · Permalink · Source line 14
The fiber over \(x\) is the actual fixed subspace
The total space is the subset \(\mathcal E=\{(x,v):P(x)v=v\}\subseteq M\times F\), with the induced topology. The construction provides local homeomorphisms of this total space as well as the transition functions between them.
III.25.1 An invertible intertwiner near each anchor
On this page · Permalink · Source line 21
For idempotents \(p,q\), set
Lean proves \(T(p,p)=I\) and \(pT(p,q)=T(p,q)q\). For an anchor \(a\in M\), define
The invertible elements form an open subset of the algebra of bounded operators. Consequently \(U_a\) is open and contains \(a\). The family \((U_a)\) covers the whole base. Invertibility is derived locally, not assumed at every pair of points.
III.25.2 The mutually inverse local maps
On this page · Permalink · Source line 32
Write \(T_a(x)=T(P(x),P(a))\). For \(x\in U_a\),
The intertwining identity and its inverse counterpart show that the displayed targets are correct. Lean proves both inverse laws, continuity, linearity in the fiber, and smooth dependence on the base. Thus
is a local product homeomorphism that preserves the base point.
III.25.3 Smooth overlap maps and rank
On this page · Permalink · Source line 48
The coordinate transition is \(g_{ab}(x)=A_b(x)B_a(x)\). It is smooth on \(U_a\cap U_b\), agrees with the actual change between local homeomorphisms, and satisfies
A continuous linear equivalence between \(\mathcal E_a\) and \(\mathcal E_x\) also gives local constancy of fiber dimension. No single constant rank across disconnected components is assumed.
III.26 A connection on the constructed bundle
On this page · Permalink · Source line 59
The global formula is defined using the actual manifold derivative:
Here \(D_M\) is represented by mvfderiv. A second definition, GlobalConnection.covariant, has values in the actual fiber:
It is not only an ambient expression asserted to land in the range.
III.26.1 Connection axioms and smoothness
On this page · Permalink · Source line 70
The formal proofs establish range preservation, additivity in the section, linearity over functions in the vector field argument, and the scalar Leibniz identity
Smooth \(P\), smooth sections and smooth vector fields give smooth covariant derivatives. Equality of section germs gives equality of covariant derivatives at the point, so the operation is local.
III.26.2 Smoothness of sections in bundle coordinates
On this page · Permalink · Source line 77
Let \(x\in U_a\). If \(P(y)s(y)=s(y)\) in a neighborhood of \(x\), then
The range condition is only local. The proof uses the actual inverse local maps and equality of germs. It follows that smoothness in bundle coordinates does not depend on the chosen chart.
III.26.3 The local connection and its change of coordinates
On this page · Permalink · Source line 86
For a coordinate function \(u\) valued in \(\mathcal E_a\), define
For every overlap point, Lean proves the operator identity
This is proved for arbitrary local coordinate functions. It does not assume that \(u\) was obtained from a globally smooth section or that a smooth extension has been supplied. Together with the local smoothness criterion, this closes the gluing step left open in the fifth block.
III.27 From differentiated projectors to the two-form
On this page · Permalink · Source line 101
The curvature is defined by the covariant commutator, including the actual manifold Lie bracket. It is not defined to equal the desired projector expression.
III.27.1 The flat ambient identity is proved in charts
On this page · Permalink · Source line 104
For a smooth vector-valued function \(s\), the proof identifies directional derivatives with the pullback into each extended chart. It then proves
This uses the chart pullback of the actual vector fields and the ordinary differential identity, then transfers the result back to the manifold. The auxiliary module works locally at a point, so the argument applies within arbitrary open chart domains.
III.27.2 Projector and section identities are derived
On this page · Permalink · Source line 111
Differentiating \(P^2=P\) in a tangent direction \(v\) yields
Differentiating \(Ps=s\) gives
Both statements are consequences of actual derivative rules. They are not additional assumptions.
III.27.3 Cancellation of the second derivatives
On this page · Permalink · Source line 123
The product rule and the identity for the ambient Lie bracket reduce curvature to
Substitute the identity obtained by differentiating the range condition for the section. The terms containing \(P{\,\mathrm d} P[v]P\) vanish, leaving
Lean also proves that this depends only on \(X(x)\), \(Y(x)\) and \(s(x)\), not on their extensions. The operator-valued form is alternating, additive, and homogeneous, and lands in the actual fiber. Constant projector bundles have zero curvature form.
III.27.4 Geometry and scalar conventions
On this page · Permalink · Source line 139
The main global curvature theorem uses a smooth real manifold without boundary, modeled on a complete normed real space, and bounded real-linear endomorphisms of a complete normed real space. Finite-dimensional parameter and quantum spaces fall within the corresponding real differential calculus. Complex quantum spaces can be viewed through their underlying real normed spaces. This block does not introduce a separate typeclass wrapper for complex bundles.
The atlas and global connection constructions also support the more general infrastructure for models with corners wherever their hypotheses apply. The curvature completion claim concerns the stated theorem for manifolds without boundary. Extending that curvature result to boundaries or corners requires further work.
III.27.5 An explicit smooth atlas
On this page · Permalink · Source line 144
The implementation exposes the actual total space, local product homeomorphisms, linear transitions, smoothness proofs, and cocycle laws. It does not register these as a ContMDiffVectorBundle instance. This is an interface choice. The range bundle atlas, local trivializations, overlap identities, and curvature formula are all constructed or proved from the stated inputs.
The equivalence for smooth sections and the gauge law make the atlas usable intrinsically. The connection is also defined with values in fiber (P x). Six constructed objects that contain proof fields, including both local equivalences and the derivative with values in the fiber, have separate axiom audits.