English
For linear trivializations e1, e1' of F1 over B and e2, e2' of F2 over B, the coordinate change on the product trivialization equals the product map of the coordinate changes on each factor, at a base point b where both base sets hold.
Русский
Для линейных тривиализаций e1, e1' для F1 и e2, e2' для F2 над B координатное изменение на произведённой тривиализации равно произведению координатных изменений на каждом факторе, в точке b, где оба основания заданы.
LaTeX
$$$ (e_1 \\times e_2).coordChangeL 𝕜 (e_1' \\times e_2') b = (e_1.coordChangeL 𝕜 e_1' b) \\;\\mathrm{prodMap} \\; (e_2.coordChangeL 𝕜 e_2' b) $$$
Lean4
@[simp]
theorem coordChangeL_prod [e₁.IsLinear 𝕜] [e₁'.IsLinear 𝕜] [e₂.IsLinear 𝕜] [e₂'.IsLinear 𝕜] ⦃b⦄
(hb : (b ∈ e₁.baseSet ∧ b ∈ e₂.baseSet) ∧ b ∈ e₁'.baseSet ∧ b ∈ e₂'.baseSet) :
((e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b : F₁ × F₂ →L[𝕜] F₁ × F₂) =
(e₁.coordChangeL 𝕜 e₁' b : F₁ →L[𝕜] F₁).prodMap (e₂.coordChangeL 𝕜 e₂' b) :=
by
rw [ContinuousLinearMap.ext_iff, ContinuousLinearMap.coe_prodMap']
rintro ⟨v₁, v₂⟩
change
(e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b (v₁, v₂) = (e₁.coordChangeL 𝕜 e₁' b v₁, e₂.coordChangeL 𝕜 e₂' b v₂)
rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply']
exacts [rfl, hb, ⟨hb.1.2, hb.2.2⟩, ⟨hb.1.1, hb.2.1⟩]
