iff_unramified_and_smooth — Mathlib

English

A morphism of algebras is formally étale if and only if it is formally unramified and formally smooth.

Русский

Отображение алгебр формально étale тогда и только тогда, когда оно формально нерасчленимо и формально гладко.

LaTeX

$$$\text{FormallyEtale}(R,A) \iff (\text{FormallyUnramified}(R,A) \land \text{FormallySmooth}(R,A))$$$

Lean4

theorem iff_unramified_and_smooth : FormallyEtale R A ↔ FormallyUnramified R A ∧ FormallySmooth R A :=
  by
  rw [FormallyUnramified.iff_comp_injective, formallySmooth_iff, formallyEtale_iff]
  simp_rw [← forall_and, Function.Bijective]

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