The Cartan Model of Equivariant de Rham Cohomology

Intuition Beginner

Ordinary cohomology measures the shape of a space: how many holes it has, in each dimension. But many spaces come with a symmetry — a rotation, a circle of motions, a group acting on every point at once. Plain cohomology forgets that the symmetry was ever there. Equivariant cohomology is the version that remembers it.

The trick is to widen what counts as an object. Instead of a single differential form, you allow a recipe: pick a direction of symmetry, and the recipe hands you back a form, depending in a polynomial way on the direction you picked. So the new objects carry two kinds of data at once — the usual geometry of the space, and an extra polynomial dependence on the symmetry directions.

A familiar analogy: a thermostat reading is one number, but a thermostat that reports temperature as a formula in the time of day carries more — it remembers a rhythm. Equivariant cohomology is cohomology that still carries the rhythm of its symmetry.

Visual Beginner

Picture a space with a circle of rotations acting on it, like a sphere spun about its axis. The two poles never move; everything else slides along circles of latitude. Plain cohomology sees the sphere. Equivariant cohomology also sees the spinning.

The picture to keep is a two-input machine. Feed it a point of the space and a chosen symmetry direction; it returns a number. The fixed points — where the symmetry does nothing — turn out to control almost everything, because that is where the extra polynomial data has nowhere to hide.

Worked example Beginner

Take a circle of rotations acting on the flat plane, spinning everything about the origin. The origin stays put; every other point travels on a circle. The symmetry has one direction, so a recipe in our new sense is a form on the plane that also depends on a single number, the chosen rotation speed, which we call $u$.

The simplest interesting recipe is the one whose form part is the area form and whose polynomial part is the squared distance to the origin times $u$. Written out, it is the area form added to $u$ times one-half the squared radius. The first piece is geometry; the second piece records how far each point sits from the fixed origin, scaled by the speed.

Now apply the equivariant version of the boundary operator. On this recipe the two contributions cancel exactly: the change in the area piece is matched and undone by the contraction of the radius piece along the spinning motion. So the recipe is equivariantly closed.

What this tells us: the moment map of a rotation — here, one-half the squared radius — is the precise polynomial correction that turns the area form into an equivariantly closed object. Geometry alone is not closed under the new rule; geometry plus the right symmetry data is.

Check your understanding Beginner

Formal definition Intermediate+

Let $G$ be a compact Lie group with Lie algebra $\mathfrak{g}$, acting smoothly on a manifold $M$ ^{[Berline-Getzler-Vergne Ch. 7]}. Each $\xi \in \mathfrak{g}$ generates a fundamental vector field $X_{\xi }$ on $M$, the infinitesimal generator of the flow $t\mapsto \exp (t\xi )\cdot$, with the contraction (interior product) ${\iota }_{X_{\xi }}:{\Omega }^{\bullet }(M)\to {\Omega }^{\bullet -1}(M)$ and the Lie derivative ${\mathcal{L}}_{X_{\xi }}=d{\iota }_{X_{\xi }}+{\iota }_{X_{\xi }}d$ (the Cartan magic formula, using the exterior derivative 03.04.04).

Definition (Cartan complex). The Cartan complex is the space of $G$-invariant polynomial maps from $\mathfrak{g}$ to differential forms,

$${\Omega }_G^{\bullet }(M):=({\Omega }^{\bullet }(M)\otimes \mathbb{R}[\mathfrak{g}]{)}^G,$$

where $\mathbb{R}[\mathfrak{g}]=S^{\bullet }({\mathfrak{g}}^{\ast })$ is the algebra of polynomial functions on $\mathfrak{g}$, and the superscript $G$ denotes invariants under the simultaneous action of $G$ on forms (by pullback) and on $\mathbb{R}[\mathfrak{g}]$ (by the coadjoint action). An element $\alpha$ is a map $\xi \mapsto \alpha (\xi )\in {\Omega }^{\bullet }(M)$, polynomial in $\xi$, with $g^{\ast }\alpha ({\mathrm{Ad}}_g\xi )=\alpha (\xi )$ for all $g\in G$.

Grading. ${\Omega }_G^{\bullet }(M)$ carries the total degree: a homogeneous polynomial of degree $j$ valued in $p$-forms has total degree $p+2j$. The factor of $2$ assigns ${\mathfrak{g}}^{\ast }$ degree $2$, so that the equivariant differential below raises total degree by one.

