ModuleCompositumEmbedding.lean
Nyll.ClassFieldTheory.AlgebraicNumberTheory.CompositumEmbedding
4 declarations indexed from sourceView source ↗ Module documentation
Embedding a finite Galois compositum into a common field
Two finite normal extensions embedded in a common field generate the same compositum as their chosen realizations in the separable closure. This normality argument is the field-theoretic mechanism used to place the local inertia-field compositum in one cyclotomic target.
Declarations
AlgebraicNumberTheory.cyclotomicFieldEmbeddingOfDvd
DocumentationDivisibility of cyclotomic orders gives an embedding of the smaller concrete cyclotomic field into the larger one.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace AlgebraicNumberTheory
open Polynomial
AlgebraicNumberTheory.cyclotomicFieldEmbeddingOfBaseAndDvd
DocumentationBase extension and divisibility of cyclotomic orders together give an embedding into the larger cyclotomic field over the enlarged base.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace AlgebraicNumberTheory
open Polynomial
AlgebraicNumberTheory.finiteGaloisCompositumEmbeddingOfEmbeddings
DocumentationIf two finite Galois extensions embed in one field, their concrete compositum in the chosen separable closure embeds in that field as well.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace AlgebraicNumberTheory
open Polynomial
variable (K L E T : Type)
variable [Field K] [Field L] [Field E] [Field T]
variable [Algebra K L] [Algebra K E] [Algebra K T]
variable [FiniteDimensional K L] [FiniteDimensional K E]
variable [IsAbelianGalois K L] [IsAbelianGalois K E]
AlgebraicNumberTheory.exists_finiteGaloisCompositumEmbeddingOfEmbeddings_left_eq
DocumentationThe common-target embedding can be chosen to agree with the prescribed embedding of the left factor. Normality first identifies the two copies of the left field; the correcting automorphism then extends to the whole Galois compositum.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace AlgebraicNumberTheory
open Polynomial
variable (K L E T : Type)
variable [Field K] [Field L] [Field E] [Field T]
variable [Algebra K L] [Algebra K E] [Algebra K T]
variable [FiniteDimensional K L] [FiniteDimensional K E]
variable [IsAbelianGalois K L] [IsAbelianGalois K E]