Topological fields #
A topological division ring is a topological ring whose inversion function is continuous at every non-zero element.
The induced topology on units of a topological semiring.
This is not a global instance since other topologies could be relevant. Instead there is a class
induced_units asserting that something equivalent to this construction holds.
Equations
- top_eq : t = topological_space.induced coe _inst_2
Asserts the topology on units is the induced topology.
Note: this is not always the correct topology. Another good candidate is the subspace topology of $R \times R$, with the units embedded via $u \mapsto (u, u^{-1})$. These topologies are not (propositionally) equal in general.
Instances
- to_topological_ring : topological_ring K
- to_has_continuous_inv₀ : has_continuous_inv₀ K
A topological division ring is a division ring with a topology where all operations are continuous, including inversion.
In this section, we show that units of a topological division ring endowed with the induced topology form a topological group. These are not global instances because one could want another topology on units. To turn on this feature, use:
local attribute [instance]
topological_semiring.topological_space_units topological_division_ring.units_top_group
This section is about affine homeomorphisms from a topological field 𝕜 to itself.
Technically it does not require 𝕜 to be a topological field, a topological ring that
happens to be a field is enough.
The map λ x, a * x + b, as a homeomorphism from 𝕜 (a topological field) to itself, when a ≠ 0.
Equations
- affine_homeomorph a b h = {to_equiv := {to_fun := λ (x : 𝕜), a * x + b, inv_fun := λ (y : 𝕜), (y - b) / a, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}