English
There is an equivalence between the set of NormedAddGroupHom M N vanishing on the inseparable setoid and NormedAddGroupHom (SeparationQuotient M) N.
Русский
Существует эквивалентность между множеством NormedAddGroupHom M N, исчезающим на inseparable-множество-ход, и NormedAddGroupHom (SeparationQuotient M) N.
LaTeX
$$$\\text{Equiv} \\,\\{ f:\\mathrm{NormedAddGroupHom}\\ M\\ N \\mid \\forall x, \\|x\\| = 0 \\to f x = 0 \\} \\;\\simeq\\; \\mathrm{NormedAddGroupHom}(\\mathrm{SeparationQuotient}\\ M\\ N)$$$
Lean4
/-- The equivalence between `NormedAddGroupHom M N` vanishing on the inseparable setoid and
`NormedAddGroupHom (SeparationQuotient M) N`. -/
@[simps]
noncomputable def liftNormedAddGroupHomEquiv {N : Type*} [SeminormedAddCommGroup N] :
{ f : NormedAddGroupHom M N // ∀ x, ‖x‖ = 0 → f x = 0 } ≃ NormedAddGroupHom (SeparationQuotient M) N
where
toFun f := liftNormedAddGroupHom f f.prop
invFun
g :=
⟨g.comp normedMk, by
intro x hx
rw [← norm_mk, norm_eq_zero] at hx
simp [hx]⟩
right_inv
_ := by
ext x
obtain ⟨x, rfl⟩ := surjective_mk x
rfl
