ker_kerSquareLift — Mathlib

English

The kernel of the lifted map kerSquareLift is exactly the cotangent ideal of ker f.

Русский

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

LaTeX

$$\ker( f^{\mathrm{kerSquareLift}} ) = \cotangentIdeal( \ker f )$$

Lean4

theorem _root_.AlgHom.ker_kerSquareLift (f : A →ₐ[R] B) :
    RingHom.ker f.kerSquareLift.toRingHom = (RingHom.ker f.toRingHom).cotangentIdeal :=
  by
  apply le_antisymm
  · intro x hx; obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x; exact ⟨x, hx, rfl⟩
  · rintro _ ⟨x, hx, rfl⟩; exact hx

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