English
If f: M → N is a localized linear map and M has NoZeroSmulDivisors as an R-module, then N has NoZeroSmulDivisors as an A-module after localization: NoZeroSmulDivisors A N.
Русский
Если f: M → N — локализованное линейное отображение и у M нет нулевых делителей умножения, то у N после локализации возникает свойство NoZeroSmulDivisors: NoZeroSmulDivisors A N.
LaTeX
$$$\text{NoZeroSMulDivisors}(A,N)$$$
Lean4
theorem noZeroSMulDivisors (S : Submonoid R) [NoZeroSMulDivisors R M] [IsLocalization S A] [IsLocalizedModule S f] :
NoZeroSMulDivisors A N := by
rw [noZeroSMulDivisors_iff]
intro c x hcx
obtain ⟨a, s, rfl⟩ := IsLocalization.mk'_surjective S c
obtain ⟨⟨m, t⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f x
rw [Function.uncurry_apply_pair] at hcx ⊢
rw [mk'_smul_mk', mk'_eq_zero, IsLocalizedModule.eq_zero_iff S] at hcx
obtain ⟨u, hl⟩ := hcx
rw [← smul_assoc] at hl
obtain (hua | rfl) := NoZeroSMulDivisors.eq_zero_or_eq_zero_of_smul_eq_zero hl
· rw [IsLocalization.mk'_eq_zero_iff]
exact Or.inl ⟨u, hua⟩
· simp
