orderIsoMapComap_symm_apply' — Mathlib

English

If p ≤ q are submodules, then comap q.subtype p ≃ₗ[R] p; i.e., p is canonically isomorphic to the comap of p along the inclusion q.subtype.

Русский

Если p ≤ q — подмодули, то comap q.subtype p ≃ p; то есть p канонически изоморфен через обратный образ вдоль вложения.

LaTeX

$$$ comap q.subtype p \\simeq p \\quad \\text{при } p \\le q $$$

Lean4

theorem orderIsoMapComap_symm_apply' (e : M ≃ₛₗ[τ₁₂] M₂) (p : Submodule R₂ M₂) :
    (orderIsoMapComap e).symm p = map e.symm p :=
  p.comap_equiv_eq_map_symm _

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