## Stream: new members

### Topic: Definition of a quotient ring

#### RL (Sep 20 2022 at 04:28):

How would you declare/define the ring

$\mathbb{F}_p[x]/(x^2-2)$

where p is a prime, in Lean?

#### Anne Baanen (Sep 20 2022 at 04:33):

F_p is zmod p (docs#zmod), F_p[x] is (zmod p)[X] (docs#polynomial) and you can quotient a ring by an ideal with the ⧸ operator, so something like:

import data.zmod.basic
import data.polynomial.algebra_map
import ring_theory.ideal.operations

open_locale polynomial -- enable R[X] notation for polynomial X
open polynomial

def R (p : ℕ) : Type* := (zmod p)[X] ⧸ (ideal.span ({X^2 - 2} : set (zmod p)[X]))


#### Thomas Browning (Sep 20 2022 at 04:36):

A shorthand is docs#adjoin_root

#### Anne Baanen (Sep 20 2022 at 04:36):

Yes, I was just about to say that :)

import ring_theory.adjoin_root -- add this to the list of imports

def R' (p : ℕ) : Type* := adjoin_root (X^2 - 2 : (zmod p)[X])


#### Kevin Buzzard (Sep 20 2022 at 07:00):

We have custom notation for lists, vectors, matrices etc: how about custom notation [some bracket] a,b,c [some close bracket] for "ideal generated by a,b,c"? (or left ideal in the non-commutative case)?

#### Eric Wieser (Sep 20 2022 at 08:56):

What makes "ideal generated by" more special than "submodule generated by" or "subring generated by" or "intermediate field generated by" or ...?

#### Eric Wieser (Sep 20 2022 at 08:58):

Would (gen {x, y, z} : ideal R) be an acceptable spelling, where we introduce some has_gen typeclass that works for all subobjects? (Replace gen with the word or symbol of your choice)

#### Riccardo Brasca (Sep 20 2022 at 08:58):

It's probably more commonly used, especially than "subring generated by", but of course there is nothing special about it.

#### Alex J. Best (Sep 20 2022 at 09:31):

It would be nice to have some notation for these things. The fact you have to specify the type of the set in Anne's first message is very annoying

#### Yaël Dillies (Sep 20 2022 at 09:32):

I guess the common thing here is that your gen will be a lower adjoint between some set α and some subobjects of α.

#### Anne Baanen (Sep 20 2022 at 19:30):

Would closure be a good enough name in this case? Should it be defined as a canonical docs#lower_adjoint?

#### Jireh Loreaux (Sep 20 2022 at 19:54):

I don't like closure, as that evokes topology. (e.g., what if you want the topological closure of the ideal generated by a single element?)

#### Jireh Loreaux (Sep 20 2022 at 19:54):

Also that's a name conflict with docs#closure

#### Junyan Xu (Sep 20 2022 at 21:32):

It's already everywhere: docs#subring.closure, docs#submonoid.closure, docs#subfield.closure etc. For submodule/ideal it's called docs#module.span (without the "sub") / ideal.span, and for subalgebra/intermediate_field it's called docs#algebra.adjoin (without "sub") / intermediate_field.adjoin. I think it would be nice to uniformize the terminologies!

By the way I think docs#submodule.closure_neg should be renamed span_neg and the original docs#submodule.span_neg should be removed (it requires ring rather than semiring).

#### Eric Wieser (Sep 20 2022 at 21:54):

We could maybe call it algebra.closure or set_like.closure to disambiguate from topology?

#### Junyan Xu (Sep 20 2022 at 22:03):

There's the generic bundled docs#closure_operator but apparently not used very often

#### Junyan Xu (Sep 20 2022 at 22:06):

Hmm that's actually from set to set. Seems that lower_adjoint is the thing that takes a set to an algebraic structure? It's indeed intuitive that closure takes something to a bigger thing of the same type.

#### Jireh Loreaux (Sep 20 2022 at 23:05):

Personally, I've always used "generate", or some form of that word, for these constructions. Ultimately I don't care too much though.

#### Thomas Browning (Sep 20 2022 at 23:28):

You can't define closure for an arbitrary set_like, since you need to know that the set-theoretic intersection remains a subobject. But you might be able to have a unified definition subobject_like.closure.

#### Anne Baanen (Sep 21 2022 at 05:29):

(Small correction, docs#submodule.span, not module.span)

#### Eric Wieser (Sep 21 2022 at 08:44):

@Thomas Browning, my thinking was to put it in the namespace anyway even if it doesn't hold for all subobjects. That's consistent with what I did with docs#set_like.one_mem_graded

#### Jireh Loreaux (Sep 22 2022 at 15:06):

oh, I just realized, there is another point of naming confusion between the algebraic and topological closures in mathlib: docs#ideal.closure is the topological closure.

#### Adam Topaz (Sep 22 2022 at 15:08):

I haven't really followed the discussion above, but it's worth mentioning that we have docs#closure_operator

#### Adam Topaz (Sep 22 2022 at 15:09):

(which is satisfied by docs#closure although I couldn't find that fact in mathlib)

#### RL (Aug 15 2023 at 10:29):

RL said:

How would you declare/define the ring

$\mathbb{F}_p[x]/(x^2-2)$

where p is a prime, in Lean?

Can I ask the same question using Lean 4?
Thank you.

#### Pedro Sánchez Terraf (Aug 15 2023 at 11:36):

It seems the corresponding construction in Lean4 is docs#AdjoinRoot.

#### Jireh Loreaux (Aug 15 2023 at 12:41):

Note that in Lean 4 you can query where Lean 3 declarations were mapped during the porting process using the #lookup command.

#### Pedro Sánchez Terraf (Sep 01 2023 at 19:58):

Jireh Loreaux said:

Note that in Lean 4 you can query where Lean 3 declarations were mapped during the porting process using the #lookup command.

It should be #lookup3, isn't it? I was a long time trying to make it work and I could not figure out why it didn't.
Btw, the prefix without the 3 does not trigger any auto-completion (at least on the version I'm working on right now).

#### Patrick Massot (Sep 01 2023 at 20:28):

Yes, it's #lookup3

#### Mario Carneiro (Sep 01 2023 at 20:30):

yeah, there is no autocompletion for keywords right now

Last updated: Dec 20 2023 at 11:08 UTC