Commit 2023-08-23 11:25 34d86d99

feat(RingTheory/FiniteType): generalize some results to non-commutative rings (#6681) I was hoping to use this in combination with #6680 to show the TensorAlgebra is finitely generated, where I needed to generalize FiniteType.equiv; but it turns out that the FiniteType instance on MonoidAlgebra also isn't generalized! The summary here is:

• Move Algebra.adjoin_algebraMap from Mathlib/RingTheory/Adjoin/Tower.lean to Mathlib/RingTheory/Adjoin/Basic.lean and golf the proof to oblivion
• Provide an alternative statement of adjoin_union_eq_adjoin_adjoin, adjoin_algebraMap_image_union_eq_adjoin_adjoin, which works in non-commutative rings, and use it along with a new adjoin_top lemma to prove Algebra.fg_trans' more generally.
• Introduce a new S variable throughout, with the convention that R and S are commutative, A and B remain not-necessarily-commutative, and A/S/R is a tower of algebras.
• Apply some zero-effort generalizations to semirings.