Merge remote-tracking branch 'origin/master' into delete_deprecated

archive/100-theorems-list/37_solution_of_cubic.lean

@@ -46,7 +46,7 @@ variables {ω p q r s t : K}
 
 lemma cube_root_of_unity_sum (hω : is_primitive_root ω 3) : 1 + ω + ω^2 = 0 :=
 begin
-  convert is_root_cyclotomic (nat.succ_pos _) hω,
+  convert hω.is_root_cyclotomic (nat.succ_pos _),
   rw [cyclotomic_eq_geom_sum nat.prime_three, eval_geom_sum],
   simp only [geom_sum_succ, geom_sum_zero],
   ring,

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

@@ -509,7 +509,7 @@ omit h
 /-- The infinite sequence of cubes contradicts the finiteness of the family. -/
 theorem not_correct : ¬correct cs :=
 begin
-  intro h, apply not_le_of_lt (lt_omega_iff_fintype.mpr ⟨_inst_1⟩),
+  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),
   dsimp only [decreasing_sequence], rw hnm

archive/imo/imo2008_q3.lean

@@ -7,7 +7,7 @@ import data.real.basic
 import data.real.sqrt
 import data.nat.prime
 import number_theory.primes_congruent_one
-import number_theory.quadratic_reciprocity
+import number_theory.legendre_symbol.quadratic_reciprocity
 import tactic.linear_combination
 
 /-!

counterexamples/homogeneous_prime_not_prime.lean

@@ -10,7 +10,7 @@ import tactic.derive_fintype
 /-!
 # A homogeneous prime that is homogeneously prime but not prime
 
-In `src/ring_theory/graded_algebra/radical.lean`,  we assumed that the underline grading is inedxed
+In `src/ring_theory/graded_algebra/radical.lean`,  we assumed that the underline grading is indexed
 by a `linear_ordered_cancel_add_comm_monoid` to prove that a homogeneous ideal is prime if and only
 if it is homogeneously prime. This file is aimed to show that even if this assumption isn't strictly
 necessary, the assumption of "being cancellative" is. We construct a counterexample where the

counterexamples/pseudoelement.lean

