isStandardSmoothOfRelativeDimension

English

If there exists an IsStandardSmoothOfRelativeDimension n R S, then S is standard smooth over R.

Русский

Если существует IsStandardSmoothOfRelativeDimension n R S, то S является стандартно гладким над R.

LaTeX

$$$\text{IsStandardSmoothOfRelativeDimension}(n,R,S) \Rightarrow \mathrm{IsStandardSmooth}(R,S)$$$

Lean4

theorem isStandardSmoothOfRelativeDimension [Finite ι] (P : SubmersivePresentation R S ι σ) (hP : P.dimension = n) :
    IsStandardSmoothOfRelativeDimension n R S :=
  by
  refine ⟨⟨_, _, _, inferInstance, P.reindex (Fintype.equivFin _).symm (Fintype.equivFin σ).symm, ?_⟩⟩
  simp [hP]

Похожие утверждения