Fixed rings and characteristic polynomials of group actions

The fixed subring and fixed subalgebra are invariant extensions, so the integral-extension and prime-orbit theorems apply to them.

Let a finite group G act on an integral domain B. Mathlib's MulSemiringAction.charpoly G b = ∏ g : G, (X - C (g • b)) is the monic polynomial whose roots are the translates of b. When those translates are pairwise distinct, it divides every polynomial vanishing on all of them. This is the step that turns "vanishes on the orbit" into an explicit factorization, for instance when comparing the displacement of a generator of an intermediate ring with a product of displacements of a generator of the top ring.

Main results

• The fixed-subring and fixed-subalgebra instances of Algebra.IsInvariant identify the invariant extensions.
• TauCeti.MulSemiringAction.charpoly_dvd: if g ↦ g • b is injective and f vanishes at every g • b, then charpoly G b ∣ f.
• TauCeti.MulSemiringAction.eval_smul_charpoly: evaluating σ • charpoly H b at b gives the product of the displacements b - σ • τ • b.

instance TauCeti.Algebra.IsInvariant.instIsInvariantSubtypeMemSubringSubring_tauCeti (A : Type u_1) (G : Type u_2) [CommRing A] [Group G] [MulSemiringAction G A] : Algebra.IsInvariant (↥(FixedPoints.subring A G)) A G

The fixed subring is an invariant extension: every fixed element lies in its image.

instance TauCeti.Algebra.IsInvariant.instIsInvariantSubtypeMemSubalgebraSubalgebra_tauCeti (R : Type u_1) (A : Type u_2) (G : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] : Algebra.IsInvariant (↥(FixedPoints.subalgebra R A G)) A G

The fixed subalgebra is an invariant extension: every fixed element lies in its image.

theorem TauCeti.MulSemiringAction.charpoly_dvd {G : Type u_1} {B : Type u_2} [Group G] [Fintype G] [CommRing B] [IsDomain B] [MulSemiringAction G B] {b : B} (hb : Function.Injective fun (g : G) => g • b) {f : Polynomial B} (hf : ∀ (g : G), Polynomial.eval (g • b) f = 0) : MulSemiringAction.charpoly G b ∣ f

The characteristic polynomial of a point with pairwise distinct translates divides every polynomial vanishing on its orbit.

theorem TauCeti.MulSemiringAction.eval_smul_charpoly {G : Type u_1} {H : Type u_2} {B : Type u_3} [Monoid G] [Group H] [Fintype H] [CommRing B] [MulSemiringAction G B] [MulSemiringAction H B] (σ : G) (b : B) : Polynomial.eval b (σ • MulSemiringAction.charpoly H b) = ∏ τ : H, (b - σ • τ • b)

Evaluating a transformed characteristic polynomial at the point gives the product of its displacements: (σ • charpoly H b)(b) = ∏ τ, (b - σ • τ • b).