NYLL
Module

CyclotomicCompositumDegree.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.CyclotomicCompositumDegree
3 declarations indexed from sourceView source ↗

Module documentation

Degrees of actual cyclotomic composita

A common primitive root proves that the upper cyclotomic field is generated over the lower cyclotomic field by the other field's image. Coprime degrees then give the original prime degree after this base extension.

Imports2
Imported by2

Declarations

theorem

cyclotomic_compositum_adjoin_range_eq_top

L22 ↗
ValuationTheory.DiscreteValuationField.cyclotomic_compositum_adjoin_range_eq_top
Documentation

The lower cyclotomic field already contains a primitive generator of the upper cyclotomic extension, so adjoining the other field's image suffices.

Source context 1 command

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

namespace ValuationTheory.DiscreteValuationField
Lean source · statement
theorem cyclotomic_compositum_adjoin_range_eq_top
    (F K L E : Type*) [Field F] [Field K] [Field L] [Field E]
    [Algebra F L] [Algebra K E] [Algebra L E]
    (n : ℕ) [NeZero n]
    [IsCyclotomicExtension {n} F L] [IsCyclotomicExtension {n} K E] :
    Algebra.adjoin L (Set.range (algebraMap K E)) = ⊤
theorem

finrank_eq_of_coprime_of_adjoin_eq_top

L48 ↗
ValuationTheory.DiscreteValuationField.finrank_eq_of_coprime_of_adjoin_eq_top
Source context 1 command

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

namespace ValuationTheory.DiscreteValuationField
Lean source · statement
theorem finrank_eq_of_coprime_of_adjoin_eq_top
    (F L E : Type*) [Field F] [Field L] [Field E]
    [Algebra F L] [Algebra F E] [Algebra L E] [IsScalarTower F L E]
    [Algebra.IsAlgebraic F L] (A : IntermediateField F E)
    (hcop : (Module.finrank F A).Coprime (Module.finrank F L))
    (hgen : Algebra.adjoin L (A : Set E) = ⊤) :
    Module.finrank L E = Module.finrank F A
theorem

cyclotomic_compositum_finrank_eq_prime

L69 ↗
ValuationTheory.DiscreteValuationField.cyclotomic_compositum_finrank_eq_prime
Documentation

Adjoining the same prime-order roots of unity to a prime-degree extension preserves its degree. Generation and coprimality are supplied by the actual cyclotomic extensions.

Source context 1 command

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

namespace ValuationTheory.DiscreteValuationField
Lean source · statement
theorem cyclotomic_compositum_finrank_eq_prime
    (F K L E : Type*) [Field F] [Field K] [Field L] [Field E]
    [Algebra F K] [Algebra F L] [Algebra F E] [Algebra K E] [Algebra L E]
    [IsScalarTower F K E] [IsScalarTower F L E]
    (p : ℕ) [Fact p.Prime]
    [IsCyclotomicExtension {p} F L] [IsCyclotomicExtension {p} K E]
    (hdegree : Module.finrank F K = p) : Module.finrank L E = p

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