quotOfListConsSMulTopEquivQuotSMulTopOuter

English

Definition of the inner quotient equivalence between M and QuotSMulTop constructions.

Русский

Определение внутреннего эквивалентного отображения между конструкциями M и QuotSMulTop.

LaTeX

$$Definition of QuotSMulTopInner (informal description).$$

Lean4

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

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