NYLL
Module

RegularLocalRingRegularSequenceAscent.lean

Nyll.AlgebraicCurves.Geometry.Schemes.RegularLocalRingRegularSequenceAscent
18 declarations indexed from sourceView source ↗

Module documentation

Ascent of regular local rings through regular sequences

Regularity ascends from a quotient by a regular sequence. The final examples show how this applies to p-adic integers and why regularity of the sequence is necessary.

Imports1
Imported by2

Declarations

theorem

mem_nonZeroDivisors_of_isSMulRegular

L34 ↗
RegularLocalRingQuotientAscent.mem_nonZeroDivisors_of_isSMulRegular
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Preliminaries
variable {A : Type*} [CommRing A]
Lean source · statement
theorem mem_nonZeroDivisors_of_isSMulRegular {x : A} (h : IsSMulRegular A x) :
    x ∈ nonZeroDivisors A
theorem

ofList_ne_top_of_isRegular

L48 ↗
RegularLocalRingQuotientAscent.ofList_ne_top_of_isRegular
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Preliminaries
variable {A : Type*} [CommRing A]
Lean source · statement
theorem ofList_ne_top_of_isRegular {rs : List A} (h : Sequence.IsRegular A rs) :
    Ideal.ofList rs ≠ ⊤
theorem

mem_maximalIdeal_of_isRegular

L55 ↗
RegularLocalRingQuotientAscent.mem_maximalIdeal_of_isRegular
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Preliminaries
variable {A : Type*} [CommRing A]
Lean source · statement
theorem mem_maximalIdeal_of_isRegular [IsLocalRing A] {rs : List A}
    (h : Sequence.IsRegular A rs) :
    ∀ r ∈ rs, r ∈ maximalIdeal A
theorem

spanFinrank_ofList_le_length

L60 ↗
RegularLocalRingQuotientAscent.spanFinrank_ofList_le_length
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Preliminaries
variable {A : Type*} [CommRing A]
Lean source · statement
theorem spanFinrank_ofList_le_length (rs : List A) :
    (Ideal.ofList rs).spanFinrank ≤ rs.length
theorem

spanFinrank_maximalIdeal_le_quotient_ofList_add_length

L83 ↗
RegularLocalRingQuotientAscent.spanFinrank_maximalIdeal_le_quotient_ofList_add_length
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Ascent
variable {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
Lean source · statement
theorem spanFinrank_maximalIdeal_le_quotient_ofList_add_length (rs : List A)
    [IsLocalRing (A ⧸ Ideal.ofList rs)] :
    (maximalIdeal A).spanFinrank
      ≤ (maximalIdeal (A ⧸ Ideal.ofList rs)).spanFinrank + rs.length
theorem

isRegularLocalRing_of_isRegularLocalRing_quotient_ofList

L100 ↗
RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Ascent
variable {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
Lean source · statement
theorem isRegularLocalRing_of_isRegularLocalRing_quotient_ofList (rs : List A)
    (hreg : Sequence.IsRegular A rs)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.ofList rs)) :
    IsRegularLocalRing A
theorem

isRegularLocalRing_of_isRegularLocalRing_quotient_isWeaklyRegular

L116 ↗
RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_isWeaklyRegular
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Ascent
variable {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
Lean source · statement
theorem isRegularLocalRing_of_isRegularLocalRing_quotient_isWeaklyRegular (rs : List A)
    (hmem : ∀ r ∈ rs, r ∈ maximalIdeal A)
    (hreg : Sequence.IsWeaklyRegular A rs)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.ofList rs)) :
    IsRegularLocalRing A
theorem

isRegularLocalRing_of_isRegularLocalRing_quotient_regularSequence

L124 ↗
RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_regularSequence
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Ascent
variable {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
Lean source · statement
theorem isRegularLocalRing_of_isRegularLocalRing_quotient_regularSequence (rs : List A)
    (hmem : ∀ r ∈ rs, r ∈ maximalIdeal A)
    (hreg : Sequence.IsRegular A rs)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.ofList rs)) :
    IsRegularLocalRing A
theorem

isRegularLocalRing_of_surjective_ker_ofList

