[Merged by Bors] - feat(category_theory): functorial images #2373

TwoFX · 2020-04-10T06:59:12Z

This is the first in a series of most likely three PRs about the cohomology functor. In this PR, I

add documentation for comma.lean,
introduce the arrow category as a special case of the comma construction, and
introduce the notion of functorial images, which means that commutative squares induce morphisms on images making the obvious diagram commute.

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
reviewed and applied the documentation requirements
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

src/category_theory/comma.lean

src/category_theory/limits/shapes/images.lean

semorrison · 2020-04-11T00:43:05Z

Could you add a paragraph to the module doc for images.lean, explaining the has_image_map typeclass? (Actually, we should document has_image there as well... I seem to have done a bad job of this first time round.)

semorrison · 2020-04-11T01:00:02Z

src/category_theory/limits/shapes/images.lean

+{ map := 𝟙 (image f.hom),
+  factor_map' := by erw [arrow.id_left, category.id_comp, category.comp_id],
+  map_ι' := by erw [arrow.id_right, category.id_comp, category.comp_id] }


Suggested change

{ map := 𝟙 (image f.hom),

factor_map' := by erw [arrow.id_left, category.id_comp, category.comp_id],

map_ι' := by erw [arrow.id_right, category.id_comp, category.comp_id] }

{ map := 𝟙 (image f.hom), }

Both of these proofs actually work by simp, dsimp, simp.

It would be good to understand why we need to drop back to dsimp here. Unfortunately this seems to be frequently necessary when using highly dependent types.

I know that I've written a great many erws in the category_theory library, but most of them are code smells, and we should be suspicious of them.

In this case let's leave the proofs out, as they are boring and tidy can cope just fine.

I haven't been able to fully pin this down, but I think the reason why the dsimp is needed here has something to do with the fact that implicit arguments are in the wrong from: category.id_comp expects that the goal contains 𝟙 X ≫ f with f : X ⟶ Y, but in reality the codomain of f is something like (𝟭 C).obj X (actually, in this particular case there's some auto_param in there too because of how comma is defined, but fixing that doesn't solve the problem) and in non-trivial cases simp and rw category.id_comp cannot make sense of that and rw functor.id_obj produces motive is not type correct, while dsimp only [functor.id_obj] somehow manages to do the right thing.

@gebner provided a very interesting solution to this dsimp, simp problem!

But for now everything is great here.

semorrison · 2020-04-11T01:05:41Z

src/category_theory/limits/shapes/images.lean

+variables {f g : arrow C} [has_image f.hom] [has_image g.hom] (sq : f ⟶ g)
+
+section
+local attribute [ext] has_image_map


Any reason to make this local? It seems a reasonable lemma to have ext be able to use.

Why would you use ext on a subsingleton?

Because then tidy can make easy progress, because it call ext.

It shouldn't call ext. There is no need to: has_image_map sq is a subsingleton, so if we have a goal x = y where x y : has_image_map sq, then tidy will just close the goal with exact dec_trivial. It would be bad if tidy called ext, because then it couldn't automatically solve the goal any more.

tidy will always call dec_trivial before trying ext, so it won't actually fall down this hole.

I guess the thing I hadn't appreciated is that applying this ext attribute creates what is actually a quite poor ext lemma (which gets named has_image_map_ext). Of course, the attribute @[ext] on this lemma disappears by the end of the section, so it's not particularly bad pollution.

I'm now happy to leave as is --- although if you'd prefer to not have the has_image_map_ext declaration be synthesised and left around at all I think that would be reasonable. (Just do the cases ..., congr yourself in the construction of the subsingleton.)

src/category_theory/limits/shapes/images.lean

TwoFX · 2020-04-11T05:03:54Z

Could you add a paragraph to the module doc for images.lean, explaining the has_image_map typeclass? (Actually, we should document has_image there as well... I seem to have done a bad job of this first time round.)

Done!

…lib into arrow_category

semorrison · 2020-04-11T11:46:44Z

bors d+

bors · 2020-04-11T11:46:45Z

✌️ TwoFX 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 · 2020-04-11T22:52:53Z

bors r+

This is the first in a series of most likely three PRs about the cohomology functor. In this PR, I * add documentation for `comma.lean`, * introduce the arrow category as a special case of the comma construction, and * introduce the notion of functorial images, which means that commutative squares induce morphisms on images making the obvious diagram commute.

bors · 2020-04-11T23:58:47Z

Build succeeded

Build mathlib

bors · 2020-04-11T23:58:47Z

Pull request successfully merged into master.

@semorrison

This is the second in a series of most likely three PRs about the cohomology functor. As such, this PR depends on #2373. In the project laid out in `homology.lean`, @semorrison asks what the minimal assumptions are that are needed to get induced maps on images. In this PR, I offer a tautologial answer to this question: We get induced maps on images when there are induced maps on images. In this way, we can let type class resolution answer the question whether cohomology is functorial. In particular, the third PR will contain the fact that if our images are strong epi-mono factorizations, then we get induced maps on images. Since the regular coimage construction in regular categories is a strong epi-mono factorization, the approach in this PR generalizes the previous suggestion of requiring `V` to be regular. A quick remark about cohomology and dependent types: As you can see, at one point Lean forces us to write `i - 1 + 1` instead of `i` because these two things are not definitionally equal. I am afraid, as we do more with cohomology, there will be many cases of this issue, and to compose morphisms whose types contain different incarnations of the same integer, we will have to insert some `eq_to_hom`-esque glue and pray that we will be able to rewrite them all away in the proofs without getting the beloved `motive is not type correct` error. Maybe there is some better way to solve this problem? (Or am I overthinking this and it is not actually going to be an issue at all?)

@semorrison

This is the second in a series of most likely three PRs about the cohomology functor. As such, this PR depends on #2373. In the project laid out in `homology.lean`, @semorrison asks what the minimal assumptions are that are needed to get induced maps on images. In this PR, I offer a tautologial answer to this question: We get induced maps on images when there are induced maps on images. In this way, we can let type class resolution answer the question whether cohomology is functorial. In particular, the third PR will contain the fact that if our images are strong epi-mono factorizations, then we get induced maps on images. Since the regular coimage construction in regular categories is a strong epi-mono factorization, the approach in this PR generalizes the previous suggestion of requiring `V` to be regular. A quick remark about cohomology and dependent types: As you can see, at one point Lean forces us to write `i - 1 + 1` instead of `i` because these two things are not definitionally equal. I am afraid, as we do more with cohomology, there will be many cases of this issue, and to compose morphisms whose types contain different incarnations of the same integer, we will have to insert some `eq_to_hom`-esque glue and pray that we will be able to rewrite them all away in the proofs without getting the beloved `motive is not type correct` error. Maybe there is some better way to solve this problem? (Or am I overthinking this and it is not actually going to be an issue at all?)

This is the first in a series of most likely three PRs about the cohomology functor. In this PR, I * add documentation for `comma.lean`, * introduce the arrow category as a special case of the comma construction, and * introduce the notion of functorial images, which means that commutative squares induce morphisms on images making the obvious diagram commute.

@semorrison

…2374) This is the second in a series of most likely three PRs about the cohomology functor. As such, this PR depends on leanprover-community#2373. In the project laid out in `homology.lean`, @semorrison asks what the minimal assumptions are that are needed to get induced maps on images. In this PR, I offer a tautologial answer to this question: We get induced maps on images when there are induced maps on images. In this way, we can let type class resolution answer the question whether cohomology is functorial. In particular, the third PR will contain the fact that if our images are strong epi-mono factorizations, then we get induced maps on images. Since the regular coimage construction in regular categories is a strong epi-mono factorization, the approach in this PR generalizes the previous suggestion of requiring `V` to be regular. A quick remark about cohomology and dependent types: As you can see, at one point Lean forces us to write `i - 1 + 1` instead of `i` because these two things are not definitionally equal. I am afraid, as we do more with cohomology, there will be many cases of this issue, and to compose morphisms whose types contain different incarnations of the same integer, we will have to insert some `eq_to_hom`-esque glue and pray that we will be able to rewrite them all away in the proofs without getting the beloved `motive is not type correct` error. Maybe there is some better way to solve this problem? (Or am I overthinking this and it is not actually going to be an issue at all?)

This is the first in a series of most likely three PRs about the cohomology functor. In this PR, I * add documentation for `comma.lean`, * introduce the arrow category as a special case of the comma construction, and * introduce the notion of functorial images, which means that commutative squares induce morphisms on images making the obvious diagram commute.

@semorrison

…2374) This is the second in a series of most likely three PRs about the cohomology functor. As such, this PR depends on leanprover-community#2373. In the project laid out in `homology.lean`, @semorrison asks what the minimal assumptions are that are needed to get induced maps on images. In this PR, I offer a tautologial answer to this question: We get induced maps on images when there are induced maps on images. In this way, we can let type class resolution answer the question whether cohomology is functorial. In particular, the third PR will contain the fact that if our images are strong epi-mono factorizations, then we get induced maps on images. Since the regular coimage construction in regular categories is a strong epi-mono factorization, the approach in this PR generalizes the previous suggestion of requiring `V` to be regular. A quick remark about cohomology and dependent types: As you can see, at one point Lean forces us to write `i - 1 + 1` instead of `i` because these two things are not definitionally equal. I am afraid, as we do more with cohomology, there will be many cases of this issue, and to compose morphisms whose types contain different incarnations of the same integer, we will have to insert some `eq_to_hom`-esque glue and pray that we will be able to rewrite them all away in the proofs without getting the beloved `motive is not type correct` error. Maybe there is some better way to solve this problem? (Or am I overthinking this and it is not actually going to be an issue at all?)

