Module

FinitePresentationAwayRelations.lean

Nyll.SchemeTheory.RingTheory.FinitePresentationAwayRelations

1 declaration indexed from sourceView source ↗

Module documentation

Extending finite relations from a principal open

Suppose a finite relation ideal vanishes under an algebra map after inverting one element. Multiplying its finitely many generators by suitable powers of that element gives a smaller finitely generated ideal in the actual kernel. The two ideals have equal extensions to the localization.

For a finite, finitely presented source algebra, its quotient by the new ideal is still finite and finitely presented and has an actual map to the target. Thus the relation correction preserves both the prescribed local relations and the target map. No Noetherian or integral-target hypothesis is needed for this step.

This is a ring-local ingredient for finite algebra approximation as used in Stacks, Tags 0817 and 09YZ. It does not assert the existence of compatible global algebra models or an extension of every algebra on an open subscheme.

Imports9

Mathlib.RingTheory.FinitePresentation
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Ideal.Defs
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Quotient.Defs
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.Localization.Defs
Mathlib.Tactic.Choose

Imported by1

Nyll.SchemeTheory.RingTheory.All

theorem

exists_finitePresentation_quotient_eq_map_away

L46 ↗

AlgHom.exists_finitePresentation_quotient_eq_map_away

Documentation

Finitely many relations which vanish after localization can be replaced by relations in the actual kernel, without changing their localized ideal. The resulting finite-FP quotient carries the original map to the target.

Source context 3 commands

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

noncomputable section
universe u v w
namespace AlgHom

Lean source · statement

theorem exists_finitePresentation_quotient_eq_map_away
    (R : Type u) [CommRing R] (A : Type v) [CommRing A] [Algebra R A]
    [Module.Finite R A] [Algebra.FinitePresentation R A]
    (B : Type w) [CommRing B] [Algebra R B]
    (φ : A →ₐ[R] B) (r : A) (I : Ideal A) (hI : I.FG)
    (hzero : ∀ a : A, a ∈ I →
      algebraMap B (Localization.Away (φ r)) (φ a) = 0) :
    ∃ J : Ideal A, J.FG ∧ J ≤ I ∧
      Module.Finite R (A ⧸ J) ∧ Algebra.FinitePresentation R (A ⧸ J) ∧
      ∃ ψ : A ⧸ J →ₐ[R] B,
        ψ.comp (Ideal.Quotient.mkₐ R J) = φ ∧
        J.map (algebraMap A (Localization.Away r)) =
          I.map (algebraMap A (Localization.Away r))

Module documentation

Extending finite relations from a principal open

Declarations

exists_finitePresentation_quotient_eq_map_away