Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: port/CategoryTheory.Limits.HasLimits #2368

Closed
wants to merge 27 commits into from
Closed

[Merged by Bors] - feat: port/CategoryTheory.Limits.HasLimits #2368

wants to merge 27 commits into from

Conversation

mattrobball
Copy link
Collaborator

@mattrobball mattrobball commented Feb 19, 2023 •
edited by github-actions bot

@mattrobball mattrobball added the mathlib-port This is a port of a theory file from mathlib. label Feb 19, 2023
@semorrison semorrison added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Feb 19, 2023
@mattrobball mattrobball mentioned this pull request Feb 19, 2023
Closed
1 task
@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 20, 2023
This was referenced Feb 22, 2023
Closed
Closed
@mattrobball mattrobball force-pushed the port/CategoryTheory.Limits.HasLimits branch from d0a99d9 to 6912297 Compare February 25, 2023 01:45
@mattrobball
# This is a combination of 126 commits.
8fcb216 
# This is the 1st commit message:

automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean

# The commit message #2 will be skipped:

# feat: port CategoryTheory.Limits.IsLimit

# The commit message #3 will be skipped:

# Initial file copy from mathport

# The commit message #4 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #5 will be skipped:

# feat: port CategoryTheory.Limits.Cones

# The commit message #6 will be skipped:

# Initial file copy from mathport

# The commit message #7 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #8 will be skipped:

# feat: port CategoryTheory.Yoneda

# The commit message #9 will be skipped:

# Initial file copy from mathport

# The commit message #10 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #11 will be skipped:

# feat: port CategoryTheory.Functor.Currying

# The commit message #12 will be skipped:

# Initial file copy from mathport

# The commit message #13 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #14 will be skipped:

# fix all but one decl

# The commit message #15 will be skipped:

# fix last errors

# The commit message #16 will be skipped:

# feat: port CategoryTheory.Functor.Hom

# The commit message #17 will be skipped:

# Initial file copy from mathport

# The commit message #18 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #19 will be skipped:

# feat: port CategoryTheory.Types

# The commit message #20 will be skipped:

# Initial file copy from mathport

# The commit message #21 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #22 will be skipped:

# feat: port CategoryTheory.EpiMono

# The commit message #23 will be skipped:

# Initial file copy from mathport

# The commit message #24 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #25 will be skipped:

# feat: port CategoryTheory.Groupoid

# The commit message #26 will be skipped:

# Initial file copy from mathport

# The commit message #27 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #28 will be skipped:

# feat: port CategoryTheory.Pi.Basic

# The commit message #29 will be skipped:

# Initial file copy from mathport

# The commit message #30 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #31 will be skipped:

# fix some errors

# The commit message #32 will be skipped:

# some more fixes

# The commit message #33 will be skipped:

# more fixes

# The commit message #34 will be skipped:

# finally fixed

# The commit message #35 will be skipped:

# lint

# The commit message #36 will be skipped:

# add porting note for scary warning

# The commit message #37 will be skipped:

# add porting note about proliferation of match

# The commit message #38 will be skipped:

# initial pass

# The commit message #39 will be skipped:

# fix errors

# The commit message #40 will be skipped:

# lint

# The commit message #41 will be skipped:

# fix errors; lint; add porting notes

# The commit message #42 will be skipped:

# fix errors; lint; add porting note

# The commit message #43 will be skipped:

# fix error

# The commit message #44 will be skipped:

# fix some errors

# The commit message #45 will be skipped:

# minor fixes

# The commit message #46 will be skipped:

# fix all but four

# The commit message #47 will be skipped:

# fix last errors; lint

# The commit message #48 will be skipped:

# feat: port CategoryTheory.DiscreteCategory

# The commit message #49 will be skipped:

# Initial file copy from mathport

# The commit message #50 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #51 will be skipped:

# get file to build

# The commit message #52 will be skipped:

# lint

# The commit message #53 will be skipped:

# lint some more

# The commit message #54 will be skipped:

# feat: port CategoryTheory.Functor.ReflectsIsomorphisms

# The commit message #55 will be skipped:

# Initial file copy from mathport

# The commit message #56 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #57 will be skipped:

# feat: port CategoryTheory.Functor.EpiMono

# The commit message #58 will be skipped:

# Initial file copy from mathport

# The commit message #59 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #60 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Adjunction

# The commit message #61 will be skipped:

# Initial file copy from mathport

# The commit message #62 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #63 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Basic

# The commit message #64 will be skipped:

# Initial file copy from mathport

# The commit message #65 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #66 will be skipped:

# feat: port CategoryTheory.CommSq

# The commit message #67 will be skipped:

# Initial file copy from mathport

# The commit message #68 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #69 will be skipped:

# first pass

# The commit message #70 will be skipped:

# names and removing restate_axiom

# The commit message #71 will be skipped:

# fix lint

# The commit message #72 will be skipped:

# remove spurious edit

# The commit message #73 will be skipped:

# fix errors; lint

# The commit message #74 will be skipped:

# feat: port CategoryTheory.Adjunction.Basic