This is the first in a series of most likely three PRs about the cohomology functor. In this PR, I * add documentation for `comma.lean`, * introduce the arrow category as a special case of the comma construction, and * introduce the notion of functorial images, which means that commutative squares induce morphisms on images making the obvious diagram commute.

@semorrison

…2374) This is the second in a series of most likely three PRs about the cohomology functor. As such, this PR depends on leanprover-community#2373. In the project laid out in `homology.lean`, @semorrison asks what the minimal assumptions are that are needed to get induced maps on images. In this PR, I offer a tautologial answer to this question: We get induced maps on images when there are induced maps on images. In this way, we can let type class resolution answer the question whether cohomology is functorial. In particular, the third PR will contain the fact that if our images are strong epi-mono factorizations, then we get induced maps on images. Since the regular coimage construction in regular categories is a strong epi-mono factorization, the approach in this PR generalizes the previous suggestion of requiring `V` to be regular. A quick remark about cohomology and dependent types: As you can see, at one point Lean forces us to write `i - 1 + 1` instead of `i` because these two things are not definitionally equal. I am afraid, as we do more with cohomology, there will be many cases of this issue, and to compose morphisms whose types contain different incarnations of the same integer, we will have to insert some `eq_to_hom`-esque glue and pray that we will be able to rewrite them all away in the proofs without getting the beloved `motive is not type correct` error. Maybe there is some better way to solve this problem? (Or am I overthinking this and it is not actually going to be an issue at all?)

