Cyclotomic integers

This file defines cyclotomic integers using AdjoinRoot and relates them to the ring of integers of the corresponding rational cyclotomic field.

theorem instIsCyclotomicExtensionSingletonNatSetRatCyclotomicField_leanPool (p : ℕ) [hpri : Fact (Nat.Prime p)] : IsCyclotomicExtension {p} ℚ (CyclotomicField p ℚ)

def CyclotomicIntegers (p : ℕ) : Type

The cyclotomic integers of conductor p, defined as an AdjoinRoot.

Equations

• CyclotomicIntegers p = AdjoinRoot (Polynomial.cyclotomic p ℤ)

@[instance_reducible]

noncomputable instance instCommRingCyclotomicIntegers (p : ℕ) : CommRing (CyclotomicIntegers p)

Equations

• instCommRingCyclotomicIntegers p = id inferInstance

theorem IsPrimitiveRoot.cyclotomic_eq_minpoly (p : ℕ) [hpri : Fact (Nat.Prime p)] (x : NumberField.RingOfIntegers (CyclotomicField p ℚ)) (hx : IsPrimitiveRoot (↑x) p) : minpoly ℤ x = Polynomial.cyclotomic p ℤ

noncomputable def CyclotomicIntegers.equiv (p : ℕ) [hpri : Fact (Nat.Prime p)] : CyclotomicIntegers p ≃+* NumberField.RingOfIntegers (CyclotomicField p ℚ)

The canonical equivalence between CyclotomicIntegers p and the ring of integers of the p-th cyclotomic field.

Equations

• CyclotomicIntegers.equiv p = (AdjoinRoot.equiv' (Polynomial.cyclotomic p ℤ) ⋯.integralPowerBasis ⋯ ⋯).toRingEquiv

theorem CyclotomicIntegers.equiv_symm_apply (p : ℕ) [hpri : Fact (Nat.Prime p)] (a : NumberField.RingOfIntegers (CyclotomicField p ℚ)) : (equiv p).symm a = (⋯.integralPowerBasis.lift (AdjoinRoot.root (Polynomial.cyclotomic p ℤ)) ⋯) a

theorem CyclotomicIntegers.equiv_apply (p : ℕ) [hpri : Fact (Nat.Prime p)] (a : AdjoinRoot (Polynomial.cyclotomic p ℤ)) : (equiv p) a = (AdjoinRoot.liftAlgHom (Polynomial.cyclotomic p ℤ) (Algebra.ofId ℤ (NumberField.RingOfIntegers (CyclotomicField p ℚ))) ⋯.toInteger ⋯) a

instance CyclotomicIntegers.instIsDomain (p : ℕ) [hpri : Fact (Nat.Prime p)] : IsDomain (CyclotomicIntegers p)

noncomputable def CyclotomicIntegers.zeta (p : ℕ) : CyclotomicIntegers p

The tautological primitive root of unity in CyclotomicIntegers p.

Equations

• CyclotomicIntegers.zeta p = AdjoinRoot.root (Polynomial.cyclotomic p ℤ)

theorem CyclotomicIntegers.equiv_zeta (p : ℕ) [hpri : Fact (Nat.Prime p)] : (equiv p) (zeta p) = ⋯.toInteger

theorem CyclotomicIntegers.prime_one_sub_zeta (p : ℕ) [hpri : Fact (Nat.Prime p)] : Prime (1 - zeta p)

theorem CyclotomicIntegers.one_sub_zeta_mem_nonZeroDivisors (p : ℕ) [hpri : Fact (Nat.Prime p)] : 1 - zeta p ∈ nonZeroDivisors (CyclotomicIntegers p)

theorem CyclotomicIntegers.not_isUnit_one_sub_zeta (p : ℕ) [hpri : Fact (Nat.Prime p)] : ¬IsUnit (1 - zeta p)

theorem CyclotomicIntegers.one_sub_zeta_dvd_int_iff (p : ℕ) [hpri : Fact (Nat.Prime p)] (n : ℤ) : 1 - zeta p ∣ ↑n ↔ ↑p ∣ n

theorem CyclotomicIntegers.one_sub_zeta_dvd (p : ℕ) [hpri : Fact (Nat.Prime p)] : 1 - zeta p ∣ ↑p

theorem CyclotomicIntegers.isCoprime_one_sub_zeta (p : ℕ) [hpri : Fact (Nat.Prime p)] (n : ℤ) (hn : ¬↑p ∣ n) : IsCoprime (1 - zeta p) ↑n

theorem CyclotomicIntegers.exists_dvd_int (p : ℕ) [hpri : Fact (Nat.Prime p)] (n : CyclotomicIntegers p) (hn : n ≠ 0) : ∃ (m : ℤ), m ≠ 0 ∧ n ∣ ↑m

noncomputable def CyclotomicIntegers.powerBasis (p : ℕ) : PowerBasis ℤ (CyclotomicIntegers p)

The power basis of CyclotomicIntegers p generated by zeta p.

Equations

• CyclotomicIntegers.powerBasis p = AdjoinRoot.powerBasis' ⋯

theorem CyclotomicIntegers.powerBasis_dim (p : ℕ) [hpri : Fact (Nat.Prime p)] : (powerBasis p).dim = p - 1

instance CyclotomicIntegers.instFreeInt (p : ℕ) : Module.Free ℤ (CyclotomicIntegers p)

theorem CyclotomicIntegers.nontrivial {p : ℕ} (hp : p ≠ 0) : Nontrivial (CyclotomicIntegers p)

theorem CyclotomicIntegers.charZero {p : ℕ} (hp : p ≠ 0) : CharZero (CyclotomicIntegers p)

instance CyclotomicIntegers.instCharZero (p : ℕ) [hpri : Fact (Nat.Prime p)] : CharZero (CyclotomicIntegers p)