Mathlib.Topology.Algebra.Field

Filter.tendsto_cocompact_mul_left₀ theorem

 [ContinuousMul K] {a : K} (ha : a ≠ 0) : Filter.Tendsto (fun x : K => a * x) (Filter.cocompact K) (Filter.cocompact K)

Full source

/-- 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_left₀ [ContinuousMul K] {a : K} (ha : a ≠ 0) :
    Filter.Tendsto (fun x : K => a * x) (Filter.cocompact K) (Filter.cocompact K) :=
  Filter.tendsto_cocompact_mul_left (inv_mul_cancel₀ ha)

Properness of Left-Multiplication by Nonzero Element in Topological Division Ring

Informal description

Let $K$ be a topological division ring with continuous multiplication. For any nonzero element $a \in K$, the left-multiplication map $x \mapsto a \cdot x$ is proper, i.e., it maps cocompact sets to cocompact sets.

Filter.tendsto_cocompact_mul_right₀ theorem

 [ContinuousMul K] {a : K} (ha : a ≠ 0) : Filter.Tendsto (fun x : K => x * a) (Filter.cocompact K) (Filter.cocompact K)

Full source

/-- Right-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₀ [ContinuousMul K] {a : K} (ha : a ≠ 0) :
    Filter.Tendsto (fun x : K => x * a) (Filter.cocompact K) (Filter.cocompact K) :=
  Filter.tendsto_cocompact_mul_right (mul_inv_cancel₀ ha)

Properness of Right-Multiplication by Nonzero Element in Topological Division Ring

Informal description

Let $K$ be a topological division ring with continuous multiplication. For any nonzero element $a \in K$, the right-multiplication map $x \mapsto x \cdot a$ is proper, meaning it preserves compactness in the sense that the preimage of any compact set under this map is compact.

instFiniteOfIsTopologicalRingOfCompactSpaceOfT2Space instance

{K} [DivisionRing K] [TopologicalSpace K] [IsTopologicalRing K] [CompactSpace K] [T2Space K] : Finite K

Full source

/-- Compact hausdorff topological fields are finite. -/
instance (priority := 100) {K} [DivisionRing K] [TopologicalSpace K]
    [IsTopologicalRing K] [CompactSpace K] [T2Space K] : Finite K := by
  suffices DiscreteTopology K by
    exact finite_of_compact_of_discrete
  rw [discreteTopology_iff_isOpen_singleton_zero]
  exact GroupWithZero.isOpen_singleton_zero

Compact Hausdorff Topological Division Rings are Finite

Informal description

Every compact Hausdorff topological division ring is finite.

IsTopologicalDivisionRing structure

extends IsTopologicalRing K, HasContinuousInv₀ K

Full source

/-- A topological division ring is a division ring with a topology where all operations are
    continuous, including inversion. -/
class IsTopologicalDivisionRing : Prop extends IsTopologicalRing K, HasContinuousInv₀ K

Topological Division Ring

Informal description

A topological division ring is a division ring $ K $ equipped with a topology such that the ring operations (addition and multiplication) are continuous, and the inversion operation $ x \mapsto x^{-1} $ is continuous at every nonzero element $ x \in K $.

Subfield.topologicalClosure definition

(K : Subfield α) : Subfield α

Full source

/-- The (topological-space) closure of a subfield of a topological field is
itself a subfield. -/
def Subfield.topologicalClosure (K : Subfield α) : Subfield α :=
  { K.toSubring.topologicalClosure with
    carrier := _root_.closure (K : Set α)
    inv_mem' := fun x hx => by
      rcases eq_or_ne x 0 with (rfl | h)
      · rwa [inv_zero]
      · rw [← inv_coe_set, ← Set.image_inv_eq_inv]
        exact mem_closure_image (continuousAt_inv₀ h) hx }

Topological closure of a subfield

Informal description

The topological closure of a subfield $ K $ of a topological field $ \alpha $ is itself a subfield of $ \alpha $. Specifically, the closure is constructed by taking the topological closure of the underlying set of $ K $ and ensuring that it is closed under inversion (with the inversion operation being continuous at every nonzero element).

