pullback — Mathlib

English

There is a fiber bundle structure on the pullback of a bundle along a map, with a canonical atlas obtained by pulling back trivializations.

Русский

Существует структура фибрового расслоения для pullback вдоль отображения; канонический атлас получается вытягиванием тривиализаций.

LaTeX

$$$\mathrm{FiberBundle}.\mathrm{pullback}(F,E,f)$$$

Lean4

@[simps]
noncomputable instance pullback [∀ x, TopologicalSpace (E x)] [FiberBundle F E] (f : K) :
    FiberBundle F ((f : B' → B) *ᵖ E)
    where
  totalSpaceMk_isInducing'
    x :=
    (totalSpaceMk_isInducing F E (f x)).of_comp (Pullback.continuous_totalSpaceMk F E) (Pullback.continuous_lift F E f)
  trivializationAtlas' := {ef | ∃ (e : Trivialization F (π F E)) (_ : MemTrivializationAtlas e), ef = e.pullback f}
  trivializationAt' x := (trivializationAt F E (f x)).pullback f
  mem_baseSet_trivializationAt' x := mem_baseSet_trivializationAt F E (f x)
  trivialization_mem_atlas' x := ⟨trivializationAt F E (f x), inferInstance, rfl⟩

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