Skip to content

[Merged by Bors] - refactor(CategoryTheory): generalize universes for representable functors#17389

Closed
joelriou wants to merge 5 commits intomasterfrom
refactor-representable-functors-universes
Closed

[Merged by Bors] - refactor(CategoryTheory): generalize universes for representable functors#17389
joelriou wants to merge 5 commits intomasterfrom
refactor-representable-functors-universes

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Oct 3, 2024 •
edited
Loading

Functor.Representable is renamed Functor.IsRepresentable, and the API now allows any universe for the target category of types: in the definition, we use natural bijections instead of natural isomorphisms between functors to types. A new structure Functor.RepresentableBy is introduced: it contains the data expressing that a functor F : Cᵒᵖ ⥤ Type _ is representable by an object Y : C.

Open in Gitpod

@joelriou joelriou added WIP Work in progress t-category-theory Category theory labels Oct 3, 2024
@joelriou joelriou changed the title refactor(CategoryTheory): generalize universes for representable func… refactor(CategoryTheory): generalize universes for representable functors Oct 3, 2024
@joelriou joelriou mentioned this pull request Oct 3, 2024
Closed
1 task
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 3, 2024 •
edited
Loading

PR summary 6e6fb6cdf5

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ AddCommGrp.forget_isCorepresentable
+ AddGrp.forget_isCorepresentable
+ CommGrp.forget_isCorepresentable
+ CorepresentableBy
+ CorepresentableBy.ext
+ CorepresentableBy.homEquiv_eq
+ CorepresentableBy.isCorepresentable
+ CorepresentableBy.ofIso
+ CorepresentableBy.toIso
+ Grp.forget_isCorepresentable
+ IsCorepresentable
+ IsCorepresentable.mk'
+ IsRepresentable
+ IsRepresentable.mk'
+ RepresentableBy
+ RepresentableBy.ext
+ RepresentableBy.homEquiv_eq
+ RepresentableBy.isRepresentable
+ RepresentableBy.ofIso
+ RepresentableBy.toIso
+ coreprW_hom_app
+ corepresentableBy
+ corepresentableByEquiv
+ instance : Functor.IsCorepresentable (𝟭 (Type v₁))
+ instance {X : C} : IsRepresentable (yoneda.obj X)
+ instance {X : Cᵒᵖ} : IsCorepresentable (coyoneda.obj X)
+ isRepresentable_of_natIso
+ reprW_hom_app
+ representableBy
+ representableByEquiv
++ isSheaf_of_isRepresentable
- AddCommGrp.forget_corepresentable
- AddGrp.forget_corepresentable
- CommGrp.forget_corepresentable
- Grp.forget_corepresentable
- coreprW_app_hom
- instance : Functor.Corepresentable (𝟭 (Type v₁))
- instance {X : C} : Representable (yoneda.obj X) where has_representation := ⟨X, ⟨Iso.refl _⟩⟩
- instance {X : Cᵒᵖ} : Corepresentable (coyoneda.obj X)
- reprW_app_hom
- representable_of_natIso
-- isSheaf_of_representable

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.

@joelriou joelriou mentioned this pull request Oct 4, 2024
Closed
5 tasks
@joelriou joelriou removed the WIP Work in progress label Oct 4, 2024
jcommelin
jcommelin reviewed Oct 4, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 4, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 4, 2024
@joelriou
refactor(CategoryTheory): generalize universes for representable func…
2a16a7b 
…tors (#17389)

`Functor.Representable` is renamed `Functor.IsRepresentable`, and the API now allows any universe for the target category of types: in the definition, we use natural bijections instead of natural isomorphisms between functors to types. A new structure `Functor.RepresentableBy` is introduced: it contains the data expressing that a functor `F : Cᵒᵖ ⥤ Type _` is representable by an object `Y : C`.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 4, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor(CategoryTheory): generalize universes for representable functors [Merged by Bors] - refactor(CategoryTheory): generalize universes for representable functors Oct 4, 2024
@mathlib-bors mathlib-bors bot closed this Oct 4, 2024
@mathlib-bors mathlib-bors bot deleted the refactor-representable-functors-universes branch October 4, 2024 11:13
@joelriou joelriou mentioned this pull request Oct 7, 2024
Closed
4 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

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.

2 participants

@joelriou @jcommelin