Module

JacobsonIdempotentFactor.lean

Nyll.SchemeTheory.RingTheory.JacobsonIdempotentFactor

1 declaration indexed from sourceView source ↗

Module documentation

Units on a lifted quotient factor

In an integral algebra over a Jacobson pair, an element congruent to the unit of a factor becomes a unit on that factor. The factor is the actual quotient by the complementary element, and its algebra structure comes from the base.

Imports3

Nyll.SchemeTheory.RingTheory.JacobsonIntegral
Nyll.SchemeTheory.RingTheory.QuotientBaseChange
Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Imported by4

theorem

isUnit_quotient_one_sub_of_eq_mod_extendedIdeal

L29 ↗

Algebra.isUnit_quotient_one_sub_of_eq_mod_extendedIdeal

Documentation

An element congruent to e modulo the extended Jacobson ideal is a unit after imposing e = 1. In particular, this applies to a lifted idempotent.

Source context 3 commands

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

@[expose] public section
universe u v
namespace Algebra

Lean source · statement

theorem isUnit_quotient_one_sub_of_eq_mod_extendedIdeal
    {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
    [Algebra.IsIntegral R C] (I : Ideal R) (hI : I ≤ Ideal.jacobson ⊥)
    (b e : C)
    (hbe : Ideal.Quotient.mk (I.map (algebraMap R C)) b =
      Ideal.Quotient.mk (I.map (algebraMap R C)) e) :
    IsUnit (Ideal.Quotient.mk (Ideal.span {1 - e}) b)

Module documentation

Units on a lifted quotient factor

Declarations

isUnit_quotient_one_sub_of_eq_mod_extendedIdeal