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} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsPrincipalIdealRing R] [IsDomain S] [Finite ι] (I : Ideal S) (b : Module.Basis ι R S) (hI : I ≠ ⊥) : (S ⧸ I) ≃ₗ[R] (i : ι) → R ⧸ span {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

• I.quotientEquivPiSpan b hI = (Submodule.restrictScalars R I).quotientEquivPiSpan b ⋯

noncomputable def Ideal.quotientEquivPiZMod {ι : Type u_1} {S : Type u_3} [CommRing S] [IsDomain S] [Finite ι] (I : Ideal S) (b : Module.Basis ι ℤ S) (hI : I ≠ ⊥) : S ⧸ I ≃+ ((i : ι) → ZMod (smithCoeffs b I hI i).natAbs)

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

Equations

• I.quotientEquivPiZMod b hI = (Submodule.restrictScalars ℤ I).quotientEquivPiZMod b ⋯

theorem Ideal.finiteQuotientOfFreeOfNeBot {S : Type u_3} [CommRing S] [IsDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] (I : Ideal S) (hI : I ≠ ⊥) : Finite (S ⧸ I)

A nonzero ideal over a free finite extension of ℤ has a finite quotient. It can't be an instance because of the side condition I ≠ ⊥.

noncomputable def Ideal.quotientEquivDirectSum {ι : Type u_1} {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsPrincipalIdealRing R] [IsDomain S] [Finite ι] (F : Type u_4) [CommRing F] [Algebra F R] [Algebra F S] [IsScalarTower F R S] (b : Module.Basis ι R S) {I : Ideal S} (hI : I ≠ ⊥) : (S ⧸ I) ≃ₗ[F] DirectSum ι fun (i : ι) => R ⧸ span {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

• Ideal.quotientEquivDirectSum F b hI = Submodule.quotientEquivDirectSum F b ⋯

theorem Ideal.finrank_quotient_eq_sum {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsPrincipalIdealRing R] [IsDomain S] (F : Type u_4) [CommRing F] [Algebra F R] [Algebra F S] [IsScalarTower F R S] {I : Ideal S} (hI : I ≠ ⊥) {ι : Type u_5} [Fintype ι] (b : Module.Basis ι R S) [Nontrivial F] [∀ (i : ι), Module.Free F (R ⧸ span {smithCoeffs b I hI i})] [∀ (i : ι), Module.Finite F (R ⧸ span {smithCoeffs b I hI i})] : Module.finrank F (S ⧸ I) = ∑ i : ι, Module.finrank F (R ⧸ span {smithCoeffs b I hI i})