mathlib

b686bc24 - feat(algebra/lie_algebra): define Lie subalgebras, morphisms, modules, submodules, quotients (#1835)

feat(algebra/lie_algebra): define Lie subalgebras, morphisms, modules, submodules, quotients (#1835) * feat(algebra/lie_algebra): define Lie subalgebras, morphisms, modules, submodules, quotients * Code review: colons at end of line * Update src/algebra/lie_algebra.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/algebra/lie_algebra.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/algebra/lie_algebra.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Catch up after GH commits from code review * Remove accidentally-included '#lint' * Rename: lie_subalgebra.bracket --> lie_subalgebra.lie_mem * Lie ideals are subalgebras * Add missing doc string * Update src/algebra/lie_algebra.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Allow quotients of lie_modules by lie_submodules (part 1) The missing piece is the construction of a lie_module structure on the quotient by a lie_submodule, i.e.,: `instance lie_quotient_lie_module : lie_module R L N.quotient := ...` I will add this in due course. * Code review: minor fixes * New lie_module approach based on add_action, linear_action * Remove add_action by merging into linear_action. I would prefer to keep add_action, and especially like to keep the feature that linear_action extends has_scalar, but unfortunately this is not possible with the current typeclass resolution algorithm since we should never extend a class with fewer carrier types. * Add missing doc string * Simplify Lie algebra adjoing action definitions * whitespace tweaks * Remove redundant explicit type * Update src/algebra/lie_algebra.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/algebra/lie_algebra.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/algebra/lie_algebra.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/algebra/lie_algebra.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Catch up after rename bracket --> map_lie in morphism * Update src/linear_algebra/linear_action.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/linear_algebra/linear_action.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/linear_algebra/linear_action.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/linear_algebra/linear_action.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/linear_algebra/linear_action.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/linear_algebra/linear_action.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/linear_algebra/linear_action.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/linear_algebra/linear_action.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/linear_algebra/linear_action.lean Co-Authored-By: Johan Commelin <johan@commelin.net> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>