How to define the set of all K-algebraic functions in Lean?

Stream: maths

[Justus Willbad]

I want to do algebra in Lean for formulating some simple new mathematical theorems. But I don't yet know the syntax and commands of Lean.

How can I define variables of the meanings below in Lean?

I'm working at https://live.lean-lang.org.

Until now, I have only
import Mathlib
variable (K : Type*)
without an error comment by Lean.

"variable (K : Type*) [field K]" gives the error comment "invalid binder annotation, type is not a class instance
?m.12"

In the literature, I found: "To define a field extension in Lean, we write:
(F E : Type*) [field F] [field E] [algebra F E]"
But how can I formulate the whole thing in Lean?

the fields $\mathbb{Q}, \mathbb{C}$
a field $\mathbb{K}$
the field $\mathbb{K}(X_1,...,X_n)$
the algebraic closure of $\mathbb{K}(X_1,...,X_n)$
an element of the algebraic closure of $\mathbb{K}(X_1,...,X_n)$
the set of all $\mathbb{K}$-algebraic complex functions
the set of all complex exponential functions with base $e$
the set of all complex logarithm functions with base $e$
the set of all compositions of finite numbers of complex exponential functions with base $e$, complex logarithm functions with base $e$ and/or $\mathbb{K}$-algebraic complex functions
the inverse relation of a function
the set of all branches of a correspondence (multivariate function)
the set of all branches of the inverse relation of a function
a polynomial over $\mathbb{K}$ without a univariate factor over $\mathbb{K}$
a $\mathbb{K}$-algebraic equation

[Ruben Van de Velde]

That's a lot all at once. The real and complex numbers are typed as \R and \C respectively

[Kim Morrison]

@Justus Willbad, how about you post some code showing what point you've got up to. People will be much happier to help you with "the next step" than to try to respond to a giant list. These things are all doable in Lean. :-)

[Adam Topaz]

Mathematically speaking it’s also unclear what you mean by “the field $\mathbb{K}$.”

[Ben Eltschig]

A few things:

• you can wrap your code block in triple-backticks; zulip will then render it as code correctly.
• the field typeclass is called Field, with an uppercase F. Generally, the convention in lean 4 is to start typeclasses like Field with capital letters - the literature you looked at is probably for lean 3.
• when trying to find things in mathlib the mathlib docs, external search tools like moogle.ai and the chat history here on zulip are I think your best bets. You can for example find definitions of algebras and the algebraic closure of a field with those; I don't know of any material on multivariate functions and/or branch cuts though, maybe someone else knows more on that.

[Ben Eltschig]

Also, the reason that variable (K : Type*) [field K] gave you that weird error message is that lean assumed field to be some variable you meant to implicitly introduce, and then failed to make sense of field K. You can disable that behaviour by writing set_option autoImplicit false near the top of your file, then things like field K will give much more sensible error messages like unknown identifier 'field' instead.

[Jz Pan]

Justus Willbad said:

the field K(X1​,...,Xn​)

Unfortunately, we don't have this directly yet, you need to say "the fraction field of K[X1,...,Xn]"

[Justus Willbad]

"Field" instead of "field" works fine.

To build the set of all $\mathbb{Q}$-algebraic functions, I need the set of all polynomials over $\mathbb{Q}$ of arbitrary numbers of variables. How can I get this and how can I define a countably infinite number of variables $X_1,X_2,...$?

[Johan Commelin]

docs#MvPolynomial and use Nat as the type that indexes your variables.

[Justus Willbad]

That was my idea then. But how can I create an indexed variable or generate a set of a countably infinite number of unnamed variables?

[Jz Pan]

Justus Willbad said:

That was my idea. But how can I create an indexed variable?

In Lean, MvPolynomial σ R means R[X_i | i ∈ σ] written in paper. Is this clear?

[Junyan Xu]

The variables are docs#MvPolynomial.X.

[Justus Willbad]

How can I create a variable R that is the fraction field of the set P of the polynomials over the field K?
And how the algebraic closure of R over K?
variable (K : Type*) [Field K]
variable (P : MvPolynomial σ K)

mathlib3 documentation: "is_fraction_ring R K states K is the field of fractions of an integral domain R."
Documentation: "IsFractionRing R K states K is the ring of fractions of a commutative ring R."

variable (P : Type*) [CommRing P] {R : Type*} [CommRing R] [Algebra P R] [IsFractionRing P R]
How can I substitute P?

I think it would help if there is a Lean command IsFractionField.

[Ruben Van de Velde]

Why are you looking at mathlib3 documentation?

[Kevin Buzzard]

docs#FractionRing

[Kevin Buzzard]

That's what you're looking for.

[Yakov Pechersky]

import Mathlib

variable {σ K : Type*} [Field K]
variable {P : MvPolynomial σ K}

local notation "KXYs" => FractionRing (MvPolynomial σ K)

#synth Field (KXYs)
#synth Field (AlgebraicClosure (KXYs))

[Justus Willbad]

I cannot find where the command #synth is described:
https://lean-lang.org/lean4/doc/syntax.html?search=#synth

[Kevin Buzzard]

It just means "check that the typeclass inference system (the square bracket system) can find the instance of the structure". So in the first case it means "check that the system knows that KXYs is a field"

[Kim Morrison]

@Justus Willbad it is described in the Language Reference:

https://lean-lang.org/doc/reference/latest//The-Lean-Language/Type-Classes/#instance-synth