[Merged by Bors] - feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks by smorel394 · Pull Request #20363 · leanprover-community/mathlib4

smorel394 · 2024-12-31T14:11:48Z

Suppose that we use categories C and D equiped with a shifts by an additive monoid A, functors F,F' : C ⥤ D, a functor G : D ⥤ C, a natural transformation τ : F ⟶ F' and an adjunction adj between F and G.

For any map of additive monoids φ : B →+ A, we define type synonyms PullbackShift.functor F φ for F, PullbackShift.natTrans τ φ for τ, and PullbackShift.adjunction adj φ for adj. We then prove that a CommShift structure on F (resp. τ, resp. adj) induces a CommShift structure on PullbackShift.functor F φ (resp. PullbackShift.natTrans τ φ, resp. PullbackShift.adjunction adj φ ).
Similarly, we define type synonyms OppositeShift.functor A F for F.op, OppositeShift.natTrans A τ for τ.op and OppositeShift.adjunction A adj for adj.op, and prove that a CommShift structure on F (resp. τ, resp. adj) induces a CommShift structure on OppositeShift.functor A F (resp. OppositeShift.natTrans A τ, resp. OppositeShift.adjunction A adj ) for the naive shifts on the opposite categories.
The point of the second part is to reserve F.op etc to carry CommShift structures for the modified shift on the opposite categories used in the theory of (pre)triangulated categories. We illustrate this by simplifying the definition of the instance commShiftOpInt (a CommShift ℤ instance on F.op for the modified shifts) in the file Triangulated.Opposite.Functor.

depends on: [Merged by Bors] - chore(CategoryTheory/Shift): fix NatTrans.CommShift #20364

github-actions · 2024-12-31T14:12:40Z

PR summary 000cd46006

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Shift.Pullback	684	688	+4 (+0.58%)
Mathlib.CategoryTheory.Shift.Opposite	809	812	+3 (+0.37%)
Mathlib.CategoryTheory.Triangulated.Opposite.Functor	1150	1153	+3 (+0.26%)

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences`	1
`Mathlib.CategoryTheory.Triangulated.Yoneda`	2
6 files `Mathlib.CategoryTheory.Triangulated.Opposite.Functor` `Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated` `Mathlib.CategoryTheory.Shift.ShiftedHomOpposite` `Mathlib.CategoryTheory.Triangulated.Opposite.Triangle` `Mathlib.CategoryTheory.Shift.Opposite` `Mathlib.CategoryTheory.Triangulated.Opposite.Basic`	3
`Mathlib.CategoryTheory.Shift.Pullback`	4

Declarations diff

+ OppositeShift.adjunction
+ OppositeShift.functor
+ OppositeShift.natIsoComp
+ OppositeShift.natIsoId
+ OppositeShift.natTrans
+ PullbackShift.adjunction
+ PullbackShift.functor
+ PullbackShift.natIsoComp
+ PullbackShift.natIsoId
+ PullbackShift.natTrans
+ commShiftOp_iso_eq
+ instance : NatTrans.CommShift (OppositeShift.natIsoId C A).hom A
+ instance : NatTrans.CommShift (PullbackShift.natIsoComp φ F G).hom A
+ instance : NatTrans.CommShift (PullbackShift.natIsoId C φ).hom A
+ instance [F.CommShift A] [G.CommShift A] :
++ commShift_op
+++ on
-+++ commShiftPullback

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.

Decrease in tech debt: (relative, absolute) = (3.00, 0.00)

Current number	Change	Type
1512	-3	erw

Current commit 000cd46006
Reference commit 5e298f933b

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

Mathlib/CategoryTheory/Shift/Opposite.lean

mathlib4-dependent-issues-bot · 2025-01-03T12:23:31Z

This PR/issue depends on:

~~[Merged by Bors] - chore(CategoryTheory/Shift): fix NatTrans.CommShift #20364~~
By Dependent Issues (🤖). Happy coding!

Mathlib/CategoryTheory/Shift/Pullback.lean

Mathlib/CategoryTheory/Shift/Opposite.lean

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean

joelriou · 2025-01-10T14:42:06Z

Could you edit the PR description so that it matches more what the PR has become?

bors d+

smorel394 · 2025-01-10T15:06:43Z

Could you edit the PR description so that it matches more what the PR has become?

bors d+

I also changed the initial descriptions in the files themselves.

smorel394 · 2025-01-10T15:26:47Z

bors r+

mathlib-bors · 2025-01-10T15:26:50Z

🔒 Permission denied

Existing reviewers: click here to make smorel394 a reviewer

smorel394 · 2025-01-10T15:27:26Z

I think I got confused, I thought "bors d+" meant I was authorized to merge myself... Oh well.

joelriou · 2025-01-10T18:10:14Z

I do not know what happened...

bors merge

…: `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363) Suppose that we use categories `C` and `D` equiped with a shifts by an additive monoid `A`, functors `F,F' : C ⥤ D`, a functor `G : D ⥤ C`, a natural transformation `τ : F ⟶ F'` and an adjunction `adj` between `F` and `G`. * For any map of additive monoids `φ : B →+ A`, we define type synonyms `PullbackShift.functor F φ` for `F`, `PullbackShift.natTrans τ φ` for `τ`, and `PullbackShift.adjunction adj φ` for `adj`. We then prove that a `CommShift` structure on `F` (resp. `τ`, resp. `adj`) induces a `CommShift` structure on `PullbackShift.functor F φ` (resp. `PullbackShift.natTrans τ φ`, resp. `PullbackShift.adjunction adj φ` ). * Similarly, we define type synonyms `OppositeShift.functor A F` for `F.op`, `OppositeShift.natTrans A τ` for `τ.op` and `OppositeShift.adjunction A adj` for `adj.op`, and prove that a `CommShift` structure on `F` (resp. `τ`, resp. `adj`) induces a `CommShift` structure on `OppositeShift.functor A F` (resp. `OppositeShift.natTrans A τ`, resp. `OppositeShift.adjunction A adj` ) for the naive shifts on the opposite categories. * The point of the second part is to reserve `F.op` etc to carry `CommShift` structures for the modified shift on the opposite categories used in the theory of (pre)triangulated categories. We illustrate this by simplifying the definition of the instance `commShiftOpInt` (a `CommShift ℤ` instance on `F.op` for the modified shifts) in the file `Triangulated.Opposite.Functor`. - [x] depends on: #20364 Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

