English
The evaluation of the equivalence (equivOfFormallySmooth) on an element x of P.H1Cotangent equals the application of map f on x; i.e., the equivalence agrees with the underlying map on H1Cotangent.
Русский
Оценка эквивалентности (equivOfFormallySmooth) на элемент x из P.H1Cotangent равна применению отображения map f к x; эквивалентность совпадает с базовым отображением на H1Cotangent.
LaTeX
$$$(equivOfFormallySmooth P_1 P_2).toLinearMap(x) = map f(x)$$$
Lean4
theorem equivOfFormallySmooth_toLinearMap {P₁ P₂ : Extension R S} (f : P₁.Hom P₂) [FormallySmooth R P₁.Ring]
[FormallySmooth R P₂.Ring] : (H1Cotangent.equivOfFormallySmooth P₁ P₂).toLinearMap = map f :=
by
ext1 x
refine (LinearEquiv.symm_apply_eq _).mpr ?_
change
((map (P₁.homInfinitesimal P₂)).restrictScalars S ∘ₗ map P₁.toInfinitesimal) x =
((map P₂.toInfinitesimal).restrictScalars S ∘ₗ map f) x
rw [← map_comp, ← map_comp, map_eq]
