compatibleMaps — Mathlib

English

Let e be a linear equivalence M ≃ M₂. Then K.comap e = K.map e.symm.

Русский

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

LaTeX

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

Lean4

/-- Given modules `M`, `M₂` over a commutative ring, together with submodules `p ⊆ M`, `q ⊆ M₂`,
the set of maps $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \}$ is a submodule of `Hom(M, M₂)`. -/
def compatibleMaps : Submodule R (N →ₗ[R] N₂)
    where
  carrier := {fₗ | pₗ ≤ comap fₗ qₗ}
  zero_mem' := by simp
  add_mem' {f₁ f₂} h₁
    h₂ := by
    apply le_trans _ (inf_comap_le_comap_add qₗ f₁ f₂)
    rw [le_inf_iff]
    exact ⟨h₁, h₂⟩
  smul_mem' c fₗ
    h := by
    dsimp at h
    exact le_trans h (comap_le_comap_smul qₗ fₗ c)

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