# Zulip Chat Archive

## Stream: new members

### Topic: Integrally closed domain

#### Barinder Singh Banwait (May 25 2020 at 18:26):

Hello Lean community! This is my first ever post here, and I'm a lean beginner. As a toy starting out project I'm trying to add the definition of what it means for an integral domain to be integrally closed, using `def integral_closure`

from integral_closure.lean. Apologies if it's already there - I'm still learning the syntax, so might have overlooked it - but I'm trying something like the following added to integral_closure.lean:

```
import ring_theory.localization
...
@[class] def is_integrally_closed (R) [integral_domain R] : Prop :=
integral_closure R (localization.fraction_ring R) = R
```

However, the Lean goal pane complains of Type mismatch, because "integral_closure R (localization.fraction_ring R)" has type "subalgebra R _", and it's being compared to type integral_domain.

What's the optimal way of resolving this? I thought of trying to get the underlying rings, and comparing those, but I wonder if there's a better way.

#### Johan Commelin (May 25 2020 at 18:37):

@Barinder Singh Banwait Hi, and welcome!

#### Johan Commelin (May 25 2020 at 18:38):

Mathematically, what you are doing is totally fine. (Of course!) However, in type theory, you need to strictly separated "ambient sets" and "subsets of an ambient set"

#### Johan Commelin (May 25 2020 at 18:38):

This is usually very close to our mathematical intuition. But sometimes it's annoying.

#### Johan Commelin (May 25 2020 at 18:39):

In your specific example, you introduce `R`

by saying `(R)`

in the statement, which is short for saying that `R`

is a "type", in other words, an "ambient set". Roughly speaking, this means that you will never compare `R`

directly to anything else.

#### Johan Commelin (May 25 2020 at 18:40):

(It is totally fine to say that it is *isomorphic* to something else, but not *equal*.)

#### Johan Commelin (May 25 2020 at 18:40):

So, long story short, you want to say that the `integral_closure R (blabla)`

is *equal* to the image of `R`

inside the localisation.

#### Barinder Singh Banwait (May 25 2020 at 18:42):

Hi Johan, thanks for the welcome!

#### Barinder Singh Banwait (May 25 2020 at 18:42):

Oh, I didn't know that putting `()`

around the R changes its meaning; i copied that from the definition of `is_noetherian_ring`

in noetherian.lean:

```
@[class] def is_noetherian_ring (R) [ring R] : Prop := is_noetherian R R
```

#### Johan Commelin (May 25 2020 at 18:43):

Barinder Singh Banwait said:

Oh, I didn't know that putting

`()`

around the R changes its meaning

It doesn't really... but you need an ambient set to start with

#### Kevin Buzzard (May 25 2020 at 18:43):

Hey Barinder. Did you see p3 of my Birmingham talk? Let that be a warning to you.

#### Johan Commelin (May 25 2020 at 18:43):

And the `(R)`

is really just shorthand for `(R : Type*)`

.

#### Barinder Singh Banwait (May 25 2020 at 18:44):

Kevin Buzzard said:

Hey Barinder. Did you see p3 of my Birmingham talk? Let that be a warning to you.

Hi Kevin! No I didn't see that talk, I'll take a look!

#### Alex J. Best (May 25 2020 at 18:45):

Kevin Buzzard said:

Hey Barinder. Did you see p3 of my Birmingham talk? Let that be a warning to you.

What's the warning? One might give up Zelda?

#### Kevin Buzzard (May 25 2020 at 18:45):

Barinder and I have talked Zelda in the past

#### Barinder Singh Banwait (May 25 2020 at 18:46):

Johan Commelin said:

And the

`(R)`

is really just shorthand for`(R : Type*)`

.

aah yes, that makes more sense now!

#### Johan Commelin (May 25 2020 at 18:48):

Yeah, we shouldn't use those abbreviations.... but hey, sometimes people are bored, and want to get the job done quickly

#### Barinder Singh Banwait (May 25 2020 at 18:51):

Johan Commelin said:

So, long story short, you want to say that the

`integral_closure R (blabla)`

isequalto the image of`R`

inside the localisation.

ok, so hopefully there is already defined somewhere a map from an integral domain into its fraction field? quickly looking through localization.lean, it looks like there is `coe : α → localization α S`

, which looks promising

#### Johan Commelin (May 25 2020 at 18:51):

Note that this file was thoroughly rewritten a few days ago

#### Johan Commelin (May 25 2020 at 18:51):

Do you have the latest version?

#### Barinder Singh Banwait (May 25 2020 at 18:53):

Johan Commelin said:

Do you have the latest version?

oh, i'm not sure ... i created the project a few days ago, and given how quickly mathlib moves, i almost certainly don't have the latest version; but i won't be far off

#### Kevin Buzzard (May 25 2020 at 18:53):

You should be able to type `leanproject up`

in your project

#### Johan Commelin (May 25 2020 at 18:55):

Hmmz... it seems that `fraction_ring`

got lost in the battle

#### Johan Commelin (May 25 2020 at 18:55):

There is now something called `fraction_map`

, which should serve the same purpose

#### Johan Commelin (May 25 2020 at 18:56):

Except that it is the map, and not the "ambient set" of the codomain.

#### Barinder Singh Banwait (May 25 2020 at 18:56):

Kevin Buzzard said:

You should be able to type

`leanproject up`

in your project

just done, thanks! and indeed Johan, i can't find `fraction_ring`

anymore

#### Johan Commelin (May 25 2020 at 18:58):

In the end, this upgrade should pay off. (It solves exactly the issue with localisations that Kevin describes on page 10 (or so) of the pdf he linked above)

#### Johan Commelin (May 25 2020 at 18:59):

Namely: `R[1/f][1/g] ≠ R[1/fg]`

... they are only isomorphic, not equal. Same issue that you ran into with your first post.

#### Johan Commelin (May 25 2020 at 18:59):

(The `≠`

is abuse of notation)

#### Barinder Singh Banwait (May 25 2020 at 19:07):

oh wow, yeah i can see it's been majorly rewritten; seems a lot more functorial now

#### Barinder Singh Banwait (May 25 2020 at 19:37):

so i've now tried, in `integral_closure.lean`

:

```
variables (K: Type u)
variables [comm_ring K]
@[class] def is_integrally_closed (R) [integral_domain R] : Prop :=
integral_closure R (localization.to_integral_domain [comm_ring K]
(φ : localization.fraction_map R K)) = localization.fraction_map R K R
```

I'm sure there are problems with the syntax there; but perhaps more importantly, Lean Goal isn't finding `localization.fraction_map`

or `localization.to_integral_domain`

; do those labels of `protected`

and `local attribute`

used in `localization.lean`

mean that these definitions are not to be used outside of this file?

