Merge remote-tracking branch 'origin/master' into adomani/use_cdots_5

Archive/Imo/Imo2013Q5.lean

@@ -241,7 +241,7 @@ theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y
   -- we need the top of the fraction to be strictly greater than 1 in order
   -- to apply `fixed_point_of_gt_1`.
   intro x hx
-  have H₀ : x * x.den = x.num := Rat.mul_den_eq_num
+  have H₀ : x * x.den = x.num := x.mul_den_eq_num
   have H : x * (↑(2 * x.den) : ℚ) = (↑(2 * x.num) : ℚ) := by push_cast; linear_combination 2 * H₀
   set x2denom := 2 * x.den
   set x2num := 2 * x.num

Mathlib.lean

@@ -88,6 +88,7 @@ import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
 import Mathlib.Algebra.Category.ModuleCat.Presheaf
+import Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
 import Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
 import Mathlib.Algebra.Category.ModuleCat.Products
 import Mathlib.Algebra.Category.ModuleCat.Projective
@@ -611,6 +612,7 @@ import Mathlib.Algebra.Ring.Defs
 import Mathlib.Algebra.Ring.Divisibility.Basic
 import Mathlib.Algebra.Ring.Divisibility.Lemmas
 import Mathlib.Algebra.Ring.Equiv
+import Mathlib.Algebra.Ring.Ext
 import Mathlib.Algebra.Ring.Fin
 import Mathlib.Algebra.Ring.Hom.Basic
 import Mathlib.Algebra.Ring.Hom.Defs
@@ -1440,6 +1442,7 @@ import Mathlib.CategoryTheory.Monoidal.Category
 import Mathlib.CategoryTheory.Monoidal.Center
 import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
 import Mathlib.CategoryTheory.Monoidal.CommMon_
+import Mathlib.CategoryTheory.Monoidal.Comon_
 import Mathlib.CategoryTheory.Monoidal.Discrete
 import Mathlib.CategoryTheory.Monoidal.End
 import Mathlib.CategoryTheory.Monoidal.Free.Basic
@@ -3902,6 +3905,7 @@ import Mathlib.Topology.Bases
 import Mathlib.Topology.Basic
 import Mathlib.Topology.Bornology.Absorbs
 import Mathlib.Topology.Bornology.Basic
+import Mathlib.Topology.Bornology.BoundedOperation
 import Mathlib.Topology.Bornology.Constructions
 import Mathlib.Topology.Bornology.Hom
 import Mathlib.Topology.Category.Born

Mathlib/Algebra/Algebra/Equiv.lean

@@ -232,7 +232,7 @@ nonrec theorem map_sum {ι : Type*} (f : ι → A₁) (s : Finset ι) :
 
 theorem map_finsupp_sum {α : Type*} [Zero α] {ι : Type*} (f : ι →₀ α) (g : ι → α → A₁) :
     e (f.sum g) = f.sum fun i b => e (g i b) :=
-  e.map_sum _ _
+  _root_.map_sum e _ _
 #align alg_equiv.map_finsupp_sum AlgEquiv.map_finsupp_sum
 
 -- Porting note: Added [coe] attribute

Mathlib/Algebra/BigOperators/List/Basic.lean

@@ -574,7 +574,7 @@ If desired, we could add a class stating that `default = 0`.
 
 /-- This relies on `default ℕ = 0`. -/
 theorem headI_add_tail_sum (L : List ℕ) : L.headI + L.tail.sum = L.sum := by
-  cases L <;> simp; rfl
+  cases L <;> simp
 #align list.head_add_tail_sum List.headI_add_tail_sum
 
 /-- This relies on `default ℕ = 0`. -/

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang
 -/
 import Mathlib.Algebra.Category.ModuleCat.EpiMono
+import Mathlib.Algebra.Category.ModuleCat.Colimits
 import Mathlib.Algebra.Category.ModuleCat.Limits
 import Mathlib.RingTheory.TensorProduct.Basic
 
@@ -873,4 +874,16 @@ noncomputable instance preservesLimitRestrictScalars
     have hc' := isLimitOfPreserves (forget₂ _ AddCommGroupCat) hc
     exact isLimitOfReflects (forget₂ _ AddCommGroupCat) hc'⟩
 
+instance preservesColimitRestrictScalars {R S : Type*} [Ring R] [Ring S]
+    (f : R →+* S) {J : Type*} [Category J] (F : J ⥤ ModuleCat.{v} S)
+    [HasColimit (F ⋙ forget₂ _ AddCommGroupCat)] :
+    PreservesColimit F (ModuleCat.restrictScalars.{v} f) := by
+  have : HasColimit ((F ⋙ restrictScalars f) ⋙ forget₂ (ModuleCat R) AddCommGroupCat) :=
+    inferInstanceAs (HasColimit (F ⋙ forget₂ _ AddCommGroupCat))
+  apply preservesColimitOfPreservesColimitCocone (HasColimit.isColimitColimitCocone F)
+  apply isColimitOfReflects (forget₂ _ AddCommGroupCat)
+  apply isColimitOfPreserves (forget₂ (ModuleCat.{v} S) AddCommGroupCat.{v})
+  exact HasColimit.isColimitColimitCocone F
+
+
 end ModuleCat