# The commit message #75 will be skipped:

# Initial file copy from mathport

# The commit message #76 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #77 will be skipped:

# Initial file copy from mathport

# The commit message #78 will be skipped:

# Mathbin -> Mathlib; add import to Mathlib.lean

# The commit message #79 will be skipped:

# push it as far as possible

# The commit message #80 will be skipped:

# minor changes

# The commit message #81 will be skipped:

# seems to work

# The commit message #82 will be skipped:

# add example and equivalence file for testing

# The commit message #83 will be skipped:

# test: create `slice.lean` test file

# The commit message #84 will be skipped:

# remove equivalence.lean

# The commit message #85 will be skipped:

# remove rewriteTarget'; change MonadExceptOf to MonadExcept

# The commit message #86 will be skipped:

# add documentation and clean up

# The commit message #87 will be skipped:

# move iteration tactics to core

# The commit message #88 will be skipped:

# modify documentation lines

# The commit message #89 will be skipped:

# add module documentation(?)

# The commit message #90 will be skipped:

# fix module docs

# The commit message #91 will be skipped:

# fix test/slice.lean

# The commit message #92 will be skipped:

# fix all but refl error

# The commit message #93 will be skipped:

# fix refl error and lint errors

# The commit message #94 will be skipped:

# fix final long line

# The commit message #95 will be skipped:

# use `Mathport` syntax
# * use existing docs
# * fix docs typos

# The commit message #96 will be skipped:

# test: add simple `rhs`/`lhs` tests

# The commit message #97 will be skipped:

# minor changes to `Tactic.Core`
# * use `m` instead of `TacticM` now that we use `MonadExcept`
# * simplify code for `iterateRange`
# * minor docs tweaks

# The commit message #98 will be skipped:

# update slice naming

# The commit message #99 will be skipped:

# some progress

# The commit message #100 will be skipped:

# only one error left

# The commit message #101 will be skipped:

# filled in last sorry

# The commit message #102 will be skipped:

# break long lines

# The commit message #103 will be skipped:

# delete linter command

# The commit message #104 will be skipped:

# fix comments

# The commit message #105 will be skipped:

# fix two simpNF lints

# The commit message #106 will be skipped:

# fill in some docstrings

# The commit message #107 will be skipped:

# fix most linter issues

# The commit message #108 will be skipped:

# add missing aligns for fields; lint

# The commit message #109 will be skipped:

# restore lost import line

# The commit message #110 will be skipped:

# fix errors; lint

# The commit message #111 will be skipped:

# feat: port CategoryTheory.Limits.Shapes.StrongEpi

# The commit message #112 will be skipped:

# Initial file copy from mathport

# The commit message #113 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #114 will be skipped:

# fix errors; lint

# The commit message #115 will be skipped:

# Update Mathlib.lean

# The commit message #116 will be skipped:

# fix errors; lint

# The commit message #117 will be skipped:

# fix errors; lint; shorten filename

# The commit message #118 will be skipped:

# fix some errors

# The commit message #119 will be skipped:

# fix some more

# The commit message #120 will be skipped:

# fix errors

# The commit message #121 will be skipped:

# lint

# The commit message #122 will be skipped:

# fix errors

# The commit message #123 will be skipped:

# lint

# The commit message #124 will be skipped:

# feat: port CategoryTheory.Category.Ulift

# The commit message #125 will be skipped:

# Initial file copy from mathport

# The commit message #126 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean
@mattrobball
automated fixes
f1c2148 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@mattrobball
automated fixes
2f25984 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@mattrobball
fix all but one decl
f7dcf96
@mattrobball
fix final error
a45d823
@mattrobball
try fix-comments.py
6373462 
only fixed a single issue for the second time now
@mattrobball
lint for CI
4dfea81
@mattrobball
align names in comments
4534cda
@mattrobball
fix import file
843cf69
@mattrobball
fix import line typo
6979193
@mattrobball
fix case error
90d60fc
@mattrobball
add updated files
9dfd1d9
@mattrobball
move names to new convention
d3d56ee
@mattrobball mattrobball force-pushed the port/CategoryTheory.Limits.HasLimits branch from 6912297 to d3d56ee Compare February 25, 2023 01:50
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 25, 2023
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Feb 27, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 27, 2023
@mattrobball mattrobball added awaiting-review The author would like community review of the PR and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Feb 27, 2023
ChrisHughes24
ChrisHughes24 reviewed Feb 27, 2023
View reviewed changes
Mathlib/CategoryTheory/Limits/HasLimits.lean Outdated
instance [h : HasLimit ((D ⋙ E) ⋙ F)] : HasLimit (D ⋙ E ⋙ F) where
exists_limit := by
rw [← Functor.assoc]
exact h.exists_limit
Copy link
Member

Choose a reason for hiding this comment

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

I think a Type class inference expert needs to look at this. @gebner is this going to cause problems? It looks like there's some loop going on but maybe it's okay.

Copy link
Contributor

Choose a reason for hiding this comment

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

