From 119d99ec26075f6a748155ec481a6c861a4da467 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 6 Apr 2023 17:10:15 +0000 Subject: [PATCH] rebuild exercises --- src/exercises_sources/friday/manifolds.lean | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/exercises_sources/friday/manifolds.lean b/src/exercises_sources/friday/manifolds.lean index 68beaaf..881343d 100644 --- a/src/exercises_sources/friday/manifolds.lean +++ b/src/exercises_sources/friday/manifolds.lean @@ -457,13 +457,14 @@ be a smooth manifold. -/ -- the type `tangent_bundle 𝓡1 myℝ` makes sense #check tangent_bundle 𝓡1 myℝ -/- The tangent space above a point of `myℝ` is just a one-dimensional vector space (identified with `ℝ`). +/- The tangent space above a point of `myℝ` is just a one-dimensional vector space +(identified with `ℝ`). So, one can prescribe an element of the tangent bundle as a pair (more on this below) -/ example : tangent_bundle 𝓡1 myℝ := ⟨(4 : ℝ), 0⟩ /- Construct the smooth manifold structure on the tangent bundle. Hint: the answer is a one-liner, and this instance is not really needed. -/ -instance tangent_bundle_myℝ : smooth_manifold_with_corners (𝓡1.prod 𝓡1) (tangent_bundle 𝓡1 myℝ) := +example : smooth_manifold_with_corners (𝓡1.prod 𝓡1) (tangent_bundle 𝓡1 myℝ) := sorry /- @@ -472,7 +473,12 @@ NB: the model space for the tangent bundle to a product manifold or a tangent sp structures with model `ℝ × ℝ`, the identity one and the product one, which are not definitionally equal. And this would be bad. -/ -#check tangent_bundle.charted_space 𝓡1 myℝ +example : charted_space (model_prod ℝ ℝ) (tangent_bundle 𝓡1 myℝ) := +sorry +/- +The charts of any smooth vector bundle are characterized by `fiber_bundle.charted_space_chart_at` +-/ +#check @fiber_bundle.charted_space_chart_at /- A smooth map between manifolds induces a map between their tangent bundles. In `mathlib` this is called the `tangent_map` (you might instead know it as the "differential" or "pushforward" of the