Theorems · Definition · linear algebra

Submodule.compatibleMaps

{S : Type u_9} →
  {N : Type u_10} →
    {N₂ : Type u_11} →
      [inst : CommSemiring S] →
        [inst_1 : AddCommMonoid N] →
          [inst_2 : AddCommMonoid N₂] →
            [inst_3 : Module S N] → [inst_4 : Module S N₂] → Submodule S N → Submodule S N₂ → Submodule S (N →ₗ[S] N₂)

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₂).

Defined in

Mathlib.Algebra.Module.Submodule.Map

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModule