A compatible prime and reduction for the cyclotomic opening

For p ∤ n, a prescribed primitive n-th root in an algebraic closure of ZMod p determines a homomorphism from the ring of integers of ℚ(ζₙ). Its kernel is a prime above (p), and the induced quotient map sends all powers of the characteristic-zero generator to the corresponding powers of the prescribed finite-characteristic root.

@[reducible, inline]

abbrev BGS.Markoff.OpeningCyclotomicField (n : ℕ) : Type

The canonical cyclotomic number field used for a common order n.

Equations

• BGS.Markoff.OpeningCyclotomicField n = CyclotomicField n ℚ

@[reducible, inline]

abbrev BGS.Markoff.OpeningCyclotomicIntegers (n : ℕ) : Type

The ring of integers of the canonical cyclotomic number field.

Equations

• BGS.Markoff.OpeningCyclotomicIntegers n = NumberField.RingOfIntegers (BGS.Markoff.OpeningCyclotomicField n)

@[reducible, inline]

abbrev BGS.Markoff.OpeningResidueClosure (p : ℕ) [Fact (Nat.Prime p)] : Type

The algebraic closure in which the prescribed characteristic-p roots live.

Equations

• BGS.Markoff.OpeningResidueClosure p = AlgebraicClosure (ZMod p)

theorem BGS.Markoff.residueClosure_natCast_ne_zero_of_coprime (p n : ℕ) [Fact (Nat.Prime p)] (hcoprime : p.Coprime n) : ↑n ≠ 0

Coprimality with the characteristic makes n nonzero in the chosen residue closure.

theorem BGS.Markoff.exists_residue_common_primitiveRoot_powers (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (w₁ w₂ w₃ : OpeningResidueClosure p) (hw₁ : w₁ ^ n = 1) (hw₂ : w₂ ^ n = 1) (hw₃ : w₃ ^ n = 1) : ∃ (ω : OpeningResidueClosure p) (a₁ : ℕ) (a₂ : ℕ) (a₃ : ℕ), IsPrimitiveRoot ω n ∧ a₁ < n ∧ a₂ < n ∧ a₃ < n ∧ ω ^ a₁ = w₁ ∧ ω ^ a₂ = w₂ ∧ ω ^ a₃ = w₃

Three n-th roots in the residue closure are powers of one primitive n-th root. The coprimality hypothesis supplies the nonvanishing of n that was previously obtained from characteristic zero.

noncomputable def BGS.Markoff.openingCyclotomicRoot (n : ℕ) [NeZero n] : OpeningCyclotomicField n

The canonical primitive n-th root in the chosen characteristic-zero cyclotomic field.

Equations

• BGS.Markoff.openingCyclotomicRoot n = IsCyclotomicExtension.zeta n ℚ (BGS.Markoff.OpeningCyclotomicField n)

theorem BGS.Markoff.openingCyclotomicRoot_isPrimitive (n : ℕ) [NeZero n] : IsPrimitiveRoot (openingCyclotomicRoot n) n

The canonical characteristic-zero root has exact order n.

noncomputable def BGS.Markoff.openingCyclotomicIntegerRoot (n : ℕ) [NeZero n] : OpeningCyclotomicIntegers n

The canonical cyclotomic root, regarded as an algebraic integer.

Equations

• BGS.Markoff.openingCyclotomicIntegerRoot n = ⋯.toInteger

noncomputable def BGS.Markoff.openingCyclotomicIntegralPowerBasis (n : ℕ) [NeZero n] : PowerBasis ℤ (OpeningCyclotomicIntegers n)

The integral power basis generated by the canonical cyclotomic root.

Equations

• BGS.Markoff.openingCyclotomicIntegralPowerBasis n = ⋯.integralPowerBasis

@[simp]

theorem BGS.Markoff.openingCyclotomicIntegralPowerBasis_gen (n : ℕ) [NeZero n] : (openingCyclotomicIntegralPowerBasis n).gen = openingCyclotomicIntegerRoot n

noncomputable def BGS.Markoff.openingCyclotomicReduction (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) : OpeningCyclotomicIntegers n →ₐ[ℤ] OpeningResidueClosure p

The compatible reduction homomorphism determined by the prescribed primitive root ω.

Equations

• BGS.Markoff.openingCyclotomicReduction p n hcoprime ω hω = (BGS.Markoff.openingCyclotomicIntegralPowerBasis n).lift ω ⋯

@[simp]

theorem BGS.Markoff.openingCyclotomicReduction_integerRoot (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) : (openingCyclotomicReduction p n hcoprime ω hω) (openingCyclotomicIntegerRoot n) = ω

The compatible reduction sends the characteristic-zero generator to the prescribed root.

noncomputable def BGS.Markoff.openingCyclotomicPrime (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) : Ideal (OpeningCyclotomicIntegers n)

The prime ideal of the cyclotomic integers selected by the prescribed residue root.

Equations

• BGS.Markoff.openingCyclotomicPrime p n hcoprime ω hω = RingHom.ker (BGS.Markoff.openingCyclotomicReduction p n hcoprime ω hω).toRingHom

theorem BGS.Markoff.openingCyclotomicPrime_isPrime (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) : (openingCyclotomicPrime p n hcoprime ω hω).IsPrime

The selected kernel is prime because the residue closure is a field.

theorem BGS.Markoff.openingCyclotomicPrime_under (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) : Ideal.under ℤ (openingCyclotomicPrime p n hcoprime ω hω) = Ideal.span {↑p}

The selected prime lies above the rational prime (p).

noncomputable def BGS.Markoff.openingCyclotomicQuotientReduction (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) : OpeningCyclotomicIntegers n ⧸ openingCyclotomicPrime p n hcoprime ω hω →+* OpeningResidueClosure p

The quotient by the compatible prime embeds in the chosen residue closure.

Equations

• BGS.Markoff.openingCyclotomicQuotientReduction p n hcoprime ω hω = (BGS.Markoff.openingCyclotomicReduction p n hcoprime ω hω).kerLift

theorem BGS.Markoff.openingCyclotomicQuotientReduction_injective (p n : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) : Function.Injective ⇑(openingCyclotomicQuotientReduction p n hcoprime ω hω)

The quotient reduction is injective: its source is exactly the quotient by the kernel.

theorem BGS.Markoff.openingCyclotomicQuotientReduction_integerRoot_pow (p n a : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) : (openingCyclotomicQuotientReduction p n hcoprime ω hω) ((Ideal.Quotient.mk (openingCyclotomicPrime p n hcoprime ω hω)) (openingCyclotomicIntegerRoot n ^ a)) = ω ^ a

The quotient reduction sends every power of the integral generator to the matching power of the prescribed residue root.

theorem BGS.Markoff.openingCyclotomicQuotientReduction_three_powers (p n a₁ a₂ a₃ : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) : have reduce := openingCyclotomicQuotientReduction p n hcoprime ω hω; have quotient := Ideal.Quotient.mk (openingCyclotomicPrime p n hcoprime ω hω); reduce (quotient (openingCyclotomicIntegerRoot n ^ a₁)) = ω ^ a₁ ∧ reduce (quotient (openingCyclotomicIntegerRoot n ^ a₂)) = ω ^ a₂ ∧ reduce (quotient (openingCyclotomicIntegerRoot n ^ a₃)) = ω ^ a₃

One chosen prime therefore realizes three prescribed powers simultaneously.