English
The collection of fiberwise linear transition maps between trivializations forms a groupoid where morphisms are C^n-compatible coordinate changes.
Русский
Группа переходов по тривиализациям образует групоид с переходами гладкости C^n.
LaTeX
$$$$\\text{HasGroupoid }(\\text{TotalSpace }F E)(\\text{contMDiffFiberwiseLinear } B F IB n)$$$$
Lean4
/-- For a `C^n` vector bundle `E` over `B` with fiber modelled on `F`, the change-of-co-ordinates
between two trivializations `e`, `e'` for `E`, considered as charts to `B × F`, is `C^n` and
fiberwise linear. -/
instance hasGroupoid : HasGroupoid (TotalSpace F E) (contMDiffFiberwiseLinear B F IB n) where
compatible := by
rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩
haveI : MemTrivializationAtlas e := ⟨he⟩
haveI : MemTrivializationAtlas e' := ⟨he'⟩
rw [mem_contMDiffFiberwiseLinear_iff]
refine
⟨_, _, e.open_baseSet.inter e'.open_baseSet, contMDiffOn_coordChangeL e e', contMDiffOn_symm_coordChangeL e e',
?_⟩
refine OpenPartialHomeomorph.eqOnSourceSetoid.symm ⟨?_, ?_⟩
·
simp only [FiberwiseLinear.openPartialHomeomorph, trans_toPartialEquiv, symm_toPartialEquiv,
e.symm_trans_source_eq e']
· rintro ⟨b, v⟩ hb
exact (e.apply_symm_apply_eq_coordChangeL e' hb.1 v).symm
