Linear projection for subsets of indices.

Stream: Is there code for X?

[Peter Nelson]

Is there API for the following natural linear maps? exact? finds nothing of the appropriate type.

import Mathlib.LinearAlgebra.pi

variable {α 𝔽 : Type _} [Field 𝔽]

-- forget all entries outside s
def drop_entries (s : Set α) : (α → 𝔽) →ₗ[𝔽] (s → 𝔽) where
  toFun v x := v x
  map_add' := fun _ _ ↦ by ext; simp
  map_smul' := fun _ _ ↦ by ext; simp

-- forget all entries outside s
def drop_entries' (s t : Set α) (hst : s ⊆ t) : (t → 𝔽) →ₗ[𝔽] (s → 𝔽) where
  toFun v x := v ⟨x, hst x.prop⟩
  map_add' := fun _ _ ↦ by ext; simp
  map_smul' := fun _ _ ↦ by ext; simp

[Heather Macbeth]

@Peter Nelson I think you can combine docs#LinearMap.funLeft with docs#Subtype.val

[Eric Wieser]

Or docs#Set.inclusion for drop_entries'