Module

IntegralLocalizationIdempotentModel.lean

Nyll.SchemeTheory.RingTheory.IntegralLocalizationIdempotentModel

3 declarations indexed from sourceView source ↗

Module documentation

Finite localization models preserving quotient idempotents

Ideal membership uses only finitely many coefficients. Including those coefficients in a finite subalgebra makes a quotient idempotent descend to that subalgebra. A finite-type principal localization can also be preserved.

Imports6

Nyll.SchemeTheory.RingTheory.IntegralLocalizationFiniteModel
Mathlib.Algebra.Group.Idempotent
Mathlib.LinearAlgebra.Span.Defs
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Quotient.Defs
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Imported by3

theorem

exists_finite_set_of_mem_map

L31 ↗

Algebra.exists_finite_set_of_mem_map

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 exists_finite_set_of_mem_map
    {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
    (I : Ideal R) {x : C} (hx : x ∈ I.map (algebraMap R C)) :
    ∃ T : Set C, T.Finite ∧ ∀ S : Subalgebra R C, T ⊆ S →
      ∃ y : S, (y : C) = x ∧ y ∈ I.map (algebraMap R S)

theorem

exists_finite_subalgebra_quotient_idempotent

L69 ↗

Algebra.exists_finite_subalgebra_quotient_idempotent

Documentation

A quotient idempotent in an integral algebra descends to the quotient of a finite subalgebra containing its representative.

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 exists_finite_subalgebra_quotient_idempotent
    {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
    [Algebra.IsIntegral R C] (I : Ideal R) (b : C)
    (hb : IsIdempotentElem (Ideal.Quotient.mk (I.map (algebraMap R C)) b)) :
    ∃ S : Subalgebra R C, Module.Finite R S ∧ ∃ hbS : b ∈ S,
      IsIdempotentElem
        (Ideal.Quotient.mk (I.map (algebraMap R S)) (⟨b, hbS⟩ : S))

theorem

exists_finite_subalgebra_idempotent_awayMap_bijective

L102 ↗

Algebra.exists_finite_subalgebra_idempotent_awayMap_bijective

Documentation

A quotient idempotent in an integral algebra has a finite subalgebra model in which it is still idempotent modulo the extended ideal. If localizing at the element is of finite type, the model has the same principal localization.

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 exists_finite_subalgebra_idempotent_awayMap_bijective
    {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
    [Algebra.IsIntegral R C] (I : Ideal R) (b : C)
    [Algebra.FiniteType R (Localization.Away b)]
    (hb : IsIdempotentElem (Ideal.Quotient.mk (I.map (algebraMap R C)) b)) :
    ∃ S : Subalgebra R C, Module.Finite R S ∧ ∃ hbS : b ∈ S,
      IsIdempotentElem
        (Ideal.Quotient.mk (I.map (algebraMap R S)) (⟨b, hbS⟩ : S)) ∧
      Function.Bijective (Localization.awayMap S.val.toRingHom ⟨b, hbS⟩)

Module documentation

Finite localization models preserving quotient idempotents

Declarations

exists_finite_set_of_mem_map

exists_finite_subalgebra_quotient_idempotent

exists_finite_subalgebra_idempotent_awayMap_bijective