English
Generalized injecting lemma for unitization with field scalars and more general alphabet.
Русский
Обобщенная лемма инъективности единизации для полевых скаляров и более общего алфавита.
LaTeX
$$Generalized injectivity$$
Lean4
/-- If a `NonUnitalSubalgebra` over a field does not contain `1`, then its unitization is
isomorphic to its `Algebra.adjoin`. -/
@[simps! apply_coe]
noncomputable def unitizationAlgEquiv (h1 : (1 : A) ∉ s) : Unitization R s ≃ₐ[R] Algebra.adjoin R (s : Set A) :=
let algHom : Unitization R s →ₐ[R] Algebra.adjoin R (s : Set A) :=
((unitization s).codRestrict _ fun x ↦ (unitization_range s).le <| AlgHom.mem_range_self _ x)
AlgEquiv.ofBijective algHom <| by
refine ⟨?_, fun x ↦ ?_⟩
· have := AlgHomClass.unitization_injective s h1 ((Subalgebra.val _).comp algHom) fun _ ↦ by simp [algHom]
rw [AlgHom.coe_comp] at this
exact this.of_comp
· obtain (⟨a, ha⟩ : (x : A) ∈ (unitization s).range) := (unitization_range s).ge x.property
exact ⟨a, Subtype.ext ha⟩
