NYLL
Module

IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
23 declarations indexed from sourceView source ↗

Module documentation

Is Regular Local Ring span Finrank ker add ring Krull Dim eq

Imports7
Imported by2

Declarations

def

cotImage

L41 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.cotImage
Documentation

The span in the cotangent space of elements of the ideal lying in the maximal ideal.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section CotImage
variable {A : Type*} [CommRing A] [IsLocalRing A]
Lean source · statement
def cotImage (K : Ideal A) : Submodule (ResidueField A) (CotangentSpace A)
theorem

toCotangent_mem_cotImage

L45 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.toCotangent_mem_cotImage
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section CotImage
variable {A : Type*} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem toCotangent_mem_cotImage {K : Ideal A} (m : ↥(maximalIdeal A)) (hm : (m : A) ∈ K) :
    (maximalIdeal A).toCotangent m ∈ cotImage K
theorem

cotImage_mono

L49 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.cotImage_mono
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section CotImage
variable {A : Type*} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem cotImage_mono {K K' : Ideal A} (h : K ≤ K') : cotImage K ≤ cotImage K'
theorem

residue_smul_eq

L54 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.residue_smul_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section CotImage
variable {A : Type*} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem residue_smul_eq (c : A) (w : CotangentSpace A) : (residue A c) • w = c • w
theorem

exists_eq_toCotangent_of_mem_cotImage

L58 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.exists_eq_toCotangent_of_mem_cotImage
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section CotImage
variable {A : Type*} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem exists_eq_toCotangent_of_mem_cotImage {K : Ideal A} {w : CotangentSpace A} (hw : w ∈
  cotImage K) :
    ∃ m : ↥(maximalIdeal A), (m : A) ∈ K ∧ (maximalIdeal A).toCotangent m = w
def

cotSpan

L79 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.cotSpan
Documentation

The span of the images of the chosen maximal-ideal elements in the cotangent space.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section CotImage
variable {A : Type*} [CommRing A] [IsLocalRing A]
Lean source · statement
def cotSpan {ι : Type*} (z : ι → ↥(maximalIdeal A)) : Submodule (ResidueField A) (CotangentSpace A)
def

idealSpan

L84 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.idealSpan
Documentation

The ideal generated by the chosen family of maximal-ideal elements.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section CotImage
variable {A : Type*} [CommRing A] [IsLocalRing A]
Lean source · statement
def idealSpan {ι : Type*} (z : ι → ↥(maximalIdeal A)) : Ideal A
theorem

idealSpan_le

L87 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.idealSpan_le
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section CotImage
variable {A : Type*} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem idealSpan_le {ι : Type*} (z : ι → ↥(maximalIdeal A)) : idealSpan z ≤ maximalIdeal A
theorem

exists_eq_toCotangent_of_mem_cotSpan

L92 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.exists_eq_toCotangent_of_mem_cotSpan
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section CotImage
variable {A : Type*} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem exists_eq_toCotangent_of_mem_cotSpan {ι : Type*} {z : ι → ↥(maximalIdeal A)} {u :
  CotangentSpace A}
    (hu : u ∈ cotSpan z) :
    ∃ y : ↥(maximalIdeal A), (y : A) ∈ idealSpan z ∧ (maximalIdeal A).toCotangent y = u
theorem

cotSpan_sup_cotImage_eq_top

L112 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.cotSpan_sup_cotImage_eq_top
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section CotImage
variable {A : Type*} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem cotSpan_sup_cotImage_eq_top {ι : Type*} (z : ι → ↥(maximalIdeal A)) (K : Ideal A)
    (h : maximalIdeal A ≤ idealSpan z ⊔ K) : cotSpan z ⊔ cotImage K = ⊤
theorem

le_idealSpan_sup_of_cotSpan_sup_cotImage_eq_top

L144 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.le_idealSpan_sup_of_cotSpan_sup_cotImage_eq_top
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section CotImage
variable {A : Type*} [CommRing A] [IsLocalRing A]
Lean source · statement
theorem le_idealSpan_sup_of_cotSpan_sup_cotImage_eq_top [IsNoetherianRing A] {ι : Type*}
    (z : ι → ↥(maximalIdeal A)) (K : Ideal A) (h : cotSpan z ⊔ cotImage K = ⊤) :
    maximalIdeal A ≤ idealSpan z ⊔ K
theorem

spanFinrank_span_finset_le

L174 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.spanFinrank_span_finset_le
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section Helpers
variable {R : Type*} [CommRing R]
Lean source · statement
theorem spanFinrank_span_finset_le {M : Type*} [AddCommGroup M] [Module R M] (s : Finset M) :
    (Submodule.span R (s : Set M)).spanFinrank ≤ s.card
theorem

spanFinrank_span_range_le

L181 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.spanFinrank_span_range_le
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section Helpers
variable {R : Type*} [CommRing R]
Lean source · statement
theorem spanFinrank_span_range_le {M : Type*} [AddCommGroup M] [Module R M] {n : ℕ} (v : Fin n → M)
  :
    (Submodule.span R (Set.range v)).spanFinrank ≤ n
theorem

ringKrullDim_eq_natCast_iff

L190 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.ringKrullDim_eq_natCast_iff
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section Helpers
variable {R : Type*} [CommRing R]
Lean source · statement
theorem ringKrullDim_eq_natCast_iff [IsLocalRing R] (n : ℕ) :
    ringKrullDim R = n ↔ (maximalIdeal R).height = n
theorem

