map_toCotangent_ker — Mathlib

English

The kernel of the cotangent map composed with the quotient map satisfies (LinearMap.ker I.toCotangent).map I.subtype = I^2.

Русский

Ядро отображения котонтangent состоит в том, что образ подмодуля ядра через отображение-подмодуль равен I^2.

LaTeX

$$$(\\ker I.toCotangent).map(I.subtype) = I^2$$$

Lean4

theorem map_toCotangent_ker : (LinearMap.ker I.toCotangent).map I.subtype = I ^ 2 := by
  rw [Ideal.toCotangent, Submodule.ker_mkQ, pow_two, Submodule.map_smul'' I ⊤ (Submodule.subtype I),
    Algebra.id.smul_eq_mul, Submodule.map_subtype_top]

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