English
Simplified version of mem_restrictScalars specialized form.
Русский
Упрощенная версия mem_restrictScalars для специального случая.
LaTeX
$$mem_restrictScalars_simp$$
Lean4
/-- A sufficient condition for injectivity of `NonUnitalSubalgebra.unitization` when the scalars
are a commutative ring. When the scalars are a field, one should use the more natural
`NonUnitalStarSubalgebra.unitization_injective` whose hypothesis is easier to verify. -/
theorem _root_.AlgHomClass.unitization_injective' {F R S A : Type*} [CommRing R] [Ring A] [Algebra R A] [SetLike S A]
[hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] (s : S) (h : ∀ r, r ≠ 0 → algebraMap R A r ∉ s)
[FunLike F (Unitization R s) A] [AlgHomClass F R (Unitization R s) A] (f : F) (hf : ∀ x : s, f x = x) :
Function.Injective f := by
refine (injective_iff_map_eq_zero f).mpr fun x hx => ?_
induction x with
| inl_add_inr r
a =>
simp_rw [map_add, hf, ← Unitization.algebraMap_eq_inl, AlgHomClass.commutes] at hx
rw [add_eq_zero_iff_eq_neg] at hx ⊢
by_cases hr : r = 0
· ext
· simp [hr]
· simpa [hr] using hx
· exact (h r hr <| hx ▸ (neg_mem a.property)).elim