Definition (equivariant differential). The Cartan differential is

$$(d_{\mathfrak{g}}\alpha )(\xi ):=d(\alpha (\xi ))-{\iota }_{X_{\xi }}(\alpha (\xi )),$$

de Rham minus contraction by the fundamental vector field. On a homogeneous element this raises total degree by $1$: $d$ raises form degree by $1$, while ${\iota }_{X_{\xi }}$ lowers form degree by $1$ and the explicit $\xi$ raises polynomial degree by $1$, a net change of $-1+2=+1$.

Definition (equivariant cohomology). The equivariant de Rham cohomology of $M$ is

$$H_G^{\bullet }(M):=\frac{\ker (d_{\mathfrak{g}}:{\Omega }_G^{\bullet }(M)\to {\Omega }_G^{\bullet +1}(M))}{\mathrm{im}(d_{\mathfrak{g}}:{\Omega }_G^{\bullet -1}(M)\to {\Omega }_G^{\bullet }(M))}.$$

An element $\alpha$ with $d_{\mathfrak{g}}\alpha =0$ is equivariantly closed. The construction is a genuine complex only because of the invariance restriction: by the Cartan magic formula, $d_{\mathfrak{g}}^2=-{\mathcal{L}}_{X_{\xi }}$ as an operator depending on $\xi$, and this vanishes precisely on $G$-invariant elements, where ${\mathcal{L}}_{X_{\xi }}\alpha =0$.

Counterexamples to common slips

• Dropping invariance. Without the superscript $G$, the operator $d_{\mathfrak{g}}$ does not square to zero: $d_{\mathfrak{g}}^2=-{\mathcal{L}}_{X_{\xi }}\ne 0$ on a non-invariant element. The invariant restriction is not cosmetic.
• Forgetting the degree convention. Assigning ${\mathfrak{g}}^{\ast }$ degree $1$ makes $d_{\mathfrak{g}}$ inhomogeneous. Polynomial generators must carry degree $2$.
• Confusing $H_G^{\bullet }(M)$ with $H^{\bullet }(M)$. For $M$ a point, $H^{\bullet }(\mathrm{pt})$ is one-dimensional, but $H_G^{\bullet }(\mathrm{pt})=\mathbb{R}[\mathfrak{g}{]}^G=S^{\bullet }({\mathfrak{g}}^{\ast }{)}^G$, the invariant polynomials — far from a point.

Key theorem with proof Intermediate+

Theorem (the Cartan complex is a complex). Let $G$ be a compact Lie group acting smoothly on $M$. On the Cartan complex ${\Omega }_G^{\bullet }(M)=({\Omega }^{\bullet }(M)\otimes \mathbb{R}[\mathfrak{g}]{)}^G$, the Cartan differential satisfies $d_{\mathfrak{g}}^2=0$. Hence $H_G^{\bullet }(M)$ is well-defined.

Proof. Fix $\xi \in \mathfrak{g}$ and work with the operator $d_{\xi }:=d-{\iota }_{X_{\xi }}$ acting on ${\Omega }^{\bullet }(M)$, before imposing invariance. Compute the square,

$$d_{\xi }^2=(d-{\iota }_{X_{\xi }})(d-{\iota }_{X_{\xi }})=d^2-d{\iota }_{X_{\xi }}-{\iota }_{X_{\xi }}d+{\iota }_{X_{\xi }}^2.$$

The exterior derivative is a differential, so $d^2=0$. Contraction by a single vector field is an odd derivation with ${\iota }_{X_{\xi }}^2=0$, since ${\iota }_{X_{\xi }}{\iota }_{X_{\xi }}\omega$ feeds the same vector into two antisymmetric slots. The two cross terms combine by the Cartan magic formula:

$$d{\iota }_{X_{\xi }}+{\iota }_{X_{\xi }}d={\mathcal{L}}_{X_{\xi }}.$$

Therefore

$$d_{\xi }^2=-(d{\iota }_{X_{\xi }}+{\iota }_{X_{\xi }}d)=-{\mathcal{L}}_{X_{\xi }}.$$

