Skip to content

[Merged by Bors] - feat(FiberedCategory/BasedCategory): add bicategory of based categories#13545

Closed
callesonne wants to merge 36 commits intomasterfrom
fiberedcategory_basedcategory
Closed

[Merged by Bors] - feat(FiberedCategory/BasedCategory): add bicategory of based categories#13545
callesonne wants to merge 36 commits intomasterfrom
fiberedcategory_basedcategory

Conversation

@callesonne
Copy link
Copy Markdown
Collaborator

@callesonne callesonne commented Jun 5, 2024

We define the strict bicategory of based categories. Its objects are categories equipped with a functor to some fixed base-category. The strict bicategory of fibered categories will later be built on top of this one.

Co-authored-by: Paul Lezeau paul.lezeau@gmail.com

This is a remake of a previous PR of the same name, but some awful git accident happened and I think its just easier to remake the PR. (I by mistake added 400 commits to the PR by rebasing instead of merging with master in some weird way).

Open in Gitpod

@callesonne
Copy link
Copy Markdown
Collaborator Author

callesonne commented Jun 5, 2024

@joelriou I already incorporated all, except one, of your comments on the previous PR, thanks a lot for them! The suggestion about making BasedFunctor have functor as a field instead of extending Functor I have not changed yet. That is because this change would not let me use the notation F.obj for a F : BasedFunctor, and instead I would have to use F.functor.obj. Is there a way around this?

@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Jun 5, 2024

@joelriou I already incorporated all, except one, of your comments on the previous PR, thanks a lot for them! The suggestion about making BasedFunctor have functor as a field instead of extending Functor I have not changed yet. That is because this change would not let me use the notation F.obj for a F : BasedFunctor, and instead I would have to use F.functor.obj. Is there a way around this?

Ok, let us keep extends.

joelriou
joelriou reviewed Jun 17, 2024
View reviewed changes
@joelriou joelriou added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 17, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 17, 2024 •
edited
Loading

PR summary 4398168f81

Import changes

No significant changes to the import graph

Declarations diff

+ BasedCategory
+ BasedCategory.ofFunctor
+ BasedFunctor
+ BasedNatTrans
+ app_isHomLift
+ bicategory
+ comp_assoc
+ comp_id
+ ext
+ forgetful
+ homCategory
+ homCategory.ext
+ id_comp
+ instance (F : 𝒳 ⥤ᵇ 𝒴) (a : 𝒳.obj) : IsHomLift 𝒴.p (𝟙 (𝒳.p.obj a)) (𝟙 (F.obj a))
+ instance (𝒳 : BasedCategory.{v₂, u₂} 𝒮) : Category 𝒳.obj := 𝒳.category
+ instance : (forgetful 𝒳 𝒴).ReflectsIsomorphisms
+ instance : Bicategory.Strict (BasedCategory.{v₂, u₂} 𝒮)
+ instance : Category (BasedCategory.{v₂, u₂} 𝒮)
+ instance {F G : 𝒳 ⥤ᵇ 𝒴} (α : F ⟶ G) [IsIso α] : IsIso (X:=F.toFunctor) α.toNatTrans := by
+ isHomLift
+ isHomLift_iff
+ isHomLift_map
+ isIso_of_toNatTrans_isIso
+ mkNatIso
+ preserves_isHomLift
+ w_obj
+ whiskerLeft
+ whiskerRight
++ comp
+++ id

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

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

@callesonne callesonne added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 17, 2024
@joelriou joelriou added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 21, 2024
@callesonne callesonne added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 21, 2024
@joelriou joelriou added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 21, 2024
@callesonne callesonne added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 21, 2024
joelriou
joelriou reviewed Jun 22, 2024
View reviewed changes
joelriou
joelriou reviewed Jun 22, 2024
View reviewed changes
joelriou
joelriou reviewed Jun 22, 2024
View reviewed changes
callesonne and others added 3 commits June 23, 2024 09:21
@callesonne @joelriou
Update Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean
3b503c1 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@callesonne @joelriou
Update Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean
12d3280 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@callesonne @joelriou
Update Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean
4398168 
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Jun 23, 2024

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 23, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 23, 2024
@callesonne
feat(FiberedCategory/BasedCategory): add bicategory of based categori…
41c8f83 
…es (#13545)

We define the strict bicategory of based categories. Its objects are categories equipped with a functor to some fixed base-category. The strict bicategory of fibered categories will later be built on top of this one.

Co-authored-by: Paul Lezeau [paul.lezeau@gmail.com](mailto:paul.lezeau@gmail.com)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 23, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(FiberedCategory/BasedCategory): add bicategory of based categories [Merged by Bors] - feat(FiberedCategory/BasedCategory): add bicategory of based categories Jun 23, 2024
@mathlib-bors mathlib-bors bot closed this Jun 23, 2024
@mathlib-bors mathlib-bors bot deleted the fiberedcategory_basedcategory branch June 23, 2024 15:48
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@callesonne @kbuzzard
feat(FiberedCategory/BasedCategory): add bicategory of based categori…
e7c0ef0 
…es (#13545)

We define the strict bicategory of based categories. Its objects are categories equipped with a functor to some fixed base-category. The strict bicategory of fibered categories will later be built on top of this one.

Co-authored-by: Paul Lezeau [paul.lezeau@gmail.com](mailto:paul.lezeau@gmail.com)
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@callesonne @dagurtomas
feat(FiberedCategory/BasedCategory): add bicategory of based categori…
3089e27 
…es (#13545)

We define the strict bicategory of based categories. Its objects are categories equipped with a functor to some fixed base-category. The strict bicategory of fibered categories will later be built on top of this one.

Co-authored-by: Paul Lezeau [paul.lezeau@gmail.com](mailto:paul.lezeau@gmail.com)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@joelriou joelriou joelriou left review comments

Assignees

@Paul-Lez Paul-Lez

Labels

ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@callesonne @joelriou @Paul-Lez