Category:Geometric Rotations

From ProofWiki
Jump to navigation Jump to search

This category contains results about rotations in the context of Euclidean Geometry.
Definitions specific to this category can be found in Definitions/Geometric Rotations.


A rotation in the context of Euclidean geometry is an isometry from a Euclidean Space $\R^n$ as follows.

A rotation is defined usually for either:

$n = 2$, representing the plane

or:

$n = 3$, representing ordinary space.


Rotation in the Plane

A rotation $r_\alpha$ in the plane is an isometry on the Euclidean Space $\Gamma = \R^2$ as follows.


Let $O$ be a distinguished point in $\Gamma$, which has the property that:

$\map {r_\alpha} O = O$

That is, $O$ maps to itself.


Let $P \in \Gamma$ such that $P \ne O$.

Let $OP$ be joined by a straight line.

Let a straight line $OP'$ be constructed such that:

$(1): \quad OP' = OP$
$(2): \angle POP' = \alpha$ such that $OP \to OP'$ is in the anticlockwise direction:
Rotation-in-Plane.png


Then:

$\map {r_\alpha} P = P'$

Thus $r_\alpha$ is a rotation (in the plane) of (angle) $\alpha$ about (the axis) $O$.


Rotation in Space

A rotation $r_\theta$ in space is an isometry on the Euclidean Space $\Gamma = \R^3$ as follows.


Let $AB$ be a distinguished straight line in $\Gamma$, which has the property that:

$\forall P \in AB: \map {r_\theta} P = P$

That is, all points on $AB$ map to themselves.


Let $P \in \Gamma$ such that $P \notin AB$.

Let a straight line be constructed from $P$ to $O$ on $AB$ such that $OP$ is perpendicular to $AB$.

Let a straight line $OP'$ be constructed perpendicular to $AB$ such that:

$(1): \quad OP' = OP$
$(2): \quad \angle POP' = \theta$ such that $OP \to OP'$ is in the anticlockwise direction:


Rotation-in-Space.png


Then:

$\map {r_\theta} P = P'$

Thus $r_\theta$ is a rotation (in space) of (angle) $\theta$ about (the axis) $O$.