An open map out of a nonarchimedean group stays open, and an open surjection stays surjective #
For a continuous open homomorphism f : G → H from a first-countable nonarchimedean additive
group to a uniform additive group, the induced map on separated completions is again open; if f
is moreover surjective then so is that map. Openness is what the statements turn on: a continuous
surjection alone gives only a dense image in the completion of H. Nothing is asked of H beyond
being a uniform additive group.
Main results #
AddMonoidHom.isOpenMap_completion: the induced map on completions is open.AddMonoidHom.surjective_completion: it is surjective whenfis.
theorem
AddMonoidHom.isOpenMap_completion
{G : Type u_1}
[AddCommGroup G]
[UniformSpace G]
[IsUniformAddGroup G]
{H : Type u_2}
[AddGroup H]
[UniformSpace H]
[IsUniformAddGroup H]
[NonarchimedeanAddGroup G]
[(nhds 0).IsCountablyGenerated]
(f : G →+ H)
(hf : Continuous ⇑f)
(hopen : IsOpenMap ⇑f)
:
IsOpenMap ⇑(f.completion hf)
A continuous open homomorphism out of a first-countable nonarchimedean additive group induces an open map on the separated completions.
theorem
AddMonoidHom.surjective_completion
{G : Type u_1}
[AddCommGroup G]
[UniformSpace G]
[IsUniformAddGroup G]
{H : Type u_2}
[AddGroup H]
[UniformSpace H]
[IsUniformAddGroup H]
[NonarchimedeanAddGroup G]
[(nhds 0).IsCountablyGenerated]
(f : G →+ H)
(hf : Continuous ⇑f)
(hsurj : Function.Surjective ⇑f)
(hopen : IsOpenMap ⇑f)
:
Function.Surjective ⇑(f.completion hf)
A continuous open surjection out of a first-countable nonarchimedean additive group induces a surjection on the separated completions.