Definitions/Def_Mathlib_RingTheory_Invariant_FixedSubringGaloisGroup.lean

The standing context is a commutative ring S together with a group G acting on S by ring automorphisms (a MulSemiringAction), the action being faithful. The single result, FixedPoints.isGaloisGroup_subring, asserts that G is a Galois group for the extension of S over its fixed-point subring S^G = FixedPoints.subring S G, i.e. that IsGaloisGroup G (FixedPoints.subring S G) S holds. Since IsGaloisGroup is a structure all of whose fields are propositions, the content of the statement is exactly the conjunction of its three fields, each verified here for the fixed subring: faithfulness of the G-action on S, which is the standing hypothesis; compatibility of the G-action with multiplication by scalars from the base, namely g \cdot (r s) = r\,(g \cdot s) for r \in S^G and s \in S, which follows because g is a ring automorphism and fixes r; and the invariance condition Algebra.IsInvariant for the base S^G in S with respect to G, i.e. that every b \in S with g \cdot b = b for all g \in G is the image of an element of the base — tautological here, as the base has been taken to be precisely the subring of G-fixed elements. Thus the lemma supplies, for an arbitrary faithful action of a group by ring automorphisms, the canonical instance of the Galois-group hypothesis used by the invariant-theoretic and ramification-theoretic machinery, with no auxiliary condition such as finiteness of G or normality.