equiv — Mathlib

English

If e: R ≃+* S is a ring equivalence, then the induced map e: R →+* S is standard-smooth of relative dimension 0.

Русский

Если e: R ≃+* S является изоморфизмом колец, то индуцированный отображение e: R →+* S является стандартно гладким относительно размерности 0.

LaTeX

$$$$ \forall R S [\mathrm{CommRing} R] [\mathrm{CommRing} S](e : R \cong+* S), \; \operatorname{IsStandardSmoothOfRelativeDimension}(0, (e : R \to+* S)). $$$$

Lean4

theorem equiv (e : R ≃+* S) : IsStandardSmoothOfRelativeDimension 0 (e : R →+* S) :=
  by
  algebraize [e.toRingHom]
  exact Algebra.IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective e.bijective

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