quotientQuotientEquivQuotientSup — Mathlib

English

If S ⊆ T ⊆ M are submodules, there is a canonical linear isomorphism between ((M/S) / (T.map S.mkQ)) and M/(S ⊔ T).

Русский

Пусть S ⊆ T ⊆ M — подмодули. Существует канонический линейный изоморфизм между ((M/S) / (T.map S.mkQ)) и M/(S ⊔ T).

LaTeX

$$$$((M/S) / (T.map S.mkQ)) \\cong_R M \\!/(S \\sqcup T)$$$$

Lean4

/-- Essentially the same equivalence as in the third isomorphism theorem,
except restated in terms of suprema/addition of submodules instead of `≤`. -/
def quotientQuotientEquivQuotientSup : ((M ⧸ S) ⧸ T.map S.mkQ) ≃ₗ[R] M ⧸ S ⊔ T :=
  quotEquivOfEq _ _ (by rw [map_sup, mkQ_map_self, bot_sup_eq]) ≪≫ₗ quotientQuotientEquivQuotient S (S ⊔ T) le_sup_left

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