How to prove 1/2 is not integral over Z ?

Stream: maths

[Qingfeng Li]

How to prove that:

import Mathlib

example : ¬ IsIntegral ℤ (1 / 2 : ℚ) := by
  sorry

In math we try to show the minpoly is 2x-1 which is not monic, but in mathlib it's illegal because the definition of minpoly is monic.

[Riccardo Brasca]

We know that ℤ is integrally closed, so this should be easy.

[Riccardo Brasca]

Something like

import Mathlib

example : ¬ IsIntegral ℤ (1 / 2 : ℚ) := by
  intro h
  obtain ⟨x, hx⟩ := ((isIntegrallyClosed_iff_isIntegrallyClosedIn ℚ).1 inferInstance).isIntegral_iff.1 h
  apply_fun (· * 2) at hx
  replace hx : (x : ℚ) * ((2 : ℤ) : ℚ) = 1 := by
    simpa using hx
  norm_cast at hx
  rcases Int.mul_eq_one_iff_eq_one_or_neg_one.1 hx with ⟨_, h⟩ | ⟨_, h⟩ <;>
  norm_num at h

[Riccardo Brasca]

Note that most of the proof is to show that 1/2 is not an integer.

[Ruben Van de Velde]

Shorter (*):

import Mathlib


section NormNum -- #26428
open Mathlib.Meta.NormNum Qq Int

variable {α : Type*} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α]
variable {R : Type*} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R]
theorem isNat_intFract_of_isNat (r : R) (m : ℕ) : IsNat r m → IsNat (Int.fract r) 0 := by
  rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

theorem isNat_intFract_of_isInt (r : R) (m : ℤ) : IsInt r m → IsNat (Int.fract r) 0 := by
  rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

theorem isNNRat_intFract_of_isNNRat (r : α) (n d : ℕ) :
    IsNNRat r n d → IsNNRat (Int.fract r) (n % d) d := by
  rintro ⟨inv, rfl⟩
  refine ⟨inv, ?_⟩
  simp only [invOf_eq_inv, ← div_eq_mul_inv, fract_div_natCast_eq_div_natCast_mod]

theorem isRat_intFract_of_isRat_negOfNat (r : α) (n d : ℕ) :
    IsRat r (negOfNat n) d → IsRat (Int.fract r) (-n % d) d := by
  rintro ⟨inv, rfl⟩
  refine ⟨inv, ?_⟩
  simp only [invOf_eq_inv, ← div_eq_mul_inv, fract_div_intCast_eq_div_intCast_mod,
    negOfNat_eq, ofNat_eq_coe]

/-- `norm_num` extension for `Int.fract` -/
@[norm_num (Int.fract _)]
def evalIntFract : NormNumExt where eval {u α} e := do
  match e with
  | ~q(@Int.fract _ $instR $instO $instF $x) =>
    match ← derive x with
    | .isBool .. => failure
    | .isNat _ _ pb => do
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      have z : Q(ℕ) := Lean.mkRawNatLit 0
      letI : $z =Q 0 := ⟨⟩
      return .isNat _ z q(isNat_intFract_of_isNat $x _ $pb)
    | .isNegNat _ _ pb => do
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      have z : Q(ℕ) := Lean.mkRawNatLit 0
      letI : $z =Q 0 := ⟨⟩
      return .isNat _ z q(isNat_intFract_of_isInt _ _ $pb)
    | .isNNRat _ q n d h => do
      let _i ← synthInstanceQ q(Field $α)
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      have n' : Q(ℕ) := Lean.mkRawNatLit (q.num.natAbs % q.den)
      letI : $n' =Q $n % $d := ⟨⟩
      return .isNNRat _ (Int.fract q) n' d q(isNNRat_intFract_of_isNNRat _ $n $d $h)
    | .isNegNNRat _ q n d h => do
      let _i ← synthInstanceQ q(Field $α)
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      have n' : Q(ℤ) := mkRawIntLit (q.num % q.den)
      letI : $n' =Q -$n % $d := ⟨⟩
      return .isRat _ (Int.fract q) n' d q(isRat_intFract_of_isRat_negOfNat _ $n $d $h)
  | _, _, _ => failure

example : Int.fract (3.7 : ℚ) = 0.7 := by norm_num
example : Int.fract (-3.7 : ℚ) = 0.3 := by norm_num

end NormNum

