Topological fields

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} [DivisionRing K] [TopologicalSpace K] [ContinuousMul K] {a : K} (ha : a ≠ 0) : Filter.Tendsto (fun (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.

theorem Filter.tendsto_cocompact_mul_right₀ {K : Type u_1} [DivisionRing K] [TopologicalSpace K] [ContinuousMul K] {a : K} (ha : a ≠ 0) : Filter.Tendsto (fun (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.

class TopologicalDivisionRing (K : Type u_1) [DivisionRing K] [TopologicalSpace K] extends TopologicalRing , HasContinuousInv₀ , TopologicalSemiring , ContinuousNeg , ContinuousAdd , ContinuousMul : Prop

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

def Subfield.topologicalClosure {α : Type u_2} [Field α] [TopologicalSpace α] [TopologicalDivisionRing α] (K : Subfield α) : Subfield α

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

Equations

• K.topologicalClosure = { carrier := closure ↑K, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯, inv_mem' := ⋯ }

theorem Subfield.le_topologicalClosure {α : Type u_2} [Field α] [TopologicalSpace α] [TopologicalDivisionRing α] (s : Subfield α) : s ≤ s.topologicalClosure

theorem Subfield.isClosed_topologicalClosure {α : Type u_2} [Field α] [TopologicalSpace α] [TopologicalDivisionRing α] (s : Subfield α) : IsClosed ↑s.topologicalClosure

theorem Subfield.topologicalClosure_minimal {α : Type u_2} [Field α] [TopologicalSpace α] [TopologicalDivisionRing α] (s : Subfield α) {t : Subfield α} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ 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.

def affineHomeomorph {𝕜 : Type u_2} [Field 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] (a : 𝕜) (b : 𝕜) (h : a ≠ 0) : 𝕜 ≃ₜ 𝕜

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

Equations

• affineHomeomorph a b h = { toFun := fun (x : 𝕜) => a * x + b, invFun := fun (y : 𝕜) => (y - b) / a, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem affineHomeomorph_apply {𝕜 : Type u_2} [Field 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] (a : 𝕜) (b : 𝕜) (h : a ≠ 0) (x : 𝕜) : (affineHomeomorph a b h) x = a * x + b

@[simp]

theorem affineHomeomorph_symm_apply {𝕜 : Type u_2} [Field 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] (a : 𝕜) (b : 𝕜) (h : a ≠ 0) (y : 𝕜) : (affineHomeomorph a b h).symm y = (y - b) / a

theorem IsLocalMin.inv {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [LinearOrderedSemifield β] {f : α → β} {a : α} (h1 : IsLocalMin f a) (h2 : ∀ᶠ (z : α) in nhds a, 0 < f z) : IsLocalMax f⁻¹ a

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

theorem IsPreconnected.eq_one_or_eq_neg_one_of_sq_eq {α : Type u_2} {𝕜 : Type u_3} {f : α → 𝕜} {S : Set α} [TopologicalSpace α] [TopologicalSpace 𝕜] [T1Space 𝕜] [Ring 𝕜] [NoZeroDivisors 𝕜] (hS : IsPreconnected S) (hf : ContinuousOn f S) (hsq : Set.EqOn (f ^ 2) 1 S) : Set.EqOn f 1 S ∨ Set.EqOn 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.

theorem IsPreconnected.eq_or_eq_neg_of_sq_eq {α : Type u_2} {𝕜 : Type u_3} {f : α → 𝕜} {g : α → 𝕜} {S : Set α} [TopologicalSpace α] [TopologicalSpace 𝕜] [T1Space 𝕜] [Field 𝕜] [HasContinuousInv₀ 𝕜] [ContinuousMul 𝕜] (hS : IsPreconnected S) (hf : ContinuousOn f S) (hg : ContinuousOn g S) (hsq : Set.EqOn (f ^ 2) (g ^ 2) S) (hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0) : Set.EqOn f g S ∨ Set.EqOn 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.

theorem IsPreconnected.eq_of_sq_eq {α : Type u_2} {𝕜 : Type u_3} {f : α → 𝕜} {g : α → 𝕜} {S : Set α} [TopologicalSpace α] [TopologicalSpace 𝕜] [T1Space 𝕜] [Field 𝕜] [HasContinuousInv₀ 𝕜] [ContinuousMul 𝕜] (hS : IsPreconnected S) (hf : ContinuousOn f S) (hg : ContinuousOn g S) (hsq : Set.EqOn (f ^ 2) (g ^ 2) S) (hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0) {y : α} (hy : y ∈ S) (hy' : f y = g y) : Set.EqOn 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.