English
If l and hl satisfy the right relations, then the map sectionOfRetractionKerToTensorAux l hl σ hσ hf' yields a morphism preserving ker-structure under algebra maps.
Русский
Если l и hl удовлетворяют нужным отношениям, секция сохраняет структуру ядра при алгебраических отображениях.
LaTeX
$$sectionOfRetractionKerToTensorAux l hl σ hσ hf' gives a homomorphism with ker structure$$
Lean4
/-- Given a surjective algebra homomorphism `f : P →ₐ[R] S` with square-zero kernel `I`.
Let `σ` be an arbitrary (set-theoretic) section of `f`.
Suppose we have a retraction `l` of the injection `I →ₗ[P] S ⊗[P] Ω[P/R]`, then
`x ↦ σ x - l (1 ⊗ D (σ x))` is an algebra homomorphism and a section to `f`.
-/
noncomputable def sectionOfRetractionKerToTensorAux : S →ₐ[R] P
where
toFun x := σ x - l (1 ⊗ₜ .D _ _ (σ x))
map_one' := by simp [sectionOfRetractionKerToTensorAux_prop l hl (σ 1) 1 (by simp [hσ])]
map_mul' a
b :=
by
have (x y : _) : (l x).1 * (l y).1 = 0 := by rw [← Ideal.mem_bot, ← hf', pow_two];
exact Ideal.mul_mem_mul (l x).2 (l y).2
simp only [sectionOfRetractionKerToTensorAux_prop l hl (σ (a * b)) (σ a * σ b) (by simp [hσ]), Derivation.leibniz,
tmul_add, tmul_smul, map_add, map_smul, Submodule.coe_add, SetLike.val_smul, smul_eq_mul, mul_sub, sub_mul, this,
sub_zero]
ring
map_add' a
b := by
simp only [sectionOfRetractionKerToTensorAux_prop l hl (σ (a + b)) (σ a + σ b) (by simp [hσ]), map_add, tmul_add,
Submodule.coe_add, add_sub_add_comm]
map_zero' := by simp [sectionOfRetractionKerToTensorAux_prop l hl (σ 0) 0 (by simp [hσ])]
commutes'
r := by
simp [sectionOfRetractionKerToTensorAux_prop l hl (σ (algebraMap R S r)) (algebraMap R P r)
(by simp [hσ, ← IsScalarTower.algebraMap_apply])]