#### Alex J. Best (May 25 2020 at 19:42):

to_integral_domain is in the fraction_map namespace

#### Alex J. Best (May 25 2020 at 19:43):

As for the syntax, the square brackets are used to declare that an argument is a typeclass, and will be inferred automatically by lean, so when you call a function which has these for arguments you don't need to supply them explicitly, so [comm_ring K] after the := won't work.

#### Barinder Singh Banwait (May 25 2020 at 19:45):

Alex J. Best said:

As for the syntax, the square brackets are used to declare that an argument is a typeclass, and will be inferred automatically by lean, so when you call a function which has these for arguments you don't need to supply them explicitly, so [comm_ring K] after the := won't work.

ok thanks, so that's just fixed by replacing `[comm_ring K]`

by `K`

?

#### Alex J. Best (May 25 2020 at 19:47):

You should remove it completely I think, the signature is

```
fraction_map.to_integral_domain : Π {K : Type u_4} {A : Type u_5} [_inst_4 : integral_domain A] [_inst_5 : comm_ring K], fraction_map A K → integral_domain K
```

so there is only one argument you need to supply as the others are surrounded by {} or [] lean will work them out from the fraction_map A K you give it.

#### Kevin Buzzard (May 25 2020 at 19:47):

By "in `integral_closure.lean`

", I hope you mean "I made a new file which starts with the line `import ring_theory.integral_closure`

" rather than "I am editing a library file".

#### Kevin Buzzard (May 25 2020 at 19:48):

Also, the error messages look quite intimidating at first, but they really tell you what's going on

#### Barinder Singh Banwait (May 25 2020 at 19:48):

Alex J. Best said:

to_integral_domain is in the fraction_map namespace

apologies, i'm very new to Lean and namespaces: is it the case that those definitions within the `namespace fraction_map`

are not accessible to other lean files?

#### Kevin Buzzard (May 25 2020 at 19:49):

Definitions like `blah`

in that namespace are all called `fraction_map.blah`

outside it

#### Barinder Singh Banwait (May 25 2020 at 19:51):

Kevin Buzzard said:

Definitions like

`blah`

in that namespace are all called`fraction_map.blah`

outside it

aaaaaaaah ... yes, it finds it now! and the error message gives me the next clue, which @Alex J. Best already noted: "too many arguments"

#### Kevin Buzzard (May 25 2020 at 19:51):

If you `open fraction_map`

then you can go back to calling it `blah`

#### Kevin Buzzard (May 25 2020 at 19:55):

What is this `fraction_map`

?

```
/-- Localization map from an integral domain `R` to its field of fractions. -/
@[reducible] def fraction_map [comm_ring K] := localization (non_zero_divisors R) K
```

Is this docstring wrong?

#### Kevin Buzzard (May 25 2020 at 19:55):

I don't understand how localisation works any more :-)

#### Barinder Singh Banwait (May 25 2020 at 19:57):

Kevin Buzzard said:

By "in

`integral_closure.lean`

", I hope you mean "I made a new file which starts with the line`import ring_theory.integral_closure`

" rather than "I am editing a library file".

i did actually start in my new file `src/hello_world.lean`

, but at some point switched to directly editing the `_target/deps/mathlib/src/ring_theory/integral_closure.lean`

, and trying to add the definition there somewhere. I'm guessing I should stick to my sandbox and not edit the library files?

but if the goal is to contribute to mathlib, starting off with small commits, then wouldn't that ultimately be done directly to the library file, to a branch of a fork of the mathlib repo?

#### Kevin Buzzard (May 25 2020 at 19:59):

Yeah you should definitely edit the library files at some point. But it might not be a good idea as a beginner. For example, all those library files are compiled into olean files on your system right now, because `leanproject`

downloaded compiled binaries for all of them. If you edit one, then it might need recompiling, and every file it imports might need recompiling too, and then everything will become very slow as VS Code tries to do it all on the fly. You can edit the library files but there are caveats.

#### Barinder Singh Banwait (May 25 2020 at 20:00):

Kevin Buzzard said:

If you

`open fraction_map`

then you can go back to calling it`blah`

oh, so that's what `open`

means! does that imply that all namespace names in the library are unique?

#### Barinder Singh Banwait (May 25 2020 at 20:02):

Kevin Buzzard said:

What is this

`fraction_map`

?`/-- Localization map from an integral domain `R` to its field of fractions. -/ @[reducible] def fraction_map [comm_ring K] := localization (non_zero_divisors R) K`

Is this docstring wrong?

the doc at the top says this:

```
When `R` is an integral domain, we define `fraction_map R K` as an abbreviation for
`localization (non_zero_divisors R) K`, the natural map to `R`'s field of fractions.
```

but i haven't looked under the hood of `localization`

#### Kevin Buzzard (May 25 2020 at 20:03):

Yeah I see, it's all been completely rewritten

#### Kevin Buzzard (May 25 2020 at 20:03):

oh hi @Amelia Livingston , I was just being confused by your new PR :-)

#### Kevin Buzzard (May 25 2020 at 20:04):

`localization`

is not a Prop, that's as far as I've got

#### Kevin Buzzard (May 25 2020 at 20:05):

`localization S A`

for `S`

a submonoid of `R`

, is the type of ring homs R -> A which induce an isomorphism $R[1/S]\to A$ I think

#### Barinder Singh Banwait (May 25 2020 at 20:06):

Kevin Buzzard said:

Yeah you should definitely edit the library files at some point. But it might not be a good idea as a beginner. For example, all those library files are compiled into olean files on your system right now, because

`leanproject`

downloaded compiled binaries for all of them. If you edit one, then it might need recompiling, and every file it imports might need recompiling too, and then everything will become very slow as VS Code tries to do it all on the fly. You can edit the library files but there are caveats.

ok, i wasn't aware of this recompiling issue; i'll continue in my own src folder for now

#### Alex J. Best (May 25 2020 at 20:10):

Kevin Buzzard said:

I don't understand how localisation works any more :-)

Same, this was quite confusing, maybe not the easiest project to tackle in this state of flux @Barinder Singh Banwait , I just got to

```
@[class] def is_integrally_closed (R) [integral_domain R] (φ : fraction_map R K) : Prop :=
(integral_closure R φ.codomain : set φ.codomain) = set.range φ.to_fun
```

but honestly I have no idea if this is the right thing!

#### Alex J. Best (May 25 2020 at 20:13):

Here I take the fraction map as an argument, so this leaves the problem of constructing the fraction field to the user, I guess this is how we get around problems of isomorphic-but-not-equal constructions, by making future definitions not depend on the exact construction used, but it feels weird to state being integrally closed in this way,

#### Barinder Singh Banwait (May 25 2020 at 20:19):

Alex J. Best said:

Kevin Buzzard said:

