# mathlib3documentation

linear_algebra.free_module.ideal_quotient

# Ideals in free modules over PIDs #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main results #

• ideal.quotient_equiv_pi_span: 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.quotient_equiv_pi_span {R : Type u_1} {S : Type u_2} {ι : Type u_3} [comm_ring R] [comm_ring S] [ S] [is_domain R] [is_domain S] [finite ι] (I : ideal S) (b : R S) (hI : I ) :
(S I) ≃ₗ[R] Π (i : ι), R ideal.span hI i}

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

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

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

Equations
noncomputable def ideal.fintype_quotient_of_free_of_ne_bot {S : Type u_2} [comm_ring S] [is_domain S] [ S] [ 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
noncomputable def ideal.quotient_equiv_direct_sum {R : Type u_1} {S : Type u_2} {ι : Type u_3} [comm_ring R] [comm_ring S] [ S] [is_domain R] [is_domain S] [finite ι] (F : Type u_4) [comm_ring F] [ R] [ S] [ S] (b : R S) {I : ideal S} (hI : I ) :
(S I) ≃ₗ[F] (λ (i : ι), R ideal.span hI i})

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

Equations
theorem ideal.finrank_quotient_eq_sum {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [ S] [is_domain R] [is_domain S] (F : Type u_4) [comm_ring F] [ R] [ S] [ S] {I : ideal S} (hI : I ) {ι : Type u_3} [fintype ι] (b : R S) [nontrivial F] [ (i : ι), (R ideal.span hI i})] [ (i : ι), (R ideal.span hI i})] :
(S I) = finset.univ.sum (λ (i : ι), (R ideal.span hI i}))