Module

Smooth_isDomain_and_isIntegrallyClosed_stalk_of_isDiscreteValuationRing.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_isDomain_and_isIntegrallyClosed_stalk_of_isDiscreteValuationRing

1 declaration indexed from sourceView source ↗

Module documentation

Smooth is Domain and is Integrally Closed stalk of is Discrete Valuation Ring

Imports5

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Mathlib.AlgebraicGeometry.Stalk
Mathlib.RingTheory.RingHom.Smooth
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_Smooth_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime

Imported by2

theorem

isDomain_and_isIntegrallyClosed_stalk_of_isDiscreteValuationRing

L30 ↗

AlgebraicGeometry.Smooth.isDomain_and_isIntegrallyClosed_stalk_of_isDiscreteValuationRing

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Smooth_isDomain_and_isIntegrallyClosed_stalk_of_isDiscreteValuationRing
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry

Lean source · statement

theorem
  _root_.AlgebraicGeometry.Smooth.isDomain_and_isIntegrallyClosed_stalk_of_isDiscreteValuationRing
    (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) [Smooth t] (x : T) :
    IsDomain (T.presheaf.stalk x) ∧ IsIntegrallyClosed (T.presheaf.stalk x)

Module documentation

Smooth is Domain and is Integrally Closed stalk of is Discrete Valuation Ring

Declarations

isDomain_and_isIntegrallyClosed_stalk_of_isDiscreteValuationRing