Documentation

Mathlib.RingTheory.Invariant.Galois

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.

source
@[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
Instances For
    source
    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
    source
    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.

    source
    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).

    source
    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

    If Q is a prime ideal of B lying over a prime ideal P of A, then the extension Frac(B/Q) over Frac(A/P) is normal.

    source
    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

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

    source
    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)

    If Q is a maximal ideal of B lying over a maximal ideal P of A, then the extension B/Q over A/P is normal.

    source
    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.