NYLL
Module

FiniteAbelianCompositum.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.FiniteAbelianCompositum
13 declarations indexed from sourceView source ↗

Module documentation

Finite abelian composita

This file gives a common realization, in a chosen separable closure, of the compositum of two finite abelian Galois extensions. It also records the canonical factor embeddings and their elementary degree bounds.

Imports3
Imported by4

Declarations

def

finiteGaloisFieldRange

L30 ↗
AlgebraicNumberTheory.finiteGaloisFieldRange
Documentation

The chosen copy of a finite Galois extension in the separable closure.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory
open scoped IsMulCommutative
universe u v
Lean source · statement
def finiteGaloisFieldRange
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L] :
    IntermediateField K (SeparableClosure K)
def

finiteGaloisFieldRangeEquiv

L38 ↗
AlgebraicNumberTheory.finiteGaloisFieldRangeEquiv
Documentation

The chosen embedding identifies the extension with its field range.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory
open scoped IsMulCommutative
universe u v
Lean source · statement
def finiteGaloisFieldRangeEquiv
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L] :
    L ≃ₐ[K] finiteGaloisFieldRange K L
instance

finiteGaloisFieldRange_finiteDimensional

L46 ↗
AlgebraicNumberTheory.finiteGaloisFieldRange_finiteDimensional
Documentation

The chosen field-range model is finite-dimensional over the base.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory
open scoped IsMulCommutative
universe u v
Lean source · statement
instance finiteGaloisFieldRange_finiteDimensional
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L] :
    FiniteDimensional K (finiteGaloisFieldRange K L)
instance

finiteGaloisFieldRange_isGalois

L53 ↗
AlgebraicNumberTheory.finiteGaloisFieldRange_isGalois
Documentation

The chosen field-range model is Galois over the base.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory
open scoped IsMulCommutative
universe u v
Lean source · statement
instance finiteGaloisFieldRange_isGalois
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L] :
    IsGalois K (finiteGaloisFieldRange K L)
theorem

isAbelianGalois_sup

L66 ↗
AlgebraicNumberTheory.isAbelianGalois_sup
Documentation

The compositum, inside a common overfield, of two abelian Galois intermediate fields is again abelian Galois over the base.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory
open scoped IsMulCommutative
universe u v
section AbelianCompositum
variable (K : Type u) [Field K]
variable {Omega : Type v} [Field Omega] [Algebra K Omega]
Lean source · statement
theorem isAbelianGalois_sup
    (A B : IntermediateField K Omega)
    [FiniteDimensional K A] [FiniteDimensional K B]
    [IsAbelianGalois K A] [IsAbelianGalois K B] :
    IsAbelianGalois K (A ⊔ B : IntermediateField K Omega)
def

finiteAbelianCompositumField

L139 ↗
AlgebraicNumberTheory.finiteAbelianCompositumField
Documentation

A concrete common realization of the compositum of two finite abelian extensions in the chosen separable closure of the base.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory
open scoped IsMulCommutative
universe u v
section ConcreteAbelianCompositum
variable (K L E : Type)
variable [Field K]
variable [Field L] [Field E] [Algebra K L] [Algebra K E]
variable [FiniteDimensional K L] [FiniteDimensional K E]
variable [IsAbelianGalois K L] [IsAbelianGalois K E]
Lean source · statement
def finiteAbelianCompositumField :
    IntermediateField K (SeparableClosure K)
instance

finiteAbelianCompositumField_finiteDimensional

L144 ↗
AlgebraicNumberTheory.finiteAbelianCompositumField_finiteDimensional
Documentation

The concrete compositum is finite-dimensional over the base.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory
open scoped IsMulCommutative
universe u v
section ConcreteAbelianCompositum
variable (K L E : Type)
variable [Field K]
variable [Field L] [Field E] [Algebra K L] [Algebra K E]
variable [FiniteDimensional K L] [FiniteDimensional K E]
variable [IsAbelianGalois K L] [IsAbelianGalois K E]
Lean source · statement
instance finiteAbelianCompositumField_finiteDimensional :
    FiniteDimensional K (finiteAbelianCompositumField K L E)
instance

finiteAbelianCompositumField_isAbelianGalois

L150 ↗
AlgebraicNumberTheory.finiteAbelianCompositumField_isAbelianGalois
Documentation

