FormallyEtale — Mathlib

English

The formality of etale for the algebra map equals the formality of etale for the ring map.

Русский

Формальная étale для алгебраического отображения совпадает с формальной étale для кольцевого отображения.

LaTeX

$$$(\text{algebraMap } R S).FormallyEtale \iff \text{Algebra.FormallyEtale } R S$$$

Lean4

/-- A ring homomorphism `R →+* A` is formally étale if it is formally unramified and formally smooth.
See `Algebra.FormallyEtale`.
-/
@[algebraize Algebra.FormallyEtale]
def FormallyEtale (f : R →+* S) : Prop :=
  letI := f.toAlgebra
  Algebra.FormallyEtale R S

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