Upgrade Lean and mathlib

leanpkg.toml

@@ -5,4 +5,4 @@ lean_version = "leanprover-community/lean:3.50.3"
 path = "src"
 
 [dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "d1723c047a091ae3fca0af8aeab1743e1a898611"}
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "9dba31df156d9d65b9d78db449542ca73d147c68"}

src/demos/category_theory.lean

@@ -1,5 +1,5 @@
 import category_theory.category.basic
-import category_theory.functor
+import category_theory.functor.basic
 
 import algebra.category.Group.images
 import algebra.category.Group.colimits
@@ -11,7 +11,7 @@ import category_theory.abelian.basic
 import category_theory.limits.shapes.finite_limits
 
 import topology.instances.real
-import topology.category.Top
+import topology.category.Top.limits
 import topology.category.UniformSpace
 
 

src/demos/linalg.lean

@@ -1,4 +1,4 @@
-import algebra.module
+import algebra.module.basic
 import analysis.inner_product_space.basic
 import data.matrix.notation
 import data.matrix.dmatrix
@@ -20,7 +20,7 @@
 not necessarily a field.
 -/
 
 #print module
 -- class module (R : Type u) (M : Type v) [semiring R] [add_comm_monoid M]
 -- extends distrib_mul_action R M := ...
 
@@ -29,12 +29,12 @@
 then a module structure over `R` on `M` has a scalar multiplication `•` (`has_smul.smul`),
 which satisfies the following identities:
 -/
 #check add_smul -- ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x
 #check smul_add -- ∀ (r : R) (x y : M), r • (x + y) = r • x + r • y
 #check mul_smul -- ∀ (r s : R) (x : M), (r * s) • x = r • (s • x)
 #check one_smul -- ∀ (x : M), 1 • x = x
 #check zero_smul -- ∀ (x : M), 0 • x = 0
 #check smul_zero -- ∀ (r : R), r • 0 = 0
 /-
 These equations define modules (and vector spaces).
 -/
@@ -213,14 +213,14 @@
 Like vectors in `n → R`, matrices are typically indexed over `fin k`.
 To define a matrix, you map the indexes to the entry:
 -/
-def example_matrix : matrix (fin 2) (fin 3) ℤ := λ i j, i + j
+def example_matrix : matrix (fin 2) (fin 3) ℤ := matrix.of (λ i j, (↑i + ↑j : ℤ))
 #eval example_matrix 1 2
 
-/- Like vectors, we can use `![...]` notation to define matrices: -/
+/- Simiilarly to vectors, we can use `!![...]` notation to define matrices: -/
 def other_example_matrix : matrix (fin 3) (fin 2) ℤ :=
-![![0, 1],
-  ![1, 2],
-  ![2, 3]]
+!![0, 1;
+   1, 2;
+   2, 3]
 
 /- We have the 0 matrix and the sum of two matrices: -/
 example (i j) : (0 : matrix m n R) i j = 0 := dmatrix.zero_apply i j
@@ -262,7 +262,7 @@
 -/
 variables [decidable_eq m] [decidable_eq n]
 variables (v : basis m R M) (w : basis n R N)
-#check linear_map.to_matrix v w -- (M →ₗ[R] N) ≈ₗ[R] matrix n m R
+#check linear_map.to_matrix v w -- (M →ₗ[R] N) ≃ₗ[R] matrix n m R
 
 /-
 Invertible (i.e. nonsingular) matrices have an inverse operation denoted by `⁻¹`.

src/exercises_sources/friday/analysis.lean

@@ -14,7 +14,7 @@ namespace lftcm
 noncomputable theory
 
 open real
-open_locale topological_space filter classical real
+open_locale topology filter classical real
 
 /-!
 # Derivatives

src/exercises_sources/friday/manifolds.lean

@@ -457,13 +457,13 @@ 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ℝ) :=
+/- Type-class inference can construct the smooth manifold structure on the tangent bundle. -/
+example : smooth_manifold_with_corners (𝓡1.prod 𝓡1) (tangent_bundle 𝓡1 myℝ) :=
 sorry
 
 /-
@@ -472,7 +472,13 @@ 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

src/exercises_sources/friday/topology.lean

@@ -1,6 +1,6 @@
 import topology.metric_space.basic
 
-open_locale classical filter topological_space
+open_locale classical filter topology
 
 namespace lftcm
 open filter set
