NYLL
Module

Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent
8 declarations indexed from sourceView source ↗

Module documentation

Ideal nat Cast le ring Krull Dim quotient of mem minimal Primes map of algebraic

Independent

Imports3
Imported by2

Declarations

lemma

exists_ltSeries_comap_eq_last

L33 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent.P2mFibDim.exists_ltSeries_comap_eq_last
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent
universe u v w
namespace P2mFibDim
open Ideal
Lean source · statement
lemma exists_ltSeries_comap_eq_last {R S : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsIntegral R S] (hinj : Function.Injective (algebraMap R S))
    (l : LTSeries (PrimeSpectrum R)) :
    ∃ L : LTSeries (PrimeSpectrum S), L.length = l.length ∧
      PrimeSpectrum.comap (algebraMap R S) L.last = l.last
theorem

ringKrullDim_le_of_isIntegral_of_injective

L62 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent.P2mFibDim.ringKrullDim_le_of_isIntegral_of_injective
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent
universe u v w
namespace P2mFibDim
open Ideal
Lean source · statement
theorem ringKrullDim_le_of_isIntegral_of_injective {R S : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsIntegral R S] (hinj : Function.Injective (algebraMap R S)) :
    ringKrullDim R ≤ ringKrullDim S
theorem

ringKrullDim_localization_le

L71 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent.P2mFibDim.ringKrullDim_localization_le
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent
universe u v w
namespace P2mFibDim
open Ideal
Lean source · statement
theorem ringKrullDim_localization_le {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    (M : Submonoid R) [IsLocalization M S] : ringKrullDim S ≤ ringKrullDim R
lemma

exists_nat_eq

L78 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent.P2mFibDim.exists_nat_eq
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent
universe u v w
namespace P2mFibDim
open Ideal
Lean source · statement
lemma exists_nat_eq {x : WithBot ℕ∞} {n : ℕ} (h0 : 0 ≤ x) (h : x ≤ n) : ∃ a : ℕ, x = a
theorem

exists_ringKrullDim_eq_natCast

L95 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent.P2mFibDim.exists_ringKrullDim_eq_natCast
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent
universe u v w
namespace P2mFibDim
open Ideal
section Main
variable (k : Type u) [Field k] {R : Type v} {C : Type w} [CommRing R] [IsDomain R] [Algebra k R]
  [Algebra.FiniteType k R] [CommRing C] [IsDomain C] [Algebra k C] [Algebra R C]
  [IsScalarTower k R C] [Algebra.FiniteType R C]
Lean source · statement
theorem exists_ringKrullDim_eq_natCast (A : Type*) [CommRing A]
    [Nontrivial A] [Algebra k A] [Algebra.FiniteType k A] : ∃ n : ℕ, ringKrullDim A = n
theorem

ringKrullDim_localization_add_le

L119 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent.P2mFibDim.ringKrullDim_localization_add_le
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent
universe u v w
namespace P2mFibDim
open Ideal
section Main
variable (k : Type u) [Field k] {R : Type v} {C : Type w} [CommRing R] [IsDomain R] [Algebra k R]
  [Algebra.FiniteType k R] [CommRing C] [IsDomain C] [Algebra k C] [Algebra R C]
  [IsScalarTower k R C] [Algebra.FiniteType R C]
include k in
omit [IsDomain R] [Algebra k C] [IsScalarTower k R C] [Algebra.FiniteType R C] in
Lean source · statement
theorem ringKrullDim_localization_add_le
    {d : ℕ} (z : Fin d → C) (hz : AlgebraicIndependent R z) (r : R) (hr : r ≠ 0)
    (hint : ∀ c : C, ∃ n : ℕ, IsIntegral (Algebra.adjoin R (Set.range z)) (r ^ n • c)) :
    ringKrullDim (Localization.Away r) + d ≤ ringKrullDim C
theorem

main

L278 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent.P2mFibDim.main
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent
universe u v w
namespace P2mFibDim
open Ideal
section Main
variable (k : Type u) [Field k] {R : Type v} {C : Type w} [CommRing R] [IsDomain R] [Algebra k R]
  [Algebra.FiniteType k R] [CommRing C] [IsDomain C] [Algebra k C] [Algebra R C]
  [IsScalarTower k R C] [Algebra.FiniteType R C]
include k in
Lean source · statement
theorem main {d : ℕ} (z : Fin d → C) (hz : AlgebraicIndependent R z) (r : R) (hr : r ≠ 0)
    (hint : ∀ c : C, ∃ n : ℕ, IsIntegral (Algebra.adjoin R (Set.range z)) (r ^ n • c))
    (p : Ideal R) [p.IsMaximal] (hrp : r ∉ p)
    (Q : Ideal C) (hQ : Q ∈ (p.map (algebraMap R C)).minimalPrimes) :
    (d : WithBot ℕ∞) ≤ ringKrullDim (C ⧸ Q)
theorem

natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent

L362 ↗
Ideal.natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Ideal_natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent
universe u v w
Lean source · statement
theorem
  _root_.Ideal.natCast_le_ringKrullDim_quotient_of_mem_minimalPrimes_map_of_algebraicIndependent
    (k : Type u) [Field k] {R : Type v} {C : Type w} [CommRing R] [IsDomain R] [Algebra k R]
    [Algebra.FiniteType k R] [CommRing C] [IsDomain C] [Algebra k C] [Algebra R C]
    [IsScalarTower k R C] [Algebra.FiniteType R C]
    {d : ℕ} (z : Fin d → C) (hz : AlgebraicIndependent R z) (r : R) (hr : r ≠ 0)
    (hint : ∀ c : C, ∃ n : ℕ, IsIntegral (Algebra.adjoin R (Set.range z)) (r ^ n • c))
    (p : Ideal R) [p.IsMaximal] (hrp : r ∉ p)
    (Q : Ideal C) (hQ : Q ∈ (p.map (algebraMap R C)).minimalPrimes) :
    (d : WithBot ℕ∞) ≤ ringKrullDim (C ⧸ Q)

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