powQuotPowSuccEquivMapMkPowSuccPow

English

The inverse of quotQuotEquivCommₐ R I J equals the inverse of quotQuotEquivComm I J with I,J swapped.

Русский

Обратное отображение quotQuotEquivCommₐ R I J равно обратному отображению quotQuotEquivComm I J с поменянными местами I и J.

LaTeX

$$$((quotQuotEquivCommₐ R I J).symm) = (quotQuotEquivComm I J).symm$$$

Lean4

/-- `I ^ n ⧸ I ^ (n + 1)` can be viewed as a quotient module and as ideal of `R ⧸ I ^ (n + 1)`.
This definition gives the equivalence between the two, instead of the `R`-linear equivalence,
to bypass typeclass synthesis issues on complex `Module` goals. -/
noncomputable def powQuotPowSuccEquivMapMkPowSuccPow :
    ((I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R))) ≃
      Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n) :=
  powQuotPowSuccLinearEquivMapMkPowSuccPow I n

Похожие утверждения