Invariance: closedness of the invariant differential #
The differential form ω_i = ∑_k (M⁻¹)_{ik} dX_k attached to a formal group law is invariant,
and — the content of this file — closed: ∂_l (M⁻¹)_{ik} = ∂_k (M⁻¹)_{il}
(ChabautyColeman.FormalGroupLaw.pderiv_diffMatrixInv_symm). This is the technical heart of
the formal-logarithm construction: it is what lets the radial antiderivative recover the
invariant differential. The proof runs through the substitution identities
ChabautyColeman.FormalGroupLaw.diffMatrix_subst_F and
ChabautyColeman.FormalGroupLaw.diffMatrixInv_subst_F and an antisymmetrization argument.
Main statements #
ChabautyColeman.FormalGroupLaw.diffMatrixInv_subst_F: the invariant differential is invariant.ChabautyColeman.FormalGroupLaw.pderiv_diffMatrixInv_symm: the invariant differential is closed.
Blueprint node: lem:fgl-invariance.
The matrix invariance identity of the invariant differential:
M(F(X,Y)) = (D_Y F)(X,Y) · M(Y), obtained by differentiating associativity in the
third block of variables at 0.
The invariance identity for the inverse Jacobian matrix N = M⁻¹ of a formal group
law: N(F(X,Y)) · D_Y F(X,Y) = N(Y), entrywise. Equivalently, the invariant differential
δ = N(X) dX satisfies δ(F(X,Y)) · D_Y F(X,Y) = δ(Y).
The invariant differential of a commutative formal group law is closed: the partial
derivatives of the entries of any row of the inverse Jacobian matrix M⁻¹ satisfy the
symmetry ∂_l (M⁻¹)_{ik} = ∂_k (M⁻¹)_{il}. Commutativity of the formal group law is
essential here.