English
There is a natural lift of a NormedAddGroupHom f: M → N to a NormedAddGroupHom on the separation quotient SeperationQuotient M → N, provided hf ensures f vanishes on zero-norm elements.
Русский
Существует естественный подъём нормированного аддитивного гомоморфизма f: M → N до нормированного гомоморфизма на фактор-пространстве SeperationQuotient M → N, при условии hf, что f обращает нуль на элементы нулевой нормы.
LaTeX
$$$\\mathrm{liftNormedAddGroupHom}:\\; (f:\\mathrm{NormedAddGroupHom}\\ M\\ N)\\to\\mathrm{NormedAddGroupHom}(\\mathrm{SeparationQuotient}\\ M\\ N)$, с указанной реализацией toFun через SeparationQuotient.liftContinuousAddMonoidHom и apply_eq_apply_of_inseparable f hf.$$
Lean4
/-- The lift of a group hom to the separation quotient as a group hom. -/
@[simps]
noncomputable def liftNormedAddGroupHom (f : NormedAddGroupHom M N) (hf : ∀ x, ‖x‖ = 0 → f x = 0) :
NormedAddGroupHom (SeparationQuotient M) N
where
toFun := SeparationQuotient.liftContinuousAddMonoidHom f <| apply_eq_apply_of_inseparable f hf
map_add' v₁ v₂ := map_add ..
bound' := by
refine ⟨‖f‖, fun v ↦ ?_⟩
obtain ⟨v, rfl⟩ := surjective_mk v
exact le_opNorm f v
