Normal closure of an extension of domains

We define the normal closure of an extension of domains R ⊆ S as a domain T such that R ⊆ S ⊆ T and the extension Frac T / Frac R is Galois, and prove several instances about it.

Under the hood, T is defined as the integralClosure of S inside the IntermediateField.normalClosure of the extension Frac S / Frac R inside the AlgebraicClosure of Frac S. In particular, if S is a Dedekind domain, then T is also a Dedekind domain.

Technical notes

• Many instances are proved about the IntermediateField.normalClosure of the extension Frac S / Frac R inside the AlgebraicClosure of Frac S. However these are only needed for the construction of T and to prove some results about it. Therefore, these instances are local.
• Ring.NormalClosure is defined as a type rather than a Subalgebra for performance reasons (and thus we need to provide explicit instances for it). Although defining it as a Subalgebra does not cause timeouts in this file, it does slow down considerably its compilation and does trigger timeouts in applications.

def Ring.instAlgebraFractionRing (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : Algebra (FractionRing R) (FractionRing S)

We register this specific instance as a local instance rather than making FractionRing.liftAlgebra a local instance because the latter causes timeouts since it is too general.

Equations

• Ring.instAlgebraFractionRing R S = FractionRing.liftAlgebra R (FractionRing S)

def Ring.instAlgebraSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : Algebra S ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))

This is a local instance since it is only used in this file to construct Ring.NormalClosure.

Equations

• One or more equations did not get rendered due to their size.

theorem Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : IsScalarTower S (FractionRing S) ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))

def Ring.NormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : Type u_2

The normal closure of an extension of domains R ⊆ S. It is defined as a domain T such that R ⊆ S ⊆ T and Frac T / Frac R is Galois.

Equations

• Ring.NormalClosure R S = ↥(integralClosure S ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S))))

instance Ring.instCommRingNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : CommRing (NormalClosure R S)

Equations

• One or more equations did not get rendered due to their size.

instance Ring.instIsDomainNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : IsDomain (NormalClosure R S)

instance Ring.instNontrivialNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : Nontrivial (NormalClosure R S)

instance Ring.instAlgebraNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : Algebra S (NormalClosure R S)

Equations

• One or more equations did not get rendered due to their size.

def Ring.instAlgebraNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : Algebra (NormalClosure R S) ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))

This is a local instance since it is only used in this file to construct Ring.NormalClosure.

Equations

• One or more equations did not get rendered due to their size.

instance Ring.instAlgebraNormalClosure_1 (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : Algebra R (NormalClosure R S)

Equations

• Ring.instAlgebraNormalClosure_1 R S = ((algebraMap S (Ring.NormalClosure R S)).comp (algebraMap R S)).toAlgebra

theorem Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : IsScalarTower S (NormalClosure R S) ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))

theorem Ring.instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : IsIntegralClosure (NormalClosure R S) S ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))

instance Ring.instIsScalarTowerNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : IsScalarTower R S (NormalClosure R S)

theorem Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1 (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : IsScalarTower R (FractionRing S) ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))

theorem Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : IsScalarTower R S ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))

theorem Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1 (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : IsScalarTower R (NormalClosure R S) ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))

theorem Ring.instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : FaithfulSMul S ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))

instance Ring.instNoZeroSMulDivisorsNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : NoZeroSMulDivisors S (NormalClosure R S)

instance Ring.instFaithfulSMulNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] : FaithfulSMul R (NormalClosure R S)

theorem Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] [Module.Finite R S] : FiniteDimensional (FractionRing S) ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))

theorem Ring.instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] [Module.Finite R S] : IsFractionRing (NormalClosure R S) ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))

instance Ring.instIsIntegrallyClosedNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] [Module.Finite R S] : IsIntegrallyClosed (NormalClosure R S)

theorem Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] [Module.Finite R S] [PerfectField (FractionRing R)] : Algebra.IsSeparable (FractionRing S) ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))

instance Ring.instIsGaloisFractionRingNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] [Module.Finite R S] [PerfectField (FractionRing R)] : IsGalois (FractionRing R) (FractionRing (NormalClosure R S))

instance Ring.instFiniteNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] [Module.Finite R S] [PerfectField (FractionRing R)] [IsDedekindDomain S] : Module.Finite S (NormalClosure R S)

instance Ring.instFiniteNormalClosure_1 (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] [Module.Finite R S] [PerfectField (FractionRing R)] [IsDedekindDomain S] : Module.Finite R (NormalClosure R S)

instance Ring.instIsDedekindDomainNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S] [Module.Finite R S] [PerfectField (FractionRing R)] [IsDedekindDomain S] : IsDedekindDomain (NormalClosure R S)