quotientQuotientEquivQuotientAux — Mathlib

English

Quotient-quotient equivalence respects the MK operation.

Русский

Эквивалентность квотирования сохраняется при повторном квотировании.

LaTeX

$$theorem quotientQuotientEquivQuotientAux_mk_mk (x : M) : quotientQuotientEquivQuotientAux S T h (Quotient.mk (Quotient.mk x)) = Quotient.mk x$$

Lean4

/-- The map from the third isomorphism theorem for modules: `(M / S) / (T / S) → M / T`. -/
def quotientQuotientEquivQuotientAux (h : S ≤ T) : (M ⧸ S) ⧸ T.map S.mkQ →ₗ[R] M ⧸ T :=
  liftQ _ (mapQ S T LinearMap.id h)
    (by
      rintro _ ⟨x, hx, rfl⟩
      rw [LinearMap.mem_ker, mkQ_apply, mapQ_apply]
      exact (Quotient.mk_eq_zero _).mpr hx)

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