Invariant Extensions of Rings and Galois Theory

Given an extension of rings B/A and an action of G on B, the predicate Algebra.IsInvariant A B G states that every fixed point of B lies in the image of A.

This file relates this predicate Algebra.IsInvariant to Galois theory.

@[implicit_reducible]

noncomputable def IsIntegralClosure.MulSemiringAction (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 B L] [IsFractionRing A K] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra.IsAlgebraic K L] : _root_.MulSemiringAction Gal(L/K) B

In the AKLB setup, the Galois group of L/K acts on B.

Equations

• IsIntegralClosure.MulSemiringAction A K L B = MulSemiringAction.compHom B (galRestrict A K L B).toMonoidHom

instance instSMulDistribClassAlgEquiv (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 B L] [IsFractionRing A K] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsIntegralClosure B A L] [Algebra.IsAlgebraic K L] : have this := IsIntegralClosure.MulSemiringAction A K L B; SMulDistribClass Gal(L/K) B L

theorem Algebra.isInvariant_of_isGalois (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 B L] [IsFractionRing A K] [IsFractionRing B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsIntegrallyClosed A] [IsIntegralClosure B A L] [FiniteDimensional K L] [h : IsGalois K L] : IsInvariant A B Gal(L/K)

In the AKLB setup, every fixed point of B lies in the image of A.

theorem Algebra.isInvariant_of_isGalois' (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 B L] [IsFractionRing A K] [IsFractionRing B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsIntegrallyClosed A] [IsIntegralClosure B A L] [FiniteDimensional K L] [IsGalois K L] : IsInvariant A B (B ≃ₐ[A] B)

A variant of Algebra.isInvariant_of_isGalois, replacing Gal(L/K) by Aut(B/A).

theorem Ideal.IsFractionRing.normal {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Finite G] [Group G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] (P : Ideal A) (Q : Ideal B) [Q.LiesOver P] [P.IsPrime] [Q.IsPrime] (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] [Algebra (A ⧸ P) K] [IsFractionRing (A ⧸ P) K] [Algebra (B ⧸ Q) L] [IsFractionRing (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] [IsScalarTower (A ⧸ P) K L] : Normal K L

theorem Ideal.IsFractionRing.finite_of_isInvariant {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Finite G] [Group G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] (P : Ideal A) (Q : Ideal B) [Q.LiesOver P] [P.IsPrime] [Q.IsPrime] (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] [Algebra (A ⧸ P) K] [IsFractionRing (A ⧸ P) K] [Algebra (B ⧸ Q) L] [IsFractionRing (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] [IsScalarTower (A ⧸ P) K L] [SMulCommClass G A B] [Algebra.IsSeparable K L] : Module.Finite K L

theorem Ideal.Quotient.normal {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Finite G] [Group G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] (P : Ideal A) (Q : Ideal B) [Q.LiesOver P] [P.IsMaximal] [Q.IsMaximal] : Normal (A ⧸ P) (B ⧸ Q)

For any domain k containing B ⧸ Q, any endomorphism of k can be restricted to an endomorphism of B ⧸ Q.

theorem Ideal.Quotient.finite_of_isInvariant {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Finite G] [Group G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] (P : Ideal A) (Q : Ideal B) [Q.LiesOver P] [P.IsMaximal] [Q.IsMaximal] [SMulCommClass G A B] [Algebra.IsSeparable (A ⧸ P) (B ⧸ Q)] : Module.Finite (A ⧸ P) (B ⧸ Q)

If the extension B/Q over A/P is separable, then it is finite dimensional.