Merge master into nightly-testing

Author: leanprover-community-mathlib4-bot

Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean

@@ -66,24 +66,33 @@ def Γ [IsIdempotentComplete C] [HasFiniteCoproducts C] : ChainComplex C ℕ ⥤
 
 variable [IsIdempotentComplete C] [HasFiniteCoproducts C]
 
-theorem hN₁ :
-    (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor =
-      N₁ :=
-  Functor.congr_obj (functorExtension₁_comp_whiskeringLeft_toKaroubi _ _) N₁
-set_option linter.uppercaseLean3 false in
-#align category_theory.idempotents.dold_kan.hN₁ CategoryTheory.Idempotents.DoldKan.hN₁
-
-theorem hΓ₀ :
-    (toKaroubiEquivalence (ChainComplex C ℕ)).functor ⋙ Preadditive.DoldKan.equivalence.inverse =
+/-- A reformulation of the isomorphism `toKaroubi (SimplicialObject C) ⋙ N₂ ≅ N₁` -/
+def isoN₁ :
+    (toKaroubiEquivalence (SimplicialObject C)).functor ⋙
+      Preadditive.DoldKan.equivalence.functor ≅ N₁ := toKaroubiCompN₂IsoN₁
+
+@[simp]
+lemma isoN₁_hom_app_f (X : SimplicialObject C) :
+    (isoN₁.hom.app X).f = PInfty := rfl
+
+/-- A reformulation of the canonical isomorphism
+`toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ≅ Γ ⋙ toKaroubi (SimplicialObject C)`. -/
+def isoΓ₀ :
+    (toKaroubiEquivalence (ChainComplex C ℕ)).functor ⋙ Preadditive.DoldKan.equivalence.inverse ≅
       Γ ⋙ (toKaroubiEquivalence _).functor :=
-  Functor.congr_obj (functorExtension₂_comp_whiskeringLeft_toKaroubi _ _) Γ₀
-#align category_theory.idempotents.dold_kan.hΓ₀ CategoryTheory.Idempotents.DoldKan.hΓ₀
+  (functorExtension₂CompWhiskeringLeftToKaroubiIso _ _).app Γ₀
+
+@[simp]
+lemma N₂_map_isoΓ₀_hom_app_f (X : ChainComplex C ℕ) :
+    (N₂.map (isoΓ₀.hom.app X)).f = PInfty := by
+  ext
+  apply comp_id
 
 /-- The Dold-Kan equivalence for pseudoabelian categories given
 by the functors `N` and `Γ`. It is obtained by applying the results in
 `Compatibility.lean` to the equivalence `Preadditive.DoldKan.Equivalence`. -/
 def equivalence : SimplicialObject C ≌ ChainComplex C ℕ :=
-  Compatibility.equivalence (eqToIso hN₁) (eqToIso hΓ₀)
+  Compatibility.equivalence isoN₁ isoΓ₀
 #align category_theory.idempotents.dold_kan.equivalence CategoryTheory.Idempotents.DoldKan.equivalence
 
 theorem equivalence_functor : (equivalence : SimplicialObject C ≌ _).functor = N :=
@@ -98,12 +107,11 @@ theorem equivalence_inverse : (equivalence : SimplicialObject C ≌ _).inverse =
 for the construction of our counit isomorphism `η` -/
 theorem hη :
     Compatibility.τ₀ =
-      Compatibility.τ₁ (eqToIso hN₁) (eqToIso hΓ₀)
+      Compatibility.τ₁ isoN₁ isoΓ₀
         (N₁Γ₀ : Γ ⋙ N₁ ≅ (toKaroubiEquivalence (ChainComplex C ℕ)).functor) := by
   ext K : 3
-  simp only [Compatibility.τ₀_hom_app, Compatibility.τ₁_hom_app, eqToIso.hom]
-  refine' (N₂Γ₂_compatible_with_N₁Γ₀ K).trans _
-  simp only [N₂Γ₂ToKaroubiIso_hom, eqToHom_map, eqToHom_app, eqToHom_trans_assoc]
+  simp only [Compatibility.τ₀_hom_app, Compatibility.τ₁_hom_app]
+  refine' (N₂Γ₂_compatible_with_N₁Γ₀ K).trans (by simp )
 #align category_theory.idempotents.dold_kan.hη CategoryTheory.Idempotents.DoldKan.hη
 
 /-- The counit isomorphism induced by `N₁Γ₀` -/
@@ -119,23 +127,26 @@ theorem equivalence_counitIso :
 #align category_theory.idempotents.dold_kan.equivalence_counit_iso CategoryTheory.Idempotents.DoldKan.equivalence_counitIso
 
 theorem hε :
-    Compatibility.υ (eqToIso hN₁) =
+    Compatibility.υ (isoN₁) =
       (Γ₂N₁ : (toKaroubiEquivalence _).functor ≅
           (N₁ : SimplicialObject C ⥤ _) ⋙ Preadditive.DoldKan.equivalence.inverse) := by
+  dsimp only [isoN₁]
   ext1
   rw [← cancel_epi Γ₂N₁.inv, Iso.inv_hom_id]
   ext X : 2
   rw [NatTrans.comp_app]
   erw [compatibility_Γ₂N₁_Γ₂N₂_natTrans X]
   rw [Compatibility.υ_hom_app, Preadditive.DoldKan.equivalence_unitIso, Iso.app_inv, assoc]
   erw [← NatTrans.comp_app_assoc, IsIso.hom_inv_id]
-  rw [NatTrans.id_app, id_comp, NatTrans.id_app, eqToIso.hom, eqToHom_app, eqToHom_map]
-  rw [compatibility_Γ₂N₁_Γ₂N₂_inv_app, eqToHom_trans, eqToHom_refl]
+  rw [NatTrans.id_app, id_comp, NatTrans.id_app, Γ₂N₂ToKaroubiIso_inv_app]
+  dsimp only [Preadditive.DoldKan.equivalence_inverse, Preadditive.DoldKan.Γ]
+  rw [← Γ₂.map_comp, Iso.inv_hom_id_app, Γ₂.map_id]
+  rfl
 #align category_theory.idempotents.dold_kan.hε CategoryTheory.Idempotents.DoldKan.hε
 
 /-- The unit isomorphism induced by `Γ₂N₁`. -/
 def ε : 𝟭 (SimplicialObject C) ≅ N ⋙ Γ :=
-  Compatibility.equivalenceUnitIso (eqToIso hΓ₀) Γ₂N₁
+  Compatibility.equivalenceUnitIso isoΓ₀ Γ₂N₁
 #align category_theory.idempotents.dold_kan.ε CategoryTheory.Idempotents.DoldKan.ε
 
 theorem equivalence_unitIso :

Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean

@@ -63,9 +63,17 @@ def N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ) :=
 set_option linter.uppercaseLean3 false in
 #align algebraic_topology.dold_kan.N₂ AlgebraicTopology.DoldKan.N₂
 
