English
If P1 → P2 is a morphism of extensions and both are formally smooth, then the map in H1Cotangent induced by the morphism agrees with the corresponding map on H1Cotangent through the equivalence of FormallySmooth extensions.
Русский
Если P1 → P2 является морфизмом расширений, и оба расширения формально гладкие, то отображение между H1Cotangent, индуцированное морфизмом, согласуется с соответствующим отображением на H1Cotangent через эквивалентность формально гладких расширений.
LaTeX
$$equivOfFormallySmooth(P1,P2).toLinearMap = map f$$
Lean4
/-- Given extensions `0 → I₁ → P₁ → S → 0` and `0 → I₂ → P₂ → S → 0` with `P₁` formally smooth,
this is an arbitrarily chosen map `P₁/I₁² → P₂/I₂²` of extensions.
-/
noncomputable def homInfinitesimal (P₁ P₂ : Extension R S) [FormallySmooth R P₁.Ring] :
P₁.infinitesimal.Hom P₂.infinitesimal :=
letI lift : P₁.Ring →ₐ[R] P₂.infinitesimal.Ring :=
FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring S)
(IsScalarTower.toAlgHom R P₂.infinitesimal.Ring S) P₂.infinitesimal.algebraMap_surjective
⟨2, show P₂.infinitesimal.ker ^ 2 = ⊥ by rw [ker_infinitesimal]; exact Ideal.cotangentIdeal_square _⟩
{ toRingHom :=
(Ideal.Quotient.liftₐ (P₁.ker ^ 2) lift
(by
change P₁.ker ^ 2 ≤ RingHom.ker lift
rw [pow_two, Ideal.mul_le]
have : ∀ r ∈ P₁.ker, lift r ∈ P₂.infinitesimal.ker := fun r hr ↦
(FormallySmooth.liftOfSurjective_apply _ (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring S) _ _ r).trans
hr
intro r hr s hs
rw [RingHom.mem_ker, map_mul, ← Ideal.mem_bot, ← P₂.ker.cotangentIdeal_square, ← ker_infinitesimal, pow_two]
exact Ideal.mul_mem_mul (this r hr) (this s hs))).toRingHom
toRingHom_algebraMap := by simp
algebraMap_toRingHom
x := by
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
exact FormallySmooth.liftOfSurjective_apply _ (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring S) _ _ x }