I don't understand how localisation works any more :-)

Same, this was quite confusing, maybe not the easiest project to tackle in this state of flux Barinder Singh Banwait , I just got to

`@[class] def is_integrally_closed (R) [integral_domain R] (φ : fraction_map R K) : Prop := (integral_closure R φ.codomain : set φ.codomain) = set.range φ.to_fun`

but honestly I have no idea if this is the right thing!

maybe not the easiest project, but a decent one to learn by running?!?

#### Barinder Singh Banwait (May 25 2020 at 20:22):

Alex J. Best said:

Here I take the fraction map as an argument, so this leaves the problem of constructing the fraction field to the user, I guess this is how we get around problems of isomorphic-but-not-equal constructions, by making future definitions not depend on the exact construction used, but it feels weird to state being integrally closed in this way,

yes indeed, because an "integrally closed domain" means "integrally closed in fraction field", so ideally the user shouldn't need to construct it explicitly

#### Amelia Livingston (May 25 2020 at 20:24):

I haven't read this thread in depth because I've got an exam tomorrow and the next day but I can help more after that. A couple of things:

- Your life will be easier if you assume
`K`

is a field, not an arbitrary comm ring. I'll add to the docs explaining this. - @Alex J. Best - I think that looks okay - does it still work if you replace
`to_fun`

with`to_map`

?`to_map`

is the underlying ring hom and it might cause problems using the underlying function`to_fun`

- The
`fraction_map`

