Theorems · Inductive type · commutative algebra

Algebra.IsInvariant

(A : Type u_1) →
  (B : Type u_2) →
    (G : Type u_3) →
      [inst : CommSemiring A] →
        [inst_1 : Semiring B] → [Algebra A B] → [inst : 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).

Defined in

Mathlib.RingTheory.Invariant.Defs

Cited by

28 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommSemiringSemiringAlgebraGroupMulSemiringAction