L132 ↗
RegularLocalRingQuotientAscent.isRegularLocalRing_of_surjective_ker_ofList
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Ascent
variable {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
Lean source · statement
theorem isRegularLocalRing_of_surjective_ker_ofList {B : Type*} [CommRing B]
    (f : A →+* B) (hf : Function.Surjective f) (rs : List A)
    (hker : RingHom.ker f = Ideal.ofList rs)
    (hreg : Sequence.IsRegular A rs)
    (hB : IsRegularLocalRing B) :
    IsRegularLocalRing A
theorem

isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_iterated

L148 ↗
RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_iterated
Source context 5 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section IteratedAscent
Lean source · statement
theorem isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_iterated :
    ∀ (n : ℕ) (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (rs : List A),
      rs.length = n → Sequence.IsRegular A rs →
      IsRegularLocalRing (A ⧸ Ideal.ofList rs) → IsRegularLocalRing A
theorem

isRegularLocalRing_of_quotient_via_iterated_ascent

L202 ↗
RegularLocalRingQuotientAscent.isRegularLocalRing_of_quotient_via_iterated_ascent
Source context 5 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section IteratedAscent
Lean source · statement
theorem isRegularLocalRing_of_quotient_via_iterated_ascent
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (rs : List A)
    (hreg : Sequence.IsRegular A rs)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.ofList rs)) :
    IsRegularLocalRing A
theorem

gate_padicInt_isRegular_singleton_p

L216 ↗
RegularLocalRingQuotientAscent.gate_padicInt_isRegular_singleton_p
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Gates
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem gate_padicInt_isRegular_singleton_p :
    Sequence.IsRegular ℤ_[p] [(p : ℤ_[p])]
theorem

gate_padicInt_quotient_ofList_isRegularLocalRing

L230 ↗
RegularLocalRingQuotientAscent.gate_padicInt_quotient_ofList_isRegularLocalRing
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Gates
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem gate_padicInt_quotient_ofList_isRegularLocalRing :
    IsRegularLocalRing (ℤ_[p] ⧸ Ideal.ofList [(p : ℤ_[p])])
theorem

gate_isRegularLocalRing_padicInt_via_sequence

L235 ↗
RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_sequence
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Gates
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem gate_isRegularLocalRing_padicInt_via_sequence : IsRegularLocalRing ℤ_[p]
theorem

gate_isRegularLocalRing_padicInt_via_iterated_ascent

L241 ↗
RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_iterated_ascent
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Gates
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem gate_isRegularLocalRing_padicInt_via_iterated_ascent : IsRegularLocalRing ℤ_[p]
theorem

gate_padicInt_dimension_jump_length

L247 ↗
RegularLocalRingQuotientAscent.gate_padicInt_dimension_jump_length
Source context 6 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Gates
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem gate_padicInt_dimension_jump_length :
    ringKrullDim (ℤ_[p] ⧸ Ideal.ofList [(p : ℤ_[p])])
      + ([(p : ℤ_[p])].length : WithBot ℕ∞) = ringKrullDim ℤ_[p]
theorem

not_isRegular_dualNumber_singleton_eps

L258 ↗
RegularLocalRingQuotientAscent.not_isRegular_dualNumber_singleton_eps
Source context 5 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Teeth
Lean source · statement
theorem not_isRegular_dualNumber_singleton_eps :
    ¬ Sequence.IsRegular (DualNumber ℚ) [(DualNumber.eps : DualNumber ℚ)]
theorem

not_forall_isRegularLocalRing_of_quotient_ofList_dropping_isRegular

L264 ↗
RegularLocalRingQuotientAscent.not_forall_isRegularLocalRing_of_quotient_ofList_dropping_isRegular
Source context 5 commands

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

noncomputable section
open IsLocalRing RingTheory Pointwise
namespace RegularLocalRingQuotientAscent
universe u
section Teeth
Lean source · statement
theorem not_forall_isRegularLocalRing_of_quotient_ofList_dropping_isRegular :
    ¬ (∀ (A : Type) [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (rs : List A),
        (∀ r ∈ rs, r ∈ maximalIdeal A) → IsRegularLocalRing (A ⧸ Ideal.ofList rs) →
        IsRegularLocalRing A)

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