Subfields of cyclotomic fields

TheoremUnique subfield of each degree in the \(p\)-th cyclotomic field#✓fully proved

Let \(p\) be a prime and let \(s\) be a natural number dividing \(p - 1\). Then the \(p\)-th cyclotomic field \(\mathbb{Q}(\zeta_p)\) has exactly one intermediate field \(K\) over \(\mathbb{Q}\) with \([K : \mathbb{Q}] = s\).

theorem existsUnique_intermediateField_finrank (p s : ℕ) (hp : p.Prime)
    (hs : s ∣ p - 1) :
    ∃! K : IntermediateField ℚ (CyclotomicField p ℚ), Module.finrank ℚ K = s

Used by 2

Used byCharacterization of the degree-\(s\) subfield of the \(p\)-th cyclotomic field · The degree-\(s\) subfield of the \(p\)-th cyclotomic field

DefinitionThe degree-\(s\) subfield of the \(p\)-th cyclotomic field#✓fully proved

For a prime \(p\) and a natural number \(s\) dividing \(p - 1\), this is the unique intermediate field \(K\) of the \(p\)-th cyclotomic field \(\mathbb{Q}(\zeta_p)\) over \(\mathbb{Q}\) with \([K : \mathbb{Q}] = s\).

noncomputable def intermediateFieldOfFinrank (p s : ℕ) (hp : p.Prime) (hs : s ∣ p - 1) :
    IntermediateField ℚ (CyclotomicField p ℚ) :=
  (existsUnique_intermediateField_finrank p s hp hs).choose

Uses 1 · Used by 1

Statement usesUnique subfield of each degree in the \(p\)-th cyclotomic field

Used byCharacterization of the degree-\(s\) subfield of the \(p\)-th cyclotomic field

TheoremCharacterization of the degree-\(s\) subfield of the \(p\)-th cyclotomic field#✓fully proved

Let \(p\) be a prime, let \(s\) be a natural number dividing \(p - 1\), and let \(K\) be an intermediate field of the \(p\)-th cyclotomic field \(\mathbb{Q}(\zeta_p)\) over \(\mathbb{Q}\). Then \(K\) is the degree-\(s\) subfield of \(\mathbb{Q}(\zeta_p)\) if and only if \([K : \mathbb{Q}] = s\).

theorem eq_intermediateFieldOfFinrank_iff (p s : ℕ) (hp : p.Prime) (hs : s ∣ p - 1)
    (K : IntermediateField ℚ (CyclotomicField p ℚ)) :
    K = intermediateFieldOfFinrank p s hp hs ↔ Module.finrank ℚ K = s

Uses 2

Statement usesThe degree-\(s\) subfield of the \(p\)-th cyclotomic field

Proof usesUnique subfield of each degree in the \(p\)-th cyclotomic field

TheoremTwo cyclotomic subfields whose levels have lcm \(m\) generate the \(m\)-th cyclotomic field#✓fully proved

Let \(n_0\), \(n_1\) and \(m\) be natural numbers with \(n_0, n_1 \neq 0\) and \(\operatorname{lcm}(n_0, n_1) = m\). Let \(E_0\) and \(E_1\) be intermediate fields of the \(m\)-th cyclotomic field \(\mathbb{Q}(\zeta_m)\) over \(\mathbb{Q}\) such that \(E_0\) is generated over \(\mathbb{Q}\) by a primitive \(n_0\)-th root of unity and \(E_1\) by a primitive \(n_1\)-th root of unity. Then the compositum of \(E_0\) and \(E_1\) is all of \(\mathbb{Q}(\zeta_m)\).

theorem sup_eq_top_of_lcm_eq (n₀ n₁ m : ℕ) [NeZero n₀] [NeZero n₁]
    (E₀ E₁ : IntermediateField ℚ (CyclotomicField m ℚ))
    [IsCyclotomicExtension {n₀} ℚ E₀] [IsCyclotomicExtension {n₁} ℚ E₁]
    (hlcm : Nat.lcm n₀ n₁ = m) : E₀ ⊔ E₁ = ⊤

Used by 1

Used byA field strictly above one cyclotomic subfield meets the other

TheoremA field strictly above one cyclotomic subfield meets the other#✓fully proved

Let \(n_0\), \(n_1\) and \(m\) be natural numbers with \(n_0, n_1 \neq 0\) and \(\operatorname{lcm}(n_0, n_1) = m\). Let \(E_0\) and \(E_1\) be intermediate fields of the \(m\)-th cyclotomic field \(\mathbb{Q}(\zeta_m)\) over \(\mathbb{Q}\) such that \(E_0\) is generated over \(\mathbb{Q}\) by a primitive \(n_0\)-th root of unity and \(E_1\) by a primitive \(n_1\)-th root of unity. If \(F\) is an intermediate field of \(\mathbb{Q}(\zeta_m)\) with \(E_0 \subsetneq F\), then \(F \cap E_1 \neq \mathbb{Q}\).

theorem inf_ne_bot_of_lt_of_lcm_eq (n₀ n₁ m : ℕ) [NeZero n₀] [NeZero n₁]
    (E₀ E₁ : IntermediateField ℚ (CyclotomicField m ℚ))
    [IsCyclotomicExtension {n₀} ℚ E₀] [IsCyclotomicExtension {n₁} ℚ E₁]
    (F : IntermediateField ℚ (CyclotomicField m ℚ))
    (hlcm : Nat.lcm n₀ n₁ = m) (hE₀F : E₀ < F) : F ⊓ E₁ ≠ ⊥

Uses 2

Proof usesTwo cyclotomic subfields whose levels have lcm \(m\) generate the \(m\)-th cyclotomic field · Intermediate fields of an abelian extension form a modular lattice

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.