Skip to content

feat: port CategoryTheory.NatIso#820

Merged
kim-em merged 17 commits intomasterfrom
CategoryTheory.NatIso
Dec 4, 2022
Merged

feat: port CategoryTheory.NatIso#820
kim-em merged 17 commits intomasterfrom
CategoryTheory.NatIso

Conversation

@rosborn
Copy link
Copy Markdown
Contributor

@rosborn rosborn commented Dec 2, 2022 •
edited by github-actions bot
Loading

mathlib SHA: 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904

Porting Notes:
1. category.assoc isn't able to be used in rewrites or simps. It has a more general type than in mathlib3 which may be causing issues.
2. Iso.inv_hom_id_app_assoc and Iso.inv_hom_id_assoc generated by reassoc has a different type than in mathlib3
4. aesop fails to prove hom_inv_id and inv_hom_id in the definition of ofComponents. This is likely due to aesop not using ext lemmas.

@rosborn rosborn added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Dec 2, 2022
kim-em
kim-em reviewed Dec 2, 2022
View reviewed changes
kim-em
kim-em reviewed Dec 2, 2022
View reviewed changes
kim-em
kim-em reviewed Dec 2, 2022
View reviewed changes
kim-em
kim-em reviewed Dec 2, 2022
View reviewed changes
@ChrisHughes24
Copy link
Copy Markdown
Member

ChrisHughes24 commented Dec 2, 2022

In what sense is the definition of Category.assoc more general than in Lean3?

@rosborn
Copy link
Copy Markdown
Contributor Author

rosborn commented Dec 2, 2022

Yea, sorry. The category.assoc problem was me being braindead. There does seem to be a divergence in how reassoc is generating theorems.
In mathlib3, it converted α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X) into α.inv.app X ≫ α.hom.app X ≫ f' = f', but in mathlib4 it converted it into app (α.inv ≫ α.hom) X ≫ h = app (𝟙 G) X ≫ h

@rosborn rosborn added help-wanted The author needs attention to resolve issues and removed WIP Work in progress labels Dec 2, 2022
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 2, 2022 •
edited
Loading

Re: 4. Please use aesop_cat.

(Err, this is broken, see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/hygiene.20question.3F/near/313556764. Hopefully fixed soon.)

Edit: fixed in #825.

@kim-em kim-em added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review and removed help-wanted The author needs attention to resolve issues labels Dec 2, 2022
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 2, 2022

Okay, I think we are down to just one issue: ext won't apply IsIso.inv_eq_of_hom_inv_id anymore, because it's not of the shape ext wants.

Options:

  1. decide that ext should be more capable
  2. tag these lemmas with apply in aesop_cat.
  3. ???

Option 2. seems fine to me; it's effectively what we were doing previously via tidy+ext.

@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 3, 2022
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 3, 2022

This PR/issue depends on:

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 3, 2022

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 3, 2022
@github-actions github-actions bot mentioned this pull request Dec 4, 2022
Closed
@kim-em kim-em merged commit 8aaf280 into master Dec 4, 2022
@bors bors bot deleted the CategoryTheory.NatIso branch December 4, 2022 02:02
rosborn added a commit that referenced this pull request Dec 4, 2022
@rosborn
Merge branch 'master' into CategoryTheory.Functor.FullyFaithful
a57ac3a 
* master:
  chore: parallelize testing in CI (#845)
  feat: Match mathlib#17801 (#839)
  feat: Match mathlib#16761 (#840)
  feat: port CategoryTheory.NatIso (#820)
  feat: port algebra.ring.basic (#830)
  feat: port Combinatorics.Quiver.ConnectedComponent (#836)
  chore: bump to nightly-2022-12-03 (#838)
@github-actions github-actions bot mentioned this pull request Dec 6, 2022
Open
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Dec 6, 2022
@jcommelin
chore(*): add mathlib4 synchronization comments (#17806)
8770c84 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.divisibility.basic`: leanprover-community/mathlib4#833
* `algebra.group.with_one.defs`: leanprover-community/mathlib4#841
* `algebra.hom.commute`: leanprover-community/mathlib4#831
* `algebra.hom.group`: leanprover-community/mathlib4#659
* `algebra.hom.units`: leanprover-community/mathlib4#745
* `algebra.ring.basic`: leanprover-community/mathlib4#830
* `category_theory.natural_isomorphism`: leanprover-community/mathlib4#820
* `combinatorics.quiver.connected_component`: leanprover-community/mathlib4#836
* `combinatorics.quiver.subquiver`: leanprover-community/mathlib4#828



Co-authored-by: Johan Commelin <johan@commelin.net>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

Assignees

No one assigned

Labels

mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@rosborn @ChrisHughes24 @kim-em