example : ¬ IsIntegral ℤ (1 / 2 : ℚ) := by
  intro h
  obtain ⟨x, hx⟩ := ((isIntegrallyClosed_iff_isIntegrallyClosedIn ℚ).1 inferInstance).isIntegral_iff.1 h
  apply_fun Int.fract at hx
  norm_num at hx

[Qingfeng Li]

Thanks, I leant a lot. Actrually I'm tring to prove some element is not integral, such as (√5 + 1) / 4 and find it hard to analyse the minpoly.
Is it easy to prove

import Mathlib
open Polynomial
example : ¬ IsIntegral ℤ ((√5 + 1) / 4 : ℝ) := by
  let f : ℤ[X] := C 4 * X ^ 2 - C 2 * X - C 1
  have f_root : f.aeval ((√5 + 1) / 4 : ℝ) = 0 := by sorry
  sorry

by just judge that f is not monic? Or it need some works?

[Riccardo Brasca]

I think your problem is mathematical, not really Lean related. Can you write down a very precise proof (with pen and paper)? You find a non-monic poly that has the element as root, and then what?

[Riccardo Brasca]

Ruben Van de Velde said:

Shorter (*):

import Mathlib


section NormNum -- #26428
open Mathlib.Meta.NormNum Qq Int

variable {α : Type*} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α]
variable {R : Type*} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R]
theorem isNat_intFract_of_isNat (r : R) (m : ℕ) : IsNat r m → IsNat (Int.fract r) 0 := by
  rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

theorem isNat_intFract_of_isInt (r : R) (m : ℤ) : IsInt r m → IsNat (Int.fract r) 0 := by
  rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

theorem isNNRat_intFract_of_isNNRat (r : α) (n d : ℕ) :
    IsNNRat r n d → IsNNRat (Int.fract r) (n % d) d := by
  rintro ⟨inv, rfl⟩
  refine ⟨inv, ?_⟩
  simp only [invOf_eq_inv, ← div_eq_mul_inv, fract_div_natCast_eq_div_natCast_mod]

theorem isRat_intFract_of_isRat_negOfNat (r : α) (n d : ℕ) :
    IsRat r (negOfNat n) d → IsRat (Int.fract r) (-n % d) d := by
  rintro ⟨inv, rfl⟩
  refine ⟨inv, ?_⟩
  simp only [invOf_eq_inv, ← div_eq_mul_inv, fract_div_intCast_eq_div_intCast_mod,
    negOfNat_eq, ofNat_eq_coe]

/-- `norm_num` extension for `Int.fract` -/
@[norm_num (Int.fract _)]
def evalIntFract : NormNumExt where eval {u α} e := do
  match e with
  | ~q(@Int.fract _ $instR $instO $instF $x) =>
    match ← derive x with
    | .isBool .. => failure
    | .isNat _ _ pb => do
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      have z : Q(ℕ) := Lean.mkRawNatLit 0
      letI : $z =Q 0 := ⟨⟩
      return .isNat _ z q(isNat_intFract_of_isNat $x _ $pb)
    | .isNegNat _ _ pb => do
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      have z : Q(ℕ) := Lean.mkRawNatLit 0
      letI : $z =Q 0 := ⟨⟩
      return .isNat _ z q(isNat_intFract_of_isInt _ _ $pb)
    | .isNNRat _ q n d h => do
      let _i ← synthInstanceQ q(Field $α)
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      have n' : Q(ℕ) := Lean.mkRawNatLit (q.num.natAbs % q.den)
      letI : $n' =Q $n % $d := ⟨⟩
      return .isNNRat _ (Int.fract q) n' d q(isNNRat_intFract_of_isNNRat _ $n $d $h)
    | .isNegNNRat _ q n d h => do
      let _i ← synthInstanceQ q(Field $α)
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      have n' : Q(ℤ) := mkRawIntLit (q.num % q.den)
      letI : $n' =Q -$n % $d := ⟨⟩
      return .isRat _ (Int.fract q) n' d q(isRat_intFract_of_isRat_negOfNat _ $n $d $h)
  | _, _, _ => failure

example : Int.fract (3.7 : ℚ) = 0.7 := by norm_num
example : Int.fract (-3.7 : ℚ) = 0.3 := by norm_num

end NormNum

