## 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

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