Topological fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A topological division ring is a topological ring whose inversion function is continuous at every non-zero element.

theorem filter.tendsto_cocompact_mul_left₀ {K : Type u_1} [division_ring K] [topological_space K] [has_continuous_mul K] {a : K} (ha : a ≠ 0) :

filter.tendsto (λ (x : K), a * x) (filter.cocompact K) (filter.cocompact K)

Left-multiplication by a nonzero element of a topological division ring is proper, i.e., inverse images of compact sets are compact.

source

theorem filter.tendsto_cocompact_mul_right₀ {K : Type u_1} [division_ring K] [topological_space K] [has_continuous_mul K] {a : K} (ha : a ≠ 0) :

filter.tendsto (λ (x : K), x * a) (filter.cocompact K) (filter.cocompact K)

Right-multiplication by a nonzero element of a topological division ring is proper, i.e., inverse images of compact sets are compact.

source

@[class]

structure topological_division_ring (K : Type u_1) [division_ring K] [topological_space K] :

Prop

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.

Instances of this typeclass

source

def subfield.topological_closure {α : Type u_2} [field α] [topological_space α] [topological_division_ring α] (K : subfield α) :

subfield α

The (topological-space) closure of a subfield of a topological field is itself a subfield.

Equations

K.topological_closure = {carrier := closure ↑K, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, neg_mem' := _, inv_mem' := _}

source

theorem subfield.le_topological_closure {α : Type u_2} [field α] [topological_space α] [topological_division_ring α] (s : subfield α) :

s ≤ s.topological_closure

source

theorem subfield.is_closed_topological_closure {α : Type u_2} [field α] [topological_space α] [topological_division_ring α] (s : subfield α) :

is_closed ↑(s.topological_closure)

source

theorem subfield.topological_closure_minimal {α : Type u_2} [field α] [topological_space α] [topological_division_ring α] (s : subfield α) {t : subfield α} (h : s ≤ t) (ht : is_closed ↑t) :

s.topological_closure ≤ t

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.

source

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

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 := _}

source

@[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

source

@[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

source

theorem is_local_min.inv {α : Type u_2} {β : Type u_3} [topological_space α] [linear_ordered_semifield β] {f : α → β} {a : α} (h1 : is_local_min f a) (h2 : ∀ᶠ (z : α) in nhds a, 0 < f z) :

is_local_max f⁻¹ a

Some results about functions on preconnected sets valued in a ring or field with a topology.

source

theorem is_preconnected.eq_one_or_eq_neg_one_of_sq_eq {α : Type u_2} {𝕜 : Type u_3} {f : α → 𝕜} {S : set α} [topological_space α] [topological_space 𝕜] [t1_space 𝕜] [ring 𝕜] [no_zero_divisors 𝕜] (hS : is_preconnected S) (hf : continuous_on f S) (hsq : set.eq_on (f ^ 2) 1 S) :

set.eq_on f 1 S ∨ set.eq_on f (-1) S

If f is a function α → 𝕜 which is continuous on a preconnected set S, and f ^ 2 = 1 on S, then either f = 1 on S, or f = -1 on S.

source

theorem is_preconnected.eq_or_eq_neg_of_sq_eq {α : Type u_2} {𝕜 : Type u_3} {f g : α → 𝕜} {S : set α} [topological_space α] [topological_space 𝕜] [t1_space 𝕜] [field 𝕜] [has_continuous_inv₀ 𝕜] [has_continuous_mul 𝕜] (hS : is_preconnected S) (hf : continuous_on f S) (hg : continuous_on g S) (hsq : set.eq_on (f ^ 2) (g ^ 2) S) (hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0) :

set.eq_on f g S ∨ set.eq_on f (-g) S

If f, g are functions α → 𝕜, both continuous on a preconnected set S, with f ^ 2 = g ^ 2 on S, and g z ≠ 0 all z ∈ S, then either f = g or f = -g on S.

source

theorem is_preconnected.eq_of_sq_eq {α : Type u_2} {𝕜 : Type u_3} {f g : α → 𝕜} {S : set α} [topological_space α] [topological_space 𝕜] [t1_space 𝕜] [field 𝕜] [has_continuous_inv₀ 𝕜] [has_continuous_mul 𝕜] (hS : is_preconnected S) (hf : continuous_on f S) (hg : continuous_on g S) (hsq : set.eq_on (f ^ 2) (g ^ 2) S) (hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0) {y : α} (hy : y ∈ S) (hy' : f y = g y) :

set.eq_on f g S

If f, g are functions α → 𝕜, both continuous on a preconnected set S, with f ^ 2 = g ^ 2 on S, and g z ≠ 0 all z ∈ S, then as soon as f = g holds at one point of S it holds for all points.