English
If R ⟶ A and A ⟶ B are algebra morphisms and A,B are unramified over R and over A respectively, then R ⟶ B is unramified.
Русский
Если существуют алгебра-морфизмы R ⟶ A ⟶ B и A неразветвлено над R, а B неразветвлено над A, то R ⟶ B неразветвлено над R.
LaTeX
$$$[\text{Unramified } R \; A]\;[\text{Unramified } A \; B] \Rightarrow [\text{Unramified } R \; B]$$$
Lean4
theorem comp [FormallyUnramified R A] [FormallyUnramified A B] : FormallyUnramified R B :=
by
rw [iff_comp_injective]
intro C _ _ I hI f₁ f₂ e
have e' :=
FormallyUnramified.lift_unique I ⟨2, hI⟩ (f₁.comp <| IsScalarTower.toAlgHom R A B)
(f₂.comp <| IsScalarTower.toAlgHom R A B) (by rw [← AlgHom.comp_assoc, e, AlgHom.comp_assoc])
letI := (f₁.restrictDomain A).toAlgebra
let F₁ : B →ₐ[A] C := { f₁ with commutes' := fun r => rfl }
let F₂ : B →ₐ[A] C := { f₂ with commutes' := AlgHom.congr_fun e'.symm }
ext1 x
change F₁ x = F₂ x
congr
exact FormallyUnramified.ext I ⟨2, hI⟩ (AlgHom.congr_fun e)
