English
Let R, P, S be commutative rings with R ⟶ P ⟶ S forming a tower of algebras, with ker(algebraMap P → S) squared equal to zero and algebraMap P S being surjective. Then the composition of the canonical P-algebra homomorphism IsScalarTower.toAlgHom R P S with the section of kerToTensor corresponding to a suitable P-linear retraction l is the identity on S. In other words, the retraction given by the section splits the extension at the level of S.
Русский
Пусть R, P, S — кольца с тождественными отображениями R → P → S, образующие цилиндрическую цепочку алгебр, при этом ker(algebraMap P → S)^2 = 0 и алгебраическая карта P → S сюръективна. Тогда композиция канонического P-алгебраического гомоморфа IsScalarTower.toAlgHom R P S с секцией kerToTensor, соответствующей подходящему P-линейному редекцию l, является тождественным отображением на S. Иными словами, секция в секции разрыва распадается на уровне S.
LaTeX
$$$\\big(\\text{IsScalarTower.toAlgHom } R P S\\big) \\circ \\big(\\text{sectionOfRetractionKerToTensor }(l,\\, hl,\\, hf')\\big) = \\text{AlgHom.id }_S$$$
Lean4
@[simp]
theorem toAlgHom_comp_sectionOfRetractionKerToTensor :
(IsScalarTower.toAlgHom R P S).comp (sectionOfRetractionKerToTensor l hl hf' hf) = AlgHom.id _ _ :=
toAlgHom_comp_sectionOfRetractionKerToTensorAux (hf := hf) ..
