English
There is a canonical diffeomorphism between the two models (I, M) and (I.transContinuousLinearEquiv e, M) given by the identity on M; its coordinate behavior is controlled by e as described above.
Русский
Существуют канонические диффеоморфизмы между двумя моделями (I, M) и (I.transContinuousLinearEquiv e, M), задаваемые единичной картой на M; их координатная поведении задаётся через e.
LaTeX
$$$\exists \mathrm{diff}: M \to M,\; \mathrm{diff} = \mathrm{id}_M \quad\text{and}\quad \mathrm{coord}_{I.transContinuousLinearEquiv e} = e \circ \mathrm{coord}_I$$$
Lean4
/-- The identity diffeomorphism between a manifold with model `I` and the same manifold
with model `I.trans_diffeomorph e`. -/
def toTransContinuousLinearEquiv (e : E ≃L[𝕜] F) : M ≃ₘ^n⟮I, I.transContinuousLinearEquiv e⟯ M
where
toEquiv := Equiv.refl M
contMDiff_toFun
x := by
refine contMDiffWithinAt_iff'.2 ⟨continuousWithinAt_id, ?_⟩
refine e.contDiff.contDiffWithinAt.congr_of_mem (fun y hy ↦ ?_) ?_
·
simp only [Equiv.coe_refl, id, (· ∘ ·), I.coe_extChartAt_transContinuousLinearEquiv,
(extChartAt I x).right_inv hy.1]
· exact ⟨(extChartAt I x).map_source (mem_extChartAt_source x), trivial, by simp only [mfld_simps]⟩
contMDiff_invFun
x := by
refine contMDiffWithinAt_iff'.2 ⟨continuousWithinAt_id, ?_⟩
refine e.symm.contDiff.contDiffWithinAt.congr_of_mem (fun y hy => ?_) ?_
· simp only [mem_inter_iff, I.extChartAt_transContinuousLinearEquiv_target] at hy
simp only [Equiv.coe_refl, Equiv.refl_symm, id, (· ∘ ·), I.coe_extChartAt_transContinuousLinearEquiv_symm,
(extChartAt I x).right_inv hy.1]
exact
⟨(extChartAt _ x).map_source (mem_extChartAt_source x), trivial, by
simp only [e.symm_apply_apply, Equiv.refl_symm, Equiv.coe_refl, mfld_simps]⟩
