Commit 2026-01-22 10:30 2389810a

feat: RingHom.adjoinAlgebraMap (#33016) Consider a tower of rings A / B / C and b : B, then there is a natural map from A[b] to A[algebraMap B C b] (adjoin b viewed as an element of C). This PR adds 3 versions, depending on whether we use Algebra.adjoin or IntermediateField.adjoin:

• Algebra.RingHom.adjoinAlgebraMap : Algebra.adjoin A {b} →+* Algebra.adjoin A {(algebraMap B C) b}
• IntermediateField.RingHom.adjoinAlgebraMapOfAlgebra : Algebra.adjoin A {b} →+* A⟮((algebraMap B C) b)⟯
• IntermediateField.RingHom.adjoinAlgebraMap : A⟮b⟯ →+* A⟮((algebraMap B C) b)⟯ Note: We create a new file for Algebra.RingHom.adjoinAlgebraMap, which is intended for results about adjoining singletons, because it is convenient to import Algebra.Adjoin.Polynomial.