flt5_beta_coprime_conj_pid

Disproved

by tianyipeng · May 13, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

algebragraph-theorynumber-theoryproved

Given a, b, s : Z with gcd(a,b)=1, beta : ZZ5 = RingOfIntegers(CyclotomicField 5 Q) with Algebra.norm Z beta = s^5, and hPID : ZZ5 is a PID, for each Galois automorphism sigma : CK5 <~a[Q] CK5 with sigma != AlgEquiv.refl, IsCoprime beta ((RingOfIntegers.mapAlgEquiv sigma) beta) in ZZ5. Strategy: beta - sigma(beta) = b*(zeta - sigma(zeta)) = b * unit * lambda (since (1-zeta^k) is unitlambda for k not 0 mod 5, proved via N(1-zeta^k)=N(lambda)=5). Any common divisor d | beta and sigma(beta) in ZZ5 divides beta - sigma(beta) = unitlambda*b. If d|lambda then since lambda is the unique prime above 5, N(beta)=s^5 and gcd(a,b)=1 prevent both beta and sigma(beta) being divisible by lambda. If d|b then d|N(beta)=s^5 and combined gcd conditions show d is a unit.

Preamble

import Mathlib.NumberTheory.NumberField.Cyclotomic.PID
import Mathlib.NumberTheory.Cyclotomic.Basic
import Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
import Mathlib.RingTheory.PrincipalIdealDomain
import Mathlib.NumberTheory.NumberField.Basic
import Mathlib.Data.Int.Basic
import Mathlib.Data.Int.GCD

Formal statement

theorem flt5_beta_coprime_conj_pid (a b s : ℤ) (h_cop : Int.gcd a b = 1) (β : NumberField.RingOfIntegers (CyclotomicField 5 ℚ)) (hβ : Algebra.norm ℤ β = s ^ 5) (hPID : IsPrincipalIdealRing (NumberField.RingOfIntegers (CyclotomicField 5 ℚ))) : ∀ σ : (CyclotomicField 5 ℚ) ≃ₐ[ℚ] (CyclotomicField 5 ℚ), σ ≠ AlgEquiv.refl → IsCoprime β (NumberField.RingOfIntegers.mapAlgEquiv σ β) := by sorry

View graph