English
Let E1 and E2 be vector bundles over a base space B with a fixed ring homomorphism σ. The trivialization at x0 intertwining F1 →SL[σ] F2 and the corresponding E1 x →SL[σ] E2 x is equal to the σ-twisted composition of the base trivializations at x0.
Русский
Пусть E1 и E2 — векторные расслоения над основанием B и заданы σ-поперечные линейные отображения. Привилегированный тривиализационный отображатель в точке x0 соответствует σ-связанной карте между F1 и F2 и эквивалентной F1 x0 →SL[σ] E1 x0 и E2 x0; равенство междуса тривиализаций отражает композицию по σ.
LaTeX
$$$\\operatorname{trivializationAt} \\left(F_1 \\to SL[\\sigma] F_2\\right)\\left(\\lambda x. E_1 x \\to SL[\\sigma] E_2 x\\right) x_0 = \\left( \\operatorname{trivializationAt} F_1 E_1 x_0 \\right) \\mathrm{continuousLinearMap} \\sigma \\left( \\operatorname{trivializationAt} F_2 E_2 x_0 \\right).$$$
Lean4
theorem hom_trivializationAt (x₀ : B) :
trivializationAt (F₁ →SL[σ] F₂) (fun x ↦ E₁ x →SL[σ] E₂ x) x₀ =
(trivializationAt F₁ E₁ x₀).continuousLinearMap σ (trivializationAt F₂ E₂ x₀) :=
rfl
