NYLL
Module

CyclotomicExtension.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.CyclotomicExtension
2 declarations indexed from sourceView source ↗

Module documentation

Cyclotomic extensions and infinite orientations

Adjoining every primary root of unity gives the primary cyclotomic extension. Infinite degree of that extension forces the absolute cyclotomic orientation to have infinite image.

Imports2
Imported by2

Declarations

def

primaryCyclotomicExtension

L22 ↗
Yamaguchi26AbfaithfulGalois.primaryCyclotomicExtension
Documentation

The actual field obtained by adjoining every p-power root of unity.

Source context 2 commands

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

namespace Yamaguchi26AbfaithfulGalois
universe u
Lean source · statement
def primaryCyclotomicExtension (K : Type u) [Field K] (p : ℕ) :
    IntermediateField K (SeparableClosure K)
theorem

infinite_range_absoluteCyclotomicOrientation_of_infinite_extension

L30 ↗
Yamaguchi26AbfaithfulGalois.infinite_range_absoluteCyclotomicOrientation_of_infinite_extension
Documentation

Infinite degree of the cyclotomic extension forces the absolute cyclotomic orientation to have infinite image.

Source context 2 commands

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

namespace Yamaguchi26AbfaithfulGalois
universe u
Lean source · statement
theorem infinite_range_absoluteCyclotomicOrientation_of_infinite_extension
    (p : ℕ) [Fact p.Prime] (K : Type u) [Field K] [NeZero (p : K)]
    (hdegree : ¬ FiniteDimensional K (primaryCyclotomicExtension K p)) :
    Set.Infinite (Set.range (absoluteCyclotomicOrientation p K))

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