map_eq — Mathlib

English

If f and g are two morphisms P → P', then the induced H1Cotangent maps are equal whenever f = g.

Русский

Если f и g — два гомоморфизма P → P', то индуцированные отображения на H1Cotangent совпадают при равенстве f = g.

LaTeX

$$$\\text{If } f = g, \\text{ then } \\mathrm{map}(f) = \\mathrm{map}(g).$$$

Lean4

theorem map_eq (f g : Hom P P') : map f = map g := by
  ext x
  simp only [map_apply_coe]
  rw [← sub_eq_zero, ← Cotangent.val_sub, ← LinearMap.sub_apply, Cotangent.map_sub_map]
  simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.map_coe_ker, map_zero, Cotangent.val_zero]

Похожие утверждения