Zulip Chat Archive

Stream: Is there code for X?

Topic: Finitely generated algebras, etc

Winston Yin (Jul 15 2021 at 15:14):

What's the best way to define k-algebras generated by, say, 2 elements x and y? What should I use as x and y?

Johan Commelin (Jul 15 2021 at 15:17):

You can add an assumption subalgebra.adjoin {x,y} = \top. (Thanks for the fix, Eric!)

Eric Wieser (Jul 15 2021 at 15:17):

Except subalgebra.span is called docs#algebra.adjoin. We also have docs#submodule.span and docs#monoid.closure as names for the analogous things, so it's always confusing.

Adam Topaz (Jul 15 2021 at 15:18):

You can also ask for a surjective morphism from the free algebra on fin 2 or bool or any other type with two elements

Adam Topaz (Jul 15 2021 at 15:18):

We probably don't have the equivalence between these two approaches, but that would be a nice PR

Eric Wieser (Jul 15 2021 at 15:19):

You might even want an alg_equiv to free_algebra R (fin 2) depending on what you mean by 2 elements

Winston Yin (Jul 15 2021 at 15:20):

fin 2 is what I needed, thanks! In cases where x and y come from something else, I will use alg_equiv. Thanks!

Winston Yin (Jul 15 2021 at 15:21):

I'm not sure I understood the algebra.adjoin approach from Johan

Adam Topaz (Jul 15 2021 at 15:21):

alg_equiv with the free algebra is too strong if you just want something generated by two elements

Riccardo Brasca (Jul 15 2021 at 15:23):

You can also work with mv_polynomial, as in docs#algebra.finite_type.iff_quotient_mv_polynomial and friends

Adam Topaz (Jul 15 2021 at 15:24):

I'm assuming algebras need not be commutative in this case? If so, then polynomials aren't a good choice

Eric Wieser (Jul 15 2021 at 15:24):

Johan's approach lets you specify the generators more directly as x y : X, as opposed to using F (free_algebra.ι R X 0) and F (free_algebra.ι R X 1) (where F is the morphism Adam describes)

Riccardo Brasca (Jul 15 2021 at 15:24):

Ah yes, I was thinking about the commutative case.

Eric Wieser (Jul 15 2021 at 15:25):

Everyone always does!

Kevin Buzzard (Jul 15 2021 at 15:28):

A lot of the mathematicians here read research papers where ring := comm_ring

Adam Topaz (Jul 15 2021 at 15:29):

import data.matrix.notation
import algebra.free_algebra

variables (A : Type*) [comm_semiring A] (R : Type*) [semiring R] [algebra A R]

def is_generated_by (x y : R) : Prop := function.surjective (free_algebra.lift A ![x,y])