comapSubtypeEquivOfLe — Mathlib

English

Let e be a linear equivalence M ≃ M₂. Then for any submodule K of M, the image under e equals the comap under e.symm.

Русский

Пусть e — линейное эквивалентное отображение M ≃ M₂. Тогда для любого подмодуля K ⊆ M сохраняется равенство: K.map e = K.comap e.symm.

LaTeX

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

Lean4

/-- If `s ≤ t`, then we can view `s` as a submodule of `t` by taking the comap
of `t.subtype`. -/
@[simps apply_coe symm_apply]
def comapSubtypeEquivOfLe {p q : Submodule R M} (hpq : p ≤ q) : comap q.subtype p ≃ₗ[R] p
    where
  toFun x := ⟨x, x.2⟩
  invFun x := ⟨⟨x, hpq x.2⟩, x.2⟩
  left_inv x := by simp only [SetLike.eta]
  right_inv x := by simp only [SetLike.eta]
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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