[Merged by Bors] - chore(category_theory/limits): Generalize universes for limits #10243

erdOne · 2021-11-09T14:21:47Z

Aware: ulift_functor ahead. Should I keep a universe unchanged version for these?
Update: only one occurrence downstream needed additional ulifts. I think its good for now.

erdOne · 2021-11-09T15:21:47Z

The thing about abbreviation is that I can no longer write has_limits C := {} and let auto_param do its job since Lean parses it into the empty set.

erdOne · 2021-11-09T20:58:22Z

src/category_theory/limits/has_limits.lean

+/--
+`C` has all limits of size `v u` (`has_limits_of_size.{v u} C`)
+if it has limits of every shape `J : Type u` with `[category.{v} J]`.
+-/
+class has_limits_of_size : Prop :=
 (has_limits_of_shape :
-  Π (J : Type v) [𝒥 : small_category J], has_limits_of_shape J C . tactic.apply_instance)
+  Π (J : Type u₁) [𝒥 : category.{v₁} J], has_limits_of_shape J C . tactic.apply_instance)
+
+/-- `C` has all (small) limits if it has limits of every shape that is as big as its hom-sets. -/
+abbreviation has_limits (C : Type u) [category.{v} C] : Prop := has_limits_of_size.{v v} C
+
+lemma has_limits.has_limits_of_shape {C : Type u} [category.{v} C] [has_limits C]
+  (J : Type v) [category.{v} J] :
+  has_limits_of_shape J C := has_limits_of_size.has_limits_of_shape J


This (and its dual) is the major definitional change in this PR.
has_limits still means about the same thing, but lean seems to lose some ability to infer some types here and there and thus type and universe annotations needed to be added here and there.

I'm not sure I understand this claim. In several place I see that ulift gets added. Certainly ulift X is not defeq to X, right? I think there are many definitional changes in this PR.

…ity/mathlib into limit_universe

jcommelin

Thanks a lot for taking this on! I thought it would be a very nasty can of worms. But it seems to go quite well 🐙

jcommelin · 2021-11-15T18:55:37Z

src/category_theory/category/ulift.lean

@@ -45,21 +45,21 @@ variables {C : Type u₁} [category.{v₁} C]

 /-- The functorial version of `ulift.up`. -/
 @[simps]
-def ulift.up : C ⥤ (ulift.{u₂} C) :=
+def ulift.up_functor : C ⥤ (ulift.{u₂} C) :=


Why did you change this name?

It conflicts with _root_.ulift.up in lots of files when I tried to import this into has_limits.lean.
It (and the definitions using it) is never used outside of this file, so I thought it would be faster if I changed the name of this.

src/category_theory/category/ulift.lean

src/category_theory/fin_category.lean

src/category_theory/limits/has_limits.lean

jcommelin · 2021-11-15T19:04:39Z

src/category_theory/limits/has_limits.lean

@@ -212,11 +223,12 @@ The isomorphism (in `Type`) between
 morphisms from a specified object `W` to the limit object,
 and cones with cone point `W`.
 -/
-def limit.hom_iso (F : J ⥤ C) [has_limit F] (W : C) : (W ⟶ limit F) ≅ (F.cones.obj (op W)) :=
+def limit.hom_iso (F : J ⥤ C) [has_limit F] (W : C) :
+  ulift.{u₁} (W ⟶ limit F : Type v) ≅ (F.cones.obj (op W)) :=


Will we also still need a version without ulift for easy use when the universe variables are the same?

Based on the use case downstream, I think this works fine when composing with ulift_trivial.

jcommelin · 2021-11-15T19:05:53Z

src/category_theory/limits/has_limits.lean

+/--
+`C` has all limits of size `v u` (`has_limits_of_size.{v u} C`)
+if it has limits of every shape `J : Type u` with `[category.{v} J]`.
+-/
+class has_limits_of_size : Prop :=
 (has_limits_of_shape :
-  Π (J : Type v) [𝒥 : small_category J], has_limits_of_shape J C . tactic.apply_instance)
+  Π (J : Type u₁) [𝒥 : category.{v₁} J], has_limits_of_shape J C . tactic.apply_instance)
+
+/-- `C` has all (small) limits if it has limits of every shape that is as big as its hom-sets. -/
+abbreviation has_limits (C : Type u) [category.{v} C] : Prop := has_limits_of_size.{v v} C
+
+lemma has_limits.has_limits_of_shape {C : Type u} [category.{v} C] [has_limits C]
+  (J : Type v) [category.{v} J] :
+  has_limits_of_shape J C := has_limits_of_size.has_limits_of_shape J


I'm not sure I understand this claim. In several place I see that ulift gets added. Certainly ulift X is not defeq to X, right? I think there are many definitional changes in this PR.

jcommelin · 2021-11-15T19:06:30Z

src/category_theory/limits/shapes/finite_products.lean

+/-- We can now write this for powers. -/
+noncomputable example [has_finite_products C] (X : C) : C := ∏ (λ (i : fin 5), X)
+


It's really cool that this is now possible!

