Integrally closed domain

Stream: new members

[Barinder Singh Banwait]

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]

@Barinder Singh Banwait Hi, and welcome!

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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]

Hi Johan, thanks for the welcome!

[Barinder Singh Banwait]

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]

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]

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

[Johan Commelin]

And the (R) is really just shorthand for (R : Type*).

[Barinder Singh Banwait]

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]

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]

Barinder and I have talked Zelda in the past

[Barinder Singh Banwait]

Johan Commelin said:

And the (R) is really just shorthand for (R : Type*).

aah yes, that makes more sense now!

[Johan Commelin]

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

[Barinder Singh Banwait]

Johan Commelin said:

So, long story short, you want to say that the integral_closure R (blabla) is equal to 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]

Note that this file was thoroughly rewritten a few days ago

[Johan Commelin]

Do you have the latest version?

[Barinder Singh Banwait]

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]

You should be able to type leanproject up in your project

[Johan Commelin]

Hmmz... it seems that fraction_ring got lost in the battle

[Johan Commelin]

There is now something called fraction_map, which should serve the same purpose

[Johan Commelin]

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

[Barinder Singh Banwait]

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]

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]

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]

(The ≠ is abuse of notation)

[Barinder Singh Banwait]

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

[Barinder Singh Banwait]

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]

to_integral_domain is in the fraction_map namespace

[Alex J. Best]

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]

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]

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]

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]

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

[Barinder Singh Banwait]

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]

Definitions like blah in that namespace are all called fraction_map.blah outside it

[Barinder Singh Banwait]

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]

If you open fraction_map then you can go back to calling it blah

[Kevin Buzzard]

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]

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

[Barinder Singh Banwait]

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]

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]

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]

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]

Yeah I see, it's all been completely rewritten

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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:

1. 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.
2. @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
3. 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]

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]

E.g. with (R S) (f : R -> S) (x y) (h : f x = y) lean will guess most types

[Alex J. Best]

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

[Alex J. Best]

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]

@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]

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

[Kenny Lau]

$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]

there you go, no fraction field needed

[Kenny Lau]

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]

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]

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

[Kenny Lau]

with a characterisation of "is a fraction field"

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

You (Kenny) are formalizing the absolute notion

[Yury G. Kudryashov]

Then we can have integrally_closed_in R A, integrally_closed R, and theorem(s) linking these two notions.

[Scott Morrison]

@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]

And PR your branch!

[Johan Commelin]

Kevin Buzzard said:

You (Kenny) are formalizing the absolute notion

But that's also what Barinder was doing

[Johan Commelin]

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]

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]

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]

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

[Johan Commelin]

a lives in A, and R is not a subset of A.

[Johan Commelin]

So you have to apply the map to get to A

[Johan Commelin]

You could write something like \exists r : R, a = r or alternatively a \in set.range blabla like yesterday.

[Barinder Singh Banwait]

@Johan Commelin the first suggestion gives

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

So you can write \exists r : R, algebra_map A r = a, which is pretty ugly, I agree.

[Barinder Singh Banwait]

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]

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

[Johan Commelin]

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]

Finally, there are tactics library_search and suggest, that can help with finding things in the library.

[Barinder Singh Banwait]

aah yes, I remember library_search from the tutorials ... thanks!

[Anne Baanen]

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]

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]

The ? is an unknown universe level.

[Scott Morrison]

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

[Scott Morrison]

What is the type signature of algebra_map?

[Scott Morrison]

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]

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

[Barinder Singh Banwait]

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

[Scott Morrison]

Or type #print algebra_map before the current theorem.

[Johan Commelin]

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

[Johan Commelin]

Yup... it has () around both R and A, so you need to explicitly give both.

[Scott Morrison]

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

[Johan Commelin]

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]

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]

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]

If you try #print hello_world you will be disappointed

[Barinder Singh Banwait]

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]

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

[Johan Commelin]

For the relative version, your definition seems perfect.

[Barinder Singh Banwait]

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]

@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]

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]

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

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]

@Barinder Singh Banwait I think fraction_map is exactly that.

[Johan Commelin]

@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]

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

[Johan Commelin]

Silly me. Now it should be fixed.

[Johan Commelin]

finset.nat.antidiagonal n is the finite set of pairs of natural numbers (i,j) with i + j = n.

[Patrick Massot]

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

[Kevin Buzzard]

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]

This is from the perfectoid project, right?

[Kevin Buzzard]

Right, it's in for_mathlib

[Johan Commelin]

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

[Bhavik Mehta]

You know you really should PR things to mathlib :P

[Patrick Massot]

Yes we know

[Patrick Massot]

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

[Kevin Buzzard]

@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]

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

[Kevin Buzzard]

I know :-)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Barinder Singh Banwait]

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]

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]

Yup, I also noticed the injectivity thing

[Johan Commelin]

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

[Johan Commelin]

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]

So we switched to injective ring homs

[Johan Commelin]

@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]

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]

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]

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]

you mean the use tactic will be written differently?

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

@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]

open_locale big_operators

[Johan Commelin]

Somewhere near the top of your file

[Barinder Singh Banwait]

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]

What are the imports?

[Barinder Singh Banwait]

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

[Kevin Buzzard]

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

[Barinder Singh Banwait]

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]

Kevin Buzzard said:

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

ok one sec ...

[Barinder Singh Banwait]

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]

Thanks. If you hover over is_integrally_closed_in then you will see that indeed it takes one explicit argument

[Kevin Buzzard]

Just hover over the function where the error is

[Barinder Singh Banwait]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

oh, apparently algebra is a class so Lean can do this

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

This lemma is not true though, right?

[Barinder Singh Banwait]

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]

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

[Kevin Buzzard]

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

[Barinder Singh Banwait]

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]

I think the quantifiers are also not where you want them, if A is meant to be the fraction field.

[Reid Barton]

It's better to prove: for every fraction field A: R is integrally closed iff it's integrally closed in A.

[Reid Barton]

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]

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]

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]

Is faction_map a typeclass?

[Barinder Singh Banwait]

ermm...@[reducible] def fraction_map [comm_ring K] := localization (non_zero_divisors R) K ... so i guess not?

[Kevin Buzzard]

(Then it shouldn't be in square brackets)

[Kevin Buzzard]

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

[Barinder Singh Banwait]

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]

@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]

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]

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]

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

[Barinder Singh Banwait]

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]

Looks good to me!

[Barinder Singh Banwait]

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]

but it's wrong

[Kenny Lau]

n=1, 2r+s=0

[Kenny Lau]

(r=1, s=-2)

[Kenny Lau]

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]

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]

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

[Johan Commelin]

And after that, there should be a submodule.sum_mem lemma, hopefully.

[Barinder Singh Banwait]

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]

1. you might consider using finset.range (n+1) instead of antidiagonal
2. if you insist, then there should be some finset.insert_erase lemma for you to rewrite with

[Johan Commelin]

@Kenny Lau Using finset.range will create nat subtraction problems elsewhere.

[Johan Commelin]

So I would opt for the finset.insert_erase approach

[Kenny Lau]

solvable nat subtraction problems

[Johan Commelin]

Solvable finset.insert_erase problem