From 78c397526553c364691388fabe75d3b98ceba145 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 9 Feb 2022 07:16:44 +0000 Subject: [PATCH] feat(category_theory/pseudoabelian/basic): basic facts and contructions about pseudoabelian categories (#11817) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> --- src/category_theory/idempotents/basic.lean | 207 +++++++++++++++ src/category_theory/idempotents/karoubi.lean | 261 +++++++++++++++++++ src/category_theory/preadditive/default.lean | 12 + 3 files changed, 480 insertions(+) create mode 100644 src/category_theory/idempotents/basic.lean create mode 100644 src/category_theory/idempotents/karoubi.lean diff --git a/src/category_theory/idempotents/basic.lean b/src/category_theory/idempotents/basic.lean new file mode 100644 index 0000000000000..31acc5781d0e0 --- /dev/null +++ b/src/category_theory/idempotents/basic.lean @@ -0,0 +1,207 @@ +/- +Copyright (c) 2022 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ + +import category_theory.abelian.basic + +/-! +# Idempotent complete categories + +In this file, we define the notion of idempotent complete categories +(also known as Karoubian categories, or pseudoabelian in the case of +preadditive categories). + +## Main definitions + +- `is_idempotent_complete C` expresses that `C` is idempotent complete, i.e. +all idempotents in `C` split. Other caracterisations of idempotent completeness are given +by `is_idempotent_complete_iff_has_equalizer_of_id_and_idempotent` and +`is_idempotent_complete_iff_idempotents_have_kernels`. +- `is_idempotent_complete_of_abelian` expresses that abelian categories are +idempotent complete. +- `is_idempotent_complete_iff_of_equivalence` expresses that if two categories `C` and `D` +are equivalent, then `C` is idempotent complete iff `D` is. +- `is_idempotent_complete_iff_opposite` expresses that `Cᵒᵖ` is idempotent complete +iff `C` is. + +## References +* [Stacks: Karoubian categories] https://stacks.math.columbia.edu/tag/09SF + +-/ + +open category_theory +open category_theory.category +open category_theory.limits +open category_theory.preadditive +open opposite + +namespace category_theory + +variables (C : Type*) [category C] + +/-- A category is idempotent complete iff all idempotents endomorphisms `p` +split as a composition `p = e ≫ i` with `i ≫ e = 𝟙 _` -/ +class is_idempotent_complete : Prop := +(idempotents_split : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → + ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p) + +namespace idempotents + +/-- A category is idempotent complete iff for all idempotents endomorphisms, +the equalizer of the identity and this idempotent exists. -/ +lemma is_idempotent_complete_iff_has_equalizer_of_id_and_idempotent : + is_idempotent_complete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → has_equalizer (𝟙 X) p := +begin + split, + { introI, + intros X p hp, + rcases is_idempotent_complete.idempotents_split X p hp with ⟨Y, i, e, ⟨h₁, h₂⟩⟩, + exact ⟨nonempty.intro + { cone := fork.of_ι i + (show i ≫ 𝟙 X = i ≫ p, by rw [comp_id, ← h₂, ← assoc, h₁, id_comp]), + is_limit := begin + apply fork.is_limit.mk', + intro s, + refine ⟨s.ι ≫ e, _⟩, + split, + { erw [assoc, h₂, ← limits.fork.condition s, comp_id], }, + { intros m hm, + erw [← hm], + simp only [← hm, assoc, fork.ι_eq_app_zero, + fork.of_ι_π_app, h₁], + erw comp_id m, } + end }⟩, }, + { intro h, + refine ⟨_⟩, + intros X p hp, + haveI := h X p hp, + use equalizer (𝟙 X) p, + use equalizer.ι (𝟙 X) p, + use equalizer.lift p (show p ≫ 𝟙 X = p ≫ p, by rw [hp, comp_id]), + split, + { ext, + rw [assoc, equalizer.lift_ι, id_comp], + conv { to_rhs, erw [← comp_id (equalizer.ι (𝟙 X) p)], }, + exact (limits.fork.condition (equalizer.fork (𝟙 X) p)).symm, }, + { rw [equalizer.lift_ι], }, } +end + +variables {C} + +/-- In a preadditive category, when `p : X ⟶ X` is idempotent, +then `𝟙 X - p` is also idempotent. -/ +lemma idempotence_of_id_sub_idempotent [preadditive C] + {X : C} (p : X ⟶ X) (hp : p ≫ p = p) : + (𝟙 _ - p) ≫ (𝟙 _ - p) = (𝟙 _ - p) := +by simp only [comp_sub, sub_comp, id_comp, comp_id, hp, sub_self, sub_zero] + +variables (C) + +/-- A preadditive category is pseudoabelian iff all idempotent endomorphisms have a kernel. -/ +lemma is_idempotent_complete_iff_idempotents_have_kernels [preadditive C] : + is_idempotent_complete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → has_kernel p := +begin + rw is_idempotent_complete_iff_has_equalizer_of_id_and_idempotent, + split, + { intros h X p hp, + haveI := h X (𝟙 _ - p) (idempotence_of_id_sub_idempotent p hp), + convert has_kernel_of_has_equalizer (𝟙 X) (𝟙 X - p), + rw [sub_sub_cancel], }, + { intros h X p hp, + haveI : has_kernel (𝟙 _ - p) := h X (𝟙 _ - p) (idempotence_of_id_sub_idempotent p hp), + apply preadditive.has_limit_parallel_pair, }, +end + +/-- An abelian category is idempotent complete. -/ +@[priority 100] +instance is_idempotent_complete_of_abelian (D : Type*) [category D] [abelian D] : + is_idempotent_complete D := +by { rw is_idempotent_complete_iff_idempotents_have_kernels, intros, apply_instance, } + +variables {C} + +lemma split_imp_of_iso {X X' : C} (φ : X ≅ X') (p : X ⟶ X) (p' : X' ⟶ X') + (hpp' : p ≫ φ.hom = φ.hom ≫ p') + (h : ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p) : + (∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') := +begin + rcases h with ⟨Y, i, e, ⟨h₁, h₂⟩⟩, + use [Y, i ≫ φ.hom, φ.inv ≫ e], + split, + { slice_lhs 2 3 { rw φ.hom_inv_id, }, + rw [id_comp, h₁], }, + { slice_lhs 2 3 { rw h₂, }, + rw [hpp', ← assoc, φ.inv_hom_id, id_comp], } +end + +lemma split_iff_of_iso {X X' : C} (φ : X ≅ X') (p : X ⟶ X) (p' : X' ⟶ X') + (hpp' : p ≫ φ.hom = φ.hom ≫ p') : + (∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p) ↔ + (∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') := +begin + split, + { exact split_imp_of_iso φ p p' hpp', }, + { apply split_imp_of_iso φ.symm p' p, + rw [← comp_id p, ← φ.hom_inv_id], + slice_rhs 2 3 { rw hpp', }, + slice_rhs 1 2 { erw φ.inv_hom_id, }, + simpa only [id_comp], }, +end + +lemma equivalence.is_idempotent_complete {D : Type*} [category D] (ε : C ≌ D) + (h : is_idempotent_complete C) : is_idempotent_complete D := +begin + refine ⟨_⟩, + intros X' p hp, + let φ := ε.counit_iso.symm.app X', + erw split_iff_of_iso φ p (φ.inv ≫ p ≫ φ.hom) + (by { slice_rhs 1 2 { rw φ.hom_inv_id, }, rw id_comp,}), + rcases is_idempotent_complete.idempotents_split (ε.inverse.obj X') (ε.inverse.map p) + (by rw [← ε.inverse.map_comp, hp]) with ⟨Y, i, e, ⟨h₁,h₂⟩⟩, + use [ε.functor.obj Y, ε.functor.map i, ε.functor.map e], + split, + { rw [← ε.functor.map_comp, h₁, ε.functor.map_id], }, + { simpa only [← ε.functor.map_comp, h₂, equivalence.fun_inv_map], }, +end + +/-- If `C` and `D` are equivalent categories, that `C` is idempotent complete iff `D` is. -/ +lemma is_idempotent_complete_iff_of_equivalence {D : Type*} [category D] (ε : C ≌ D) : + is_idempotent_complete C ↔ is_idempotent_complete D := +begin + split, + { exact equivalence.is_idempotent_complete ε, }, + { exact equivalence.is_idempotent_complete ε.symm, }, +end + +lemma is_idempotent_complete_of_is_idempotent_complete_opposite + (h : is_idempotent_complete Cᵒᵖ) : is_idempotent_complete C := +begin + refine ⟨_⟩, + intros X p hp, + rcases is_idempotent_complete.idempotents_split (op X) p.op + (by rw [← op_comp, hp]) with ⟨Y, i, e, ⟨h₁, h₂⟩⟩, + use [Y.unop, e.unop, i.unop], + split, + { simpa only [← unop_comp, h₁], }, + { simpa only [← unop_comp, h₂], }, +end + +lemma is_idempotent_complete_iff_opposite : + is_idempotent_complete Cᵒᵖ ↔ is_idempotent_complete C := +begin + split, + { exact is_idempotent_complete_of_is_idempotent_complete_opposite, }, + { intro h, + apply is_idempotent_complete_of_is_idempotent_complete_opposite, + rw is_idempotent_complete_iff_of_equivalence (op_op_equivalence C), + exact h, }, +end + +instance [is_idempotent_complete C] : is_idempotent_complete (Cᵒᵖ) := +by rwa is_idempotent_complete_iff_opposite + +end idempotents + +end category_theory diff --git a/src/category_theory/idempotents/karoubi.lean b/src/category_theory/idempotents/karoubi.lean new file mode 100644 index 0000000000000..47dba7e667ba0 --- /dev/null +++ b/src/category_theory/idempotents/karoubi.lean @@ -0,0 +1,261 @@ +/- +Copyright (c) 2022 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ + +import category_theory.idempotents.basic +import category_theory.preadditive.additive_functor +import category_theory.equivalence + +/-! +# The Karoubi envelope of a category + +In this file, we define the Karoubi envelope `karoubi C` of a category `C`. + +## Main constructions and definitions + +- `karoubi C` is the Karoubi envelope of a category `C`: it is an idempotent +complete category. It is also preadditive when `C` is preadditive. +- `to_karoubi C : C ⥤ karoubi C` is a fully faithful functor, which is an equivalence +(`to_karoubi_is_equivalence`) when `C` is idempotent complete. + +-/ + +noncomputable theory + +open category_theory.category +open category_theory.preadditive +open category_theory.limits +open_locale big_operators + +namespace category_theory + +variables (C : Type*) [category C] + +namespace idempotents + +/-- In a preadditive category `C`, when an object `X` decomposes as `X ≅ P ⨿ Q`, one may +consider `P` as a direct factor of `X` and up to unique isomorphism, it is determined by the +obvious idempotent `X ⟶ P ⟶ X` which is the projector on `P` with kernel `Q`. More generally, +one may define a formal direct factor of an object `X : C` : it consists of an idempotent +`p : X ⟶ X` which is thought as the "formal image" of `p`. The type `karoubi C` shall be the +type of the objects of the karoubi enveloppe of `C`. It makes sense for any category `C`. -/ +@[nolint has_inhabited_instance] +structure karoubi := (X : C) (p : X ⟶ X) (idempotence : p ≫ p = p) + +namespace karoubi + +variables {C} + +@[ext] +lemma ext {P Q : karoubi C} (h_X : P.X = Q.X) + (h_p : P.p ≫ eq_to_hom h_X = eq_to_hom h_X ≫ Q.p) : P = Q := +begin + cases P, + cases Q, + dsimp at h_X h_p, + subst h_X, + simpa only [true_and, eq_self_iff_true, id_comp, eq_to_hom_refl, + heq_iff_eq, comp_id] using h_p, +end + +/-- A morphism `P ⟶ Q` in the category `karoubi C` is a morphism in the underlying category +`C` which satisfies a relation, which in the preadditive case, expresses that it induces a +map between the corresponding "formal direct factors" and that it vanishes on the complement +formal direct factor. -/ +@[ext] +structure hom (P Q : karoubi C) := (f : P.X ⟶ Q.X) (comm : f = P.p ≫ f ≫ Q.p) + +instance [preadditive C] (P Q : karoubi C) : inhabited (hom P Q) := +⟨⟨0, by rw [zero_comp, comp_zero]⟩⟩ + +@[simp] +lemma hom_ext {P Q : karoubi C} {f g : hom P Q} : f = g ↔ f.f = g.f := +begin + split, + { intro h, rw h, }, + { ext, } +end + +@[simp, reassoc] +lemma p_comp {P Q : karoubi C} (f : hom P Q) : P.p ≫ f.f = f.f := +by rw [f.comm, ← assoc, P.idempotence] + +@[simp, reassoc] +lemma comp_p {P Q : karoubi C} (f : hom P Q) : f.f ≫ Q.p = f.f := +by rw [f.comm, assoc, assoc, Q.idempotence] + +lemma p_comm {P Q : karoubi C} (f : hom P Q) : P.p ≫ f.f = f.f ≫ Q.p := +by rw [p_comp, comp_p] + +lemma comp_proof {P Q R : karoubi C} (g : hom Q R) (f : hom P Q) : + f.f ≫ g.f = P.p ≫ (f.f ≫ g.f) ≫ R.p := +by rw [assoc, comp_p, ← assoc, p_comp] + +/-- The category structure on the karoubi envelope of a category. -/ +instance : category (karoubi C) := +{ hom := karoubi.hom, + id := λ P, ⟨P.p, by { repeat { rw P.idempotence, }, }⟩, + comp := λ P Q R f g, ⟨f.f ≫ g.f, karoubi.comp_proof g f⟩, + id_comp' := λ P Q f, by { ext, simp only [karoubi.p_comp], }, + comp_id' := λ P Q f, by { ext, simp only [karoubi.comp_p], }, + assoc' := λ P Q R S f g h, by { ext, simp only [category.assoc], }, } + +@[simp] +lemma comp {P Q R : karoubi C} (f : P ⟶ Q) (g : Q ⟶ R) : + f ≫ g = ⟨f.f ≫ g.f, comp_proof g f⟩ := by refl + +@[simp] +lemma id_eq {P : karoubi C} : 𝟙 P = ⟨P.p, by repeat { rw P.idempotence, }⟩ := by refl + +/-- It is possible to coerce an object of `C` into an object of `karoubi C`. +See also the functor `to_karoubi`. -/ +instance coe : has_coe_t C (karoubi C) := ⟨λ X, ⟨X, 𝟙 X, by rw comp_id⟩⟩ + +@[simp] +lemma coe_X (X : C) : (X : karoubi C).X = X := by refl + +@[simp] +lemma coe_p (X : C) : (X : karoubi C).p = 𝟙 X := by refl + +@[simp] +lemma eq_to_hom_f {P Q : karoubi C} (h : P = Q) : + karoubi.hom.f (eq_to_hom h) = P.p ≫ eq_to_hom (congr_arg karoubi.X h) := +by { subst h, simp only [eq_to_hom_refl, karoubi.id_eq, comp_id], } + +end karoubi + +/-- The obvious fully faithful functor `to_karoubi` sends an object `X : C` to the obvious +formal direct factor of `X` given by `𝟙 X`. -/ +@[simps] +def to_karoubi : C ⥤ karoubi C := +{ obj := λ X, ⟨X, 𝟙 X, by rw comp_id⟩, + map := λ X Y f, ⟨f, by simp only [comp_id, id_comp]⟩ } + +instance : full (to_karoubi C) := +{ preimage := λ X Y f, f.f, + witness' := λ X Y f, by { ext, simp only [to_karoubi_map_f], }, } + +instance : faithful (to_karoubi C) := { } + +variables {C} + +@[simps] +instance [preadditive C] {P Q : karoubi C} : add_comm_group (P ⟶ Q) := +{ add := λ f g, ⟨f.f+g.f, begin + rw [add_comp, comp_add], + congr', + exacts [f.comm, g.comm], + end⟩, + zero := ⟨0, by simp only [comp_zero, zero_comp]⟩, + zero_add := λ f, by { ext, simp only [zero_add], }, + add_zero := λ f, by { ext, simp only [add_zero], }, + add_assoc := λ f g h', by simp only [add_assoc], + add_comm := λ f g, by { ext, apply_rules [add_comm], }, + neg := λ f, ⟨-f.f, by simpa only [neg_comp, comp_neg, neg_inj] using f.comm⟩, + add_left_neg := λ f, by { ext, apply_rules [add_left_neg], }, } + +namespace karoubi + +lemma hom_eq_zero_iff [preadditive C] {P Q : karoubi C} {f : hom P Q} : f = 0 ↔ f.f = 0 := hom_ext + +/-- The map sending `f : P ⟶ Q` to `f.f : P.X ⟶ Q.X` is additive. -/ +@[simps] +def inclusion_hom [preadditive C] (P Q : karoubi C) : add_monoid_hom (P ⟶ Q) (P.X ⟶ Q.X) := +{ to_fun := λ f, f.f, + map_zero' := rfl, + map_add' := λ f g, rfl } + +@[simp] +lemma sum_hom [preadditive C] {P Q : karoubi C} {α : Type*} (s : finset α) (f : α → (P ⟶ Q)) : + (∑ x in s, f x).f = ∑ x in s, (f x).f := +add_monoid_hom.map_sum (inclusion_hom P Q) f s + +end karoubi + +/-- The category `karoubi C` is preadditive if `C` is. -/ +instance [preadditive C] : preadditive (karoubi C) := +{ hom_group := λ P Q, by apply_instance, + add_comp' := λ P Q R f g h, + by { ext, simp only [add_comp, quiver.hom.add_comm_group_add_f, karoubi.comp], }, + comp_add' := λ P Q R f g h, + by { ext, simp only [comp_add, quiver.hom.add_comm_group_add_f, karoubi.comp], }, } + +instance [preadditive C] : functor.additive (to_karoubi C) := { } + +open karoubi + +variables (C) + +instance : is_idempotent_complete (karoubi C) := +begin + refine ⟨_⟩, + intros P p hp, + have hp' := hom_ext.mp hp, + simp only [comp] at hp', + use ⟨P.X, p.f, hp'⟩, + use ⟨p.f, by rw [comp_p p, hp']⟩, + use ⟨p.f, by rw [hp', p_comp p]⟩, + split; simpa only [hom_ext] using hp', +end + +instance [is_idempotent_complete C] : ess_surj (to_karoubi C) := ⟨λ P, begin + have h : is_idempotent_complete C := infer_instance, + rcases is_idempotent_complete.idempotents_split P.X P.p P.idempotence + with ⟨Y,i,e,⟨h₁,h₂⟩⟩, + use Y, + exact nonempty.intro + { hom := ⟨i, by erw [id_comp, ← h₂, ← assoc, h₁, id_comp]⟩, + inv := ⟨e, by erw [comp_id, ← h₂, assoc, h₁, comp_id]⟩, + hom_inv_id' := by { ext, simpa only [comp, h₁], }, + inv_hom_id' := by { ext, simp only [comp, ← h₂, id_eq], }, }, +end⟩ + +/-- If `C` is idempotent complete, the functor `to_karoubi : C ⥤ karoubi C` is an equivalence. -/ +def to_karoubi_is_equivalence [is_idempotent_complete C] : + is_equivalence (to_karoubi C) := +equivalence.of_fully_faithfully_ess_surj (to_karoubi C) + +namespace karoubi + +variables {C} + +/-- The split mono which appears in the factorisation `decomp_id P`. -/ +@[simps] +def decomp_id_i (P : karoubi C) : P ⟶ P.X := ⟨P.p, by erw [coe_p, comp_id, P.idempotence]⟩ + +/-- The split epi which appears in the factorisation `decomp_id P`. -/ +@[simps] +def decomp_id_p (P : karoubi C) : (P.X : karoubi C) ⟶ P := +⟨P.p, by erw [coe_p, id_comp, P.idempotence]⟩ + +/-- The formal direct factor of `P.X` given by the idempotent `P.p` in the category `C` +is actually a direct factor in the category `karoubi C`. -/ +lemma decomp_id (P : karoubi C) : + 𝟙 P = (decomp_id_i P) ≫ (decomp_id_p P) := +by { ext, simp only [comp, id_eq, P.idempotence, decomp_id_i, decomp_id_p], } + +lemma decomp_p (P : karoubi C) : + (to_karoubi C).map P.p = (decomp_id_p P) ≫ (decomp_id_i P) := +by { ext, simp only [comp, decomp_id_p_f, decomp_id_i_f, P.idempotence, to_karoubi_map_f], } + +lemma decomp_id_i_to_karoubi (X : C) : decomp_id_i ((to_karoubi C).obj X) = 𝟙 _ := +by { ext, refl, } + +lemma decomp_id_p_to_karoubi (X : C) : decomp_id_p ((to_karoubi C).obj X) = 𝟙 _ := +by { ext, refl, } + +lemma decomp_id_i_naturality {P Q : karoubi C} (f : P ⟶ Q) : f ≫ decomp_id_i _ = + decomp_id_i _ ≫ ⟨f.f, by erw [comp_id, id_comp]⟩ := +by { ext, simp only [comp, decomp_id_i_f, karoubi.comp_p, karoubi.p_comp], } + +lemma decomp_id_p_naturality {P Q : karoubi C} (f : P ⟶ Q) : decomp_id_p P ≫ f = + (⟨f.f, by erw [comp_id, id_comp]⟩ : (P.X : karoubi C) ⟶ Q.X) ≫ decomp_id_p Q := +by { ext, simp only [comp, decomp_id_p_f, karoubi.comp_p, karoubi.p_comp], } + +end karoubi + +end idempotents + +end category_theory diff --git a/src/category_theory/preadditive/default.lean b/src/category_theory/preadditive/default.lean index cf257c117d85b..9cafd92606ff4 100644 --- a/src/category_theory/preadditive/default.lean +++ b/src/category_theory/preadditive/default.lean @@ -224,6 +224,18 @@ has_limit.mk { cone := fork.of_ι (kernel.ι (f - g)) (sub_eq_zero.1 $ (λ s, by simp) (λ s m h, by { ext, simpa using h walking_parallel_pair.zero }) } +/-- Conversely, an equalizer of `f` and `g` is a kernel of `f - g`. -/ +lemma has_kernel_of_has_equalizer + [has_equalizer f g] : has_kernel (f - g) := +has_limit.mk + { cone := fork.of_ι (equalizer.ι f g) + (by erw [comp_zero, comp_sub, equalizer.condition f g, sub_self]), + is_limit := fork.is_limit.mk _ + (λ s, equalizer.lift s.ι (by simpa only [comp_sub, comp_zero, sub_eq_zero] + using s.condition)) + (λ s, by simp only [fork.ι_eq_app_zero, fork.of_ι_π_app, equalizer.lift_ι]) + (λ s m h, by { ext, simpa only [equalizer.lift_ι] using h walking_parallel_pair.zero, }), } + end section