TwoFX added 5 commits April 8, 2020 18:09

Docstrings for comma categories

40147dd

WIP

10788d5

A simp lemma is not firing :(

6e57682

feat(category_theory): functorial images

66e34e3

Minor

3247ae1

TwoFX added the awaiting-review The author would like community review of the PR label Apr 10, 2020

TwoFX added this to In progress in Homological algebra via automation Apr 10, 2020

TwoFX mentioned this pull request Apr 10, 2020

[Merged by Bors] - feat(algebra/homology): the cohomology functor #2374

Closed

4 tasks

jcommelin reviewed Apr 10, 2020

View reviewed changes

semorrison reviewed Apr 10, 2020

View reviewed changes

src/category_theory/limits/shapes/images.lean Outdated Show resolved Hide resolved

Apply suggestions from code review

5c7ed4d

jcommelin requested a review from semorrison April 10, 2020 13:38

add missing simp lemmas for comma

5aa9ba3

semorrison reviewed Apr 11, 2020

View reviewed changes

cleaning up a different proof

c4530ce

semorrison reviewed Apr 11, 2020

View reviewed changes

src/category_theory/limits/shapes/images.lean Show resolved Hide resolved

Apply more suggestions from code review

072f377

Scott Morrison added 2 commits April 11, 2020 19:22

Merge branch 'arrow_category' of github.com:leanprover-community/math…

e6bfb46

…lib into arrow_category

cleanup a different proof in the same file

16e1bc7

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 Apr 11, 2020

bors bot changed the title ~~feat(category_theory): functorial images~~ [Merged by Bors] - feat(category_theory): functorial images Apr 11, 2020

bors bot closed this Apr 11, 2020

bryangingechen deleted the arrow_category branch April 14, 2020 06:00

TwoFX moved this from In progress to Done in Homological algebra Apr 14, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(category_theory): functorial images #2373

[Merged by Bors] - feat(category_theory): functorial images #2373

TwoFX commented Apr 10, 2020

semorrison commented Apr 11, 2020

semorrison Apr 11, 2020

TwoFX Apr 11, 2020

semorrison Apr 11, 2020

semorrison Apr 11, 2020

TwoFX Apr 11, 2020

jcommelin Apr 11, 2020

TwoFX Apr 11, 2020 •

edited

semorrison Apr 11, 2020

TwoFX commented Apr 11, 2020

semorrison commented Apr 11, 2020

bors bot commented Apr 11, 2020

semorrison commented Apr 11, 2020

bors bot commented Apr 11, 2020

bors bot commented Apr 11, 2020

[Merged by Bors] - feat(category_theory): functorial images #2373

[Merged by Bors] - feat(category_theory): functorial images #2373

Conversation

TwoFX commented Apr 10, 2020

semorrison commented Apr 11, 2020

semorrison Apr 11, 2020

Choose a reason for hiding this comment

TwoFX Apr 11, 2020

Choose a reason for hiding this comment

semorrison Apr 11, 2020

Choose a reason for hiding this comment

semorrison Apr 11, 2020

Choose a reason for hiding this comment

TwoFX Apr 11, 2020

Choose a reason for hiding this comment

jcommelin Apr 11, 2020

Choose a reason for hiding this comment

TwoFX Apr 11, 2020 • edited

Choose a reason for hiding this comment

semorrison Apr 11, 2020

Choose a reason for hiding this comment

TwoFX commented Apr 11, 2020

semorrison commented Apr 11, 2020

bors bot commented Apr 11, 2020

semorrison commented Apr 11, 2020

bors bot commented Apr 11, 2020

Build succeeded

bors bot commented Apr 11, 2020

Pull request successfully merged into master.

TwoFX Apr 11, 2020 •

edited