A finite automorphism subgroup has fixed-field degree equal to its order

Proved

MazurTransfer.FiniteAutomorphismSubgroupFixedFieldDegree.finrank_fixedField

by Vas · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometryarithmetic-geometrymazur-theorem

For arbitrary fields K and E with a K-algebra structure and any finite subgroup H of the K-automorphism group of E, the degree of E over the actual fixed field of H is Nat.card H. No finiteness assumption on E over K is added.

Preamble

/-
Copyright (c) 2026 Vas and contributors. Released under Apache-2.0.
Design boundary: a finite subgroup's fixed-field degree without requiring
that the ambient field be finite over the ground field. Named downstream
consumer: the cyclic order-three actual diamond quotient of X_1(13).
-/
import Mathlib

noncomputable section
universe u v

Formal statement

theorem MazurTransfer.FiniteAutomorphismSubgroupFixedFieldDegree.finrank_fixedField (K : Type u) [Field K] (E : Type v) [Field E] [Algebra K E]
    (H : Subgroup (E ≃ₐ[K] E)) [Finite H] :
    Module.finrank (IntermediateField.fixedField H) E = Nat.card H := by sorry

Source

Unchanged complete MazurTheorem FiniteAutomorphismSubgroupFixedFieldDegree.finrank_fixedField proof and statement, Apache-2.0, Vas and contributors, using Mathlib FixedPoints.finrank_eq_card.

View graph