Abelian extensions

In this file, we define the typeclass of abelian extensions and provide some basic API.

class IsAbelianGalois (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] extends IsGalois K L, IsMulCommutative Gal(L/K) : Prop

The class of abelian extensions, defined as galois extensions whose galois group is commutative.

• to_isSeparable : Algebra.IsSeparable K L
• to_normal : Normal K L
• is_comm : Std.Commutative fun (x1 x2 : Gal(L/K)) => x1 * x2

theorem IsAbelianGalois.tower_bot (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsAbelianGalois K M] : IsAbelianGalois K L

theorem IsAbelianGalois.tower_top (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsAbelianGalois K M] : IsAbelianGalois L M

theorem IsAbelianGalois.of_algHom {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] (f : L →ₐ[K] M) [IsAbelianGalois K M] : IsAbelianGalois K L

instance instIsAbelianGaloisSubtypeMemIntermediateField (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsAbelianGalois K L] (K' : IntermediateField K L) : IsAbelianGalois K ↥K'

instance instIsAbelianGaloisSubtypeMemIntermediateField_1 (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra K L] [IsAbelianGalois K L] (K' : IntermediateField K L) : IsAbelianGalois (↥K') L

instance instIsAbelianGalois (K : Type u_1) [Field K] : IsAbelianGalois K K

instance instIsAbelianGaloisSubtypeMemIntermediateFieldBot (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : IsAbelianGalois K ↥⊥

theorem IsAbelianGalois.of_isCyclic (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] : IsAbelianGalois K L

instance IsAbelianGalois.sup {F : Type u_4} {E : Type u_5} [Field F] [Field E] [Algebra F E] (K L : IntermediateField F E) [IsAbelianGalois F ↥K] [IsAbelianGalois F ↥L] : IsAbelianGalois F ↥(K ⊔ L)

The compositum of two abelian extensions is abelian: its Galois group embeds into the product of the (commutative) factor Galois groups.