English
There is a natural equivalence between the extension-homomorphism data and the infinitesimal homomorphism data, allowing to transport structures across formally smooth extensions.
Русский
Существует естественное эквивалентное соответствие между данными гомоморфизмов расширения и данными инфинитезимального гомоморфизма, что позволяет переносить структуры через формально гладкие расширения.
LaTeX
$$$\\text{equivOfFormallySmooth}(P_1,P_2) : P_1.H1Cotangent \\simeq P_2.H1Cotangent$$$
Lean4
/-- Given a formally smooth `R`-algebra `P` and a surjective algebra homomorphism `f : P →ₐ[R] S`
with kernel `I` (typically a presentation `R[X] → S`),
`S` is formally smooth iff the `P`-linear map `I/I² → S ⊗[P] Ω[P⁄R]` is split injective.
-/
@[stacks 031I]
theorem formallySmooth_iff_split_injection (P : Algebra.Extension.{u} R S) [FormallySmooth R P.Ring] :
Algebra.FormallySmooth R S ↔ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id :=
by
refine (Algebra.FormallySmooth.iff_split_injection P.algebraMap_surjective).trans ?_
let e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent := { __ := AddEquiv.refl _, map_smul' r m := by ext1; simp; rfl }
constructor
· intro ⟨l, hl⟩
exact ⟨(e.comp l).extendScalarsOfSurjective P.algebraMap_surjective, LinearMap.ext (DFunLike.congr_fun hl : _)⟩
· intro ⟨l, hl⟩
exact ⟨e.symm.toLinearMap ∘ₗ l.restrictScalars P.Ring, LinearMap.ext (DFunLike.congr_fun hl : _)⟩