mathlib-bors · 2025-01-10T18:59:36Z

Pull request successfully merged into master.

Build succeeded:

…: `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363) Suppose that we use categories `C` and `D` equiped with a shifts by an additive monoid `A`, functors `F,F' : C ⥤ D`, a functor `G : D ⥤ C`, a natural transformation `τ : F ⟶ F'` and an adjunction `adj` between `F` and `G`. * For any map of additive monoids `φ : B →+ A`, we define type synonyms `PullbackShift.functor F φ` for `F`, `PullbackShift.natTrans τ φ` for `τ`, and `PullbackShift.adjunction adj φ` for `adj`. We then prove that a `CommShift` structure on `F` (resp. `τ`, resp. `adj`) induces a `CommShift` structure on `PullbackShift.functor F φ` (resp. `PullbackShift.natTrans τ φ`, resp. `PullbackShift.adjunction adj φ` ). * Similarly, we define type synonyms `OppositeShift.functor A F` for `F.op`, `OppositeShift.natTrans A τ` for `τ.op` and `OppositeShift.adjunction A adj` for `adj.op`, and prove that a `CommShift` structure on `F` (resp. `τ`, resp. `adj`) induces a `CommShift` structure on `OppositeShift.functor A F` (resp. `OppositeShift.natTrans A τ`, resp. `OppositeShift.adjunction A adj` ) for the naive shifts on the opposite categories. * The point of the second part is to reserve `F.op` etc to carry `CommShift` structures for the modified shift on the opposite categories used in the theory of (pre)triangulated categories. We illustrate this by simplifying the definition of the instance `commShiftOpInt` (a `CommShift ℤ` instance on `F.op` for the modified shifts) in the file `Triangulated.Opposite.Functor`. - [x] depends on: #20364 Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

* origin/master: (88 commits) chore(scripts): update nolints.json (#20672) chore: de-simp `map_eq_zero_iff_eq_one` (#20662) feat(Combinatorics/SimpleGraph): add independent sets (#18608) chore(CategoryTheory/Limits/Cones): functoriality of `mapCone` (#20641) feat(Algebra/Category/ModuleCat): pullback of presheaves of modules (#17366) feat(AlgebraicTopology): model categories (#19158) chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548) feat(Data/List/ReduceOption): add replicate theorems (#20644) feat: approximate subgroups (#20050) feat: use scoped trace nodes in linarith (#19855) feat: disjoint union of charted spaces (#20619) feat: add some term elaborators for reduction (#15192) feat(Topology/Category): category of delta-generated spaces (#19499) add a variable_alias for Quantale and AddQuantale (#19282) feat(Computability/DFA): implement `isRegular_iff` (#19940) chore: unpin and bump batteries and importgraph (#20651) chore: split `Mathlib/Algebra/Group/Int` (#20624) feat: three lemmas related to Hausdorff distance (#20585) chore: `initialize_simps_projections` for `Submodule` (#20582) feat(Order): Boolean algebra structure on idempotents (#20618) chore(CategoryTheory): moving/renaming Subpresheaf (#20583) refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630) feat: sets of doubling strictly less than 3/2 (#20572) chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452) feat: `s \ t ∩ u = (s ∩ u) \ t` (#20298) feat: product of subalgebras (#20202) feat: `Submodule.restrictScalars` commutes with `pow` (#20581) feat: `a ∈ s ^ n` iff there exists a sequence `f` of `n` elements of `s` such that `∏ i, f i = a` (#20580) chore: make `FooHom.coe_id` a `norm_cast` lemma (#20576) chore: use ofNat more (#20546) feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363) feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797) refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590) feat: Make `PNat.recOn` induction eliminator (#20617) feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608) feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574) feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573) chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611) feat: AbsoluteValue.IsNontrivial (#20588) chore(Data/Finsupp): split off extensionality from `Defs.lean` (#19092) chore(Data/Set): split the `CoeSort` instance to its own file (#19031) feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612) feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286) chore: cleanup more `erw` (#20601) chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587) chore: cleanup imports in PrimePow/Divisors (#20626) chore: split Algebra/BigOperators/Group/List (#20625) chore: reduce Topology->Order imports by moving content (#20627) chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592) refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333) ...

…riangulated functor is triangulated (#20543) If a functor `G : D ⥤ C` between pretriangulated categories is triangulated, and if we have an adjunction `F ⊣ G` (that commutes with the shifts), then `F` is also a triangulated functor. We prove this from the symmetric statement (`F` triangulated implies `G` triangulated) using opposite categories. - [ ] depends on: #20363 Co-authored-by: smorel394 <67864981+smorel394@users.noreply.github.com>

morel added 7 commits December 28, 2024 14:48

initial commit

d79e12b

doc

b54356d

def -> lemma

840309d

Merge remote-tracking branch 'origin' into SM.commShiftAdjunctionOp

fa0d8fb

reorganize stuff

dbde4ec

reboot one file

a2724fa

shorten proofs

1fe342f

github-actions bot added the t-category-theory Category theory label Dec 31, 2024

joelriou reviewed Dec 31, 2024

View reviewed changes

Mathlib/CategoryTheory/Shift/Opposite.lean Show resolved Hide resolved

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 31, 2024

morel added 6 commits December 31, 2024 17:57

mess

8e09a11

bigger mess

acd4d8c

unit

06dc16b

compiles but ugly

79a7266

slightly less ugly but still ugly

0ce99b8

fix 'Opposite'

60e37d7

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 1, 2025

Merge remote-tracking branch 'origin' into SM.commShiftAdjunctionOp

13b03f0

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 1, 2025

morel added 3 commits January 2, 2025 08:08

Merge remote-tracking branch 'origin' into SM.commShiftAdjunctionOp

76b26f6

doc strings

ddb89c9

cleanup

57cffa9

smorel394 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 2, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 2, 2025

morel added 2 commits January 2, 2025 14:44

pulled back adjunctions...

c1d0478

doc string

c340079

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 3, 2025

Merge remote-tracking branch 'origin' into SM.commShiftAdjunctionOp

a74a6e8

joelriou reviewed Jan 10, 2025

View reviewed changes

Mathlib/CategoryTheory/Shift/Pullback.lean Outdated Show resolved Hide resolved

joelriou reviewed Jan 10, 2025

View reviewed changes

Mathlib/CategoryTheory/Shift/Opposite.lean Outdated Show resolved Hide resolved

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 10, 2025

smorel394 and others added 4 commits January 10, 2025 09:53

Update Mathlib/CategoryTheory/Shift/Opposite.lean

36294b4

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

whitespace dark magic

b9837a8

Update Mathlib/CategoryTheory/Shift/Pullback.lean

2a5cd4e

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Update Mathlib/CategoryTheory/Shift/Opposite.lean

d5119fd

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

smorel394 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 10, 2025

joelriou reviewed Jan 10, 2025

View reviewed changes

Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean Outdated Show resolved Hide resolved

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 10, 2025

apply suggestion

d0df95d

smorel394 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 10, 2025

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 10, 2025

morel added 2 commits January 10, 2025 16:01

adjust doc

7dc0a6d

more doc

000cd46

ghost added the ready-to-merge This PR has been sent to bors. label Jan 10, 2025

mathlib-bors bot closed this Jan 10, 2025

mathlib-bors bot deleted the SM.commShiftAdjunctionOp branch January 10, 2025 18:59

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks#20363

[Merged by Bors] - feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks#20363
smorel394 wants to merge 38 commits intomasterfrom
SM.commShiftAdjunctionOp

smorel394 commented Dec 31, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Dec 31, 2024 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Jan 3, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joelriou commented Jan 10, 2025

Uh oh!

smorel394 commented Jan 10, 2025

Uh oh!

smorel394 commented Jan 10, 2025

Uh oh!

mathlib-bors bot commented Jan 10, 2025

Uh oh!

smorel394 commented Jan 10, 2025 •

edited

Loading

Uh oh!

joelriou commented Jan 10, 2025

Uh oh!

mathlib-bors bot commented Jan 10, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

smorel394 commented Dec 31, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Dec 31, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 000cd46006

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Jan 3, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joelriou commented Jan 10, 2025

Uh oh!

smorel394 commented Jan 10, 2025

Uh oh!

smorel394 commented Jan 10, 2025

Uh oh!

mathlib-bors bot commented Jan 10, 2025

Uh oh!

smorel394 commented Jan 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

joelriou commented Jan 10, 2025

Uh oh!

mathlib-bors bot commented Jan 10, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

smorel394 commented Dec 31, 2024 •

edited

Loading

github-actions bot commented Dec 31, 2024 •

edited

Loading

smorel394 commented Jan 10, 2025 •

edited

Loading