Subfield.le_topologicalClosure theorem

(s : Subfield α) : s ≤ s.topologicalClosure

Full source

theorem Subfield.le_topologicalClosure (s : Subfield α) : s ≤ s.topologicalClosure :=
  _root_.subset_closure

Subfield is Contained in its Topological Closure

Informal description

For any subfield $s$ of a topological field $\alpha$, the subfield $s$ is contained in its topological closure.

Subfield.isClosed_topologicalClosure theorem

(s : Subfield α) : IsClosed (s.topologicalClosure : Set α)

Full source

theorem Subfield.isClosed_topologicalClosure (s : Subfield α) :
    IsClosed (s.topologicalClosure : Set α) :=
  isClosed_closure

Topological Closure of a Subfield is Closed

Informal description

For any subfield $s$ of a topological field $\alpha$, the topological closure of $s$ is a closed subset of $\alpha$.

Subfield.topologicalClosure_minimal theorem

(s : Subfield α) {t : Subfield α} (h : s ≤ t) (ht : IsClosed (t : Set α)) : s.topologicalClosure ≤ t

Full source

theorem Subfield.topologicalClosure_minimal (s : Subfield α) {t : Subfield α} (h : s ≤ t)
    (ht : IsClosed (t : Set α)) : s.topologicalClosure ≤ t :=
  closure_minimal h ht

Minimality of Topological Closure of a Subfield

Informal description

Let $s$ be a subfield of a topological field $\alpha$, and let $t$ be another subfield of $\alpha$ such that $s \subseteq t$ and $t$ is closed in $\alpha$. Then the topological closure of $s$ is contained in $t$.

affineHomeomorph definition

(a b : 𝕜) (h : a ≠ 0) : 𝕜 ≃ₜ 𝕜

Full source

/--
The map `fun x => a * x + b`, as a homeomorphism from `𝕜` (a topological field) to itself,
when `a ≠ 0`.
-/
@[simps]
def affineHomeomorph (a b : 𝕜) (h : a ≠ 0) : 𝕜 ≃ₜ 𝕜 where
  toFun x := a * x + b
  invFun y := (y - b) / a
  left_inv x := by
    simp only [add_sub_cancel_right]
    exact mul_div_cancel_left₀ x h
  right_inv y := by simp [mul_div_cancel₀ _ h]

Affine homeomorphism of a topological field

Informal description

For a topological field $\mathbb{K}$ and elements $a, b \in \mathbb{K}$ with $a \neq 0$, the affine map $x \mapsto a x + b$ defines a homeomorphism from $\mathbb{K}$ to itself. The inverse map is given by $y \mapsto \frac{y - b}{a}$.

affineHomeomorph_image_Icc theorem

 {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b c d : 𝕜)
  (h : 0 < a) : affineHomeomorph a b h.ne' '' Set.Icc c d = Set.Icc (a * c + b) (a * d + b)

Full source

