NYLL
Module

PrincipalLocalizationModel.lean

Nyll.SchemeTheory.RingTheory.Descent.PrincipalLocalizationModel
2 declarations indexed from sourceView source ↗

Module documentation

Finitely presented models over actual principal localizations

Finitely many elements of a fraction field lie in a single principal localization of the original domain. Use the existing common-denominator construction and the actual localization subalgebra of the fraction field.

Applying this to the coefficients of an actual finite presentation constructs a model over that principal localization. The model is finitely presented over both the localization and the original ring, and its scalar extension to the original fraction field is the original algebra. No finite presentation of the entire fraction field over the original ring is assumed.

This is the finite-model prerequisite for Stacks, Tag 0BSM. Descent of the strict splitting isomorphism remains a separate step.

Imports9
  • Mathlib.Algebra.Algebra.Subalgebra.Tower
  • Mathlib.Algebra.Group.Submonoid.Membership
  • Mathlib.RingTheory.Extension.Presentation.Basic
  • Mathlib.RingTheory.Extension.Presentation.Core
  • Mathlib.RingTheory.FinitePresentation
  • Mathlib.RingTheory.Localization.AsSubring
  • Mathlib.RingTheory.Localization.Away.AdjoinRoot
  • Mathlib.RingTheory.Localization.FractionRing
  • Mathlib.RingTheory.Localization.Integer
Imported by1

Declarations

theorem

exists_principalLocalization_subalgebra_of_finset

L47 ↗
SchemeTheory.exists_principalLocalization_subalgebra_of_finset
Documentation

A finite set of fractions is contained in one actual principal localization subalgebra, which is finitely presented over the original ring.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u
variable (R K : Type u) [CommRing R] [IsDomain R] [Field K]
  [Algebra R K] [IsFractionRing R K]
Lean source · statement
theorem exists_principalLocalization_subalgebra_of_finset (s : Finset K) :
    ∃ (d : R), d ≠ 0 ∧ ∃ C : Subalgebra R K,
      IsLocalization.Away d C ∧ Algebra.FinitePresentation R C ∧
        ∀ x ∈ s, x ∈ C
theorem

exists_principalLocalization_finitePresentation_model

L72 ↗
SchemeTheory.exists_principalLocalization_finitePresentation_model
Documentation

A finitely presented fraction-field algebra has an actual model over a single principal localization. Its displayed base-ring algebra is compatible with the localization algebra and is itself finitely presented.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u
variable (R K : Type u) [CommRing R] [IsDomain R] [Field K]
  [Algebra R K] [IsFractionRing R K]
Lean source · statement
theorem exists_principalLocalization_finitePresentation_model
    (B : Type u) [CommRing B] [Algebra K B] [Algebra.FinitePresentation K B] :
    ∃ (d : R), d ≠ 0 ∧ ∃ C : Subalgebra R K,
      IsLocalization.Away d C ∧ Algebra.FinitePresentation R C ∧
      ∃ (B₀ : Type u) (_ : CommRing B₀) (_ : Algebra C B₀) (_ : Algebra R B₀),
        IsScalarTower R C B₀ ∧ Algebra.FinitePresentation C B₀ ∧
          Algebra.FinitePresentation R B₀ ∧ Nonempty ((K ⊗[C] B₀) ≃ₐ[K] B)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.