Module

IdempotentLiftSupport.lean

Nyll.SchemeTheory.RingTheory.IdempotentLiftSupport

1 declaration indexed from sourceView source ↗

Module documentation

Lifting quotient idempotents with prescribed open support

If the basic open of an idempotent in a quotient ring lies over an open subset of the original spectrum, it has a lift whose basic open is contained in that subset. The lift is obtained from a positive power and need not itself be idempotent.

Imports3

Mathlib.Algebra.Group.Idempotent
Mathlib.RingTheory.Ideal.Quotient.Defs
Mathlib.RingTheory.Spectrum.Prime.Topology

Imported by2

theorem

exists_lift_idempotent_basicOpen_le

L31 ↗

PrimeSpectrum.exists_lift_idempotent_basicOpen_le

Documentation

A quotient idempotent has a lift whose basic open lies in any prescribed open containing its image in the original spectrum. The lift is not asserted to be idempotent.

Source context 4 commands

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

@[expose] public section
universe u
open TopologicalSpace
namespace PrimeSpectrum

Lean source · statement

theorem exists_lift_idempotent_basicOpen_le {R : Type u} [CommRing R]
    (I : Ideal R) (e : R ⧸ I) (he : IsIdempotentElem e)
    (U : Opens (PrimeSpectrum R))
    (hU : basicOpen e ≤ Opens.comap
      ⟨comap (Ideal.Quotient.mk I), continuous_comap (Ideal.Quotient.mk I)⟩ U) :
    ∃ g : R, Ideal.Quotient.mk I g = e ∧ basicOpen g ≤ U

Module documentation

Lifting quotient idempotents with prescribed open support

Declarations

exists_lift_idempotent_basicOpen_le