feat(representation_theory/group_cohomology_resolution): add projective resolution (#17443)

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>

Author: Amelia Livingston

src/algebra/homology/quasi_iso.lean

@@ -3,8 +3,8 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Joël Riou
 -/
-import algebra.homology.homology
 import algebra.homology.homotopy
+import category_theory.abelian.homology
 
 /-!
 # Quasi-isomorphisms
@@ -55,14 +55,158 @@ lemma quasi_iso_of_comp_right (f : C ⟶ D) (g : D ⟶ E) [quasi_iso g] [quasi_i
   quasi_iso f :=
 { is_iso := λ i, is_iso.of_is_iso_fac_right ((homology_functor V c i).map_comp f g).symm }
 
+namespace homotopy_equiv
+
+section
+variables {W : Type*} [category W] [preadditive W] [has_cokernels W] [has_images W]
+  [has_equalizers W] [has_zero_object W] [has_image_maps W]
+
 /-- An homotopy equivalence is a quasi-isomorphism. -/
-lemma homotopy_equiv.to_quasi_iso {W : Type*} [category W] [preadditive W]
-  [has_cokernels W] [has_images W] [has_equalizers W] [has_zero_object W]
-  [has_image_maps W] {C D : homological_complex W c} (e : homotopy_equiv C D) :
+lemma to_quasi_iso {C D : homological_complex W c} (e : homotopy_equiv C D) :
   quasi_iso e.hom :=
 ⟨λ i, begin
   refine ⟨⟨(homology_functor W c i).map e.inv, _⟩⟩,
   simp only [← functor.map_comp, ← (homology_functor W c i).map_id],
   split; apply homology_map_eq_of_homotopy,
   exacts [e.homotopy_hom_inv_id, e.homotopy_inv_hom_id],
 end⟩
+
+lemma to_quasi_iso_inv {C D : homological_complex W c} (e : homotopy_equiv C D) (i : ι) :
+  (@as_iso _ _ _ _ _ (e.to_quasi_iso.1 i)).inv = (homology_functor W c i).map e.inv :=
+begin
+  symmetry,
+  simp only [←iso.hom_comp_eq_id, as_iso_hom, ←functor.map_comp, ←(homology_functor W c i).map_id,
+    homology_map_eq_of_homotopy e.homotopy_hom_inv_id _],
+end
+
+end
+end homotopy_equiv
+namespace homological_complex.hom
+section to_single₀
+variables {W : Type*} [category W] [abelian W]
+
+section
+variables {X : chain_complex W ℕ} {Y : W} (f : X ⟶ ((chain_complex.single₀ _).obj Y))
+  [hf : quasi_iso f]
+
+/-- If a chain map `f : X ⟶ Y[0]` is a quasi-isomorphism, then the cokernel of the differential
+`d : X₁ → X₀` is isomorphic to `Y.` -/
+noncomputable def to_single₀_cokernel_at_zero_iso : cokernel (X.d 1 0) ≅ Y :=
+(X.homology_zero_iso.symm.trans ((@as_iso _ _ _ _ _ (hf.1 0)).trans
+  ((chain_complex.homology_functor_0_single₀ W).app Y)))
+
+lemma to_single₀_cokernel_at_zero_iso_hom_eq [hf : quasi_iso f] :
+  f.to_single₀_cokernel_at_zero_iso.hom = cokernel.desc (X.d 1 0) (f.f 0)
+    (by rw ←f.2 1 0 rfl; exact comp_zero) :=
+begin
+  ext,
+  dunfold to_single₀_cokernel_at_zero_iso chain_complex.homology_zero_iso homology_of_zero_right
+    homology.map_iso chain_complex.homology_functor_0_single₀ cokernel.map,
+  dsimp,
+  simp only [cokernel.π_desc, category.assoc, homology.map_desc, cokernel.π_desc_assoc],
+  simp [homology.desc, iso.refl_inv (X.X 0)],
+end
+
+lemma to_single₀_epi_at_zero [hf : quasi_iso f] :
+  epi (f.f 0) :=
+begin
+  constructor,
+  intros Z g h Hgh,
+  rw [←cokernel.π_desc (X.d 1 0) (f.f 0) (by rw ←f.2 1 0 rfl; exact comp_zero),
+    ←to_single₀_cokernel_at_zero_iso_hom_eq] at Hgh,
+  rw (@cancel_epi _ _ _ _ _ _ (epi_comp _ _) _ _).1 Hgh,
+end
+
+lemma to_single₀_exact_d_f_at_zero [hf : quasi_iso f] :
+  exact (X.d 1 0) (f.f 0) :=
+begin
+  rw preadditive.exact_iff_homology_zero,
+  have h : X.d 1 0 ≫ f.f 0 = 0,
+  { simp only [← f.2 1 0 rfl, chain_complex.single₀_obj_X_d, comp_zero], },
+  refine ⟨h, nonempty.intro (homology_iso_kernel_desc _ _ _ ≪≫ _)⟩,
+  { suffices : is_iso (cokernel.desc _ _ h),
+    { haveI := this, apply kernel.of_mono, },
+      rw ←to_single₀_cokernel_at_zero_iso_hom_eq,
+      apply_instance }
+end
+
+lemma to_single₀_exact_at_succ [hf : quasi_iso f] (n : ℕ) :
+  exact (X.d (n + 2) (n + 1)) (X.d (n + 1) n) :=
+(preadditive.exact_iff_homology_zero _ _).2 ⟨X.d_comp_d _ _ _,
+⟨(chain_complex.homology_succ_iso _ _).symm.trans
+  ((@as_iso _ _ _ _ _ (hf.1 (n + 1))).trans homology_zero_zero)⟩⟩
+
+end
+section
+variables {X : cochain_complex W ℕ} {Y : W}
+  (f : (cochain_complex.single₀ _).obj Y ⟶ X)
+
+/-- If a cochain map `f : Y[0] ⟶ X` is a quasi-isomorphism, then the kernel of the differential
+`d : X₀ → X₁` is isomorphic to `Y.` -/
+noncomputable def from_single₀_kernel_at_zero_iso [hf : quasi_iso f] : kernel (X.d 0 1) ≅ Y :=
+(X.homology_zero_iso.symm.trans ((@as_iso _ _ _ _ _ (hf.1 0)).symm.trans
+  ((cochain_complex.homology_functor_0_single₀ W).app Y)))
+
+lemma from_single₀_kernel_at_zero_iso_inv_eq [hf : quasi_iso f] :
+  f.from_single₀_kernel_at_zero_iso.inv = kernel.lift (X.d 0 1) (f.f 0)
+    (by rw f.2 0 1 rfl; exact zero_comp) :=
+begin
+  ext,
+  dunfold from_single₀_kernel_at_zero_iso cochain_complex.homology_zero_iso homology_of_zero_left
+    homology.map_iso cochain_complex.homology_functor_0_single₀ kernel.map,
+  simp only [iso.trans_inv, iso.app_inv, iso.symm_inv, category.assoc,
+    equalizer_as_kernel, kernel.lift_ι],
+  dsimp,
+  simp only [category.assoc, homology.π_map, cokernel_zero_iso_target_hom,
+    cokernel_iso_of_eq_hom_comp_desc, kernel_subobject_arrow, homology.π_map_assoc,
+    is_iso.inv_comp_eq],
+  simp [homology.π, kernel_subobject_map_comp, iso.refl_hom (X.X 0), category.comp_id],
+end
+
+lemma from_single₀_mono_at_zero [hf : quasi_iso f] :
+  mono (f.f 0) :=
+begin
+  constructor,
+  intros Z g h Hgh,
+  rw [←kernel.lift_ι (X.d 0 1) (f.f 0) (by rw f.2 0 1 rfl; exact zero_comp),
+    ←from_single₀_kernel_at_zero_iso_inv_eq] at Hgh,
+  rw (@cancel_mono _ _ _ _ _ _ (mono_comp _ _) _ _).1 Hgh,
+end
+
+lemma from_single₀_exact_f_d_at_zero [hf : quasi_iso f] :
+  exact (f.f 0) (X.d 0 1) :=
+begin
+  rw preadditive.exact_iff_homology_zero,
+  have h : f.f 0 ≫ X.d 0 1 = 0,
+  { simp only [homological_complex.hom.comm, cochain_complex.single₀_obj_X_d, zero_comp] },
+  refine ⟨h, nonempty.intro (homology_iso_cokernel_lift _ _ _ ≪≫ _)⟩,
+  { suffices : is_iso (kernel.lift (X.d 0 1) (f.f 0) h),
+    { haveI := this, apply cokernel.of_epi },
+    rw ←from_single₀_kernel_at_zero_iso_inv_eq f,
+    apply_instance },
+end
+
+lemma from_single₀_exact_at_succ [hf : quasi_iso f] (n : ℕ) :
+  exact (X.d n (n + 1)) (X.d (n + 1) (n + 2)) :=
+(preadditive.exact_iff_homology_zero _ _).2
+  ⟨X.d_comp_d _ _ _, ⟨(cochain_complex.homology_succ_iso _ _).symm.trans
+  ((@as_iso _ _ _ _ _ (hf.1 (n + 1))).symm.trans homology_zero_zero)⟩⟩
+
+end
+end to_single₀
+end homological_complex.hom
+
+variables {A : Type*} [category A] [abelian A] {B : Type*} [category B] [abelian B]
+  (F : A ⥤ B) [functor.additive F] [preserves_finite_limits F] [preserves_finite_colimits F]
+  [faithful F]
+
+lemma category_theory.functor.quasi_iso_of_map_quasi_iso
+  {C D : homological_complex A c} (f : C ⟶ D)
+  (hf : quasi_iso ((F.map_homological_complex _).map f)) : quasi_iso f :=
+⟨λ i, begin
+  haveI : is_iso (F.map ((homology_functor A c i).map f)),
+  { rw [← functor.comp_map, ← nat_iso.naturality_2 (F.homology_functor_iso i) f,
+      functor.comp_map],
+    apply_instance, },
+  exact is_iso_of_reflects_iso _ F,
+end⟩

src/algebraic_geometry/open_immersion.lean

@@ -110,7 +110,7 @@ variables {X Y : PresheafedSpace.{v} C} {f : X ⟶ Y} (H : is_open_immersion f)
 abbreviation open_functor := H.base_open.is_open_map.functor
 
 /-- An open immersion `f : X ⟶ Y` induces an isomorphism `X ≅ Y|_{f(X)}`. -/
-@[simps] noncomputable
+@[simps hom_c_app] noncomputable
 def iso_restrict : X ≅ Y.restrict H.base_open :=
 PresheafedSpace.iso_of_components (iso.refl _)
 begin
@@ -140,11 +140,11 @@ begin
     transitivity f.c.app x ≫ X.presheaf.map (𝟙 _),
     { congr },
     { erw [X.presheaf.map_id, category.comp_id] } },
-  { simp }
+  { refl, }
 end
 
 @[simp] lemma iso_restrict_inv_of_restrict : H.iso_restrict.inv ≫ f = Y.of_restrict _ :=
-by { rw iso.inv_comp_eq, simp }
+by { rw [iso.inv_comp_eq, iso_restrict_hom_of_restrict] }
 
 instance mono [H : is_open_immersion f] : mono f :=
 by { rw ← H.iso_restrict_hom_of_restrict, apply mono_comp }

src/category_theory/abelian/homology.lean

@@ -1,10 +1,12 @@
 /-
 Copyright (c) 2022 Adam Topaz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Adam Topaz
+Authors: Adam Topaz, Amelia Livingston
 -/
-import category_theory.abelian.exact
+import algebra.homology.additive
 import category_theory.abelian.pseudoelements
+import category_theory.limits.preserves.shapes.kernels
+import category_theory.limits.preserves.shapes.images
 
 /-!
 
@@ -261,5 +263,49 @@ begin
 end
 
 end
-
 end homology
+
+namespace category_theory.functor
+
+variables {ι : Type*} {c : complex_shape ι} {B : Type*} [category B] [abelian B] (F : A ⥤ B)
+  [functor.additive F] [preserves_finite_limits F] [preserves_finite_colimits F]
+
+/-- When `F` is an exact additive functor, `F(Hᵢ(X)) ≅ Hᵢ(F(X))` for `X` a complex. -/
+noncomputable def homology_iso (C : homological_complex A c) (j : ι) :
+  F.obj (C.homology j) ≅ ((F.map_homological_complex _).obj C).homology j :=
+(preserves_cokernel.iso _ _).trans (cokernel.map_iso _ _ ((F.map_iso (image_subobject_iso _)).trans
+  ((preserves_image.iso _ _).symm.trans (image_subobject_iso _).symm))
+  ((F.map_iso (kernel_subobject_iso _)).trans ((preserves_kernel.iso _ _).trans
+  (kernel_subobject_iso _).symm))
+  begin
+    dsimp,
+    ext,
+    simp only [category.assoc, image_to_kernel_arrow],
+    erw [kernel_subobject_arrow', kernel_comparison_comp_ι, image_subobject_arrow'],
+    simp [←F.map_comp],
+  end)
+
+/-- If `F` is an exact additive functor, then `F` commutes with `Hᵢ` (up to natural isomorphism). -/
+noncomputable def homology_functor_iso (i : ι) :
+  homology_functor A c i ⋙ F ≅ F.map_homological_complex c ⋙ homology_functor B c i :=
+nat_iso.of_components (λ X, homology_iso F X i)
+begin
+  intros X Y f,
+  dsimp,
+  rw [←iso.inv_comp_eq, ←category.assoc, ←iso.eq_comp_inv],
+  refine coequalizer.hom_ext _,
+  dsimp [homology_iso],
+  simp only [homology.map, ←category.assoc, cokernel.π_desc],
+  simp only [category.assoc, cokernel_comparison_map_desc, cokernel.π_desc,
+    π_comp_cokernel_comparison, ←F.map_comp],
+  erw ←kernel_subobject_iso_comp_kernel_map_assoc,
+  simp only [homological_complex.hom.sq_from_right,
+    homological_complex.hom.sq_from_left, F.map_homological_complex_map_f, F.map_comp],
+  dunfold homological_complex.d_from homological_complex.hom.next,
+  dsimp,
+  rw [kernel_map_comp_preserves_kernel_iso_inv_assoc, ←F.map_comp_assoc,
+    ←kernel_map_comp_kernel_subobject_iso_inv],
+  any_goals { simp },
+end
+
+end category_theory.functor

src/category_theory/abelian/injective_resolution.lean

@@ -3,8 +3,9 @@ Copyright (c) 2022 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang, Scott Morrison
 -/
+import algebra.homology.quasi_iso
 import category_theory.preadditive.injective_resolution
-import category_theory.abelian.exact
+import category_theory.abelian.homology
 import algebra.homology.homotopy_category
 
 /-!
@@ -276,5 +277,22 @@ instance : has_injective_resolutions C :=
 { out := λ _, infer_instance }
 
 end InjectiveResolution
-
 end category_theory
+namespace homological_complex.hom
+
+variables {C : Type u} [category.{v} C] [abelian C]
+
+/-- If `X` is a cochain complex of injective objects and we have a quasi-isomorphism
+`f : Y[0] ⟶ X`, then `X` is an injective resolution of `Y.` -/
+def homological_complex.hom.from_single₀_InjectiveResolution (X : cochain_complex C ℕ) (Y : C)
+  (f : (cochain_complex.single₀ C).obj Y ⟶ X) [quasi_iso f]
+  (H : ∀ n, injective (X.X n)) :
+  InjectiveResolution Y :=
+{ cocomplex := X,
+  ι := f,
+  injective := H,
+  exact₀ := f.from_single₀_exact_f_d_at_zero,
+  exact := f.from_single₀_exact_at_succ,
+  mono := f.from_single₀_mono_at_zero }
+
+end homological_complex.hom

src/category_theory/abelian/projective.lean

@@ -3,7 +3,8 @@ Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Scott Morrison, Jakob von Raumer
 -/
-import category_theory.abelian.exact
+import algebra.homology.quasi_iso
+import category_theory.abelian.homology
 import category_theory.preadditive.projective_resolution
 
 /-!
@@ -20,7 +21,7 @@ open category_theory
 open category_theory.limits
 open opposite
 
-universes v u
+universes v u v' u'
 
 namespace category_theory
 
@@ -93,5 +94,22 @@ instance : has_projective_resolutions C :=
 { out := λ Z, by apply_instance }
 
 end ProjectiveResolution
-
 end category_theory
+namespace homological_complex.hom
+
+variables {C : Type u} [category.{v} C] [abelian C]
+
+/-- If `X` is a chain complex of projective objects and we have a quasi-isomorphism `f : X ⟶ Y[0]`,
+then `X` is a projective resolution of `Y.` -/
+def to_single₀_ProjectiveResolution {X : chain_complex C ℕ} {Y : C}
+  (f : X ⟶ (chain_complex.single₀ C).obj Y) [quasi_iso f]
+  (H : ∀ n, projective (X.X n)) :
+  ProjectiveResolution Y :=
+{ complex := X,
+  π := f,
+  projective := H,
+  exact₀ := f.to_single₀_exact_d_f_at_zero,
+  exact := f.to_single₀_exact_at_succ,
+  epi := f.to_single₀_epi_at_zero }
+
+end homological_complex.hom

src/category_theory/limits/preserves/shapes/kernels.lean

@@ -114,6 +114,17 @@ begin
   apply_instance
 end
 
+@[reassoc] lemma kernel_map_comp_preserves_kernel_iso_inv {X' Y' : C} (g : X' ⟶ Y') [has_kernel g]
+  [has_kernel (G.map g)] [preserves_limit (parallel_pair g 0) G] (p : X ⟶ X') (q : Y ⟶ Y')
+  (hpq : f ≫ q = p ≫ g) :
+  kernel.map (G.map f) (G.map g) (G.map p) (G.map q)
+    (by rw [←G.map_comp, hpq, G.map_comp]) ≫ (preserves_kernel.iso G _).inv
+  = (preserves_kernel.iso G _).inv ≫ G.map (kernel.map f g p q hpq) :=
+begin
+  rw [iso.comp_inv_eq, category.assoc, preserves_kernel.iso_hom, iso.eq_inv_comp],
+  exact kernel_comparison_comp_kernel_map _ _ _ _ _ _,
+end
+
 end kernels
 
 section cokernels
@@ -206,6 +217,17 @@ begin
   apply_instance
 end
 
+@[reassoc] lemma preserves_cokernel_iso_comp_cokernel_map {X' Y' : C} (g : X' ⟶ Y')
+  [has_cokernel g] [has_cokernel (G.map g)] [preserves_colimit (parallel_pair g 0) G]
+  (p : X ⟶ X') (q : Y ⟶ Y') (hpq : f ≫ q = p ≫ g) :
+  (preserves_cokernel.iso G _).hom ≫ cokernel.map (G.map f) (G.map g) (G.map p) (G.map q)
+    (by rw [←G.map_comp, hpq, G.map_comp]) =
+  G.map (cokernel.map f g p q hpq) ≫ (preserves_cokernel.iso G _).hom :=
+begin
+  rw [←iso.comp_inv_eq, category.assoc, ←iso.eq_inv_comp],
+  exact cokernel_map_comp_cokernel_comparison _ _ _ _ _ _,
+end
+
 end cokernels
 
 end category_theory.limits