Mathlib/Algebra/Category/ModuleCat/Colimits.lean

@@ -101,13 +101,20 @@ instance : HasColimit F := ⟨_, isColimitColimitCocone F⟩
 noncomputable instance : PreservesColimit F (forget₂ _ AddCommGroupCat) :=
   preservesColimitOfPreservesColimitCocone (isColimitColimitCocone F) (colimit.isColimit _)
 
+noncomputable instance reflectsColimit :
+    ReflectsColimit F (forget₂ (ModuleCat.{w'} R) AddCommGroupCat) :=
+  reflectsColimitOfReflectsIsomorphisms _ _
+
 end HasColimit
 
 variable (J R)
 
 instance hasColimitsOfShape [HasColimitsOfShape J AddCommGroupCat.{w'}] :
     HasColimitsOfShape J (ModuleCat.{w'} R) where
 
+noncomputable instance reflectsColimitsOfShape [HasColimitsOfShape J AddCommGroupCat.{w'}] :
+    ReflectsColimitsOfShape J (forget₂ (ModuleCat.{w'} R) AddCommGroupCat) where
+
 instance hasColimitsOfSize [HasColimitsOfSize.{v, u} AddCommGroupCat.{w'}] :
     HasColimitsOfSize.{v, u} (ModuleCat.{w'} R) where
 

Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean

@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.Algebra.Category.ModuleCat.Presheaf
+import Mathlib.Algebra.Category.ModuleCat.Colimits
+
+/-! # Colimits in categories of presheaves of modules
+
+In this file, it is shown that under suitable assumptions,
+colimits exist in the category `PresheafOfModules R`.
+
+-/
+
+universe v v₁ v₂ u₁ u₂ u u'
+
+open CategoryTheory Category Limits
+
+namespace PresheafOfModules
+
+variable {C : Type u₁} [Category.{v₁} C] {R : Cᵒᵖ ⥤ RingCat.{u}}
+  {J : Type u₂} [Category.{v₂} J]
+  (F : J ⥤ PresheafOfModules.{v} R)
+
+section Colimits
+
+variable [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), PreservesColimit (F ⋙ evaluation R Y)
+  (ModuleCat.restrictScalars (R.map f))]
+
+/-- A cocone in the category `PresheafOfModules R` is colimit if it is so after the application
+of the functors `evaluation R X` for all `X`. -/
+def evaluationJointlyReflectsColimits (c : Cocone F)
+    (hc : ∀ (X : Cᵒᵖ), IsColimit ((evaluation R X).mapCocone c)) : IsColimit c where
+  desc s := Hom.mk'' (fun X => (hc X).desc ((evaluation R X).mapCocone s)) (fun X Y f => by
+    apply (hc X).hom_ext
+    intro j
+    erw [(hc X).fac_assoc ((evaluation R X).mapCocone s) j, ← restrictionApp_naturality_assoc]
+    rw [← Functor.map_comp]
+    erw [(hc Y).fac ((evaluation R Y).mapCocone s), restrictionApp_naturality]
+    rfl)
+  fac s j := by
+    ext1 X
+    exact (hc X).fac ((evaluation R X).mapCocone s) j
+  uniq s m hm := by
+    ext1 X
+    apply (hc X).uniq ((evaluation R X).mapCocone s)
+    intro j
+    dsimp
+    rw [← hm]
+    rfl
+
+variable [∀ X, HasColimit (F ⋙ evaluation R X)]
+
+instance {X Y : Cᵒᵖ} (f : X ⟶ Y) :
+    HasColimit (F ⋙ evaluation R Y ⋙ (ModuleCat.restrictScalars (R.map f))) :=
+  ⟨_, isColimitOfPreserves (ModuleCat.restrictScalars (R.map f))
+    (colimit.isColimit (F ⋙ evaluation R Y))⟩
+
+/-- Given `F : J ⥤ PresheafOfModules.{v} R`, this is the `BundledCorePresheafOfModules R` which
+corresponds to the presheaf of modules which sends `X` to the colimit of `F ⋙ evaluation R X`. -/
+@[simps]
+noncomputable def colimitBundledCore : BundledCorePresheafOfModules R where
+  obj X := colimit (F ⋙ evaluation R X)
+  map {X Y} f := colimMap (whiskerLeft F (restriction R f)) ≫
+    (preservesColimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv
+  map_id X := colimit.hom_ext (fun j => by
+    dsimp
+    rw [ι_colimMap_assoc, whiskerLeft_app, restriction_app]
+    erw [ι_preservesColimitsIso_inv (G := ModuleCat.restrictScalars (R.map (𝟙 X))),
+      ModuleCat.restrictScalarsId'App_inv_naturality]
+    rw [restrictionApp_id]
+    rfl)
+  map_comp {X Y Z} f g := colimit.hom_ext (fun j => by
+    dsimp
+    rw [ι_colimMap_assoc, whiskerLeft_app, restriction_app, assoc, ι_colimMap_assoc]
+    erw [ι_preservesColimitsIso_inv (G := ModuleCat.restrictScalars (R.map (f ≫ g))),
+      ι_preservesColimitsIso_inv_assoc (G := ModuleCat.restrictScalars (R.map f))]
+    rw [← Functor.map_comp_assoc, ι_colimMap_assoc]
+    erw [ι_preservesColimitsIso_inv (G := ModuleCat.restrictScalars (R.map g))]
+    rw [restrictionApp_comp, ModuleCat.restrictScalarsComp'_inv_app, assoc, assoc,
+      whiskerLeft_app, whiskerLeft_app, restriction_app, restriction_app]
+    simp only [Functor.map_comp, assoc]
+    rfl)
+
+/-- Given `F : J ⥤ PresheafOfModules.{v} R`, this is the canonical map
+`F.obj j ⟶ (colimitBundledCore F).toPresheafOfModules` for all `j : J`. -/
+noncomputable def colimitCoconeιApp (j : J) :
+    F.obj j ⟶ (colimitBundledCore F).toPresheafOfModules :=
+  PresheafOfModules.Hom.mk'' (fun X => colimit.ι (F ⋙ evaluation R X) j) (fun X Y f => by
+    dsimp
+    erw [colimit.ι_desc_assoc, assoc, ← ι_preservesColimitsIso_inv]
+    rfl)
+
+@[reassoc (attr := simp)]
+lemma colimitCoconeιApp_naturality {i j : J} (f : i ⟶ j) :
+    F.map f ≫ colimitCoconeιApp F j = colimitCoconeιApp F i := by
+  ext1 X
+  exact colimit.w (F ⋙ evaluation R X) f
+
+/-- The (colimit) cocone for `F : J ⥤ PresheafOfModules.{v} R` that is constructed from
+the colimit of `F ⋙ evaluation R X` for all `X`. -/
+@[simps]
+noncomputable def colimitCocone : Cocone F where
+  pt := (colimitBundledCore F).toPresheafOfModules
+  ι := { app := colimitCoconeιApp F }
+
+/-- The cocone `colimitCocone F` is colimit for any `F : J ⥤ PresheafOfModules.{v} R`. -/
+noncomputable def isColimitColimitCocone : IsColimit (colimitCocone F) :=
+  evaluationJointlyReflectsColimits _ _ (fun _ => colimit.isColimit _)
+
+instance hasColimit : HasColimit F := ⟨_, isColimitColimitCocone F⟩
+
+noncomputable instance evaluationPreservesColimit (X : Cᵒᵖ) :
+    PreservesColimit F (evaluation R X) :=
+  preservesColimitOfPreservesColimitCocone (isColimitColimitCocone F) (colimit.isColimit _)
+
+variable [∀ X, PreservesColimit F
+  (evaluation R X ⋙ forget₂ (ModuleCat (R.obj X)) AddCommGroupCat)]
+
+noncomputable instance toPresheafPreservesColimit :
+    PreservesColimit F (toPresheaf R) :=
+  preservesColimitOfPreservesColimitCocone (isColimitColimitCocone F)
+    (Limits.evaluationJointlyReflectsColimits _
+      (fun X => isColimitOfPreserves (evaluation R X ⋙ forget₂ _ AddCommGroupCat)
+        (isColimitColimitCocone F)))
+
+end Colimits
+
+variable (R J)
+
+section HasColimitsOfShape
+
+variable [HasColimitsOfShape J AddCommGroupCat.{v}]
+
+instance hasColimitsOfShape : HasColimitsOfShape J (PresheafOfModules.{v} R) where
+
+noncomputable instance evaluationPreservesColimitsOfShape (X : Cᵒᵖ) :
+    PreservesColimitsOfShape J (evaluation R X : PresheafOfModules.{v} R ⥤ _) where
+
+noncomputable instance toPresheafPreservesColimitsOfShape :
+    PreservesColimitsOfShape J (toPresheaf.{v} R) where
+
+end HasColimitsOfShape
+
+namespace Finite
+
+instance hasFiniteColimits : HasFiniteColimits (PresheafOfModules.{v} R) :=
+  ⟨fun _ => inferInstance⟩
+
+noncomputable instance evaluationPreservesFiniteColimits (X : Cᵒᵖ) :
+    PreservesFiniteColimits (evaluation.{v} R X) where
+
+noncomputable instance toPresheafPreservesFiniteColimits :
+    PreservesFiniteColimits (toPresheaf R) where
+
+end Finite
+
+end PresheafOfModules

Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean

@@ -13,9 +13,6 @@ import Mathlib.CategoryTheory.Limits.FunctorCategory
 In this file, it is shown that under suitable assumptions,
 limits exist in the category `PresheafOfModules R`.
 
-## TODO
-* do the same for colimits
-
 -/
 
 universe v v₁ v₂ u₁ u₂ u u'

Mathlib/Algebra/DirectSum/Algebra.lean

@@ -72,7 +72,7 @@ instance : Algebra R (⨁ i, A i) where
   toFun := (DirectSum.of A 0).comp GAlgebra.toFun
   map_zero' := AddMonoidHom.map_zero _
   map_add' := AddMonoidHom.map_add _
-  map_one' := (DirectSum.of A 0).congr_arg GAlgebra.map_one
+  map_one' := DFunLike.congr_arg (DirectSum.of A 0) GAlgebra.map_one
   map_mul' a b := by
     simp only [AddMonoidHom.comp_apply]
     rw [of_mul_of]

Mathlib/Algebra/Group/Submonoid/Units.lean

@@ -105,11 +105,11 @@ lemma inv_val_mem_of_mem_units (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units) :
 
 @[to_additive]
 lemma coe_inv_val_mul_coe_val (S : Submonoid M) {x : Sˣ} :
-    ((x⁻¹ : Sˣ) : M) * ((x : Sˣ) : M) = 1 := S.subtype.congr_arg x.inv_mul
+    ((x⁻¹ : Sˣ) : M) * ((x : Sˣ) : M) = 1 := DFunLike.congr_arg S.subtype x.inv_mul
 
 @[to_additive]
 lemma coe_val_mul_coe_inv_val (S : Submonoid M) {x : Sˣ} :
-    ((x : Sˣ) : M) * ((x⁻¹ : Sˣ) : M) = 1 := S.subtype.congr_arg x.mul_inv
+    ((x : Sˣ) : M) * ((x⁻¹ : Sˣ) : M) = 1 := DFunLike.congr_arg S.subtype x.mul_inv
 
 @[to_additive]
 lemma mk_inv_mul_mk_eq_one (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units) :

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

@@ -375,6 +375,7 @@ lemma div_eq_one_iff_eq (hb : b ≠ 0) : a / b = 1 ↔ a = b := hb.isUnit.div_eq
 lemma div_mul_cancel_right₀ (hb : b ≠ 0) (a : G₀) : b / (a * b) = a⁻¹ :=
   hb.isUnit.div_mul_cancel_right _
 
+set_option linter.deprecated false in
 @[deprecated div_mul_cancel_right₀] -- 2024-03-20
 lemma div_mul_left (hb : b ≠ 0) : b / (a * b) = 1 / a := hb.isUnit.div_mul_left
 #align div_mul_left div_mul_left
@@ -441,6 +442,7 @@ instance (priority := 100) CommGroupWithZero.toDivisionCommMonoid :
 lemma div_mul_cancel_left₀ (ha : a ≠ 0) (b : G₀) : a / (a * b) = b⁻¹ :=
   ha.isUnit.div_mul_cancel_left _
 
+set_option linter.deprecated false in
 @[deprecated div_mul_cancel_left₀] -- 2024-03-22
 lemma div_mul_right (b : G₀) (ha : a ≠ 0) : a / (a * b) = 1 / b := ha.isUnit.div_mul_right _
 #align div_mul_right div_mul_right

Mathlib/Algebra/Order/CauSeq/Completion.lean

@@ -236,7 +236,7 @@ theorem inv_mk {f} (hf) : (@mk α _ β _ abv _ f)⁻¹ = mk (inv f hf) :=
 #align cau_seq.completion.inv_mk CauSeq.Completion.inv_mk
 
 theorem cau_seq_zero_ne_one : ¬(0 : CauSeq _ abv) ≈ 1 := fun h =>
-  have : LimZero (1 - 0) := Setoid.symm h
+  have : LimZero (1 - 0 : CauSeq _ abv) := Setoid.symm h
   have : LimZero 1 := by simpa
   by apply one_ne_zero <| const_limZero.1 this
 #align cau_seq.completion.cau_seq_zero_ne_one CauSeq.Completion.cau_seq_zero_ne_one