Module

IntegralFinitePresentationModel.lean

Nyll.SchemeTheory.RingTheory.IntegralFinitePresentationModel

1 declaration indexed from sourceView source ↗

Module documentation

Finite, finitely presented models for finite sets of integral elements

Each finite subset of an integral algebra is contained in the image of an actual finite, finitely presented algebra over the original base. The model is constructed by successively adjoining roots of the elements' monic polynomials. No Noetherian hypothesis on the base is needed.

This is a ring-local precursor to the finite-presentation refinement in Stacks Project, Tag 09Z0. A filtered diagram, its colimit comparison, and a global relative-Spec approximation are separate constructions.

Imports9

Mathlib.Algebra.Category.CommAlgCat.Basic
Mathlib.Algebra.Polynomial.Eval.Coeff
Mathlib.Algebra.Polynomial.Monic
Mathlib.Data.Finset.Empty
Mathlib.Data.Finset.Insert
Mathlib.RingTheory.AdjoinRoot
Mathlib.RingTheory.FinitePresentation
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.IntegralClosure.Algebra.Defs

Imported by2

theorem

exists_finitePresentation_range_finset

L40 ↗

Algebra.IsIntegral.exists_finitePresentation_range_finset

Documentation

A finite set in an integral algebra lifts to an actual finite, finitely presented algebra. The source model lies in the universe of the base ring, even when the target algebra lies in a different universe.

Source context 3 commands

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

noncomputable section
universe u v
namespace Algebra.IsIntegral

Lean source · statement

theorem exists_finitePresentation_range_finset
    (R : Type u) (B : Type v) [CommRing R] [CommRing B] [Algebra R B]
    [Algebra.IsIntegral R B] (s : Finset B) :
    ∃ A : CommAlgCat.{u} R, Module.Finite R A ∧ Algebra.FinitePresentation R A ∧
      ∃ φ : A →ₐ[R] B, (s : Set B) ⊆ Set.range φ

Module documentation

Finite, finitely presented models for finite sets of integral elements

Declarations

exists_finitePresentation_range_finset