Module

IntegralLocalizationFiniteModel.lean

Nyll.SchemeTheory.RingTheory.IntegralLocalizationFiniteModel

1 declaration indexed from sourceView source ↗

Module documentation

Finite models of localizations of integral algebras

If a principal localization of an integral algebra is of finite type, finitely many numerators of algebra generators already generate that localization. They can be adjoined together with any prescribed finite set before localizing. The resulting subalgebra is finite as a module by integrality.

Imports4

Mathlib.RingTheory.FiniteType
Mathlib.RingTheory.IntegralClosure.Algebra.Defs
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Mathlib.RingTheory.Localization.Away.Basic

Imported by2

theorem

exists_finite_subalgebra_awayMap_bijective_of_finiteType

L33 ↗

Algebra.exists_finite_subalgebra_awayMap_bijective_of_finiteType

Documentation

A principal localization of an integral algebra that is of finite type comes from a finite subalgebra containing any prescribed finite set and the element being inverted. The comparison is the canonical localization 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_subalgebra_awayMap_bijective_of_finiteType
    {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
    [Algebra.IsIntegral R C] (b : C) [Algebra.FiniteType R (Localization.Away b)]
    (T : Set C) (hT : T.Finite) :
    ∃ S : Subalgebra R C, Module.Finite R S ∧ T ⊆ S ∧ ∃ hb : b ∈ S,
      Function.Bijective (Localization.awayMap S.val.toRingHom ⟨b, hb⟩)

Module documentation

Finite models of localizations of integral algebras

Declarations

exists_finite_subalgebra_awayMap_bijective_of_finiteType