English
The diagonal morphism for Spec maps satisfies a specific equality: the diagonal of Spec.map(algebraMap) equals the composition of Spec.map(lmul') with the inverse of the pullback isomorphism.
Русский
Диагональ для отображений Spec удовлетворяет конкретному равенству: диагональ Spec.map(algebraMap) равна композиции Spec.map(lmul') с обратной стороны изоморфизма обратной диаграммы.
LaTeX
$$$$\\text{pullback.diagonal}(\\mathrm{Spec.map}(\\mathrm{CommRingCat.ofHom}(\\mathrm{algebraMap}\,R\\,S))) = \\mathrm{Spec.map}(\\mathrm{CommRingCat.ofHom}(\\mathrm{Algebra.TensorProduct.lmul'}\\,R : S \\otimes[R] S \\to_{R} S).\\mathrm{toRingHom}) \\; \\ggg \\; (\\mathrm{pullbackSpecIso}\\,R\\,S\\,S)^{-1}$$$$
Lean4
theorem diagonal_Spec_map :
pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap R S))) =
Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S).toRingHom) ≫
(pullbackSpecIso R S S).inv :=
by
ext1 <;>
simp only [pullback.diagonal_fst, pullback.diagonal_snd, ← Spec.map_comp, ← Spec.map_id, AlgHom.toRingHom_eq_coe,
Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd]
· congr 1; ext x; change x = Algebra.TensorProduct.lmul' R (S := S) (x ⊗ₜ[R] 1); simp
· congr 1; ext x; change x = Algebra.TensorProduct.lmul' R (S := S) (1 ⊗ₜ[R] x); simp
