# Zulip Chat Archive

## Stream: maths

### Topic: subrings

#### Johan Commelin (Jun 07 2018 at 06:54):

/-- `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 (Jun 07 2018 at 06:55):

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 (Jun 07 2018 at 07:08):

Ok, the easy way out: I'll extend `is_submonoid`

. Even though it feels "unmathematical" to me.

#### Kevin Buzzard (Jun 07 2018 at 08:32):

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 (Jun 07 2018 at 09:22):

I think it would be best if we could extend both `is_submonoid`

and `is_add_subgroup`

.

#### Scott Morrison (Jun 07 2018 at 10:39):

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 (Jun 07 2018 at 10:40):

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 (Jun 07 2018 at 10:40):

(Of course actually redundant things should be lemmas.)

#### Johan Commelin (Jun 07 2018 at 15:22):

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

#### Johan Commelin (Jun 07 2018 at 15:22):

Here is a small start on subrings

#### Johan Commelin (Jun 08 2018 at 06:47):

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

#### Johan Commelin (Jun 08 2018 at 06:47):

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

#### Johan Commelin (Jun 08 2018 at 06:48):

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

#### Kevin Buzzard (Jun 08 2018 at 06:51):

I think lots of people did univariate polynomials

#### Kevin Buzzard (Jun 08 2018 at 06:51):

but I don't know if anyone submitted a PR

#### Kevin Buzzard (Jun 08 2018 at 06:51):

I think Kenny proved a universal property

#### Kevin Buzzard (Jun 08 2018 at 06:52):

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

#### Kevin Buzzard (Jun 08 2018 at 06:53):

@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 (Jun 08 2018 at 06:53):

Yes, that is what I am currently trying to do

#### Kevin Buzzard (Jun 08 2018 at 06:53):

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

#### Kevin Buzzard (Jun 08 2018 at 06:53):

but I am not sure this result is needed

#### Kevin Buzzard (Jun 08 2018 at 06:53):

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

#### Kevin Buzzard (Jun 08 2018 at 06:54):

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

#### Johan Commelin (Jun 08 2018 at 06:54):

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

#### Johan Commelin (Jun 08 2018 at 06:54):

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

#### Johannes Hölzl (Jun 08 2018 at 08:58):

@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 (Jun 08 2018 at 10:59):

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

#### Johan Commelin (Jun 08 2018 at 11:21):

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

#### Johan Commelin (Jun 08 2018 at 11:34):

Current proposal:

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

#### Kevin Buzzard (Jun 08 2018 at 13:32):

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

#### Johannes Hölzl (Jun 08 2018 at 13:40):

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 (Jun 08 2018 at 13:41):

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 (Jun 08 2018 at 13:41):

And that doesn't make sense.

#### Johan Commelin (Jun 08 2018 at 13:41):

But maybe I'm missing something.

#### Kevin Buzzard (Jun 08 2018 at 13:58):

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

#### Kevin Buzzard (Jun 08 2018 at 13:58):

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 (Jun 08 2018 at 13:58):

why not?

#### Kevin Buzzard (Jun 08 2018 at 13:58):

it's the same math/CS thing

#### Kevin Buzzard (Jun 08 2018 at 13:58):

it's just like dividing by zero

#### Mario Carneiro (Jun 08 2018 at 13:58):

Is that even a CS thing?

#### Kevin Buzzard (Jun 08 2018 at 13:58):

yes

#### Kevin Buzzard (Jun 08 2018 at 13:59):

nobody divides by zero except CS people

#### Kevin Buzzard (Jun 08 2018 at 13:59):

oh

#### Kevin Buzzard (Jun 08 2018 at 13:59):

maybe applied mathematicians do

#### Kevin Buzzard (Jun 08 2018 at 13:59):

no not even them

#### Mario Carneiro (Jun 08 2018 at 13:59):

where's the division by zero

#### Kevin Buzzard (Jun 08 2018 at 13:59):

they only do 0 / 0

#### Kevin Buzzard (Jun 08 2018 at 13:59):

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

#### Kevin Buzzard (Jun 08 2018 at 13:59):

when nobody in their right mind would do this

#### Mario Carneiro (Jun 08 2018 at 13:59):

presumably this is exactly what is meant by I^n

#### Kevin Buzzard (Jun 08 2018 at 13:59):

Exactly

#### Mario Carneiro (Jun 08 2018 at 14:00):

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

#### Kevin Buzzard (Jun 08 2018 at 14:00):

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

#### Kevin Buzzard (Jun 08 2018 at 14:00):

Yes, well-defined and kind-of pointless

#### Mario Carneiro (Jun 08 2018 at 14:00):

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

#### Kevin Buzzard (Jun 08 2018 at 14:00):

so we don't think of it

#### Kevin Buzzard (Jun 08 2018 at 14:00):

exactly

#### Kevin Buzzard (Jun 08 2018 at 14:00):

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

#### Mario Carneiro (Jun 08 2018 at 14:00):

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

#### Kevin Buzzard (Jun 08 2018 at 14:00):

This is just another instance of this canonical disconnect

#### Kevin Buzzard (Jun 08 2018 at 14:01):

we only define things where we need them

#### Kevin Buzzard (Jun 08 2018 at 14:01):

you over-define and sift later

#### Kevin Buzzard (Jun 08 2018 at 14:01):

it's just cultural

#### Mario Carneiro (Jun 08 2018 at 14:01):

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

#### Mario Carneiro (Jun 08 2018 at 14:02):

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

#### Johan Commelin (Jun 08 2018 at 14:02):

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

#### Mario Carneiro (Jun 08 2018 at 14:03):

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

#### Mario Carneiro (Jun 08 2018 at 14:03):

you can still define I^n that way

#### Johan Commelin (Jun 08 2018 at 14:04):

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) sorry, I meant `span { a*b | a \in A, b \in B}`

`span { a*b | a \in span A, b \in span B}`

#### Mario Carneiro (Jun 08 2018 at 14:04):

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

#### Mario Carneiro (Jun 08 2018 at 14:04):

in ring theory you obviously need the second definition

#### Johan Commelin (Jun 08 2018 at 14:04):

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

#### Mario Carneiro (Jun 08 2018 at 14:05):

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

?

#### Kenny Lau (Jun 08 2018 at 14:05):

yes

#### Johan Commelin (Jun 08 2018 at 14:06):

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 (Jun 08 2018 at 14:06):

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 (Jun 08 2018 at 14:07):

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 (Jun 08 2018 at 14:08):

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

...

#### Mario Carneiro (Jun 08 2018 at 14:09):

One problem with doing this generally is that `-A`

is taken in sets

#### Johan Commelin (Jun 08 2018 at 14:10):

Hmm, there is no semiring structure actually. Because `neg A`

is `span (-A)`

, and so `neg neg A \ne A`

.

#### Johan Commelin (Jun 08 2018 at 14:11):

Unless `A`

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

#### Johan Commelin (Jun 08 2018 at 14:12):

I think the nice thing to do is to define a class `ideals R`

, just as with `opens X`

.

#### Johan Commelin (Jun 08 2018 at 14:12):

And then put the nice structure on `ideals R`

.

#### Mario Carneiro (Jun 08 2018 at 14:12):

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

#### Mario Carneiro (Jun 08 2018 at 14:13):

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

#### Mario Carneiro (Jun 08 2018 at 14:13):

but the distributive law fails I think

#### Johan Commelin (Jun 08 2018 at 14:13):

Aah, you are right of course

#### Mario Carneiro (Jun 08 2018 at 14:14):

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

, `{1, 2}*{1} + {1,2}*{1} = {2,3,4}`

#### Johan Commelin (Jun 08 2018 at 14:15):

No, your counterexample fails. Both sides are `R`

.

#### Johan Commelin (Jun 08 2018 at 14:16):

And in fact, I think you get a semiring.

#### Johan Commelin (Jun 08 2018 at 14:16):

The output of `+`

and `*`

is always an ideal.

#### Johan Commelin (Jun 08 2018 at 14:17):

`A + B`

is defined as `span (span A +' span B)`

, where `+'`

is the stupid element-wise addition.

#### Johan Commelin (Jun 08 2018 at 14:17):

Analogously for `*`

.

#### Johan Commelin (Jun 08 2018 at 14:18):

(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 `span`

s.)

#### Mario Carneiro (Jun 08 2018 at 14:21):

I think `span (A +' B)`

should suffice?

#### Mario Carneiro (Jun 08 2018 at 14:22):

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

#### Johan Commelin (Jun 08 2018 at 14:23):

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

#### Johan Commelin (Jun 08 2018 at 14:23):

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

#### Johan Commelin (Jun 08 2018 at 14:23):

So we tweak our definition, and throw in some extra `span`

s.

#### Mario Carneiro (Jun 08 2018 at 14:26):

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

#### Mario Carneiro (Jun 08 2018 at 14:27):

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

#### Johan Commelin (Jun 08 2018 at 14:33):

Take `A = R`

, `B = {1}`

and `C = {-1}`

. Then LHS = 0 while RHS = R.

#### Reid Barton (Jun 08 2018 at 16:34):

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 (Jun 08 2018 at 16:49):

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 (Jun 08 2018 at 16:51):

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

?

#### Johan Commelin (Jun 08 2018 at 16:51):

So all the `is_open`

s, `is_ideal`

s and `is_subring`

s get gathered into classes `opens`

, `ideals`

, and `subrings`

. But things like rings and groups shouldn't...

#### Reid Barton (Jun 08 2018 at 16:53):

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 (Jun 08 2018 at 16:53):

`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 (Jun 08 2018 at 16:55):

Right

#### Johan Commelin (Jun 08 2018 at 16:57):

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

#### Johan Commelin (Jun 08 2018 at 16:59):

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 (Jun 08 2018 at 17:00):

And I couldn't just easily prove stuff.

#### Johan Commelin (Jun 08 2018 at 17:00):

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

#### Ashvni Narayanan (Aug 01 2020 at 00:29):

```
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 (Aug 01 2020 at 00:33):

Try turning on `set_option pp.all true`

?

#### Ashvni Narayanan (Aug 01 2020 at 00:44):

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 (Aug 01 2020 at 00:52):

Is `coe_set_range`

in mathlib?

#### Reid Barton (Aug 01 2020 at 00:52):

It looks like a universe issue

#### Reid Barton (Aug 01 2020 at 00:52):

`@ring_hom.{0 u}`

versus `@ring_hom.{?l_1 ?l_1}`

#### Ashvni Narayanan (Aug 01 2020 at 00:52):

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 (Aug 01 2020 at 01:04):

Reid Barton said:

Is

`coe_set_range`

in mathlib?

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

#### Reid Barton (Aug 01 2020 at 01:18):

I would assume the `variables`

are set up in a way that causes this universe issue.

#### Ashvni Narayanan (Aug 01 2020 at 01:23):

Changing

```
variable {R : Type u} [ring R]
```

to

```
variable {R : Type*} [ring R]
```

solved it, thank you!

#### Ashvni Narayanan (Aug 04 2020 at 15:47):

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 (Aug 04 2020 at 15:51):

Is it because `has_neg`

should be `has_neg.neg`

?

#### Adam Topaz (Aug 04 2020 at 15:52):

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 (Aug 04 2020 at 15:53):

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

#### Adam Topaz (Aug 04 2020 at 16:17):

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

#### Adam Topaz (Aug 04 2020 at 16:18):

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

?

#### Kevin Buzzard (Aug 04 2020 at 16:30):

`(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 (Aug 04 2020 at 16:31):

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

#### Adam Topaz (Aug 04 2020 at 16:33):

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 (Aug 04 2020 at 21:57):

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 (Aug 04 2020 at 21:57):

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

#### Kevin Buzzard (Aug 04 2020 at 21:58):

That should certainly work. What are you doing though?

#### Ashvni Narayanan (Aug 04 2020 at 22:01):

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 (Aug 04 2020 at 22:02):

Then your suggestion looks perfect!

#### Kevin Buzzard (Aug 04 2020 at 22:02):

Because -1 is in your ring

#### Kevin Buzzard (Aug 04 2020 at 22:03):

The lemma as it stands without allowing -1 is false

#### Reid Barton (Aug 04 2020 at 22:03):

Yeah I'm confused

#### Ashvni Narayanan (Aug 04 2020 at 22:04):

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

#### Reid Barton (Aug 04 2020 at 22:05):

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 (Aug 04 2020 at 22:07):

oh `mem_closure_iff_exists_list`

also already exists, so now I'm doubly confused

#### Reid Barton (Aug 04 2020 at 22:07):

You're trying to prove `mem_closure_iff_exists_list`

even though mathlib already has a proof?

#### Kevin Buzzard (Aug 04 2020 at 22:09):

We're bundling subrings. It existed for `is_subring`

.

#### Ashvni Narayanan (Aug 04 2020 at 22:12):

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 (Aug 04 2020 at 22:14):

I see

Last updated: May 06 2021 at 17:38 UTC