Quotienting by a polynomial

Stream: mathlib4

[Son Ho]

Is there a canonical definition for the quotient ring R[X] / P[X], where R is a ring and P[X] ∈ R[X] is a polynomial?

[Adam Topaz]

You use docs#Ideal.span and take the quotient by that ideal

[Adam Topaz]

Namely:

import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.Data.Polynomial.Basic

variable (R : Type*) [CommRing R] (P : Polynomial R)

#check Polynomial R ⧸ Ideal.span {P}

[Son Ho]

Thanks! (again :) )

[Adam Topaz]

Or if you want some nicer notation:

import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.Data.Polynomial.Basic

open scoped Polynomial

variable (R : Type*) [CommRing R] (P : Polynomial R)

#check R[X] ⧸ Ideal.span {P}

[Adam Topaz]

I don't remember whether we have notation for Ideal.span...

[Eric Rodriguez]

there's notation for docs#Submodule.span, which is defeq IIRC, but sadly it is untypeable... see file#Mathlib/LinearAlgebra/Span at ~l270

[Eric Rodriguez]

In specific, it is supposedly \. according to the top of the file, but that is now the Lean4 dot

[Adam Topaz]

Can we somehow introduce the notations:

1. $\langle f \rangle$ for the ideal generated by an element $f$,
2. $\langle f_1, f_2, f_3, f_4 \rangle$ for the ideal generated by the set $\{f_1,...,f_4\}$ and
3. $\langle S \rangle$ for the ideal generated by a set $S$?

Is Lean4's notation flexible enough for this much overloading?

[Eric Wieser]

We something similar for IntermediateField.adjoin, so could presumably do the same thing

[Adam Topaz]

docs#IntermediateField.adjoin

[Eric Rodriguez]

(just a note - that notation is broken in conjunction with the one for C^infty and such like - I was going to mention this when I had time to work on it but I thought it may be relevant)

[Adam Topaz]

I only see https://github.com/leanprover-community/mathlib4/blob/cdbcc21987465a4a2b7818916888e1dcee620bb2/Mathlib/FieldTheory/Adjoin.lean#L472 for finitely many elements... is there one for sets as well?

[Eric Rodriguez]

(also this should be moved)