ring morphism from Z

Stream: new members

[orlando]

Hello,

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

[orlando]

perhaps this is already done !

[Patrick Massot]

It's called int.cast.

[orlando]

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

[orlando]

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]

When I had just started Lean, polynomial wasn't there! I had to get an undergraduate to make it ;-)

[orlando]

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]

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]

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]

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]

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]

example (R : Type*) [comm_ring R] (p : polynomial ℤ) : polynomial R := p -- this fails, and so does := ↑p

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

It's not a problem

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[orlando]

okay !

[Kevin Buzzard]

notation p `(` r `)` := eval r p

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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.