section of the file will be added to a bit (I'll try open a PR on Wednesday); there are some useful lemmas from the old version of the file I want to 'port'.

#### Yury G. Kudryashov (May 25 2020 at 20:24):

My 5c: `(R)`

is a shorthand for `(R : guess_me)`

, i.e. lean will try to guess the type of R based on how do you use it

#### Yury G. Kudryashov (May 25 2020 at 20:27):

E.g. with `(R S) (f : R -> S) (x y) (h : f x = y)`

lean will guess most types

#### Alex J. Best (May 25 2020 at 20:27):

@Amelia Livingston Good luck with the exams, please don't get distracted on our account!

#### Alex J. Best (May 25 2020 at 20:31):

Barinder Singh Banwait said:

Alex J. Best said:

Kevin Buzzard said:

I don't understand how localisation works any more :-)

Same, this was quite confusing, maybe not the easiest project to tackle in this state of flux Barinder Singh Banwait , I just got to

`@[class] def is_integrally_closed (R) [integral_domain R] (φ : fraction_map R K) : Prop := (integral_closure R φ.codomain : set φ.codomain) = set.range φ.to_fun`

but honestly I have no idea if this is the right thing!

maybe not the easiest project, but a decent one to learn by running?!?

I'm not sure to be honest, I think there are probably quite a few other things that you would find mathematically relevant / interesting that don't touch on areas where mathlib isn't in such a state of transition right now. That said you've just learned some stuff about typeclasses and namespaces while running so who knows

#### Kevin Buzzard (May 25 2020 at 20:39):

@Barinder Singh Banwait I think just the opposite of Alex! I think that this brand spanking new approach to localisations needs to be tested, and I know that Barinder knows the mathematics behind the material, and it's about time this whole Dedekind Domain / DVR / Nullstellensatz level of commutative algebra gets going again. If someone makes it their project and then just asks lots of questions, people like me will get dragged back in because talking about localisations is a lot more interesting than marking undergraduate scripts. We need to check it works. Amelia has refactored the library and now we need to see it in action.

#### Alex J. Best (May 25 2020 at 20:42):

I guess I was swayed by Amelia saying she has more to add to the file yet!

#### Kenny Lau (May 25 2020 at 21:01):

$R$ is integrally closed

iff for every $r, s \in R$ with $s \ne 0$, if $(r/s)^n + a_1 (r/s)^{n-1} + \cdots + a_n = 0$, then $r/s \in R$

iff for every $r, s \in R$ with $s \ne 0$, if $r^n + a_1 r^{n-1} s + \cdots + a_n s^n = 0$, then $s \mid r$

#### Kenny Lau (May 25 2020 at 21:01):

there you go, no fraction field needed

#### Kenny Lau (May 25 2020 at 21:02):

iff for every $r, s \in R$ with $s \ne 0$, if $r^n \in \langle r^{n-1} s, \cdots, s^n \rangle$, then $s \mid r$

#### Kenny Lau (May 25 2020 at 21:03):

this is just like observing that $R$ is a valuation domain iff for every $r, s \in R$, either $r \mid s$ or $s \mid r$

#### Kenny Lau (May 25 2020 at 21:04):

then you can show that $R$ is integrally closed iff its integral closure w.r.t. any fraction field is itself

#### Kenny Lau (May 25 2020 at 21:05):

with a characterisation of "is a fraction field"

#### Yury G. Kudryashov (May 25 2020 at 21:47):

BTW, do we have something like `homogenize (p : polynomial R) (n := nat_degree p) : mv_polynomial (option unit) R`

?

#### Kevin Buzzard (May 25 2020 at 21:47):

There's a concept of A being integrally closed in B though

#### Kevin Buzzard (May 25 2020 at 21:47):

You (Kenny) are formalizing the absolute notion

#### Yury G. Kudryashov (May 25 2020 at 21:49):

Then we can have `integrally_closed_in R A`

, `integrally_closed R`

, and theorem(s) linking these two notions.

#### Scott Morrison (May 26 2020 at 02:02):

@Barinder Singh Banwait, going back to something you said above: you should definitely not edit mathlib by editing files in the `_target`

directory. Tools like `leanproject`

happily clobber this directory, and it's just asking to lose your work to edit files there. Better to clone `mathlib`

directly, and work in a branch there.

#### Yury G. Kudryashov (May 26 2020 at 02:18):

And PR your branch!

#### Johan Commelin (May 26 2020 at 03:27):

Kevin Buzzard said:

You (Kenny) are formalizing the absolute notion

But that's also what Barinder was doing

#### Johan Commelin (May 26 2020 at 03:28):

And we'll want the equivalence with Kenny's props anyway. I think following Kenny's approach for the absolute version is a good idea.

#### Barinder Singh Banwait (May 26 2020 at 14:26):

Scott Morrison said:

Barinder Singh Banwait, going back to something you said above: you should definitely not edit mathlib by editing files in the

`_target`

directory. Tools like`leanproject`

happily clobber this directory, and it's just asking to lose your work to edit files there. Better to clone`mathlib`

directly, and work in a branch there.

ok, thanks for clarifying. I have already forked and cloned `mathlib`

locally, but am currently working in a project environment to get to grips with the library and syntax.

#### Barinder Singh Banwait (May 26 2020 at 14:27):

Trying to follow Kenny's suggestion above for the relative case (i.e. A is integrally closed in B) led me to the following way to implement `is_integrally_closed_in`

, not using `integral_closure`

, but the lower-level `is_integral`

for elements. I tried the following in my sandbox (modelled on the setup in `integral_closure.lean`

):

```
universes u v
variables (R : Type u) {A : Type v}
variables [comm_ring R] [comm_ring A]
variables [algebra R A]
def is_integrally_closed_in : Prop := ∀ (a : A), is_integral R a → a ∈ R
```

That doesn't work though:

```
failed to synthesize type class instance for
R : Type u,
A : Type v,
_inst_1 : comm_ring R,
_inst_2 : comm_ring A,
_inst_3 : algebra R A,
a : A,
a : is_integral R a
⊢ has_mem A (Type u)
```

I'm still unsure how to read these errors, but I think it's complaining that it doesn't know what `a ∈ R`

means, if `a`

was supposed to be of type A. So something like

```
def is_integrally_closed_in : Prop := ∀ (a : A), is_integral R a → is_in_base_ring a
```

might work, except I don't know if there is such a method `is_in_base_ring`

for elements of R-algebras?

#### Johan Commelin (May 26 2020 at 14:28):

@Barinder Singh Banwait Yup, it's the same ambient set issue again (-;

#### Johan Commelin (May 26 2020 at 14:28):

`a`

lives in `A`

, and `R`

is not a *subset* of `A`

.

#### Johan Commelin (May 26 2020 at 14:28):

So you have to apply the map to get to `A`

#### Johan Commelin (May 26 2020 at 14:29):

You could write something like `\exists r : R, a = r`

or alternatively `a \in set.range blabla`

like yesterday.

#### Barinder Singh Banwait (May 26 2020 at 14:37):

@Johan Commelin the first suggestion gives

```
term
r
has type
R : Type u
but is expected to have type
A : Type v
```

#### Johan Commelin (May 26 2020 at 14:39):

Ooh, sorry... I thought that there would be an "invisible map" (see https://xenaproject.wordpress.com/2020/04/30/the-invisible-map/) that would get you from `R`

to `A`

.

Aka: `coe`

#### Johan Commelin (May 26 2020 at 14:40):

So, we'll have to apply the map explicitly.

#### Johan Commelin (May 26 2020 at 14:40):

In this case, the name of the map is `algebra_map A`

#### Johan Commelin (May 26 2020 at 14:41):

So you can write `\exists r : R, algebra_map A r = a`

, which is pretty ugly, I agree.

#### Barinder Singh Banwait (May 26 2020 at 14:43):

where is the map? is it the one in `algebra.lean`

? and in general, how do i find these things for myself? right click on algebra, go to definition, and hope to find it somewhere nearby?

#### Johan Commelin (May 26 2020 at 14:44):

Yup, that's one of the most useful ways of finding things.

#### Johan Commelin (May 26 2020 at 14:44):

Besides that: there is quite a rigid naming convention. After playing a little bit, you'll find that you can start guessing the names of lemmas.

#### Johan Commelin (May 26 2020 at 14:44):

Finally, there are tactics `library_search`

and `suggest`

, that can help with finding things in the library.

#### Barinder Singh Banwait (May 26 2020 at 14:47):

aah yes, I remember `library_search`

from the tutorials ... thanks!

#### Anne Baanen (May 26 2020 at 14:50):

If you have `φ : fraction_map R K`

, you can use `localization.is_integer φ a`

to say `∃ x : R, φ x = a`

. It might be worth the effort to generalize this to any `algebra`

.

#### Barinder Singh Banwait (May 26 2020 at 14:50):

Johan Commelin said:

So you can write

`\exists r : R, algebra_map A r = a`

, which is pretty ugly, I agree.

unfortunately it's still not liking the type of `r`

:

```
type mismatch at application
algebra_map A r
term
r
has type
R : Type u
but is expected to have type
Type ? : Type (?+1)
```

what is even meant by `Type ? : Type (?+1)`

? sorry for the numerous questions!

#### Scott Morrison (May 26 2020 at 14:51):

The `?`

is an unknown universe level.

#### Scott Morrison (May 26 2020 at 14:51):

So it is saying that it was expecting another argument which should have been a type, before the `R`

.

#### Scott Morrison (May 26 2020 at 14:52):

What is the type signature of `algebra_map`

?

#### Scott Morrison (May 26 2020 at 14:52):

Usually the first thing I do when I get a type mismatch error is hover my mouse of the current occurrence of the function, and see what its arguments are meant to be.

#### Johan Commelin (May 26 2020 at 14:52):

Huh... I thought I knew this part of the library... @Barinder Singh Banwait sorry for messing up

#### Barinder Singh Banwait (May 26 2020 at 14:53):

looks like it's `(R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A]`

#### Scott Morrison (May 26 2020 at 14:53):

Or type `#print algebra_map`

before the current theorem.

#### Johan Commelin (May 26 2020 at 14:53):

Maybe it wants to see the even uglier `algebra_map R A r`

#### Johan Commelin (May 26 2020 at 14:53):

Yup... it has `()`

around both `R`

and `A`

, so you need to explicitly give both.

#### Scott Morrison (May 26 2020 at 14:54):

(Johan really wishes that Lean were better at inference, but inference and coercions to functions do not play well together.)

#### Johan Commelin (May 26 2020 at 14:54):

We should be able to change that to `{R : Type u}`

by now... but I suggest that you don't bother with that now.

#### Scott Morrison (May 26 2020 at 14:54):

Because `algebra_map`

doesn't return an honest function, but instead a `ring_hom`

, it (used to be?) is hard for Lean to infer the type `R`

.

#### Barinder Singh Banwait (May 26 2020 at 14:56):

Scott Morrison said:

Or type

`#print algebra_map`

before the current theorem.

oh wow, print statements in Lean! first i've seen that

#### Johan Commelin (May 26 2020 at 14:59):

If you try `#print hello_world`

you will be disappointed

#### Barinder Singh Banwait (May 26 2020 at 15:00):

Johan Commelin said:

Yup... it has

`()`

around both`R`

and`A`

, so you need to explicitly give both.

yes! that works! is this an appropriate formal definition of "A is integrally closed in B", in the spirit of Kenny's suggestion above?

#### Johan Commelin (May 26 2020 at 15:01):

Well, Kenny didn't talk about the relative version right?

#### Johan Commelin (May 26 2020 at 15:01):

For the relative version, your definition seems perfect.

#### Barinder Singh Banwait (May 26 2020 at 15:03):

no he didn't indeed ... but wouldn't the absolute version just be the relative version, but with the ambient R-algebra set to the fraction field of R?

#### Johan Commelin (May 26 2020 at 15:58):

@Barinder Singh Banwait I think that for the absolute version, it might be nice to take Kenny's version as definition (because it avoids talking about *the* fraction field, so you don't have to choose one). After that, the first lemma to prove is that Kenny's def is equivalent to `is_integrally_closed_in R (any_arbitrary_fraction_field R)`

.

#### Johan Commelin (May 26 2020 at 16:00):

The reason this is nice: `Q`

is *not* the fraction field of `Z`

. Of course it satisfies the correct universal property, so you can easily plug it into `any_arbitrary_fraction_field R`

.

#### Barinder Singh Banwait (May 26 2020 at 16:42):

Johan Commelin said:

Barinder Singh Banwait I think that for the absolute version, it might be nice to take Kenny's version as definition (because it avoids talking about

thefraction field, so you don't have to choose one). After that, the first lemma to prove is that Kenny's def is equivalent to`is_integrally_closed_in R (any_arbitrary_fraction_field R)`

.

ok, that sounds like a plan for me to get on with! :big_smile: (though i'll probably be back before too long asking about how to tell lean about `any_arbitrary_fraction_field`

)

#### Johan Commelin (May 26 2020 at 16:47):

@Barinder Singh Banwait I think `fraction_map`

is exactly that.

#### Johan Commelin (May 26 2020 at 19:07):

@Barinder Singh Banwait What do you think of

```
variables (R : Type u)
variables [comm_ring R]
def is_integrally_closed : Prop :=
∀ ⦃r s : R⦄, (∃ (n : ℕ) (f : ℕ → R) (hf : f 0 = 1),
∑ ij in finset.nat.antidiagonal n, f ij.1 * r ^ ij.2 * s ^ ij.1 = 0) → s ∣ r
```

#### Johan Commelin (May 26 2020 at 19:08):

I didn't think about this definition... I might have gotten the order wrong...

#### Johan Commelin (May 26 2020 at 19:09):

Silly me. Now it should be fixed.

#### Johan Commelin (May 26 2020 at 19:11):

`finset.nat.antidiagonal n`

is the finite set of pairs of natural numbers `(i,j)`

with `i + j = n`

.

#### Patrick Massot (May 26 2020 at 19:34):

Don't we have a definition for this in the perfectoid project?

#### Kevin Buzzard (May 26 2020 at 19:40):

```
import ring_theory.integral_closure
variables (R : Type*) (A : Type*) [decidable_eq R] [decidable_eq A]
variables [comm_ring R] [comm_ring A] [algebra R A]
open function
/--An R-algebra A is integrally closed if every element of A that is integral over R is contained in
the image of the canonical map R → A. This algebra_map is required to be injective.-/
structure is_integrally_closed : Prop :=
(inj : injective (algebra_map A : R → A))
(closed : ∀ a : A, (is_integral R a) → a ∈ set.range (algebra_map A : R → A))
```

#### Patrick Massot (May 26 2020 at 19:41):

This is from the perfectoid project, right?

#### Kevin Buzzard (May 26 2020 at 19:43):

Right, it's in `for_mathlib`

#### Johan Commelin (May 26 2020 at 19:47):

But this is the relative case, not the absolute one. (To be clear: we want both.)

#### Bhavik Mehta (May 26 2020 at 20:14):

You know you really should PR things to mathlib :P

#### Patrick Massot (May 26 2020 at 20:14):

Yes we know

#### Patrick Massot (May 26 2020 at 20:14):

This is why we try to teach younger people to avoid our past mistakes

#### Kevin Buzzard (May 26 2020 at 20:25):

@Bhavik Mehta do you understand that Johan's massive removal of a bunch of stuff from core was part of a perfectoid PR? Sometimes these things take forever. When I've finished marking I am going to completely refactor normal subgroups and quotient groups again just to PR more perfectoid stuff. The task is humongous for us and we do appreciate that it needs doing but it is surprisingly difficult!

#### Bhavik Mehta (May 26 2020 at 20:25):

Haha I know I was just poking a bit of fun :)

