English
Two different ways of forming a difference of cotangent-space maps are equal: map_sub_map(f,g) equals the other representation via restriction and composition.
Русский
Две различные формы разности отображений котантпространств равны друг другу через ограничение и композицию.
LaTeX
$$$\\mathrm{map\\_sub\\_map}(f,g) = (f.\\mathrm{sub}) \\circ (g.\\mathrm{sub})$$$
Lean4
theorem map_sub_map (f g : Hom P P') : map f - map g = (f.sub g) ∘ₗ P.cotangentComplex :=
by
ext x
obtain ⟨x, rfl⟩ := mk_surjective x
simp only [LinearMap.sub_apply, map_mk, LinearMap.coe_comp, Function.comp_apply, cotangentComplex_mk, Hom.sub_tmul,
one_smul, val_mk]
apply (Ideal.cotangentEquivIdeal _).injective
ext
simp only [val_sub, val_mk, map_sub, AddSubgroupClass.coe_sub, Ideal.cotangentEquivIdeal_apply,
Ideal.toCotangent_to_quotient_square, Submodule.mkQ_apply, Ideal.Quotient.mk_eq_mk, Hom.subToKer_apply_coe,
Hom.toAlgHom_apply]
