Module

SeparableClosureEmbedding.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.SeparableClosureEmbedding

6 declarations indexed from sourceView source ↗

Module documentation

Embeddings into a separable closure

This file provides the common realization of a separable extension inside the chosen separable closure of its base field.

Imports3

Mathlib.FieldTheory.IsSepClosed
Mathlib.FieldTheory.KrullTopology
Mathlib.NumberTheory.NumberField.Basic

Imported by13

theorem

continuous_algEquiv_autCongr

L28 ↗

AlgebraicNumberTheory.continuous_algEquiv_autCongr

Documentation

Conjugation by a field equivalence is continuous on automorphism groups equipped with the Krull topology.

Source context 3 commands

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

noncomputable section
namespace AlgebraicNumberTheory
universe u v

Lean source · statement

theorem continuous_algEquiv_autCongr
    {F E E' : Type*}
    [Field F] [Field E] [Field E']
    [Algebra F E] [Algebra F E']
    (e : E ≃ₐ[F] E') :
    Continuous (AlgEquiv.autCongr e)

def

separableEmbeddingIntoSeparableClosure

L64 ↗

AlgebraicNumberTheory.separableEmbeddingIntoSeparableClosure

Documentation

A chosen embedding of a separable extension into the separable closure of its base field.

Source context 4 commands

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

noncomputable section
namespace AlgebraicNumberTheory
universe u v
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
  [Algebra.IsSeparable K L]

Lean source · statement

def separableEmbeddingIntoSeparableClosure :
    L →ₐ[K] SeparableClosure K

def

numberFieldSeparableClosureEmbedding

L72 ↗

AlgebraicNumberTheory.numberFieldSeparableClosureEmbedding

Documentation

A chosen ℚ-embedding of a number field into mathlib's fixed separable closure of ℚ.

Source context 5 commands

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

noncomputable section
namespace AlgebraicNumberTheory
universe u v
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
  [Algebra.IsSeparable K L]
variable (K : Type*) [Field K] [NumberField K]

Lean source · statement

def numberFieldSeparableClosureEmbedding :
    K →ₐ[ℚ] SeparableClosure ℚ

def

numberFieldInRationalSeparableClosure

L78 ↗

AlgebraicNumberTheory.numberFieldInRationalSeparableClosure

Documentation

The actual copy of K cut out by the chosen embedding into SeparableClosure ℚ.

Source context 5 commands

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

noncomputable section
namespace AlgebraicNumberTheory
universe u v
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
  [Algebra.IsSeparable K L]
variable (K : Type*) [Field K] [NumberField K]

Lean source · statement

def numberFieldInRationalSeparableClosure :
    IntermediateField ℚ (SeparableClosure ℚ)

instance

numberFieldInRationalSeparableClosure_finiteDimensional

L82 ↗

AlgebraicNumberTheory.numberFieldInRationalSeparableClosure_finiteDimensional

Source context 5 commands

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

noncomputable section
namespace AlgebraicNumberTheory
universe u v
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
  [Algebra.IsSeparable K L]
variable (K : Type*) [Field K] [NumberField K]

Lean source · statement

instance
    numberFieldInRationalSeparableClosure_finiteDimensional :
    FiniteDimensional ℚ
      (numberFieldInRationalSeparableClosure K)

instance

numberFieldInRationalSeparableClosure_numberField

L88 ↗

AlgebraicNumberTheory.numberFieldInRationalSeparableClosure_numberField

Source context 5 commands

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

noncomputable section
namespace AlgebraicNumberTheory
universe u v
variable (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
  [Algebra.IsSeparable K L]
variable (K : Type*) [Field K] [NumberField K]

Lean source · full declaration

instance
    numberFieldInRationalSeparableClosure_numberField :
    NumberField (numberFieldInRationalSeparableClosure K) where
  to_charZero := inferInstance
  to_finiteDimensional := inferInstance

Module documentation

Embeddings into a separable closure

Declarations

continuous_algEquiv_autCongr

separableEmbeddingIntoSeparableClosure

numberFieldSeparableClosureEmbedding

numberFieldInRationalSeparableClosure

numberFieldInRationalSeparableClosure_finiteDimensional

numberFieldInRationalSeparableClosure_numberField