--- porting note: added to ease the port of `AlgebraicTopology.DoldKan.NCompGamma`
-lemma compatibility_N₁_N₂ : toKaroubi (SimplicialObject C) ⋙ N₂ = N₁ :=
-  Functor.congr_obj (functorExtension₁_comp_whiskeringLeft_toKaroubi _ _) N₁
+/-- The canonical isomorphism `toKaroubi (SimplicialObject C) ⋙ N₂ ≅ N₁`. -/
+def toKaroubiCompN₂IsoN₁ : toKaroubi (SimplicialObject C) ⋙ N₂ ≅ N₁ :=
+  (functorExtension₁CompWhiskeringLeftToKaroubiIso _ _).app N₁
+
+@[simp]
+lemma toKaroubiCompN₂IsoN₁_hom_app (X : SimplicialObject C) :
+    (toKaroubiCompN₂IsoN₁.hom.app X).f = PInfty := rfl
+
+@[simp]
+lemma toKaroubiCompN₂IsoN₁_inv_app (X : SimplicialObject C) :
+    (toKaroubiCompN₂IsoN₁.inv.app X).f = PInfty := rfl
 
 end DoldKan
 

Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean

@@ -119,24 +119,46 @@ set_option linter.uppercaseLean3 false in
 -- Porting note: added to speed up elaboration
 attribute [irreducible] N₁Γ₀
 