@@ -53,7 +53,7 @@
 The filter axiom are also available as standalone lemmas where the filter argument is implicit
 Compare
 -/
 #check @filter.sets_of_superset
 #check @mem_of_superset
 
 -- And analogously:

src/exercises_sources/thursday/category_theory/exercise2.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 /-!
 Let's show that taking polynomials over a ring is functor `Ring ⥤ Ring`.
@@ -12,10 +12,10 @@
 * use `polynomial.map_ring_hom`
 -/
 
 def Ring.polynomial : Ring ⥤ Ring :=
 sorry
 
 def CommRing.polynomial : CommRing ⥤ CommRing :=
 sorry
 
 open category_theory

src/exercises_sources/thursday/category_theory/exercise4.lean

@@ -1,4 +1,4 @@
-import algebra.category.Ring
+import algebra.category.Ring.basic
 import category_theory.yoneda
 import data.polynomial.algebra_map
 

src/exercises_sources/thursday/groups_rings_fields.lean

@@ -2,6 +2,7 @@ import linear_algebra.finite_dimensional
 import ring_theory.algebraic
 import data.zmod.basic
 import data.real.basic
+import data.nat.choose.dvd
 import tactic
 
 /-!

src/exercises_sources/thursday/linear_algebra.lean

@@ -1,7 +1,6 @@
 import analysis.inner_product_space.basic
 import data.matrix.notation
 import linear_algebra.bilinear_form
-import linear_algebra.matrix
 import tactic
 
 universes u v
@@ -134,7 +133,7 @@ Hints:
   * Use the `simp` tactic to simplify `(x + y) i` to `x i + y i` and `(s • x) i` to `s * x i`.
   * To deal with equalities containing many `+` and `*` symbols, use the `ring` tactic.
 -/
-def A : matrix (fin 2) (fin 2) R := ![![1, 0], ![-2, 1]]
+def A : matrix (fin 2) (fin 2) R := !![1, 0; -2, 1]
 def your_bilin_form : bilin_form R (fin 2 → R) :=
 sorry
 
@@ -166,10 +165,13 @@ Hints:
 * Try the lemmas `finset.sum_nonneg`, `finset.sum_eq_zero_iff_of_nonneg`,
   `mul_self_nonneg` and `mul_self_eq_zero`.
 -/
-noncomputable instance : inner_product_space ℝ (n → ℝ) :=
-inner_product_space.of_core
+noncomputable instance : normed_add_comm_group (n → ℝ):=
+@inner_product_space.of_core.to_normed_add_comm_group ℝ (n → ℝ) _ _ _
 sorry
 
+noncomputable instance : inner_product_space ℝ (n → ℝ) :=
+inner_product_space.of_core _
+
 end pi
 
 end exercise3

src/exercises_sources/tuesday/numbers.lean

@@ -1,7 +1,7 @@
 import tactic
 import data.real.basic
 import data.int.gcd
-import number_theory.padics
+import number_theory.padics.padic_numbers
 import data.nat.prime_norm_num
 
 /-!

src/exercises_sources/tuesday/sets.lean

@@ -1,4 +1,5 @@
 import data.set.basic data.set.lattice data.nat.parity
+import data.nat.prime
 import tactic.linarith
 
 open set nat function

src/for_mathlib/manifolds.lean

@@ -21,7 +21,7 @@ include hp
 lemma pi_Lp.norm_coord_le_norm (x : pi_Lp p α) (i : ι) : ‖x i‖ ≤ ‖x‖ :=
 begin
   unfreezingI { rcases p.trichotomy with (rfl | rfl | h) },
