type class question

Stream: new members

[Nicolás Ojeda Bär]

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!)
I get:

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 ?
Thanks!

[Kevin Buzzard]

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]

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]

There is already a theory of alpha-algebras which solves this problem and you probably want to use that.

[Kevin Buzzard]

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]

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]

Indeed, that makes sense. Thanks for pointing out ring_theory.algebra, I wasn't aware of it.

[Nicolás Ojeda Bär]

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]

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]

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]

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]

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]

You declared a ring structure on R, but not a commutative one.

[Nicolás Ojeda Bär]

Ah, yes. Thanks!

[Kevin Buzzard]

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 0 notation.

[Nicolás Ojeda Bär]

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]

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]

Isn't formalising great ;-)

[Kevin Buzzard]

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.