The definition uses the normalization of the reduction in its total fraction ring. It requires the reduction to be a domain, its normalization to be local, and the resulting residue field extension to be purely inseparable. This is Stacks Project, Definition 15.108.1, not a criterion formulated in terms of strict henselization.
The integral closure of the reduction in its total ring of fractions. When the reduction is a domain, the ambient ring is its fraction field.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace IsLocalRing
universe uabbrev reducedNormalization (R : Type u) [CommRing R] : Type uThe actual quotient map followed by the inclusion into the normalization of the reduction.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace IsLocalRing
universe udef reducedNormalizationMap (R : Type u) [CommRing R] :
R →+* reducedNormalization RThe normalization map is integral, including for a nonreduced base.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace IsLocalRing
universe utheorem reducedNormalizationMap_isIntegral (R : Type u) [CommRing R] :
(reducedNormalizationMap R).IsIntegralWhen both rings are local, integrality makes the actual normalization map local: its maximal ideal contracts to the maximal ideal of the base.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace IsLocalRing
universe utheorem reducedNormalizationMap_isLocalHom (R : Type u) [CommRing R]
[IsLocalRing R] [IsLocalRing (reducedNormalization R)] :
IsLocalHom (reducedNormalizationMap R)A local ring is geometrically unibranch if its reduction is a domain, the normalization of that reduction is local, and the induced residue field extension is purely inseparable.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace IsLocalRing
universe udef IsGeometricallyUnibranch (R : Type u) [CommRing R] [IsLocalRing R] : Prop