Physlib.ClassicalMechanics.HarmonicOscillator.Geometric.Basic

Configuration space of the harmonic oscillator

i. Overview

The configuration space `Q` of the one-dimensional harmonic oscillator is the space of possible positions of the oscillator, formalised here as a one-dimensional smooth manifold.

`Q` carries a single chosen global coordinate, modeled by `EuclideanSpace ℝ (Fin 1)`. This coordinate supplies the topology and the smooth-manifold structure through a single global chart.

The global coordinate also identifies each tangent space with the same Euclidean model. The map `tangentCoord q` records the coordinate representative of a tangent vector at `q`; this tangent-coordinate infrastructure is used by later geometric constructions on the oscillator.

ii. Key results

- `ConfigurationSpace` : the configuration manifold `Q` of the harmonic oscillator, wrapping the chosen `EuclideanSpace ℝ (Fin 1)` coordinate. - `ConfigurationSpace.valEquiv` : the coordinate equivalence identifying `Q` with its `EuclideanSpace ℝ (Fin 1)` model. - `ConfigurationSpace.valHomeomorphism` : the global coordinate homeomorphism underlying the manifold chart. - `ConfigurationSpace.valDiffeomorph` : the global coordinate chart as an analytic diffeomorphism, upgrading `valHomeomorphism` to a smooth identification of `Q` with its model. - the `ChartedSpace` and `IsManifold` instances, exhibiting `Q` as a one-dimensional analytic manifold modeled on `EuclideanSpace ℝ (Fin 1)`. - `tangentCoord` : the chart-induced continuous linear equivalence from the tangent space at a configuration to `EuclideanSpace ℝ (Fin 1)`. - `instNormedAddCommGroupTangent` and `instNormedSpaceTangent` : the normed real vector-space structure on tangent spaces, supplied through the global coordinate model. - `instFiniteDimensionalTangent` : finite-dimensionality of each tangent space, transported through `tangentCoord`. - `ConfigurationSpace.toSpace` : the point of physical `Space 1` determined by a configuration.

iii. Table of contents

A. The configuration space type
B. Topology and coordinate homeomorphism
C. Smooth manifold structure
D. The coordinate diffeomorphism
E. Tangent-coordinate infrastructure
F. Map to physical space

iv. References

- Ivo Terek, Introductory Variational Calculus on Manifolds, page 1 (Section 1, Basic definitions and examples).

A. The configuration space type

`ConfigurationSpace` wraps a single chosen global coordinate valued in `EuclideanSpace ℝ (Fin 1)`. We record extensionality in this coordinate together with a function-like coordinate access mirroring that of `EuclideanSpace ℝ (Fin 1)`.

B. Topology and coordinate homeomorphism

`ConfigurationSpace` carries the topology induced by its chosen coordinate `ConfigurationSpace.val`: a set of configurations is open exactly when it is the preimage of an open set under `val`. The wrapper/unwrapper pair is the coordinate equivalence `valEquiv`, which is a homeomorphism `valHomeomorphism` for this induced topology — its continuity in both directions is just the universal property of the induced topology. We transport Hausdorffness and second countability across it from the model space, so `Q` is a well-behaved topological manifold.

C. Smooth manifold structure

`ConfigurationSpace` is an analytic manifold modeled on `EuclideanSpace ℝ (Fin 1)`, via the single global chart `valHomeomorphism`. With one chart the only coordinate change is the chart's self-transition, which is analytic, so chart compatibility is immediate.

D. The coordinate diffeomorphism

The single global chart is an analytic diffeomorphism, not merely a homeomorphism, so `Q` is identified with its `EuclideanSpace ℝ (Fin 1)` model as a smooth manifold. With one chart this is immediate: the only transition is the analytic self-transition already recorded in the manifold structure. This smooth identification is what lets smoothness of maps to or from `Q` be tested in the chosen global coordinate, the device used for trajectories and their velocities.

E. Tangent-coordinate infrastructure

The global coordinate on `ConfigurationSpace` also gives a coordinate representative for tangent vectors. The tangent spaces inherit their normed real vector-space structure from the Euclidean coordinate model, and `tangentCoord q` records the resulting continuous linear equivalence.

