Module

ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc

8 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring ring Krull Dim residue Valuation Subring of Prime eq krull Dim Icc

Imports1

Nyll.AlgebraicCurves.Valuations.ValuationSubring_ResidueValuationSubring

Imported by1

Nyll.AlgebraicCurves.Valuations.All

def

subtypeIso

L32 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc.CompVIccSol.subtypeIso

Documentation

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

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc
open IsLocalRing
namespace CompVIccSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)

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

Ω

L40 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc.CompVIccSol.Ω

Documentation

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

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc
open IsLocalRing
namespace CompVIccSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)

Lean source · statement

abbrev Ω (A : ValuationSubring L)

def

σ

L43 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc.CompVIccSol.σ

Documentation

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

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc
open IsLocalRing
namespace CompVIccSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)

Lean source · statement

def σ : Ω A

def

isoIic

L47 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc.CompVIccSol.isoIic

Documentation

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

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc
open IsLocalRing
namespace CompVIccSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)

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)

theorem

krullDim_zeroLocus_eq

L64 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc.CompVIccSol.krullDim_zeroLocus_eq

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc
open IsLocalRing
namespace CompVIccSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)

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

L72 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc.CompVIccSol.ringKrullDim_residueValuationSubring

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc
open IsLocalRing
namespace CompVIccSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)

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_ofPrime_pair

L79 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc.CompVIccSol.ringKrullDim_ofPrime_pair

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc
open IsLocalRing
namespace CompVIccSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)

Lean source · statement

theorem ringKrullDim_ofPrime_pair (Q P : Ideal A) [Q.IsPrime] [P.IsPrime] (hQP : Q ≤ P) :
    ringKrullDim ((A.ofPrime P).residueValuationSubring (A.ofPrime Q)
        (ValuationSubring.ofPrime_le_of_le A Q P hQP)) =
      Order.krullDim (Set.Icc (⟨Q, inferInstance⟩ : PrimeSpectrum A) ⟨P, inferInstance⟩)

theorem

ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc

L118 ↗

ValuationSubring.ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc
open IsLocalRing

Lean source · statement

theorem _root_.ValuationSubring.ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc
    {L : Type*} [Field L] (A : ValuationSubring L) (Q P : Ideal A) [Q.IsPrime] [P.IsPrime]
    (hQP : Q ≤ P) :
    ringKrullDim ((A.ofPrime P).residueValuationSubring (A.ofPrime Q)
        (ValuationSubring.ofPrime_le_of_le A Q P hQP)) =
      Order.krullDim (Set.Icc (⟨Q, inferInstance⟩ : PrimeSpectrum A) ⟨P, inferInstance⟩)

Module documentation

Valuation Subring ring Krull Dim residue Valuation Subring of Prime eq krull Dim Icc

Declarations