## Stream: maths

### Topic: definition of integrally closed

#### 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:R\to S$ is an injective map of rings (all rings are commutative here) then we say "$R$ is integrally closed in $S$" (but really it's just a predicate on $f$) if every $s\in S$ which is a root of a monic polynomial in $R[X]$ is in fact in $R$. 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: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 $R\to Frac(R)$ is integrally closed, or we could ask whether every injective ring hom $R\to A$ is integrally closed, where $A$ satisfies the predicate for being the field of fractions of $R$. Note of course that $\mathbb{Z}\to\mathbb{Q}$ satisfies the predicate, but $\mathbb{Q}$ is not equal to the field of fractions of $\mathbb{Z}$ (it's just canonically isomorphic to it). So we have three possibilities for the definition:

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

Because all these maps are isomorphic in the category of $R$-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 ?

#### 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) := ...


#### 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 $R$, so :point_up: what Scott said

#### Reid Barton (May 30 2020 at 10:00):

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

#### Scott Morrison (May 30 2020 at 10:00):

(I was just starting to say the same!)

#### Scott Morrison (May 30 2020 at 10:00):

You could define integrally_closed as a function on under R.

#### Scott Morrison (May 30 2020 at 10:01):

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

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

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

#### Scott Morrison (May 30 2020 at 10:03):

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

#### Scott Morrison (May 30 2020 at 10:04):

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

#### 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

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

#### Kevin Buzzard (May 30 2020 at 10:14):

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

#### Reid Barton (May 30 2020 at 10:16):

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

• $\mathbb{Z}[x, y] \to \mathbb{Z}[z]$--this says that any two elements of $R$ which become the same in $S$ are equal in $R$, i.e., $R \to S$ injective
• for each $d \ge 0$, $\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) := a_0 + a_1 t + \cdots + a_{d-1} t^{d-1} + t^d$ with coefficients in $R$ has a root in $S$, then that root already belongs to $R$

#### 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

#### 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?

#### Reid Barton (May 30 2020 at 10:19):

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

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

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

#### 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

#### Reid Barton (May 30 2020 at 10:32):

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

#### Reid Barton (May 30 2020 at 10:33):

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

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

#### 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?

#### Reid Barton (May 30 2020 at 12:18):

what I had in mind was to use unique_choice instead

#### 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

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

#### 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?

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

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

#### Reid Barton (May 30 2020 at 16:47):

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

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

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

#### 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

#### 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"?

#### Johan Commelin (May 30 2020 at 16:55):

Yup, a clever tactic should just figure it out itself

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

#### Johan Commelin (May 31 2020 at 12:06):

@Scott Morrison What's the definition of hygienic?

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


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

#### 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

#### Scott Morrison (May 31 2020 at 12:10):

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

#### Scott Morrison (May 31 2020 at 12:10):

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

#### Johan Commelin (May 31 2020 at 12:11):

Sounds fantastic!

#### Reid Barton (May 31 2020 at 12:40):

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

#### Reid Barton (May 31 2020 at 12:40):

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

#### Scott Morrison (May 31 2020 at 12:42):

as I said, baby steps :-)

#### Kenny Lau (May 31 2020 at 13:13):

how many seconds does it take?

306ms?

#### 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