# Ideals in free modules over PIDs #

## Main results #

• Ideal.quotientEquivPiSpan: S ⧸ I, if S is finite free as a module over a PID R, can be written as a product of quotients of R by principal ideals.
noncomputable def Ideal.quotientEquivPiSpan {ι : Type u_1} {R : Type u_2} {S : Type u_3} [] [] [Algebra R S] [] [] [] (I : ) (b : Basis ι R S) (hI : I ) :
(S I) ≃ₗ[R] (i : ι) → R Ideal.span {Ideal.smithCoeffs b I hI i}

We can write the quotient of an ideal over a PID as a product of quotients by principal ideals.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def Ideal.quotientEquivPiZMod {ι : Type u_1} {S : Type u_3} [] [] [] (I : ) (b : Basis ι S) (hI : I ) :
S I ≃+ ((i : ι) → ZMod (Int.natAbs (Ideal.smithCoeffs b I hI i)))

Ideal quotients over a free finite extension of ℤ are isomorphic to a direct product of ZMod.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def Ideal.fintypeQuotientOfFreeOfNeBot {S : Type u_3} [] [] [] [] (I : ) (hI : I ) :
Fintype (S I)

A nonzero ideal over a free finite extension of ℤ has a finite quotient.

Can't be an instance because of the side condition I ≠ ⊥, and more importantly, because the choice of Fintype instance is non-canonical.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def Ideal.quotientEquivDirectSum {ι : Type u_1} {R : Type u_2} {S : Type u_3} [] [] [Algebra R S] [] [] [] (F : Type u_4) [] [Algebra F R] [Algebra F S] [] (b : Basis ι R S) {I : } (hI : I ) :
(S I) ≃ₗ[F] DirectSum ι fun (i : ι) => R Ideal.span {Ideal.smithCoeffs b I hI i}

Decompose S⧸I as a direct sum of cyclic R-modules (quotients by the ideals generated by Smith coefficients of I).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Ideal.finrank_quotient_eq_sum {R : Type u_2} {S : Type u_3} [] [] [Algebra R S] [] [] (F : Type u_4) [] [Algebra F R] [Algebra F S] [] {I : } (hI : I ) {ι : Type u_5} [] (b : Basis ι R S) [] [∀ (i : ι), Module.Free F (R Ideal.span {Ideal.smithCoeffs b I hI i})] [∀ (i : ι), Module.Finite F (R Ideal.span {Ideal.smithCoeffs b I hI i})] :