Antisymmetrized raised covariant derivative and $G$

Proved

RelPartMech.covDeriv_antisymm_contra

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsrelativity

For the Levi-Civita connection of a smooth metric $g$ , a covector field $A_\gamma$ and $A^\beta=g^{\beta\gamma}A_\gamma$ , with $\nabla_\alpha A^\beta=\partial_\alpha A^\beta+\Gamma^\beta_{\gamma\alpha}A^\gamma$ and $\nabla^\alpha=g^{\alpha\gamma}\nabla_\gamma$ ,

\nabla^\alpha A^\beta-\nabla^\beta A^\alpha = \partial^\alpha A^\beta-\partial^\beta A^\alpha + G^{\alpha\beta\gamma}A_\gamma .

With contravariant indices the antisymmetrized covariant and partial derivatives differ, and $G$ expresses the difference.

Preamble

import Mathlib
import Definitions.Def_RelPartMech_coordinates

open scoped ContDiff

Formal statement

namespace RelPartMech

theorem covDeriv_antisymm_contra {n : ℕ} (g : MetricField n) (hg : IsSmoothMetric g)
    (A : CovectorField n) (α β : Fin n) (x : Coord n) :
    ∑ γ, ginv g x α γ * covDerivContra g (raise g A) γ β x
      - ∑ γ, ginv g x β γ * covDerivContra g (raise g A) γ α x =
      pdUp g α (raise g A β) x - pdUp g β (raise g A α) x
        + ∑ γ, gSymbolUp g α β γ x * A γ x := by sorry

end RelPartMech

Source

G. Carcassi, C. A. Aidala, "Relativity and Particle Mechanics" (note, uploaded PDF), p. 8, eq. (15), last block

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Antisymmetrized raised covariant derivative and GGG

Antisymmetrized raised covariant derivative and $G$