Zulip Chat Archive

Stream: maths

Topic: definition of integrally closed


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

I think that one way of making progress in UG/MSc algebra and number theory would be to get a bunch of definitions down, and then asking people to prove the theorems. One thing I realised from reading the integrally closed domain thread is that there is more than one definition of an integrally closed domain, and I am wondering whether automation is currently up to the task of proving that they're the same.

There is a relative notion of integrally closed (i.e. a predicate on morphisms), and the definition doesn't matter but here it is for completeness : if f:RSf:R\to S is an injective map of rings (all rings are commutative here) then we say "RR is integrally closed in SS" (but really it's just a predicate on ff) if every sSs\in S which is a root of a monic polynomial in R[X]R[X] is in fact in RR. It's just some predicate on injective ring homs, is the main point.

The absolute notion (a predicate on objects) is this: a mathematician would say that an integral domain is integrally closed if it's integrally closed in its field of fractions, i.e. if the map f:RFrac(R)f:R\to Frac(R) is integrally closed in the sense above. But because the field of fractions of an integral domain should properly be thought of as only being defined up to unique isomorphism, we now have two absolute definitions of integrally closed: we could ask whether the map RFrac(R)R\to Frac(R) is integrally closed, or we could ask whether every injective ring hom RAR\to A is integrally closed, where AA satisfies the predicate for being the field of fractions of RR. Note of course that ZQ\mathbb{Z}\to\mathbb{Q} satisfies the predicate, but Q\mathbb{Q} is not equal to the field of fractions of Z\mathbb{Z} (it's just canonically isomorphic to it). So we have three possibilities for the definition:

1) RFrac(R)R\to Frac(R) is integrally closed;
2) There exists a field of fractions AA of RR such that RAR\to A is integrally closed;
3) For all fields of fractions AA of RR, the map RAR\to A is integrally closed.

Because all these maps are isomorphic in the category of RR-algebras, and the relative notion is isomorphism-invariant, all these definitions are logically equivalent. But right now there are people trying to formalise statements about integrally closed rings, and we need the proofs that these are equivalent. Can this be done by automation yet? @Scott Morrison ?

view this post on Zulip Scott Morrison (May 30 2020 at 09:57):

So I think the question here is:

lemma integrally_closed_invariant {R S T : Ring} (f : R  S) (φ : S  T) :
  integrally_closed f  integrally_closed (f  φ.hom) := ...

view this post on Zulip Reid Barton (May 30 2020 at 09:58):

I assume you're not expecting automation (or at least not the same automation) to prove that any two fraction fields are isomorphic under RR, so :point_up: what Scott said

view this post on Zulip Reid Barton (May 30 2020 at 10:00):

You could even write it as an isomorphism in under R, if that helps somehow.

view this post on Zulip Scott Morrison (May 30 2020 at 10:00):

(I was just starting to say the same!)

view this post on Zulip Scott Morrison (May 30 2020 at 10:00):

You could define integrally_closed as a function on under R.

view this post on Zulip Scott Morrison (May 30 2020 at 10:01):

And then check that it is functorial with respect to isomorphisms in under R

view this post on Zulip Scott Morrison (May 30 2020 at 10:02):

