English
Let e be a linear trivialization of a vector bundle. Then for every base point b in the base set and every vector y in the model fiber, applying the inverse fiber map to y followed by the fiber map returns y. In other words, the local trivialization provides a two-sided inverse between the local model space F and the fiber E_b on base-set points.
Русский
Пусть e — линейное тривиализация векторного расслоения. Тогда для каждого b, принадлежащего базовому множеству, и каждого вектора y в модельной клетке F применение инверсии вдоль волокна к y, затем линейного сопоставления вдоль волокна возвращает y. Иными словами, локальная тривиализация задаёт двусторонний обратный переход между локальной моделью F и волокном E_b на базовом множестве.
LaTeX
$$$\forall b \in e.baseSet,\; (e.linearMapAt\, R\, b) \circ (e.symm\u2090\u2060 R\, b) = \mathrm{id}_F.$$$
Lean4
theorem linearMapAt_symmₗ (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet) (y : F) :
e.linearMapAt R b (e.symmₗ R b y) = y :=
by
rw [e.linearMapAt_def_of_mem hb]
exact (e.linearEquivAt R b hb).right_inv y
