# Topological fields #

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

source
theorem Filter.tendsto_cocompact_mul_left₀ {K : Type u_1} [DivisionRing K] [TopologicalSpace K] [ContinuousMul K] {a : K} (ha : a ≠ 0) :
Tendsto (fun (x : K) => a * x) (cocompact K) (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} [DivisionRing K] [TopologicalSpace K] [ContinuousMul K] {a : K} (ha : a ≠ 0) :
Tendsto (fun (x : K) => x * a) (cocompact K) (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
theorem DivisionRing.finite_of_compactSpace_of_t2Space {K : Type u_2} [DivisionRing K] [TopologicalSpace K] [IsTopologicalRing K] [CompactSpace K] [T2Space K] :
Finite K

Compact Hausdorff topological fields are finite. This is not an instance, as it would apply to every `Finite` goal, causing slowly failing typeclass search in some cases.

source
class IsTopologicalDivisionRing (K : Type u_1) [DivisionRing K] [TopologicalSpace K] extends IsTopologicalRing K, ContinuousInv₀ K :
Prop

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

- continuous_add : Continuous fun (p : K × K) => p.1 + p.2
- continuous_mul : Continuous fun (p : K × K) => p.1 * p.2
- continuous_neg : Continuous fun (a : K) => -a
- continuousAt_inv₀ ⦃x : K⦄ : x ≠ 0 → ContinuousAt Inv.inv x

Instances

source
def Subfield.topologicalClosure {α : Type u_2} [Field α] [TopologicalSpace α] [IsTopologicalDivisionRing α] (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' := ⋯ }

Instances For

source
theorem Subfield.le_topologicalClosure {α : Type u_2} [Field α] [TopologicalSpace α] [IsTopologicalDivisionRing α] (s : Subfield α) :
s ≤ s.topologicalClosure
source
theorem Subfield.isClosed_topologicalClosure {α : Type u_2} [Field α] [TopologicalSpace α] [IsTopologicalDivisionRing α] (s : Subfield α) :
IsClosed ↑s.topologicalClosure
source
theorem Subfield.topologicalClosure_minimal {α : Type u_2} [Field α] [TopologicalSpace α] [IsTopologicalDivisionRing α] (s : Subfield α) {t : Subfield α} (h : s ≤ t) (ht : IsClosed ↑t) :
s.topologicalClosure ≤ t
source
def Nonneg.unitsHomeomorphPos (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] [TopologicalSpace R] [ContinuousInv₀ R] :
{ r : R // 0 ≤ r }ˣ ≃ₜ { r : R // 0 < r }

In an ordered field, the units of the nonnegative elements are the positive elements.

Equations

- Nonneg.unitsHomeomorphPos R = { toEquiv := (Nonneg.unitsEquivPos R).toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem Nonneg.unitsHomeomorphPos_apply_coe (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] [TopologicalSpace R] [ContinuousInv₀ R] (r : { r : R // 0 ≤ r }ˣ) :
↑((unitsHomeomorphPos R) r) = ↑↑r
source
@[simp]
theorem Nonneg.val_inv_unitsHomeomorphPos_symm_apply_coe (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] [TopologicalSpace R] [ContinuousInv₀ R] (r : { r : R // 0 < r }) :
↑↑((unitsHomeomorphPos R).symm r)⁻¹ = (↑r)⁻¹
source
@[simp]
theorem Nonneg.val_unitsHomeomorphPos_symm_apply_coe (R : Type u_2) [DivisionSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [PosMulReflectLT R] [TopologicalSpace R] [ContinuousInv₀ R] (r : { r : R // 0 < r }) :
↑↑((unitsHomeomorphPos R).symm r) = ↑r

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 affineHomeomorph {𝕜 : Type u_2} [Field 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (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 := ⋯ }

Instances For

source
@[simp]
theorem affineHomeomorph_symm_apply {𝕜 : Type u_2} [Field 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b : 𝕜) (h : a ≠ 0) (y : 𝕜) :
(affineHomeomorph a b h).symm y = (y - b) / a
source
@[simp]
theorem affineHomeomorph_apply {𝕜 : Type u_2} [Field 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b : 𝕜) (h : a ≠ 0) (x : 𝕜) :
(affineHomeomorph a b h) x = a * x + b
source
theorem affineHomeomorph_image_Icc {𝕜 : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
⇑(affineHomeomorph a b ⋯) '' Set.Icc c d = Set.Icc (a * c + b) (a * d + b)
source
theorem affineHomeomorph_image_Ico {𝕜 : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
⇑(affineHomeomorph a b ⋯) '' Set.Ico c d = Set.Ico (a * c + b) (a * d + b)
source
theorem affineHomeomorph_image_Ioc {𝕜 : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
⇑(affineHomeomorph a b ⋯) '' Set.Ioc c d = Set.Ioc (a * c + b) (a * d + b)
source
theorem affineHomeomorph_image_Ioo {𝕜 : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
⇑(affineHomeomorph a b ⋯) '' Set.Ioo c d = Set.Ioo (a * c + b) (a * d + b)
source
theorem IsLocalMin.inv {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Semifield β] [LinearOrder β] [IsStrictOrderedRing β] {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.

source
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`.

source
theorem IsPreconnected.eq_or_eq_neg_of_sq_eq {α : Type u_2} {𝕜 : Type u_3} {f g : α → 𝕜} {S : Set α} [TopologicalSpace α] [TopologicalSpace 𝕜] [T1Space 𝕜] [Field 𝕜] [ContinuousInv₀ 𝕜] [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`.

source
theorem IsPreconnected.eq_of_sq_eq {α : Type u_2} {𝕜 : Type u_3} {f g : α → 𝕜} {S : Set α} [TopologicalSpace α] [TopologicalSpace 𝕜] [T1Space 𝕜] [Field 𝕜] [ContinuousInv₀ 𝕜] [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.

source
instance Subfield.continuousSMul {F : Type u_2} [DivisionRing F] [TopologicalSpace F] (X : Type u_3) [TopologicalSpace X] [MulAction F X] [ContinuousSMul F X] (M : Subfield F) :
ContinuousSMul (↥M) X