English
If there exists a divisibility condition h: ∀ x ∈ S, ∃ r,s ∈ R with s a unit and f(s) x = f(r), then f is surjective on stalks.
Русский
Если существует условие делимости, что всякий элемент x ∈ S можно выразить как f(r) делённого на неприводимый элемент, тогда f сюръективно на стэках.
LaTeX
$$$\\exists\\, h: (\\forall x \\in S, \\exists r,s\\in R, IsUnit(f(s)) \\land f(s) \\cdot x = f(r)) \\Rightarrow f.SurjectiveOnStalks$$$
Lean4
/-- If `R → T` is surjective on stalks, and `J` is some prime of `T`,
then every element `x` in `S ⊗[R] T` satisfies `(1 ⊗ r • t) * x = a ⊗ t` for some
`r : R`, `a : S`, and `t : T` such that `r • t ∉ J`.
-/
theorem exists_mul_eq_tmul (hf₂ : (algebraMap R T).SurjectiveOnStalks) (x : S ⊗[R] T) (J : Ideal T) (hJ : J.IsPrime) :
∃ (t : T) (r : R) (a : S), (r • t ∉ J) ∧ (1 : S) ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t := by
induction x with
| zero => exact ⟨1, 1, 0, by rw [one_smul]; exact J.primeCompl.one_mem, by rw [mul_zero, TensorProduct.zero_tmul]⟩
| tmul x₁ x₂ =>
obtain ⟨y, s, c, hs, hc, e⟩ := (surjective_localRingHom_iff _).mp (hf₂ J hJ) x₂
simp_rw [Algebra.smul_def]
refine ⟨c, s, y • x₁, J.primeCompl.mul_mem hc hs, ?_⟩
rw [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_comm _ c, e, TensorProduct.smul_tmul, Algebra.smul_def,
mul_comm]
| add x₁ x₂ hx₁ hx₂ =>
obtain ⟨t₁, r₁, a₁, hr₁, e₁⟩ := hx₁
obtain ⟨t₂, r₂, a₂, hr₂, e₂⟩ := hx₂
have : (r₁ * r₂) • (t₁ * t₂) = (r₁ • t₁) * (r₂ • t₂) := by simp_rw [← smul_eq_mul]; rw [smul_smul_smul_comm]
refine ⟨t₁ * t₂, r₁ * r₂, r₂ • a₁ + r₁ • a₂, this.symm ▸ J.primeCompl.mul_mem hr₁ hr₂, ?_⟩
rw [this, ← one_mul (1 : S), ← Algebra.TensorProduct.tmul_mul_tmul, mul_add, mul_comm (_ ⊗ₜ _), mul_assoc, e₁,
Algebra.TensorProduct.tmul_mul_tmul, one_mul, smul_mul_assoc, ← TensorProduct.smul_tmul, mul_comm (_ ⊗ₜ _),
mul_assoc, e₂, Algebra.TensorProduct.tmul_mul_tmul, one_mul, smul_mul_assoc, ← TensorProduct.smul_tmul,
TensorProduct.add_tmul, mul_comm t₁ t₂]
