English
There is a one-to-one correspondence between P-linear retractions l of the kernel-to-tensor construction kerToTensor and algebra homomorphism sections g of the surjective map f: P → S. This correspondence is realized by the map that sends a retraction l to the associated section g and conversely.
Русский
Существует взаимно однозначное соответствие между P-линейными редекциями l для построения kerToTensor и гомоморфными секциями g над отображением f: P → S, которое сюръективно. Это соответствие переводит редекцию l в секцию g и обратно.
LaTeX
$$$\\{\,l \\mid l \\circ (\\kerToTensor) = \\mathrm{id} \} \\cong {\\,g \\mid (IsScalarTower.toAlgHom R P S) \\circ g = \\mathrm{id} \\text{ on }S}$$$
Lean4
/-- Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`,
there is a one-to-one correspondence between `P`-linear retractions of `I →ₗ[P] S ⊗[P] Ω[P/R]`
and algebra homomorphism sections of `f`.
-/
noncomputable def retractionKerToTensorEquivSection :
{ l // l ∘ₗ (kerToTensor R P S) = LinearMap.id } ≃ { g // (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S }
where
toFun l := ⟨_, toAlgHom_comp_sectionOfRetractionKerToTensor _ l.2 hf' hf⟩
invFun g := ⟨_, retractionOfSectionOfKerSqZero_comp_kerToTensor _ hf' g.2⟩
left_inv
l := by
ext s p
obtain ⟨s, rfl⟩ := hf s
have (x y : _) : (l.1 x).1 * (l.1 y).1 = 0 := by rw [← Ideal.mem_bot, ← hf', pow_two];
exact Ideal.mul_mem_mul (l.1 x).2 (l.1 y).2
simp only [AlgebraTensorModule.curry_apply, Derivation.coe_comp, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
Derivation.coeFn_coe, Function.comp_apply, curry_apply, retractionOfSectionOfKerSqZero_tmul_D,
sectionOfRetractionKerToTensor_algebraMap, ← mul_sub, sub_sub_cancel]
rw [sub_mul]
simp only [this, Algebra.algebraMap_eq_smul_one, ← smul_tmul', LinearMapClass.map_smul, SetLike.val_smul,
smul_eq_mul, sub_zero]
right_inv g := by ext s; obtain ⟨s, rfl⟩ := hf s; simp
