definition of integrally closed

Stream: maths

[Kevin Buzzard]

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]

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]

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]

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

[Scott Morrison]

(I was just starting to say the same!)

[Scott Morrison]

You could define integrally_closed as a function on under R.

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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

[Kevin Buzzard]

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]

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]

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

[Reid Barton]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Reid Barton]

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]

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]

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]

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

[Reid Barton]

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

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

[Reid Barton]

what I had in mind was to use unique_choice instead

[Reid Barton]

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]

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

[Barinder Singh Banwait]

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]

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

[Reid Barton]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Barinder Singh Banwait]

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

Yup, a clever tactic should just figure it out itself

[Scott Morrison]

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]

@Scott Morrison What's the definition of hygienic?

[Scott Morrison]

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]

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]

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]

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

[Scott Morrison]

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

[Johan Commelin]

Sounds fantastic!

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

as I said, baby steps :-)

[Kenny Lau]

how many seconds does it take?

[Scott Morrison]

306ms?

[Johan Commelin]

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