ringKrullDim_le_natCast_iff

L197 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.ringKrullDim_le_natCast_iff
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section Helpers
variable {R : Type*} [CommRing R]
Lean source · statement
theorem ringKrullDim_le_natCast_iff [IsLocalRing R] (n : ℕ) :
    ringKrullDim R ≤ n ↔ (maximalIdeal R).height ≤ n
theorem

natCast_le_ringKrullDim_iff

L204 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.natCast_le_ringKrullDim_iff
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section Helpers
variable {R : Type*} [CommRing R]
Lean source · statement
theorem natCast_le_ringKrullDim_iff [IsLocalRing R] (n : ℕ) :
    (n : WithBot ℕ∞) ≤ ringKrullDim R ↔ (n : ℕ∞) ≤ (maximalIdeal R).height
theorem

mem_maximalIdeal_of_map_mem

L222 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.mem_maximalIdeal_of_map_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section Surjection
variable {A C : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [CommRing C] [IsLocalRing
  C]
  (g : A →+* C) (hg : Function.Surjective g)
include hg
omit [IsNoetherianRing A] hg in
Lean source · statement
theorem mem_maximalIdeal_of_map_mem {a : A} (ha : g a ∈ maximalIdeal C) : a ∈ maximalIdeal A
theorem

maximalIdeal_le_idealSpan_sup_ker

L226 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.maximalIdeal_le_idealSpan_sup_ker
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section Surjection
variable {A C : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [CommRing C] [IsLocalRing
  C]
  (g : A →+* C) (hg : Function.Surjective g)
include hg
omit [IsNoetherianRing A] in
Lean source · full declaration
theorem maximalIdeal_le_idealSpan_sup_ker {ι : Type*} (z : ι → ↥(maximalIdeal A))
    (h : maximalIdeal C ≤ Ideal.span (Set.range fun i => g (z i))) :
    maximalIdeal A ≤ idealSpan z ⊔ RingHom.ker g := by
  intro m hm
  have hgm : g m ∈ maximalIdeal C := by
    rw [← map_maximalIdeal_of_surjective g hg]; exact Ideal.mem_map_of_mem g hm
  have hspan : Ideal.span (Set.range fun i => g (z i)) = Ideal.map g (idealSpan z) := by
    rw [idealSpan, Ideal.map_span, ← Set.range_comp]; rfl
  have := h hgm
  rw [hspan, Ideal.mem_map_iff_of_surjective g hg] at this
  obtain ⟨y, hy, hgy⟩ := this
  have : m = y + (m - y) := by ring
  rw [this]
  refine Submodule.add_mem_sup hy ?_
  rw [RingHom.mem_ker, map_sub, hgy, sub_self]
theorem

finrank_quotient_cotImage_le

L242 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.finrank_quotient_cotImage_le
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section Surjection
variable {A C : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [CommRing C] [IsLocalRing
  C]
  (g : A →+* C) (hg : Function.Surjective g)
include hg
Lean source · statement
theorem finrank_quotient_cotImage_le :
    Module.finrank (ResidueField A) (CotangentSpace A ⧸ cotImage (RingHom.ker g)) ≤
      (maximalIdeal C).spanFinrank
theorem

spanFinrank_maximalIdeal_le_finrank_quotient_cotImage

L286 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.spanFinrank_maximalIdeal_le_finrank_quotient_cotImage
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section Surjection
variable {A C : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [CommRing C] [IsLocalRing
  C]
  (g : A →+* C) (hg : Function.Surjective g)
include hg
Lean source · statement
theorem spanFinrank_maximalIdeal_le_finrank_quotient_cotImage :
    (maximalIdeal C).spanFinrank ≤
      Module.finrank (ResidueField A) (CotangentSpace A ⧸ cotImage (RingHom.ker g))
theorem

spanFinrank_maximalIdeal_eq_finrank_quotient_cotImage

L322 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.spanFinrank_maximalIdeal_eq_finrank_quotient_cotImage
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section Surjection
variable {A C : Type*} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [CommRing C] [IsLocalRing
  C]
  (g : A →+* C) (hg : Function.Surjective g)
include hg
Lean source · statement
theorem spanFinrank_maximalIdeal_eq_finrank_quotient_cotImage :
    (maximalIdeal C).spanFinrank =
      Module.finrank (ResidueField A) (CotangentSpace A ⧸ cotImage (RingHom.ker g))
theorem

main

L332 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq.RSMU.main
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
noncomputable section
namespace RSMU
section Main
Lean source · statement
theorem main {A B : Type*} [CommRing A] [CommRing B] [IsRegularLocalRing A] [IsRegularLocalRing B]
    (f : A →+* B) (hf : Function.Surjective f) :
    ((RingHom.ker f).spanFinrank : WithBot ℕ∞) + ringKrullDim B = ringKrullDim A
theorem

spanFinrank_ker_add_ringKrullDim_eq

L467 ↗
IsRegularLocalRing.spanFinrank_ker_add_ringKrullDim_eq
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_spanFinrank_ker_add_ringKrullDim_eq
open IsLocalRing
Lean source · statement
theorem _root_.IsRegularLocalRing.spanFinrank_ker_add_ringKrullDim_eq
    {A B : Type*} [CommRing A] [CommRing B] [IsRegularLocalRing A] [IsRegularLocalRing B]
    (f : A →+* B) (hf : Function.Surjective f) :
    ((RingHom.ker f).spanFinrank : WithBot ℕ∞) + ringKrullDim B = ringKrullDim A

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