Now reinstate the polynomial dependence and the invariance. An element $\alpha \in ({\Omega }^{\bullet }(M)\otimes \mathbb{R}[\mathfrak{g}]{)}^G$ is invariant under the simultaneous $G$-action, so its infinitesimal invariance reads ${\mathcal{L}}_{X_{\xi }}\alpha (\xi )=0$ for every $\xi$: the Lie derivative along $X_{\xi }$ of the value at $\xi$ vanishes, because invariance under $\exp (t\xi )$ differentiates to annihilation by ${\mathcal{L}}_{X_{\xi }}$. Hence $(d_{\mathfrak{g}}^2\alpha )(\xi )=-{\mathcal{L}}_{X_{\xi }}\alpha (\xi )=0$ for all $\xi$, so $d_{\mathfrak{g}}^2=0$ on ${\Omega }_G^{\bullet }(M)$. $\square$

Bridge. This squaring identity is the foundational reason equivariant cohomology exists at all, and it builds toward the equivariant Chern-Weil theory of the next section: feeding curvature into invariant polynomials produces equivariantly closed forms exactly because $d_{\mathfrak{g}}$ behaves like the ordinary differential on the invariant subalgebra. The Cartan magic formula appears again in 03.06.06, where the same interplay of $d$, $\iota$, and $\mathcal{L}$ governs the descent of basic forms to the base; this is exactly the same algebra, now with the contraction term made explicit rather than killed by horizontality. The construction generalises ordinary de Rham cohomology, which it recovers when $G$ is the identity group and the contraction term disappears. The bridge between the moment map of a Hamiltonian action and an equivariantly closed form is what putting these together exposes: the equivariant symplectic form $\omega +\mu$ is $d_{\mathfrak{g}}$-closed precisely when $d{\mu }^{\xi }={\iota }_{X_{\xi }}\omega$, the defining equation of the moment map underlying Duistermaat-Heckman 05.04.05.

Exercises Intermediate+

Lean formalization Intermediate+

lean_status: none — Mathlib lacks the equivariant de Rham apparatus. A future development would need smooth group actions with fundamental vector fields, the interior product, the Cartan magic formula, the invariant polynomial algebra with its doubled grading, and the equivariant differential.

A plausible future statement would have this shape:

-- Pseudocode only: required structures are not yet in Mathlib.
theorem cartan_differential_squares_to_zero
    {G : Type*} [LieGroup G] {M : Type*} [SmoothManifold M]
    (act : SmoothAction G M)
    (α : CartanComplex G M) :
    cartanDiff act (cartanDiff act α) = 0 := by
  -- d² = 0, ι² = 0, and the Cartan magic formula give d_g² = -L_X,
  -- which vanishes on the G-invariant subalgebra.
  sorry

The gap is concrete: implementing this upstream would first require the contraction-and-Lie-derivative calculus, then the invariant-subalgebra restriction.

Advanced results Master

The Cartan model is the computational face of equivariant cohomology, and three structural results organise its use.

Equivariant Chern-Weil. Let $P\to M$ be a $G$-equivariant principal $K$-bundle with $K$-connection, and let $G$ act on $P$ covering its action on $M$. The Chern-Weil construction 03.06.06 admits an equivariant refinement: the equivariant curvature is

$$F_{\mathfrak{g}}(\xi )=F+{\mu }^{\xi },$$

where $F$ is the ordinary curvature and ${\mu }^{\xi }={\iota }_{X_{\xi }}\omega -{\mathcal{L}}_{X_{\xi }}$-corrected moment, the contraction of the connection $\omega$ by the fundamental vector field. For an invariant polynomial $f\in S^{\bullet }({\mathfrak{k}}^{\ast }{)}^K$, the form $f(F_{\mathfrak{g}})$ is $d_{\mathfrak{g}}$-closed and represents an equivariant characteristic class in $H_G^{\bullet }(M)$. Setting $\xi =0$ recovers the ordinary characteristic class; the polynomial dependence on $\xi$ is the equivariant refinement. This is the mechanism that produces the equivariant Euler class $e_G(N_F)$ appearing in localisation.

Equivariantly closed extensions of the symplectic form. For a Hamiltonian $G$-action on $(M,\omega )$ with moment map $\mu :M\to {\mathfrak{g}}^{\ast }$, the form

$$\bar{\omega }(\xi )=\omega +{\mu }^{\xi },{\mu }^{\xi }:=⟨\mu ,\xi ⟩,$$

