Zulip Chat Archive

Stream: new members

Topic: Integrally closed domain


view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 25 2020 at 18:37):

@Barinder Singh Banwait Hi, and welcome!

view this post on Zulip 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"

view this post on Zulip Johan Commelin (May 25 2020 at 18:38):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 25 2020 at 18:40):

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

view this post on Zulip 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.

view this post on Zulip Barinder Singh Banwait (May 25 2020 at 18:42):

Hi Johan, thanks for the welcome!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 25 2020 at 18:43):

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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 25 2020 at 18:45):

Barinder and I have talked Zelda in the past

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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) 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

view this post on Zulip Johan Commelin (May 25 2020 at 18:51):

Note that this file was thoroughly rewritten a few days ago

view this post on Zulip Johan Commelin (May 25 2020 at 18:51):

Do you have the latest version?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 25 2020 at 18:53):

You should be able to type leanproject up in your project

view this post on Zulip Johan Commelin (May 25 2020 at 18:55):

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

view this post on Zulip Johan Commelin (May 25 2020 at 18:55):

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

view this post on Zulip Johan Commelin (May 25 2020 at 18:56):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 25 2020 at 18:59):

(The is abuse of notation)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Alex J. Best (May 25 2020 at 19:42):

to_integral_domain is in the fraction_map namespace

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 25 2020 at 19:49):

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

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (May 25 2020 at 19:51):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 25 2020 at 19:55):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 25 2020 at 20:03):

Yeah I see, it's all been completely rewritten

view this post on Zulip Kevin Buzzard (May 25 2020 at 20:03):

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

view this post on Zulip Kevin Buzzard (May 25 2020 at 20:04):

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

view this post on Zulip 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]AR[1/S]\to A I think

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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,

view this post on Zulip 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?!?

view this post on Zulip 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

view this post on Zulip 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:

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Alex J. Best (May 25 2020 at 20:27):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Kenny Lau (May 25 2020 at 21:01):

RR is integrally closed
iff for every r,sRr, s \in R with s0s \ne 0, if (r/s)n+a1(r/s)n1++an=0(r/s)^n + a_1 (r/s)^{n-1} + \cdots + a_n = 0, then r/sRr/s \in R
iff for every r,sRr, s \in R with s0s \ne 0, if rn+a1rn1s++ansn=0r^n + a_1 r^{n-1} s + \cdots + a_n s^n = 0, then srs \mid r

view this post on Zulip Kenny Lau (May 25 2020 at 21:01):

there you go, no fraction field needed

view this post on Zulip Kenny Lau (May 25 2020 at 21:02):

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

view this post on Zulip Kenny Lau (May 25 2020 at 21:03):

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

view this post on Zulip Kenny Lau (May 25 2020 at 21:04):

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

view this post on Zulip Kenny Lau (May 25 2020 at 21:05):

with a characterisation of "is a fraction field"

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 25 2020 at 21:47):

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

view this post on Zulip Kevin Buzzard (May 25 2020 at 21:47):

You (Kenny) are formalizing the absolute notion

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (May 26 2020 at 02:18):

And PR your branch!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 26 2020 at 14:28):

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

view this post on Zulip Johan Commelin (May 26 2020 at 14:28):

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

view this post on Zulip Johan Commelin (May 26 2020 at 14:28):

So you have to apply the map to get to A

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 26 2020 at 14:40):

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

view this post on Zulip Johan Commelin (May 26 2020 at 14:40):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 26 2020 at 14:44):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Barinder Singh Banwait (May 26 2020 at 14:47):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Scott Morrison (May 26 2020 at 14:51):

The ? is an unknown universe level.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (May 26 2020 at 14:52):

What is the type signature of algebra_map?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip Scott Morrison (May 26 2020 at 14:53):

Or type #print algebra_map before the current theorem.

view this post on Zulip Johan Commelin (May 26 2020 at 14:53):

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

view this post on Zulip Johan Commelin (May 26 2020 at 14:53):

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

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 26 2020 at 14:59):

If you try #print hello_world you will be disappointed

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 26 2020 at 15:01):

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

view this post on Zulip Johan Commelin (May 26 2020 at 15:01):

For the relative version, your definition seems perfect.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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 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)

view this post on Zulip Johan Commelin (May 26 2020 at 16:47):

@Barinder Singh Banwait I think fraction_map is exactly that.

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 26 2020 at 19:08):

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

view this post on Zulip Johan Commelin (May 26 2020 at 19:09):

Silly me. Now it should be fixed.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 26 2020 at 19:34):

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

