local notations/definitions

Stream: new members

[Jon Eugster]

After defining some variables like variables (R: Type*) [integral_domain R] I would quite often make local definitions like "let $K$ be the field of fractions of $R$". I use local notation `K` := fraction_ring R for this.

Is that the correct way or is there a better way to do it? (to be clear, writing K should literally behave like writing fraction_ring R, and just make the statement more readable.)

Moreover, is there a way to fix a notation during a theorem statement, like example {R: Type*} [ring R] (**denote K := fraction_ring R**) (p: polynomial K) ... : ... := sorry

[Eric Wieser]

Moreover, is there a way to fix a notation during a theorem statement

This is legal:

example {R : Type*} [semiring R] : let notation `two` := (2 : R) in two + two = 4 := rfl

[Johan Commelin]

@Jon Eugster The recommended way is to write something like

variables (R K : Type*) [integral_domain R] [field K] (f : localization_map (non_zero_divisors R) K)

[Johan Commelin]

The problem is that if you use the literal fraction_ring R, then you can not apply your theorems to $\Z$ and $\mathbb Q$.

[Johan Commelin]

Because rat is not defined to be fraction_ring int.

[Johan Commelin]

Similarly $\mathbb Q_p$ is not defined to be the fraction_ring of $\Z_p$.

[Jon Eugster]

Johan Commelin said:

The problem is that if you use the literal fraction_ring R, then you can not apply your theorems to $\Z$ and $\mathbb Q$.

Oh that's interesting. So do you think there should be eventually a lemma saying ℚ ≅ₐ fraction_ring ℤ or is there a fundamental problem that would prevent that from working?

[Anne Baanen]

Johan Commelin said:

Jon Eugster The recommended way is to write something like

variables (R K : Type*) [integral_domain R] [field K] (f : localization_map (non_zero_divisors R) K)

For a slight bit of conciseness, you can also write docs#fraction_map instead of localization_map (non_zero_divisors R)

[Jon Eugster]

Anne Baanen said:

Johan Commelin said:

Jon Eugster The recommended way is to write something like

variables (R K : Type*) [integral_domain R] [field K] (f : localization_map (non_zero_divisors R) K)

For a slight bit of conciseness, you can also write docs#fraction_map instead of localization_map (non_zero_divisors R)

So I take it that fraction_map and fraction_ring are not fully compatible at the moment?

[Johan Commelin]

Jon Eugster said:

So do you think there should be eventually a lemma saying ℚ ≅ₐ fraction_ring ℤ or is there a fundamental problem that would prevent that from working?

No, that can certainly work. But it means you would need to invoke that all the time. And show that what every you proved about fraction_ring is invariant under ring isomorphisms. (Which is always trivial on paper, but not in Lean.

[Johan Commelin]

If you use fraction_map then you can apply it to fraction_ring.

[Johan Commelin]

fraction_ring is an explicit construction of a ring that satisfies the conditions for fraction_map.

[Johan Commelin]

But the library also contains the facts that $\mathbb Q$ satisfies this when $R = \Z$, etc...

[Anne Baanen]

Jon Eugster said:

Johan Commelin said:

The problem is that if you use the literal fraction_ring R, then you can not apply your theorems to $\Z$ and $\mathbb Q$.

Oh that's interesting. So do you think there should be eventually a lemma saying ℚ ≅ₐ fraction_ring ℤ or is there a fundamental problem that would prevent that from working?

This is almost, but not quite due to technical issues, docs#fraction_ring.alg_equiv_of_quotient:

example : fraction_ring ℤ ≃ₐ[ℤ] ℚ :=
fraction_ring.alg_equiv_of_quotient fraction_map.int.fraction_map

But you get an error that ℚ doesn't have the same algebra ℤ structure as fraction_map.int.fraction_map.codomain

[Anne Baanen]

(I have the solution to that technical issue, to assume an algebra R K instance in localization_map, but haven't gotten around to implementing it.)

[Anne Baanen]

Fun fact: convert is smart enough to fix the coherence issue:

noncomputable example : fraction_ring ℤ ≃ₐ[ℤ] ℚ :=
by convert fraction_ring.alg_equiv_of_quotient fraction_map.int.fraction_map -- Works!

[Jon Eugster]

nvm

[Jon Eugster]

Would it be terrible to make a definition like

def Frac (R: Type*) [integral_domain R] := localization_map (non_zero_divisors R)

so I could just work with $\operatorname{Frac}(R)$ everywhere to make it more look like a mathematical proof?

[Johan Commelin]

localization_map is a type of function.

[Johan Commelin]

Specifically the functions from R to a localisation of R.

[Johan Commelin]

You should read

variables (R K : Type*) [integral_domain R] [field K] (f : fraction_map R K)

as "let R be an integral domain, and K a field that is the fraction field of R. Additionally, let f be the ring hom R -> K."