diff --git a/Physlib/SpaceAndTime/Space/API-map.yaml b/Physlib/SpaceAndTime/Space/API-map.yaml
new file mode 100644
index 000000000..76b5483f2
--- /dev/null
+++ b/Physlib/SpaceAndTime/Space/API-map.yaml
@@ -0,0 +1,93 @@
+version: v0.1
+
+Title: Space
+
+Overview: |
+    The key data structure is `Space d`, a structure with a single field `val : Fin d → ℝ`
+    modelling `d`-dimensional flat Euclidean space (default `d = 3`) with an arbitrary but
+    fixed choice of length unit and origin. The API equips it with metric/torsor,
+    vector-space, norm, inner-product and smooth-manifold structures, and the surrounding
+    definitions and lemmas (basis, coordinates, length units, cross product, slices,
+    derivatives of functions and distributions, and the actions of translations and rotations).
+
+ParentAPIs:
+  - "Distribution (Physlib/Mathematics/Distribution)"
+  - "Time (Physlib/SpaceAndTime/Time)"
+  - "Lorentz vectors (Physlib/Relativity/Tensors/RealTensor/Vector)"
+
+References:
+  - "Lean Zulip, #Physlib > Space vs EuclideanSpace: https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Space.20vs.20EuclideanSpace/with/575938877"
+
+Requirements:
+
+  - description: "The key data structure `Space d` (a structure with field `val : Fin d → ℝ`) is defined."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/Basic.lean (Space)"
+
+  - description: "The API contains the structure of an `ℝ`-vector space (module) on `Space d`."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/Module.lean (AddCommGroup (Space d), Module ℝ (Space d))"
+
+  - description: "The API contains a norm, an inner product and a metric on `Space d`, making it a finite-dimensional real inner-product space and metric space."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/Module.lean (Norm, InnerProductSpace ℝ (Space d)); Physlib/SpaceAndTime/Space/Basic.lean (Dist, MetricSpace)"
+
+  - description: "The API contains a choice of origin (the vector-space zero) and the standard affine-isometry chart to `EuclideanSpace`."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/Origin.lean (Zero (Space d), chartEuclidean)"
+
+  - description: "The API contains a smooth-manifold structure on `Space d` (charted space over and diffeomorphic to `EuclideanSpace ℝ (Fin d)`)."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/Basic.lean (homEuclideanSpaceSpace, ChartedSpace, IsManifold)"
+
+  - description: "The API contains basis vectors for `Space d`."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/Module.lean (basis : OrthonormalBasis (Fin d) ℝ (Space d))"
+
+  - description: "The API contains a `VSub` instance to `EuclideanSpace`."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/Basic.lean (VSub (EuclideanSpace ℝ (Fin d)) (Space d))"
+
+  - description: "The API contains a `NormedAddTorsor` instance from `EuclideanSpace`."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/Basic.lean (AddTorsor and NormedAddTorsor (EuclideanSpace ℝ (Fin d)) (Space d))"
+
+  - description: "The API contains translations of points and of distributions on space."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/Basic.lean (AddAction (EuclideanSpace ℝ (Fin d)) (Space d)); Physlib/SpaceAndTime/Space/Translations.lean (translateSchwartz, distTranslate)"
+
+  - description: "The API contains the action of the group of rotations on `Space d`."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/EuclideanGroup/Basic.lean (RotationGroup); Physlib/SpaceAndTime/Space/EuclideanGroup/Action.lean (MulAction (EuclideanGroup d) (Space d), rotation_smul_eq)"
+
+  - description: "The API contains the relation between Spaces of different dimensions."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/Slice.lean (slice : Space d.succ ≃L[ℝ] ℝ × Space d); Physlib/SpaceAndTime/Space/Module.lean (oneEquiv : Space 1 ≃ₗᵢ[ℝ] ℝ)"
+
+  - description: "The API contains the type `LengthUnit` of choices of length unit, with scaling and concrete units."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/LengthUnit.lean (LengthUnit, scale, meters)"
+
+  - description: "The API contains the cross product on `EuclideanSpace ℝ (Fin 3)` with properties relating it to time derivatives and inner products."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/CrossProduct.lean (⨯ₑ₃, time_deriv_cross_commute, inner_cross_self)"
+
+  - description: "The API contains the derivatives of functions from `Space` to normed spaces."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/Derivatives/Basic.lean (Space.deriv, notation ∂[·])"
+
+  - description: "The API contains the derivatives of functions from `Space` to manifolds."
+    done: false
+    location: N/A
+
+  - description: "The API contains a means of constructing distributions on `Space` from functions (via the `IsDistBounded` boundedness condition), including the constant and constant-slice distributions."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/IsDistBounded.lean (IsDistBounded); Physlib/SpaceAndTime/Space/DistOfFunction.lean (distOfFunction); Physlib/SpaceAndTime/Space/DistConst.lean (distConst); Physlib/SpaceAndTime/Space/ConstantSliceDist.lean (sliceSchwartz, constantSliceDist)"
+
+  - description: "The API contains the derivatives of distributions from `Space` to normed spaces."
+    done: true
+    location: "Physlib/SpaceAndTime/Space/Derivatives/Basic.lean (distDeriv); Physlib/SpaceAndTime/Space/Derivatives/Grad.lean (distGrad); Physlib/SpaceAndTime/Space/Derivatives/Div.lean (distDiv); Physlib/SpaceAndTime/Space/Derivatives/Curl.lean (distCurl)"
+
+  - description: "The API contains the derivatives of distributions from `Space` to manifolds."
+    done: false
+    location: N/A