-  { exact false.elim (lt_irrefl _ (ennreal.zero_lt_one.trans_le hp.out)) },
+  { exact false.elim (lt_irrefl _ (zero_lt_one.trans_le hp.out)) },
   { rw pi_Lp.norm_eq_csupr,
     exact le_cSup (finite_range _).bdd_above (mem_range_self _) },
   { calc
@@ -74,7 +74,7 @@ begin
     begin
       refine (F i).mk_continuous 1 (λ x, _),
       unfreezingI { rcases p.trichotomy with (rfl | rfl | h) },
-      { exact false.elim (lt_irrefl _ (ennreal.zero_lt_one.trans_le hp.out)) },
+      { exact false.elim (lt_irrefl _ (zero_lt_one.trans_le hp.out)) },
       { haveI : nonempty ι := ⟨i⟩,
         simp only [pi_Lp.norm_eq_csupr, linear_map.coe_mk, one_mul],
         refine cSup_le (range_nonempty _) _,

src/hints/category_theory/exercise2/hint1.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 
@@ -10,11 +10,11 @@
 { obj := sorry,
   map := sorry, }
 
 def CommRing.polynomial : CommRing ⥤ CommRing :=
 sorry
 
 open category_theory
 
 def commutes :
   (forget₂ CommRing Ring) ⋙ Ring.polynomial ≅ CommRing.polynomial ⋙ (forget₂ CommRing Ring) :=
 sorry

src/hints/category_theory/exercise2/hint2.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 
@@ -18,7 +18,7 @@
   end,
   map := sorry, }
 
 def CommRing.polynomial : CommRing ⥤ CommRing :=
 sorry
 
 open category_theory

src/hints/category_theory/exercise2/hint3.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 
@@ -32,11 +32,11 @@
     -- The next hint file walks you through doing this.
   end, }
 
 def CommRing.polynomial : CommRing ⥤ CommRing :=
 sorry
 
 open category_theory
 
 def commutes :
   (forget₂ CommRing Ring) ⋙ Ring.polynomial ≅ CommRing.polynomial ⋙ (forget₂ CommRing Ring) :=
 sorry

src/hints/category_theory/exercise2/hint4.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 

src/hints/category_theory/exercise2/hint5.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 
@@ -9,6 +9,6 @@
 { obj := λ R, Ring.of (polynomial R),
   map := λ R S f, polynomial.map_ring_hom f }
 
 def CommRing.polynomial : CommRing ⥤ CommRing :=
 -- Let's just copy and paste the construction above, replace `Ring.of` with `CommRing.of`!
 sorry

src/hints/category_theory/exercise2/hint6.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 

src/hints/category_theory/exercise2/hint7.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 noncomputable theory -- the default implementation of polynomials is noncomputable
 

src/hints/category_theory/exercise4/hint1.lean

@@ -1,4 +1,4 @@
-import algebra.category.Ring
+import algebra.category.Ring.basic
 import category_theory.yoneda
 import data.polynomial.algebra_map
 

src/hints/category_theory/exercise4/hint2.lean

@@ -1,4 +1,4 @@
-import algebra.category.Ring
+import algebra.category.Ring.basic
 import category_theory.yoneda
 import data.polynomial.algebra_map
 

src/hints/category_theory/exercise4/hint3.lean

@@ -1,4 +1,4 @@
-import algebra.category.Ring
+import algebra.category.Ring.basic
 import category_theory.yoneda
 import data.polynomial.algebra_map
 

src/hints/category_theory/exercise4/hint4.lean

@@ -1,4 +1,4 @@
-import algebra.category.Ring
+import algebra.category.Ring.basic
 import category_theory.yoneda
 import data.polynomial.algebra_map
 

src/solutions/friday/manifolds.lean

@@ -510,13 +510,13 @@ 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ℝ) :=
+/- Type-class inference can construct the smooth manifold structure on the tangent bundle. -/
+example : smooth_manifold_with_corners (𝓡1.prod 𝓡1) (tangent_bundle 𝓡1 myℝ) :=
 -- sorry
 by apply_instance
 -- sorry
@@ -527,7 +527,15 @@ 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
+by apply_instance
+-- 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
@@ -559,8 +567,11 @@ begin
   let p : tangent_bundle 𝓡1 myℝ := ⟨(4 : ℝ), 0⟩,
   let F := chart_at (model_prod ℝ ℝ) p,
   have A : ¬ ((4 : ℝ) < 1), by norm_num,
-  have S : F.source = univ, by simp [F, chart_at, A, @local_homeomorph.refl_source ℝ _],
-  have T : F.target = univ, by simp [F, chart_at, A, @local_homeomorph.refl_target ℝ _],
+  have S : F.source = univ,
+  by simp [F, fiber_bundle.charted_space_chart_at, chart_at, A, local_homeomorph.refl_source ℝ],
+  have T : F.target = univ,
+  by simp [F, fiber_bundle.charted_space_chart_at, chart_at, A, local_homeomorph.refl_source ℝ,
+    local_homeomorph.refl_target ℝ],
   exact F.to_homeomorph_of_source_eq_univ_target_eq_univ S T,
   -- sorry
 end
