Commit 2020-01-22 20:10 b686bc24

View on Github →

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