NYLL
Module

ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
14 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring ring Krull Dim eq ring Krull Dim residue Valuation Subring add

Imports1
Imported by1

Declarations

theorem

length_le_height_add_coheight

L34 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.CompVRankSol.length_le_height_add_coheight
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
namespace CompVRankSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)
section order
variable {α : Type*} [LinearOrder α]
Lean source · statement
theorem length_le_height_add_coheight (a : α) (p : LTSeries α) :
    (p.length : ℕ∞) ≤ Order.height a + Order.coheight a
theorem

krullDim_eq_height_add_coheight

L89 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.CompVRankSol.krullDim_eq_height_add_coheight
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
namespace CompVRankSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)
section order
variable {α : Type*} [LinearOrder α]
Lean source · statement
theorem krullDim_eq_height_add_coheight (a : α) :
    Order.krullDim α = ((Order.height a + Order.coheight a : ℕ∞) : WithBot ℕ∞)
theorem

krullDim_eq_krullDim_Iic_add_krullDim_Ici

L98 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.CompVRankSol.krullDim_eq_krullDim_Iic_add_krullDim_Ici
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
namespace CompVRankSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)
section order
variable {α : Type*} [LinearOrder α]
Lean source · statement
theorem krullDim_eq_krullDim_Iic_add_krullDim_Ici (a : α) :
    Order.krullDim α = Order.krullDim (Set.Iic a) + Order.krullDim (Set.Ici a)
def

subtypeIso

L109 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.CompVRankSol.subtypeIso
Documentation

The order isomorphism on subtypes induced by an order isomorphism preserving their predicates.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
namespace CompVRankSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)
section rank
Lean source · full declaration
def subtypeIso {α β : Type*} [LE α] [LE β] (f : α ≃o β) {p : α → Prop} {q : β → Prop}
    (hpq : ∀ a, p a ↔ q (f a)) : {a // p a} ≃o {b // q b} where
  toEquiv := f.toEquiv.subtypeEquiv hpq
  map_rel_iff' {a b} := by
    change f a ≤ f b ↔ (a : α) ≤ b
    exact f.map_rel_iff
abbrev

Ω

L117 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.CompVRankSol.Ω
Documentation

The ordered type of valuation rings containing the fixed valuation ring.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
namespace CompVRankSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)
section rank
Lean source · statement
abbrev Ω (A : ValuationSubring L)
def

σ

L120 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.CompVRankSol.σ
Documentation

The chosen valuation overring, regarded as an element of the ordered type of overrings.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
namespace CompVRankSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)
section rank
Lean source · statement
def σ : Ω A
def

isoIic

L124 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.CompVRankSol.isoIic
Documentation

The order isomorphism from primes containing the center to valuation overrings below the chosen one.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
namespace CompVRankSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)
section rank
Lean source · statement
def isoIic :
    {P : (PrimeSpectrum A)ᵒᵈ // OrderDual.ofDual P ∈
        PrimeSpectrum.zeroLocus ((A.idealOfLE S h : Ideal A) : Set A)} ≃o Set.Iic (σ A S h)
def

isoIci

L145 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.CompVRankSol.isoIci
Documentation

Order equivalence between the opposite prime spectrum of the overring and the upper interval of valuation overrings above its image.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
namespace CompVRankSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)
section rank
Lean source · statement
def isoIci : (PrimeSpectrum S)ᵒᵈ ≃o Set.Ici (σ A S h)
theorem

krullDim_zeroLocus_eq

L153 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.CompVRankSol.krullDim_zeroLocus_eq
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
namespace CompVRankSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)
section rank
Lean source · statement
theorem krullDim_zeroLocus_eq :
    Order.krullDim (PrimeSpectrum.zeroLocus ((A.idealOfLE S h : Ideal A) : Set A)) =
      Order.krullDim (Set.Iic (σ A S h))
theorem

ringKrullDim_residueValuationSubring

L161 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.CompVRankSol.ringKrullDim_residueValuationSubring
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
namespace CompVRankSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)
section rank
Lean source · statement
theorem ringKrullDim_residueValuationSubring :
    ringKrullDim (A.residueValuationSubring S h) =
      Order.krullDim (PrimeSpectrum.zeroLocus ((A.idealOfLE S h : Ideal A) : Set A))
theorem

ringKrullDim_eq_krullDim_Ici

L168 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.CompVRankSol.ringKrullDim_eq_krullDim_Ici
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
namespace CompVRankSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)
section rank
Lean source · statement
theorem ringKrullDim_eq_krullDim_Ici : ringKrullDim S = Order.krullDim (Set.Ici (σ A S h))
theorem

ringKrullDim_eq_krullDim_Ω

L172 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.CompVRankSol.ringKrullDim_eq_krullDim_Ω
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
namespace CompVRankSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)
section rank
Lean source · statement
theorem ringKrullDim_eq_krullDim_Ω : ringKrullDim A = Order.krullDim (Ω A)
theorem

rank_formula

L176 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add.CompVRankSol.rank_formula
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
namespace CompVRankSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)
section rank
Lean source · statement
theorem rank_formula :
    ringKrullDim A = ringKrullDim (A.residueValuationSubring S h) + ringKrullDim S
theorem

ringKrullDim_eq_ringKrullDim_residueValuationSubring_add

L185 ↗
ValuationSubring.ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
open IsLocalRing
Lean source · statement
theorem _root_.ValuationSubring.ringKrullDim_eq_ringKrullDim_residueValuationSubring_add
    {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S) :
    ringKrullDim A = ringKrullDim (A.residueValuationSubring S h) + ringKrullDim S

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