@@ -636,13 +647,14 @@ begin
   -- are left with a statement speaking of derivatives of real functions, without any manifold code left.
   -- sorry
   have : ¬ ((3 : ℝ) < 1), by norm_num,
-  simp only [chart_at, this, mem_Ioo, if_false, and_false],
-  dsimp [tangent_bundle_core, basic_smooth_vector_bundle_core.chart, bundle.total_space.proj],
+  simp only [chart_at, fiber_bundle.charted_space_chart_at, this, mem_Ioo, if_false, and_false,
+    local_homeomorph.trans_apply, tangent_bundle.trivialization_at_apply, fderiv_within_univ]
+    with mfld_simps,
   split_ifs,
-  { simp only [chart_at, h, my_first_local_homeo, if_true, fderiv_within_univ, mem_Ioo, fderiv_id',
-      continuous_linear_map.coe_id', continuous_linear_map.neg_apply, fderiv_neg] with mfld_simps },
-  { simp only [chart_at, h, fderiv_within_univ, mem_Ioo, if_false, @local_homeomorph.refl_symm ℝ,
-      fderiv_id, continuous_linear_map.coe_id'] with mfld_simps }
+  { simp only [my_first_local_homeo, fderiv_neg, fderiv_id',
+      continuous_linear_map.coe_id', continuous_linear_map.neg_apply] with mfld_simps },
+  { simp only [@local_homeomorph.refl_symm ℝ, fderiv_id,
+      continuous_linear_map.coe_id'] with mfld_simps }
   -- sorry
 end
 
@@ -946,7 +958,7 @@ def G : tangent_bundle (𝓡∂ 1) (Icc (0 : ℝ) 1) → (Icc (0 : ℝ) 1) × 
 lemma continuous_G : continuous G :=
 begin
   -- sorry
-  apply continuous.prod_mk (tangent_bundle_proj_continuous _ _),
+  refine (continuous_proj (euclidean_space ℝ (fin 1)) (tangent_space (𝓡∂ 1))).prod_mk _,
   refine continuous_snd.comp _,
   apply continuous.comp (homeomorph.continuous _),
   apply cont_mdiff.continuous_tangent_map cont_mdiff_g le_top,

src/solutions/friday/topology.lean

@@ -1,6 +1,6 @@
 import topology.metric_space.basic
 
-open_locale classical filter topological_space
+open_locale classical filter topology
 
 namespace lftcm
 open filter set
@@ -94,7 +94,7 @@
 The filter axiom are also available as standalone lemmas where the filter argument is implicit
 Compare
 -/
 #check @filter.sets_of_superset
 #check @mem_of_superset
 
 -- And analogously:

src/solutions/thursday/category_theory/exercise2.lean

@@ -1,5 +1,5 @@
 import algebra.category.Ring.basic
-import data.polynomial
+import data.polynomial.lifts
 
 /-!
 Let's show that taking polynomials over a ring is functor `Ring ⥤ Ring`.

src/solutions/thursday/category_theory/exercise4.lean

@@ -1,4 +1,4 @@
-import algebra.category.Ring
+import algebra.category.Ring.basic
 import category_theory.yoneda
 import data.polynomial.algebra_map
 
@@ -24,7 +24,7 @@
 ring homomorphism from `ℤ` into any commutative ring.
 -/
 example (R : CommRing) : ℤ →+* R :=
 by library_search
 
 /-!
 Also useful may be the functions

src/solutions/thursday/groups_rings_fields.lean

@@ -2,6 +2,7 @@ import linear_algebra.finite_dimensional
 import ring_theory.algebraic
 import data.zmod.basic
 import data.real.basic
+import data.nat.choose.dvd
 import tactic
 
 /-!
@@ -292,8 +293,7 @@ begin
   { intros i hi hi0,
     convert mul_zero _,
     rw char_p.cast_eq_zero_iff K p,
-    apply nat.prime.dvd_choose_self _ _ (fact.out p.prime),
-    { rwa pos_iff_ne_zero },
+    apply nat.prime.dvd_choose_self (fact.out p.prime) hi0 _,
     { simpa using hi } },
   { intro h,
     simp only [le_zero_iff, mem_range, not_lt] at h,