F. Map to physical space

The point of one-dimensional physical `Space 1` determined by a configuration, obtained by reading off the underlying coordinate. This links the abstract configuration manifold to the concrete coordinate model.

12 declarations

theorem

$x(i) = x.\text{val}(i)$ for configurations in $Q$

#coe_apply

Let $Q$ denote the configuration space of the one-dimensional harmonic oscillator, which is modeled on the Euclidean space $\mathbb{E}^1$ (represented as `EuclideanSpace ℝ (Fin 1)`). For any configuration $x \in Q$ and index $i \in \text{Fin } 1$ , the value obtained by treating $x$ as a function applied to $i$ is equal to the $i$ -th component of its underlying global coordinate vector $x.\text{val}$ .

instance

Topological space structure on the configuration space $Q$

#instTopologicalSpace

The configuration space $Q$ of the harmonic oscillator is endowed with the topological structure induced by the coordinate map $\text{val} : Q \to \mathbb{R}^1$ (where $\mathbb{R}^1$ is represented by $\text{EuclideanSpace } \mathbb{R} (\text{Fin } 1)$ ). This topology is defined such that a subset $U \subseteq Q$ is open if and only if it is the preimage of an open set in the Euclidean model space $\mathbb{R}^1$ under the map $\text{val}$ .

definition

Coordinate equivalence $Q \simeq \mathbb{E}^1$

#valEquiv

This definition establishes a coordinate equivalence (a bijection) between the configuration space $Q$ of the one-dimensional harmonic oscillator and its model space $\mathbb{E}^1$ (represented as `EuclideanSpace ℝ (Fin 1)`). The map sends a configuration $x \in Q$ to its underlying coordinate value $x.\text{val} \in \mathbb{E}^1$ , with an inverse that wraps a coordinate vector back into a configuration point.

instance

The configuration space $Q$ is a Hausdorff space

#instT2Space

The configuration space $Q$ of the one-dimensional harmonic oscillator is a Hausdorff space (also known as a $T_2$ space). This topological property is transported from the Euclidean model space $\mathbb{R}^1$ (represented as $\text{EuclideanSpace } \mathbb{R} (\text{Fin } 1)$ ) via the global coordinate homeomorphism.

instance

The configuration space $Q$ is second-countable

#instSecondCountableTopology

The configuration space $Q$ of the one-dimensional harmonic oscillator is second-countable. This property is inherited from the Euclidean model space $\mathbb{R}^1$ (represented as $\text{EuclideanSpace } \mathbb{R} (\text{Fin } 1)$ ) via the coordinate homeomorphism.

instance

Charted space structure on the configuration space $Q$ modeled on $\mathbb{R}^1$

#instChartedSpaceEuclideanSpaceRealFinOfNatNat

The configuration space $Q$ of the one-dimensional harmonic oscillator is equipped with a charted space structure modeled on the Euclidean space $\mathbb{R}^1$ (represented as $\text{EuclideanSpace } \mathbb{R} (\text{Fin } 1)$ ). This structure is defined by an atlas containing a single global chart, which is the homeomorphism $\text{valHomeomorphism} : Q \simeq \mathbb{R}^1$ that maps each configuration to its corresponding coordinate value.

instance

The Configuration Space $Q$ is an Analytic Manifold Modeled on $\mathbb{R}^1$

#instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENat

The configuration space $Q$ of the one-dimensional harmonic oscillator is an analytic manifold (of class $C^\omega$ ) modeled on the 1-dimensional Euclidean space $\mathbb{R}^1$ (represented as $\text{EuclideanSpace } \mathbb{R} (\text{Fin } 1)$ ) with the standard identity model with corners $\mathcal{I}(\mathbb{R}, \mathbb{R}^1)$ . This manifold structure is established via a single global coordinate chart.

definition

Analytic diffeomorphism $Q \simeq \mathbb{R}^1$

#valDiffeomorph

