quotOfListConsSMulTopEquivQuotSMulTopInner

English

There is a linear equivalence between M modulo (r :: rs) and QuotSMulTop r applied to M modulo rs.

Русский

Существует линейное эквивалентное отображение между M/(r :: rs) и QuotSMulTop r (M/(rs)).

LaTeX

$$$\\left(M \\Big\\slash (\\text{Ideal.ofList } (r :: rs) \\;\\top)\\right) \\cong_{R} \\; \\text{QuotSMulTop } r \\left(M \\Big/ (\\text{Ideal.ofList rs } \\top)\\right)$$$

Lean4

/-- The equivalence between M ⧸ (r₀, r₁, …, rₙ)M and (M ⧸ r₀M) ⧸ (r₁, …, rₙ) (M ⧸ r₀M). -/
def quotOfListConsSMulTopEquivQuotSMulTopInner :
    (M ⧸ (Ideal.ofList (r :: rs) • ⊤ : Submodule R M)) ≃ₗ[R]
      QuotSMulTop r M ⧸ (Ideal.ofList rs • ⊤ : Submodule R (QuotSMulTop r M)) :=
  quotEquivOfEq _ _ (Ideal.ofList_cons_smul r rs ⊤) ≪≫ₗ
      (quotientQuotientEquivQuotientSup (r • ⊤) (Ideal.ofList rs • ⊤)).symm ≪≫ₗ
    quotEquivOfEq _ _ (by rw [map_smul'', map_top, range_mkQ])

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