Quotients of powers of principal ideals

This file deals with taking quotients of powers of principal ideals.

Main definitions and results

• Ideal.quotEquivPowQuotPowSucc: for a principal ideal I, R ⧸ I ≃ₗ[R] I ^ n ⧸ I ^ (n + 1)

Implementation details

At site of usage, calling LinearEquiv.toEquiv can cause timeouts in the search for a complex synthesis like Module 𝒪[K] 𝓀[k], so the plain equiv versions are provided.

These equivs are defined here as opposed to in the quotients file since they cannot be formed as ring equivs.

noncomputable def Ideal.quotEquivPowQuotPowSucc {R : Type u_1} [CommRing R] [IsDomain R] {I : Ideal R} (h : Submodule.IsPrincipal I) (h' : I ≠ ⊥) (n : ℕ) : (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ I • ⊤

For a principal ideal I, R ⧸ I ≃ₗ[R] I ^ n ⧸ I ^ (n + 1). To convert into a form that uses the ideal of R ⧸ I ^ (n + 1), compose with Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPow.

Equations

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

noncomputable def Ideal.quotEquivPowQuotPowSuccEquiv {R : Type u_1} [CommRing R] [IsDomain R] {I : Ideal R} (h : Submodule.IsPrincipal I) (h' : I ≠ ⊥) (n : ℕ) : R ⧸ I ≃ ↥(I ^ n) ⧸ I • ⊤

For a principal ideal I, R ⧸ I ≃ I ^ n ⧸ I ^ (n + 1). Supplied as a plain equiv to bypass typeclass synthesis issues on complex Module goals. To convert into a form that uses the ideal of R ⧸ I ^ (n + 1), compose with Ideal.powQuotPowSuccEquivMapMkPowSuccPow.

Equations

• Ideal.quotEquivPowQuotPowSuccEquiv h h' n = ↑(Ideal.quotEquivPowQuotPowSucc h h' n)