# Zulip Chat Archive

## Stream: new members

### Topic: ring morphism from Z

#### orlando (Mar 22 2020 at 20:44):

Hello,

If $R$ is a commutatif ring, there exists an unique morphisme $f : \mathbb{Z} \to R$, how show this fact in lean ?

#### orlando (Mar 22 2020 at 20:44):

perhaps this is already done !

#### Patrick Massot (Mar 22 2020 at 20:57):

It's called `int.cast`

.

#### orlando (Mar 22 2020 at 21:00):

oh nice, there is a theorem " eq_cast " i thinck it's ok ! Thx !

#### orlando (Mar 22 2020 at 22:17):

Yeaaaaaaaaaaaah !!! :grinning_face_with_smiling_eyes:

import algebra.category.CommRing.basic import algebra.ring import tactic import data.polynomial import algebra.ring import category_theory.types import data.int.basic universes v u open CommRing open is_ring_hom open polynomial open int variables(R : Type)[comm_ring R](P : polynomial ℤ) structure V (R: Type)[comm_ring R] := -- set of solution of P(x) = 0 with x in R (x : R) -- if φ : R → R' is a ring morphism then we have application (certif : eval₂(int.cast) (x) (P) = 0 ) -- φ : V(P)(R) → V(P(R') lemma ext : ∀ {ζ1 ζ2 : V P R}, ζ1.x = ζ2.x → ζ1 = ζ2 := λ ζ1 ζ2, begin cases ζ1, cases ζ2, intro h, congr ; try { assumption }, end definition map_V (R : Type) [comm_ring R] (R' : Type)[comm_ring R'] (f : R → R') [is_ring_hom f] : (V P R) → (V P R') := λ ζ,begin exact {x := f ζ.x, certif := begin have H : eval₂ (f ∘ int.cast) (f ζ.x) P = f (eval₂ int.cast (ζ.x) P), rw ← hom_eval₂ P int.cast f ζ.x, have G : f ∘ int.cast = int.cast, exact (int.eq_cast') (f ∘ int.cast), rw G at H, rw H, have cer : eval₂ int.cast ζ.x P =0, exact ζ.certif, rw cer, exact map_zero f, end} end

#### Kevin Buzzard (Mar 22 2020 at 22:23):

When I had just started Lean, `polynomial`

wasn't there! I had to get an undergraduate to make it ;-)

#### orlando (Mar 22 2020 at 22:29):

Kevin, it's very hard to use : $eval_2 (int.cast) (x) (P)$ , for us it's just $P(x) = 0$ with $x \in R$ !!!

#### Kevin Buzzard (Mar 22 2020 at 22:40):

This is called "learning the interface". The most important thing to understand is: "if it is a standard fact, it will be there".

#### Kevin Buzzard (Mar 22 2020 at 22:42):

I wanted to learn the interface for polynomials in more than one variable recently, because I was formalising basic algebraic geometry (I just finished teaching an undergraduate alg geom course at my university). So I read data.mv_polynomial and then I wrote the docstring which you can see in the first 90 lines. I didn't do that for `polynomial.lean`

yet so it was probably harder work for you to find the theorems.

#### Kevin Buzzard (Mar 22 2020 at 22:46):

I agree that formalising is much harder work than mathematics on paper. The idea is that if we make a really good interface then it will not be so painful. I would imagine that there is already a coercion from $\mathbb{Z}$ to $R$ but I don't think that there is a rule that says that if there is a coercion from $A$ to $B$ then there is also a coercion from $A[X]$ to $B[X]$. If this was added then it might make the code look nicer, but then a computer scientist might come along and say that this is a bad coercion because of some computer science reason involving type class search.

#### Kevin Buzzard (Mar 22 2020 at 22:47):

import data.polynomial example (R : Type) [comm_ring R] (n : ℤ) : R := n

This works, so integers can be regarded as elements of a commutative ring. If you look at what happened, it actually defined the term to be `↑n`

#### Kevin Buzzard (Mar 22 2020 at 22:48):

`example (R : Type*) [comm_ring R] (p : polynomial ℤ) : polynomial R := p`

-- this fails, and so does `:= ↑p`

#### Kevin Buzzard (Mar 22 2020 at 22:51):

noncomputable instance (R : Type*) [comm_ring R] : has_coe (polynomial ℤ) (polynomial R) := ⟨polynomial.map (coe : ℤ → R)⟩

#### Kevin Buzzard (Mar 22 2020 at 22:54):

import data.polynomial noncomputable theory example (R : Type) [comm_ring R] (n : ℤ) : R := ↑n instance foo (R : Type*) [comm_ring R] : has_lift_t ℤ R := by apply_instance instance (R : Type*) [comm_ring R] : has_coe (polynomial ℤ) (polynomial R) := ⟨polynomial.map (coe : ℤ → R)⟩ open polynomial example (R : Type*) [comm_ring R] (p : polynomial ℤ) (r : R) : R := eval r p

There -- now it is just `eval`

and you could set up notation for `eval`

so that it becomes some kind of `p(r)`

, although probably you would have to use some funky brackets

#### orlando (Mar 22 2020 at 22:54):

Yes i use 'map'

example (R : Type*) [comm_ring R] (p : polynomial ℤ) : polynomial R := map (int.cast) p

But non computable (i don't know if it's a problem ?)

#### Kevin Buzzard (Mar 22 2020 at 22:55):

It's not a problem

#### Kevin Buzzard (Mar 22 2020 at 22:55):

It's a problem for some people, but not for mathematicians

#### Kevin Buzzard (Mar 22 2020 at 22:56):

It's probably something to do with the fact that you can't tell if a coefficient is zero or not if there is no algorithm for deciding equality between two elements of R or something.

#### Kevin Buzzard (Mar 22 2020 at 22:57):

For example there is no algorithm which tells you if two real numbers are equal: you cannot just tell a computer to prove $\sum_{n\geq1}1/n^2=\pi^2/6$. All it can do is to check it to 10000 decimal places

#### Kevin Buzzard (Mar 22 2020 at 22:58):

And because you don't care about this, you don't care that your example is noncomputable

#### orlando (Mar 22 2020 at 22:58):

okay !

#### Kevin Buzzard (Mar 22 2020 at 22:58):

notation p `(` r `)` := eval r p example (R : Type*) [comm_ring R] (p : polynomial ℤ) (r : R) : R := p(r)

#### Kevin Buzzard (Mar 22 2020 at 23:00):

I suspect that this is really bad notation for all sorts of reasons :-)

#### Kevin Buzzard (Mar 22 2020 at 23:01):

but what I am showing you is that if you don't like the interface then there are always possibilities to make it better, either by adding more theorems or adding more notation.

#### Kevin Buzzard (Mar 22 2020 at 23:02):

orlando said:

Yes i use 'map'

I used `map`

too, but I buried it in ```
instance (R : Type*) [comm_ring R] : has_coe (polynomial ℤ) (polynomial R) :=
⟨polynomial.map (coe : ℤ → R)⟩
```

#### Kevin Buzzard (Mar 22 2020 at 23:04):

and also

variables (R : Type*) [comm_ring R] example : (coe : ℤ → R) = (int.cast : ℤ → R) := rfl

I used a map which was the same as yours by definition (not just a theorem that they are the same, they are the same by definition). So our definitions of evaluation are the same.

#### Kevin Buzzard (Mar 22 2020 at 23:05):

`example : (λ n, ↑n : ℤ → R) = (int.cast : ℤ → R) := rfl`

#### Kevin Buzzard (Mar 22 2020 at 23:08):

When you are in this situation, when there are several ways of saying the exact same thing, you have to decide on a "canonical" way! I believe that the canonical way is `↑n`

here (which is just notation for `coe`

). What do I mean by this? I mean that when you prove 100 lemmas about this map, you have to decide exactly how to phrase them (for example you want to prove that this map $\mathbb{Z}\to R$ sends products to products, and you have to decide how to say this). The rule is that you state everything using the canonical notation, and then you teach the simplifier all the theorems expressed using the canonical notation, and then the simplifier hopefully works well.

#### Kevin Buzzard (Mar 22 2020 at 23:11):

You can see in `data.int.basic`

straight after the definition of `int.cast`

they define the coercion:

/-- Canonical homomorphism from the integers to any ring(-like) structure `α` -/ protected def cast : ℤ → α | (n : ℕ) := n | -[1+ n] := -(n+1) @[priority 10] instance cast_coe : has_coe ℤ α := ⟨int.cast⟩

and if you import data.int.basic and do stuff like `#check int.cast_one`

or `#check int.cast_add`

, all these results are stated using `↑`

notation.

#### Kevin Buzzard (Mar 22 2020 at 23:12):

and if you do things like `#print int.cast_add`

you can see they are all tagged with `simp`

. This is how the simplifier learns to use this stuff. But it means that it's important to stick with the canonical choice if you want to maximise your use of the simplifier.

Last updated: May 08 2021 at 09:11 UTC