AlgebraicGeometry.Smooth.isDiscreteValuationRing_stalk_of_forall_specializes
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Smooth_isDiscreteValuationRing_stalk_of_forall_specializes
universe u
open CategoryTheory AlgebraicGeometry TopologyLean source · statement
theorem _root_.AlgebraicGeometry.Smooth.isDiscreteValuationRing_stalk_of_forall_specializes
(R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
{T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) [Smooth t]
(η : T) (hηs : t.base η = IsLocalRing.closedPoint R)
(hgen : ∀ y : T, y ⤳ η → t.base y = IsLocalRing.closedPoint R → y = η) :
∃ _ : IsDomain (T.presheaf.stalk η), IsDiscreteValuationRing (T.presheaf.stalk η)