Follow-ups from `free_algebra`, `exterior_algebra`, `tensor_algebra`, `clifford_algebra`, `universal_enveloping_algebra`

[Vierkantor]

In the later PRs (#4297, #4430) for this series of definitions, I had suggestions that would apply equally to the previous files in the series (#4077, #4079, #4041). These should be fixed in one PR across 5 files:

ι_comp_lift: shouldn't this be lift_comp_ι to match the order of the symbols?

• [ ] free_algebra.ι_comp_lift
• [ ] exterior_algebra.ι_comp_lift
• [ ] tensor_algebra.ι_comp_lift
• [ ] clifford_algebra.ι_comp_lift
• [ ] universal_enveloping_algebra.ι_comp_lift

lift_unique: What do you think about adding a simp lemma turning (ring_quot.mk_alg_hom R (rel R M)) ((foo_algebra.ι R) x into ι R x, so that we can delete the last refl?

• [ ] exterior_algebra.lift_unique
• [ ] tensor_algebra.lift_unique
• [ ] clifford_algebra.lift_unique
• [ ] universal_enveloping_algebra.lift_unique

There is a lot of rw ← lift_unique, can this become its own lemma, and/or consolidate it with lift_comp_ι?

• [ ] free_algebra.lean
• [ ] exterior_algebra.lean
• [ ] tensor_algebra.lean
• [ ] clifford_algebra.lean

hom_ext is not optimal as an @[ext] lemma, it should be @[ext] lemma hom_ext' : f.to_linear_map (ι R x) = g.to_linear_map (ι R x) → f = g

• [ ] free_algebra.hom_ext
• [ ] exterior_algebra.hom_ext
• [ ] tensor_algebra.hom_ext
• [ ] clifford_algebra.hom_ext
• [ ] universal_enveloping_algebra.hom_ext

lift's docstring is a long sentence, how about "If f : M →ₗ[R] A satisfies cond : ∀ m : M, f m * f m = Q m, it factors as lift Q f cond \circ ι Q. In other words, lift Q f cond is the canonical lift of f : : M →ₗ[R] A to clifford_algebra Q →ₐ[R] A."

• [ ] free_algebra.lift (not too bad because there is no cond)
• [ ] exterior_algebra.lift
• [ ] tensor_algebra.lift (not too bad because there is no cond)
• [ ] clifford_algebra.lift

Since lift_ι_apply is essentially lift_comp_ι without the ext, wouldn't it be nicer if lift_ι_apply was defined first and ι_comp_lift := by { ext, apply lift_ι_apply }?

• [ ] free_algebra
• [ ] exterior_algebra
• [ ] tensor_algebra
• [ ] clifford_algebra

comp_ι_square_zero and comp_ι_square_scalar don't really match the statement:

• [ ] exterior_algebra.comp_ι_square_zero: how about apply_ι_square_eq?
• [ ] clifford_algebra.comp_ι_square_scalar: how about apply_ι_square_eq?

[eric-wieser]

cc @adamtopaz (tensor_algebra) and @semorrison (free_algebra) also.

https://github.com/leanprover-community/mathlib/blob/master/src/algebra/lie/universal_enveloping.lean is likely also subject to many of these suggestions, cc @ocfnash. I've edited the issue to include these too.

[eric-wieser]

hom_ext is not optimal as an @[ext] lemma, it should be @[ext] lemma hom_ext' : f.to_linear_map (ι R x) = g.to_linear_map (ι R x) → f = g

This goes against the direction in #5200, which chooses these .comp lemmas so that a different ext lemma can be appended.