Local Faddeev–Popov slice Jacobian and orbit-intersection count

Choose a submanifold chart $(z,w)$ at $s_0$ with $S$ given by $w=0$. Since $\ker d{\chi }_{s_0}=T_{s_0}S$ and $d{\chi }_{s_0}$ is onto, the derivative of $\chi$ in the $w$-directions is an isomorphism. Therefore $(z,w)\mapsto (\chi (z,w),z)$ has invertible derivative; [F2] gives adapted target coordinates $(y,z)=(\chi ,z)$ near $s_0$. This uses the supplied finite-dimensional data [F1] and inherited countable-choice premise [A1].

In source coordinates $(\xi ,z)$ on $K\times S$ and target coordinates $(y,z)$, $D{\mathrm{\Psi }}_{(e,s_0)}$ has block matrix $\left(\begin{array}{cc}{M}_{s_0}& 0\\ \ast & I_{n-k}\end{array}\right)$: the upper-left block is $d{\chi }_{s_0}\circ R_{s_0}=M_{s_0}$, the upper-right block vanishes because $\chi$ is zero on $S$, and the lower-right block is the identity because $z$ is the slice coordinate. Its determinant is nonzero by the hypothesis on $M_{s_0}$. Applying [F2] gives an open neighborhood on which $\mathrm{\Psi }$ is a diffeomorphism; choose an open product $V\times W$ inside that neighborhood and set $O=\mathrm{\Psi }(V\times W)$, which is open because a local diffeomorphism is open. The diffeomorphism gives exactly one pair $(g,s)\in V\times W$ for every $x\in O$. If $s^{\mathrm{\prime }}=s\cdot g$ with $s,s^{\mathrm{\prime }}\in W$ and $g\in V$, both $(g,s)$ and $(e,s^{\mathrm{\prime }})$ map to $s^{\mathrm{\prime }}$, so injectivity gives $g=e$ and $s=s^{\mathrm{\prime }}$. No assertion about other orbits or group elements outside $V$ follows.

In the same coordinates, the block determinant has absolute value $\mathrm{\mid }\det M_{s_0}\mathrm{\mid }$. Dividing by the source density coefficient ${\rho }_K(\xi (e)){\rho }_S(z_0)$ and using ${\mathrm{\Delta }}_{\mathrm{F}\mathrm{P}}(s_0)=\mathrm{\mid }\det M_{s_0}\mathrm{\mid }\mathrm{/}{\rho }_K(\xi (e))$ gives $J_{\mathrm{\Psi }}(e,s_0)={\rho }_X(0,z_0){\mathrm{\Delta }}_{\mathrm{F}\mathrm{P}}(s_0)\mathrm{/}{\rho }_S(z_0)$. On the chosen chart, [F3] applied to each compactly supported Riemann-integrable target function gives ${\int }_{O}fd{\mu }_X={\int }_{V\times W}(f\circ \mathrm{\Psi })J_{\mathrm{\Psi }}d{\mu }_{K}d{\mu }_S$.

At $g\in K$, the left-invariant frame is $Z\mapsto d(L_g{)}_{e}Z$, and the right-action identity gives $D(F_x{)}_g(d(L_g{)}_{e}Z)=M_{x\cdot g}Z$. The density ${\mu }_K$ has coefficient ${\rho }_K(\xi (e))$ in this frame, so ${\mathrm{\Delta }}_{\mathrm{F}\mathrm{P}}(x\cdot g)d{\mu }_K(g)$ changes to Lebesgue density under $y=F_x(g)$. Around each of the finitely many roots choose pairwise disjoint relatively compact inverse neighborhoods $V_i\subset \mathrm{\Gamma }$ and smooth cutoffs ${\psi }_i$ supported there and equal to $1$ near $g_i$. The compactly supported remainder $\phi (1-{\sum }_i{\psi }_i)$ has support disjoint from $F_x^{-1}(0)$, because every zero in $\mathrm{supp}\phi$ is listed and each cutoff is $1$ near its root; hence $\mathrm{\mid }{F}_x\mathrm{\mid }$ has a positive minimum on that support and the remainder integral vanishes for small $ϵ$. On each branch, [F3] gives ${\int }_{V_i}\phi (g){\psi }_i(g){\eta }_{ϵ}(F_x(g)){\mathrm{\Delta }}_{\mathrm{F}\mathrm{P}}(x\cdot g)d{\mu }_K(g)={\int }_{F_x(V_i)}\phi (F_{x,i}^{-1}(y)){\psi }_i(F_{x,i}^{-1}(y)){\eta }_{ϵ}(y)dy$. For small $ϵ$, the support of ${\eta }_{ϵ}$ is contained in $F_x(V_i)$, and this integral differs from $\phi (g_i)$ by at most ${\sup }_{\mathrm{\mid }y\mathrm{\mid }\le Cϵ}\mathrm{\mid }\phi (F_{x,i}^{-1}(y)){\psi }_i(F_{x,i}^{-1}(y))-\phi (g_i)\mathrm{\mid }\int {\eta }_{ϵ}(y)dy$, which tends to zero by continuity and unit mass. Summing the branch limits and the zero remainder proves the formula and counts the distinct transverse intersections.