Definition of a quotient ring

Stream: new members

[RL]

How would you declare/define the ring

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

where p is a prime, in Lean?

[Anne Baanen]

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]

A shorthand is docs#adjoin_root

[Anne Baanen]

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]

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]

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

[Eric Wieser]

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]

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

[Alex J. Best]

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]

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

[Anne Baanen]

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

[Jireh Loreaux]

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]

Also that's a name conflict with docs#closure

[Junyan Xu]

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]

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

[Junyan Xu]

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

[Junyan Xu]

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]

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]

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]

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

[Eric Wieser]

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

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]

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

[Adam Topaz]

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

[RL]

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]

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

[Jireh Loreaux]

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]

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]

Yes, it's #lookup3

[Mario Carneiro]

yeah, there is no autocompletion for keywords right now