faithfulSMul_iff_injective_smul_one

English

A faithful SMul is equivalent to the injectivity of the map r ↦ r • 1 on the base ring/monoid.

Русский

Верное SMul эквивалентно инъективности отображения r ↦ r • 1 на основание моноида/кольца.

LaTeX

$$$\\mathrm{FaithfulSMul } R A \\iff \\mathrm{Injective}(\\lambda r: R. r \\cdot 1)$.$$

Lean4

theorem faithfulSMul_iff_injective_smul_one (R A : Type*) [MulOneClass A] [SMul R A] [IsScalarTower R A A] :
    FaithfulSMul R A ↔ Injective (fun r : R ↦ r • (1 : A)) :=
  by
  refine ⟨fun ⟨h⟩ {r₁ r₂} hr ↦ h fun a ↦ ?_, fun h ↦ ⟨fun {r₁ r₂} hr ↦ h ?_⟩⟩
  · simp only at hr
    rw [← one_mul a, ← smul_mul_assoc, ← smul_mul_assoc, hr]
  · simpa using hr 1

Похожие утверждения