Module

NativeNormalizationPrime.lean

Nyll.SchemeTheory.Normalization.NativeNormalizationPrime

4 declarations indexed from sourceView source ↗

Module documentation

Prime contraction in subalgebra normalizations

Proves faithfulness and lies-over properties for subalgebra normalizations. For faithful algebras over a discrete valuation ring, the contracted maximal prime is nonzero.

Imports4

Nyll.SchemeTheory.Normalization.SubalgebraPreimage
Mathlib.RingTheory.Ideal.GoingUp
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.DiscreteValuationRing.Basic

Imported by9

theorem

subalgebraNormalizationCommAlgCat_faithfulSMul

L25 ↗

SchemeTheory.subalgebraNormalizationCommAlgCat_faithfulSMul

Documentation

The actual normalization coefficient map remains faithful in every native subalgebra of the original faithful algebra.

Source context 2 commands

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

namespace SchemeTheory
universe u v

Lean source · statement

theorem subalgebraNormalizationCommAlgCat_faithfulSMul
    {A : Type u} {L : Type v} [CommRing A] [CommRing L]
    [Algebra A L] [FaithfulSMul A L] (S : Subalgebra A L) :
    FaithfulSMul A (subalgebraNormalizationCommAlgCat S)

theorem

normalizationCommAlgCat_liesOver_maximalIdeal

L36 ↗

SchemeTheory.normalizationCommAlgCat_liesOver_maximalIdeal

Documentation

A maximal prime of an actual normalization lies over the unique maximal ideal of the local coefficient ring.

Source context 2 commands

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

namespace SchemeTheory
universe u v

Lean source · statement

theorem normalizationCommAlgCat_liesOver_maximalIdeal
    {A : Type u} {L : Type v} [CommRing A] [IsLocalRing A]
    [CommRing L] [Algebra A L]
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsMaximal] :
    Q.LiesOver (IsLocalRing.maximalIdeal A)

theorem

subalgebraNormalizationPrime_liesOver_maximalIdeal

L49 ↗

SchemeTheory.subalgebraNormalizationPrime_liesOver_maximalIdeal

Documentation

Literal contraction into a native finite normalization preserves the original base prime.

Source context 2 commands

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

namespace SchemeTheory
universe u v

Lean source · statement

theorem subalgebraNormalizationPrime_liesOver_maximalIdeal
    {A : Type u} {L : Type v} [CommRing A] [IsLocalRing A]
    [CommRing L] [Algebra A L] (S : Subalgebra A L)
    (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal] :
    (Q.comap (subalgebraNormalizationRingMap S)).LiesOver (IsLocalRing.maximalIdeal A)

theorem

subalgebraNormalizationPrime_ne_bot

L60 ↗

SchemeTheory.subalgebraNormalizationPrime_ne_bot

Documentation

The actual contracted prime is nonzero because its original DVR coefficient maximal ideal is nonzero.

Source context 2 commands

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

namespace SchemeTheory
universe u v

Lean source · statement

theorem subalgebraNormalizationPrime_ne_bot
    {A : Type u} {L : Type v} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [CommRing L] [Algebra A L] [FaithfulSMul A L] (S : Subalgebra A L)
    (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal] :
    Q.comap (subalgebraNormalizationRingMap S) ≠ ⊥

Module documentation

Prime contraction in subalgebra normalizations

Declarations

subalgebraNormalizationCommAlgCat_faithfulSMul

normalizationCommAlgCat_liesOver_maximalIdeal

subalgebraNormalizationPrime_liesOver_maximalIdeal

subalgebraNormalizationPrime_ne_bot