The map `valDiffeomorph` is an analytic diffeomorphism (of class $C^\omega$ ) between the configuration space $Q$ and its model Euclidean space $\mathbb{R}^1$ (represented as $\text{EuclideanSpace } \mathbb{R} (\text{Fin } 1)$ ). This global coordinate chart upgrades the underlying coordinate homeomorphism to a smooth identification of the configuration manifold $Q$ with its model space $\mathbb{R}^1$ .

instance

Normed additive commutative group structure on the tangent space $T_q Q$

#instNormedAddCommGroupTangent

For any configuration $q$ in the configuration space $Q$ of the one-dimensional harmonic oscillator, the tangent space $T_q Q$ is endowed with the structure of a normed additive commutative group. This structure is induced by the model space $\mathbb{R}^1$ (represented as $\text{EuclideanSpace } \mathbb{R} (\text{Fin } 1)$ ).

instance

Normed real vector space structure on the tangent space $T_q Q$

#instNormedSpaceTangent

For any configuration $q$ in the configuration space $Q$ of the one-dimensional harmonic oscillator, the tangent space $T_q Q$ is endowed with the structure of a normed vector space over $\mathbb{R}$ . This structure is induced by the model space $\mathbb{R}^1$ (represented as $\text{EuclideanSpace } \mathbb{R} (\text{Fin } 1)$ ).

definition

Continuous linear equivalence between $T_q Q$ and $\mathbb{R}^1$

#tangentCoord

For any configuration $q$ in the configuration space $Q$ of the one-dimensional harmonic oscillator, $\text{tangentCoord}(q)$ is the continuous linear equivalence between the tangent space $T_q Q$ and the Euclidean model space $\mathbb{R}^1$ (represented as $\text{EuclideanSpace } \mathbb{R} (\text{Fin } 1)$ ). This identification is induced by the manifold's global coordinate chart.

instance

Tangent Spaces of the Configuration Space $Q$ are Finite-Dimensional

#instFiniteDimensionalTangent

For any configuration $q$ in the configuration space $Q$ of the one-dimensional harmonic oscillator, the tangent space $T_q Q$ (associated with the smooth manifold structure modeled on $\mathbb{R}^1$ ) is a finite-dimensional vector space over $\mathbb{R}$ .

Physlib.ClassicalMechanics.HarmonicOscillator.Geometric.Basic

Configuration space of the harmonic oscillator

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. The configuration space type

B. Topology and coordinate homeomorphism

C. Smooth manifold structure

D. The coordinate diffeomorphism

E. Tangent-coordinate infrastructure

F. Map to physical space

x(i)=x.val(i)x(i) = x.\text{val}(i)x(i)=x.val(i) for configurations in QQQ

Topological space structure on the configuration space QQQ

Coordinate equivalence Q≃E1Q \simeq \mathbb{E}^1Q≃E1

The configuration space QQQ is a Hausdorff space

The configuration space QQQ is second-countable

Charted space structure on the configuration space QQQ modeled on R1\mathbb{R}^1R1

The Configuration Space QQQ is an Analytic Manifold Modeled on R1\mathbb{R}^1R1

Analytic diffeomorphism Q≃R1Q \simeq \mathbb{R}^1Q≃R1

Normed additive commutative group structure on the tangent space TqQT_q QTq​Q

Normed real vector space structure on the tangent space TqQT_q QTq​Q

Continuous linear equivalence between TqQT_q QTq​Q and R1\mathbb{R}^1R1

Tangent Spaces of the Configuration Space QQQ are Finite-Dimensional

$x(i) = x.\text{val}(i)$ for configurations in $Q$

Topological space structure on the configuration space $Q$

Coordinate equivalence $Q \simeq \mathbb{E}^1$

The configuration space $Q$ is a Hausdorff space

The configuration space $Q$ is second-countable

Charted space structure on the configuration space $Q$ modeled on $\mathbb{R}^1$

The Configuration Space $Q$ is an Analytic Manifold Modeled on $\mathbb{R}^1$

Analytic diffeomorphism $Q \simeq \mathbb{R}^1$

Normed additive commutative group structure on the tangent space $T_q Q$

Normed real vector space structure on the tangent space $T_q Q$

Continuous linear equivalence between $T_q Q$ and $\mathbb{R}^1$

Tangent Spaces of the Configuration Space $Q$ are Finite-Dimensional