Zulip Chat Archive

Stream: new members

Topic: local notations/definitions


Jon Eugster (May 20 2021 at 10:42):

After defining some variables like variables (R: Type*) [integral_domain R] I would quite often make local definitions like "let KK be the field of fractions of RR". 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 (May 20 2021 at 10:54):

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 (May 20 2021 at 10:54):

@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 (May 20 2021 at 10:54):

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

Johan Commelin (May 20 2021 at 10:55):

Because rat is not defined to be fraction_ring int.

Johan Commelin (May 20 2021 at 10:55):

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

Jon Eugster (May 20 2021 at 10:59):

Johan Commelin said:

The problem is that if you use the literal fraction_ring R, then you can not apply your theorems to Z\Z and Q\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 (May 20 2021 at 11:01):

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 (May 20 2021 at 11:03):

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 (May 20 2021 at 11:03):

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 (May 20 2021 at 11:04):

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

Johan Commelin (May 20 2021 at 11:04):

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

Johan Commelin (May 20 2021 at 11:04):

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

Anne Baanen (May 20 2021 at 11:05):

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\Z and Q\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 (May 20 2021 at 11:06):

(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 (May 20 2021 at 11:08):

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 (May 20 2021 at 11:23):

nvm

Jon Eugster (May 20 2021 at 11:26):

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 Frac(R)\operatorname{Frac}(R) everywhere to make it more look like a mathematical proof?

Johan Commelin (May 20 2021 at 11:28):

localization_map is a type of function.

Johan Commelin (May 20 2021 at 11:28):

Specifically the functions from R to a localisation of R.

Johan Commelin (May 20 2021 at 11:30):

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."


Last updated: Dec 20 2023 at 11:08 UTC