General covering maps

Covering-map lemmas that hold for arbitrary topological spaces and extend Mathlib.Topology.Covering.Basic at the pinned revision.

isCoveringMap_prodMap_id was extracted here by MO1.12 (#1323) from the GL⁺(2, ℝ) cover's coordinate argument, where it was stated and proved. Its statement quantifies over three arbitrary topological spaces and mentions no matrix, no phase and no stability condition, so the ledger's row 08 places general covering lemmas with the topology owner rather than beside the group they were first needed for.

The declaration keeps the fully qualified name it was introduced under, per the cutover ledger's first standing decision: paths move, namespaces do not. The namespace therefore reads oddly here, and that is recorded rather than repaired.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.isCoveringMap_prodMap_id {E : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace E] [TopologicalSpace X] [TopologicalSpace Y] {f : E → X} (hf : IsCoveringMap f) : IsCoveringMap (Prod.map f id)

A covering map remains a covering map after taking its product with an identity map.