Prime classification, part 2: the quotient ring isomorphism

Thesis. §3.2, the proof of Proposition 3.2.1 reasons about the quotient O/(p) directly (in the thesis, via the presentation ℤ/pᵏ[x]/g(x) and explicit index computations).

This file proves the structural bridge:

• quadraticOrderModPEquivPolyModQuot — O/(p) ≅ 𝔽ₚ[X]/(polyMod d p)
• quadraticOrderModPEquivXSqQuot — in the ramified case (p ∣ d), O/(p) ≅ 𝔽ₚ[X]/(X²) (the dual numbers)

Divergence from thesis. This ring isomorphism is the central reorganisation of the argument. The thesis manipulates O/(p) through the concrete polynomial-quotient presentation and computes ideal indices by hand. Here we instead transport every ideal-theoretic property of (p) ⊆ O (maximality → inert, radicality → split, non-radicality → ramified) across this single iso to the corresponding property of (polyMod d p) ⊆ 𝔽ₚ[X], where the field/PID structure of 𝔽ₚ[X] does the work. The downstream files (Inert, Split, Ramified) are thin wrappers over this transport. This is a Lean-idiomatic route; the mathematical content matches Prop 3.2.1.

noncomputable def QuadraticOrder.quadraticOrderModPEquivPolyModQuot (d : ℤ) (p : ℕ) [Fact (Nat.Prime p)] : QuadraticOrder d ⧸ Ideal.span {↑p} ≃+* Polynomial (ZMod p) ⧸ Ideal.span {polyMod d p}

The structural bridge: QuadraticOrder d / (p) is ring-equivalent to (ZMod p)[X] / (polyMod d p). This is the key isomorphism connecting ideal-theoretic properties of (p) in QuadraticOrder d to polynomial-level properties of polyMod d p in (ZMod p)[X]. It is the foundation on which the inert/split/ramified ideal-theoretic characterisations are built.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QuadraticOrder.quadraticOrderModPEquivXSqQuot (d : ℤ) (p : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hd : d % 4 = 0 ∨ d % 4 = 1) (hpd : ↑p ∣ d) : QuadraticOrder d ⧸ Ideal.span {↑p} ≃+* Polynomial (ZMod p) ⧸ Ideal.span {Polynomial.X ^ 2}

Ramified-case quotient isomorphism: when p ∣ d (with the discriminant hypothesis d ≡ 0 ∨ 1 (mod 4) and p ≠ 2), the quotient QuadraticOrder d / (p) is isomorphic to (ZMod p)[X] / (X²). This makes the dual-numbers / non-reduced structure of the ramified branch explicit: the image of X in this quotient is nilpotent of order 2, witnessing that (p) is not a radical ideal in QuadraticOrder d.

Equations

• QuadraticOrder.quadraticOrderModPEquivXSqQuot d p hp2 hd hpd = (QuadraticOrder.quadraticOrderModPEquivPolyModQuot d p).trans (Ideal.quotEquivOfEq ⋯)