bump to nightly-2023-04-06-16

mathlib commit leanprover-community/mathlib@06a655b
leanprover-community · Apr 6, 2023 · f3692ad · f3692ad
1 parent f3c842f
commit f3692ad
Show file tree

Hide file tree

Showing 9 changed files with 967 additions and 71 deletions.
diff --git a/Mathbin/AlgebraicTopology/DoldKan/NCompGamma.lean b/Mathbin/AlgebraicTopology/DoldKan/NCompGamma.lean
@@ -192,8 +192,8 @@ def natTrans : (n₂ : Karoubi (SimplicialObject C) ⥤ _) ⋙ Γ₂ ⟶ 𝟭 _
 
 theorem natTrans_app_f_app (P : Karoubi (SimplicialObject C)) :
     Γ₂N₂.natTrans.app P =
-      (n₂ ⋙ Γ₂).map P.decompIdI ≫
-        (compatibilityΓ₂N₁Γ₂N₂.Hom ≫ Γ₂N₁.natTrans).app P.pt ≫ P.decompIdP :=
+      (n₂ ⋙ Γ₂).map P.decompId_i ≫
+        (compatibilityΓ₂N₁Γ₂N₂.Hom ≫ Γ₂N₁.natTrans).app P.pt ≫ P.decompId_p :=
   whiskeringLeft_obj_preimage_app (compatibilityΓ₂N₁Γ₂N₂.Hom ≫ Γ₂N₁.natTrans) P
 #align algebraic_topology.dold_kan.Γ₂N₂.nat_trans_app_f_app AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app
 

diff --git a/Mathbin/Analysis/SpecificLimits/Basic.lean b/Mathbin/Analysis/SpecificLimits/Basic.lean
diff --git a/Mathbin/CategoryTheory/Idempotents/Biproducts.lean b/Mathbin/CategoryTheory/Idempotents/Biproducts.lean
@@ -130,11 +130,11 @@ def complement (P : Karoubi C) : Karoubi C
 instance (P : Karoubi C) : HasBinaryBiproduct P P.complement :=
   hasBinaryBiproduct_of_total
     { pt := P.pt
-      fst := P.decompIdP
-      snd := P.complement.decompIdP
-      inl := P.decompIdI
-      inr := P.complement.decompIdI
-      inl_fst := P.decomp_id.symm
+      fst := P.decompId_p
+      snd := P.complement.decompId_p
+      inl := P.decompId_i
+      inr := P.complement.decompId_i
+      inl_fst := P.decompId.symm
       inl_snd :=
         by
         simp only [decomp_id_i_f, decomp_id_p_f, complement_p, comp_sub, comp_f, hom_ext,
@@ -145,7 +145,7 @@ instance (P : Karoubi C) : HasBinaryBiproduct P P.complement :=
         simp only [decomp_id_i_f, complement_p, decomp_id_p_f, sub_comp, comp_f, hom_ext,
           quiver.hom.add_comm_group_zero_f, P.idem]
         erw [id_comp, sub_self]
-      inr_snd := P.complement.decomp_id.symm }
+      inr_snd := P.complement.decompId.symm }
     (by
       simp only [hom_ext, ← decomp_p, quiver.hom.add_comm_group_add_f, to_karoubi_map_f, id_eq,
         coe_p, complement_p, add_sub_cancel'_right])
@@ -155,8 +155,8 @@ preadditive category is actually a direct factor of the image `(to_karoubi C).ob
 of `P.X` in the category `karoubi C` -/
 def decomposition (P : Karoubi C) : P ⊞ P.complement ≅ (toKaroubi _).obj P.pt
     where
-  Hom := biprod.desc P.decompIdI P.complement.decompIdI
-  inv := biprod.lift P.decompIdP P.complement.decompIdP
+  Hom := biprod.desc P.decompId_i P.complement.decompId_i
+  inv := biprod.lift P.decompId_p P.complement.decompId_p
   hom_inv_id' := by
     ext1
     · simp only [← assoc, biprod.inl_desc, comp_id, biprod.lift_eq, comp_add, ← decomp_id, id_comp,

diff --git a/Mathbin/CategoryTheory/Idempotents/FunctorExtension.lean b/Mathbin/CategoryTheory/Idempotents/FunctorExtension.lean
diff --git a/Mathbin/CategoryTheory/Idempotents/Karoubi.lean b/Mathbin/CategoryTheory/Idempotents/Karoubi.lean
diff --git a/Mathbin/LinearAlgebra/StdBasis.lean b/Mathbin/LinearAlgebra/StdBasis.lean
diff --git a/Mathbin/RingTheory/SimpleModule.lean b/Mathbin/RingTheory/SimpleModule.lean
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "f638d299ce012032021d0892d4f824381d798aa7",
+    "rev": "34fd1cd4d80765166ce16a3af30272f36ca073d0",
     "name": "lean3port",
-    "inputRev?": "f638d299ce012032021d0892d4f824381d798aa7"}},
+    "inputRev?": "34fd1cd4d80765166ce16a3af30272f36ca073d0"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "56944fb65c22a653305bf286886c0837a8cc6899",
+    "rev": "37b23dab695396bee39b27841e2475e01df12874",
     "name": "mathlib",
-    "inputRev?": "56944fb65c22a653305bf286886c0837a8cc6899"}},
+    "inputRev?": "37b23dab695396bee39b27841e2475e01df12874"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

diff --git a/lakefile.lean b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-04-06-14"
+def tag : String := "nightly-2023-04-06-16"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"f638d299ce012032021d0892d4f824381d798aa7"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"34fd1cd4d80765166ce16a3af30272f36ca073d0"
 
 @[default_target]
 lean_lib Mathbin where