Module

ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one

7 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring ring Krull Dim le to ENat trdeg rat add one

Imports2

Mathlib.RingTheory.DedekindDomain.Dvr
Nyll.AlgebraicCurves.Valuations.ValuationSubring_ringKrullDim_le_ringKrullDim_comap_add_trdeg

Imported by1

Nyll.AlgebraicCurves.Valuations.All

def

unitInts

L30 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one.AbhRatSol.unitInts

Documentation

The multiplicative submonoid of integers that become units in the valuation ring.

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one
namespace AbhRatSol
open ValuationSubring

Lean source · statement

def unitInts (B : ValuationSubring ℚ) : Submonoid ℤ

lemma

mem_unitInts

L33 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one.AbhRatSol.mem_unitInts

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one
namespace AbhRatSol
open ValuationSubring

Lean source · statement

lemma mem_unitInts {B : ValuationSubring ℚ} {n : ℤ} :
    n ∈ unitInts B ↔ IsUnit (algebraMap ℤ B n)

lemma

unitInts_le_nonZeroDivisors

L36 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one.AbhRatSol.unitInts_le_nonZeroDivisors

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one
namespace AbhRatSol
open ValuationSubring

Lean source · statement

lemma unitInts_le_nonZeroDivisors (B : ValuationSubring ℚ) : unitInts B ≤ nonZeroDivisors ℤ

lemma

isUnit_den

L43 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one.AbhRatSol.isUnit_den

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one
namespace AbhRatSol
open ValuationSubring

Lean source · statement

lemma isUnit_den (B : ValuationSubring ℚ) (x : B) : IsUnit (algebraMap ℤ B ((x : ℚ).den : ℤ))

instance

isLocalization

L65 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one.AbhRatSol.isLocalization

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one
namespace AbhRatSol
open ValuationSubring

Lean source · statement

instance isLocalization (B : ValuationSubring ℚ) : IsLocalization (unitInts B) B

theorem

ringKrullDim_le_one

L76 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one.AbhRatSol.ringKrullDim_le_one

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one
namespace AbhRatSol
open ValuationSubring

Lean source · statement

theorem ringKrullDim_le_one (B : ValuationSubring ℚ) : ringKrullDim B ≤ 1

theorem

ringKrullDim_le_toENat_trdeg_rat_add_one

L85 ↗

ValuationSubring.ringKrullDim_le_toENat_trdeg_rat_add_one

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_ringKrullDim_le_toENat_trdeg_rat_add_one
open AbhRatSol in

Lean source · statement

theorem _root_.ValuationSubring.ringKrullDim_le_toENat_trdeg_rat_add_one
    {L : Type*} [Field L] [Algebra ℚ L] (A : ValuationSubring L) :
    ringKrullDim A ≤ (Cardinal.toENat (Algebra.trdeg ℚ L) : WithBot ℕ∞) + 1

Module documentation

Valuation Subring ring Krull Dim le to ENat trdeg rat add one

Declarations

unitInts

mem_unitInts

unitInts_le_nonZeroDivisors

isUnit_den

isLocalization

ringKrullDim_le_one

ringKrullDim_le_toENat_trdeg_rat_add_one