satisfies $d_{\mathfrak{g}}\bar{\omega }=d\omega -{\iota }_{X_{\xi }}\omega +d{\mu }^{\xi }=-{\iota }_{X_{\xi }}\omega +d{\mu }^{\xi }=0$, the last equality being the defining moment-map equation $d{\mu }^{\xi }={\iota }_{X_{\xi }}\omega$. So the equivariant symplectic form $\bar{\omega }$ is canonically equivariantly closed, and its exponential $e^{\bar{\omega }}=e^{\omega }{e}^{\mu }$ is the integrand of the Duistermaat-Heckman integral 05.04.05. The moment map is not an accessory: it is exactly the degree-two correction that makes $\omega$ survive into equivariant cohomology.

The Atiyah-Bott / Berline-Vergne localisation formula. Let $G=T$ be a torus acting on a compact oriented manifold $M$ with isolated or non-degenerate fixed-point set, components $F\subseteq M^T$. For an equivariantly closed form $\alpha \in {\Omega }_T^{\bullet }(M)$ the equivariant integral localises:

$${\int }_M\alpha =\sum _F{\int }_F\frac{\alpha {|}_F}{e_T(N_F)},$$

where $N_F$ is the normal bundle of $F$ in $M$ and $e_T(N_F)$ is its equivariant Euler class, computed by equivariant Chern-Weil. The right side is supported entirely on the fixed-point set: the geometry away from $M^T$ contributes nothing, because there the $T$-action has no zeros and $\alpha$ is equivariantly exact in a neighbourhood. Applying this to $\alpha =e^{\bar{\omega }}$ recovers the equivariant integration form of Duistermaat-Heckman 05.04.05 as the prototype — the stationary-phase exactness of the moment-map integral is the special case of localisation for the equivariant symplectic form.

Synthesis. The Cartan model identifies a piece of equivariant-geometric data — a $G$-manifold with its action — with a piece of mixed form-and-polynomial algebra, and the bridge is a single operator identity: $d_{\mathfrak{g}}^2=-{\mathcal{L}}_{X_{\xi }}$, vanishing on invariants. The foundational reason equivariant cohomology computes anything is exactly that this differential restricts the full $\mathbb{Z}$-graded form-polynomial algebra to a genuine complex, and the central insight is that its closed classes are pinned down by the fixed-point set through localisation. This is exactly the same descent-by-invariance that makes ordinary Chern-Weil 03.06.06 produce characteristic classes; the equivariant version generalises it by retaining the contraction term that horizontality previously erased. Putting these together, the equivariant symplectic form, the equivariant Euler class, and the localisation formula are three readings of one structure: $\bar{\omega }=\omega +\mu$ is the equivariantly closed extension, $e_T(N_F)$ is the equivariant Chern-Weil class of the normal data, and the localisation sum is dual to the fixed-point decomposition of the $T$-action.

Full proof set Master

Proposition (equivariant closedness of $\bar{\omega }$). Let $G$ act on $(M,\omega )$ in a Hamiltonian fashion with moment map $\mu : M \to \mathfrak g^$,normalisedby$d\mu^\xi = \iota_{X_\xi}\omega$forevery$\xi \in \mathfrak g$(where$\mu^\xi = \langle \mu, \xi\rangle$).Then$\bar\omega(\xi) := \omega + \mu^\xi$liesin$\Omega_G^2(M)$ and is equivariantly closed.*

Proof. First, $\bar{\omega }$ is $G$-invariant: $\omega$ is $G$-invariant by hypothesis on the Hamiltonian action, and $\mu$ is equivariant for the coadjoint action ($\mu (g\cdot x)={\mathrm{Ad}}_{g^{-1}}^{\ast }\mu (x)$), so the pairing $⟨\mu ,\xi ⟩$ transforms correctly to make $\xi \mapsto {\mu }^{\xi }$ an invariant element of ${\Omega }^0(M)\otimes {\mathfrak{g}}^{\ast }$. The form part $\omega$ has form degree $2$ and polynomial degree $0$; the moment part ${\mu }^{\xi }$ has form degree $0$ and polynomial degree $1$, hence total degree $2$ as well. So $\bar{\omega }\in {\Omega }_G^2(M)$.