view this post on Zulip 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))

view this post on Zulip Patrick Massot (May 26 2020 at 19:41):

This is from the perfectoid project, right?

view this post on Zulip Kevin Buzzard (May 26 2020 at 19:43):

Right, it's in for_mathlib

view this post on Zulip Johan Commelin (May 26 2020 at 19:47):

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

view this post on Zulip Bhavik Mehta (May 26 2020 at 20:14):

You know you really should PR things to mathlib :P

view this post on Zulip Patrick Massot (May 26 2020 at 20:14):

Yes we know

view this post on Zulip Patrick Massot (May 26 2020 at 20:14):

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

view this post on Zulip 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!

view this post on Zulip Bhavik Mehta (May 26 2020 at 20:25):

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

view this post on Zulip Kevin Buzzard (May 26 2020 at 20:25):

I know :-)

view this post on Zulip Kevin Buzzard (May 26 2020 at 20:26):

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

view this post on Zulip Kevin Buzzard (May 26 2020 at 20:26):

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

view this post on Zulip 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 rnrn1s,,snr^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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 27 2020 at 08:07):

Yup, I also noticed the injectivity thing

view this post on Zulip Johan Commelin (May 27 2020 at 08:07):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 27 2020 at 08:08):

So we switched to injective ring homs

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Barinder Singh Banwait (May 27 2020 at 10:37):

you mean the use tactic will be written differently?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 27 2020 at 10:46):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 27 2020 at 10:47):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 27 2020 at 11:13):

open_locale big_operators

view this post on Zulip Johan Commelin (May 27 2020 at 11:13):

Somewhere near the top of your file

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 27 2020 at 15:58):

What are the imports?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 27 2020 at 16:00):

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

view this post on Zulip 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

view this post on Zulip 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 ...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 27 2020 at 16:02):

Just hover over the function where the error is

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 27 2020 at 16:05):

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

view this post on Zulip Kevin Buzzard (May 27 2020 at 16:05):

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

view this post on Zulip 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"

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 27 2020 at 16:08):

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

view this post on Zulip Kevin Buzzard (May 27 2020 at 16:08):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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` ?

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (May 27 2020 at 16:14):

This lemma is not true though, right?

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 27 2020 at 16:15):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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 RR be an integral domain. Then, \forall fraction fields AA of RR, we have : RR is integrally closed R\Leftrightarrow R is integrally closed in AA.

view this post on Zulip Kevin Buzzard (May 27 2020 at 17:28):

Is faction_map a typeclass?

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 27 2020 at 17:29):

(Then it shouldn't be in square brackets)

view this post on Zulip Kevin Buzzard (May 27 2020 at 17:30):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 !

view this post on Zulip 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 (-;

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 27 2020 at 18:42):

Looks good to me!

view this post on Zulip 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

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

with an0a_n \neq 0. Then rnr^n \in span rn1s,,sn\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 :(

view this post on Zulip Kenny Lau (May 29 2020 at 07:02):

but it's wrong

view this post on Zulip Kenny Lau (May 29 2020 at 07:03):

n=1, 2r+s=0

view this post on Zulip Kenny Lau (May 29 2020 at 07:03):

(r=1, s=-2)

view this post on Zulip Kenny Lau (May 29 2020 at 07:04):

Kenny Lau said:

RR is integrally closed
iff for every r,sRr, s \in R with s0s \ne 0, if (r/s)n+a1(r/s)n1++an=0(r/s)^n + a_1 (r/s)^{n-1} + \cdots + a_n = 0, then r/sRr/s \in R
iff for every r,sRr, s \in R with s0s \ne 0, if rn+a1rn1s++ansn=0r^n + a_1 r^{n-1} s + \cdots + a_n s^n = 0, then srs \mid r

you will notice in my formulation that the coefficient of rnr^n is 11

view this post on Zulip 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 a0=1a_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

view this post on Zulip Kenny Lau (May 29 2020 at 07:10):

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

view this post on Zulip Johan Commelin (May 29 2020 at 07:28):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 29 2020 at 07:50):

  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

view this post on Zulip Johan Commelin (May 29 2020 at 08:11):

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

view this post on Zulip Johan Commelin (May 29 2020 at 08:11):

So I would opt for the finset.insert_erase approach

view this post on Zulip Kenny Lau (May 29 2020 at 08:11):

solvable nat subtraction problems

view this post on Zulip Johan Commelin (May 29 2020 at 08:11):

Solvable finset.insert_erase problem


Last updated: May 13 2021 at 05:21 UTC