subrings

Stream: maths

[Johan Commelin]

/-- `S` is a subgroup: a set containing 1 and closed under multiplication, addition and and additive inverse. -/
class is_subring  (S : set R) : Prop := -- would like `extends is_add_subgroup`, but that class doesn't exist
(one_mem       : (1 : R) ∈ S)
(mul_mem {x y} : x ∈ S → y ∈ S → x * y ∈ S)
(add_mem {x y} : x ∈ S → y ∈ S → x + y ∈ S)
(inv_mem {x}   : x ∈ S → -x ∈ S)

instance subtype.ring {S : set R} [is_subring S] : ring S := sorry

[Johan Commelin]

I think the route of defining is_add_subgroup will pay off in the end. Is this again one of those things where [to_additive] should help? The last time I tried that, it didn't work.

[Johan Commelin]

Ok, the easy way out: I'll extend is_submonoid. Even though it feels "unmathematical" to me.

[Kevin Buzzard]

A minimalist definition of subgroup is : non-empty and closed under lam x y,xy^{-1}. Is there any point using this minimalist definition? You could do the same with add_mem and inv_mem here. Does this save time or obfuscate? Or both?

[Johan Commelin]

I think it would be best if we could extend both is_submonoid and is_add_subgroup.

[Scott Morrison]

Regarding minimalist definitions (x * y^{-1}), I think it is best if the official definition is the bog standard definition, with no clever tricks or surprises. It's fine to then provide an alternative constructor which allows you to take advantage of shortcuts like this if you want them.

[Scott Morrison]

Until the constructions become seriously dire, I think it's best to optimise definitions to be usable (after you've constructed instances), rather than easy to satisfy.

[Scott Morrison]

(Of course actually redundant things should be lemmas.)

[Johan Commelin]

https://github.com/jcommelin/lean-perfectoid-spaces/tree/subring/src/for_mathlib

[Johan Commelin]

Here is a small start on subrings

[Johan Commelin]

Update: https://github.com/jcommelin/lean-perfectoid-spaces/blob/subring/src/for_mathlib/subring.lean

[Johan Commelin]

@Kevin Buzzard what do you think is the best strategy for integral elements?

[Johan Commelin]

Were univariate polynomials already there? Somewhere? Did Chris or Nicholas do this?

[Kevin Buzzard]

I think lots of people did univariate polynomials

[Kevin Buzzard]

but I don't know if anyone submitted a PR

[Kevin Buzzard]

I think Kenny proved a universal property

[Kevin Buzzard]

@Chris Hughes @Kenny Lau @Johannes Hölzl Did any of you PR a definition of a polynomial in 1 variable into mathlib?

[Kevin Buzzard]

@Johan Commelin Note that for the definition of a perfectoid space it might be the case that one only has to formalise the definition, i.e. "I am a root of a monic poly with coefficients in the smaller ring"

[Johan Commelin]

Yes, that is what I am currently trying to do

[Kevin Buzzard]

To prove integral closure is a ring will involve some Noetherian arguments

[Kevin Buzzard]

but I am not sure this result is needed

[Kevin Buzzard]

We need "I am a subring of R^o"

[Kevin Buzzard]

but I am not sure we need "...and by the way R^o is a ring"

[Johan Commelin]

