NYLL
Module

JacobsonIdempotentRigidity.lean

Nyll.SchemeTheory.RingTheory.JacobsonIdempotentRigidity
2 declarations indexed from sourceView source ↗

Module documentation

Uniqueness of idempotents modulo a Jacobson ideal

An idempotent in the Jacobson radical vanishes, since its complement is a unit annihilating it. Applying this to the two complementary products shows that reduction modulo a Jacobson ideal is injective on idempotents.

Imports4
  • Mathlib.Algebra.Ring.Idempotent
  • Mathlib.RingTheory.Ideal.Quotient.Defs
  • Mathlib.RingTheory.Jacobson.Ideal
  • Mathlib.Tactic.Ring
Imported by3

Declarations

lemma

eq_zero_of_mem_jacobson

L28 ↗
IsIdempotentElem.eq_zero_of_mem_jacobson
Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u
namespace IsIdempotentElem
Lean source · statement
lemma eq_zero_of_mem_jacobson
    {R : Type u} [CommRing R] {e : R} (he : IsIdempotentElem e)
    (hmem : e ∈ Ideal.jacobson (⊥ : Ideal R)) : e = 0
theorem

eq_of_quotient_eq_of_le_jacobson

L41 ↗
IsIdempotentElem.eq_of_quotient_eq_of_le_jacobson
Documentation

Two idempotents with the same image modulo an ideal in the Jacobson radical are equal.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u
namespace IsIdempotentElem
Lean source · statement
theorem eq_of_quotient_eq_of_le_jacobson
    {R : Type u} [CommRing R] (J : Ideal R) (hJ : J ≤ Ideal.jacobson ⊥)
    {e f : R} (he : IsIdempotentElem e) (hf : IsIdempotentElem f)
    (hquot : Ideal.Quotient.mk J e = Ideal.Quotient.mk J f) : e = f

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.