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 : 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.

noncomputable def Ideal.quotientEquivPiZMod {ι : Type u_1} {S : Type u_3} [CommRing S] [IsDomain S] [Finite ι] (I : Ideal S) (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.

noncomputable def Ideal.fintypeQuotientOfFreeOfNeBot {S : Type u_3} [CommRing S] [IsDomain S] [Module.Free ℤ S] [Module.Finite ℤ S] (I : Ideal S) (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.

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 : Basis ι R S) {I : Ideal S} (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.

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 : Basis ι R S) [Nontrivial F] [∀ (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})] : FiniteDimensional.finrank F (S ⧸ I) = Finset.sum Finset.univ fun (i : ι) => FiniteDimensional.finrank F (R ⧸ Ideal.span {Ideal.smithCoeffs b I hI i})