[Merged by Bors] - feat(category_theory/functor_category): monos in the functor category - #4811
[Merged by Bors] - feat(category_theory/functor_category): monos in the functor category#4811b-mehta wants to merge 1 commit into
Conversation
b-mehta
commented
Oct 28, 2020
b-mehta
commented
b-mehta
added
awaiting-review
| congr_fun (congr_arg app (T.naturality f)) Z | ||
|
|
||
| /-- A natural transformation is a monomorphism if each component is. -/ | ||
| lemma mono_app_of_mono (α : F ⟶ G) [∀ (X : C), mono (α.app X)] : mono α := |
There was a problem hiding this comment.
Do you want the [..]? I guess that typeclass inference will not be able to find those instances. Probably there would first need to be a dsimp that unfolds the app into something for which an instance exists.
And with the [..], applying the lemma will fail if it can find the instance. So it might be better to use (..) and then call apply_instance in those cases where find the instance is actually possible.
There was a problem hiding this comment.
This is a fair point - I was mimicking what's done in natural_isomorphism.lean, where it has
def is_iso_of_is_iso_app (α : F ⟶ G) [∀ X : C, is_iso (α.app X)] : is_iso α :=
so I thought this version should be okay - I don't mind changing though
There was a problem hiding this comment.
Ooh well, if it's also done over there, let's try this. If it doesn't work, it's easy enough to change.
|
Thanks 🎉 bors merge |
github-actions
Bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
Bot
changed the title
2 participants
