mathlib documentation


Ideals in free modules over PIDs #

Main results #

noncomputable def ideal.quotient_equiv_pi_span {ι : Type u_1} {R : Type u_2} {S : Type u_3} [comm_ring R] [comm_ring S] [algebra R S] [is_domain R] [is_principal_ideal_ring R] [is_domain S] [fintype ι] (I : ideal S) (b : basis ι R S) (hI : I ) :
(S I) ≃ₗ[R] Π (i : ι), R ideal.span {ideal.smith_coeffs b I hI i}

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

noncomputable def ideal.quotient_equiv_pi_zmod {ι : Type u_1} {S : Type u_3} [comm_ring S] [is_domain S] [fintype ι] (I : ideal S) (b : basis ι S) (hI : I ) :
S I ≃+ Π (i : ι), zmod (ideal.smith_coeffs b I hI i).nat_abs

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

noncomputable def ideal.fintype_quotient_of_free_of_ne_bot {S : Type u_3} [comm_ring S] [is_domain S] [ 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.