English
For any chart i, the base set of the tangent bundle core equals the source of i.
Русский
Для любой диаграммы i базовое множество ядра касательного расслоения равно области определения i.
LaTeX
$$$$ (tangentBundleCore I M).baseSet i = i.1.source $$$$
Lean4
/-- Let `M` be a `C^1` manifold with model `I` on `(E, H)`.
Then `tangentBundleCore I M` is the vector bundle core for the tangent bundle over `M`.
It is indexed by the atlas of `M`, with fiber `E` and its change of coordinates from the chart `i`
to the chart `j` at point `x : M` is the derivative of the composite
```
I.symm i.symm j I
E -----> H -----> M --> H --> E
```
within the set `range I ⊆ E` at `I (i x) : E`. -/
@[simps indexAt coordChange]
def tangentBundleCore : VectorBundleCore 𝕜 M E (atlas H M)
where
baseSet i := i.1.source
isOpen_baseSet i := i.1.open_source
indexAt := achart H
mem_baseSet_at := mem_chart_source H
coordChange i j x := fderivWithin 𝕜 (j.1.extend I ∘ (i.1.extend I).symm) (range I) (i.1.extend I x)
coordChange_self i x hx
v := by
rw [Filter.EventuallyEq.fderivWithin_eq, fderivWithin_id', ContinuousLinearMap.id_apply]
· exact I.uniqueDiffWithinAt_image
· filter_upwards [i.1.extend_target_mem_nhdsWithin hx] with y hy
exact (i.1.extend I).right_inv hy
· simp_rw [Function.comp_apply, i.1.extend_left_inv hx]
continuousOn_coordChange i
j := by
have : IsManifold I (0 + 1) M := by simpa
refine (contDiffOn_fderiv_coord_change (n := 0) i j).continuousOn.comp (i.1.continuousOn_extend.mono ?_) ?_
· rw [i.1.extend_source]; exact inter_subset_left
simp_rw [← i.1.extend_image_source_inter, mapsTo_image]
coordChange_comp := by
have : IsManifold I (0 + 1) M := by simpa
rintro i j k x ⟨⟨hxi, hxj⟩, hxk⟩ v
rw [fderivWithin_fderivWithin, Filter.EventuallyEq.fderivWithin_eq]
· have := i.1.extend_preimage_mem_nhds (I := I) hxi (j.1.extend_source_mem_nhds (I := I) hxj)
filter_upwards [nhdsWithin_le_nhds this] with y hy
simp_rw [Function.comp_apply, (j.1.extend I).left_inv hy]
· simp_rw [Function.comp_apply, i.1.extend_left_inv hxi, j.1.extend_left_inv hxj]
·
exact
(contDiffWithinAt_extend_coord_change' (subset_maximalAtlas k.2) (subset_maximalAtlas j.2) hxk
hxj).differentiableWithinAt
le_rfl
·
exact
(contDiffWithinAt_extend_coord_change' (subset_maximalAtlas j.2) (subset_maximalAtlas i.2) hxj
hxi).differentiableWithinAt
le_rfl
· intro x _; exact mem_range_self _
· exact I.uniqueDiffWithinAt_image
· rw [Function.comp_apply, i.1.extend_left_inv hxi]
