Prove an exercise from Atiyah's book

Stream: new members

[Nick_adfor]

I want to prove an exercise from Atiyah's book An introduction to Commutative Algebra P67 5. i)

Theorem: Let A ⊆ B be rings, B integral over A. If x ∈ A is a unit in B then it is a unit in A.

Proof:

1. Since x is a unit in B, ∃ y ∈ B such that x·y = 1

2. Because B is integral over A, y satisfies a monic polynomial equation:
   yⁿ + aₙ₋₁yⁿ⁻¹ + ··· + a₁y + a₀ = 0 (aᵢ ∈ A)

3. Multiply through by xⁿ⁻¹:
   xⁿ⁻¹yⁿ + aₙ₋₁xⁿ⁻¹yⁿ⁻¹ + ··· + a₁xⁿ⁻¹y + a₀xⁿ⁻¹ = 0

4. Using x·y = 1, we get:
   y = -aₙ₋₁ - aₙ₋₂x - ··· - a₀xⁿ⁻¹

5. Since all terms on the right are in A, we conclude y ∈ A

6. Therefore x has an inverse y in A, so x is a unit in A

import Mathlib

variable (A B : Type*) [CommRing A][CommRing B]
variable [Algebra A B]
variable (inj_algebraMap : Function.Injective (algebraMap A B))
variable (hB_int : Algebra.IsIntegral A B)

theorem unit_in_B_implies_unit_in_A (x : A) (hx : IsUnit (algebraMap A B x)) : IsUnit x := by
  obtain ⟨u, hu⟩ := hx
  set y := u.inv
  have hxy : algebraMap A B x * y = 1 := by
    rw [← hu]; exact u.mul_inv
  have hy_integral : IsIntegral A y := hB_int y
  obtain ⟨p, hp_monic, hp_root⟩ := hy_integral
  ...

But before I finish it, I find some question in my code:

