English
A nonunital algebra homomorphism from A into a unital R-algebra C extends to a unital algebra homomorphism from the unitization into C.
Русский
Неединообразный алгебра-гомоморфизм из A в развёрнутую единичную R-алгебру может быть продолжен до единичного алгебра-гомоморфизма из единичизации в C.
LaTeX
$$$\text{Given } φ: A \to_{NU}^R C, \; φ \mapsto (a,b) \mapsto \mathrm{algebraMap}_R(C) + φ(b)$ (definition of lift).$$$
Lean4
/-- A non-unital algebra homomorphism from `A` into a unital `R`-algebra `C` lifts to a unital
algebra homomorphism from the unitization into `C`. This is extended to an `Equiv` in
`Unitization.lift` and that should be used instead. This declaration only exists for performance
reasons. -/
@[simps]
def _root_.NonUnitalAlgHom.toAlgHom (φ : A →ₙₐ[R] C) : Unitization R A →ₐ[R] C
where
toFun := fun x => algebraMap R C x.fst + φ x.snd
map_one' := by simp only [fst_one, map_one, snd_one, φ.map_zero, add_zero]
map_mul' := fun x y => by
induction x with
| inl_add_inr x_r x_a =>
induction y with
|
inl_add_inr =>
simp only [fst_mul, fst_add, fst_inl, fst_inr, snd_mul, snd_add, snd_inl, snd_inr, add_zero, map_mul, zero_add,
map_add, map_smul φ]
rw [add_mul, mul_add, mul_add]
rw [← Algebra.commutes _ (φ x_a)]
simp only [Algebra.algebraMap_eq_smul_one, smul_one_mul, add_assoc]
map_zero' := by simp only [fst_zero, map_zero, snd_zero, φ.map_zero, add_zero]
map_add' := fun x y => by
induction x with
| inl_add_inr =>
induction y with
|
inl_add_inr =>
simp only [fst_add, fst_inl, fst_inr, add_zero, map_add, snd_add, snd_inl, snd_inr, zero_add, φ.map_add]
rw [add_add_add_comm]
commutes' := fun r => by simp only [algebraMap_eq_inl, fst_inl, snd_inl, φ.map_zero, add_zero]
