[Merged by Bors] - feat(algebra/universal_enveloping_algebra): construction of universal enveloping algebra and its universal property

[ocfnash]

Main definitions

• universal_enveloping_algebra
• universal_enveloping_algebra.algebra
• universal_enveloping_algebra.lift
• universal_enveloping_algebra.ι_comp_lift
• universal_enveloping_algebra.lift_unique
• universal_enveloping_algebra.hom_ext

[ocfnash]

If this is merged, it might be worth a follow-up PR grouping some of the Lie algebra theory into its own folder. E.g., something along the lines of:

• algebra/lie_algebra.lean --> algebra/lie/basic.lean [this could also be broken down into more files]
• algebra/classical_lie_algebras.lean --> algebra/lie/classical.lean
• algebra/universal_enveloping_algebra.lean --> algebra/lie/universal_enveloping.lean

[semorrison]

Could we have an @[ext] lemma, stating that to show that two algebra maps out of the enveloping algebra are equal, it suffices to show the precompositions with the inclusion are equal?

(Perhaps tensor_algebra needs this as well!)

[ocfnash]

Could we have an @[ext] lemma, stating that to show that two algebra maps out of the enveloping algebra are equal, it suffices to show the precompositions with the inclusion are equal?

(Perhaps tensor_algebra needs this as well!)

Agreed! I'm afraid I'm heading away on holiday and will have phone-only internet access for the next week. I tried to squeeze your worthy suggestions in this morning but have run out of time. I got this far:

@[ext] lemma hom_ext {g₁ g₂ : universal_enveloping_algebra R L →ₐ[R] A}
  (h : ∀ x, g₁ (ι R L x) = g₂ (ι R L x)) : g₁ = g₂ :=
begin
  let f₁ := (lie_algebra.of_associative_algebra_hom g₁).comp (ι R L),
  let f₂ := (lie_algebra.of_associative_algebra_hom g₂).comp (ι R L),
  have h' : f₁ = f₂, by { sorry, }, -- Should be: ext x, exact (h x),
  have h₁ : g₁ = lift R L A f₁, { apply lift_unique, refl, },
  have h₂ : g₂ = lift R L A f₂, { apply lift_unique, refl, },
  rw [h₁, h₂, h'],
end

To my embarrassment, extensionality for Lie algebra morphisms is missing! Assuming nobody else finishes this, I'll take this up in a week when I get back.

[semorrison]

Because ext will chain together @[ext] lemmas, it's also fine to state the hypothesis as an equation of functions, rather than quantifying over the argument.

[semorrison]

Hopefully extensionality for Lie algebra morphisms is just a matter of putting @[ext] on the relevant structure?

[semorrison]

In the meantime, looking again at tensor_algebra, I decided it was best to factor out the constructions of free algebras, and noncommutative quotients.

We should have a look at #4079, and rewrite this PR based on that model. I'm happy to help/do it at some point, but I'll leave this with you for now.

[ocfnash]

In the meantime, looking again at tensor_algebra, I decided it was best to factor out the constructions of free algebras, and noncommutative quotients.

We should have a look at #4079, and rewrite this PR based on that model. I'm happy to help/do it at some point, but I'll leave this with you for now.

I’m writing this on a phone while away but I will gratefully refactor along the lines you suggest when I get back on Sunday. Perhaps by then the points raised by @adamtopaz on Zulip will have been settled.

[adamtopaz]

(Perhaps tensor_algebra needs this as well!)

The tensor_algebra has this already :) Although it's not tagged with @[ext].

mathlib/src/linear_algebra/tensor_algebra.lean

Line 266 in 2ab31f9

theorem hom_ext {A : Type*} [semiring A] [algebra R A] {f g : tensor_algebra R M →ₐ[R] A} :

I think the same sort of proof, using lift_unique should work in this case as well.

[ocfnash]

As noted above, we want to refactor this to use ring_quot introduced in the second of this trio of PRs:

• [Merged by Bors] - feat(algebra/free_algebra): free (noncommutative) algebras #4077
• [Merged by Bors] - feat(algebra/ring_quot): quotients of noncommutative rings #4078
• [Merged by Bors] - refactor(linear_algebra/tensor_algebra): build as a quotient of a free algebra #4079

I'm happy to do any of:

1. refactor now (rebasing to branch off the branch in [Merged by Bors] - refactor(linear_algebra/tensor_algebra): build as a quotient of a free algebra #4079, probably), or
2. wait till the above trio land, or
3. merge this as-is, and follow up to refactor.

though option 1 is probably my least favourite given that being the fourth link in a chain of dependent PRs might mean quite a bit of rebasing etc.

[semorrison]

If you don't object to waiting, I think option 2. is fine. In the meantime, if you want to add some review comments on that trio, and/discuss on zulip, that might move things along. :-)

[semorrison]

@ocfnash, that stack of PRs has now hit master, so I've un-marked this PR as "blocked". Let me know if you want any help with it!

[ocfnash]

@ocfnash, that stack of PRs has now hit master, so I've un-marked this PR as "blocked". Let me know if you want any help with it!

Excellent thanks. I feel a bit guilty at not helping with the review. I'll have some time this afternoon and will update this PR. I think I shouldn't need help but I will keep the offer in mind :-)

[ocfnash]

I'm not 100% sure I like the approach I've just put in place, but I've warmed up to it sufficiently that I feel it's worth asking for opinion(s) in review.

I've decided I like this approach.

I'd also like to dig into the typeclass inference issues that I was whining about on Zulip.

[semorrison]

Looks great. Just some minor nitpicks on the comments.

bors d+

[bors]

✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

Can we wait for #4252 before merging?

[ocfnash]

Can we wait for #4252 before merging?

Absolutely. I'll wait for that to land, merge in what it brings to this branch, drop my then-redundant algebra.as_ring, and then finally merge this.

[ocfnash]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests