Undergraduate math list (algebras)

Stream: general

[Patrick Massot]

Oliver, the question is whether you can write a def that takes a lie algebra structure and outputs a non_unital_non_assoc_semiring

[Eric Wieser]

Patrick Massot said:

Oliver, the question is whether you can write a def that takes a lie algebra structure and outputs a non_unital_non_assoc_semiring

Should we have bracketive/unbracketive to match multiplicative/additive? One translates between + and *, the other between lie brackets and *.

[Oliver Nash]

Patrick Massot said:

Oliver, the question is whether you can write a def that takes a lie algebra structure and outputs a non_unital_non_assoc_semiring

I see, well we can do this:

import algebra.lie.basic

variables (L : Type* ) [lie_ring L]

def lie_ring.to_non_unital_non_assoc_semiring : non_unital_non_assoc_semiring L :=
{ mul           := has_bracket.bracket,
  left_distrib  := lie_add,
  right_distrib := add_lie,
  zero_mul      := zero_lie,
  mul_zero      := lie_zero,
  .. (by apply_instance : add_comm_group L), }

[Oliver Nash]

And if we had also assumed lie_algebra R L (for a comm_ring R) we could define the relevant is_scalar_tower and smul_comm_class classes.

[Eric Wieser]

Where does the has_scalar R L instance come from?

[Oliver Nash]

From lie_algebra.to_module

[Eric Wieser]

docs#lie_algebra.to_module

[Eric Wieser]

Oh I was getting confused by lie_ring_module which has a different sort of action, never mind

[Oliver Nash]

Oh, but actually you have a point, we need a has_scalar L L.

[Oliver Nash]

Which I guess would come from lie_ring.to_non_unital_non_assoc_semiring via has_mul.to_has_scalar if we set things up right.

[Patrick Massot]

Oh wow, someone took the trouble to sort the conversations in different topics

[Patrick Massot]

What is the conclusion then? Do you have a fully working instance?

[Oliver Nash]

No but I could create one. It would be a type synonym and 3/4 associated instances on it. I can create and PR it if you would like but it is not very likely to be used.

[Oliver Nash]

I'd be more inclined to do it if we "fixed" our algbera class.

[Oliver Nash]

Of course, very easy and won't do any harm.

[Patrick Massot]

I don't think it necessarily needs to be PRed, but clarifying this would be nice

[Patrick Massot]

What do you mean by fixing here?

[Oliver Nash]

Changing its definition so that it does not require the underlying "ring" to be unital and associative.

[Oliver Nash]

There was an old branch where Scott and I made a brief attempt to do this and more recently there is this: https://github.com/leanprover-community/mathlib/commit/dcbed292a23994dfddf70d8262a4defb3103e968#diff-7fa8b94b14c549770d3cddb5a015c4c6029e40e3cd5161d574d9b9f5e7cdff1bR54

[Patrick Massot]

Ok, that's a big refactor.

[Oliver Nash]

Yep

[Oliver Nash]

Patrick Massot said:

I don't think it necessarily needs to be PRed, but clarifying this would be nice

I'll paste a complete version here later today.

[Oliver Nash]

The following is not pretty but I think should illustrate how to do this:

import algebra.lie.basic

def lie_ring.to_has_mul (L : Type*) := L
def forward {L : Type*} : L → lie_ring.to_has_mul L := λ x, x
def back {L : Type*} : lie_ring.to_has_mul L → L := λ x, x

variables {R L : Type*} [comm_ring R] [lie_ring L] [lie_algebra R L]

instance : non_unital_non_assoc_semiring (lie_ring.to_has_mul L) :=
{ mul           := λ x y, forward ⁅back x, back y⁆,
  left_distrib  := lie_add,
  right_distrib := add_lie,
  zero_mul      := zero_lie,
  mul_zero      := lie_zero,
  .. (by apply_instance : add_comm_group L), }

instance : module R (lie_ring.to_has_mul L) :=
@lie_algebra.to_module R L _ _ _

instance : is_scalar_tower R (lie_ring.to_has_mul L) (lie_ring.to_has_mul L) :=
{ smul_assoc := smul_lie, }

lemma lie_smul' (t : R) (x y : L) : t • ⁅x, y⁆ = ⁅x, t • y⁆ := by rw lie_smul