#### Kevin Buzzard (May 26 2020 at 20:25):

I know :-)

#### Kevin Buzzard (May 26 2020 at 20:26):

Major design decisions have been made eg bundling ring homs since we wrote the project

#### Kevin Buzzard (May 26 2020 at 20:26):

But on the other hand I regard this now as an excuse to make mathlib better

#### Barinder Singh Banwait (May 27 2020 at 08:01):

Johan Commelin said:

Barinder Singh Banwait What do you think of

`variables (R : Type u) variables [comm_ring R] def is_integrally_closed : Prop := ∀ ⦃r s : R⦄, s ≠ 0 → (∃ (n : ℕ) (f : ℕ → R) (hf : f 0 = 1), ∑ ij in finset.nat.antidiagonal n, f ij.1 * r ^ ij.2 * s ^ ij.1 = 0) → s ∣ r`

That looks good! Much better than what I was trying, which was the last of Kenny's displayed definitions involving $r^n \in\langle r^{n-1}s,\cdots,s^n\rangle$; I tried (after asking over at "noob questions")

```
def is_integrally_closed (R) [integral_domain R] : Prop :=
(∀ (r : R) (s : R), (s ≠ 0) ∧ (∃ n : ℕ ,
r^n ∈ span (set.image (λ i : fin n, r^(n-1-i) * s^(↑i + 1)) : set R)) → s ∣ r
```

but this failed because the `set.image`

was of type `set (fin n) → set R`

and I needed it to be of type `set R`

#### Barinder Singh Banwait (May 27 2020 at 08:02):

Looking at the 'perfectoid project' implementation of `is_integrally_closed`

, it looks like my attempt at `is_integrally_closed_in`

above was missing the requirement that the algebra map is injective which gives the inclusion of rings

#### Johan Commelin (May 27 2020 at 08:07):

Yup, I also noticed the injectivity thing

#### Johan Commelin (May 27 2020 at 08:07):