theorem affineHomeomorph_image_Icc {𝕜 : Type*}
    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜]
    [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
    affineHomeomorphaffineHomeomorph a b h.ne' '' Set.Icc c d = Set.Icc (a * c + b) (a * d + b) := by
  simp [h]

Image of Closed Interval under Affine Homeomorphism: $[c, d] \mapsto [a c + b, a d + b]$

Informal description

Let $\mathbb{K}$ be a topological field with a linear order and a strict ordered ring structure. For any elements $a, b, c, d \in \mathbb{K}$ with $a > 0$, the image of the closed interval $[c, d]$ under the affine homeomorphism $x \mapsto a x + b$ is the closed interval $[a c + b, a d + b]$. In other words: $$\{a x + b \mid x \in [c, d]\} = [a c + b, a d + b]$$

affineHomeomorph_image_Ico theorem

 {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b c d : 𝕜)
  (h : 0 < a) : affineHomeomorph a b h.ne' '' Set.Ico c d = Set.Ico (a * c + b) (a * d + b)

Full source

theorem affineHomeomorph_image_Ico {𝕜 : Type*}
    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜]
    [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
    affineHomeomorphaffineHomeomorph a b h.ne' '' Set.Ico c d = Set.Ico (a * c + b) (a * d + b) := by
  simp [h]

Image of Half-Open Interval under Affine Homeomorphism: $[c, d) \mapsto [a c + b, a d + b)$

Informal description

Let $\mathbb{K}$ be a topological field with a linear order and a strict ordered ring structure. For any elements $a, b, c, d \in \mathbb{K}$ with $a > 0$, the image of the half-open interval $[c, d)$ under the affine homeomorphism $x \mapsto a x + b$ is the half-open interval $[a c + b, a d + b)$.

affineHomeomorph_image_Ioc theorem

 {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b c d : 𝕜)
  (h : 0 < a) : affineHomeomorph a b h.ne' '' Set.Ioc c d = Set.Ioc (a * c + b) (a * d + b)

Full source

theorem affineHomeomorph_image_Ioc {𝕜 : Type*}
    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜]
    [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
    affineHomeomorphaffineHomeomorph a b h.ne' '' Set.Ioc c d = Set.Ioc (a * c + b) (a * d + b) := by
  simp [h]

Image of $(c, d]$ under Affine Homeomorphism: $(c, d] \mapsto (a c + b, a d + b]$

Informal description

Let $\mathbb{K}$ be a topological field with a linear order and a strict ordered ring structure. For any elements $a, b, c, d \in \mathbb{K}$ with $a > 0$, the image of the left-open right-closed interval $(c, d]$ under the affine homeomorphism $x \mapsto a x + b$ is the left-open right-closed interval $(a c + b, a d + b]$. In other words: $$\{a x + b \mid x \in (c, d]\} = (a c + b, a d + b]$$

affineHomeomorph_image_Ioo theorem

 {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] (a b c d : 𝕜)
  (h : 0 < a) : affineHomeomorph a b h.ne' '' Set.Ioo c d = Set.Ioo (a * c + b) (a * d + b)

Full source

theorem affineHomeomorph_image_Ioo {𝕜 : Type*}
    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜]
    [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
    affineHomeomorphaffineHomeomorph a b h.ne' '' Set.Ioo c d = Set.Ioo (a * c + b) (a * d + b) := by
  simp [h]

Image of Open Interval under Affine Homeomorphism: $(c, d) \mapsto (a c + b, a d + b)$

Informal description

Let $\mathbb{K}$ be a topological field with a linear order and a strict ordered ring structure. For any elements $a, b, c, d \in \mathbb{K}$ with $a > 0$, the image of the open interval $(c, d)$ under the affine homeomorphism $x \mapsto a x + b$ is the open interval $(a c + b, a d + b)$.

IsLocalMin.inv theorem

{f : α → β} {a : α} (h1 : IsLocalMin f a) (h2 : ∀ᶠ z in 𝓝 a, 0 < f z) : IsLocalMax f⁻¹ a

Full source

theorem IsLocalMin.inv {f : α → β} {a : α} (h1 : IsLocalMin f a) (h2 : ∀ᶠ z in 𝓝 a, 0 < f z) :
    IsLocalMax f⁻¹ a := by
  filter_upwards [h1, h2] with z h3 h4 using(inv_le_inv₀ h4 h2.self_of_nhds).mpr h3

Reciprocal of a Local Minimum is a Local Maximum

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, and let $a \in \alpha$. If $f$ has a local minimum at $a$ and $f$ is strictly positive in a neighborhood of $a$, then the reciprocal function $f^{-1}$ has a local maximum at $a$.

Subfield.continuousSMul instance

(M : Subfield F) : ContinuousSMul M X

Full source

instance Subfield.continuousSMul (M : Subfield F) : ContinuousSMul M X :=
  Subring.continuousSMul M.toSubring X

Continuous Scalar Multiplication on Subfields of Topological Fields

Informal description

For any subfield $M$ of a topological field $F$, the scalar multiplication operation $M \times X \to X$ is continuous, where $X$ is a topological space equipped with an $M$-action.