equiv_symm — Mathlib

English

If p is equivalent to 0 (the bottom submodule), then the quotient by p is canonically isomorphic to M itself.

Русский

Если p эквивалентно нулю, то фактор‑модуль M/ p канонически изоморфен самому M.

LaTeX

$$$$ \\text{quotEquivOfEqBot} : (M / p) \\cong M \\quad (\\text{when } p = 0). $$$$

Lean4

@[simp]
theorem equiv_symm {R M N : Type*} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    (P : Submodule R M) (Q : Submodule R N) (f : M ≃ₗ[R] N) (hf : P.map f = Q) :
    (Quotient.equiv P Q f hf).symm = Quotient.equiv Q P f.symm ((Submodule.map_symm_eq_iff f).mpr hf) :=
  rfl

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