Skip to content

feat(CategoryTheory): naturality lemmas for Core construction #29284

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 11 commits into
base: master
Choose a base branch
from
+62 −0
Open

feat(CategoryTheory): naturality lemmas for Core construction #29284

Changes from 7 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
68ac6e1
chore: rename hom_to_functor, id_to_functor
Jlh18 Sep 2, 2025
5ad3680
fix: post-build error
Jlh18 Sep 2, 2025
f7a5a1f
feat: instance HasColimits Grpd
Jlh18 Sep 3, 2025
4ce15a6
delete Colimits file
Jlh18 Sep 3, 2025
e78c94a
delete Grpd.Core file
Jlh18 Sep 3, 2025
70db0ca
merge master
Jlh18 Sep 18, 2025
2d79eab
Merge branch 'master' into Core2
Jlh18 Sep 18, 2025
b273d77
Merge branch 'master' into Core2
Jlh18 Oct 1, 2025
4b8d3e0
refactor: replace equality of functors with isos
Jlh18 Oct 1, 2025
600fd42
chore: no rfl
Jlh18 Oct 2, 2025
bdf9d8f
fix: switch eqToIso to Iso.refl
Jlh18 Oct 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 31 additions & 0 deletions Mathlib/CategoryTheory/Core.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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) :
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For this assertion (and the next two), could you only state this as an isomorphism? (It may be unclear that we actually need equalities of functors here, and in general I would argue that it is better to get the isomorphism first, and then deduce the equality if it is absolutely needed using Functor.ext_of_iso.)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am happy to make it an iso, but I definitely also want the equality. This is because I want a 1-adjunction between Grpd and Cat, where this is the right adjoint to the forgetful functor. This allows me to show that Grpd inherits 1-colimits from Cat, as a coreflective subcategory. (see #29282)

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
Expand Down