NYLL
Module

RegularLocalRingQuotientNonZeroDivisorAscent.lean

Nyll.AlgebraicCurves.Geometry.Schemes.RegularLocalRingQuotientNonZeroDivisorAscent
21 declarations indexed from sourceView source ↗

Module documentation

Lifting regularity through a non-zero-divisor quotient

Imports22
  • Mathlib.Algebra.Module.SpanRank
  • Mathlib.Algebra.Module.SpanRankOperations
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.RingTheory.Ideal.Quotient.Operations
  • Mathlib.RingTheory.Ideal.Quotient.Noetherian
  • Mathlib.RingTheory.RegularLocalRing.Defs
  • Mathlib.RingTheory.KrullDimension.Regular
  • Mathlib.RingTheory.KrullDimension.Zero
  • Mathlib.RingTheory.LocalRing.RingHom.Basic
  • Mathlib.RingTheory.Ideal.Cotangent
  • Mathlib.NumberTheory.Padics.RingHoms
  • Mathlib.NumberTheory.Padics.PadicIntegers
  • Mathlib.RingTheory.DualNumber
  • Mathlib.Algebra.DualNumber
  • Mathlib.Data.ZMod.Basic
  • Mathlib.Data.Set.Card
  • Mathlib.Data.Finset.Card
  • Mathlib.Algebra.Field.Rat
  • Mathlib.RingTheory.LocalRing.ResidueField.Basic
  • Mathlib.RingTheory.Noetherian.Basic
  • Mathlib.RingTheory.PrincipalIdealDomain
  • Mathlib.Tactic.Set
Imported by3

Declarations

theorem

spanFinrank_comap_le_of_surjective

L50 ↗
RegularLocalRingQuotientAscent.spanFinrank_comap_le_of_surjective
Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section GeneratorCounting
variable {A B : Type*} [CommRing A] [CommRing B]
Lean source · statement
theorem spanFinrank_comap_le_of_surjective {f : A →+* B} (hf : Function.Surjective f)
    {J : Ideal B} (hJ : Submodule.FG J) (hker : Submodule.FG (RingHom.ker f)) :
    (J.comap f).spanFinrank ≤ J.spanFinrank + (RingHom.ker f).spanFinrank
theorem

spanFinrank_maximalIdeal_le_of_surjective

L85 ↗
RegularLocalRingQuotientAscent.spanFinrank_maximalIdeal_le_of_surjective
Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section GeneratorCounting
variable {A B : Type*} [CommRing A] [CommRing B]
Lean source · statement
theorem spanFinrank_maximalIdeal_le_of_surjective [IsLocalRing A] [IsLocalRing B]
    [IsNoetherianRing B] (f : A →+* B) (hf : Function.Surjective f)
    (hker : Submodule.FG (RingHom.ker f)) :
    (maximalIdeal A).spanFinrank ≤ (maximalIdeal B).spanFinrank + (RingHom.ker f).spanFinrank
theorem

finrank_cotangentSpace_le_of_surjective

L97 ↗
RegularLocalRingQuotientAscent.finrank_cotangentSpace_le_of_surjective
Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section GeneratorCounting
variable {A B : Type*} [CommRing A] [CommRing B]
Lean source · statement
theorem finrank_cotangentSpace_le_of_surjective [IsLocalRing A] [IsLocalRing B]
    [IsNoetherianRing A] [IsNoetherianRing B] (f : A →+* B) (hf : Function.Surjective f) :
    Module.finrank (ResidueField A) (CotangentSpace A)
      ≤ Module.finrank (ResidueField B) (CotangentSpace B) + (RingHom.ker f).spanFinrank
theorem

isRegularLocalRing_of_isRegularLocalRing_quotient

L111 ↗
RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient
Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Ascent
variable {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
Lean source · statement
theorem isRegularLocalRing_of_isRegularLocalRing_quotient {x : A} (hx : x ∈ maximalIdeal A)
    (hnzd : x ∈ nonZeroDivisors A)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.span {x})) :
    IsRegularLocalRing A
theorem

isRegularLocalRing_of_surjective_ker_span_singleton