(We're still too much used to thinking of subrings :rofl:)

#### Johan Commelin (May 27 2020 at 08:08):

When we formalised Huber pairs, we worked with subrings for a long time, until I realised this meant that we couldn't turn `Z_p, Q_p`

into a huber pair.

#### Johan Commelin (May 27 2020 at 08:08):

So we switched to injective ring homs

#### Johan Commelin (May 27 2020 at 08:16):

@Barinder Singh Banwait One big advantage of `finset.nat.antidiagonal`

is that it avoids talking about subtraction of natural numbers. If you want to know why this is a good thing, write `#eval 2 - 3`

#### Barinder Singh Banwait (May 27 2020 at 10:33):

Johan Commelin said:

Barinder Singh Banwait One big advantage of

`finset.nat.antidiagonal`

is that it avoids talking about subtraction of natural numbers. If you want to know why this is a good thing, write`#eval 2 - 3`

aah, I see. I note that `#eval 1/0`

gives the same result :laughing:

#### Barinder Singh Banwait (May 27 2020 at 10:33):

is a `structure`

the same as a `def`

? I was just going to write

```
def is_integrally_closed_in : Prop :=
(injective (algebra_map R A)) ∧
(∀ (a : A), is_integral R a → ∃ r : R, algebra_map R A r = a)
```

which seems to compile fine, but is the `structure`

syntax better?

#### Kevin Buzzard (May 27 2020 at 10:34):

`structure`

does define a new thing, like `def`

, but it defines something for which the use syntax will be a bit different.

#### Barinder Singh Banwait (May 27 2020 at 10:37):

you mean the `use`

tactic will be written differently?

#### Kevin Buzzard (May 27 2020 at 10:37):

As long as the interface is there, then the only difference for users will be that there will be a slightly different syntax available for usage. For example if you defined a group to be `axiom1 \and axiom2 \and axiom3`

and then if you had a term `G`

of this type, you would forever be writing things like `G.2.1`

to get to axiom 2. With a structure it's just `G.mul_one`

by definition. But these things can typically be worked around. It's kind of an implementation issue I guess.

#### Kevin Buzzard (May 27 2020 at 10:39):

I just mean the obvious statement that there are lots of ways of implementing the same mathematical idea, but different implementations will then give you different ways of accessing the information hidden inside the idea

#### Barinder Singh Banwait (May 27 2020 at 10:40):

oh i see, that makes sense, so you get to name your conditions which i can see will make for way more readable code

#### Kevin Buzzard (May 27 2020 at 10:40):

I prefer it if some CS person does the definitions and then I just prove the theorems. But sometimes the CS people just say "we don't know, it depends on what you want to do with it, just try anything and then change it later if it's annoying"

#### Kevin Buzzard (May 27 2020 at 10:40):

My advice is to ask someone like @Johan Commelin just to tell you a definition and then start proving theorems with it.

#### Barinder Singh Banwait (May 27 2020 at 10:46):

yep @Johan Commelin has helped me out a lot, i've now got the definitions of absolute/relative integrally-closed, am now working on lemmas proving equivalence of definitions

#### Johan Commelin (May 27 2020 at 10:46):

@Barinder Singh Banwait In this case I would use the `structure`

version

#### Kevin Buzzard (May 27 2020 at 10:47):

proving lemmas is much more fun because you don't have to keep asking "is this right?" -- if it compiles, it's right.

#### Johan Commelin (May 27 2020 at 10:47):

Looking forward to the "fundamental theorem of absolute integrally-closedness"

#### Kevin Buzzard (May 27 2020 at 10:48):

Already one can ask whether the integral closure of the integral closure is the integral closure, this makes sense in a relative situation and...isn't this the sort of thing which Kenny has already essentially done?

#### Barinder Singh Banwait (May 27 2020 at 10:49):

Kevin Buzzard said:

Already one can ask whether the integral closure of the integral closure is the integral closure, this makes sense in a relative situation and...isn't this the sort of thing which Kenny has already essentially done?

yes i recall seeing `integral_closure_idem`

in integral_closure.lean

#### Barinder Singh Banwait (May 27 2020 at 11:13):

@Johan Commelin is there a trick to get the $\sum$ notation above to work? In your definition above `∑ ij in finset.nat.antidiagonal n`

, it's complaining about `unexpected token`

, but elsewhere in the library it seems fine

#### Johan Commelin (May 27 2020 at 11:13):

`open_locale big_operators`

#### Johan Commelin (May 27 2020 at 11:13):

Somewhere near the top of your file

#### Barinder Singh Banwait (May 27 2020 at 15:56):

I'm having some trouble stating that "fundamental theorem"; i've tried:

```
structure is_integrally_closed_in : Prop :=
(inj : injective (algebra_map R A))
(closed : ∀ (a : A), is_integral R a → ∃ r : R, algebra_map R A r = a)
lemma fundamental_theorem_integrally_closedness (R) [integral_domain R] :
is_integrally_closed R ↔ ∀ (A : Type*) [comm_ring A], is_integrally_closed_in R (fraction_map R A) :=
```

but I get this error:

```
function expected at
is_integrally_closed_in R
term has type
Prop
```

what's going on here? i thought that `is_integrally_closed_in`

needs two arguments R and A, but apparently I'm wrong, is it a map from R to A that is required?

#### Kevin Buzzard (May 27 2020 at 15:58):

What are the imports?

#### Barinder Singh Banwait (May 27 2020 at 15:59):

```
import ring_theory.noetherian
import ring_theory.integral_closure
import ring_theory.adjoin
import ring_theory.algebra
```

#### Kevin Buzzard (May 27 2020 at 16:00):

Can you post fully working code? I still can't get it to compile

#### Barinder Singh Banwait (May 27 2020 at 16:00):

and here are the global variables and opens:

```
universes u v
variables (R : Type u) {A : Type v}
variables [comm_ring R] [comm_ring A]
variables [algebra R A]
variables i : ℕ
variables (K : Type*)
open ideal
open function
open_locale big_operators
```

#### Barinder Singh Banwait (May 27 2020 at 16:00):

Kevin Buzzard said:

Can you post fully working code? I still can't get it to compile

ok one sec ...

#### Barinder Singh Banwait (May 27 2020 at 16:01):

```
import ring_theory.noetherian
import ring_theory.integral_closure
import ring_theory.adjoin
import ring_theory.algebra
universes u v
variables (R : Type u) {A : Type v}
variables [comm_ring R] [comm_ring A]
variables [algebra R A]
variables i : ℕ
variables (K : Type*)
open ideal
open function
open_locale big_operators
structure is_integrally_closed_in : Prop :=
(inj : injective (algebra_map R A))
(closed : ∀ (a : A), is_integral R a → ∃ r : R, algebra_map R A r = a)
def my_set (R) [integral_domain R] (r : R) (s : R) (n : ℕ) :=
{ x | ∃ (i:ℕ ) (h : 0≤ i) (h2 :i≤ n-1), x = r^(n-1-i) *s^(i+1) }
def is_integrally_closed (R) [integral_domain R] : Prop :=
∀ (r : R) (s : R), (s ≠ 0) ∧ (∃ n : ℕ ,
r^n ∈ span (my_set R r s n)) → s ∣ r
lemma equiv_johan_absolute (R) [integral_domain R] :
is_integrally_closed R ↔ ∀ ⦃r s : R⦄, s ≠ 0 → (∃ (n : ℕ) (f : ℕ → R) (hf : f 0 = 1),
∑ ij in finset.nat.antidiagonal n, f ij.1 * r ^ ij.2 * s ^ ij.1 = 0) → s ∣ r :=
begin
sorry,
end
lemma fundamental_theorem_integrally_closedness (R) [integral_domain R] :
is_integrally_closed R ↔ ∀ (A : Type*) [comm_ring A], is_integrally_closed_in R (fraction_map R A) :=
begin
sorry,
end
```

#### Kevin Buzzard (May 27 2020 at 16:02):

Thanks. If you hover over `is_integrally_closed_in`

then you will see that indeed it takes one explicit argument

#### Kevin Buzzard (May 27 2020 at 16:02):

Just hover over the function where the error is

#### Barinder Singh Banwait (May 27 2020 at 16:04):

the explicit arguments are the one in round parentheses, right? so in this case that's just `(R : Type u)`

; so it only needs one R of type `universes`

?

#### Kevin Buzzard (May 27 2020 at 16:05):

In your current set-up it is just asking for a ring R, yes

#### Kevin Buzzard (May 27 2020 at 16:05):

which of course is not a good idea, and which explains the error

#### Kevin Buzzard (May 27 2020 at 16:06):

You should think of `R : Type u`

as it asking for a set, and `[comm_ring R]`

as it saying "actually, that set needs a ring structure, but I'll find it from somewhere"

#### Barinder Singh Banwait (May 27 2020 at 16:07):

so the real problem is with the definition of `is_integrally_closed_in`

, which ought to have input either two rings, or an algebra map from R to A?

#### Kevin Buzzard (May 27 2020 at 16:07):

If your input is just the two rings then however will Lean guess the map between them?

#### Kevin Buzzard (May 27 2020 at 16:08):

oh, apparently `algebra`

is a class so Lean *can* do this

#### Kevin Buzzard (May 27 2020 at 16:08):

So yes, it looks like the input ought to be two rings

#### Kevin Buzzard (May 27 2020 at 16:09):

and before the function is run, there had better be a variable `[algebra R A]`

which will put the R-algebra structure on A into the typeclass inference system

#### Kevin Buzzard (May 27 2020 at 16:11):

This set-up is stil a bit messed up, even after the fix which I'm pushing you to notice yourself, but unfortunately I don't have time to fix it right now even though I want to support you as a new user; I have to get back to marking.

#### Kevin Buzzard (May 27 2020 at 16:12):

But before I go, does anyone know why if I hover over `[algebra R A] I see `

algebra R A ring.to_semiring` ?

#### Barinder Singh Banwait (May 27 2020 at 16:13):

ok thanks Kevin ... so i've tried to make the inputs to `is_integrally_closed_in`

more explicit:

```
structure is_integrally_closed_in (R : Type u) (A : Type v) [comm_ring R] [comm_ring A] [algebra R A] : Prop :=
(inj : injective (algebra_map R A))
(closed : ∀ (a : A), is_integral R a → ∃ r : R, algebra_map R A r = a)
```

and then i tried

```
lemma fundamental_theorem_integrally_closedness (R) [integral_domain R] :
is_integrally_closed R ↔ ∀ (A : Type*) [comm_ring A] [algebra R A], is_integrally_closed_in R A:=
```

but that gave me error at `algebra`

with semiring and comm_ring

#### Barinder Singh Banwait (May 27 2020 at 16:14):

Kevin Buzzard said:

But before I go, does anyone know why if I hover over

`[algebra R A] I see`

algebra R A ring.to_semiring` ?

yes, my problem exactly!

#### Kevin Buzzard (May 27 2020 at 16:14):

This lemma is not true though, right?

#### Barinder Singh Banwait (May 27 2020 at 16:14):

Kevin Buzzard said:

This set-up is stil a bit messed up, even after the fix which I'm pushing you to notice yourself, but unfortunately I don't have time to fix it right now even though I want to support you as a new user; I have to get back to marking.

of course, absolutely - thanks for your help!

#### Kevin Buzzard (May 27 2020 at 16:15):

Because if R is integrally closed it doesn't imply that every map R -> A is injective

#### Kevin Buzzard (May 27 2020 at 16:15):

so first you might want to figure out what maths statement you're making

#### Barinder Singh Banwait (May 27 2020 at 16:23):

yes indeed, now the lemma is false; that last `A`

should be a fraction field of R. but the closest thing we have to that is a `fraction_map`

#### Reid Barton (May 27 2020 at 16:32):

I think the quantifiers are also not where you want them, if `A`

is meant to be the fraction field.

#### Reid Barton (May 27 2020 at 16:32):

It's better to prove: for every fraction field `A`

: `R`

is integrally closed iff it's integrally closed in `A`

.

#### Reid Barton (May 27 2020 at 16:33):

Because now you can also conclude that if `R`

is integrally closed in one fraction field, it is also in another. (And the statement is generally easier to use.)

#### Reid Barton (May 27 2020 at 16:35):

Of course there's no additional mathematical content in this version because fraction fields are all "the same", but if `A`

can be something more general (e.g., any field that `R`

maps to?) then there is.

#### Barinder Singh Banwait (May 27 2020 at 17:27):

Reid Barton said:

It's better to prove: for every fraction field

`A`

:`R`

is integrally closed iff it's integrally closed in`A`

.

aah yes, putting the "for every fraction field" before the `:`

makes a lot more sense, thanks Reid!

So i've got a statement that now compiles:

```
lemma fundamental_theorem_integrally_closedness (R : Type u) (A : Type v) [integral_domain R] [comm_ring A] [algebra R A] [fraction_map R A]:
is_integrally_closed R ↔ is_integrally_closed_in R A :=
begin
sorry,
end
```

That's putting a lot of structure on R and A; does this now translate to saying: Let $R$ be an integral domain. Then, $\forall$ fraction fields $A$ of $R$, we have : $R$ is integrally closed $\Leftrightarrow R$ is integrally closed in $A$.

#### Kevin Buzzard (May 27 2020 at 17:28):

Is faction_map a typeclass?

#### Barinder Singh Banwait (May 27 2020 at 17:29):

ermm...`@[reducible] def fraction_map [comm_ring K] := localization (non_zero_divisors R) K`

... so i guess not?

#### Kevin Buzzard (May 27 2020 at 17:29):

(Then it shouldn't be in square brackets)

#### Kevin Buzzard (May 27 2020 at 17:30):

But this is looking better -- maybe just change to round brackets?

#### Barinder Singh Banwait (May 27 2020 at 17:33):

so changing it from `[fraction_map R A]`

to `(fraction_map R A)`

gives `don't know how to synthesize placeholder`

, but changing it to `(H : fraction_map R A)`

works fine, and i guess this is what I want; that A is a fraction field of R is a hypothesis, so that `H : `

is necessary?

#### Johan Commelin (May 27 2020 at 17:46):

@Barinder Singh Banwait With `[...]`

you don't need to give the argument a name, with the other types of parens you (usually) do need to give the name.

#### Johan Commelin (May 27 2020 at 17:46):

But I suggest you call it `f`

instead of `H`

, because we want to think of it as the map from `R`

to its fraction field.

#### Barinder Singh Banwait (May 27 2020 at 18:08):

Johan Commelin said:

But I suggest you call it

`f`

instead of`H`

, because we want to think of it as the map from`R`

to its fraction field.

ok, will do, thanks @Johan Commelin !

#### Johan Commelin (May 27 2020 at 18:10):

Please let me know if you've got a working statement! It's high time that this lemma is proven (-;

#### Barinder Singh Banwait (May 27 2020 at 18:40):

i think i've got the statement now:

```
import ring_theory.noetherian
import ring_theory.integral_closure
import ring_theory.adjoin
import ring_theory.algebra
universes u v
variables (R : Type u) {A : Type v}
variables [comm_ring R] [comm_ring A]
variables [algebra R A]
variables i : ℕ
variables (K : Type*)
open ideal
open function
open_locale big_operators
structure is_integrally_closed_in (R : Type u) (A : Type v) [comm_ring R] [comm_ring A]
[algebra R A] : Prop :=
(inj : injective (algebra_map R A))
(closed : ∀ (a : A), is_integral R a → ∃ r : R, algebra_map R A r = a)
def my_set (R) [integral_domain R] (r : R) (s : R) (n : ℕ) :=
{ x | ∃ (i:ℕ ) (h : 0≤ i) (h2 :i≤ n-1), x = r^(n-1-i) *s^(i+1) }
def is_integrally_closed (R) [integral_domain R] : Prop :=
∀ (r : R) (s : R), (s ≠ 0) ∧ (∃ n : ℕ ,
r^n ∈ span (my_set R r s n)) → s ∣ r
lemma equiv_johan_absolute (R) [integral_domain R] :
is_integrally_closed R ↔ ∀ ⦃r s : R⦄, s ≠ 0 → (∃ (n : ℕ) (f : ℕ → R) (hf : f 0 = 1),
∑ ij in finset.nat.antidiagonal n, f ij.1 * r ^ ij.2 * s ^ ij.1 = 0) → s ∣ r :=
begin
sorry,
end
lemma fundamental_theorem_integrally_closedness (R : Type u) (A : Type v) [integral_domain R]
[comm_ring A] [algebra R A] (f : fraction_map R A):
is_integrally_closed R ↔ is_integrally_closed_in R A :=
begin
sorry,
end
```

(this is just in my project for now, i know that those names aren't fit for the library!) i haven't started on the proofs yet, i was going to start that tomorrow morning

#### Johan Commelin (May 27 2020 at 18:42):

Looks good to me!

#### Barinder Singh Banwait (May 29 2020 at 06:55):

i've got stuck on proving the following mathematically-obvious statement from above: Suppose we have a linear relation

$\sum_{i+j=n} a_i r^j s^i = 0.$

with $a_n \neq 0$. Then $r^n \in$ span $\langle r^{n-1}s, \cdots, s^n\rangle$. How does one show span membership? I saw that linear_algebra.basic has a `mem_span`

lemma, which I tried in the following MWE as follows:

```
lemma mwe (R) [integral_domain R] (n : ℕ) (f : ℕ → R) (hf : f 0 = 1) : ∀ ⦃r s : R⦄, s ≠ 0 →
∑ ij in finset.nat.antidiagonal n, f ij.1 * r ^ ij.2 * s ^ ij.1 = 0 →
r^n ∈ span R (my_set R r s n) :=
begin
intros r s,
intro s_non_zero,
intro H,
rw mem_span,
intro p,
intro p_H,
???
end
```

...but then I get stuck :(

#### Kenny Lau (May 29 2020 at 07:02):

but it's wrong

#### Kenny Lau (May 29 2020 at 07:03):

n=1, 2r+s=0

#### Kenny Lau (May 29 2020 at 07:03):

(r=1, s=-2)

#### Kenny Lau (May 29 2020 at 07:04):

Kenny Lau said:

$R$ is integrally closed

iff for every $r, s \in R$ with $s \ne 0$, if $(r/s)^n + a_1 (r/s)^{n-1} + \cdots + a_n = 0$, then $r/s \in R$

iff for every $r, s \in R$ with $s \ne 0$, if $r^n + a_1 r^{n-1} s + \cdots + a_n s^n = 0$, then $s \mid r$

you will notice in my formulation that the coefficient of $r^n$ is $1$

#### Barinder Singh Banwait (May 29 2020 at 07:07):

Oh yes, quite right, sorry I forgot to explicitly state in my last post that I'm taking $a_0 = 1$. My apologies. It is in the statement of the `lemma mwe`

i'm trying to prove; i'll edit for clarity, Thanks Kenny

#### Kenny Lau (May 29 2020 at 07:10):

you can do some rewrites to change the goal into `finset.sum _ \in span R _`

#### Johan Commelin (May 29 2020 at 07:28):

And after that, there should be a `submodule.sum_mem`

lemma, hopefully.

#### Barinder Singh Banwait (May 29 2020 at 07:44):

thanks, yes that all looks promising. unfortunately i'm struggling to rewrite as suggested, i'm not sure how I can "isolate a summand" from a sum, which is my Hypothesis `H`

; so far I've got this:

```
lemma mwe (R) [integral_domain R] (n : ℕ) (f : ℕ → R) (hf : f 0 = 1) : ∀ ⦃r s : R⦄, s ≠ 0 →
∑ ij in finset.nat.antidiagonal n, f ij.1 * r ^ ij.2 * s ^ ij.1 = 0 →
r^n ∈ span R (my_set R r s n) :=
begin
intros r s,
intro s_non_zero,
intro H,
have K : r^n = (range n).sum (λ i, -1 * f (i+1) * r^(n-i-1) * s^(1+i)), by sorry,
rw K,
rw mem_span,
intro p,
intro p_H,
apply submodule.sum_mem,
rw my_set at p_H,
intro c,
intro C,
sorry,
end
```

#### Kenny Lau (May 29 2020 at 07:50):

- you might consider using
`finset.range (n+1)`

instead of antidiagonal - if you insist, then there should be some
`finset.insert_erase`

lemma for you to rewrite with

#### Johan Commelin (May 29 2020 at 08:11):

@Kenny Lau Using `finset.range`

will create nat subtraction problems elsewhere.

#### Johan Commelin (May 29 2020 at 08:11):

So I would opt for the `finset.insert_erase`

approach

#### Kenny Lau (May 29 2020 at 08:11):

solvable nat subtraction problems

#### Johan Commelin (May 29 2020 at 08:11):

Solvable `finset.insert_erase`

problem

Last updated: May 13 2021 at 05:21 UTC