English
The product of two trivializations e1 and e2 yields a trivialization for the product bundle.
Русский
Произведение двух тривиализаций e1 и e2 образует тривиализацию для произведения расслоений.
LaTeX
$$$\mathrm{prod}\;:\; \mathrm{Trivialization}(F_1\times F_2, \pi (F_1\times F_2)(E_1\times^b E_2))$$$
Lean4
/-- Given trivializations `e₁`, `e₂` for bundle types `E₁`, `E₂` over a base `B`, the induced
trivialization for the fiberwise product of `E₁` and `E₂`, whose base set is
`e₁.baseSet ∩ e₂.baseSet`. -/
@[simps!]
noncomputable def prod : Trivialization (F₁ × F₂) (π (F₁ × F₂)(E₁ ×ᵇ E₂))
where
toFun := Prod.toFun' e₁ e₂
invFun := Prod.invFun' e₁ e₂
source := π (F₁ × F₂)(E₁ ×ᵇ E₂) ⁻¹' (e₁.baseSet ∩ e₂.baseSet)
target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ
map_source' _ h := ⟨h, Set.mem_univ _⟩
map_target' _ h := h.1
left_inv' _ := Prod.left_inv
right_inv' _ := Prod.right_inv
open_source :=
by
convert (e₁.open_source.prod e₂.open_source).preimage (FiberBundle.Prod.isInducing_diag F₁ E₁ F₂ E₂).continuous
ext x
simp only [Trivialization.source_eq, mfld_simps]
open_target := (e₁.open_baseSet.inter e₂.open_baseSet).prod isOpen_univ
continuousOn_toFun := Prod.continuous_to_fun
continuousOn_invFun := Prod.continuous_inv_fun
baseSet := e₁.baseSet ∩ e₂.baseSet
open_baseSet := e₁.open_baseSet.inter e₂.open_baseSet
source_eq := rfl
target_eq := rfl
proj_toFun _ _ := rfl
