chore(RingTheory/Smooth): split StandardSmooth (leanprover-community#28725)

We factor out the `SubmersivePresentation` part into a separate file to prepare for new content. Also the module docstrings and TODOs are updated.

Author: chrisflav

Mathlib.lean

@@ -5424,6 +5424,7 @@ import Mathlib.RingTheory.Extension.Cotangent.Basic
 import Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
 import Mathlib.RingTheory.Extension.Generators
 import Mathlib.RingTheory.Extension.Presentation.Basic
+import Mathlib.RingTheory.Extension.Presentation.Submersive
 import Mathlib.RingTheory.FilteredAlgebra.Basic
 import Mathlib.RingTheory.Filtration
 import Mathlib.RingTheory.FiniteLength