Foundation Pinch Algebra Principal Ideal Eq Of Mutual Dvd

Mutual divisibility and ideals

In a commutative ring, an ideal generated by a single element a is the set of all multiples of a. The declaration principal_ideal_eq_of_mutual_dvd states that if a divides b and b divides a, then the principal ideal generated by a equals the principal ideal generated by b. The proof is a short two-line argument: any multiple of a is a multiple of b via the reverse divisibility, and conversely.

This fact belongs to the classical algebra of ideals, and its proof does not depend on any special property of the ring. It holds in every commutative ring, whether or not the ring is a unique factorization domain. The declaration is part of the framework's machine-checked library of formal theorems, and its proof is verified by the Lean kernel.

The framework uses this lemma as a template for a larger project: the equality of principal ideals from mutual divisibility appears in the algebraic heart of a proposed stage of the Birch and Swinnerton-Dyer conjecture. The idea is that if two objects in a ring divide each other, they are the same ideal, and this can be used to identify two apparently different constructions. The framework also derives a companion template, imc_equality_template, which packages the same argument for reuse.

The declaration does not claim that mutual divisibility implies equality of the elements themselves. In a ring with zero divisors, a divides b and b divides a can hold without a equaling b. It also does not claim that the ideals are equal in any stronger sense, such as equality of the elements up to a unit; that is a separate statement, mutual_div_unit, which requires the ring to be a unique factorization domain.

/-- **F5.1.2/1.4**: Principal ideal equality from mutual divisibility.
    In a commutative ring, (a) = (b) iff a | b and b | a. -/
theorem principal_ideal_eq_of_mutual_dvd {R : Type*} [CommRing R]
    {a b : R} (hab : a ∣ b) (hba : b ∣ a) :
    Ideal.span ({a} : Set R) = Ideal.span {b} := by
  ext x
  simp only [Ideal.mem_span_singleton]
  constructor
  · intro ⟨r, hr⟩
    obtain ⟨c, hc⟩ := hba
    exact ⟨r * c, by rw [hr, hc]; ring⟩
  · intro ⟨r, hr⟩
    obtain ⟨d, hd⟩ := hab
    exact ⟨r * d, by rw [hr, hd]; ring⟩

/-- **F5.1.2/1.4**: Principal ideal equality from mutual divisibility.
    In a commutative ring, (a) = (b) iff a | b and b | a. -/
theorem principal_ideal_eq_of_mutual_dvd {R : Type*} [CommRing R]
    {a b : R} (hab : a ∣ b) (hba : b ∣ a) :
    Ideal.span ({a} : Set R) = Ideal.span {b} := by
  ext x
  simp only [Ideal.mem_span_singleton]
  constructor
  · intro ⟨r, hr⟩
    obtain ⟨c, hc⟩ := hba
    exact ⟨r * c, by rw [hr, hc]; ring⟩
  · intro ⟨r, hr⟩
    obtain ⟨d, hd⟩ := hab
    exact ⟨r * d, by rw [hr, hd]; ring⟩

/-- **F5.2.3**: IMC equality from Kato (one side) + reverse divisibility (other side).
    This is the algebraic heart of BSD Stage 6.

    Given: (A) | (B) and (B) | (A) in a commutative ring,
    conclude (A) = (B) as principal ideals. -/
theorem imc_equality_template {R : Type*} [CommRing R]
    {A B : R} (hAB : A ∣ B) (hBA : B ∣ A) :
    Ideal.span ({A} : Set R) = Ideal.span {B} :=
  principal_ideal_eq_of_mutual_dvd hAB hBA

What this page does not claim

Mutual divisibility implies equality of the elements themselves in a ring with zero divisors. The ideals are equal in the stronger sense of the elements being equal up to a unit; that requires a unique factorization domain. The framework's use of this lemma proves the Birch and Swinnerton-Dyer conjecture.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PinchAlgebra.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: