NYLL
Module

UnboundedDegree.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.UnboundedDegree
2 declarations indexed from sourceView source ↗

Module documentation

Unbounded finite Galois degrees inside an infinite Galois extension

A finite-dimensional extension has only finitely many automorphisms. An infinite Galois group therefore supplies arbitrarily large linearly independent finite families. Their finite Galois closures give the required actual intermediate fields.

Imports7
  • Mathlib.FieldTheory.Galois.GaloisClosure
  • Mathlib.FieldTheory.IntermediateField.Basic
  • Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
  • Mathlib.Algebra.Algebra.Equiv
  • Mathlib.LinearAlgebra.Dimension.Free
  • Mathlib.LinearAlgebra.Dimension.Finite
  • Mathlib.LinearAlgebra.LinearIndependent.Defs
Imported by2

Declarations

theorem

exists_finiteGaloisIntermediateField_finrank_ge_of_infinite_aut

L30 ↗
AlgebraicNumberTheory.exists_finiteGaloisIntermediateField_finrank_ge_of_infinite_aut
Documentation

An extension with infinitely many base-field automorphisms contains finite Galois intermediate fields of arbitrarily large degree.

Source context 2 commands

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

namespace AlgebraicNumberTheory
universe u v
Lean source · statement
theorem exists_finiteGaloisIntermediateField_finrank_ge_of_infinite_aut
    (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
    [IsGalois K L] [Infinite (L ≃ₐ[K] L)] (N : ℕ) :
    ∃ M : FiniteGaloisIntermediateField K L, N ≤ Module.finrank K M
theorem

exists_finiteGaloisIntermediateField_le_finrank_ge_of_infinite_aut

L56 ↗
AlgebraicNumberTheory.exists_finiteGaloisIntermediateField_le_finrank_ge_of_infinite_aut
Documentation

An infinite Galois intermediate extension contains ambient finite Galois intermediate fields of arbitrarily large degree. The actual lift keeps the field inclusion available to arithmetic consumers.

Source context 2 commands

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

namespace AlgebraicNumberTheory
universe u v
Lean source · statement
theorem exists_finiteGaloisIntermediateField_le_finrank_ge_of_infinite_aut
    (K : Type u) (Ω : Type v) [Field K] [Field Ω] [Algebra K Ω]
    (L : IntermediateField K Ω) [IsGalois K L] [Infinite (L ≃ₐ[K] L)]
    (N : ℕ) :
    ∃ E : FiniteGaloisIntermediateField K Ω,
      E.toIntermediateField ≤ L ∧ N ≤ Module.finrank K E

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