English
The value of the trivialization map on a pair of σ-linear maps equals the image of the source and target trivializations under the σ-twisted continuous linear map.
Русский
Значение тривиализационной карты на паре σ-линейных отображений совпадает с образом соответствующих тривиализаций под σ-образованной линейной картой.
LaTeX
$$$\\operatorname{trivializationAt} (F_1 \\to SL[\\sigma] F_2) (\\lambda x. E_1 x \\to SL[\\sigma] E_2 x) x_0 x = \\langle x.1, \\; \\text{inCoordinates } F_1 E_1 F_2 E_2 x_0 x.1 x_0 x.1 x.2 \\rangle$$$
Lean4
theorem hom_trivializationAt_apply (x₀ : B) (x : TotalSpace (F₁ →SL[σ] F₂) (fun x ↦ E₁ x →SL[σ] E₂ x)) :
trivializationAt (F₁ →SL[σ] F₂) (fun x ↦ E₁ x →SL[σ] E₂ x) x₀ x =
⟨x.1, inCoordinates F₁ E₁ F₂ E₂ x₀ x.1 x₀ x.1 x.2⟩ :=
rfl