L139 ↗
RegularLocalRingQuotientAscent.isRegularLocalRing_of_surjective_ker_span_singleton
Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Ascent
variable {A : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
Lean source · statement
theorem isRegularLocalRing_of_surjective_ker_span_singleton {B : Type*} [CommRing B]
    (f : A →+* B) (hf : Function.Surjective f) {x : A}
    (hker : RingHom.ker f = Ideal.span {x}) (hx : x ∈ maximalIdeal A)
    (hnzd : x ∈ nonZeroDivisors A) (hB : IsRegularLocalRing B) :
    IsRegularLocalRing A
def

padicIntQuotientSpanPEquiv

L157 ↗
RegularLocalRingQuotientAscent.padicIntQuotientSpanPEquiv
Documentation

The residue ring of the p-adic integers is the field of integers modulo p.

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Gates
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def padicIntQuotientSpanPEquiv : (ℤ_[p] ⧸ Ideal.span {(p : ℤ_[p])}) ≃+* ZMod p
theorem

gate_padicInt_hypotheses

L161 ↗
RegularLocalRingQuotientAscent.gate_padicInt_hypotheses
Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Gates
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem gate_padicInt_hypotheses :
    (p : ℤ_[p]) ∈ maximalIdeal ℤ_[p] ∧ (p : ℤ_[p]) ∈ nonZeroDivisors ℤ_[p] ∧
      IsRegularLocalRing (ℤ_[p] ⧸ Ideal.span {(p : ℤ_[p])})
theorem

gate_isRegularLocalRing_padicInt

L171 ↗
RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt
Source context 5 commands

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

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

gate_padicInt_conclusion_consistency

L176 ↗
RegularLocalRingQuotientAscent.gate_padicInt_conclusion_consistency
Source context 5 commands

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

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

gate_padicInt_dimension_jump

L180 ↗
RegularLocalRingQuotientAscent.gate_padicInt_dimension_jump
Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Gates
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem gate_padicInt_dimension_jump :
    ringKrullDim (ℤ_[p] ⧸ Ideal.span {(p : ℤ_[p])}) + 1 = ringKrullDim ℤ_[p]
def

dualNumberFst

L191 ↗
RegularLocalRingQuotientAscent.dualNumberFst
Documentation

The ring homomorphism sending a dual number to its constant coefficient.

Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Teeth
Lean source · full declaration
def dualNumberFst (K : Type*) [CommRing K] : DualNumber K →+* K where
  toFun := TrivSqZeroExt.fst
  map_one' := TrivSqZeroExt.fst_one
  map_mul' := TrivSqZeroExt.fst_mul
  map_zero' := TrivSqZeroExt.fst_zero
  map_add' := TrivSqZeroExt.fst_add
theorem

dualNumberFst_apply

L198 ↗
RegularLocalRingQuotientAscent.dualNumberFst_apply
Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Teeth
Lean source · statement
theorem dualNumberFst_apply (K : Type*) [CommRing K] (x : DualNumber K) :
    dualNumberFst K x = TrivSqZeroExt.fst x
theorem

ker_dualNumberFst

L201 ↗
RegularLocalRingQuotientAscent.ker_dualNumberFst
Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Teeth
Lean source · statement
theorem ker_dualNumberFst (K : Type*) [CommRing K] :
    RingHom.ker (dualNumberFst K) = Ideal.span {(DualNumber.eps : DualNumber K)}
theorem

dualNumberFst_surjective

L207 ↗
RegularLocalRingQuotientAscent.dualNumberFst_surjective
Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Teeth
Lean source · statement
theorem dualNumberFst_surjective (K : Type*) [CommRing K] :
    Function.Surjective (dualNumberFst K)
def

dualNumberQuotientSpanEpsEquiv

L212 ↗
RegularLocalRingQuotientAscent.dualNumberQuotientSpanEpsEquiv
Documentation

Quotienting the dual numbers by the infinitesimal generator recovers the base ring.

Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Teeth
Lean source · statement
def dualNumberQuotientSpanEpsEquiv (K : Type*) [CommRing K] :
    (DualNumber K ⧸ Ideal.span {(DualNumber.eps : DualNumber K)}) ≃+* K
theorem

quotient_span_eps_isRegularLocalRing

L217 ↗
RegularLocalRingQuotientAscent.quotient_span_eps_isRegularLocalRing
Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Teeth
Lean source · statement
theorem quotient_span_eps_isRegularLocalRing :
    IsRegularLocalRing (DualNumber ℚ ⧸ Ideal.span {(DualNumber.eps : DualNumber ℚ)})
theorem

eps_ne_zero

L221 ↗
RegularLocalRingQuotientAscent.eps_ne_zero
Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Teeth
Lean source · statement
theorem eps_ne_zero : (DualNumber.eps : DualNumber ℚ) ≠ 0
theorem

eps_notMem_nonZeroDivisors

L226 ↗
RegularLocalRingQuotientAscent.eps_notMem_nonZeroDivisors
Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Teeth
Lean source · statement
theorem eps_notMem_nonZeroDivisors :
    (DualNumber.eps : DualNumber ℚ) ∉ nonZeroDivisors (DualNumber ℚ)
theorem

eps_mem_maximalIdeal

L232 ↗
RegularLocalRingQuotientAscent.eps_mem_maximalIdeal
Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Teeth
Lean source · statement
theorem eps_mem_maximalIdeal :
    (DualNumber.eps : DualNumber ℚ) ∈ maximalIdeal (DualNumber ℚ)
theorem

not_isRegularLocalRing_dualNumber

L237 ↗
RegularLocalRingQuotientAscent.not_isRegularLocalRing_dualNumber
Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Teeth
Lean source · statement
theorem not_isRegularLocalRing_dualNumber : ¬ IsRegularLocalRing (DualNumber ℚ)
theorem

not_forall_isRegularLocalRing_of_quotient_dropping_nonZeroDivisor

L268 ↗
RegularLocalRingQuotientAscent.not_forall_isRegularLocalRing_of_quotient_dropping_nonZeroDivisor
Source context 4 commands

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

noncomputable section
open IsLocalRing
namespace RegularLocalRingQuotientAscent
section Teeth
Lean source · statement
theorem not_forall_isRegularLocalRing_of_quotient_dropping_nonZeroDivisor :
    ¬ (∀ (A : Type) [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (x : A),
        x ∈ maximalIdeal A → IsRegularLocalRing (A ⧸ Ideal.span {x}) →
        IsRegularLocalRing A)

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