Right, we never take the closure (-; We only have stuff that already is a subring, and then prove it is closed

[Johan Commelin]

Oooh, what you are saying is different from what I was saying...

[Johannes Hölzl]

@Kevin Buzzard There are no univariate polynomials in mathlib or in a PR. I want to move the polynomials from Mason-Stother proof in July / August.

[Chris Hughes]

I will do that once I've done my project.

[Johan Commelin]

What is the best way to define the n-th power of an ideal?

[Johan Commelin]

Current proposal:

span {i | ∃ x : multiset I, x.card = n ∧ i = (x.map subtype.val).prod}

[Kevin Buzzard]

I think Kenny did product of ideals so you could just define them recursively

[Johannes Hölzl]

Are Kenny's ideals a subtype parameterised by the ring? I guess they form a monoid? Then you could just write I ^ n?

[Johan Commelin]

But I has type set R. And there is some instance hanging around telling you that it is an ideal. So now Lean wants have_pow (set R) nat.

[Johan Commelin]

And that doesn't make sense.

[Johan Commelin]

But maybe I'm missing something.

[Kevin Buzzard]

It doesn't make sense to a mathematician -- that's what you're missing.

[Kevin Buzzard]

I think the idea in CS is that you just define I*J for I and J sets to be the ideal generated by the ij

[Mario Carneiro]

why not?

[Kevin Buzzard]

it's the same math/CS thing

[Kevin Buzzard]

it's just like dividing by zero

[Mario Carneiro]

Is that even a CS thing?

[Kevin Buzzard]

yes

[Kevin Buzzard]

nobody divides by zero except CS people

[Kevin Buzzard]

oh

[Kevin Buzzard]

maybe applied mathematicians do

[Kevin Buzzard]

no not even them

[Mario Carneiro]

where's the division by zero

[Kevin Buzzard]

they only do 0 / 0

[Kevin Buzzard]

the "division by zero" is when you multiply two sets that are not ideals together

[Kevin Buzzard]

when nobody in their right mind would do this

[Mario Carneiro]

presumably this is exactly what is meant by I^n

[Kevin Buzzard]

Exactly

[Mario Carneiro]

The notion A*B for A,B sets is well defined even if they are not ideals

[Kevin Buzzard]

It's just a different way of thinking about things. I know exactly why Johan is confused.

[Kevin Buzzard]

Yes, well-defined and kind-of pointless

[Mario Carneiro]

but if you want to restrict to ideals, it makes no difference

[Kevin Buzzard]

so we don't think of it

[Kevin Buzzard]

exactly

[Kevin Buzzard]

and then whenever you apply it, you are probably carrying around a proof that things are ideals

[Mario Carneiro]

not at all pointless, the notation is not limited to ring theory

[Kevin Buzzard]

This is just another instance of this canonical disconnect

[Kevin Buzzard]

we only define things where we need them

[Kevin Buzzard]

you over-define and sift later

[Kevin Buzzard]

it's just cultural

[Mario Carneiro]

I'm certain I've seen A - B and A + B and other things as well with weirder sets than ideals

[Mario Carneiro]

i.e. "prove C + C = [0, 2] where C is the cantor set"

[Johan Commelin]

0/0 is also well-defined. It is 57.

[Mario Carneiro]

but I'm not even stressing this domain of definition, define it on ideals if you want

[Mario Carneiro]

you can still define I^n that way

[Johan Commelin]

And A * B for A B : set R has two definitions that make sense. (1) { a*b | a \in A, b \in B} or (2) span { a*b | a \in A, b \in B} sorry, I meant span { a*b | a \in span A, b \in span B}

[Mario Carneiro]

since I^(n+1) = I^n * I and I^0 = B and these are both ideals

[Mario Carneiro]

in ring theory you obviously need the second definition

[Johan Commelin]

I would say that (1) is more natural. But for ideals you want (2)

[Mario Carneiro]

A question: using the set definition, is span (I*I*I) = span (span (I*I) * I)?

[Kenny Lau]

yes

[Johan Commelin]

Anyway, Kevin, here is https://github.com/jcommelin/lean-perfectoid-spaces/tree/subring with is_integrally_closed up to some sorrys in mason-stother.

[Kenny Lau]

A subset B is trivial, to see that B subset A, suffices to show that span(I*I)*I subset I*I*I, and then it follows from distributivity

[Mario Carneiro]

Here's another CS-ism: instead of dealing with ideals, generalize to all sets by implicitly taking the span when you need to

[Johan Commelin]

Ok, so we put a semiring structure on set R...

[Mario Carneiro]

One problem with doing this generally is that -A is taken in sets

[Johan Commelin]

Hmm, there is no semiring structure actually. Because neg A is span (-A), and so neg neg A \ne A.

[Johan Commelin]

Unless A is an ideal... but that is a very crazy assumption. (-;

[Johan Commelin]

I think the nice thing to do is to define a class ideals R, just as with opens X.

[Johan Commelin]

And then put the nice structure on ideals R.

[Mario Carneiro]

actually if you only want a semiring you don't need neg

[Mario Carneiro]

I don't think you have to worry about any cancellation

[Mario Carneiro]

but the distributive law fails I think

[Johan Commelin]

Aah, you are right of course

[Mario Carneiro]

{1, 2}*({1} + {1}) = {2, 4}, {1, 2}*{1} + {1,2}*{1} = {2,3,4}

[Johan Commelin]

No, your counterexample fails. Both sides are R.

[Johan Commelin]

And in fact, I think you get a semiring.

[Johan Commelin]

The output of + and * is always an ideal.

[Johan Commelin]

A + B is defined as span (span A +' span B), where +' is the stupid element-wise addition.

[Johan Commelin]

Analogously for *.

[Johan Commelin]

(I agree that my initial definition was wrong. But I had not learnt your CS-ism back then. So I didn't put in enough spans.)

[Mario Carneiro]

I think span (A +' B) should suffice?

[Mario Carneiro]

My observation is that elementwise addition is non-distributive (although it is associative and commutative if the underlying op is)

[Johan Commelin]

Right, but you want that multiplication and addition of ideals is distributive.

[Johan Commelin]

That is a fact that will someday be in mathlib, I hope.

[Johan Commelin]

So we tweak our definition, and throw in some extra spans.

[Mario Carneiro]

You don't need the extra spans though, the span in the upgraded addition is sufficient to fix the issues

[Mario Carneiro]

span (A *' span (B +' C)) = span (span (A *' B) +' span (A *' C))

[Johan Commelin]

Take A = R, B = {1} and C = {-1}. Then LHS = 0 while RHS = R.

[Reid Barton]

The main point here is that you should be writing (I : ideal R), not (I : set R) (h : is_ideal I) or whatever.

[Johan Commelin]

So why do we still write (R : Type) [ring R]? Shouldn't we write R : Ring and G : Group or something like that?

[Johan Commelin]

Or does the difference have to do with whether your class is a Prop?

[Johan Commelin]

So all the is_opens, is_ideals and is_subrings get gathered into classes opens, ideals, and subrings. But things like rings and groups shouldn't...

[Reid Barton]

I think in many cases you should also be writing R : Ring etc. Particularly in settings where the only thing you know about R is that it is a ring.

[Reid Barton]

R : Ring might be less convenient when dealing with specific objects. For examples, the real numbers are a ring but they are also a topological space, etc.

[Johan Commelin]

Right

[Johan Commelin]

@Reid Barton I think Mario said something along the lines that type inference and coercions don't work together.

[Johan Commelin]

So, suppose you have the following statement instance {R : Type} [ring R] (S: subrings R) : ring S. If you then want to prove instance {R : Type} [comm_ring R] (S: subrings R) : comm_ring S I think you run in to trouble, because now Lean needs to turn S into a Type and also infer that it is a ring.

[Johan Commelin]

And I couldn't just easily prove stuff.

[Johan Commelin]

(I don't have Lean here atm... so I can't reproduce the exact problem I ran into.

[Ashvni Narayanan]

lemma coe_bot : ((⊥ : subring R) : set R) = set.range (coe : ℤ → R) := (int.cast_ring_hom R).coe_set_range

Here, ⊥ is defined to be

instance : has_bot (subring R) := ⟨(int.cast_ring_hom R).set_range⟩

The proof of the above lemma gives the error :

type mismatch at application
  (int.cast_ring_hom R).coe_set_range
term
  int.cast_ring_hom R
has type
  ℤ →+* R : Type u
but is expected to have type
  ?m_1 →+* ?m_2 : Type ?
Additional information:
c:\Users\ashvn\my_project\DVR\src\bundled_subrings_working.lean: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch at application
    (int.cast_ring_hom R).coe_set_range
  term
    int.cast_ring_hom R
  has type
    ℤ →+* R : Type u
  but is expected to have type
    ?m_1 →+* ?m_2 : Type ?

The lemma coe_set_range says:

@[simp] lemma coe_set_range : (f.set_range : set S) = set.range f := set.image_univ

I don't see why there is a type mismatch error occurs, since both \Z and R are rings. I also don't understand the long error.

[Reid Barton]

Try turning on set_option pp.all true?

[Ashvni Narayanan]

Gives the error:

type mismatch at application
  @ring_hom.coe_set_range.{?l_1} ?m_2 ?m_3 ?m_4 ?m_5 (@int.cast_ring_hom.{u} R _inst_1)
term
  @int.cast_ring_hom.{u} R _inst_1
has type
  @ring_hom.{0 u} int R int.semiring (@ring.to_semiring.{u} R _inst_1) : Type u
but is expected to have type
  @ring_hom.{?l_1 ?l_1} ?m_2 ?m_3 (@ring.to_semiring.{?l_1} ?m_2 ?m_4) (@ring.to_semiring.{?l_1} ?m_3 ?m_5) : Type ?l_1
Additional information:
c:\Users\ashvn\my_project\DVR\src\bundled_subrings_working.lean: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch at application
    @ring_hom.coe_set_range.{?l_1} ?m_2 ?m_3 ?m_4 ?m_5 (@int.cast_ring_hom.{u} R _inst_1)
  term
    @int.cast_ring_hom.{u} R _inst_1
  has type
    @ring_hom.{0 u} int R int.semiring (@ring.to_semiring.{u} R _inst_1) : Type u
  but is expected to have type
    @ring_hom.{?l_1 ?l_1} ?m_2 ?m_3 (@ring.to_semiring.{?l_1} ?m_2 ?m_4)
      (@ring.to_semiring.{?l_1} ?m_3 ?m_5) : Type ?l_1

It seems to me that the problem is that we have int.semiring instead of int.to_semiring?

[Reid Barton]

Is coe_set_range in mathlib?

[Reid Barton]

It looks like a universe issue

[Reid Barton]

@ring_hom.{0 u} versus @ring_hom.{?l_1 ?l_1}

[Ashvni Narayanan]

Actually, this is just a copy of

lemma coe_bot : ((⊥ : subsemiring R) : set R) = set.range (coe : ℕ → R) :=
(nat.cast_ring_hom R).coe_srange

for subrings, so this works for \N, but not for \Z (as a subring)

[Ashvni Narayanan]

Reid Barton said:

Is coe_set_range in mathlib?

No, the lemma I want to use is defined in the file.

[Reid Barton]

I would assume the variables are set up in a way that causes this universe issue.

[Ashvni Narayanan]

Changing

variable {R : Type u} [ring R]

to

variable {R : Type*} [ring R]

solved it, thank you!

[Ashvni Narayanan]

I have a ring R, and a list L : list(list R)) . I want to define a list M : list(list R)) such that

(list.map list.prod M).sum = - (list.map list.prod L).sum

I think this definition should do it :

    let M := list.map (list.map (has_neg )) L,

however, this gives an error

type mismatch at application
  list.map (list.map has_neg) L
term
  L
has type
  list (list R) : Type u_1
but is expected to have type
  list (list (Type ?)) : Type (?+1)

Any help is appreciated, thank you!

[Adam Topaz]

Is it because has_neg should be has_neg.neg?

[Adam Topaz]

Also, I don't think this would work, since the product of [-1,-2] is not the negative of the product of [1,2].

[Adam Topaz]

But it's possible I'm misunderstanding what you're trying to do here...

[Adam Topaz]

This is a difficult question, since list.prod evaluates the empty list to 1.

[Adam Topaz]

How you you define this for, say, the following list of lists: [[],[]]?

[Kevin Buzzard]

(list.map list.prod L).sum when evaluated at [[1,2],[3,4]] is ([2,12]).sum which is 14. If you negate everything you still get 14.

[Adam Topaz]

Yeah, so it seems you want to only negate the head of each list, but then the empty lists cause issues.

[Adam Topaz]

I think you want to define a function like this:

import algebra

def helper {α : Type*} [ring α] : list α → list α
| [] := [-1]
| (a :: as) := -a :: as

and map using that.

[Ashvni Narayanan]

I defined

  let M := list.map (λ (b :list R), (list.cons (-1) b)) L,

and it seems to work. I believe it is equivalent to the definition you gave?
Thank you!

[Adam Topaz]

It's a bit different, but it also works.

[Kevin Buzzard]

That should certainly work. What are you doing though?

[Ashvni Narayanan]

I was trying to prove this (got from the subsemiring file) :

lemma mem_closure_iff_exists_list {s : set R} {x} : x ∈ closure s ↔
  ∃ L : list (list R), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (L.map list.prod).sum = x :=

After struggling with the negation case for a while, I found this in the is_subring file :

theorem exists_list_of_mem_closure {s : set R} {x : R} (hx : x ∈ closure s) :
  (∃ L : list (list R), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = (-1:R)) ∧ (L.map list.prod).sum = x) :=

The proof is similar, so I am currently working the proof around.

[Kevin Buzzard]

Then your suggestion looks perfect!

[Kevin Buzzard]

Because -1 is in your ring

[Kevin Buzzard]

The lemma as it stands without allowing -1 is false

[Reid Barton]

Yeah I'm confused

[Ashvni Narayanan]

Yes exactly, I realised that only after trying the negation case for very long

[Reid Barton]

Since exists_list_of_mem_closure already exists, what are you trying to prove? A corresponding statement for semirings? i.e. what is R?

[Reid Barton]

oh mem_closure_iff_exists_list also already exists, so now I'm doubly confused

[Reid Barton]

You're trying to prove mem_closure_iff_exists_list even though mathlib already has a proof?

[Kevin Buzzard]

We're bundling subrings. It existed for is_subring.

[Ashvni Narayanan]

I am trying to adapt exists_list_of_mem_closure for bundled subrings, the definition of closure is somewhat different, and the existing proof breaks, because it uses something from deprecated.subgroups.

[Reid Barton]

I see