Documentation

Mathlib.LinearAlgebra.FreeModule.IdealQuotient

Ideals in free modules over PIDs #

Main results #

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 (Ideal.smithCoeffs b I hI i).natAbs)

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

    Equations
    • I.quotientEquivPiZMod b hI = let a := Ideal.smithCoeffs b I hI; let e := I.quotientEquivPiSpan b hI; let e' := AddEquiv.piCongrRight fun (i : ι) => (a i).quotientSpanEquivZMod; (e).trans e'
    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 ) :
      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
      • 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})] :