Now apply $d_{\mathfrak{g}}$. By definition $d_{\mathfrak{g}}\bar{\omega }(\xi )=d\bar{\omega }(\xi )-{\iota }_{X_{\xi }}\bar{\omega }(\xi )$. The exterior derivative gives $d\omega +d{\mu }^{\xi }=0+d{\mu }^{\xi }$, since $\omega$ is closed. The contraction gives ${\iota }_{X_{\xi }}\omega +{\iota }_{X_{\xi }}{\mu }^{\xi }={\iota }_{X_{\xi }}\omega +0$, since contraction annihilates the function ${\mu }^{\xi }$. Therefore

$$d_{\mathfrak{g}}\bar{\omega }(\xi )=d{\mu }^{\xi }-{\iota }_{X_{\xi }}\omega =0$$

by the moment-map normalisation. Hence $\bar{\omega }$ is equivariantly closed. $\square$

Proposition ($d_{\mathfrak{g}}^2=0$ on invariants). On ${\Omega }_G^{\bullet }(M)$ the Cartan differential satisfies $d_{\mathfrak{g}}^2=0$.

Proof. For fixed $\xi$, expand $(d-{\iota }_{X_{\xi }}{)}^2=d^2-(d{\iota }_{X_{\xi }}+{\iota }_{X_{\xi }}d)+{\iota }_{X_{\xi }}^2=-{\mathcal{L}}_{X_{\xi }}$, using $d^2=0$, ${\iota }_{X_{\xi }}^2=0$, and the Cartan magic formula. Invariance of $\alpha \in {\Omega }_G^{\bullet }(M)$ under $\exp (t\xi )$ differentiates at $t=0$ to ${\mathcal{L}}_{X_{\xi }}\alpha (\xi )=0$. Hence $d_{\mathfrak{g}}^2\alpha =-{\mathcal{L}}_{X_{\xi }}\alpha =0$. $\square$

Proposition (equivariant integral descends to cohomology). For $M$ closed and oriented and $\alpha \in {\Omega }_G^{\bullet }(M)$ equivariantly closed, the top-form component of ${\int }_M$ depends only on the class $[\alpha ]\in H_G^{\bullet }(M)$.

Proof. Suppose ${\alpha }^{\prime }=\alpha +d_{\mathfrak{g}}\gamma$. The difference $d_{\mathfrak{g}}\gamma =d\gamma -{\iota }_{X_{\xi }}\gamma$ contributes, in top form degree, only the term $d({\gamma }_{\dim M-1})$, the de Rham derivative of the form part one degree below top; the contraction term lowers form degree and cannot reach top degree from a top form. By Stokes' theorem on the closed manifold, ${\int }_{M}d({\gamma }_{\dim M-1})=0$. Therefore ${\int }_M{\alpha }^{\prime }={\int }_M\alpha$ at top form degree, and the equivariant integral is a function on $H_G^{\bullet }(M)$. $\square$

Connections Master

• Duistermaat-Heckman and localisation 05.04.05. The equivariant symplectic form $\bar{\omega }=\omega +\mu$ is the canonical equivariantly closed object of this model, and its exponential is the Duistermaat-Heckman integrand. The Atiyah-Bott / Berline-Vergne localisation formula stated here in Cartan-model language has Duistermaat-Heckman as its prototype: the stationary-phase exactness of ${\int }_M{e}^{i⟨t,\mu ⟩}{\omega }^n/n!$ is the localisation of $e^{\bar{\omega }}$ to the fixed-point set. That unit assumes the present model silently; this unit supplies it.

• Chern-Weil homomorphism 03.06.06. The equivariant Chern-Weil map feeds equivariant curvature $F+\mu$ into invariant polynomials to produce equivariant characteristic classes, including the equivariant Euler class $e_G(N_F)$ that appears in the denominator of the localisation formula. The ordinary Chern-Weil homomorphism is the $\xi =0$ restriction, and the descent-by-invariance that defines $d_{\mathfrak{g}}$ on the invariant subalgebra is the same algebra that makes basic forms descend to the base in that unit.

• Kirillov character formula 03.09.25. The Kirillov formula is a consumer of this model: it expresses the character of an irreducible representation as an equivariant integral over a coadjoint orbit, evaluated by fixed-point localisation in the Cartan model. The orbit's symplectic form, its moment map, and its torus-fixed points are exactly the data the present unit makes precise, and the character formula is the localisation sum read as a Weyl-determinant quotient.

