English
Given a set s ⊆ α, restrictSupportEquiv(s,M) is the canonical bijection between the finitely supported functions with support contained in s and finitely supported functions on s.
Русский
Пусть s ⊆ α. restrictSupportEquiv(s,M) есть каноническая биекция между функциями с конечной опорой, поддержка которых лежит в s, и функциями на s с конечной опорой.
LaTeX
$$$\\mathrm{restrictSupportEquiv}(s,M) : \\{ f : α →₀ M \\,|\\, \\uparrow f.support \\subseteq s \\} \\simeq (s →₀ M)$$$
Lean4
/-- Given an `AddCommMonoid M` and `s : Set α`, `restrictSupportEquiv s M` is the `Equiv`
between the subtype of finitely supported functions with support contained in `s` and
the type of finitely supported functions from `s`. -/
-- TODO: add [DecidablePred (· ∈ s)] as an assumption
@[simps apply]
def restrictSupportEquiv (s : Set α) (M : Type*) [AddCommMonoid M] : { f : α →₀ M // ↑f.support ⊆ s } ≃ (s →₀ M)
where
toFun f := subtypeDomain (· ∈ s) f.1
invFun
f :=
letI := Classical.decPred (· ∈ s);
⟨f.extendDomain, support_extendDomain_subset _⟩
left_inv
f :=
letI := Classical.decPred (· ∈ s);
Subtype.ext <| extendDomain_subtypeDomain f.1 f.prop
right_inv
_ :=
letI := Classical.decPred (· ∈ s);
subtypeDomain_extendDomain _
