English
The supported preimage under a map f is contained in the comap of the supported on the target.
Русский
Предобраз поддерживаемого подмодуля относительно отображения f содержится в обратном отображении на целевой модуль.
LaTeX
$$$\mathrm{supported}(M,R, f^{-1}'s) \le \mathrm{comap}(\mathrm{lmapDomain}(M,R,f), \mathrm{supported}(M,R, s))$$$
Lean4
/-- Interpret `Finsupp.restrictSupportEquiv` as a linear equivalence between
`supported M R s` and `s →₀ M`. -/
@[simps!]
def supportedEquivFinsupp (s : Set α) : supported M R s ≃ₗ[R] s →₀ M :=
by
let F : supported M R s ≃ (s →₀ M) := restrictSupportEquiv s M
refine F.toLinearEquiv ?_
have :
(F : supported M R s → ↥s →₀ M) =
(lsubtypeDomain s : (α →₀ M) →ₗ[R] s →₀ M).comp (Submodule.subtype (supported M R s)) :=
rfl
rw [this]
exact LinearMap.isLinear _