-theorem N₂Γ₂_toKaroubi : toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ = Γ₀ ⋙ N₁ := by
-  have h := Functor.congr_obj (functorExtension₂_comp_whiskeringLeft_toKaroubi
-    (ChainComplex C ℕ) (SimplicialObject C)) Γ₀
-  have h' := Functor.congr_obj (functorExtension₁_comp_whiskeringLeft_toKaroubi
-    (SimplicialObject C) (ChainComplex C ℕ)) N₁
-  dsimp [N₂, Γ₂, functorExtension₁] at h h' ⊢
-  rw [← Functor.assoc, h, Functor.assoc, h']
-set_option linter.uppercaseLean3 false in
-#align algebraic_topology.dold_kan.N₂Γ₂_to_karoubi AlgebraicTopology.DoldKan.N₂Γ₂_toKaroubi
-
 /-- Compatibility isomorphism between `toKaroubi _ ⋙ Γ₂ ⋙ N₂` and `Γ₀ ⋙ N₁` which
 are functors `ChainComplex C ℕ ⥤ Karoubi (ChainComplex C ℕ)`. -/
-@[simps!]
 def N₂Γ₂ToKaroubiIso : toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ ≅ Γ₀ ⋙ N₁ :=
-  eqToIso N₂Γ₂_toKaroubi
+  calc
+    toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ ≅
+      toKaroubi (ChainComplex C ℕ) ⋙ (Γ₂ ⋙ N₂) := (Functor.associator _ _ _).symm
+    _ ≅ (Γ₀ ⋙ toKaroubi (SimplicialObject C)) ⋙ N₂ :=
+        isoWhiskerRight ((functorExtension₂CompWhiskeringLeftToKaroubiIso _ _).app Γ₀) N₂
+    _ ≅ Γ₀ ⋙ toKaroubi (SimplicialObject C) ⋙ N₂ := Functor.associator _ _ _
+    _ ≅ Γ₀ ⋙ N₁ :=
+      isoWhiskerLeft Γ₀ ((functorExtension₁CompWhiskeringLeftToKaroubiIso _ _).app N₁)
 set_option linter.uppercaseLean3 false in
 #align algebraic_topology.dold_kan.N₂Γ₂_to_karoubi_iso AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso
 
+@[simp]
+lemma N₂Γ₂ToKaroubiIso_hom_app (X : ChainComplex C ℕ) :
+    (N₂Γ₂ToKaroubiIso.hom.app X).f = PInfty := by
+  ext n
+  dsimp [N₂Γ₂ToKaroubiIso]
+  simp only [comp_id, assoc, PInfty_f_idem]
+  conv_rhs =>
+    rw [← PInfty_f_idem]
+  congr 1
+  apply (Γ₀.splitting X).hom_ext'
+  intro A
+  rw [Splitting.ι_desc_assoc, assoc]
+  apply id_comp
+
+@[simp]
+lemma N₂Γ₂ToKaroubiIso_inv_app (X : ChainComplex C ℕ) :
+    (N₂Γ₂ToKaroubiIso.inv.app X).f = PInfty := by
+  ext n
+  dsimp [N₂Γ₂ToKaroubiIso]
+  simp only [comp_id, PInfty_f_idem_assoc, AlternatingFaceMapComplex.obj_X, Γ₀_obj_obj]
+  convert comp_id _
+  apply (Γ₀.splitting X).hom_ext'
+  intro A
+  rw [Splitting.ι_desc]
+  erw [comp_id, id_comp]
+
 -- Porting note: added to speed up elaboration
 attribute [irreducible] N₂Γ₂ToKaroubiIso
 
@@ -151,16 +173,15 @@ set_option linter.uppercaseLean3 false in
 theorem N₂Γ₂_inv_app_f_f (X : Karoubi (ChainComplex C ℕ)) (n : ℕ) :
     (N₂Γ₂.inv.app X).f.f n =
       X.p.f n ≫ (Γ₀.splitting X.X).ιSummand (Splitting.IndexSet.id (op [n])) := by
-  simp only [N₂Γ₂, Functor.preimageIso, Iso.trans,
-    whiskeringLeft_obj_preimage_app, N₂Γ₂ToKaroubiIso_inv, assoc,
-    Functor.id_map, NatTrans.comp_app, eqToHom_app, Karoubi.comp_f,
-    Karoubi.eqToHom_f, Karoubi.decompId_p_f, HomologicalComplex.comp_f,
-    N₁Γ₀_inv_app_f_f, Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f,
-    Functor.comp_map, Functor.comp_obj, Karoubi.decompId_i_f,
-    eqToHom_refl, comp_id, N₂_map_f_f, Γ₂_map_f_app, N₁_obj_p,
-    PInfty_on_Γ₀_splitting_summand_eq_self_assoc, toKaroubi_obj_X,
-    Splitting.ι_desc, Splitting.IndexSet.id_fst, SimplexCategory.len_mk, unop_op,
-    Karoubi.HomologicalComplex.p_idem_assoc]
+  dsimp [N₂Γ₂]
+  simp only [whiskeringLeft_obj_preimage_app, NatTrans.comp_app, Functor.comp_map,
+    Karoubi.comp_f, N₂Γ₂ToKaroubiIso_inv_app, HomologicalComplex.comp_f,
+    N₁Γ₀_inv_app_f_f, toKaroubi_obj_X, Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f,
+    Γ₀.obj_obj, PInfty_on_Γ₀_splitting_summand_eq_self, N₂_map_f_f,
+    Γ₂_map_f_app, unop_op, Karoubi.decompId_p_f, PInfty_f_idem_assoc,
+    PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Splitting.IndexSet.id_fst, SimplexCategory.len_mk,
+    Splitting.ι_desc]
+  apply Karoubi.HomologicalComplex.p_idem_assoc
 set_option linter.uppercaseLean3 false in
 #align algebraic_topology.dold_kan.N₂Γ₂_inv_app_f_f AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f
 

Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean

@@ -172,43 +172,39 @@ end Γ₂N₁
 
 -- porting note: removed @[simps] attribute because it was creating timeouts
 /-- The compatibility isomorphism relating `N₂ ⋙ Γ₂` and `N₁ ⋙ Γ₂`. -/
-def compatibility_Γ₂N₁_Γ₂N₂ : toKaroubi (SimplicialObject C) ⋙ N₂ ⋙ Γ₂ ≅ N₁ ⋙ Γ₂ :=
-  eqToIso (by rw [← Functor.assoc, compatibility_N₁_N₂])
+def Γ₂N₂ToKaroubiIso : toKaroubi (SimplicialObject C) ⋙ N₂ ⋙ Γ₂ ≅ N₁ ⋙ Γ₂ :=
+  (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight toKaroubiCompN₂IsoN₁ Γ₂
 set_option linter.uppercaseLean3 false in
-#align algebraic_topology.dold_kan.compatibility_Γ₂N₁_Γ₂N₂ AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂
+#align algebraic_topology.dold_kan.compatibility_Γ₂N₁_Γ₂N₂ AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso
 
--- porting note: no @[simp] attribute because this would trigger a timeout
-lemma compatibility_Γ₂N₁_Γ₂N₂_hom_app (X : SimplicialObject C) :
-    compatibility_Γ₂N₁_Γ₂N₂.hom.app X =
-      eqToHom (by rw [← Functor.assoc, compatibility_N₁_N₂]) := by
-  dsimp only [compatibility_Γ₂N₁_Γ₂N₂, CategoryTheory.eqToIso]
-  apply eqToHom_app
+@[simp]
+lemma Γ₂N₂ToKaroubiIso_hom_app (X : SimplicialObject C) :
+    Γ₂N₂ToKaroubiIso.hom.app X = Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) := by
+  simp [Γ₂N₂ToKaroubiIso]
 
--- Porting note: added to speed up elaboration
-attribute [irreducible] compatibility_Γ₂N₁_Γ₂N₂
+@[simp]
+lemma Γ₂N₂ToKaroubiIso_inv_app (X : SimplicialObject C) :
+    Γ₂N₂ToKaroubiIso.inv.app X = Γ₂.map (toKaroubiCompN₂IsoN₁.inv.app X) := by
+  simp [Γ₂N₂ToKaroubiIso]
 
-lemma compatibility_Γ₂N₁_Γ₂N₂_inv_app (X : SimplicialObject C) :
-    compatibility_Γ₂N₁_Γ₂N₂.inv.app X =
-      eqToHom (by rw [← Functor.assoc, compatibility_N₁_N₂]) := by
-  rw [← cancel_mono (compatibility_Γ₂N₁_Γ₂N₂.hom.app X), Iso.inv_hom_id_app,
-    compatibility_Γ₂N₁_Γ₂N₂_hom_app, eqToHom_trans, eqToHom_refl]
+-- Porting note: added to speed up elaboration
+attribute [irreducible] Γ₂N₂ToKaroubiIso
 
 namespace Γ₂N₂
 
 /-- The natural transformation `N₂ ⋙ Γ₂ ⟶ 𝟭 (SimplicialObject C)`. -/
 def natTrans : (N₂ : Karoubi (SimplicialObject C) ⥤ _) ⋙ Γ₂ ⟶ 𝟭 _ :=
   ((whiskeringLeft _ _ _).obj (toKaroubi (SimplicialObject C))).preimage
-    (by exact compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans)
+    (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans)
 set_option linter.uppercaseLean3 false in
 #align algebraic_topology.dold_kan.Γ₂N₂.nat_trans AlgebraicTopology.DoldKan.Γ₂N₂.natTrans
 
 theorem natTrans_app_f_app (P : Karoubi (SimplicialObject C)) :
-    Γ₂N₂.natTrans.app P = by
-      exact (N₂ ⋙ Γ₂).map P.decompId_i ≫
-        (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p := by
+    Γ₂N₂.natTrans.app P =
+      (N₂ ⋙ Γ₂).map P.decompId_i ≫
+        (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p := by
   dsimp only [natTrans]
-  rw [whiskeringLeft_obj_preimage_app
-    (compatibility_Γ₂N₁_Γ₂N₂.hom ≫ Γ₂N₁.natTrans : _ ⟶ toKaroubi _ ⋙ 𝟭 _) P, Functor.id_map]
+  simp only [whiskeringLeft_obj_preimage_app, Functor.id_map, assoc]
 set_option linter.uppercaseLean3 false in
 #align algebraic_topology.dold_kan.Γ₂N₂.nat_trans_app_f_app AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app
 
@@ -219,7 +215,7 @@ end Γ₂N₂
 
 theorem compatibility_Γ₂N₁_Γ₂N₂_natTrans (X : SimplicialObject C) :
     Γ₂N₁.natTrans.app X =
-      (compatibility_Γ₂N₁_Γ₂N₂.app X).inv ≫
+      (Γ₂N₂ToKaroubiIso.app X).inv ≫
         Γ₂N₂.natTrans.app ((toKaroubi (SimplicialObject C)).obj X) := by
   rw [Γ₂N₂.natTrans_app_f_app]
   dsimp only [Karoubi.decompId_i_toKaroubi, Karoubi.decompId_p_toKaroubi, Functor.comp_map,
@@ -239,14 +235,16 @@ theorem identity_N₂_objectwise (P : Karoubi (SimplicialObject C)) :
   have eq₂ : (Γ₀.splitting (N₂.obj P).X).ιSummand (Splitting.IndexSet.id (op [n])) ≫
       (N₂.map (Γ₂N₂.natTrans.app P)).f.f n = PInfty.f n ≫ P.p.app (op [n]) := by
     dsimp
-    simp only [assoc, Γ₂N₂.natTrans_app_f_app, Functor.comp_map, NatTrans.comp_app,
-      Karoubi.comp_f, compatibility_Γ₂N₁_Γ₂N₂_hom_app, eqToHom_refl, Karoubi.eqToHom_f,
-      PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Functor.comp_obj]
-    dsimp [N₂]
-    simp only [Splitting.ι_desc_assoc, assoc, id_comp, unop_op,
-      Splitting.IndexSet.id_fst, len_mk, Splitting.IndexSet.e,
-      Splitting.IndexSet.id_snd_coe, op_id, P.X.map_id, id_comp,
-      PInfty_f_naturality_assoc, PInfty_f_idem_assoc, app_idem]
+    rw [PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Γ₂N₂.natTrans_app_f_app]
+    dsimp
+    rw [Γ₂N₂ToKaroubiIso_hom_app, assoc, Splitting.ι_desc_assoc, assoc, assoc]
+    dsimp [toKaroubi]
+    rw [Splitting.ι_desc_assoc]
+    dsimp
+    simp only [assoc, Splitting.ι_desc_assoc, unop_op, Splitting.IndexSet.id_fst,
+      len_mk, NatTrans.naturality, PInfty_f_idem_assoc,
+      PInfty_f_naturality_assoc, app_idem_assoc]
+    erw [P.X.map_id, comp_id]
   simp only [Karoubi.comp_f, HomologicalComplex.comp_f, Karoubi.id_eq, N₂_obj_p_f, assoc,
     eq₁, eq₂, PInfty_f_naturality_assoc, app_idem, PInfty_f_idem_assoc]
 set_option linter.uppercaseLean3 false in