What goes wrong if you remove these two instances?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Everything below it goes red because it cannot synthesize them. Since Lean cannot currently go from (f \circ g) \circ h to f \circ (g \circ h), inside HasLimit I don't think it can go back. But probably the safest thing is to add them to the declarations manually.

Copy link
Contributor

Choose a reason for hiding this comment

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

BTW, since associativity of functor composition is true by definition, these instances could be replaced with:

instance [h : HasLimit (D ⋙ E ⋙ F)] : HasLimit ((D ⋙ E) ⋙ F) := h
instance [h : HasLimit ((D ⋙ E) ⋙ F)] : HasLimit (D ⋙ E ⋙ F) := h

But we should figure out whether these instances will cause issues as Chris suggested.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Oh yeah. I didn't realize I did both directions. Yeesh

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

BTW, since associativity of functor composition is true by definition, these instances could be replaced with:

instance [h : HasLimit (D ⋙ E ⋙ F)] : HasLimit ((D ⋙ E) ⋙ F) := h
instance [h : HasLimit ((D ⋙ E) ⋙ F)] : HasLimit (D ⋙ E ⋙ F) := h

But we should figure out whether these instances will cause issues as Chris suggested.

This works. But this is the best I can do for the result is

theorem limit.pre_pre [h : HasLimit (D ⋙  E ⋙  F)] : haveI : HasLimit ((D ⋙  E) ⋙  F) := h;
    limit.pre F E ≫ limit.pre (E ⋙ F) D = limit.pre F (D ⋙ E) := by
  haveI : HasLimit ((D ⋙  E) ⋙  F) := h
  ext j; erw [assoc, limit.pre_π, limit.pre_π, limit.pre_π]; rfl

One haveI doesn't suffice...

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I've made these changes and removed the global instances.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Regardless of looping, I've concluded this is a dumb thing to do.

adamtopaz
adamtopaz reviewed Feb 27, 2023
View reviewed changes
Mathlib/CategoryTheory/Limits/HasLimits.lean Outdated
Comment on lines 532 to 552
@[simps obj]
def lim : (J ⥤ C) ⥤ C where
obj F := limit F
map α := limMap α
map_id F := by
apply Limits.limit.hom_ext; intro j
erw [limMap_π, Category.id_comp, Category.comp_id]
map_comp α β := by
apply Limits.limit.hom_ext; intro j
erw [assoc, IsLimit.fac, IsLimit.fac, ← assoc, IsLimit.fac, assoc]; rfl
#align category_theory.limits.lim CategoryTheory.Limits.lim

end

variable {G : J ⥤ C} (α : F ⟶ G)

-- We generate this manually since `simps` gives it a weird name.
@[simp]
theorem limMap_eq_limMap : lim.map α = limMap α :=
rfl
#align category_theory.limits.lim_map_eq_lim_map CategoryTheory.Limits.limMap_eq_limMap
Copy link
Contributor

Choose a reason for hiding this comment

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

I think we can now just use @[simps] and get rid og limMap_eq_limMap.

It seems that we don't have an analogue of limMap_eq_limMap for colimits, and that colim is tagged with [simps obj] only, which is strange IMO.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

File seems fine if I do this.

jcommelin
jcommelin reviewed Feb 28, 2023
View reviewed changes
Mathlib/CategoryTheory/Limits/HasLimits.lean Outdated Show resolved Hide resolved
Mathlib/CategoryTheory/Limits/HasLimits.lean Show resolved Hide resolved
Mathlib/CategoryTheory/Limits/HasLimits.lean Outdated Show resolved Hide resolved
Mathlib/CategoryTheory/Limits/HasLimits.lean Outdated Show resolved Hide resolved
Mathlib/CategoryTheory/Limits/HasLimits.lean Outdated Show resolved Hide resolved
jcommelin
jcommelin reviewed Feb 28, 2023
View reviewed changes
Copy link
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.

bors d+

@bors
Copy link

bors bot commented Feb 28, 2023

✌️ mattrobball can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@semorrison semorrison added delegated and removed awaiting-review The author would like community review of the PR labels Feb 28, 2023
@mattrobball mattrobball mentioned this pull request Feb 28, 2023
Closed
1 task
@mattrobball
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Feb 28, 2023
@mattrobball
feat: port/CategoryTheory.Limits.HasLimits (#2368)
7b5ca5d
@bors
Copy link

bors bot commented Feb 28, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port/CategoryTheory.Limits.HasLimits [Merged by Bors] - feat: port/CategoryTheory.Limits.HasLimits Feb 28, 2023
@bors bors bot closed this Feb 28, 2023
@bors bors bot deleted the port/CategoryTheory.Limits.HasLimits branch February 28, 2023 21:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@adamtopaz adamtopaz adamtopaz left review comments

@jcommelin jcommelin jcommelin left review comments

@ChrisHughes24 ChrisHughes24 ChrisHughes24 left review comments

Assignees
No one assigned
Labels
delegated mathlib-port This is a port of a theory file from mathlib.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@mattrobball @semorrison @adamtopaz @jcommelin @ChrisHughes24