Stream: new members
Topic: type class question
Nicolás Ojeda Bär (Oct 12 2019 at 07:13):
Hello! I have some basic mathlib-related questions:
Given a module \beta over a field \alpha where \beta is a ring I want to define the morphism \alpha \to \beta, given by x \mapsto x * 1_\beta.
So I have this:
universes u v variables (α : Type u) (β : Type v) variables [field α] [comm_ring β] [module α β] def struct_hom : α → β := λ x, x • has_one.one β
(some of this may be nonsense!)
maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
I guess the system has trouble disambiguating some of the terms in the lambda definition. How can I supply the necessary constraints ?
Kevin Buzzard (Oct 12 2019 at 07:22):
Hi Nicolas! The problem seems to be here:
import algebra.module universes u v variables (α : Type u) (β : Type v) variables [field α] [comm_ring β] [module α β] example : has_scalar α β := by apply_instance -- max instance depth
Kevin Buzzard (Oct 12 2019 at 07:25):
Whilst I'm not entirely sure why that's happening, I guess that one problem with the way you're setting things up here is that the alpha-module structure on beta will be completely unrelated to the commutative ring structure (so for example you will not even know that the addition on beta-as-alpha-module equals the addition on beta-as-commutative-ring), which is presumably not what you want.
Kevin Buzzard (Oct 12 2019 at 07:26):
There is already a theory of alpha-algebras which solves this problem and you probably want to use that.
Kevin Buzzard (Oct 12 2019 at 07:30):
import ring_theory.algebra universes u v variables (k : Type u) (R : Type v) variables [field k] [comm_ring R] [algebra k R] example : has_scalar k R := by apply_instance def struct_hom : k → R := algebra_map R
Kevin Buzzard (Oct 12 2019 at 07:32):
NB when using mathematical objects I am on a crusade to stay away from this alpha beta etc notation and stick to the notation we're used to; initially this was just mathematicians trying to cause trouble but more recently there have been situations where the computer scientists have seen the value of this convention and my impression is that they're coming round to it.
Nicolás Ojeda Bär (Oct 12 2019 at 07:32):
Indeed, that makes sense. Thanks for pointing out
ring_theory.algebra, I wasn't aware of it.
Nicolás Ojeda Bär (Oct 12 2019 at 07:33):
Ah yes, re the notation I would also prefer to use "traditional" notation but I thought the "house style" was to use greek letters for types. Will switch, thanks!
Kevin Buzzard (Oct 12 2019 at 07:34):
The house style is that, but mathematicians sort-of rebelled against it and because mathematicians infiltrated the mathlib maintainers it started slipping through into the library.
Kevin Buzzard (Oct 12 2019 at 07:35):
I think it's the unique case where mathematicians have suggested a notational change which the CS people could see the merits of. When we started suggesting that they called every lemma something like lemma 13.4 they were adamant that their more expressive system was a much better idea ;-)
Patrick Massot (Oct 12 2019 at 08:29):
Since https://github.com/leanprover-community/mathlib/pull/1521 was merged, this notation victory is official. We should update the style guide though.
Nicolás Ojeda Bär (Oct 12 2019 at 08:46):
Follow-up: trying to write down the definition of algebraic number. I have the following
import ring_theory.algebra universes u v variables (k : Type u) (R : Type v) variables [field k] [ring R] [algebra k R] def is_algebraic (x : R) : Prop := ∃ (p : polynomial k), polynomial.aeval k R x p = has_zero.zero R
I get :
failed to synthesize type class instance for k : Type u, R : Type v, _inst_1 : comm_ring k, _inst_2 : ring R, _inst_3 : algebra k R, x : R, p : polynomial k ⊢ comm_ring R
(the error points to
polynomial.aeval). What is the error saying ?
Patrick Massot (Oct 12 2019 at 08:47):
You declared a ring structure on R, but not a commutative one.
Nicolás Ojeda Bär (Oct 12 2019 at 08:48):
Ah, yes. Thanks!
Kevin Buzzard (Oct 12 2019 at 09:36):
You should demand that p is monic, to stop p=0 from letting everything be algebraic. And all this
has_zero.zero R -- you can just write this as
(0 : R). That's exactly the point of the
has_zero typeclass -- it is a type class written specifically so that we can use
Nicolás Ojeda Bär (Oct 12 2019 at 09:41):
Yes, good point, I was just looking into how best to specify that
p is non-zero. And thanks for the tip on the notation!
Kevin Buzzard (Oct 12 2019 at 09:46):
If you demand it's non-zero then you will often have to apply a lemma saying "if there's a non-zero poly which works then there's a monic poly which works" because we often say "wlog it's monic". On the other hand if you demand it's monic then you won't have to apply this lemma, but if you are trying to prove a specific thing is algebraic and you only manage to find a non-zero poly, you'll have to apply the lemma above. So you have to make a guess about whether you will say "wlog it's monic" more times than being in a situation where you've constructed a non-zero polynomial which is not obviously monic in a proof that something is algebraic, and in my comment I was implicitly guessing that there will be more wlogs.
Kevin Buzzard (Oct 12 2019 at 09:46):
Isn't formalising great ;-)
Kevin Buzzard (Oct 12 2019 at 09:48):
In maths we can just say "TFAE: (a) there's a non-zero poly (b) there's a monic poly. We define _algebraic_ to mean both of them". The advantage with this approach is that whichever one you need, you can just say it's true "by definition" :D In formalising you have to choose one of them to be the definition and then you prove the lemma that it's equivalent to the other one and then only some percentage of things are true "by definition" and the trick if you want to write smaller faster code is to maximise this percentage.
Last updated: May 09 2021 at 19:11 UTC