Documentation

Mathlib.NumberTheory.Cyclotomic.Basic

Cyclotomic extensions #

Let A and B be commutative rings with Algebra A B. For S : Set ℕ+, we define a class IsCyclotomicExtension S A B expressing the fact that B is obtained from A by adding n-th primitive roots of unity, for all n ∈ S.

Main definitions #

Main results #

Implementation details #

Our definition of IsCyclotomicExtension is very general, to allow rings of any characteristic and infinite extensions, but it will mainly be used in the case S = {n} and for integral domains. All results are in the IsCyclotomicExtension namespace. Note that some results, for example IsCyclotomicExtension.trans, IsCyclotomicExtension.finite, IsCyclotomicExtension.numberField, IsCyclotomicExtension.finiteDimensional, IsCyclotomicExtension.isGalois and CyclotomicField.algebraBase are lemmas, but they can be made local instances. Some of them are included in the Cyclotomic locale.

theorem isCyclotomicExtension_iff (S : Set ℕ+) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] :
IsCyclotomicExtension S A B (∀ {n : ℕ+}, n S∃ (r : B), IsPrimitiveRoot r n) ∀ (x : B), x Algebra.adjoin A {b : B | nS, b ^ n = 1}
class IsCyclotomicExtension (S : Set ℕ+) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] :

Given an A-algebra B and S : Set ℕ+, we define IsCyclotomicExtension S A B requiring that there is an n-th primitive root of unity in B for all n ∈ S and that B is generated over A by the roots of X ^ n - 1.

  • exists_prim_root : ∀ {n : ℕ+}, n S∃ (r : B), IsPrimitiveRoot r n

    For all n ∈ S, there exists a primitive n-th root of unity in B.

  • adjoin_roots : ∀ (x : B), x Algebra.adjoin A {b : B | nS, b ^ n = 1}

    The n-th roots of unity, for n ∈ S, generate B as an A-algebra.