example : ¬ IsIntegral ℤ (1 / 2 : ℚ) := by
  intro h
  obtain ⟨x, hx⟩ := ((isIntegrallyClosed_iff_isIntegrallyClosedIn ℚ).1 inferInstance).isIntegral_iff.1 h
  apply_fun Int.fract at hx
  norm_num at hx

I was too lazy to even complain that norm_num wasn't able to close the goal, and you made it working, amazing!

[Ruben Van de Velde]

Yeah, back in June :/

[Kenny Lau]

it seems like we want a theorem of the form "if x satisfies polynomial p with certain properties then x is not integral over something"

[Qingfeng Li]

image.png

[Kenny Lau]

we have Polynomial.IsPrimitive

[Kenny Lau]

but it doesn't seem like the theorem you quoted is available

[Kenny Lau]

if you're interested please prove it and PR to mathlib (and ping me)

[Qingfeng Li]

OK, I think this theorem is correct in math (although I haven't proven precisely)

[Kenny Lau]

it might be advisable to find a reference for it

[Kenny Lau]

note that it is false as stated (consider the polynomial -X)

[Riccardo Brasca]

It' enough to find an irreducible polynomial whose leading coefficient is not a unit and that has the element as root. This follows from minpoly.isIntegrallyClosed_dvd and minpoly.prime_of_isIntegrallyClosed

[Riccardo Brasca]

I mean irreducible over ℤ (or over any integrally closed ring). If the polynomial is moreover primitive than, by Gauss lemma, it is enough to check irreducibility over ℚ.

[Qingfeng Li]

Thanks a lot! I finally solved my problem by this lemma.

import Mathlib

open Polynomial

lemma isIntegral_iff_leadingCoeff_of_irreducible_poly_isunit {R S : Type}
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R] [CommRing S] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S]
    {α : S} {f : R[X]} (f_irr : Irreducible f) (f_root : f.aeval α = 0) :
    IsIntegral R α ↔ IsUnit f.leadingCoeff  := by
  constructor
  · intro int_a
    obtain ⟨g, hg⟩ := minpoly.isIntegrallyClosed_dvd int_a f_root
    have := Irreducible.isUnit_or_isUnit f_irr hg
    simp only [minpoly.not_isUnit R α, false_or] at this
    obtain ⟨r, uni_r, geq⟩ := Polynomial.isUnit_iff.mp this
    apply_fun Polynomial.leadingCoeff at hg
    rw [leadingCoeff_mul, ← geq, leadingCoeff_C, minpoly.monic int_a, one_mul] at hg
    rw [hg]; exact uni_r
  · rintro f_uni
    obtain ⟨r, hr, _⟩ := (isUnit_iff_exists.mp f_uni)
    refine ⟨f * C r, monic_mul_C_of_leadingCoeff_mul_eq_one hr, ?_⟩
    rw [eval₂_mul, mul_eq_zero]; left
    exact f_root


lemma isIntegral_iff_leadingCoeff_of_primitive_and_map_irreducible_poly_isunit {R S K : Type}
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R] [CommRing S] [IsDomain S] [Algebra R S] [NoZeroSMulDivisors R S]
    [Field K] [Algebra R K] [IsFractionRing R K] [NormalizedGCDMonoid R]
    {α : S} {f : R[X]} (f_pri : IsPrimitive f) (f_irr : Irreducible (map (algebraMap R K) f))
    (f_root : f.aeval α = 0) : IsIntegral R α ↔ IsUnit f.leadingCoeff :=
    isIntegral_iff_leadingCoeff_of_irreducible_poly_isunit
    ((IsPrimitive.irreducible_iff_irreducible_map_fraction_map f_pri).mpr f_irr) f_root

[Kenny Lau]

@Qingfeng Li nice! would you like to PR?

[Riccardo Brasca]

Note that this has nothing to do with number fields: you should replace ℤ by any integrally closed domain and K by any L-algebra, where L satisfies IsFractionRing R L.

[Qingfeng Li]

Yes, I'll make my code more general and submit a PR soon

[Riccardo Brasca]

Also, please add the version for primitive polynomials and irreducibility over the fraction field, in practice this is what one does.

[Kenny Lau]

@Qingfeng Li I've added a comment to your PR

[Riccardo Brasca]

Feel free to ask my review (I will have time in 48 hours though)

[Snir Broshi]

Riccardo Brasca said:

Also, please add the version for primitive polynomials and irreducibility over the fraction field, in practice this is what one does.

Is the plan to add this in a separate PR? (separate from #29798)