English
There is a fiberwise linear inverse to the forward map, denoted by e.symmₗ, giving a linear map from F to E_b when b is in the base set; otherwise it is the zero map.
Русский
Существует линейный локальный обратный отображатель к линейному преобразованию из F в E_b; если b ∈ базовое множество, это линейное отображение, иначе нулевое.
LaTeX
$$e.symmₗ R b is a linear map F → E_b; if b ∈ e.baseSet then e.symmₗ R b (e.linearMapAt R b y) = y for all y ∈ E_b; otherwise e.symmₗ R b is the zero map.$$
Lean4
/-- A fiberwise linear inverse to `e`. -/
@[simps!]
protected def symmₗ (e : Pretrivialization F (π F E)) [e.IsLinear R] (b : B) : F →ₗ[R] E b :=
by
refine IsLinearMap.mk' (e.symm b) ?_
by_cases hb : b ∈ e.baseSet
·
exact
(((e.linear R hb).mk' _).inverse (e.symm b) (e.symm_apply_apply_mk hb) fun v ↦
congr_arg Prod.snd <| e.apply_mk_symm hb v).isLinear
· rw [e.coe_symm_of_notMem hb]
exact (0 : F →ₗ[R] E b).isLinear
