English
If g: S →+* T and f: R →+* S are standard-smooth with relative dimensions n and m respectively, then their composition g ∘ f is standard-smooth of relative dimension n + m.
Русский
Если g: S →+* T и f: R →+* S стандартно гладкие с относительными размерностями n и m, то их композиция g ∘ f гладка по отношению к размерности n + m.
LaTeX
$$$$ \forall {n m : \mathbb{N}} {R S T} [\mathrm{CommRing} R] [\mathrm{CommRing} S] [\mathrm{CommRing} T](g : S \to+* T)(f : R \to+* S), \; \operatorname{IsStandardSmoothOfRelativeDimension}(n, g) \to \operatorname{IsStandardSmoothOfRelativeDimension}(m, f) \to \operatorname{IsStandardSmoothOfRelativeDimension}(n + m, (g \circ f)). $$$$
Lean4
theorem comp {g : S →+* T} {f : R →+* S} (hg : IsStandardSmoothOfRelativeDimension n g)
(hf : IsStandardSmoothOfRelativeDimension m f) : IsStandardSmoothOfRelativeDimension (n + m) (g.comp f) :=
by
rw [IsStandardSmoothOfRelativeDimension]
algebraize [f, g, (g.comp f)]
exact Algebra.IsStandardSmoothOfRelativeDimension.trans m n R S T
