of_comp — Mathlib

English

If B is an algebra over A and A is unramified over R with an appropriate tower, then B is unramified over R.

Русский

Если B является алгеброй над A, а A неразветвлено над R в рамках towers, то B неразветвлено над R.

LaTeX

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

Lean4

theorem of_comp [FormallyUnramified R B] : FormallyUnramified A B :=
  by
  rw [iff_comp_injective]
  intro Q _ _ I e f₁ f₂ e'
  letI := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
  letI : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
  refine AlgHom.restrictScalars_injective R ?_
  refine FormallyUnramified.ext I ⟨2, e⟩ ?_
  intro x
  exact AlgHom.congr_fun e' x

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