mathlib documentation

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] [topological_space R] [t : topological_space Rˣ] :
Prop

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
@[class]
structure topological_division_ring (K : Type u_1) [division_ring K] [topological_space K] :
Prop

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

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 𝕜] [topological_space 𝕜] [topological_ring 𝕜] (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 𝕜] [topological_space 𝕜] [topological_ring 𝕜] (a b : 𝕜) (h : a 0) (x : 𝕜) :
(affine_homeomorph a b h) x = a * x + b
@[simp]
theorem affine_homeomorph_symm_apply {𝕜 : Type u_2} [field 𝕜] [topological_space 𝕜] [topological_ring 𝕜] (a b : 𝕜) (h : a 0) (y : 𝕜) :
((affine_homeomorph a b h).symm) y = (y - b) / a