From 68ac6e120376726fb9545e1d6f7bc358af8bb908 Mon Sep 17 00:00:00 2001 From: jlh18 Date: Tue, 2 Sep 2025 09:56:12 -0400 Subject: [PATCH 1/7] chore: rename hom_to_functor, id_to_functor --- .../AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean | 2 +- Mathlib/CategoryTheory/Category/Grpd.lean | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean b/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean index 92818ccf75cb97..933fd0e84a7378 100644 --- a/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean +++ b/Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean @@ -231,7 +231,7 @@ open scoped ContinuousMap def equivOfHomotopyEquiv (hequiv : X ≃ₕ Y) : πₓ X ≌ πₓ Y := by apply CategoryTheory.Equivalence.mk (πₘ (TopCat.ofHom hequiv.toFun) : πₓ X ⥤ πₓ Y) (πₘ (TopCat.ofHom hequiv.invFun) : πₓ Y ⥤ πₓ X) <;> - simp only [Grpd.id_to_functor] + simp only [← Grpd.id_eq_id] · convert (asIso (homotopicMapsNatIso hequiv.left_inv.some)).symm exacts [((π).map_id X).symm, ((π).map_comp _ _).symm] · convert asIso (homotopicMapsNatIso hequiv.right_inv.some) diff --git a/Mathlib/CategoryTheory/Category/Grpd.lean b/Mathlib/CategoryTheory/Category/Grpd.lean index 8e248223a6f294..132eb01489dd43 100644 --- a/Mathlib/CategoryTheory/Category/Grpd.lean +++ b/Mathlib/CategoryTheory/Category/Grpd.lean @@ -80,11 +80,11 @@ instance forgetToCat_faithful : forgetToCat.Faithful where /-- Convert arrows in the category of groupoids to functors, which sometimes helps in applying simp lemmas -/ -theorem hom_to_functor {C D E : Grpd.{v, u}} (f : C ⟶ D) (g : D ⟶ E) : f ≫ g = f ⋙ g := +theorem comp_eq_comp {C D E : Grpd.{v, u}} (f : C ⟶ D) (g : D ⟶ E) : f ≫ g = f ⋙ g := rfl /-- Converts identity in the category of groupoids to the functor identity -/ -theorem id_to_functor {C : Grpd.{v, u}} : 𝟭 C = 𝟙 C := +theorem id_eq_id {C : Grpd.{v, u}} : 𝟙 C = 𝟭 C := rfl section Products @@ -99,7 +99,7 @@ def piLimitFanIsLimit ⦃J : Type u⦄ (F : J → Grpd.{u, u}) : Limits.IsLimit (by intros dsimp only [piLimitFan] - simp [hom_to_functor]) + simp [comp_eq_comp]) (by intro s m w apply Functor.pi_ext From f7a5a1f5ef473f21511986c58d89b70106836ca1 Mon Sep 17 00:00:00 2001 From: jlh18 Date: Tue, 2 Sep 2025 22:16:23 -0400 Subject: [PATCH 2/7] feat: instance HasColimits Grpd --- Mathlib/CategoryTheory/Core.lean | 31 +++++++++ .../CategoryTheory/Groupoid/Grpd/Colimit.lean | 35 ++++++++++ .../CategoryTheory/Groupoid/Grpd/Core.lean | 68 +++++++++++++++++++ 3 files changed, 134 insertions(+) create mode 100644 Mathlib/CategoryTheory/Groupoid/Grpd/Colimit.lean create mode 100644 Mathlib/CategoryTheory/Groupoid/Grpd/Core.lean diff --git a/Mathlib/CategoryTheory/Core.lean b/Mathlib/CategoryTheory/Core.lean index e8f24370c47faf..707e29b47069fe 100644 --- a/Mathlib/CategoryTheory/Core.lean +++ b/Mathlib/CategoryTheory/Core.lean @@ -112,6 +112,10 @@ def coreId : (𝟭 C).core ≅ 𝟭 (Core C) := Iso.refl _ def coreComp {E : Type u₃} [Category.{v₃} E] (F : C ⥤ D) (G : D ⥤ E) : (F ⋙ G).core ≅ F.core ⋙ G.core := Iso.refl _ +lemma core_comp_inclusion (F : C ⥤ D) : + F.core ⋙ Core.inclusion D = Core.inclusion C ⋙ F := + rfl + end Functor namespace Iso @@ -160,6 +164,33 @@ lemma coreAssociator {E : Type u₃} [Category.{v₃} E] {E' : Type u₄} [Categ end Iso +namespace Core + +variable {G : Type u₂} [Groupoid.{v₂} G] + +lemma functorToCore_comp_left {G' : Type u₃} [Groupoid.{v₃} G'] (H : G ⥤ C) (F : G' ⥤ G) : + functorToCore (F ⋙ H) = F ⋙ functorToCore H := by + apply Functor.ext <;> aesop_cat + +lemma functorToCore_comp_right {C' : Type u₄} [Category.{v₄} C'] (H : G ⥤ C) (F : C ⥤ C') : + functorToCore (H ⋙ F) = functorToCore H ⋙ F.core := by + apply Functor.ext <;> aesop_cat + +theorem inclusion_comp_functorToCore : inclusion G ⋙ functorToCore (𝟭 G) = 𝟭 (Core G) := by + apply Functor.ext + · intro x y f + simp only [Core.inclusion, Core.functorToCore, Functor.id_map, + Functor.comp_map, Groupoid.inv_eq_inv, IsIso.Iso.inv_hom, + eqToHom_refl, Category.comp_id, Category.id_comp] + rfl + · intro + rfl + +theorem functorToCore_inclusion : functorToCore (inclusion C) = 𝟭 (Core C) := + rfl + +end Core + variable (D : Type u₂) [Category.{v₂} D] namespace Equivalence diff --git a/Mathlib/CategoryTheory/Groupoid/Grpd/Colimit.lean b/Mathlib/CategoryTheory/Groupoid/Grpd/Colimit.lean new file mode 100644 index 00000000000000..0b57fe75f5bbf5 --- /dev/null +++ b/Mathlib/CategoryTheory/Groupoid/Grpd/Colimit.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2019 Joseph Hua. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Hua +-/ +import Mathlib.CategoryTheory.Category.Cat.Colimit +import Mathlib.CategoryTheory.Groupoid.Grpd.Core + +/-! +# The category of small groupoids has all small colimits + +The category of small categories `Cat` has all small colimits. +The category of small groupoids `Grpd` is a coreflective subcategory of `Cat`, +and therefore inherits all colimits from `Cat`. +The right adjoint to the forgetful functor is the core functor `CategoryTheory.Core.functor`. +-/ + +noncomputable section + +universe v + +open CategoryTheory.Limits + +namespace CategoryTheory + +namespace Grpd + +/-- The category of small categories has all small colimits as a reflective subcategory of the +category of simplicial sets, which has all small colimits. -/ +instance : HasColimits Grpd.{v, v} := + hasColimits_of_coreflective forgetToCat + +end Grpd + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/Groupoid/Grpd/Core.lean b/Mathlib/CategoryTheory/Groupoid/Grpd/Core.lean new file mode 100644 index 00000000000000..60c48d7c998bff --- /dev/null +++ b/Mathlib/CategoryTheory/Groupoid/Grpd/Core.lean @@ -0,0 +1,68 @@ +/- +Copyright (c) 2019 Joseph Hua. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Hua +-/ +import Mathlib.CategoryTheory.Category.Grpd +import Mathlib.CategoryTheory.Core +import Mathlib.CategoryTheory.Monad.Limits + +/-! +# The forgetful-core adjunction + +Taking the core of a category defines a functor `Cat ⥤ Grpd`. This functor is left adjoint +to the forgetful functor from `Grpd ⥤ Cat`. + +# Main definitions + +* `CategoryTheory.Core.functor`: the functor `Cat ⥤ Grpd` that on objects takes + the core of a category +* `CategoryTheory.Core.adjunction`: the adjunction with the forgetful functor + `Grpd.forgetToCat` on the left, and the core functor `Core.functor` on the right. +* An instance that `Grpd.forgetToCat` is coreflective. + +-/ + +universe w v u v₁ u₁ v₂ u₂ v₃ u₃ + +noncomputable section + +namespace CategoryTheory +namespace Core + +variable {C : Type u} [Category.{v} C] {D : Type u₁} [Category.{v₁} D] + +/-- The functor from `Cat` to `Grpd` that takes the core of a category, on objects. -/ +def functor : Cat.{v,u} ⥤ Grpd.{v,u} where + obj C := Grpd.of (Core C) + map F := F.core + +/-- The adjunction between the forgetful functor from `Grpd` to `Cat` and the core +functor from `Cat` to `Grpd`. -/ +def adjunction : Grpd.forgetToCat ⊣ functor where + unit := { + app G := functorToCore (𝟭 _) + naturality _ _ F := by + simp [functor, Grpd.comp_eq_comp, ← functorToCore_comp_left, ← functorToCore_comp_right, + Functor.id_comp, Functor.comp_id, Grpd.forgetToCat]} + counit := {app C := inclusion C} + +end Core + +namespace Grpd + +open Functor Core + +instance : IsLeftAdjoint Grpd.forgetToCat := + IsLeftAdjoint.mk ⟨ functor , ⟨ adjunction ⟩ ⟩ + +instance : IsRightAdjoint functor := + IsRightAdjoint.mk ⟨ Grpd.forgetToCat , ⟨ adjunction ⟩ ⟩ + +instance : Coreflective Grpd.forgetToCat where + R := functor + adj := adjunction + +end Grpd + +end CategoryTheory From 4ce15a6df3e7e6eadb4c75acb18330f41edd5751 Mon Sep 17 00:00:00 2001 From: jlh18 Date: Tue, 2 Sep 2025 22:20:57 -0400 Subject: [PATCH 3/7] delete Colimits file --- .../CategoryTheory/Groupoid/Grpd/Colimit.lean | 35 ------------------- 1 file changed, 35 deletions(-) delete mode 100644 Mathlib/CategoryTheory/Groupoid/Grpd/Colimit.lean diff --git a/Mathlib/CategoryTheory/Groupoid/Grpd/Colimit.lean b/Mathlib/CategoryTheory/Groupoid/Grpd/Colimit.lean deleted file mode 100644 index 0b57fe75f5bbf5..00000000000000 --- a/Mathlib/CategoryTheory/Groupoid/Grpd/Colimit.lean +++ /dev/null @@ -1,35 +0,0 @@ -/- -Copyright (c) 2019 Joseph Hua. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Hua --/ -import Mathlib.CategoryTheory.Category.Cat.Colimit -import Mathlib.CategoryTheory.Groupoid.Grpd.Core - -/-! -# The category of small groupoids has all small colimits - -The category of small categories `Cat` has all small colimits. -The category of small groupoids `Grpd` is a coreflective subcategory of `Cat`, -and therefore inherits all colimits from `Cat`. -The right adjoint to the forgetful functor is the core functor `CategoryTheory.Core.functor`. --/ - -noncomputable section - -universe v - -open CategoryTheory.Limits - -namespace CategoryTheory - -namespace Grpd - -/-- The category of small categories has all small colimits as a reflective subcategory of the -category of simplicial sets, which has all small colimits. -/ -instance : HasColimits Grpd.{v, v} := - hasColimits_of_coreflective forgetToCat - -end Grpd - -end CategoryTheory From e78c94ac69112c7d675ffa3d8907bb2785af68c8 Mon Sep 17 00:00:00 2001 From: jlh18 Date: Tue, 2 Sep 2025 22:25:20 -0400 Subject: [PATCH 4/7] delete Grpd.Core file --- .../CategoryTheory/Groupoid/Grpd/Core.lean | 68 ------------------- 1 file changed, 68 deletions(-) delete mode 100644 Mathlib/CategoryTheory/Groupoid/Grpd/Core.lean diff --git a/Mathlib/CategoryTheory/Groupoid/Grpd/Core.lean b/Mathlib/CategoryTheory/Groupoid/Grpd/Core.lean deleted file mode 100644 index 60c48d7c998bff..00000000000000 --- a/Mathlib/CategoryTheory/Groupoid/Grpd/Core.lean +++ /dev/null @@ -1,68 +0,0 @@ -/- -Copyright (c) 2019 Joseph Hua. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Hua --/ -import Mathlib.CategoryTheory.Category.Grpd -import Mathlib.CategoryTheory.Core -import Mathlib.CategoryTheory.Monad.Limits - -/-! -# The forgetful-core adjunction - -Taking the core of a category defines a functor `Cat ⥤ Grpd`. This functor is left adjoint -to the forgetful functor from `Grpd ⥤ Cat`. - -# Main definitions - -* `CategoryTheory.Core.functor`: the functor `Cat ⥤ Grpd` that on objects takes - the core of a category -* `CategoryTheory.Core.adjunction`: the adjunction with the forgetful functor - `Grpd.forgetToCat` on the left, and the core functor `Core.functor` on the right. -* An instance that `Grpd.forgetToCat` is coreflective. - --/ - -universe w v u v₁ u₁ v₂ u₂ v₃ u₃ - -noncomputable section - -namespace CategoryTheory -namespace Core - -variable {C : Type u} [Category.{v} C] {D : Type u₁} [Category.{v₁} D] - -/-- The functor from `Cat` to `Grpd` that takes the core of a category, on objects. -/ -def functor : Cat.{v,u} ⥤ Grpd.{v,u} where - obj C := Grpd.of (Core C) - map F := F.core - -/-- The adjunction between the forgetful functor from `Grpd` to `Cat` and the core -functor from `Cat` to `Grpd`. -/ -def adjunction : Grpd.forgetToCat ⊣ functor where - unit := { - app G := functorToCore (𝟭 _) - naturality _ _ F := by - simp [functor, Grpd.comp_eq_comp, ← functorToCore_comp_left, ← functorToCore_comp_right, - Functor.id_comp, Functor.comp_id, Grpd.forgetToCat]} - counit := {app C := inclusion C} - -end Core - -namespace Grpd - -open Functor Core - -instance : IsLeftAdjoint Grpd.forgetToCat := - IsLeftAdjoint.mk ⟨ functor , ⟨ adjunction ⟩ ⟩ - -instance : IsRightAdjoint functor := - IsRightAdjoint.mk ⟨ Grpd.forgetToCat , ⟨ adjunction ⟩ ⟩ - -instance : Coreflective Grpd.forgetToCat where - R := functor - adj := adjunction - -end Grpd - -end CategoryTheory From 4b8d3e04c92dce662081d4be76ae63c9c796cec6 Mon Sep 17 00:00:00 2001 From: jlh18 Date: Wed, 1 Oct 2025 14:43:42 -0400 Subject: [PATCH 5/7] refactor: replace equality of functors with isos --- Mathlib/CategoryTheory/Core.lean | 63 ++++++++++++++++++++++++-------- 1 file changed, 47 insertions(+), 16 deletions(-) diff --git a/Mathlib/CategoryTheory/Core.lean b/Mathlib/CategoryTheory/Core.lean index 707e29b47069fe..53500d524810ab 100644 --- a/Mathlib/CategoryTheory/Core.lean +++ b/Mathlib/CategoryTheory/Core.lean @@ -112,9 +112,29 @@ def coreId : (𝟭 C).core ≅ 𝟭 (Core C) := Iso.refl _ def coreComp {E : Type u₃} [Category.{v₃} E] (F : C ⥤ D) (G : D ⥤ E) : (F ⋙ G).core ≅ F.core ⋙ G.core := Iso.refl _ +/-- The natural isomorphism +``` + F.core + Core C ⥤ Core D + includion C ‖ ‖ inclusion D + V V + C ⥤ D + F +``` +thought of as pseudonaturality of `inclusion`, +when viewing `Core` as a pseudofunctor. +`Core` is in fact a strict 2-functor, +and this isomorphism is an equality of functors under the hood, +and thus can be promoted to a naturality condition between 1-functors. +-/ +@[simps!] +def coreCompInclusionIso (F : C ⥤ D) : + F.core ⋙ Core.inclusion D ≅ Core.inclusion C ⋙ F := + Iso.refl _ + lemma core_comp_inclusion (F : C ⥤ D) : F.core ⋙ Core.inclusion D = Core.inclusion C ⋙ F := - rfl + Functor.ext_of_iso (coreCompInclusionIso F) (by cat_disch) end Functor @@ -168,26 +188,37 @@ namespace Core variable {G : Type u₂} [Groupoid.{v₂} G] +/-- The functor `functorToCore (F ⋙ H)` factors through `functortoCore H`. -/ +def functorToCoreCompLeftIso {G' : Type u₃} [Groupoid.{v₃} G'] (H : G ⥤ C) (F : G' ⥤ G) : + functorToCore (F ⋙ H) ≅ F ⋙ functorToCore H := + NatIso.ofComponents (fun X ↦ eqToIso rfl) + lemma functorToCore_comp_left {G' : Type u₃} [Groupoid.{v₃} G'] (H : G ⥤ C) (F : G' ⥤ G) : - functorToCore (F ⋙ H) = F ⋙ functorToCore H := by - apply Functor.ext <;> aesop_cat + functorToCore (F ⋙ H) = F ⋙ functorToCore H := + Functor.ext_of_iso (functorToCoreCompLeftIso H F) (by cat_disch) + +/-- The functor `functorToCore (H ⋙ F)` factors through `functorToCore H`. -/ +def functorToCoreCompRightIso {C' : Type u₄} [Category.{v₄} C'] (H : G ⥤ C) (F : C ⥤ C') : + functorToCore (H ⋙ F) ≅ functorToCore H ⋙ F.core := + Iso.refl _ lemma functorToCore_comp_right {C' : Type u₄} [Category.{v₄} C'] (H : G ⥤ C) (F : C ⥤ C') : - functorToCore (H ⋙ F) = functorToCore H ⋙ F.core := by - apply Functor.ext <;> aesop_cat - -theorem inclusion_comp_functorToCore : inclusion G ⋙ functorToCore (𝟭 G) = 𝟭 (Core G) := by - apply Functor.ext - · intro x y f - simp only [Core.inclusion, Core.functorToCore, Functor.id_map, - Functor.comp_map, Groupoid.inv_eq_inv, IsIso.Iso.inv_hom, - eqToHom_refl, Category.comp_id, Category.id_comp] - rfl - · intro - rfl + functorToCore (H ⋙ F) = functorToCore H ⋙ F.core := + Functor.ext_of_iso (functorToCoreCompRightIso H F) (by cat_disch) + +/-- The functor `functorToCore (𝟭 G)` is a section of `inclusion G`. -/ +def inclusionCompFunctorToCoreIso : inclusion G ⋙ functorToCore (𝟭 G) ≅ 𝟭 (Core G) := + NatIso.ofComponents (fun X ↦ eqToIso rfl) + +theorem inclusion_comp_functorToCore : inclusion G ⋙ functorToCore (𝟭 G) = 𝟭 (Core G) := + Functor.ext_of_iso inclusionCompFunctorToCoreIso (by cat_disch) + +/-- The functor `functorToCore (inclusion C)` is isomorphic to the identity on `Core C`. -/ +def functorToCoreInclusionIso : functorToCore (inclusion C) ≅ 𝟭 (Core C) := + Iso.refl _ theorem functorToCore_inclusion : functorToCore (inclusion C) = 𝟭 (Core C) := - rfl + Functor.ext_of_iso functorToCoreInclusionIso (by cat_disch) end Core From 600fd424d41cfa52793be3b1d75796d432ea4285 Mon Sep 17 00:00:00 2001 From: jlh18 Date: Thu, 2 Oct 2025 17:56:13 -0400 Subject: [PATCH 6/7] chore: no rfl --- Mathlib/CategoryTheory/Core.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Core.lean b/Mathlib/CategoryTheory/Core.lean index 53500d524810ab..a257e842c7fea1 100644 --- a/Mathlib/CategoryTheory/Core.lean +++ b/Mathlib/CategoryTheory/Core.lean @@ -191,7 +191,7 @@ variable {G : Type u₂} [Groupoid.{v₂} G] /-- The functor `functorToCore (F ⋙ H)` factors through `functortoCore H`. -/ def functorToCoreCompLeftIso {G' : Type u₃} [Groupoid.{v₃} G'] (H : G ⥤ C) (F : G' ⥤ G) : functorToCore (F ⋙ H) ≅ F ⋙ functorToCore H := - NatIso.ofComponents (fun X ↦ eqToIso rfl) + NatIso.ofComponents (fun _ ↦ eqToIso _) lemma functorToCore_comp_left {G' : Type u₃} [Groupoid.{v₃} G'] (H : G ⥤ C) (F : G' ⥤ G) : functorToCore (F ⋙ H) = F ⋙ functorToCore H := @@ -208,7 +208,7 @@ lemma functorToCore_comp_right {C' : Type u₄} [Category.{v₄} C'] (H : G ⥤ /-- The functor `functorToCore (𝟭 G)` is a section of `inclusion G`. -/ def inclusionCompFunctorToCoreIso : inclusion G ⋙ functorToCore (𝟭 G) ≅ 𝟭 (Core G) := - NatIso.ofComponents (fun X ↦ eqToIso rfl) + NatIso.ofComponents (fun _ ↦ eqToIso _) theorem inclusion_comp_functorToCore : inclusion G ⋙ functorToCore (𝟭 G) = 𝟭 (Core G) := Functor.ext_of_iso inclusionCompFunctorToCoreIso (by cat_disch) From bdf9d8fcb61a39eef72d606036d76e4771ea5d29 Mon Sep 17 00:00:00 2001 From: jlh18 Date: Fri, 3 Oct 2025 17:20:52 -0400 Subject: [PATCH 7/7] fix: switch eqToIso to Iso.refl --- Mathlib/CategoryTheory/Core.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Core.lean b/Mathlib/CategoryTheory/Core.lean index a257e842c7fea1..aecbf5341d661b 100644 --- a/Mathlib/CategoryTheory/Core.lean +++ b/Mathlib/CategoryTheory/Core.lean @@ -191,7 +191,7 @@ variable {G : Type u₂} [Groupoid.{v₂} G] /-- The functor `functorToCore (F ⋙ H)` factors through `functortoCore H`. -/ def functorToCoreCompLeftIso {G' : Type u₃} [Groupoid.{v₃} G'] (H : G ⥤ C) (F : G' ⥤ G) : functorToCore (F ⋙ H) ≅ F ⋙ functorToCore H := - NatIso.ofComponents (fun _ ↦ eqToIso _) + NatIso.ofComponents (fun _ ↦ Iso.refl _) lemma functorToCore_comp_left {G' : Type u₃} [Groupoid.{v₃} G'] (H : G ⥤ C) (F : G' ⥤ G) : functorToCore (F ⋙ H) = F ⋙ functorToCore H := @@ -208,7 +208,7 @@ lemma functorToCore_comp_right {C' : Type u₄} [Category.{v₄} C'] (H : G ⥤ /-- The functor `functorToCore (𝟭 G)` is a section of `inclusion G`. -/ def inclusionCompFunctorToCoreIso : inclusion G ⋙ functorToCore (𝟭 G) ≅ 𝟭 (Core G) := - NatIso.ofComponents (fun _ ↦ eqToIso _) + NatIso.ofComponents (fun _ ↦ Iso.refl _) theorem inclusion_comp_functorToCore : inclusion G ⋙ functorToCore (𝟭 G) = 𝟭 (Core G) := Functor.ext_of_iso inclusionCompFunctorToCoreIso (by cat_disch)