map_toComp_injective — Mathlib

English

If x is mapped to zero on the left-hand side under compEquiv_symm, then the lifted base change of x equals Extension.CotangentSpace.map (Q.toComp P).toExtensionHom applied to x.

Русский

Если элемент x попадает в ноль при применении compEquiv_symm слева, то взятое через базовое изменение отображение равно Extension.CotangentSpace.map (Q.toComp P).toExtensionHom применённому к x.

LaTeX

$$$$ (compEquiv(Q,P)).symm (0, x) = (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom).liftBaseChange T x. $$$$

Lean4

theorem map_toComp_injective :
    Function.Injective ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom).liftBaseChange T) :=
  by
  rw [← compEquiv_symm_inr]
  apply (compEquiv Q P).symm.injective.comp
  exact Prod.mk_right_injective _

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