The codimension of a nonempty closed submanifold is unique

IsClosedSubmanifold ψ Y c carries the codimension c as a label; for Y = ∅ every c is legitimate (isClosedSubmanifold_empty'), so the codimension chosen from the monoidality witnesses of a finite succession (FiniteSuccession.codim) is not determined by the centre in general. For a nonempty Y it is: two adapted charts φ (for ψ, σ, codimension c) and φ' (for ψ', σ', codimension c') at a point a ∈ Y read Y as the coordinate subspaces {z_σ = 0} ≅ 𝕜^{n-c} and {z_{σ'} = 0} ≅ 𝕜^{n'-c'}; the chart change between the two induced charts of Y (IsAdaptedChart.chartOn) is analytic with analytic inverse, so its derivative at the point is a linear isomorphism 𝕜^{n-c} ≃ 𝕜^{n'-c'} and n - c = n' - c'; with c ≤ n, c' ≤ n' and n = n' (E ≃ 𝕜^n ≃ 𝕜^{n'}) this gives c = c' (IsClosedSubmanifold.codim_eq_of_nonempty). The two chart models ψ, ψ' are allowed to differ because the chart chosen for a succession need not be the one a list of centres was written in.

Not in the sources (linear algebra of the chart change). It is used to match the codimensions of the centres when a blow-up sequence is pushed forward along a closed embedding ([Kol07, 30.3]; the empty-centre proviso is [Kol07, 32]), in Hironaka/Manifold/FiniteSuccession/Functor/ToSuccessionPushforward.lean.

theorem Manifold.IsAdaptedChart.sub_codim_eq_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n n' : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {ψ' : E ≃L[𝕜] Fin n' → 𝕜} {Y : Set M} {c c' : ℕ} {φ φ' : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {σ' : Fin c' ↪ Fin n'} (h : IsAdaptedChart ψ Y φ σ) (h' : IsAdaptedChart ψ' Y φ' σ') {a : M} (ha : a ∈ Y) (haφ : a ∈ φ.source) (haφ' : a ∈ φ'.source) : n - c = n' - c'

Two adapted charts at a common point of Y, for the models ψ : E ≃ 𝕜^n (codimension c) and ψ' : E ≃ 𝕜^{n'} (codimension c'), give n - c = n' - c': the chart change between the two induced charts of Y is analytic with analytic inverse, so its derivative at the point is a linear isomorphism 𝕜^{n-c} ≃ 𝕜^{n'-c'}.

theorem Manifold.IsClosedSubmanifold.codim_eq_of_nonempty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n n' : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {ψ' : E ≃L[𝕜] Fin n' → 𝕜} {Y : Set M} {c c' : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hY' : IsClosedSubmanifold ψ' Y c') (hne : Y.Nonempty) : c = c'

The codimension of a nonempty closed submanifold is unique, across chart models: if Y is a closed submanifold of codimension c for ψ : E ≃ 𝕜^n and of codimension c' for ψ' : E ≃ 𝕜^{n'}, and Y ≠ ∅, then c = c' (two adapted charts at a point of Y, IsAdaptedChart.sub_codim_eq_of_mem, with c ≤ n, c' ≤ n' and n = n'). For Y = ∅ the codimension is free (isClosedSubmanifold_empty'), the case Kollár's empty-blow-up convention [Kol07, 32] sets aside.