Module

LocalizationIdempotentFactor.lean

Nyll.SchemeTheory.RingTheory.LocalizationIdempotentFactor

4 declarations indexed from sourceView source ↗

Module documentation

Transporting an idempotent factor through a principal localization

If a map becomes bijective after inverting b, it identifies the factors on which an idempotent is 1, provided b is already a unit in the source factor. The comparison is the actual map induced on the two quotient rings. In particular, integrality of the source algebra passes to the target factor.

Imports7

Mathlib.Algebra.Group.Units.Basic
Mathlib.Algebra.Ring.Idempotent
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.Tactic.Ring

Imported by4

def

idempotentFactorMap

L37 ↗

AlgHom.idempotentFactorMap

Documentation

The map induced on the factors where e and f e become 1. The construction itself does not need idempotence.

Source context 4 commands

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

@[expose] public section
universe u v w
namespace AlgHom
variable {R : Type u} {C : Type v} {B : Type w}
  [CommRing R] [CommRing C] [CommRing B] [Algebra R C] [Algebra R B]

Lean source · statement

def idempotentFactorMap (f : C →ₐ[R] B) (e : C) :
    C ⧸ Ideal.span {1 - e} →ₐ[R] B ⧸ Ideal.span {1 - f e}

theorem

idempotentFactorMap_mk

L48 ↗

AlgHom.idempotentFactorMap_mk

Source context 4 commands

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

@[expose] public section
universe u v w
namespace AlgHom
variable {R : Type u} {C : Type v} {B : Type w}
  [CommRing R] [CommRing C] [CommRing B] [Algebra R C] [Algebra R B]

Lean source · statement

theorem idempotentFactorMap_mk (f : C →ₐ[R] B) (e c : C) :
    f.idempotentFactorMap e (Ideal.Quotient.mk (Ideal.span {1 - e}) c) =
      Ideal.Quotient.mk (Ideal.span {1 - f e}) (f c)

theorem

bijective_idempotentFactorMap_of_awayMap_bijective

L54 ↗

AlgHom.bijective_idempotentFactorMap_of_awayMap_bijective

Documentation

A bijective principal-localization map identifies an idempotent factor on which the element being inverted is already a unit.

Source context 4 commands

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

@[expose] public section
universe u v w
namespace AlgHom
variable {R : Type u} {C : Type v} {B : Type w}
  [CommRing R] [CommRing C] [CommRing B] [Algebra R C] [Algebra R B]

Lean source · statement

theorem bijective_idempotentFactorMap_of_awayMap_bijective
    (f : C →ₐ[R] B) (e : C) (he : IsIdempotentElem e) (b : C)
    (hb : IsUnit (Ideal.Quotient.mk (Ideal.span {1 - e}) b))
    (hf : Function.Bijective (Localization.awayMap f.toRingHom b)) :
    Function.Bijective (f.idempotentFactorMap e)

theorem

isIntegral_idempotentFactor_of_awayMap_bijective

L118 ↗

AlgHom.isIntegral_idempotentFactor_of_awayMap_bijective

Documentation

Under the same localization comparison, integrality of the source algebra implies integrality of the target idempotent factor.

Source context 4 commands

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

@[expose] public section
universe u v w
namespace AlgHom
variable {R : Type u} {C : Type v} {B : Type w}
  [CommRing R] [CommRing C] [CommRing B] [Algebra R C] [Algebra R B]

Lean source · statement

theorem isIntegral_idempotentFactor_of_awayMap_bijective
    [Algebra.IsIntegral R C] (f : C →ₐ[R] B)
    (e : C) (he : IsIdempotentElem e) (b : C)
    (hb : IsUnit (Ideal.Quotient.mk (Ideal.span {1 - e}) b))
    (hf : Function.Bijective (Localization.awayMap f.toRingHom b)) :
    Algebra.IsIntegral R (B ⧸ Ideal.span {1 - f e})

Module documentation

Transporting an idempotent factor through a principal localization

Declarations

idempotentFactorMap

idempotentFactorMap_mk

bijective_idempotentFactorMap_of_awayMap_bijective

isIntegral_idempotentFactor_of_awayMap_bijective