Skip to content

[Merged by Bors] - feat(CategoryTheory/Localization): liftings of bifunctors#19894

Closed
joelriou wants to merge 1 commit intomasterfrom
localization-bifunctor
Closed

[Merged by Bors] - feat(CategoryTheory/Localization): liftings of bifunctors#19894
joelriou wants to merge 1 commit intomasterfrom
localization-bifunctor

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Dec 11, 2024 •
edited
Loading

When a functor F : C ⥤ E inverts a class of morphisms W : MorphismProperty C and L : C ⥤ D is a localization functor for W, then F lifts as a functor D ⥤ E. In this PR, this is generalized to bifunctors (or "functors in two variables") F : C₁ ⥤ C₂ ⥤ E, which may be lifted as a functor D₁ ⥤ D₂ ⥤ E under similar assumptions.

(We shall also need a version of this in three variables.)

Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Dec 11, 2024
@joelriou joelriou mentioned this pull request Dec 11, 2024
Closed
6 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 11, 2024

PR summary a3f5186238

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Localization.Bifunctor (new file) 417

Declarations diff

+ IsInvertedBy₂
+ Lifting₂
+ Lifting₂.flip
+ Lifting₂.fst
+ Lifting₂.iso
+ Lifting₂.liftingLift₂
+ Lifting₂.liftingLift₂Flip
+ Lifting₂.snd
+ Lifting₂.uncurry
+ curryObjProdComp
+ flipFunctor
+ fullyFaithfulUncurry
+ hom_inv_id_app_app
+ instance : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).Faithful
+ instance : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).Full
+ instance : Lifting₂ L₁ L₂ W₁ W₂ F (lift₂ F hF L₁ L₂)
+ inv_hom_id_app_app
+ lift₂
+ lift₂NatIso
+ lift₂NatTrans
+ lift₂NatTrans_app_app
+ lift₂_iso_hom_app_app₁
+ lift₂_iso_hom_app_app₂
+ natTrans₂_ext
+ whiskeringLeft₂

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

@dagurtomas
Copy link
Copy Markdown
Contributor

dagurtomas commented Dec 12, 2024

I am listed as a coauthor of the PR #12728 where this was developed, and I can confirm that the API works well there. I also did not contribute to this part, so:

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 12, 2024

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Dec 12, 2024
jcommelin
jcommelin reviewed Dec 13, 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 Dec 13, 2024
mathlib-bors bot pushed a commit that referenced this pull request Dec 13, 2024
@joelriou
feat(CategoryTheory/Localization): liftings of bifunctors (#19894)
383b074 
When a functor `F : C ⥤ E` inverts a class of morphisms `W : MorphismProperty C` and `L : C ⥤ D` is a localization functor for `W`, then `F` lifts as a functor `D ⥤ E`. In this PR, this is generalized to bifunctors (or "functors in two variables") `F : C₁ ⥤ C₂ ⥤ E`, which may be lifted as a functor `D₁ ⥤ D₂ ⥤ E` under similar assumptions.

(We shall also need a version of this in three variables.)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 13, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/Localization): liftings of bifunctors [Merged by Bors] - feat(CategoryTheory/Localization): liftings of bifunctors Dec 13, 2024
@mathlib-bors mathlib-bors bot closed this Dec 13, 2024
@mathlib-bors mathlib-bors bot deleted the localization-bifunctor branch December 13, 2024 08:15
@joelriou joelriou mentioned this pull request Jan 16, 2025
Closed
mathlib-bors bot pushed a commit that referenced this pull request Jan 20, 2025
@joelriou
feat(CategoryTheory): localization of trifunctors (#20788)
b733452 
In this PR, we study the localization of functors in three variables (similarly as #19894 was the case of functors in two variables). This shall be used in #12728 in order to obtain a monoidal structure on certain localized categories.
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

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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

@joelriou @dagurtomas @jcommelin