Commit 2023-09-05 10:32 b47296c9

View on Github →

feat(RingTheory/FiniteType): generalize results to non-commutative generators (#6757) Many of the proofs in this file go via quotients of MvPolynomial; but this forces a commutativity assumption that can be avoided by instead going via quotients of FreeAlgebra. Most of the new FreeAlgebra results are just copies of the proofs for MvPolynomial, which isn't ideal in terms of duplication.

Estimated changes

Modified Mathlib/Algebra/FreeAlgebra.lean

added theorem Algebra.adjoin_eq_range_freeAlgebra_lift

added theorem Algebra.adjoin_range_eq_range_freeAlgebra_lift

added theorem FreeAlgebra.adjoin_range_ι

Modified Mathlib/RingTheory/FiniteType.lean

added theorem AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure

modified theorem AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure

added theorem Algebra.FiniteType.iff_quotient_freeAlgebra'

added theorem Algebra.FiniteType.iff_quotient_freeAlgebra

modified theorem MonoidAlgebra.finiteType_iff_group_fg

added theorem MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure

modified theorem MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure