English
The left inverse of lcomapDomain composed with mapDomain is comapDomain_mapDomain: lcomapDomain f hf is left-inverse of mapDomain f.
Русский
Левостороннее противолежащее от lcomapDomain по отношению к mapDomain даёт comapDomain_mapDomain: lcomapDomain f hf — левый обратимый к mapDomain f.
LaTeX
$$$\\text{LeftInverse}(lcomapDomain f hf, mapDomain f) = comapDomain_mapDomain f hf$$$
Lean4
/-- Given `f : α → β` and a proof `hf` that `f` is injective, `lcomapDomain f hf` is the linear map
sending `l : β →₀ M` to the finitely supported function from `α` to `M` given by composing
`l` with `f`.
This is the linear version of `Finsupp.comapDomain`. -/
@[simps]
def lcomapDomain (f : α → β) (hf : Function.Injective f) : (β →₀ M) →ₗ[R] α →₀ M
where
toFun l := Finsupp.comapDomain f l hf.injOn
map_add' x y := by ext; simp
map_smul' c x := by ext; simp
