Integral closures in a Galois extension over a Dedekind base

Let A be a Dedekind domain with fraction field K, let M / K be a finite Galois extension, and let B be the integral closure of A in M. For a subgroup H of Gal(M/K), let C be the integral closure of A in the fixed field M ^ H. This file bundles the structure that a Dedekind base provides for these rings: B is a domain, finite and flat over A, with Galois group Gal(M/K), and C is a Dedekind domain, finite and flat over A. Together with TauCeti.IsIntegralClosure.isGaloisGroup_fixedField_and_faithfulSMul, these are the instances needed to specialize statements about invariant rings to integral closures.

The statement for C only requires that M ^ H be finite and separable over K; the ambient extension M / K need not be finite or Galois.

Main results

• TauCeti.IsIntegralClosure.isDomain_and_finite_and_flat_and_isGaloisGroup: B is a domain, finite and flat over A, with Galois group Gal(M/K).
• TauCeti.IsIntegralClosure.isDedekindDomain_and_finite_and_flat_fixedField: C is a Dedekind domain, finite and flat over A.

theorem TauCeti.IsIntegralClosure.isDomain_and_finite_and_flat_and_isGaloisGroup {A : Type u_1} {K : Type u_2} {M : Type u_3} [CommRing A] [IsDedekindDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [Field M] [Algebra K M] [FiniteDimensional K M] [IsGalois K M] {B : Type u_4} [Algebra A M] [IsScalarTower A K M] [CommRing B] [Algebra A B] [Algebra B M] [IsScalarTower A B M] [IsIntegralClosure B A M] [MulSemiringAction Gal(M/K) B] [SMulDistribClass Gal(M/K) B M] : IsDomain B ∧ Module.Finite A B ∧ Module.Flat A B ∧ IsGaloisGroup Gal(M/K) A B

Over a Dedekind base, B is a finite flat A-algebra and a domain, with Galois group Gal(M/K).

theorem TauCeti.IsIntegralClosure.isDedekindDomain_and_finite_and_flat_fixedField {A : Type u_1} {K : Type u_2} {M : Type u_3} [CommRing A] [IsDedekindDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [Field M] [Algebra K M] (H : Subgroup Gal(M/K)) [Module.Finite K ↥(IntermediateField.fixedField H)] [Algebra.IsSeparable K ↥(IntermediateField.fixedField H)] [Algebra A ↥(IntermediateField.fixedField H)] [IsScalarTower A K ↥(IntermediateField.fixedField H)] (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C ↥(IntermediateField.fixedField H)] [IsScalarTower A C ↥(IntermediateField.fixedField H)] [IsIntegralClosure C A ↥(IntermediateField.fixedField H)] : IsDedekindDomain C ∧ Module.Finite A C ∧ Module.Flat A C

Over a Dedekind base, the integral closure in a finite separable fixed field is a Dedekind domain and a finite flat A-algebra. The ambient extension need not be finite or Galois.