comp — Mathlib

English

If R ⟶ A ⟶ B are algebra maps with A unramified over R and B unramified over A, then B is unramified over R.

Русский

Если R ⟶ A ⟶ B — алгебра-гомоморфизмы, A неразветвлено над R, а B над A — неразветвлено, то B над R неразветвлено.

LaTeX

$$$[\text{Unramified } R A] \land [\text{Unramified } A B] \Rightarrow [\text{Unramified } R B]$$$

Lean4

/-- Unramified is stable under composition. -/
theorem comp [Algebra A B] [IsScalarTower R A B] [Unramified R A] [Unramified A B] : Unramified R B
    where
  formallyUnramified := FormallyUnramified.comp R A B
  finiteType := FiniteType.trans (S := A) Unramified.finiteType Unramified.finiteType

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