1. Is it OK to use inj_algebraMap to make A ⊆ B, rather than subtype or subring? (I haven't use inj_algebraMap in the theorem proof yet because of that.)
2. Step 2 and Step 3 explicitly construct a polynomial. But in my code, obtaining a p abstractly seems easier. Should I really construct a polynomial as the pen-and-paper proof? (I even think that lean can do Step 2 and Step 3 in some automatic way, as it is just some trivial calculation. But maybe what makes it difficult is the type conversion.)
3. The code is written in v4.5.0-rc1 (The version is downloaded from ICL's formalising-mathematics-2024). But hB_int shows an error in the latest version in Lean 4 Web. What happened to the version update?

[Kevin Buzzard]

1. Sure 2. I'm not sure I understand the question. What are the two examples of lean code you want an opinion about what to prefer? 3. What's the error?

[Nick_adfor]

Kevin Buzzard said:

1. Sure 2. I'm not sure I understand the question. What are the two examples of lean code you want an opinion about what to prefer? 3. What's the error?

3. The error is unknown identifier hB_int

[Kevin Buzzard]

Then include hB_int in before the theorem

[Junyan Xu]

I have a short PR #23684 (now #26746) for this, but somehow it didn't get merged after 3 months ...

[Nick_adfor]

Now I write it this way with rw?. When it suggest me to Try this: rw [Nat.add_sub_cancel_right] -- no goals, I followed it. But then, it tell me with two cases (induction). How do rw? work in such a strange way?

import Mathlib

open Polynomial

variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]


theorem unit_of_isIntegral_extension
    (hB_int : ∀ b : B, IsIntegral A b)
    (inj : Function.Injective (algebraMap A B))
    (x : A) (hx : IsUnit (algebraMap A B x)) : IsUnit x := by
  -- Let y be the inverse of x in B
  obtain ⟨u, hu⟩ := hx
  let y := u.inv -- y ∈ B, and x * y = 1 in B
  have hxy : algebraMap A B x * y = 1 := by
    rw [← hu]
    exact u.mul_inv

  -- y is integral over A
  have hy_int : IsIntegral A y := hB_int y
  obtain ⟨p, p_monic, hp⟩ := hy_int

  let n := p.natDegree
  let q : Polynomial A :=
    ∑ i ∈ Finset.range (n + 1), Polynomial.monomial (n - i) (p.coeff i)
  have hq : Polynomial.eval x q = 0 := by
    simp only [q, Polynomial.eval_finset_sum, Polynomial.eval_monomial]
    let xB := algebraMap A B x
    have h_sum_form : ∑ i ∈ Finset.range (p.natDegree + 1),
      (algebraMap A B (Polynomial.coeff p i)) * y ^ i = 0 := by
      rw [← Polynomial.eval₂_eq_sum_range]
      exact hp
    have h_sum : ∑ i ∈ Finset.range (n + 1),
      (algebraMap A B (Polynomial.coeff p i)) * y ^ i * xB ^ n = 0 := by
      apply Eq.trans _ (zero_mul (xB ^ n))
      rw [← Finset.sum_mul]
      exact congr_arg (· * xB ^ n) h_sum_form
    have h_sum_rearranged : ∑ i ∈ Finset.range (n + 1),
      (algebraMap A B (p.coeff i)) * (y ^ i * xB ^ n) = 0 := by
      rw [← h_sum]
      apply Finset.sum_congr rfl
      intro i hi
      rw [mul_assoc]
    have h_rewrite : ∀ i ∈ Finset.range (n + 1), y ^ i * xB ^ n = xB ^ (n - i) := by
      intro i hi
      have h_inv : ∀ i, y ^ i * xB ^ i = 1 := by
        intro i
        induction' i with i ih
        · simp
        · rw [pow_succ, pow_succ, ← mul_assoc, mul_assoc (y ^ i), mul_comm y (xB ^ i), ← mul_assoc (y ^ i), ih, one_mul, mul_comm, hxy]
      have hi_le : i ≤ n := Finset.mem_range_succ_iff.mp hi
      have h_eq : xB ^ n = (xB ^ i) * (xB ^ (n - i)) := by
        rw [← pow_add, Nat.add_sub_cancel' hi_le]
      calc
        y ^ i * xB ^ n = y ^ i * (xB ^ i * xB ^ (n - i)) := by rw [h_eq]
        _ = (y ^ i * xB ^ i) * xB ^ (n - i) := by rw [mul_assoc]
        _ = 1 * xB ^ (n - i) := by rw [h_inv i]
        _ = xB ^ (n - i) := by rw [one_mul]
    have h_sum_transformed : ∑ i ∈ Finset.range (n + 1), (algebraMap A B (p.coeff i)) * xB ^ (n - i) = 0 := by
      rw [← h_sum_rearranged]
      apply Finset.sum_congr rfl
      intro i hi
      rw [h_rewrite i hi]
    have h_sum_mapped : algebraMap A B (∑ i ∈ Finset.range (n + 1), p.coeff i * x ^ (n - i)) = 0 := by
      rw [map_sum]
      simp_rw [map_mul, map_pow]
      exact h_sum_transformed
    have h_zero : algebraMap A B (0 : A) = 0 := RingHom.map_zero (algebraMap A B)
    have h_sum_A : ∑ i ∈ Finset.range (n + 1), p.coeff i * x ^ (n - i) = 0 :=
      inj (by
        rw [h_zero]
        exact h_sum_mapped)
    exact h_sum_A

  let r := - ∑ i ∈ Finset.range n, (p.coeff i) * x ^ (n - 1 - i)

  have hx_inv : x * r = 1 := by
    dsimp [r]
    rw [mul_neg]
    rw [Finset.mul_sum]
    have h_eq_terms : ∀ i ∈ Finset.range n,
      x * (p.coeff i * x ^ (n - 1 - i)) = p.coeff i * x ^ (n - i) := by
      intros i hi
      calc
        x * (p.coeff i * x ^ (n - 1 - i))
          = (x * p.coeff i) * x ^ (n - 1 - i) := by rw [mul_assoc]
      _ = p.coeff i * x * x ^ (n - 1 - i) := by rw [mul_comm x (p.coeff i)]
      _ = p.coeff i * x ^ (1 + (n - 1 - i)) := by ring
      _ = p.coeff i * x ^ (n - i) := by
          congr 1
          rw [← Nat.add_sub_assoc]
          rw [Nat.add_comm]
          rw [tsub_add_eq_add_tsub] --The most terrible part!!!
          rw?

    rw [Finset.sum_congr rfl h_eq_terms]

    have p_n : p.coeff n = 1 := p_monic.coeff_natDegree
    have h_sum_eq_zero : ∑ i ∈ Finset.range (n + 1), p.coeff i * x ^ (n - i) = 0 := by
      dsimp [q] at hq
      simp only [Polynomial.eval_finset_sum, Polynomial.eval_monomial] at hq
      exact hq

    have h_split : (∑ i ∈ Finset.range n, p.coeff i * x ^ (n - i)) + p.coeff n * x ^ 0 = 0 := by
      rw [← h_sum_eq_zero]
      rw [Finset.sum_range_succ, p_n, Nat.sub_self, pow_zero, mul_one]

    rw [p_n, pow_zero, mul_one] at h_split

    have key : ∑ i ∈ Finset.range n, p.coeff i * x ^ (n - i) = -1 := by
      exact
        eq_neg_of_add_eq_zero_left
          (inj (congrArg (⇑(algebraMap A B)) (inj (congrArg (⇑(algebraMap A B)) h_split))))

    rw [key, neg_neg]




  exact
    isUnit_of_mul_eq_one x r
      (inj (congrArg (⇑(algebraMap A B)) (inj (congrArg (⇑(algebraMap A B)) hx_inv))))

/-
1. Since x is a unit in B, ∃ y ∈ B such that x·y = 1
2. Because B is integral over A, y satisfies a monic polynomial equation:
   yⁿ + aₙ₋₁yⁿ⁻¹ + ··· + a₁y + a₀ = 0 (aᵢ ∈ A)
3. Multiply through by xⁿ⁻¹:
   xⁿ⁻¹yⁿ + aₙ₋₁xⁿ⁻¹yⁿ⁻¹ + ··· + a₁xⁿ⁻¹y + a₀xⁿ⁻¹ = 0
4. Using x·y = 1, we get:
   y = -aₙ₋₁ - aₙ₋₂x - ··· - a₀xⁿ⁻¹
5. Since all terms on the right are in A, we conclude y ∈ A
6. Therefore x has an inverse y in A, so x is a unit in A
-/

[Nick_adfor]

Finished