Module

Exists_place_toSubring_eq_of_isIntegrallyClosedIn_of_isNoetherianRing.lean

Nyll.AlgebraicCurves.Places.Exists_place_toSubring_eq_of_isIntegrallyClosedIn_of_isNoetherianRing

3 declarations indexed from sourceView source ↗

Module documentation

Exists place to Subring eq of is Integrally Closed In of is Noetherian Ring

Imports2

Nyll.AlgebraicCurves.FunctionFields.CurveOver
Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

dimensionLEOne_of_height_maximalIdeal_le_one

L29 ↗

AlgebraicCurves.Places.Proofs.Exists_place_toSubring_eq_of_isIntegrallyClosedIn_of_isNoetherianRing.ALGAux.dimensionLEOne_of_height_maximalIdeal_le_one

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Exists_place_toSubring_eq_of_isIntegrallyClosedIn_of_isNoetherianRing
open AlgebraicCurve IsLocalRing
namespace ALGAux

Lean source · statement

theorem dimensionLEOne_of_height_maximalIdeal_le_one (S : Type*) [CommRing S] [IsDomain S]
    [IsLocalRing S] (h : (maximalIdeal S).height ≤ 1) : Ring.DimensionLEOne S

theorem

exists_place_of_isDedekindDomain

L44 ↗

AlgebraicCurves.Places.Proofs.Exists_place_toSubring_eq_of_isIntegrallyClosedIn_of_isNoetherianRing.ALGAux.exists_place_of_isDedekindDomain

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Exists_place_toSubring_eq_of_isIntegrallyClosedIn_of_isNoetherianRing
open AlgebraicCurve IsLocalRing
namespace ALGAux

Lean source · statement

theorem exists_place_of_isDedekindDomain (L F : Type*) [Field L] [Field F] [Algebra L F]
    (R : Subring F) [IsLocalRing R] [IsDedekindDomain R] [IsFractionRing R F]
    (hL : ∀ a : L, algebraMap L F a ∈ R) (hR : R ≠ ⊤) :
    ∃ P : Place L F, P.toValuationSubring.toSubring = R

theorem

exists_place_toSubring_eq_of_isIntegrallyClosedIn_of_isNoetherianRing

L65 ↗

AlgebraicCurve.exists_place_toSubring_eq_of_isIntegrallyClosedIn_of_isNoetherianRing

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Exists_place_toSubring_eq_of_isIntegrallyClosedIn_of_isNoetherianRing
open AlgebraicCurve IsLocalRing
open ALGAux in

Lean source · statement

theorem _root_.AlgebraicCurve.exists_place_toSubring_eq_of_isIntegrallyClosedIn_of_isNoetherianRing
    {L F : Type*} [Field L] [IsAlgClosed L] [Field F] [Algebra L F] [IsCurveOver L F]
    (R : Subring F) [IsLocalRing ↥R] [IsNoetherianRing ↥R] [IsFractionRing ↥R F]
    (hn : IsIntegrallyClosedIn ↥R F)
    (hL : ∀ a : L, algebraMap L F a ∈ R) (hR : R ≠ ⊤) :
    ∃ P : Place L F, P.toValuationSubring.toSubring = R

Module documentation

Exists place to Subring eq of is Integrally Closed In of is Noetherian Ring

Declarations

dimensionLEOne_of_height_maximalIdeal_le_one

exists_place_of_isDedekindDomain

exists_place_toSubring_eq_of_isIntegrallyClosedIn_of_isNoetherianRing