refactor: generalize universes for colimits and limits in Type #7020

joelriou · 2023-09-07T20:15:36Z

In the category Type u and other concrete categories, there are limits and colimits indexed by categories J : Type v when [UnivLE.{v, u}]. As the universe for morphisms in J is irrelevant, there is no longer any assumption that J is a small category.

The definition of the standard colimit cocone in Type u now uses Shrink (see CategoryTheory.Limits.Types), which broke some constructions of colimits which relied a little too much on the definitional properties of this cocone. While fixing these constructions, some proofs have been cleaned up. Assumptions on universes have been generalized when appropriate.

The same should be done for the standard limit cone, but I would rather attempt at this in a separate PR...

jcommelin · 2023-09-08T09:38:11Z

How does this PR mesh with the planned refactor to use univLE? This file is still using TypeMax, although the diff in the PR doesn't seem to touch it really. I haven't thought through the question myself.

joelriou · 2023-09-08T10:50:18Z

~~My PR is orthogonal to the UnivLE refactor, which seems to be done already for limits of types in this file, but not for colimits, where the colimit cocone is constructed only in TypeMax.~~

Ideally, under [UnivLE.{v, u)] we should have limits and colimits in Type u indexed by categories J such that J : Type v and [Category.{w} J] for any w. Currently, there is the irrelevant assumption that w = v. ~~My PR only removes any assumption on w, but maybe I should try to also adapt the construction of colimits under the assumption UnivLE.{v, u} rather than keeping only the TypeMax version.~~

alreadydone · 2023-10-24T00:32:41Z

~~There probably isn't much benefit to be garnered from this approach, so closing.~~

alreadydone · 2023-10-24T00:34:20Z

Sorry, I meant to close my own PR 😅

alreadydone

I like the generalizations made in this PR, but there are now merge conflicts. Also, I think many UnivLE.{v,u} can be replaced by Small.{u} J, and UnivLE is only really needed in HasLimits/HasLimitsOfSize instances, and Small is enough for HasLimitsOfShape. Do you think this is a good idea, and would you mind doing it?

Mathlib/Algebra/Category/Ring/FilteredColimits.lean

alreadydone · 2023-10-24T00:16:49Z

Mathlib/CategoryTheory/Limits/Types.lean

--porting note: @[simp] was removed because the linter said it was useless
-theorem Colimit.ι_map_apply {F G : J ⥤ TypeMax.{v, u}} (α : F ⟶ G) (j : J) (x : F.obj j) :
-    colim.{v, v}.map α (colimit.ι F j x) = colimit.ι G j (α.app j x) :=
-  congr_fun (colimit.ι_map α j) x
-#align category_theory.limits.types.colimit.ι_map_apply CategoryTheory.Limits.Types.Colimit.ι_map_apply
-
 @[simp]
