English
Equiv_of_FormallySmooth applied to a linear map equals the corresponding map after transporting along the extension map; i.e., the equivalence commutes with the extension map.
Русский
Применение эквивалента к формально гладкому расширению к линейному отображению равно соответствующему отображению после переноса вдоль отображения расширения; эквивалентность сохраняет переносы.
LaTeX
$$$(H1Cotangent.equivOfFormallySmooth P_1 P_2).toLinearMap = map f$$$
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`),
then `S` is formally smooth iff `I/I² → S ⊗[P] Ω[S⁄R]` is injective and
`S ⊗[P] Ω[P⁄R] → Ω[S⁄R]` is split surjective.
-/
theorem iff_injective_and_split :
Algebra.FormallySmooth R S ↔
Function.Injective (kerCotangentToTensor R P S) ∧
∃ l, (KaehlerDifferential.mapBaseChange R P S) ∘ₗ l = LinearMap.id :=
by
rw [Algebra.FormallySmooth.iff_split_injection hf]
refine (and_iff_right (KaehlerDifferential.mapBaseChange_surjective R _ _ hf)).symm.trans ?_
refine
Iff.trans
(((exact_kerCotangentToTensor_mapBaseChange R _ _ hf).split_tfae' (g :=
(KaehlerDifferential.mapBaseChange R P S).restrictScalars P)).out
1 0)
(and_congr Iff.rfl ?_)
rw [(LinearMap.extendScalarsOfSurjectiveEquiv hf).surjective.exists]
simp only [LinearMap.ext_iff, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply,
LinearMap.extendScalarsOfSurjective_apply, LinearMap.id_coe, id_eq]
