Galois groups of integral closures

If G is a finite Galois group of a field extension M / L and C is an integrally closed domain with fraction field L, then G is a Galois group of the integral closure B of C in M over C, for any action of G on B compatible with its action on M.

Mathlib's IsGaloisGroup.of_isFractionRing states this with M a fraction field of B and B / C integral; both follow from B being the integral closure of C in M, which is how the rings arise over a Dedekind base. The second statement is the form needed for a tower: for a domain A with fraction field K, a finite extension L of K, an extension M of L, and the integral closures C and B of A in L and in M, a Galois group of M / L is a Galois group of B / C. The third statement specializes the tower to a fixed field: for a finite extension M / K and a subgroup H of Gal(M/K), with C the integral closure of A in M ^ H, the subgroup H is a Galois group of B / C.

Main results

• IsGaloisGroup.of_isIntegralClosure: a Galois group of M / L is a Galois group of the integral closure of C in M over C.
• IsGaloisGroup.of_isIntegralClosure_tower: the same for the integral closures of a common base A in L and in M.
• IsGaloisGroup.of_isIntegralClosure_fixedField: a subgroup H of Gal(M/K) is a Galois group of the integral closures of a common base in M ^ H and in M.
• TauCeti.IsIntegralClosure.isGaloisGroup_fixedField_and_faithfulSMul: the same, bundled with the injectivity of C → B, as used to set up instances for the fixed-field integral closure.

theorem IsIntegralClosure.smulCommClass (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Field K] [Field L] [Algebra A K] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [Algebra A B] [Algebra B L] [IsScalarTower A B L] [IsFractionRing A K] [IsIntegralClosure B A L] [Algebra.IsAlgebraic K L] : SMulCommClass Gal(L/K) A B

The action of Gal(L/K) on an integral closure B of A in L commutes with the action of A, since it is the restriction of the action by K-algebra automorphisms of L.

theorem IsGaloisGroup.of_isIntegralClosure (G : Type u_1) (C : Type u_2) (B : Type u_3) (L : Type u_4) (M : Type u_5) [Group G] [Finite G] [CommRing C] [CommRing B] [Algebra C B] [Field L] [Field M] [Algebra C L] [Algebra L M] [Algebra C M] [Algebra B M] [IsScalarTower C L M] [IsScalarTower C B M] [IsFractionRing C L] [IsIntegrallyClosed C] [IsIntegralClosure B C M] [MulSemiringAction G M] [MulSemiringAction G B] [SMulDistribClass G B M] [IsGaloisGroup G L M] : IsGaloisGroup G C B

A Galois group of fields is a Galois group of integral closures. If G is a finite Galois group of M / L, where L is the fraction field of an integrally closed domain C, then G is a Galois group of the integral closure of C in M over C.

theorem IsGaloisGroup.of_isIntegralClosure_tower (G : Type u_1) (A : Type u_2) (K : Type u_3) (L : Type u_4) (M : Type u_5) (C : Type u_6) (B : Type u_7) [Group G] [Finite G] [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] [Field M] [Algebra L M] [Algebra A M] [CommRing C] [Algebra A C] [Algebra C L] [IsScalarTower A C L] [IsIntegralClosure C A L] [CommRing B] [Algebra A B] [Algebra B M] [IsScalarTower A B M] [IsIntegralClosure B A M] [Algebra C B] [Algebra C M] [IsScalarTower A C B] [IsScalarTower C L M] [IsScalarTower C B M] [MulSemiringAction G M] [MulSemiringAction G B] [SMulDistribClass G B M] [IsGaloisGroup G L M] : IsGaloisGroup G C B

Galois groups in a tower of integral closures. Let A be a domain with fraction field K, let L be a finite extension of K and M an extension of L, and let C and B be the integral closures of A in L and in M. A finite Galois group of M / L is then a Galois group of B over C.

theorem IsGaloisGroup.of_isIntegralClosure_fixedField (A : Type u_1) {K : Type u_2} {M : Type u_3} [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [Field M] [Algebra K M] [FiniteDimensional K M] [Algebra A M] (H : Subgroup Gal(M/K)) [Algebra A ↥(IntermediateField.fixedField H)] [IsScalarTower A K ↥(IntermediateField.fixedField H)] (C : Type u_4) (B : Type u_5) [CommRing C] [Algebra A C] [Algebra C ↥(IntermediateField.fixedField H)] [IsScalarTower A C ↥(IntermediateField.fixedField H)] [IsIntegralClosure C A ↥(IntermediateField.fixedField H)] [CommRing B] [Algebra A B] [Algebra B M] [IsScalarTower A B M] [IsIntegralClosure B A M] [Algebra C B] [Algebra C M] [IsScalarTower A C B] [IsScalarTower C (↥(IntermediateField.fixedField H)) M] [IsScalarTower C B M] [MulSemiringAction Gal(M/K) B] [SMulDistribClass Gal(M/K) B M] : IsGaloisGroup (↥H) C B

Fixed-field subgroups as Galois groups of integral closures. Let A be a domain with fraction field K, let M / K be a finite extension, and let H be a subgroup of Gal(M/K). If C and B are the integral closures of A in the fixed field M ^ H and in M, then H is a Galois group of B over C. The extension M / K need not be Galois.

theorem TauCeti.IsIntegralClosure.isGaloisGroup_fixedField_and_faithfulSMul (A : Type u_1) {K : Type u_2} {M : Type u_3} [CommRing A] [IsDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [Field M] [Algebra K M] [FiniteDimensional K M] [Algebra A M] (H : Subgroup Gal(M/K)) [Algebra A ↥(IntermediateField.fixedField H)] [IsScalarTower A K ↥(IntermediateField.fixedField H)] (C : Type u_4) (B : Type u_5) [CommRing C] [Algebra A C] [Algebra C ↥(IntermediateField.fixedField H)] [IsScalarTower A C ↥(IntermediateField.fixedField H)] [IsIntegralClosure C A ↥(IntermediateField.fixedField H)] [CommRing B] [Algebra A B] [Algebra B M] [IsScalarTower A B M] [IsIntegralClosure B A M] [Algebra C B] [Algebra C M] [IsScalarTower A C B] [IsScalarTower C (↥(IntermediateField.fixedField H)) M] [IsScalarTower C B M] [MulSemiringAction Gal(M/K) B] [SMulDistribClass Gal(M/K) B M] : IsGaloisGroup (↥H) C B ∧ FaithfulSMul C B

The subgroup H is a Galois group of B over C, and C embeds in B.