-theorem Colimit.w_apply' {F : J ⥤ Type v} {j j' : J} {x : F.obj j} (f : j ⟶ j') :
-    colimit.ι F j' (F.map f x) = colimit.ι F j x :=
-  congr_fun (colimit.w F f) x
-#align category_theory.limits.types.colimit.w_apply' CategoryTheory.Limits.Types.Colimit.w_apply'
-
-@[simp]
-theorem Colimit.ι_desc_apply' (F : J ⥤ Type v) (s : Cocone F) (j : J) (x : F.obj j) :
-    colimit.desc F s (colimit.ι F j x) = s.ι.app j x :=
-  congr_fun (colimit.ι_desc s j) x
-#align category_theory.limits.types.colimit.ι_desc_apply' CategoryTheory.Limits.Types.Colimit.ι_desc_apply'


Should we change these to #noaligns, or we don't care?

alreadydone · 2023-10-24T00:20:55Z

Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean

-variable [HasColimitsOfShape J TopCat.{v}]
+variable [UnivLE.{u', v}]


Why this change? I think it's now less general?

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

joelriou · 2023-11-30T12:47:34Z

I am closing this as @alreadydone may have found a better approach.

@dagurtomas

Rescuing and porting my [old proof](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/tensor.20products.20commute.20with.20direct.20limits/near/275178330) now that @dagurtomas created a file for it. Also includes some universe generalizations in the file Limits/Types which overlap with @joelriou's #7020. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

This is a smaller version of #7020. Before this PR, for limits, we gave instances for small indexing categories, but for colimits, we gave instances for `TypeMax`. This PR changes so that we give instances for small indexing categories in both cases. This is more general and also more uniform. Co-authored-by: Joël Riou <rioujoel@gmail.com>

joelriou added 4 commits September 7, 2023 21:33

feat: generalize universes for limits and colimits in Type

a08f3a1

trying to fix the build

861c6e0

fixing the build

b2c9343

removed unnecessary instances

2406654

joelriou added WIP Work in progress t-category-theory Category theory labels Sep 7, 2023

joelriou changed the title ~~feat: generalizing universes for colimits and limits in Type~~ feat: generalize universes for colimits and limits in Type Sep 7, 2023

trying to fix the build

473ada0

joelriou added awaiting-CI and removed WIP Work in progress labels Sep 7, 2023

github-actions bot removed the awaiting-CI label Sep 7, 2023

joelriou added the awaiting-review The author would like community review of the PR label Sep 7, 2023

joelriou added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 8, 2023

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Sep 12, 2023

Merge remote-tracking branch 'origin' into colimit-types-universes

8bf4172

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Sep 13, 2023

bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:27

semorrison changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:05

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Sep 21, 2023

Merge remote-tracking branch 'origin' into colimit-types-universes

29d7960

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Oct 5, 2023

joelriou added 6 commits October 5, 2023 13:27

using UnivLE for colimits of types

f311377

trying to fix the build

739c618

trying to fix the build

df1cd39

trying to fix the build

4a9e6fb

fixed colimits in TopCat

a6ffd85

fixed Limits.Final

de4e97d

joelriou added the awaiting-review The author would like community review of the PR label Oct 6, 2023

joelriou mentioned this pull request Oct 15, 2023

refactor: redefine UnivLE #7695

Closed

leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Oct 16, 2023

alreadydone closed this Oct 24, 2023

alreadydone reopened this Oct 24, 2023

alreadydone reviewed Oct 24, 2023

View reviewed changes

joelriou added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 24, 2023

joelriou and others added 2 commits October 25, 2023 10:00

Update Mathlib/Algebra/Category/Ring/FilteredColimits.lean

1f203ee

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Merge remote-tracking branch 'origin' into colimit-types-universes

9524722

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Oct 25, 2023

joelriou added 2 commits October 25, 2023 10:54

fixing the build

88c752b

wip

78bce0b

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Oct 26, 2023

alreadydone mentioned this pull request Nov 21, 2023

[Merged by Bors] - feat: uliftFunctor preserves arbitrary colimits #8545

Closed

joelriou closed this Nov 30, 2023

TwoFX mentioned this pull request Mar 4, 2024

[Merged by Bors] - refactor: generalize universes for colimits in Type #11148

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

refactor: generalize universes for colimits and limits in Type #7020

refactor: generalize universes for colimits and limits in Type #7020

joelriou commented Sep 7, 2023 •

edited

Loading

jcommelin commented Sep 8, 2023

joelriou commented Sep 8, 2023 •

edited

Loading

alreadydone commented Oct 24, 2023 •

edited

Loading

alreadydone commented Oct 24, 2023

alreadydone left a comment •

edited

Loading

alreadydone Oct 24, 2023

alreadydone Oct 24, 2023

joelriou commented Nov 30, 2023

		variable [HasColimitsOfShape J TopCat.{v}]
		variable [UnivLE.{u', v}]

refactor: generalize universes for colimits and limits in Type #7020

refactor: generalize universes for colimits and limits in Type #7020

Conversation

joelriou commented Sep 7, 2023 • edited Loading

jcommelin commented Sep 8, 2023

joelriou commented Sep 8, 2023 • edited Loading

alreadydone commented Oct 24, 2023 • edited Loading

alreadydone commented Oct 24, 2023

alreadydone left a comment • edited Loading

Choose a reason for hiding this comment

alreadydone Oct 24, 2023

Choose a reason for hiding this comment

alreadydone Oct 24, 2023

Choose a reason for hiding this comment

joelriou commented Nov 30, 2023

joelriou commented Sep 7, 2023 •

edited

Loading

joelriou commented Sep 8, 2023 •

edited

Loading

alreadydone commented Oct 24, 2023 •

edited

Loading

alreadydone left a comment •

edited

Loading