Instances
    theorem IsCyclotomicExtension.exists_prim_root {S : Set ℕ+} (A : Type u) {B : Type v} :
    ∀ {inst : CommRing A} {inst_1 : CommRing B} {inst_2 : Algebra A B} [self : IsCyclotomicExtension S A B] {n : ℕ+}, n S∃ (r : B), IsPrimitiveRoot r n

    For all n ∈ S, there exists a primitive n-th root of unity in B.

    theorem IsCyclotomicExtension.adjoin_roots {S : Set ℕ+} {A : Type u} {B : Type v} :
    ∀ {inst : CommRing A} {inst_1 : CommRing B} {inst_2 : Algebra A B} [self : IsCyclotomicExtension S A B] (x : B), x Algebra.adjoin A {b : B | nS, b ^ n = 1}

    The n-th roots of unity, for n ∈ S, generate B as an A-algebra.

    theorem IsCyclotomicExtension.iff_adjoin_eq_top (S : Set ℕ+) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] :
    IsCyclotomicExtension S A B (∀ nS, ∃ (r : B), IsPrimitiveRoot r n) Algebra.adjoin A {b : B | nS, b ^ n = 1} =

    A reformulation of IsCyclotomicExtension that uses .

    theorem IsCyclotomicExtension.iff_singleton (n : ℕ+) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] :
    IsCyclotomicExtension {n} A B (∃ (r : B), IsPrimitiveRoot r n) ∀ (x : B), x Algebra.adjoin A {b : B | b ^ n = 1}

    A reformulation of IsCyclotomicExtension in the case S is a singleton.

    If IsCyclotomicExtension ∅ A B, then the image of A in B equals B.

    If IsCyclotomicExtension {1} A B, then the image of A in B equals B.

    If (⊥ : SubAlgebra A B) = ⊤, then IsCyclotomicExtension ∅ A B.

    theorem IsCyclotomicExtension.trans (S : Set ℕ+) (T : Set ℕ+) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] (C : Type w) [CommRing C] [Algebra A C] [Algebra B C] [IsScalarTower A B C] [hS : IsCyclotomicExtension S A B] [hT : IsCyclotomicExtension T B C] (h : Function.Injective (algebraMap B C)) :

    Transitivity of cyclotomic extensions.

    theorem IsCyclotomicExtension.union_right (S : Set ℕ+) (T : Set ℕ+) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [h : IsCyclotomicExtension (S T) A B] :
    IsCyclotomicExtension T (↥(Algebra.adjoin A {b : B | aS, b ^ a = 1})) B

    If B is a cyclotomic extension of A given by roots of unity of order in S ∪ T, then B is a cyclotomic extension of adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 } given by roots of unity of order in T.

    theorem IsCyclotomicExtension.union_left (S : Set ℕ+) (T : Set ℕ+) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [h : IsCyclotomicExtension T A B] (hS : S T) :
    IsCyclotomicExtension S A (Algebra.adjoin A {b : B | aS, b ^ a = 1})

    If B is a cyclotomic extension of A given by roots of unity of order in T and S ⊆ T, then adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 } is a cyclotomic extension of B given by roots of unity of order in S.

    theorem IsCyclotomicExtension.of_union_of_dvd {n : ℕ+} {S : Set ℕ+} (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] (h : sS, n s) (hS : S.Nonempty) [H : IsCyclotomicExtension S A B] :

    If ∀ s ∈ S, n ∣ s and S is not empty, then IsCyclotomicExtension S A B implies IsCyclotomicExtension (S ∪ {n}) A B.

    theorem IsCyclotomicExtension.iff_union_of_dvd {n : ℕ+} {S : Set ℕ+} (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] (h : sS, n s) (hS : S.Nonempty) :

    If ∀ s ∈ S, n ∣ s and S is not empty, then IsCyclotomicExtension S A B if and only if IsCyclotomicExtension (S ∪ {n}) A B.

    If (⊥ : SubAlgebra A B) = ⊤, then IsCyclotomicExtension {1} A B.

    theorem IsCyclotomicExtension.equiv (S : Set ℕ+) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] {C : Type u_1} [CommRing C] [Algebra A C] [h : IsCyclotomicExtension S A B] (f : B ≃ₐ[A] C) :

    Given (f : B ≃ₐ[A] C), if IsCyclotomicExtension S A B then IsCyclotomicExtension S A C.

    theorem IsCyclotomicExtension.neZero (n : ℕ+) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [h : IsCyclotomicExtension {n} A B] [IsDomain B] :
    NeZero n
    theorem IsCyclotomicExtension.neZero' (n : ℕ+) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [IsDomain B] :
    NeZero n
    theorem IsCyclotomicExtension.finite (S : Set ℕ+) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] [h₁ : Finite S] [h₂ : IsCyclotomicExtension S A B] :

    If S is finite and IsCyclotomicExtension S A B, then B is a finite A-algebra.

    theorem IsCyclotomicExtension.numberField (S : Set ℕ+) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [h : NumberField K] [Finite S] [IsCyclotomicExtension S K L] :

    A cyclotomic finite extension of a number field is a number field.

    A finite cyclotomic extension of an integral noetherian domain is integral

    If S is finite and IsCyclotomicExtension S K A, then finiteDimensional K A.

    theorem IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] {ζ : B} {n : ℕ+} (hζ : IsPrimitiveRoot ζ n) :
    Algebra.adjoin A ((Polynomial.cyclotomic (↑n) A).rootSet B) = Algebra.adjoin A {b : B | a{n}, b ^ a = 1}
    theorem IsCyclotomicExtension.adjoin_primitive_root_eq_top {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] {n : ℕ+} [IsDomain B] [h : IsCyclotomicExtension {n} A B] {ζ : B} (hζ : IsPrimitiveRoot ζ n) :
    theorem IsPrimitiveRoot.adjoin_isCyclotomicExtension (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Algebra A B] {ζ : B} {n : ℕ+} (h : IsPrimitiveRoot ζ n) :
    theorem IsCyclotomicExtension.splits_X_pow_sub_one {n : ℕ+} {S : Set ℕ+} (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [H : IsCyclotomicExtension S K L] (hS : n S) :
    Polynomial.Splits (algebraMap K L) (Polynomial.X ^ n - 1)

    A cyclotomic extension splits X ^ n - 1 if n ∈ S.

    theorem IsCyclotomicExtension.splits_cyclotomic {n : ℕ+} {S : Set ℕ+} (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] (hS : n S) :

    A cyclotomic extension splits cyclotomic n K if n ∈ S.

    theorem IsCyclotomicExtension.isSplittingField_X_pow_sub_one (n : ℕ+) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] :
    Polynomial.IsSplittingField K L (Polynomial.X ^ n - 1)

    If IsCyclotomicExtension {n} K L, then L is the splitting field of X ^ n - 1.

    def IsCyclotomicExtension.algEquiv (n : ℕ+) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] (L' : Type u_1) [Field L'] [Algebra K L'] [IsCyclotomicExtension {n} K L'] :
    L ≃ₐ[K] L'

    Any two n-th cyclotomic extensions are isomorphic.

    Equations
    Instances For
      theorem IsCyclotomicExtension.isGalois (n : ℕ+) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] :

      If IsCyclotomicExtension {n} K L, then L is the splitting field of cyclotomic n K.

      def CyclotomicField (n : ℕ+) (K : Type w) [Field K] :

      Given n : ℕ+ and a field K, we define CyclotomicField n K as the splitting field of cyclotomic n K. If n is nonzero in K, it has the instance IsCyclotomicExtension {n} K (CyclotomicField n K).

      Equations
      Instances For
        instance CyclotomicField.instField (n : ℕ+) (K : Type w) [Field K] :
        Equations
        instance CyclotomicField.algebra (n : ℕ+) (K : Type w) [Field K] :
        Equations
        Equations
        • =
        Equations
        • =
        instance CyclotomicField.algebraBase (n : ℕ+) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] :

        If K is the fraction field of A, the A-algebra structure on CyclotomicField n K.

        Equations
        instance instIsScalarTowerCyclotomicField (n : ℕ+) (K : Type w) [Field K] {R : Type u_1} [CommRing R] [Algebra R K] :
        Equations
        • =
        Equations
        • =
        def CyclotomicRing (n : ℕ+) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] :

        If A is a domain with fraction field K and n : ℕ+, we define CyclotomicRing n A K as the A-subalgebra of CyclotomicField n K generated by the roots of X ^ n - 1. If n is nonzero in A, it has the instance IsCyclotomicExtension {n} A (CyclotomicRing n A K).

        Equations
        Instances For
          instance CyclotomicRing.instCommRing (n : ℕ+) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] :
          Equations
          instance CyclotomicRing.instIsDomain (n : ℕ+) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] :
          Equations
          • =
          instance CyclotomicRing.instInhabited (n : ℕ+) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] :
          Equations
          instance CyclotomicRing.algebraBase (n : ℕ+) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] :

          The A-algebra structure on CyclotomicRing n A K.

          Equations
          Equations
          • =
          instance CyclotomicRing.isCyclotomicExtension (n : ℕ+) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [NeZero n] :
          Equations
          • =
          theorem CyclotomicRing.eq_adjoin_primitive_root (n : ℕ+) (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] {μ : CyclotomicField n K} (h : IsPrimitiveRoot μ n) :
          CyclotomicRing n A K = (Algebra.adjoin A {μ})
          theorem IsAlgClosed.isCyclotomicExtension (S : Set ℕ+) (K : Type w) [Field K] [IsAlgClosed K] (h : aS, NeZero a) :

          Algebraically closed fields are S-cyclotomic extensions over themselves if NeZero ((a : ℕ) : K)) for all a ∈ S.