Commit 2022-04-21 15:20 91cbe460

View on Github →

feat(algebra/monoid_algebra/basic): lifts of (add_)monoid_algebras (#13382) We show that homomorphisms of the grading (add) monoids of (add) monoid algebras lift to ring/algebra homs of the algebras themselves. This PR is preparation for introducing Laurent polynomials (see adomani_laurent_polynomials, file data/polynomial/laurent for a preliminary version). Zulip

Estimated changes

Modified src/algebra/monoid_algebra/basic.lean

added def add_monoid_algebra.map_domain_alg_hom

added theorem add_monoid_algebra.map_domain_algebra_map

added def add_monoid_algebra.map_domain_non_unital_alg_hom

added def add_monoid_algebra.map_domain_ring_hom

added def monoid_algebra.map_domain_alg_hom

added theorem monoid_algebra.map_domain_algebra_map

added def monoid_algebra.map_domain_non_unital_alg_hom

added def monoid_algebra.map_domain_ring_hom

modified theorem monoid_algebra.ring_hom_ext'

modified theorem monoid_algebra.ring_hom_ext

modified def monoid_algebra.single_one_ring_hom