English
If σ: RingHom to field and the bundles are suitable, the induced pretrivialization continuousLinearMap σ e1 e2 is linear with respect to the second field.
Русский
Если σ: RingHom и расслоения удовлетворяют условиям, то индуцированная предтривиализация continuousLinearMap σ e1 e2 линейна по второй структуре поля.
LaTeX
$$$ (\\text{Pretrivialization.continuousLinearMap } σ e_1 e_2) \\text{ is linear in } 𝕜_2 $$$
Lean4
/-- Assume `eᵢ` and `eᵢ'` are trivializations of the bundles `Eᵢ` over base `B` with fiber `Fᵢ`
(`i ∈ {1,2}`), then `Pretrivialization.continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂'` is the
coordinate change function between the two induced (pre)trivializations
`Pretrivialization.continuousLinearMap σ e₁ e₂` and
`Pretrivialization.continuousLinearMap σ e₁' e₂'` of the bundle of continuous linear maps. -/
def continuousLinearMapCoordChange [e₁.IsLinear 𝕜₁] [e₁'.IsLinear 𝕜₁] [e₂.IsLinear 𝕜₂] [e₂'.IsLinear 𝕜₂] (b : B) :
(F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂ :=
((e₁'.coordChangeL 𝕜₁ e₁ b).symm.arrowCongrSL (e₂.coordChangeL 𝕜₂ e₂' b) : (F₁ →SL[σ] F₂) ≃L[𝕜₂] F₁ →SL[σ] F₂)
