Invariant Extensions of Rings

Given an extension of rings B/A and an action of G on B, we introduce a predicate Algebra.IsInvariant A B G which states that every fixed point of B lies in the image of A.

The main application is in algebraic number theory, where G := Gal(L/K) is the galois group of some finite galois extension of number fields, and A := 𝓞K and B := 𝓞L are their rings of integers.

class Algebra.IsInvariant (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommSemiring A] [Semiring B] [Algebra A B] [Group G] [MulSemiringAction G B] : Prop

An action of a group G on an extension of rings B/A is invariant if every fixed point of B lies in the image of A. The converse statement that every point in the image of A is fixed by G is smul_algebraMap (assuming SMulCommClass A B G).

• isInvariant (b : B) : (∀ (g : G), g • b = b) → ∃ (a : A), (algebraMap A B) a = b

theorem Algebra.isInvariant_iff (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommSemiring A] [Semiring B] [Algebra A B] [Group G] [MulSemiringAction G B] : IsInvariant A B G ↔ ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), (algebraMap A B) a = b