Ideals in free modules over PIDs #
Main results #
Ideal.quotientEquivPiSpan: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.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.
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.
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.
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.
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})