The extension \(B/A\).

The precise set-up we'll work in is the following. We fix \(G\) a finite group acting on \(B\) a commutative ring, and we have another commutative ring \(A\) such that \(B\) is an \(A\)-algebra and the image of \(A\) in \(B\) is precisely the \(G\)-invariant elements of \(B\). We don't ever need the map \(A\to B\) to be injective so we don't assume this.

We start with a construction which is fundamental to everything, and which explains why we need \(G\) to be finite.

DefinitionMulSemiringAction.charpoly #

If \(b\in B\) then define the characteristic polynomial \(F_b(X) \in B[X]\) of \(b\) to be \(\prod_{g\in G}(X-g\cdot b)\).

Lean

Formalized as MulSemiringAction.charpoly.

Sources

Fermat's Last Theorem (Imperial) blueprint: chapter/FrobeniusProject.tex, line 149

MathlibMulSemiringAction.charpoly

Used by 2

Used byAlgebra.IsInvariant.charpoly_mem_lifts · MulSemiringAction.monic_charpoly

Clearly \(F_b\) is a monic polynomial.

LemmaMulSemiringAction.monic_charpoly #

\(F_b\) is monic.

Proof

Obvious.

Lean

Formalized as MulSemiringAction.monic_charpoly.

Sources

Fermat's Last Theorem (Imperial) blueprint: chapter/FrobeniusProject.tex, line 159

MathlibMulSemiringAction.monic_charpoly

Uses 1 · Used by 1

Statement usesMulSemiringAction.charpoly

Used byAlgebra.IsInvariant.isIntegral

It's also clear that \(F_b\) has degree \(|G|\) and has \(b\) as a root. Also \(F_b\) is \(G\)-invariant, because acting by some \(\gamma\in G\) just permutes the order of the factors. Hence we can descend \(F_b\) to a monic polynomial \(M_b(X)\) of degree \(|G|\) in \(A[X]\). We will also refer to \(M_b\) as the characteristic polynomial of \(b\), even though it's not even well-defined if the map \(A\to B\) isn't injective.