The concrete compositum is abelian Galois over the base.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory
open scoped IsMulCommutative
universe u v
section ConcreteAbelianCompositum
variable (K L E : Type)
variable [Field K]
variable [Field L] [Field E] [Algebra K L] [Algebra K E]
variable [FiniteDimensional K L] [FiniteDimensional K E]
variable [IsAbelianGalois K L] [IsAbelianGalois K E]
Lean source · statement
instance finiteAbelianCompositumField_isAbelianGalois :
    IsAbelianGalois K (finiteAbelianCompositumField K L E)
def

finiteAbelianCompositumEmbeddingLeft

L162 ↗
AlgebraicNumberTheory.finiteAbelianCompositumEmbeddingLeft
Documentation

The given left extension embeds into its concrete compositum.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory
open scoped IsMulCommutative
universe u v
section ConcreteAbelianCompositum
variable (K L E : Type)
variable [Field K]
variable [Field L] [Field E] [Algebra K L] [Algebra K E]
variable [FiniteDimensional K L] [FiniteDimensional K E]
variable [IsAbelianGalois K L] [IsAbelianGalois K E]
Lean source · statement
def finiteAbelianCompositumEmbeddingLeft :
    L →ₐ[K] finiteAbelianCompositumField K L E
def

finiteAbelianCompositumEmbeddingRight

L168 ↗
AlgebraicNumberTheory.finiteAbelianCompositumEmbeddingRight
Documentation

The given right extension embeds into its concrete compositum.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory
open scoped IsMulCommutative
universe u v
section ConcreteAbelianCompositum
variable (K L E : Type)
variable [Field K]
variable [Field L] [Field E] [Algebra K L] [Algebra K E]
variable [FiniteDimensional K L] [FiniteDimensional K E]
variable [IsAbelianGalois K L] [IsAbelianGalois K E]
Lean source · statement
def finiteAbelianCompositumEmbeddingRight :
    E →ₐ[K] finiteAbelianCompositumField K L E
theorem

finiteAbelianCompositum_embeddingRanges_sup_eq_top

L175 ↗
AlgebraicNumberTheory.finiteAbelianCompositum_embeddingRanges_sup_eq_top
Documentation

The images of the two canonical embeddings generate their concrete compositum.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory
open scoped IsMulCommutative
universe u v
section ConcreteAbelianCompositum
variable (K L E : Type)
variable [Field K]
variable [Field L] [Field E] [Algebra K L] [Algebra K E]
variable [FiniteDimensional K L] [FiniteDimensional K E]
variable [IsAbelianGalois K L] [IsAbelianGalois K E]
Lean source · statement
theorem finiteAbelianCompositum_embeddingRanges_sup_eq_top :
    (finiteAbelianCompositumEmbeddingLeft K L E).fieldRange ⊔
        (finiteAbelianCompositumEmbeddingRight K L E).fieldRange = ⊤
theorem

finiteAbelianCompositum_finrank_left_le

L252 ↗
AlgebraicNumberTheory.finiteAbelianCompositum_finrank_left_le
Documentation

The degree of the left factor is bounded by the degree of the compositum.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory
open scoped IsMulCommutative
universe u v
section ConcreteAbelianCompositum
variable (K L E : Type)
variable [Field K]
variable [Field L] [Field E] [Algebra K L] [Algebra K E]
variable [FiniteDimensional K L] [FiniteDimensional K E]
variable [IsAbelianGalois K L] [IsAbelianGalois K E]
Lean source · statement
theorem finiteAbelianCompositum_finrank_left_le :
    Module.finrank K L ≤
      Module.finrank K (finiteAbelianCompositumField K L E)
theorem

finiteAbelianCompositum_finrank_right_le

L261 ↗
AlgebraicNumberTheory.finiteAbelianCompositum_finrank_right_le
Documentation

The degree of the right factor is bounded by the degree of the compositum.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory
open scoped IsMulCommutative
universe u v
section ConcreteAbelianCompositum
variable (K L E : Type)
variable [Field K]
variable [Field L] [Field E] [Algebra K L] [Algebra K E]
variable [FiniteDimensional K L] [FiniteDimensional K E]
variable [IsAbelianGalois K L] [IsAbelianGalois K E]
Lean source · statement
theorem finiteAbelianCompositum_finrank_right_le :
    Module.finrank K E ≤
      Module.finrank K (finiteAbelianCompositumField K L E)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.