Documentation

Mathlib.Topology.Algebra.Field

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) :
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.

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.

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.

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

Instances
    @[deprecated IsTopologicalDivisionRing (since := "2025-03-25")]

    Alias of IsTopologicalDivisionRing.


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

    Equations
    Instances For

      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

        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 𝕜] [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
          @[simp]
          theorem affineHomeomorph_apply {𝕜 : Type u_2} [Field 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b : 𝕜) (h : a 0) (x : 𝕜) :
          (affineHomeomorph a b h) x = a * x + b
          @[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
          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)
          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)
          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)
          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)
          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) :

          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 Sg 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 Sg 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.