Theorems · Theorem · field theory

IsGaloisGroup.fixingSubgroup_range_algebraMap

∀ (G : Type u_1) [inst : Group G] [Finite G] (A : Type u_5) (B : Type u_6) (C : Type u_7) (H : Subgroup G)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : CommRing C] [IsDomain C] [inst_6 : Algebra A C]
  [FaithfulSMul A C] [inst_8 : MulSemiringAction G C] [hGAC : IsGaloisGroup G A C] [inst_9 : Algebra B C]
  [FaithfulSMul B C] [hH : IsGaloisGroup (↥H) B C], fixingSubgroup G (Set.range ⇑(algebraMap B C)) = H

If G acts on a domain C with IsGaloisGroup G A C, and a subgroup H acts on C with IsGaloisGroup H B C, then the fixing subgroup of algebraMap B C equals H.

Defined in

Mathlib.FieldTheory.Galois.IsGaloisGroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupFiniteCommRingCommRingCommRingIsDomainAlgebraFaithfulSMulMulSemiringActionIsGaloisGroupAlgebraFaithfulSMulIsGaloisGroup