English
Define a StructureGroupoid on B × F whose morphisms are local homeomorphisms that are bi-C^n and fiberwise linear, and which induce the identity on the base B. The local charts come from fiberwise linear maps; the composition is defined by fiberwise composition.
Русский
Определяем группу структур на B × F, члены которой – локальные гомоморфизмы, двукратно дифференцируемые и линейные по волокну, которые оставляют базис B неизменным; переходы осуществляются через композицию по волокнам.
LaTeX
$$$\\mathcal{G} = \\{\\text{locally fiberwise bi-}C^n\\text{ diffeos with base }B\\}$, with composition as fiberwise composition giving a groupoid structure.$$
Lean4
/-- For `B` a manifold and `F` a normed space, the groupoid on `B × F` consisting of local
homeomorphisms which are bi-`C^n` and fiberwise linear, and induce the identity on `B`.
When a (topological) vector bundle is `C^n`, then the composition of charts associated
to the vector bundle belong to this groupoid. -/
def contMDiffFiberwiseLinear (n : WithTop ℕ∞) : StructureGroupoid (B × F)
where
members :=
⋃ (φ : B → F ≃L[𝕜] F) (U : Set B) (hU : IsOpen U) (hφ :
ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => φ x : B → F →L[𝕜] F) U) (h2φ :
ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => (φ x).symm : B → F →L[𝕜] F) U),
{e | e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU hφ.continuousOn h2φ.continuousOn)}
trans' := by
simp only [mem_aux]
rintro e e' ⟨φ, U, hU, hφ, h2φ, heφ⟩ ⟨φ', U', hU', hφ', h2φ', heφ'⟩
refine
⟨fun b => (φ b).trans (φ' b), _, hU.inter hU', ?_, ?_,
Setoid.trans (OpenPartialHomeomorph.EqOnSource.trans' heφ heφ') ⟨?_, ?_⟩⟩
· change
ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x : B => (φ' x).toContinuousLinearMap ∘L (φ x).toContinuousLinearMap)
(U ∩ U')
exact (hφ'.mono inter_subset_right).clm_comp (hφ.mono inter_subset_left)
· change
ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n
(fun x : B => (φ x).symm.toContinuousLinearMap ∘L (φ' x).symm.toContinuousLinearMap) (U ∩ U')
exact (h2φ.mono inter_subset_left).clm_comp (h2φ'.mono inter_subset_right)
· apply FiberwiseLinear.source_trans_openPartialHomeomorph
· rintro ⟨b, v⟩ -; apply FiberwiseLinear.trans_openPartialHomeomorph_apply
symm'
e := by
simp only [mem_aux]
rintro ⟨φ, U, hU, hφ, h2φ, heφ⟩
refine ⟨fun b => (φ b).symm, U, hU, h2φ, ?_, OpenPartialHomeomorph.EqOnSource.symm' heφ⟩
simp_rw [ContinuousLinearEquiv.symm_symm]
exact hφ
id_mem' := by
simp_rw [mem_aux]
refine
⟨fun _ ↦ ContinuousLinearEquiv.refl 𝕜 F, univ, isOpen_univ, contMDiffOn_const, contMDiffOn_const,
⟨?_, fun b _hb ↦ rfl⟩⟩
simp only [FiberwiseLinear.openPartialHomeomorph, OpenPartialHomeomorph.refl_partialEquiv, PartialEquiv.refl_source,
univ_prod_univ]
locality' := by
-- the hard work has been extracted to `locality_aux₁` and `locality_aux₂`
simp only [mem_aux]
intro e he
obtain ⟨U, hU, h⟩ := ContMDiffFiberwiseLinear.locality_aux₁ n e he
exact ContMDiffFiberwiseLinear.locality_aux₂ n e U hU h
mem_of_eqOnSource' := by
simp only [mem_aux]
rintro e e' ⟨φ, U, hU, hφ, h2φ, heφ⟩ hee'
exact ⟨φ, U, hU, hφ, h2φ, Setoid.trans hee' heφ⟩