@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2022 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Riccardo Brasca
+-/
+
+import category_theory.abelian.pseudoelements
+
+/-!
+# Pseudoelements and pullbacks
+Borceux claims in Proposition 1.9.5 that the pseudoelement constructed in
+`category_theory.abelian.pseudoelement.pseudo_pullback` is unique. We show here that this claim is
+false. This means in particular that we cannot have an extensionality principle for pullbacks in
+terms of pseudoelements.
+
+## Implementation details
+The construction, suggested in https://mathoverflow.net/a/419951/7845, is the following.
+We work in the category of `Module ℤ` and we consider the special case of `ℚ ⊞ ℚ` (that is the
+pullback over the terminal object). We consider the pseudoelements associated to `x : ℚ ⟶ ℚ ⊞ ℚ`
+given by `t ↦ (t, 2 * t)` and `y : ℚ ⟶ ℚ ⊞ ℚ` given by `t ↦ (t, t)`.
+
+## Main results
+* `category_theory.abelian.pseudoelement.exist_ne_and_fst_eq_fst_and_snd_eq_snd` : there are two
+  pseudoelements `x y : ℚ ⊞ ℚ` such that `x ≠ y`, `biprod.fst x = biprod.fst y` and
+  `biprod.snd x = biprod.snd y`.
+
+## References
+* [F. Borceux, *Handbook of Categorical Algebra 2*][borceux-vol2]
+-/
+
+open category_theory.abelian category_theory category_theory.limits Module linear_map
+
+noncomputable theory
+
+namespace category_theory.abelian.pseudoelement
+
+/-- `x` is given by `t ↦ (t, 2 * t)`. -/
+def x : over ((of ℤ ℚ) ⊞ (of ℤ ℚ)) :=
+begin
+  constructor,
+  exact biprod.lift (of_hom id) (of_hom (2 * id)),
+end
+
+/-- `y` is given by `t ↦ (t, t)`. -/
+def y : over ((of ℤ ℚ) ⊞ (of ℤ ℚ)) :=
+begin
+  constructor,
+  exact biprod.lift (of_hom id) (of_hom id),
+end
+
+/-- `biprod.fst ≫ x` is pseudoequal to `biprod.fst y`. -/
+lemma fst_x_pseudo_eq_fst_y : pseudo_equal _ (app biprod.fst x) (app biprod.fst y) :=
+begin
+  refine ⟨of ℤ ℚ, (of_hom id), (of_hom id),
+    category_struct.id.epi (of ℤ ℚ), _, _⟩,
+  { exact (Module.epi_iff_surjective _).2 (λ a, ⟨(a : ℚ), by simp⟩) },
+  { dsimp [x, y],
+    simp }
+end
+
+/-- `biprod.snd ≫ x` is pseudoequal to `biprod.snd y`. -/
+lemma snd_x_pseudo_eq_snd_y : pseudo_equal _
+  (app biprod.snd x) (app biprod.snd y) :=
+begin
+  refine ⟨of ℤ ℚ, (of_hom id), 2 • (of_hom id),
+    category_struct.id.epi (of ℤ ℚ), _, _⟩,
+  { refine (Module.epi_iff_surjective _).2 (λ a, ⟨(a/2 : ℚ), _⟩),
+    simp only [two_smul, add_apply, of_hom_apply, id_coe, id.def],
+    convert add_halves' _,
+    change char_zero ℚ,
+    apply_instance },
+  { dsimp [x, y],
+    exact concrete_category.hom_ext _ _ (λ a, by simpa) }
+end
+
+/-- `x` is not pseudoequal to `y`. -/
+lemma x_not_pseudo_eq : ¬(pseudo_equal _ x y) :=
+begin
+  intro h,
+  replace h := Module.eq_range_of_pseudoequal h,
+  dsimp [x, y] at h,
+  let φ := (biprod.lift (of_hom (id : ℚ →ₗ[ℤ] ℚ)) (of_hom (2 * id))),
+  have mem_range := mem_range_self φ (1 : ℚ),
+  rw h at mem_range,
+  obtain ⟨a, ha⟩ := mem_range,
+  rw [← Module.id_apply (φ (1 : ℚ)), ← biprod.total, ← linear_map.comp_apply, ← comp_def,
+    preadditive.comp_add] at ha,
+  let π₁ := (biprod.fst : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _),
+  have ha₁ := congr_arg π₁ ha,
+  simp only [← linear_map.comp_apply, ← comp_def] at ha₁,
+  simp only [biprod.lift_fst, of_hom_apply, id_coe, id.def, preadditive.add_comp, category.assoc,
+    biprod.inl_fst, category.comp_id, biprod.inr_fst, limits.comp_zero, add_zero] at ha₁,
+  let π₂ := (biprod.snd : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _),
+  have ha₂ := congr_arg π₂ ha,
+  simp only [← linear_map.comp_apply, ← comp_def] at ha₂,
+  have : (2 : ℚ →ₗ[ℤ] ℚ) 1 = 1 + 1 := rfl,
+  simp only [ha₁, this, biprod.lift_snd, of_hom_apply, id_coe, id.def, preadditive.add_comp,
+    category.assoc, biprod.inl_snd, limits.comp_zero, biprod.inr_snd, category.comp_id, zero_add,
+    mul_apply, self_eq_add_left] at ha₂,
+  exact @one_ne_zero ℚ _ _ ha₂,
+end
+
+local attribute [instance] pseudoelement.setoid
+
+open_locale pseudoelement
+
+/-- `biprod.fst ⟦x⟧ = biprod.fst ⟦y⟧`. -/
+lemma fst_mk_x_eq_fst_mk_y : (biprod.fst : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _) ⟦x⟧ =
+  (biprod.fst : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _) ⟦y⟧ :=
+by simpa only [abelian.pseudoelement.pseudo_apply_mk, quotient.eq] using fst_x_pseudo_eq_fst_y
+
+/-- `biprod.snd ⟦x⟧ = biprod.snd ⟦y⟧`. -/
+lemma snd_mk_x_eq_snd_mk_y : (biprod.snd : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _) ⟦x⟧ =
+  (biprod.snd : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _) ⟦y⟧ :=
+by simpa only [abelian.pseudoelement.pseudo_apply_mk, quotient.eq] using snd_x_pseudo_eq_snd_y
+
+/-- `⟦x⟧ ≠ ⟦y⟧`. -/
+lemma mk_x_ne_mk_y : ⟦x⟧ ≠ ⟦y⟧ :=
+λ h, x_not_pseudo_eq $ quotient.eq.1 h
+
+/-- There are two pseudoelements `x y : ℚ ⊞ ℚ` such that `x ≠ y`, `biprod.fst x = biprod.fst y` and
+ `biprod.snd x = biprod.snd y`. -/
+lemma exist_ne_and_fst_eq_fst_and_snd_eq_snd : ∃ x y : (of ℤ ℚ) ⊞ (of ℤ ℚ),
+  x ≠ y ∧
+  (biprod.fst : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _) x = (biprod.fst : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _) y ∧
+  (biprod.snd : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _) x = (biprod.snd : (of ℤ ℚ) ⊞ (of ℤ ℚ) ⟶ _) y:=
+⟨⟦x⟧, ⟦y⟧, mk_x_ne_mk_y, fst_mk_x_eq_fst_mk_y, snd_mk_x_eq_snd_mk_y⟩
+
+end category_theory.abelian.pseudoelement