jcommelin

Thanks 🎉

bors merge

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

bors · 2021-11-26T06:45:08Z

Build failed:

Lint mathlib

jcommelin

Thanks 🎉

bors merge

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

bors · 2021-11-26T11:59:11Z

Pull request successfully merged into master.

Build succeeded:

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

First try

2d1960f

erdOne added WIP Work in progress RFC Request for comment awaiting-CI The author would like to see what CI has to say before doing more work. labels Nov 9, 2021

erdOne added 6 commits November 9, 2021 22:23

Fix

917338f

fix lint

befe1f1

fix

eadf1fd

fix

f1b2905

fix

209ca33

more fix

6ca5efc

erdOne and others added 15 commits November 9, 2021 23:22

fix

5ae8f2d

fix

e0025f2

fix

2a0b8ac

fix

407a2e8

fix

c2b98d3

fix

e4273ed

fix

2f9515a

fix

a7e8527

fix

a5af627

fix

73ec1c4

fix

0928549

fix

ad110d9

fix

3e60b9b

Added results about functor categories

61da679

Update fin_category.lean

c72fee1

erdOne commented Nov 9, 2021

View reviewed changes

erdOne added 3 commits November 10, 2021 05:24

Better universe API?

d8e772c

fix

492efcb

Merge branch 'limit_universe' of https://github.com/leanprover-commun…

4434859

…ity/mathlib into limit_universe

erdOne added the awaiting-review The author would like community review of the PR label Nov 11, 2021

erdOne moved this from In progress to Pending review in Algebraic geometry Nov 11, 2021

jcommelin reviewed Nov 15, 2021

View reviewed changes

jcommelin 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 Nov 15, 2021

address review comments.

e57e6a1

erdOne added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 17, 2021

jcommelin requested review from semorrison, b-mehta and adamtopaz November 17, 2021 07:57

jcommelin approved these changes Nov 26, 2021

View reviewed changes

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Nov 26, 2021

bors bot pushed a commit that referenced this pull request Nov 26, 2021

chore(category_theory/limits): Generalize universes for limits (#10243)

c735564

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

erdOne and others added 6 commits November 26, 2021 14:46

Merge remote-tracking branch 'origin' into limit_universe

a2b9f14

fix

c1d5339

fix

c3aa508

fix timeout

a7b6cbd

fix

36d0950

fix

5fd3fd1

jcommelin approved these changes Nov 26, 2021

View reviewed changes

bors bot pushed a commit that referenced this pull request Nov 26, 2021

chore(category_theory/limits): Generalize universes for limits (#10243)

36f33d0

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

bors bot changed the title ~~chore(category_theory/limits): Generalize universes for limits~~ [Merged by Bors] - chore(category_theory/limits): Generalize universes for limits Nov 26, 2021

bors bot closed this Nov 26, 2021

Algebraic geometry automation moved this from Pending review to Done Nov 26, 2021

ericrbg pushed a commit that referenced this pull request Nov 27, 2021

chore(category_theory/limits): Generalize universes for limits (#10243)

3484793

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

jcommelin pushed a commit that referenced this pull request Dec 18, 2021

chore(category_theory/limits): Generalize universes for limits (#10243)

d563ab9

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(category_theory/limits): Generalize universes for limits #10243

[Merged by Bors] - chore(category_theory/limits): Generalize universes for limits #10243

erdOne commented Nov 9, 2021 •

edited

Loading

erdOne commented Nov 9, 2021

erdOne Nov 9, 2021 •

edited

Loading

jcommelin Nov 15, 2021

jcommelin left a comment

jcommelin Nov 15, 2021

erdOne Nov 17, 2021

jcommelin Nov 15, 2021

erdOne Nov 17, 2021

jcommelin Nov 15, 2021

jcommelin Nov 15, 2021

jcommelin left a comment

bors bot commented Nov 26, 2021

jcommelin left a comment

bors bot commented Nov 26, 2021

		/-- We can now write this for powers. -/
		noncomputable example [has_finite_products C] (X : C) : C := ∏ (λ (i : fin 5), X)

[Merged by Bors] - chore(category_theory/limits): Generalize universes for limits #10243

[Merged by Bors] - chore(category_theory/limits): Generalize universes for limits #10243

Conversation

erdOne commented Nov 9, 2021 • edited Loading

erdOne commented Nov 9, 2021

erdOne Nov 9, 2021 • edited Loading

Choose a reason for hiding this comment

jcommelin Nov 15, 2021

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

jcommelin Nov 15, 2021

Choose a reason for hiding this comment

erdOne Nov 17, 2021

Choose a reason for hiding this comment

jcommelin Nov 15, 2021

Choose a reason for hiding this comment

erdOne Nov 17, 2021

Choose a reason for hiding this comment

jcommelin Nov 15, 2021

Choose a reason for hiding this comment

jcommelin Nov 15, 2021

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Nov 26, 2021

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Nov 26, 2021

erdOne commented Nov 9, 2021 •

edited

Loading

erdOne Nov 9, 2021 •

edited

Loading