Composition through the base change adjunction #
For an R-algebra A, an R-algebra S and an S-algebra map q : S →ₐ[S] T,
AlgHom.liftEquiv identifies R-algebra maps A → S and A → T with S-algebra maps out of
S ⊗[R] A, compatibly with composition by q. So composing with q is bijective on R-algebra
maps out of A if and only if it is bijective on S-algebra maps out of S ⊗[R] A
(AlgHom.restrictScalars_comp_bijective_iff). This reduces lifting problems for algebras over an
arbitrary base R to lifting problems over S itself.
theorem
AlgHom.restrictScalars_comp_bijective_iff
(R : Type u_1)
{S : Type u_2}
{T : Type u_3}
(A : Type u_4)
[CommSemiring R]
[CommSemiring S]
[Semiring T]
[Semiring A]
[Algebra R S]
[Algebra S T]
[Algebra R T]
[IsScalarTower R S T]
[Algebra R A]
(q : S →ₐ[S] T)
:
Composing with an S-algebra map q : S →ₐ[S] T is bijective on R-algebra maps out of A
if and only if it is bijective on S-algebra maps out of the base change S ⊗[R] A.