Since it is a function under R -> Prop, "functorial with respect to isomorphisms" just means it takes isomorphisms in under R (i.e. isomorphisms from S to S', making the triangle commute) to "if and only if" in Prop.

view this post on Zulip Scott Morrison (May 30 2020 at 10:02):

Automatically proving that something is functorial w.r.t. isomorphisms is exactly the direction that the equiv_rw and transport PRs from earlier this year were aiming.

view this post on Zulip Scott Morrison (May 30 2020 at 10:03):

but I haven't been working on them. :-(

view this post on Zulip Scott Morrison (May 30 2020 at 10:04):

But we can dream: @[derive hygienic] def integrally_closed ... := ...

view this post on Zulip Kevin Buzzard (May 30 2020 at 10:05):

We will already have the theorem that two fraction fields are isomorphic, that will be part of the characteristic predicate of localisation story

view this post on Zulip Reid Barton (May 30 2020 at 10:13):

By the way, it seems that integrally_closed f is just a bunch of lifting conditions, so Scott's lemma follows by general nonsense (integral extensions form a subcategory containing all isomorphisms).

view this post on Zulip Kevin Buzzard (May 30 2020 at 10:14):

It says that any sSs\in S satisfying one condition, satisfies another condition.

view this post on Zulip Reid Barton (May 30 2020 at 10:16):

You can express "RSR \to S an integral extension" as the (automatically unique) right lifting property with respect to the maps

  • Z[x,y]Z[z]\mathbb{Z}[x, y] \to \mathbb{Z}[z]--this says that any two elements of RR which become the same in SS are equal in RR, i.e., RSR \to S injective
  • for each d0d \ge 0, Z[a0,a1,,ad1]Z[a0,a1,,ad1,r]/(a0+a1r++ad1rd1+rd)\mathbb{Z}[a_0, a_1, \ldots, a_{d-1}] \to \mathbb{Z}[a_0, a_1, \ldots, a_{d-1}, r]/(a_0 + a_1 r + \cdots + a_{d-1} r^{d-1} + r^d)--this says that if a polynomial P(t):=a0+a1t++ad1td1+tdP(t) := a_0 + a_1 t + \cdots + a_{d-1} t^{d-1} + t^d with coefficients in RR has a root in SS, then that root already belongs to RR

view this post on Zulip Reid Barton (May 30 2020 at 10:17):

Then, RLP(any class of maps) always contains all isomorphisms, is a subcategory, is closed under pullbacks and retracts

view this post on Zulip Kevin Buzzard (May 30 2020 at 10:19):

Do we really have to train regular mathematicians who read Atiyah-Macdonald and are completely happy with the concept of being integrally closed and are oblivious to all this nonsense about stuff only being defined up to unique isomorphism, to think in this way?

view this post on Zulip Reid Barton (May 30 2020 at 10:19):

No, you just need automation that doesn't exist yet

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

@Barinder Singh Banwait you have stumbled across something which was perhaps more subtle than I had realised.

view this post on Zulip Reid Barton (May 30 2020 at 10:30):

The automation really has to do a lot of work though (which is not to say it is necessarily complicated, just that it solves a large problem). The ring R[X]R[X] isn't changing across the isomorphism, which helps, but presumably the definition of integrally closed uses something like polynomial.eval\2, and the automation needs to know that eval\2-ing a polynomial along a map that differs from another by an isomorphism results in values related by that isomorphism

view this post on Zulip Reid Barton (May 30 2020 at 10:31):

Presumably it's going to prove this by structural induction on the definition of eval\2, but if there is choice somewhere inside eval\2, which doesn't seem inconceivable to me, then it will get stuck there

view this post on Zulip Reid Barton (May 30 2020 at 10:32):

If you wanted to prove "RR integrally closed implies an isomorphic ring RR' integrally closed" then you would also have to understand the isomorphism R[X]R[X]R[X] \cong R'[X]

view this post on Zulip Reid Barton (May 30 2020 at 10:33):

while that's somehow free with the reformulation I gave, because "R[X]R[X]" disappeared

view this post on Zulip Reid Barton (May 30 2020 at 10:37):

(In derived algebraic geometry this point of view is important, because you can't just reason with elements and this funny notion called "equality".)

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

If there is choice inside eval\2 then presumably one just proves the lemma by hand and then...tags it with hygienic?

view this post on Zulip Reid Barton (May 30 2020 at 12:18):

what I had in mind was to use unique_choice instead

view this post on Zulip Reid Barton (May 30 2020 at 12:20):

I guess this doesn't need an added constant, unique_choice can just be defined in terms of choice and then hooked up to the automation manually

view this post on Zulip Reid Barton (May 30 2020 at 12:23):

Or maybe even not manually, since I guess you can tell by looking at its type that unique_choice is "hygienic"

view this post on Zulip Barinder Singh Banwait (May 30 2020 at 16:46):

wow, there's a lot here that i don't understand. i was thinking this would be a good toy project to get my feet wet with, looks like i've inadvertently found myself at the deep end. i'll still try to proceed on the proof of the lemmas stated over on the #new members > Integrally closed domain channel as best i can though ...

I couldn't find this 'unique_choice' in the lean docs or searching in the codebase, is that something being developed on another mathlib branch or the next Lean release?

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

@Barinder Singh Banwait I think you can ignore most of this

view this post on Zulip Reid Barton (May 30 2020 at 16:47):

It's just an imaginary version of choice with a subsingleton hypothesis.

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

Kevin is asking whether a computer could come up with a proof itself.

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

But if you just want to prove your "fundamental theorem" then most of this discussion doesn't apply

view this post on Zulip Barinder Singh Banwait (May 30 2020 at 16:52):

@Reid Barton @Johan Commelin oh right, thanks for clarifying. by "come up with a proof itself", that would be analogous to how ring or linarith just "go forth and try to prove the goal"?

view this post on Zulip Johan Commelin (May 30 2020 at 16:55):

Yup, a clever tactic should just figure it out itself

view this post on Zulip Scott Morrison (May 31 2020 at 11:55):

Baby steps towards hygiene! I have a branch now where

@[derive hygienic]
def zero_ring (R : Ring) : Prop := (0 : R) = (1 : R)

successfully produces an instance of hygienic zero_ring, using a derive handler that knows nothing at all about rings.

view this post on Zulip Johan Commelin (May 31 2020 at 12:06):

@Scott Morrison What's the definition of hygienic?

view this post on Zulip Scott Morrison (May 31 2020 at 12:06):

variables {C : Type u} [category.{v} C]

class hygienic (p : C  Prop) : Prop :=
(map : Π {X Y : C}, (X  Y)  (p X  p Y))

view this post on Zulip Scott Morrison (May 31 2020 at 12:07):

I also introduced

variables {C : Type (u+1)} [large_category C] [concrete_category C]

class canonical (x : Π (Y : C), (Y : Type u)) :=
(iso_apply :  {Y Y' : C} (φ : Y  Y'), (φ.hom : Y  Y') (x Y) = x Y')

and there is some automatic derivation magic happening for instances of this simultaneously.

view this post on Zulip Scott Morrison (May 31 2020 at 12:09):

canonical says we have a family consisting of a chosen element in the underlying type for each object in some concrete category, and arbitrary isomorphisms carry chosen elements to chosen elements

view this post on Zulip Scott Morrison (May 31 2020 at 12:10):

So in particular we can easily deduce canonical (λ (R : Ring), 0).

view this post on Zulip Scott Morrison (May 31 2020 at 12:10):

and after that it's pretty easy to put the pieces together

view this post on Zulip Johan Commelin (May 31 2020 at 12:11):

Sounds fantastic!

view this post on Zulip Reid Barton (May 31 2020 at 12:40):

Does this approach really work for higher-order things like topological_space, or for fintype, etc.?

view this post on Zulip Reid Barton (May 31 2020 at 12:40):

It seems like you will need an infinite number of these canonical classes

view this post on Zulip Scott Morrison (May 31 2020 at 12:42):

as I said, baby steps :-)

view this post on Zulip Kenny Lau (May 31 2020 at 13:13):

how many seconds does it take?

view this post on Zulip Scott Morrison (Jun 01 2020 at 02:47):

306ms?

view this post on Zulip Johan Commelin (Jun 01 2020 at 02:54):

I don't think speed matter here. If it's slowish, it's just an extra argument for getting the extra-file "certificates + support code" working


Last updated: May 11 2021 at 15:12 UTC