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

Jump to bottom

Open

Jlh18 wants to merge 11 commits into leanprover-community:master from Jlh18:Core2

+62 −0

Collaborator

Jlh18 commented Sep 3, 2025 •

edited by alreadydone

Loading

Lemmas for PR #29283 to prove that Core is the right adjoint to the forgetful functor from Cat to Grpd.

These lemmas are more general than that setting, and need not be stated in the bundled format.

depends on: [Merged by Bors] - chore: rename hom_to_functor, id_to_functor #29250

Jlh18 added 5 commits

September 2, 2025 09:56


          chore: rename hom_to_functor, id_to_functor

68ac6e1


          fix: post-build error

5ad3680


          feat: instance HasColimits Grpd

f7a5a1f


          delete Colimits file

4ce15a6


          delete Grpd.Core file

e78c94a

github-actions bot added the new-contributor label

github-actions bot commented Sep 3, 2025 •

edited

Loading

PR summary 12fc3dacb3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ coreCompInclusionIso
+ core_comp_inclusion
+ functorToCoreCompLeftIso
+ functorToCoreCompRightIso
+ functorToCoreInclusionIso
+ functorToCore_comp_left
+ functorToCore_comp_right
+ functorToCore_inclusion
+ inclusionCompFunctorToCoreIso
+ inclusion_comp_functorToCore

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Jlh18 mentioned this pull request

feat(CategoryTheory): define forgetful-core adjunction between Cat and Grpd #29283

Open

1 task

mathlib4-dependent-issues-bot added the blocked-by-other-PR label

Jlh18 changed the title ~~feat: naturality lemmas for Core construction~~ feat(CategoryTheory): naturality lemmas for Core construction

mathlib4-dependent-issues-bot removed the blocked-by-other-PR label

Collaborator

mathlib4-dependent-issues-bot commented Sep 17, 2025

This PR/issue depends on:

~~[Merged by Bors] - chore: rename hom_to_functor, id_to_functor #29250~~
By Dependent Issues (🤖). Happy coding!

mathlib4-merge-conflict-bot added the merge-conflict label

Collaborator

mathlib4-merge-conflict-bot commented Sep 17, 2025

This pull request has conflicts, please merge master and resolve them.


          merge master

70db0ca

github-actions bot removed the merge-conflict label


          Merge branch 'master' into Core2

2d79eab

github-actions bot added easy and removed easy labels

leanprover-community-bot-assistant assigned kex-y

kex-y removed their assignment

leanprover-community-bot-assistant assigned hrmacbeth

hrmacbeth removed their assignment

chrisflav added the t-category-theory label

Collaborator Author

Jlh18 commented Sep 29, 2025

+t-category-theory

Collaborator Author

Jlh18 commented Sep 29, 2025

-t-category-theory

1 similar comment

Collaborator

adomani commented Sep 29, 2025

-t-category-theory

Jlh18 removed the new-contributor label

joelriou reviewed

View reviewed changes

Mathlib/CategoryTheory/Core.lean Show resolved Hide resolved

joelriou reviewed

View reviewed changes

Mathlib/CategoryTheory/Core.lean

    
              variable {G : Type u₂} [Groupoid.{v₂} G]

              lemma functorToCore_comp_left {G' : Type u₃} [Groupoid.{v₃} G'] (H : G ⥤ C) (F : G' ⥤ G) :

Collaborator

joelriou Sep 30, 2025

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.)

Collaborator Author

Jlh18 Sep 30, 2025

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)

joelriou added the awaiting-author label

Jlh18 added 2 commits

October 1, 2025 13:54


          Merge branch 'master' into Core2

b273d77


          refactor: replace equality of functors with isos

4b8d3e0

Jlh18 removed the awaiting-author label

joelriou reviewed

View reviewed changes

Mathlib/CategoryTheory/Core.lean Outdated Show resolved Hide resolved

joelriou added the awaiting-author label


          chore: no rfl

600fd42

Jlh18 removed the awaiting-author label

joelriou reviewed

View reviewed changes

Mathlib/CategoryTheory/Core.lean Outdated

    
              /-- 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 _)

Collaborator

joelriou Oct 3, 2025

Suggested change

      
              NatIso.ofComponents (fun _ ↦ eqToIso _)
          
              NatIso.ofComponents (fun _ ↦ Iso.refl _)

Collaborator Author

Jlh18 Oct 3, 2025

oh sorry I must have misread what you suggested. Fixed now.

joelriou reviewed

View reviewed changes

Mathlib/CategoryTheory/Core.lean Outdated

    
              /-- The functor `functorToCore (𝟭 G)` is a section of `inclusion G`. -/

              def inclusionCompFunctorToCoreIso : inclusion G ⋙ functorToCore (𝟭 G) ≅ 𝟭 (Core G) :=

                NatIso.ofComponents (fun _ ↦ eqToIso _)

Collaborator

joelriou Oct 3, 2025

Suggested change

      
              NatIso.ofComponents (fun _ ↦ eqToIso _)
          
              NatIso.ofComponents (fun _ ↦ Iso.refl _)

joelriou added the awaiting-author label


          fix: switch eqToIso to Iso.refl

bdf9d8f

Jlh18 removed the awaiting-author label

leanprover-community-bot-assistant assigned kim-em

joelriou reviewed

View reviewed changes

Mathlib/CategoryTheory/Core.lean

    
              ```

                                F.core

                          Core C ⥤ Core D

               includion C  ‖          ‖  inclusion D

Collaborator

joelriou Oct 18, 2025

Suggested change

      
             includion C  ‖          ‖  inclusion D
          
             inclusion C  ‖          ‖  inclusion D

joelriou reviewed

View reviewed changes

Mathlib/CategoryTheory/Core.lean

Comment on lines +126 to +128

    
              `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.

Collaborator

joelriou Oct 18, 2025

I do not think there is a need to give that many comments about this isomorphisms.

Suggested change

      
            `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.

joelriou added the awaiting-author label

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-author t-category-theory