Merge remote-tracking branch 'origin/master' into eric-wieser/exp-rat

This doesn't build, but the conflict markers are at least gone

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -496,13 +496,12 @@ noncomputable def sequence_of_cubes : ℕ → { i : ι // valley cs ((cs i).shif
 | 0     := let v := valley_unit_cube h      in ⟨mi h v, valley_mi⟩
 | (k+1) := let v := (sequence_of_cubes k).2 in ⟨mi h v, valley_mi⟩
 
-def decreasing_sequence (k : ℕ) : order_dual ℝ :=
-(cs (sequence_of_cubes h k).1).w
+def decreasing_sequence (k : ℕ) : ℝ := (cs (sequence_of_cubes h k).1).w
 
-lemma strict_mono_sequence_of_cubes : strict_mono $ decreasing_sequence h :=
-strict_mono_nat_of_lt_succ $
+lemma strict_anti_sequence_of_cubes : strict_anti $ decreasing_sequence h :=
+strict_anti_nat_of_succ_lt $ λ k,
 begin
-  intro k, let v := (sequence_of_cubes h k).2, dsimp only [decreasing_sequence, sequence_of_cubes],
+  let v := (sequence_of_cubes h k).2, dsimp only [decreasing_sequence, sequence_of_cubes],
   apply w_lt_w h v (mi_mem_bcubes : mi h v ∈ _),
 end
 
@@ -512,7 +511,7 @@ theorem not_correct : ¬correct cs :=
 begin
   intro h, apply (lt_omega_of_fintype ι).not_le,
   rw [omega, lift_id], fapply mk_le_of_injective, exact λ n, (sequence_of_cubes h n).1,
-  intros n m hnm, apply strict_mono.injective (strict_mono_sequence_of_cubes h),
+  intros n m hnm, apply (strict_anti_sequence_of_cubes h).injective,
   dsimp only [decreasing_sequence], rw hnm
 end
 

archive/imo/imo1972_b2.lean → archive/imo/imo1972_q5.lean

@@ -8,7 +8,7 @@ import data.real.basic
 import analysis.normed_space.basic
 
 /-!
-# IMO 1972 B2
+# IMO 1972 Q5
 
 Problem: `f` and `g` are real-valued functions defined on the real line. For all `x` and `y`,
 `f(x + y) + f(x - y) = 2f(x)g(y)`. `f` is not identically zero and `|f(x)| ≤ 1` for all `x`.
@@ -30,7 +30,6 @@ example (f g : ℝ → ℝ)
   (y : ℝ) :
   ∥g(y)∥ ≤ 1 :=
 begin
-  classical,
   set S := set.range (λ x, ∥f x∥),
   -- Introduce `k`, the supremum of `f`.
   let k : ℝ := Sup (S),
@@ -86,7 +85,7 @@ begin
 end
 
 
-/-- IMO 1972 B2
+/-- IMO 1972 Q5
 
 Problem: `f` and `g` are real-valued functions defined on the real line. For all `x` and `y`,
 `f(x + y) + f(x - y) = 2f(x)g(y)`. `f` is not identically zero and `|f(x)| ≤ 1` for all `x`.

docs/references.bib

@@ -421,6 +421,22 @@ @InProceedings{   deligne_formulaire
   mrreviewer    = {Jacques Velu}
 }
 
+@Article{         dold1958,
+  author        = {Dold, Albrecht},
+  title         = {Homology of symmetric products and other functors of
+                  complexes},
+  journal       = {Ann. of Math. (2)},
+  fjournal      = {Annals of Mathematics. Second Series},
+  volume        = {68},
+  year          = {1958},
+  pages         = {54--80},
+  issn          = {0003-486X},
+  mrclass       = {55.00},
+  mrnumber      = {97057},
+  mrreviewer    = {Sze-tsen Hu},
+  doi           = {10.2307/1970043}
+}
+
 @Misc{            dupuis-lewis-macbeth2022,
   title         = {Formalized functional analysis with semilinear maps},
   author        = {Frédéric Dupuis and Robert Y. Lewis and Heather
@@ -657,6 +673,20 @@ @Book{            GierzEtAl1980
   mrreviewer    = {James W. Lea, Jr.}
 }
 
+@Book{            goerss-jardine-2009,
+  author        = {Goerss, Paul G. and Jardine, John F.},
+  title         = {Simplicial homotopy theory},
+  series        = {Modern Birkh\"{a}user Classics},
+  note          = {Reprint of the 1999 edition [MR1711612]},
+  publisher     = {Birkh\"{a}user Verlag, Basel},
+  year          = {2009},
+  pages         = {xvi+510},
+  isbn          = {978-3-0346-0188-7},
+  mrclass       = {55U10 (18G55)},
+  mrnumber      = {2840650},
+  doi           = {10.1007/978-3-0346-0189-4}
+}
+
 @Book{            Gordon55,
   author        = {Russel A. Gordon},
   title         = {The integrals of Lebesgue, Denjoy, Perron, and Henstock},

docs/undergrad.yaml

@@ -71,7 +71,7 @@ Linear algebra:
     examples: ''
   Exponential:
     endomorphism exponential: ''
-    matrix exponential: 'https://en.wikipedia.org/wiki/Matrix_exponential'
+    matrix exponential: 'exp'
 
 # 2.
 Group Theory:
@@ -565,7 +565,7 @@ Probability Theory:
     $\mathrm{L}^p$ convergence: 'measure_theory.Lp'
     almost surely convergence: 'measure_theory.measure.ae'
     Markov inequality: 'measure_theory.mul_meas_ge_le_lintegral'
-    Tchebychev inequality: ''
+    Chebychev inequality: 'probability_theory.meas_ge_le_variance_div_sq'
     Levy's theorem: ''
     weak law of large numbers: ''
     strong law of large numbers: ''

scripts/nolints.txt

@@ -493,13 +493,9 @@ apply_nolint relator.right_total doc_blame
 apply_nolint relator.right_unique doc_blame
 
 -- measure_theory/group/prod.lean
-apply_nolint measure_theory.absolutely_continuous_of_is_mul_left_invariant to_additive_doc
 apply_nolint measure_theory.map_prod_inv_mul_eq to_additive_doc
 apply_nolint measure_theory.map_prod_inv_mul_eq_swap to_additive_doc
-apply_nolint measure_theory.map_prod_mul_eq to_additive_doc
-apply_nolint measure_theory.map_prod_mul_eq_swap to_additive_doc
 apply_nolint measure_theory.map_prod_mul_inv_eq to_additive_doc
-apply_nolint measure_theory.measure_eq_div_smul to_additive_doc
 apply_nolint measure_theory.measure_lintegral_div_measure to_additive_doc
 apply_nolint measure_theory.measure_mul_lintegral_eq to_additive_doc
 

src/algebra/category/Algebra/basic.lean

@@ -5,7 +5,7 @@ Authors: Scott Morrison
 -/
 import algebra.algebra.subalgebra.basic
 import algebra.free_algebra
-import algebra.category.CommRing.basic
+import algebra.category.Ring.basic
 import algebra.category.Module.basic
 
 /-!

src/algebra/category/Algebra/limits.lean

@@ -5,7 +5,7 @@ Authors: Scott Morrison
 -/
 import algebra.category.Algebra.basic
 import algebra.category.Module.limits
-import algebra.category.CommRing.limits
+import algebra.category.Ring.limits
 
 /-!
 # The category of R-algebras has all limits

src/algebra/category/BoolRing.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import algebra.category.CommRing.basic
+import algebra.category.Ring.basic
 import algebra.ring.boolean_ring
 import order.category.BoolAlg
 

src/algebra/category/Group/biproducts.lean

@@ -21,9 +21,20 @@ universe u
 
 namespace AddCommGroup
 
+-- As `AddCommGroup` is preadditive, and has all limits, it automatically has biproducts.
+instance : has_binary_biproducts AddCommGroup :=
+has_binary_biproducts.of_has_binary_products
+
+instance : has_finite_biproducts AddCommGroup :=
+has_finite_biproducts.of_has_finite_products
+
+-- We now construct explicit limit data,
+-- so we can compare the biproducts to the usual unbundled constructions.
+
 /--
 Construct limit data for a binary product in `AddCommGroup`, using `AddCommGroup.of (G × H)`.
 -/
+@[simps cone_X is_limit_lift]
 def binary_product_limit_cone (G H : AddCommGroup.{u}) : limits.limit_cone (pair G H) :=
 { cone :=
   { X := AddCommGroup.of (G × H),
@@ -36,18 +47,17 @@ def binary_product_limit_cone (G H : AddCommGroup.{u}) : limits.limit_cone (pair
       ext; [rw ← w walking_pair.left, rw ← w walking_pair.right]; refl,
     end, } }
 
+@[simp] lemma binary_product_limit_cone_cone_π_app_left (G H : AddCommGroup.{u}) :
+  (binary_product_limit_cone G H).cone.π.app walking_pair.left = add_monoid_hom.fst G H := rfl
 
-instance has_binary_product (G H : AddCommGroup.{u}) : has_binary_product G H :=
-has_limit.mk (binary_product_limit_cone G H)
-
-instance (G H : AddCommGroup.{u}) : has_binary_biproduct G H :=
-has_binary_biproduct.of_has_binary_product _ _
+@[simp] lemma binary_product_limit_cone_cone_π_app_right (G H : AddCommGroup.{u}) :
+  (binary_product_limit_cone G H).cone.π.app walking_pair.right = add_monoid_hom.snd G H := rfl
 
 /--
 We verify that the biproduct in AddCommGroup is isomorphic to
 the cartesian product of the underlying types:
 -/
-noncomputable
+@[simps] noncomputable
 def biprod_iso_prod (G H : AddCommGroup.{u}) : (G ⊞ H : AddCommGroup) ≅ AddCommGroup.of (G × H) :=
 is_limit.cone_point_unique_up_to_iso
   (binary_biproduct.is_limit G H)
@@ -75,7 +85,7 @@ def lift (s : cone F) :
 /--
 Construct limit data for a product in `AddCommGroup`, using `AddCommGroup.of (Π j, F.obj j)`.
 -/
-def product_limit_cone : limits.limit_cone F :=
+@[simps] def product_limit_cone : limits.limit_cone F :=
 { cone :=
   { X := AddCommGroup.of (Π j, F.obj j),
     π := discrete.nat_trans (λ j, pi.eval_add_monoid_hom (λ j, F.obj j) j), },
@@ -92,29 +102,22 @@ def product_limit_cone : limits.limit_cone F :=
 
 end has_limit
 
-section
-
 open has_limit
 
-variables [decidable_eq J] [fintype J]
-
-instance (f : J → AddCommGroup.{u}) : has_biproduct f :=
-has_biproduct.of_has_product _
-
 /--
 We verify that the biproduct we've just defined is isomorphic to the AddCommGroup structure
 on the dependent function type
 -/
-noncomputable
-def biproduct_iso_pi (f : J → AddCommGroup.{u}) :
+@[simps hom_apply] noncomputable
+def biproduct_iso_pi [decidable_eq J] [fintype J] (f : J → AddCommGroup.{u}) :
   (⨁ f : AddCommGroup) ≅ AddCommGroup.of (Π j, f j) :=
 is_limit.cone_point_unique_up_to_iso
   (biproduct.is_limit f)
   (product_limit_cone (discrete.functor f)).is_limit
 
-end
-
-instance : has_finite_biproducts AddCommGroup :=
-⟨λ J _ _, by exactI { has_biproduct := λ f, by apply_instance }⟩
+@[simp, elementwise] lemma biproduct_iso_pi_inv_comp_π [decidable_eq J] [fintype J]
+  (f : J → AddCommGroup.{u}) (j : J) :
+  (biproduct_iso_pi f).inv ≫ biproduct.π f j = pi.eval_add_monoid_hom (λ j, f j) j :=
+is_limit.cone_point_unique_up_to_iso_inv_comp _ _ _
 
 end AddCommGroup

src/algebra/category/Module/basic.lean

@@ -7,6 +7,7 @@ import algebra.category.Group.basic
 import category_theory.limits.shapes.kernels
 import category_theory.linear
 import linear_algebra.basic
+import category_theory.conj
 
 /-!
 # The category of `R`-modules
@@ -263,6 +264,14 @@ instance : linear S (Module.{v} S) :=
   smul_comp' := by { intros, ext, simp },
   comp_smul' := by { intros, ext, simp }, }
 
+variables {X Y X' Y' : Module.{v} S}
+
+lemma iso.hom_congr_eq_arrow_congr (i : X ≅ X') (j : Y ≅ Y') (f : X ⟶ Y) :
+  iso.hom_congr i j f = linear_equiv.arrow_congr i.to_linear_equiv j.to_linear_equiv f := rfl
+
+lemma iso.conj_eq_conj (i : X ≅ X') (f : End X) :
+  iso.conj i f = linear_equiv.conj i.to_linear_equiv f := rfl
+
 end
 
 end Module