instance : smul_comm_class R (lie_ring.to_has_mul L) (lie_ring.to_has_mul L) :=
{ smul_comm := lie_smul' }

[Oliver Nash]

Tidied up :point_up: slightly. LMK if you want anything else.

[Eric Wieser]

with_mul is probably a better name than to_has_mul.

[Patrick Massot]

It still feels weird that we don't have a plain non_unital_non_associative_algebra R A. People coming to mathlib and asking where are algebras will have a very hard time understanding the answer

[Eric Wieser]

If we do that we face the docs#domain problem, where either:

• Lots of lemmas get stated about domain that don't actually require all of ring, nontrivial, and no_zero_divisors
• No lemmas actually use domain, which means it's not really pedagogically useful

And to make matters worse, typeclass inference can't promote ring R nontrivial R no_zero_divisors R into integral_domain even though they mean the same thing

[Eric Wieser]

I think that last problem goes away in lean4

[Eric Wieser]

I guess we could just define it like docs#vector_space but not use it?

[Eric Wieser]

(i thought we did that for vector_space too but I guess not)

[Johan Commelin]

Patrick Massot said:

It still feels weird that we don't have a plain non_unital_non_associative_algebra R A. People coming to mathlib and asking where are algebras will have a very hard time understanding the answer

Understanding the answer will be just as hard as understanding why we have group and add_group. And just as hard as why we can't use ∘ to denote multiplication in endomorphism rings.

[Patrick Massot]

I disagree, this is not the same order of magnitude.

[Johan Commelin]

Hmm, ok, I agree that such algebras could exist. Do you agree that Lie algebras wouldn't be instances?

[Johan Commelin]

I've never used such algebras, apart from Lie algebras.

[Yury G. Kudryashov]

@Patrick Massot Does the "module R A + is_scalar_tower R A A + smul_comm_class R A A" definition work in this case?

[Yury G. Kudryashov]

If yes, then we can go with branch#redefine-algebra and use very weak typeclass assumptions in the definition.

[Patrick Massot]

Johan, did you intend to write "Lie algebras would be instances"?

[Patrick Massot]

I'm talking about https://en.wikipedia.org/wiki/Non-associative_algebra which does include Lie algebras and mathlib algebras as special cases

[Patrick Massot]

(although wikipedia insists the base ring is a field for some mysterious reason)

[Johan Commelin]

No. I meant "would not".

I think it is more useful that every associative algebra gives a Lie algebra, via the commutator bracket, then the fact that the Lie algebra can be viewed as a non-assoc multiplication.
Having both as instances would give two non-propeq multiplications on every assoc algebra.

[Yury G. Kudryashov]

But we can have a type tag that turns a Lie algebra into a (non-assoc) algebra.

[Yury G. Kudryashov]

Then we restate all facts in terms of Lie brackets.

[Patrick Massot]

Yury, yes I think this collection of type classes work

[Yury G. Kudryashov]

And it is equivalent to the standard definition in case of semiring A.

[Patrick Massot]

Johan, we don't have to have instances of this, I only suggest that people who want to formalize stuff about algebras can find a way to express this without searching Zulip for this thread.

[Yury G. Kudryashov]

@Eric Wieser This :up: is another reason to remove algebra_map from the definition of algebra.

[Patrick Massot]

I certainly don't want our currently supported algebras to become harder to use because of this definition.

[Patrick Massot]

I think we can simply put the definition somewhere and not use it.

[Johan Commelin]

Ok, then I fully agree with you.

[Yury G. Kudryashov]

Earlier, I suggested the same retractor as a way to get rid of some TC diamonds.

[Yury G. Kudryashov]

We only lose some definitional equalities for algebra_map, nothing more.

[Yury G. Kudryashov]

And we can reuse instances about scalar towers in definitions of algebras.

[Yaël Dillies]

Patrick Massot said:

Johan, we don't have to have instances of this, I only suggest that people who want to formalize stuff about algebras can find a way to express this without searching Zulip for this thread.

I think a better solution to this is to curate a note explaining how maths-speak translates to mathlib-speak. Typically, an explanation of how to declare a vector space or an algebra.

[Eric Wieser]

#10221 improves the docstring of algebra a little, which somewhat helps here.

[Kevin Buzzard]

for vector spaces I think we came up with a really nice idea involving either notation or reducible defs, I can't remember, it was something Anne and I talked about months ago and then I never did anything about.

[Kyle Miller]

Would it be possible to make a command to do the canonical variables incantation for you for various objects?

For example, maybe

declare algebra R A
declare vector_space K V

would do

variables [comm_semiring R] [semiring A] [algebra R A]
variables [field K] [add_comm_group V] [module K V]

I am imagining that this wouldn't be worked out automatically, but rather it would be hard-coded. Maybe another command def_declare could create entries in its database, allowing these definitions to be put near relevant classes. Perhaps as a bonus it could add {A : Type*} and so on if these variables aren't already present.

An unsophisticated implementation could be that declare is a parameterized open_locale, doing textual substitution of the arguments.

If this is possible, would it be a good idea? I like how it's not particularly magical (and you can verify its effects with #where and such) and how it doesn't abuse the language (anything nonstandard is localized to the declare line).

[Rob Lewis]

This is definitely doable (with docs#lean.parser.emit_code_here) and would make a nice little project! Working out which classes are needed from e.g. algebra R A should be doable too, at least if all the types involved appear in the target type class.

[Anne Baanen]

I have a patch for Lean lying around somewhere that allows you to write [ring R] [[algebra R A]] [[module R M]], and adds all the missing typeclass dependencies, e.g. [ring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M]. However, adding more locals broke the elaborator terribly and I couldn't figure out a good way to proceed.

[Anne Baanen]

https://github.com/leanprover-community/lean/commit/d17c9e0c67573a35b8319da15b816409e92c160e

[Kyle Miller]

@Anne Baanen Having [[...]] notation for auto-inserting all missing dependencies in binders would be great, too, if that could work, though it doesn't solve vector_space, I think. There could be an attribute for classes (abbreviation_class?) that directs this feature to try to eliminate the class completely. For example

@[abbreviation_class]
def vector_space (K V : Type*) [field K] [add_comm_group V] [module K V]

could define how `[[vector_space K V]] is replaced, though this might be confusing if you forget the double square brackets.

[Anne Baanen]

Also as you can see, where in mathlib we would know to use [add_comm_group M] when R is a ring, the fancy brackets only insert add_comm_monoid.

[Anne Baanen]

Kyle Miller said:

Anne Baanen Having [[...]] notation for auto-inserting all missing dependencies in binders would be great, too, if that could work, though it doesn't solve vector_space, I think. There could be an attribute for classes (abbreviation_class?) that directs this feature to try to eliminate the class completely. For example

@[abbreviation_class]
def vector_space (K V : Type*) [field K] [add_comm_group V] [module K V]

could define how `[[vector_space K V]] is replaced, though this might be confusing if you forget the double square brackets.

Good idea to control the dependencies through an attribute. Maybe we could also setup something like:

class module (R M : Type*) [semiring R] [add_comm_monoid M] := ...

@[dependency (field K) (add_comm_group V)]
abbreviation vector_space (K V : Type*) [semiring K] [add_comm_monoid V] := module K V
-- Don't specialize the typeclass arguments themselves!

[Eric Rodriguez]

this would be super cool!

[Yaël Dillies]

I assume this is then meant for teaching and not mathlib?

[Eric Rodriguez]

I feel like it could be huge for mathlib if you could type more maths-friendly things far more often instead of the typeclass hell you see in things like the statement of FTC

[Anne Baanen]

Anne Baanen said:

I have a patch for Lean lying around somewhere that allows you to write [ring R] [[algebra R A]] [[module R M]], and adds all the missing typeclass dependencies, e.g. [ring R] [semiring A] [algebra R A] [add_comm_monoid M] [module R M]. However, adding more locals broke the elaborator terribly and I couldn't figure out a good way to proceed.

Looking at it again, the precise diagnosis involves lines 796-801 of definition_cmds.cpp:

    bool recover_from_errors = p.m_error_recovery;
    elaborator elab(env, p.get_options(), resolve_decl_name(env, fn), metavar_context(), local_context(), recover_from_errors);
    buffer<expr> new_params;
    elaborate_params(elab, params, new_params);
    elab.freeze_local_instances();
    replace_params(params, new_params, fn, val);

In elaborate_params I added the code to add dependencies for instance arguments, however replace_params can't tell at which points new params were inserted, so it (correctly) trips an error. So a solution would probably start with passing a list of added/deleted indices to replace_params.

[Yaël Dillies]

Eric Rodriguez said:

I feel like it could be huge for mathlib if you could type more maths-friendly things far more often instead of the typeclass hell you see in things like the statement of FTC

Yeah but also the modularity is crucial. During the convexity refacotr, I literally turned a single concrete type $\R$ into around 15 shades of spaces.

[Kyle Miller]

In support of modularity, it can protect code from changes to the algebra hierarchy, since things about a vector_space don't care too much about exactly which intermediate algebraic objects you also need to include. (And there are in fact theorems about vector spaces, I believe. :wink:)

[Anne Baanen]

Anne Baanen said:

So a solution would probably start with passing a list of added/deleted indices to replace_params.

This seems to work, almost! Now the only issue is that we detect the list of missing instances by checking which errors result from elaborating the implicit+deps binder, but the errors seem to bubble up to the surface too(?)

[Anne Baanen]

Now we ignore the "missing instance" errors. What do you all think, is this addition PR-worthy? https://github.com/leanprover-community/lean/compare/implicit-dep-binder

[Eric Rodriguez]

What do the lean4 people think of this in lean4? Not sure who to @