English
If f: P → S is a surjective algebra map with square-zero kernel and P is formally smooth over R, then Ω[S/R] is projective and I/I² → S ⊗P Ω[P/R] is injective. This combines Jacobian-type criteria with differential invariants.
Русский
Если f: P → S — сюръекция с ядером I^2 = 0 и P формально гладко над R, тогда модуль Ω[S/R]Projective, и I/I^2 → S ⊗P Ω[P/R] инъективен. Это сочетает критерий Якобиана с дифференциальными invariантами.
LaTeX
$$$\\Omega_{S/R}$ projective and $I/I^2 \\hookrightarrow S\\otimes_P \\Omega[P/R]$ injective$$
Lean4
/-- Given a surjective algebra homomorphism `f : P →ₐ[R] S` with kernel `I`,
there is a one-to-one correspondence between `P`-linear retractions of `I/I² →ₗ[P] S ⊗[P] Ω[P/R]`
and algebra homomorphism sections of `f‾ : P/I² → S`.
-/
noncomputable def retractionKerCotangentToTensorEquivSection :
{ l // l ∘ₗ (kerCotangentToTensor R P S) = LinearMap.id } ≃
{ g // (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S } :=
by
let P' := P ⧸ (RingHom.ker (algebraMap P S) ^ 2)
have h₁ : Surjective (algebraMap P' S) := Function.Surjective.of_comp (g := algebraMap P P') hf
have h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥ := by
rw [RingHom.algebraMap_toAlgebra, AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]
let e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] (RingHom.ker (algebraMap P' S)) :=
(Ideal.cotangentEquivIdeal _).trans
((LinearEquiv.ofEq _ _ (IsScalarTower.toAlgHom R P S).ker_kerSquareLift.symm).restrictScalars P)
let e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := (tensorKaehlerQuotKerSqEquiv R P S).restrictScalars P
have H : kerCotangentToTensor R P S = e₂.toLinearMap ∘ₗ (kerToTensor R P' S).restrictScalars P ∘ₗ e₁.toLinearMap :=
by
ext x
obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
exact (tensorKaehlerQuotKerSqEquiv_tmul_D 1 x.1).symm
refine Equiv.trans ?_ (retractionKerToTensorEquivSection (R := R) h₂ h₁)
refine
⟨fun ⟨l, hl⟩ ↦ ⟨⟨e₁.toLinearMap ∘ₗ l ∘ₗ e₂.toLinearMap, ?_⟩, ?_⟩, fun ⟨l, hl⟩ ↦
⟨e₁.symm.toLinearMap ∘ₗ l.restrictScalars P ∘ₗ e₂.symm.toLinearMap, ?_⟩, ?_, ?_⟩
· rintro x y
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
simp only [P', ← Ideal.Quotient.algebraMap_eq, IsScalarTower.algebraMap_smul]
exact (e₁.toLinearMap ∘ₗ l ∘ₗ e₂.toLinearMap).map_smul x y
· ext1 x
rw [H] at hl
obtain ⟨x, rfl⟩ := e₁.surjective x
exact DFunLike.congr_arg e₁ (LinearMap.congr_fun hl x)
· ext x
rw [H]
apply e₁.injective
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, LinearMap.coe_restrictScalars, Function.comp_apply,
LinearEquiv.symm_apply_apply, LinearMap.id_coe, id_eq, LinearEquiv.apply_symm_apply]
exact LinearMap.congr_fun hl (e₁ x)
· intro f
ext x
simp only [AlgebraTensorModule.curry_apply, Derivation.coe_comp, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
Derivation.coeFn_coe, Function.comp_apply, curry_apply, LinearEquiv.coe_coe, LinearMap.coe_mk, AddHom.coe_coe,
LinearEquiv.apply_symm_apply, LinearEquiv.symm_apply_apply]
· intro f
ext x
simp only [AlgebraTensorModule.curry_apply, Derivation.coe_comp, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
Derivation.coeFn_coe, Function.comp_apply, curry_apply, LinearMap.coe_mk, AddHom.coe_coe, LinearEquiv.coe_coe,
LinearEquiv.symm_apply_apply, LinearEquiv.apply_symm_apply]
