Existence of compatible connections

Let $(X_n{)}_{n\in \mathbb{N}}$ be any sequence of nonempty sets. Apply [A1] to the set of distinct values $\{X_n:n\in \mathbb{N}\}$ and compose the resulting choice function with $n\mapsto X_n$. This gives a choice function for the sequence; the finite and empty indexed cases are immediate. Thus the countable-choice hypotheses of [F1], [F2], and [F3] hold. This is the only use of full AC.

For a real bundle over a boundaryless base, [F1] supplies a smooth Euclidean metric. If $M$ has boundary, take its supplied local trivializing frame cover by [F7]; in each frame pull back the standard positive-definite inner product on ${\mathbb{R}}^r$. Apply [F3] to this cover and call the resulting partition $({\rho }_{\alpha })$. The locally finite sum $g={\sum }_{\alpha }{\rho }_{\alpha }{g}_{\alpha }$, with each weighted term extended by zero outside its frame domain, is smooth because $\mathrm{supp}{\rho }_{\alpha }$ lies inside that domain. At each point the weights are nonnegative and sum to one, so $g$ is positive definite. The empty base has its unique metric. Hence every real bundle in the statement has a smooth Euclidean metric.

For a complex bundle, let $J$ be its smooth complex structure from [F4] and let $g$ be the real metric from step 2.1 on its underlying real bundle. Set $q(u,v)=g(u,v)+g(Ju,Jv)$. Then $q$ is smooth, positive definite, and $J$-invariant; in particular $q(Ju,v)=-q(u,Jv)$. Define $h(u,v)=q(u,v)-iq(Ju,v)$. The skew identity gives $h(Ju,v)=ih(u,v)$ and $h(u,Jv)=-ih(u,v)$; real bilinearity therefore makes $h$ complex-linear in its first variable and conjugate-linear in its second. Symmetry of $q$ gives $h(v,u)=\overline{h(u,v)}$, while $q(Ju,u)=0$ gives $h(u,u)=q(u,u)>0$ for $u\mathrm{\ne }0$. Thus $h$ is a smooth Hermitian metric in the stated convention.

Apply the local construction to a metric supplied at the start, or to the metric produced in steps 2.1 and 3.1 when proving existence for an arbitrary bundle. On each member of its local bundle-frame cover, apply Gram–Schmidt to the supplied frame to obtain an orthonormal frame in the real case or a unitary frame in the complex case, using [F4] and [F7]. All denominators are norms of nonzero vectors, so the procedure is smooth; in boundary charts the same formulas restrict from local smooth extensions. For a frame $e_{\alpha }$, define a local connection by ${\mathrm{\nabla }}^{\alpha }(e_{\alpha }u)=e_{\alpha }du$. Its matrix is zero in that orthonormal or unitary frame, so it is compatible with the metric by [F5] and [F6]. It is a complex connection by [F8]. Rank zero gives the empty frame and the unique zero connection.

Choose the partition $({\rho }_{\alpha })$ subordinate to this orthonormal/unitary frame cover using [F2] when $M$ is boundaryless and [F3] when it has boundary. Define $\mathrm{\nabla }s={\sum }_{\alpha }{\rho }_{\alpha }{\mathrm{\nabla }}^{\alpha }s$, extending each weighted term by zero outside its frame domain. This sum is locally finite and smooth. For a smooth scalar function $f$, each local connection obeys the relevant Leibniz rule by [F8], so $\mathrm{\nabla }(fs)={\sum }_{\alpha }{\rho }_{\alpha }(df\otimes s+f{\mathrm{\nabla }}^{\alpha }s)=df\otimes s+f\mathrm{\nabla }s$, because ${\sum }_{\alpha }{\rho }_{\alpha }=1$. The same calculation gives complex-linearity in the complex case. Since every ${\rho }_{\alpha }$ is real-valued, summing the local metric identities [F5] and [F6] gives $Xh(s,t)=h({\mathrm{\nabla }}_{X}s,t)+h(s,{\mathrm{\nabla }}_{X}t)$, or its real Euclidean version. Thus $\mathrm{\nabla }$ is globally compatible.

Steps 2.1 and 3.1 construct the stated real and complex metrics, and step 5.1 constructs compatible connections both for those metrics and for any metric supplied at the start. At an empty base the assertions are vacuous; at rank zero the unique metric and connection satisfy the identities vacuously. At rank one Gram–Schmidt and the local connection formula remain valid. On a zero-dimensional base every local connection one-form is zero, and the averaging and compatibility identities still hold. The partition and frame formulas also restrict to the boundary by steps 2.1, 4.1, and 5.1.