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, ifSis finite free as a module over a PIDR, can be written as a product of quotients ofRby 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]
[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
- I.quotient_equiv_pi_span b hI = let a : ι → R := ideal.smith_coeffs b I hI, b' : basis ι R S := ideal.ring_basis b I hI, ab : basis ι R ↥I := ideal.self_basis b I hI, e : S ≃ₗ[R] ↥I := b'.equiv ab (equiv.refl ι), f : S →ₗ[R] S := (linear_map.restrict_scalars R (submodule.subtype I)).comp ↑e, f_apply : ∀ (x : S), ⇑f x = ↑(⇑(b'.equiv ab (equiv.refl ι)) x) := _, I' : submodule R (ι → R) := submodule.pi set.univ (λ (i : ι), ideal.span {a i}) in (linear_equiv.restrict_scalars R (submodule.quotient.restrict_scalars_equiv R I)).symm.trans ((submodule.quotient.equiv (submodule.restrict_scalars R I) I' b'.equiv_fun _).trans (let this : ((Π (i : ι), (λ (i : ι), R) i) ⧸ submodule.pi set.univ (show ι → submodule R R, from λ (i : ι), ideal.span {a i})) ≃ₗ[R] Π (i : ι), (λ (i : ι), R) i ⧸ (show ι → submodule R R, from λ (i : ι), ideal.span {a i}) i := submodule.quotient_pi (show ι → submodule R R, from λ (i : ι), ideal.span {a i}) in this))
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 ≠ ⊥) :
Ideal quotients over a free finite extension of ℤ are isomorphic to a direct product of
zmod.
Equations
- I.quotient_equiv_pi_zmod b hI = let a : ι → ℤ := ideal.smith_coeffs b I hI, e : (S ⧸ I) ≃ₗ[ℤ] Π (i : ι), ℤ ⧸ ideal.span {ideal.smith_coeffs b I hI i} := I.quotient_equiv_pi_span b hI, e' : (Π (i : ι), ℤ ⧸ ideal.span {a i}) ≃+ Π (i : ι), zmod (a i).nat_abs := add_equiv.Pi_congr_right (λ (i : ι), ↑((a i).quotient_span_equiv_zmod)) in ↑e.trans e'
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 ≠ ⊥) :
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
- I.fintype_quotient_of_free_of_ne_bot hI = let b : basis (module.free.choose_basis_index ℤ S) ℤ S := module.free.choose_basis ℤ S, a : module.free.choose_basis_index ℤ S → ℤ := ideal.smith_coeffs b I hI, e : S ⧸ I ≃+ Π (i : module.free.choose_basis_index ℤ S), zmod (ideal.smith_coeffs b I hI i).nat_abs := I.quotient_equiv_pi_zmod b hI in fintype.of_equiv (Π (i : module.free.choose_basis_index ℤ S), zmod (a i).nat_abs) ↑(e.symm)
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
- ideal.quotient_equiv_direct_sum F b hI = (linear_equiv.restrict_scalars F (I.quotient_equiv_pi_span b hI)).trans (direct_sum.linear_equiv_fun_on_fintype F ι (λ (i : ι), R ⧸ ideal.span {ideal.smith_coeffs b I hI i})).symm
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})] :
finite_dimensional.finrank F (S ⧸ I) = finset.univ.sum (λ (i : ι), finite_dimensional.finrank F (R ⧸ ideal.span {ideal.smith_coeffs b I hI i}))