Mathlib.Topology.Algebra.Affine

Module docstring

{"# Topological properties of affine spaces and maps

For now, this contains only a few facts regarding the continuity of affine maps in the special case when the point space and vector space are the same.

TODO: Deal with the case where the point spaces are different from the vector spaces. Note that we do have some results in this direction under the assumption that the topologies are induced by (semi)norms. "}

AffineMap.continuous_iff theorem

{f : E →ᵃ[R] F} : Continuous f ↔ Continuous f.linear

Full source

/-- An affine map is continuous iff its underlying linear map is continuous. See also
`AffineMap.continuous_linear_iff`. -/
theorem continuous_iff {f : E →ᵃ[R] F} : ContinuousContinuous f ↔ Continuous f.linear := by
  constructor
  · intro hc
    rw [decomp' f]
    exact hc.sub continuous_const
  · intro hc
    rw [decomp f]
    exact hc.add continuous_const

Continuity of Affine Maps via Their Linear Part

Informal description

An affine map $f \colon E \to F$ between affine spaces over a topological ring $R$ is continuous if and only if its underlying linear map $f_{\text{linear}}$ is continuous.

AffineMap.lineMap_continuous theorem

[TopologicalSpace R] [ContinuousSMul R F] {p v : F} : Continuous (lineMap p v : R →ᵃ[R] F)

Full source

/-- The line map is continuous. -/
@[continuity]
theorem lineMap_continuous [TopologicalSpace R] [ContinuousSMul R F] {p v : F} :
    Continuous (lineMap p v : R →ᵃ[R] F) :=
  continuous_iff.mpr <|
    (continuous_id.smul continuous_const).add <| @continuous_const _ _ _ _ (0 : F)

Continuity of Affine Line Maps

Informal description

Let $R$ be a topological ring and $F$ be a topological space with a continuous scalar multiplication action of $R$. For any points $p, v \in F$, the affine line map $\text{lineMap}_{p,v} \colon R \to F$ defined by $\text{lineMap}_{p,v}(t) = p + t \cdot (v - p)$ is continuous.

AffineMap.homothety_continuous theorem

(x : F) (t : R) : Continuous <| homothety x t

Full source

@[continuity]
theorem homothety_continuous (x : F) (t : R) : Continuous <| homothety x t := by
  suffices ⇑(homothety x t) = fun y => t • (y - x) + x by
    rw [this]
    fun_prop
  ext y
  simp [homothety_apply]

Continuity of Homothety Maps in Real Vector Spaces

Informal description

For any point $x$ in a real vector space $F$ and any scalar $t \in \mathbb{R}$, the homothety map $\text{homothety}_x(t) : F \to F$ defined by $\text{homothety}_x(t)(y) = x + t(y - x)$ is continuous.

AffineMap.homothety_isOpenMap theorem

(x : F) (t : R) (ht : t ≠ 0) : IsOpenMap <| homothety x t

Full source

theorem homothety_isOpenMap (x : F) (t : R) (ht : t ≠ 0) : IsOpenMap <| homothety x t := by
  apply IsOpenMap.of_inverse (homothety_continuous x t⁻¹) <;> intro e <;>
    simp [← AffineMap.comp_apply, ← homothety_mul, ht]

Homothety Maps are Open for Nonzero Scalars

Informal description

For any point $x$ in a real vector space $F$ and any nonzero scalar $t \in \mathbb{R}$, the homothety map $\text{homothety}_x(t) : F \to F$ defined by $\text{homothety}_x(t)(y) = x + t(y - x)$ is an open map.