Module

IdempotentLocalizationCyclicity.lean

Nyll.SchemeTheory.RingTheory.IdempotentLocalizationCyclicity

2 declarations indexed from sourceView source ↗

Module documentation

Cyclic quotient idempotents and principal localizations

A bijection on principal localizations identifies ideals extended from the base ring. Clearing the resulting denominator gives an ideal-membership statement in the source. For a quotient idempotent, multiplication by one additional copy of the idempotent removes this denominator, so cyclicity of its factor descends.

Imports5

Mathlib.Algebra.Group.Idempotent
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.Localization.Ideal

Imported by2

theorem

exists_pow_mul_mem_map_of_awayMap_bijective

L33 ↗

Algebra.exists_pow_mul_mem_map_of_awayMap_bijective

Documentation

A bijective map of principal localizations reflects membership in an ideal extended from the base, after multiplication by a power of the element inverted.

Source context 3 commands

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

@[expose] public section
universe u v w
namespace Algebra

Lean source · statement

theorem exists_pow_mul_mem_map_of_awayMap_bijective
    {R : Type u} {A : Type v} {B : Type w}
    [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    (f : A →ₐ[R] B) (I : Ideal R) (b : A)
    (hf : Function.Bijective (Localization.awayMap f.toRingHom b))
    {x : A} (hx : f x ∈ I.map (algebraMap R B)) :
    ∃ n : ℕ, b ^ n * x ∈ I.map (algebraMap R A)

theorem

cyclic_quotient_idempotent_of_awayMap_bijective

L81 ↗

Algebra.cyclic_quotient_idempotent_of_awayMap_bijective