refactor(*): bundle is_field_hom #717
Conversation
| @@ -96,13 +96,19 @@ noncomputable instance field : discrete_field (adjoin_root f) := | |||
| ..adjoin_root.comm_ring f, | |||
| ..ideal.quotient.field (span {f} : ideal (polynomial α)) } | |||
|
|
|||
| instance : is_field_hom (coe : α → adjoin_root f) := by apply_instance | |||
| variables (α f) | |||
| def fof : α →f adjoin_root f := | |||
There was a problem hiding this comment.
I understand the f-prefix. Yet, intuitively I would just call this of.
|
|
||
| instance lift_is_field_hom [field β] {i : α → β} [is_ring_hom i] {a : β} | ||
| {h : f.eval₂ i a = 0} : is_field_hom (lift i a h) := by apply_instance | ||
| def flift [field β] (i : α → β) [is_ring_hom i] (a : β) |
There was a problem hiding this comment.
There's already lift.
|
No point making field hom and ring hom separate, especially if they're bundled. field hom should probably be reducibly defined to be ring hom. |
|
I agree, but I intend to test bundling on field homs only. If the consensus approves for bundling of ring homs, then field hom would be defined to be ring hom (or even semiring hom). |
|
So, what do we do with this experiment? @digama0 seemed to be in favour of bundling. What do others think? Do we need extended discussion? @ChrisHughes24 @kckennylau @rwbarton @avigad @semorrison |
|
My main concern with this is that we end up having to do type class inference by hand, if we want a field hom to be a group hom or whatever. I'm not sure how much of a problem this is going to be. The main upside is that the |
|
Chris' comment suggests it's worth expanding the experiment a step further
before merging: bundle both is_field_hom and is_group_hom, so we can
evaluate how much a problem it is moving between them..
…On Thu, Feb 28, 2019 at 1:54 AM Chris Hughes ***@***.***> wrote:
My main concern with this is that we end up having to do type class
inference by hand, if we want a field hom to be a group hom or whatever.
I'm not sure how much of a problem this is going to be. The main upside is
that the simp attributes work. I'd love to get unification hints to solve
this problem, but I couldn't get it to work.
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#717 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AAdLBGZuip-rE6uAkN38oRFSwV9hwdQzks5vRpwZgaJpZM4a3tzY>
.
|
|
Should we close this PR? There is no intention to merge this, because it is mostly an experiment. Scott indicates that there should be more experimenting before we know is we want bundled homs in the algebraic hierarchy. I don't think anyone is actively working on the experiment currently. We can always reopen this PR if someone returns to this experiment. |
|
I'm going to close this one for now. We can reopen once we get back to the idea of bundling morphisms. |
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list