# mathlibdocumentation

topology.algebra.field

# 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
@[class]
structure topological_ring.induced_units (R : Type u_1) [semiring R] [t : topological_space Rˣ] :
Prop
• top_eq : t = _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 of this typeclass
theorem topological_ring.units_topology_eq (R : Type u_1) [semiring R]  :
_inst_3 = _inst_2
theorem topological_ring.units_embedding (R : Type u_1) [semiring R]  :
@[protected, instance]
def topological_ring.top_monoid_units (R : Type u_1) [semiring R]  :
@[class]
structure topological_division_ring (K : Type u_1)  :
Prop
• to_topological_ring :
• to_has_continuous_inv₀ :

A topological division ring is a division ring with a topology where all operations are continuous, including inversion.

Instances of this typeclass

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

@[protected, instance]

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.

def affine_homeomorph {𝕜 : Type u_2} [field 𝕜] (a b : 𝕜) (h : a 0) :
𝕜 ≃ₜ 𝕜

The map λ x, a * x + b, as a homeomorphism from 𝕜 (a topological field) to itself, when a ≠ 0.

Equations
@[simp]
theorem affine_homeomorph_apply {𝕜 : Type u_2} [field 𝕜] (a b : 𝕜) (h : a 0) (x : 𝕜) :
h) x = a * x + b
@[simp]
theorem affine_homeomorph_symm_apply {𝕜 : Type u_2} [field 𝕜] (a b : 𝕜) (h : a 0) (y : 𝕜) :
b h).symm) y = (y - b) / a