docs/references.bib

@@ -259,15 +259,16 @@ @Book{            bourbaki1987
   author        = {Bourbaki, N.},
   title         = {Topological vector spaces. {C}hapters 1--5},
   series        = {Elements of Mathematics (Berlin)},
-  note          = {Translated from the French by H. G. Eggleston and S. Madan},
+  note          = {Translated from the French by H. G. Eggleston and S.
+                  Madan},
   publisher     = {Springer-Verlag, Berlin},
   year          = {1987},
   pages         = {viii+364},
   isbn          = {3-540-13627-4},
   mrclass       = {46-02 (46-01 46Axx 47D15)},
   mrnumber      = {910295},
   doi           = {10.1007/978-3-642-61715-7},
-  url           = {https://doi.org/10.1007/978-3-642-61715-7},
+  url           = {https://doi.org/10.1007/978-3-642-61715-7}
 }
 
 @Article{         cadiou1972,
@@ -404,7 +405,7 @@ @Book{            davey_priestley
   mrnumber      = {1902334},
   mrreviewer    = {T. S. Blyth},
   doi           = {10.1017/CBO9780511809088},
-  url           = {https://doi.org/10.1017/CBO9780511809088},
+  url           = {https://doi.org/10.1017/CBO9780511809088}
 }
 
 @InProceedings{   deligne_formulaire,
@@ -536,18 +537,17 @@ @Book{            fremlin_vol2
   note          = {Broad foundations, 2010 edition},
   publisher     = {Torres Fremlin, Colchester},
   year          = {2010},
-  isbn          = {0-9538129-2-8},
+  isbn          = {0-9538129-2-8}
 }
 
 @Book{            fremlin_vol4,
   author        = {Fremlin, David H.},
   title         = {Measure theory. {V}ol. 4},
   note          = {Topological Measure Spaces},
   publisher     = {Torres Fremlin, Colchester},
-  year          = {2003},
+  year          = {2003}
 }
 
-
 @Book{            fuchs1963,
   author        = {Fuchs, L.},
   title         = {Partially ordered algebraic systems},
@@ -808,7 +808,7 @@ @Article{         Higman52
   year          = {1952}
 }
 
-@book{            Hodges97,
+@Book{            Hodges97,
   author        = {Hodges, Wilfrid},
   title         = {A Shorter Model Theory},
   year          = {1997},
@@ -889,6 +889,14 @@ @Article{         joyal1977
                   https://bosker.files.wordpress.com/2010/12/joyal-games.pdf)}
 }
 
+@Misc{            Joyal_Street,
+  title         = {Braided monoidal categories},
+  author        = {Andr{\'e} Joyal and Ross H. Street},
+  year          = {1986},
+  note          = {Mathematics Reports 860081, Macquarie University},
+  url           = {http://maths.mq.edu.au/~street/JS1.pdf}
+}
+
 @Article{         Joyce1982,
   author        = {David Joyce},
   title         = {A classifying invariant of knots, the knot quandle},
@@ -931,7 +939,7 @@ @Book{            kechris1995
   mrnumber      = {1321597},
   mrreviewer    = {Jakub Jasi\'{n}ski},
   doi           = {10.1007/978-1-4612-4190-4},
-  url           = {https://doi.org/10.1007/978-1-4612-4190-4},
+  url           = {https://doi.org/10.1007/978-1-4612-4190-4}
 }
 
 @Article{         kleiman1979,
@@ -1458,7 +1466,7 @@ @Book{            Tent_Ziegler
   place         = {Cambridge},
   series        = {Lecture Notes in Logic},
   title         = {A Course in Model Theory},
-  DOI           = {10.1017/CBO9781139015417},
+  doi           = {10.1017/CBO9781139015417},
   publisher     = {Cambridge University Press},
   author        = {Tent, Katrin and Ziegler, Martin},
   year          = {2012},

scripts/nolints.txt

@@ -1,6 +1,11 @@
 import .all
 run_cmd tactic.skip
 
+-- algebra/big_operators/fin.lean
+apply_nolint fin.prod_univ_cast_succ to_additive_doc
+apply_nolint fin.prod_univ_succ to_additive_doc
+apply_nolint fin.prod_univ_succ_above to_additive_doc
+
 -- algebra/category/Group/limits.lean
 apply_nolint CommGroup.category_theory.forget₂.category_theory.creates_limit to_additive_doc
 apply_nolint CommGroup.forget_preserves_limits to_additive_doc
@@ -124,7 +129,6 @@ apply_nolint traversable.free.mk doc_blame
 apply_nolint traversable.length doc_blame
 apply_nolint traversable.map_fold doc_blame
 apply_nolint traversable.mfoldl doc_blame
-apply_nolint traversable.mfoldl.unop_of_free_monoid unused_arguments
 apply_nolint traversable.mfoldr doc_blame
 
 -- control/monad/cont.lean
@@ -214,10 +218,7 @@ apply_nolint locally_finite.realizer doc_blame has_inhabited_instance
 apply_nolint finset.noncomm_prod_union_of_disjoint to_additive_doc
 
 -- data/fintype/card.lean
-apply_nolint fin.prod_univ_cast_succ to_additive_doc
 apply_nolint fin.prod_univ_eq_prod_range to_additive_doc
-apply_nolint fin.prod_univ_succ to_additive_doc
-apply_nolint fin.prod_univ_succ_above to_additive_doc
 
 -- data/fp/basic.lean
 apply_nolint fp.div_nat_lt_two_pow doc_blame unused_arguments
@@ -522,11 +523,6 @@ apply_nolint affine_subspace.to_add_torsor fails_quickly
 apply_nolint function.has_scalar to_additive_doc
 apply_nolint function.smul_comm_class to_additive_doc
 
--- logic/equiv/list.lean
-apply_nolint encodable.fintype_arrow doc_blame
-apply_nolint encodable.fintype_pi doc_blame
-apply_nolint encodable.trunc_encodable_of_fintype doc_blame
-
 -- logic/relator.lean
 apply_nolint relator.bi_total doc_blame
 apply_nolint relator.bi_unique doc_blame
@@ -613,47 +609,24 @@ apply_nolint tactic.mono doc_blame
 -- number_theory/dioph.lean
 apply_nolint poly has_inhabited_instance
 
--- number_theory/zsqrtd/basic.lean
-apply_nolint zsqrtd.le doc_blame
-apply_nolint zsqrtd.lt doc_blame
-apply_nolint zsqrtd.norm doc_blame
-
--- number_theory/zsqrtd/gaussian_int.lean
-apply_nolint gaussian_int doc_blame
-apply_nolint gaussian_int.div doc_blame
-apply_nolint gaussian_int.mod doc_blame
-
 -- order/filter/at_top_bot.lean
 apply_nolint filter.map_at_top_finset_prod_le_of_prod_eq to_additive_doc
 
--- order/filter/pointwise.lean
-apply_nolint filter.has_add check_reducibility
-apply_nolint filter.has_mul check_reducibility
-
 -- order/prime_ideal.lean
 apply_nolint order.ideal.is_prime.is_maximal fails_quickly
 
 -- ring_theory/witt_vector/basic.lean
 apply_nolint witt_vector.comm_ring check_reducibility
 
--- set_theory/cofinality.lean
-apply_nolint strict_order.cof doc_blame
-
--- set_theory/game.lean
-apply_nolint pgame.inv_ty has_inhabited_instance
-
 -- set_theory/lists.lean
 apply_nolint finsets doc_blame
 
 -- set_theory/pgame.lean
-apply_nolint pgame.left_moves has_inhabited_instance
 apply_nolint pgame.relabelling has_inhabited_instance
 apply_nolint pgame.restricted has_inhabited_instance
-apply_nolint pgame.right_moves has_inhabited_instance
 
 -- set_theory/zfc.lean
 apply_nolint Set.map_definable_aux unused_arguments
-apply_nolint pSet.type has_inhabited_instance
 
 -- tactic/abel.lean
 apply_nolint tactic.abel.eval doc_blame