Theorems · Definition · commutative algebra

IsGaloisGroup.mulSemiringActionQuotient

(G : Type u_1) →
  [inst : Group G] →
    (B : Type u_3) →
      (C : Type u_4) →
        [inst_1 : Semiring C] →
          [inst_2 : MulSemiringAction G C] →
            (N : Subgroup G) →
              [inst_3 : CommSemiring B] →
                [inst_4 : Algebra B C] →
                  [FaithfulSMul B C] → [IsGaloisGroup (↥N) B C] → [inst_7 : N.Normal] → MulSemiringAction (G ⧸ N) B

If N is a normal subgroup of G and IsGaloisGroup N B C, then the quotient group G ⧸ N acts on B by (g : G ⧸ N) • x = g • x.

Defined in

Mathlib.RingTheory.IsGaloisGroup.Basic

Cited by

2 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupSemiringMulSemiringActionCommSemiringAlgebraFaithfulSMulIsGaloisGroupSubgroup.Normal