Module

OrdinaryHenselization.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.OrdinaryHenselization

9 declarations indexed from sourceView source ↗

Module documentation

The ordinary henselization at the residue-field point

Use the existing pointed étale colimit at Spec κ(A) ⟶ Spec A itself. Its Henselian property is supplied by the standard-étale simple-root construction. Its actual evaluation is surjective because its composite with the original structure map is the residue map of A. Consequently its residue-field embedding is an isomorphism with κ(A), without a separably closed field.

Imports4

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkHenselian
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkResidue
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkStructure
Mathlib.RingTheory.LocalRing.ResidueField.Basic

Imported by4

def

ordinaryHenselization

L33 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselization

Documentation

The actual pointed étale colimit at the canonical residue-field point.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable (A : Type u) [CommRing A] [IsLocalRing A]

Lean source · statement

def ordinaryHenselization : CommRingCat.{u}

instance

ordinaryHenselization_henselianLocalRing

L36 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselization_henselianLocalRing

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable (A : Type u) [CommRing A] [IsLocalRing A]

Lean source · statement

instance ordinaryHenselization_henselianLocalRing :
    HenselianLocalRing (ordinaryHenselization A)

def

ordinaryHenselizationMap

L42 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationMap

Documentation

The original map into the colimit is the germ of the identity neighborhood.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable (A : Type u) [CommRing A] [IsLocalRing A]

Lean source · statement

def ordinaryHenselizationMap : A →+* ordinaryHenselization A

instance

ordinaryHenselizationMap_isLocalHom

L45 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationMap_isLocalHom

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable (A : Type u) [CommRing A] [IsLocalRing A]

Lean source · statement

instance ordinaryHenselizationMap_isLocalHom :
    IsLocalHom (ordinaryHenselizationMap A)

instance

ordinaryHenselization_algebra

L49 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselization_algebra

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable (A : Type u) [CommRing A] [IsLocalRing A]

Lean source · statement

instance ordinaryHenselization_algebra : Algebra A (ordinaryHenselization A)

theorem

ordinaryHenselization_evaluation_surjective

L53 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselization_evaluation_surjective

Documentation

Evaluation is surjective because it contains the image of A → κ(A).

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable (A : Type u) [CommRing A] [IsLocalRing A]

Lean source · statement

theorem ordinaryHenselization_evaluation_surjective :
    Function.Surjective (geometricStalkEvaluation
      (Spec.map (CommRingCat.ofHom (IsLocalRing.residue A))))

theorem

ordinaryHenselization_residueEmbedding_surjective

L62 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselization_residueEmbedding_surjective

Documentation

The residue embedding of the constructed ordinary henselization is onto.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable (A : Type u) [CommRing A] [IsLocalRing A]

Lean source · statement

theorem ordinaryHenselization_residueEmbedding_surjective :
    Function.Surjective (geometricStalkResidueEmbedding
      (Spec.map (CommRingCat.ofHom (IsLocalRing.residue A))))

def

ordinaryHenselizationResidueEquiv

L73 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationResidueEquiv

Documentation

The actual residue field is canonically the original residue field.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable (A : Type u) [CommRing A] [IsLocalRing A]

Lean source · statement

def ordinaryHenselizationResidueEquiv :
    IsLocalRing.ResidueField (ordinaryHenselization A) ≃+*
      IsLocalRing.ResidueField A

theorem

ordinaryHenselizationResidueEquiv_map_residue

L84 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationResidueEquiv_map_residue

Documentation

The residue identification respects the original map from A.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable (A : Type u) [CommRing A] [IsLocalRing A]

Lean source · statement

theorem ordinaryHenselizationResidueEquiv_map_residue (a : A) :
    ordinaryHenselizationResidueEquiv A
      (IsLocalRing.residue (ordinaryHenselization A) (ordinaryHenselizationMap A a)) =
        IsLocalRing.residue A a

Module documentation

The ordinary henselization at the residue-field point

Declarations