Documentation

Mathlib.RingTheory.NormalClosure

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 R] [IsDomain S] [Algebra R S] [Module.IsTorsionFree 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

Instances For

def Ring.instAlgebraSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [Module.IsTorsionFree 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

Instances For

theorem Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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

Instances For

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

CommRing (NormalClosure R S)

Equations

instance Ring.instIsDomainNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree R S] :

Algebra S (NormalClosure R S)

Equations

def Ring.instAlgebraNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [Module.IsTorsionFree 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

Instances For

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

Algebra R (NormalClosure R S)

Equations

theorem Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree R S] :

FaithfulSMul S ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))

instance Ring.instIsTorsionFreeNormalClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] [Module.IsTorsionFree R S] :

Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree 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] [Module.IsTorsionFree R S] [Module.Finite R S] [PerfectField (FractionRing R)] [IsDedekindDomain S] :

IsDedekindDomain (NormalClosure R S)