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

## Instances For

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.

## Instances For

noncomputable def
Ideal.fintypeQuotientOfFreeOfNeBot
{S : Type u_3}
[CommRing S]
[IsDomain 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

- One or more equations did not get rendered due to their size.

## Instances For

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.

## Instances For

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})