mathlib3 documentation

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 #

noncomputable def ideal.quotient_equiv_pi_span {R : Type u_1} {S : Type u_2} {ι : Type u_3} [comm_ring R] [comm_ring S] [algebra R S] [is_domain R] [is_principal_ideal_ring R] [is_domain S] [finite ι] (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.

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

Equations
noncomputable def ideal.fintype_quotient_of_free_of_ne_bot {S : Type u_2} [comm_ring S] [is_domain 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
noncomputable def ideal.quotient_equiv_direct_sum {R : Type u_1} {S : Type u_2} {ι : Type u_3} [comm_ring R] [comm_ring S] [algebra R S] [is_domain R] [is_principal_ideal_ring R] [is_domain S] [finite ι] (F : Type u_4) [comm_ring F] [algebra F R] [algebra F S] [is_scalar_tower F R S] (b : basis ι R S) {I : ideal S} (hI : I ) :
(S I) ≃ₗ[F] direct_sum ι (λ (i : ι), R ideal.span {ideal.smith_coeffs 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
theorem ideal.finrank_quotient_eq_sum {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [algebra R S] [is_domain R] [is_principal_ideal_ring R] [is_domain S] (F : Type u_4) [comm_ring F] [algebra F R] [algebra F S] [is_scalar_tower F R S] {I : ideal S} (hI : I ) {ι : Type u_3} [fintype ι] (b : basis ι R S) [nontrivial F] [ (i : ι), module.free F (R ideal.span {ideal.smith_coeffs b I hI i})] [ (i : ι), module.finite F (R ideal.span {ideal.smith_coeffs b I hI i})] :