ModuleGeometricStalkResidue.lean
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkResidue
3 declarations indexed from sourceView source ↗ Module documentation
The separably closed residue field of the geometric étale stalk
Evaluation of the constructed stalk in the geometric field is a local homomorphism, so it induces an embedding of its actual residue field into that field. For a monic separable irreducible residue polynomial, lift its coefficients to the stalk. Its simple root in the geometric field lifts to a root in the stalk by the concrete standard étale neighborhood from GeometricStalkHenselian. Reduction of this root proves that the residue field is separably closed.
Thus the constructed ring is strictly local: it is Henselian with separably closed residue field. This does not yet identify it with a separately chosen strict henselization, or establish the manuscript's inertia comparison.
Declarations
EtaleFundamentalGroups.StrictHenselian.geometricStalkEvaluation_isLocalHom
DocumentationEvaluation is local because its nonzero values are precisely the units of the constructed geometric stalk.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
(s : Spec (.of Ω) ⟶ S)
EtaleFundamentalGroups.StrictHenselian.geometricStalkResidueEmbedding
DocumentationThe embedding of the actual residue field of the geometric étale stalk into the chosen geometric field.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
(s : Spec (.of Ω) ⟶ S)
EtaleFundamentalGroups.StrictHenselian.geometricStalk_residueField_isSepClosed
DocumentationEvery monic separable irreducible residue polynomial has a root, obtained by adjoining a simple root in an actual pointed étale neighborhood.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {S : Scheme.{u}} {Ω : Type u} [Field Ω]
(s : Spec (.of Ω) ⟶ S)