English
For rings R,S with an R-algebra structure on S, the morphism a ↦ algebraMap_R S(a) is epi iff s ⊗ 1 = 1 ⊗ s for all s ∈ S in S ⊗_R S.
Русский
Для колец R,S с алгебралообразной структурой на S гомоморфизм a ↦ algebraMap_R S(a) является эпиморфизмом тогда и только тогда, когда для каждого s ∈ S выполняется s ⊗ 1 = 1 ⊗ s в S ⊗_R S.
LaTeX
$$$Epi(\\mathrm{algebraMap}_{R,S}) \\iff \\forall s:\\, S,\\ s \\otimes_R 1 = 1 \\otimes_R s \\quad\\text{в } S \\otimes_R S$$$
Lean4
theorem epi_iff_tmul_eq_tmul {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] :
Epi (CommRingCat.ofHom (algebraMap R S)) ↔ ∀ s : S, s ⊗ₜ[R] 1 = 1 ⊗ₜ s :=
by
constructor
· intro H
have :=
H.1 (CommRingCat.ofHom <| Algebra.TensorProduct.includeLeftRingHom)
(CommRingCat.ofHom <| (Algebra.TensorProduct.includeRight (R := R) (A := S)).toRingHom)
(by ext r; change algebraMap R S r ⊗ₜ 1 = 1 ⊗ₜ algebraMap R S r;
simp only [Algebra.algebraMap_eq_smul_one, smul_tmul])
exact RingHom.congr_fun (congrArg Hom.hom this)
· refine fun H ↦ ⟨fun {T} f g e ↦ ?_⟩
letI : Algebra R T := (ofHom (algebraMap R S) ≫ g).hom.toAlgebra
let f' : S →ₐ[R] T := ⟨f.hom, RingHom.congr_fun (congrArg Hom.hom e)⟩
let g' : S →ₐ[R] T := ⟨g.hom, fun _ ↦ rfl⟩
ext s
simpa using congr(Algebra.TensorProduct.lift f' g' (fun _ _ ↦ .all _ _) $(H s))
