map_comp — Mathlib

English

There is a map between cotangent spaces compatible with algebra maps.

Русский

Существует отображение между котангентовыми пространствами, совместимое с алгебраическими отображениями.

LaTeX

$$$$ \mathrm{Cotangent}.map f : P.Cotangent \to P'.Cotangent $$$$

Lean4

theorem map_comp (f : Hom P P') (g : Hom P' P'') : Cotangent.map (g.comp f) = (map g).restrictScalars S ∘ₗ map f :=
  by
  ext x
  obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
  simp only [map_mk, Hom.toAlgHom_apply, Hom.comp_toRingHom, RingHom.coe_comp, Function.comp_apply, val_mk,
    LinearMap.coe_comp, LinearMap.coe_restrictScalars]

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