map_equiv_eq_comap_symm — Mathlib

English

Let e be a linear equivalence and K a submodule; the equality K.map e = K.comap e.symm holds as above.

Русский

Пусть e — линейное эквивалентное отображение, и K — подмодуль; равенство K.map e = K.comap e.symm выполняется согласно вышеописанному соотношению.

LaTeX

$$$ K.map e = K.comap e.symm $$$

Lean4

theorem map_equiv_eq_comap_symm (e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R M) :
    K.map (e : M →ₛₗ[τ₁₂] M₂) = K.comap (e.symm : M₂ →ₛₗ[τ₂₁] M) :=
  Submodule.ext fun _ => by rw [mem_map_equiv, mem_comap, LinearEquiv.coe_coe]

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