English
The source of the σ-twisted trivialization equals the preimage under projection of the base base sets of the two component trivializations.
Русский
Исходное пространство σ-сложно(t) тривиализации совпадает с прообразом по проекции пересечения базовых множеств компонент тривиализаций.
LaTeX
$$$\\big( \\operatorname{trivializationAt} (F_1 \\to SL[\\sigma] F_2) (\\lambda x. E_1 x \\to SL[\\sigma] E_2 x) x_0 \\big).\\text{source} = \\pi (F_1 \\to SL[\\sigma] F_2)(\\lambda x \\mapsto E_1 x \\to SL[\\sigma] E_2 x) ^{-1}'\\big((\\operatorname{trivializationAt} F_1 E_1 x_0).\\text{baseSet} \\cap (\\operatorname{trivializationAt} F_2 E_2 x_0).\\text{baseSet}\\big). $$$
Lean4
@[simp, mfld_simps]
theorem hom_trivializationAt_source (x₀ : B) :
(trivializationAt (F₁ →SL[σ] F₂) (fun x ↦ E₁ x →SL[σ] E₂ x) x₀).source =
π (F₁ →SL[σ] F₂)(fun x ↦ E₁ x →SL[σ] E₂ x) ⁻¹'
((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet) :=
rfl