• Family and equivariant index 03.09.21. The equivariant index of a Dirac operator is computed by an equivariant analogue of the Atiyah-Singer integrand, an equivariantly closed characteristic form integrated against the manifold; localisation to the fixed-point set produces the equivariant index density. The Cartan model is the de Rham home of that integrand.

• Exterior derivative 03.04.04. The equivariant differential $d_{\mathfrak{g}}=d-{\iota }_{X_{\xi }}$ is built from the exterior derivative, and the entire complex reduces to ordinary de Rham cohomology when $G$ is the identity group and the contraction term vanishes. The Cartan magic formula ${\mathcal{L}}_{X_{\xi }}=d{\iota }_{X_{\xi }}+{\iota }_{X_{\xi }}d$, which controls $d_{\mathfrak{g}}^2$, is the same calculus of $d$ and contraction introduced there.

Historical & philosophical context Master

Henri Cartan introduced the algebraic model now bearing his name in two 1950 Brussels colloquium notes on transgression in Lie groups and principal bundles ^{[Cartan 1950]}, building the Weil algebra and its invariant subcomplex as a finite-dimensional substitute for the cohomology of the infinite-dimensional classifying space. The model translated a topological object — the Borel construction $M{\times }_{G}EG$ — into a tractable differential-graded algebra of invariant polynomial maps from the Lie algebra to forms.

Michael Atiyah and Raoul Bott in their 1984 paper The moment map and equivariant cohomology ^{[Atiyah-Bott 1984]} used the Cartan model to prove the localisation theorem and to identify the Duistermaat-Heckman measure as an instance of equivariant localisation, work carried out independently by Nicole Berline and Michèle Vergne in 1982. Nicole Berline, Ezra Getzler, and Michèle Vergne later gave the model its standard modern treatment in the heat-kernel approach to the index theorem ^{[Berline-Getzler-Vergne Ch. 7]}, and Victor Guillemin and Shlomo Sternberg developed the Weil-to-Cartan comparison and the supersymmetric reading at length ^{[Guillemin-Sternberg]}.

Bibliography Master

@incollection{Cartan1950Transgression,
  author    = {Cartan, Henri},
  title     = {La transgression dans un groupe de {L}ie et dans un espace fibr{\'e} principal},
  booktitle = {Colloque de topologie (espaces fibr{\'e}s), Bruxelles 1950},
  publisher = {Georges Thone, Li{\`e}ge},
  year      = {1950},
  pages     = {57--71}
}

@article{AtiyahBott1984Moment,
  author  = {Atiyah, Michael F. and Bott, Raoul},
  title   = {The moment map and equivariant cohomology},
  journal = {Topology},
  volume  = {23},
  year    = {1984},
  pages   = {1--28}
}

@article{BerlineVergne1982Localisation,
  author  = {Berline, Nicole and Vergne, Mich{\`e}le},
  title   = {Classes caract{\'e}ristiques {\'e}quivariantes; formule de localisation en cohomologie {\'e}quivariante},
  journal = {C. R. Acad. Sci. Paris},
  volume  = {295},
  year    = {1982},
  pages   = {539--541}
}

@book{BerlineGetzlerVergne1992,
  author    = {Berline, Nicole and Getzler, Ezra and Vergne, Mich{\`e}le},
  title     = {Heat Kernels and {D}irac Operators},
  publisher = {Springer},
  series    = {Grundlehren der mathematischen Wissenschaften},
  volume    = {298},
  year      = {1992}
}

@book{GuilleminSternberg1999Susy,
  author    = {Guillemin, Victor and Sternberg, Shlomo},
  title     = {Supersymmetry and Equivariant de {R}ham Theory},
  publisher = {Springer},
  series    = {Mathematics Past and Present},
  year      = {1999}
}

@article{DuistermaatHeckman1982Var,
  author  = {Duistermaat, J. J. and Heckman, G. J.},
  title   = {On the variation in the cohomology of the symplectic form of the reduced phase space},
  journal = {Invent. Math.},
  volume  = {69},
  year    = {1982},
  pages   = {259--268}
}

---

Foundational tooling unit. Produced to fill the Cartan-model prerequisite assumed silently by Duistermaat-Heckman 05.04.05, the family/equivariant index 03.09.21, and the Kirillov character formula 03.09.25. Lean status none: the equivariant de Rham apparatus is not yet in Mathlib.