English
If A is formally smooth over R and B is formally smooth over A, then B is formally smooth over R.
Русский
Если A формально гладко над R, а B формально гладко над A, то B формально гладко над R.
LaTeX
$$$\operatorname{FormallySmooth}(R,A) \wedge \operatorname{FormallySmooth}(A,B) \Rightarrow \operatorname{FormallySmooth}(R,B)$$$
Lean4
theorem comp [FormallySmooth R A] [FormallySmooth A B] : FormallySmooth R B :=
by
constructor
intro C _ _ I hI f
obtain ⟨f', e⟩ := FormallySmooth.comp_surjective I hI (f.comp (IsScalarTower.toAlgHom R A B))
letI := f'.toRingHom.toAlgebra
obtain ⟨f'', e'⟩ := FormallySmooth.comp_surjective I hI { f.toRingHom with commutes' := AlgHom.congr_fun e.symm }
apply_fun AlgHom.restrictScalars R at e'
exact ⟨f''.restrictScalars _, e'.trans (AlgHom.ext fun _ => rfl)⟩
