coordChange — Mathlib

English

Coordinate change in the fiber induced by a pair of trivializations is the fiberwise map x ↦ y given by applying the second trivialization to the inverse image of the first.

Русский

Переход координат в волокне, индуцированный парой тривиализаций, есть волокнозависимая отображение.

LaTeX

$$$\\text{coordChange}(e_1,e_2,b):F\\to F$ defined by $x \\mapsto ((e_2 \\lvert e_1) (b,x)).2$$$

Lean4

/-- Coordinate transformation in the fiber induced by a pair of bundle trivializations. See also
`Trivialization.coordChangeHomeomorph` for a version bundled as `F ≃ₜ F`. -/
def coordChange (e₁ e₂ : Trivialization F proj) (b : B) (x : F) : F :=
  (e₂ <| e₁.toOpenPartialHomeomorph.symm (b, x)).2

Похожие утверждения