English
Given a finite ring extension and an identity s⊗t = t⊗s for tensors, the canonical algebra homomorphism is surjective.
Русский
При конечном расширении кольца и равенстве тензоров вида s⊗t = t⊗sдля всех элементов, каноническое гомоморфизм сюръективен.
LaTeX
$$$\text{RingHom.surjective_of_tmul_eq_tmul_of_finite}$$$
Lean4
theorem surjective_of_tmul_eq_tmul_of_finite {R S} [CommRing R] [Ring S] [Algebra R S] [Module.Finite R S]
(h₁ : ∀ s : S, s ⊗ₜ[R] 1 = 1 ⊗ₜ s) : Function.Surjective (algebraMap R S) :=
by
let R' := LinearMap.range (Algebra.ofId R S).toLinearMap
rcases subsingleton_or_nontrivial (S ⧸ R') with h | _
· rwa [Submodule.subsingleton_quotient_iff_eq_top, LinearMap.range_eq_top] at h
have : Subsingleton ((S ⧸ R') ⊗[R] (S ⧸ R')) :=
by
refine subsingleton_of_forall_eq 0 fun y ↦ ?_
induction y with
| zero => rfl
| add a b e₁ e₂ => rwa [e₁, zero_add]
| tmul x y =>
obtain ⟨x, rfl⟩ := R'.mkQ_surjective x
obtain ⟨y, rfl⟩ := R'.mkQ_surjective y
obtain ⟨s, hs⟩ : ∃ s, 1 ⊗ₜ[R] s = x ⊗ₜ[R] y := by
use x * y
trans x ⊗ₜ 1 * 1 ⊗ₜ y
· simp [h₁]
· simp
have : R'.mkQ 1 = 0 := (Submodule.Quotient.mk_eq_zero R').mpr ⟨1, map_one (algebraMap R S)⟩
rw [← map_tmul R'.mkQ R'.mkQ, ← hs, map_tmul, this, zero_tmul]
cases false_of_nontrivial_of_subsingleton ((S ⧸ R') ⊗[R] (S ⧸ R'))
