Module

OrdinaryHenselizationUniversal.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.OrdinaryHenselizationUniversal

7 declarations indexed from sourceView source ↗

Module documentation

The universal property of the constructed ordinary henselization

For a local map A → S into a Henselian local ring, extend every neighborhood point along κ(A) → κ(S) and use the existing Henselian neighborhood lifts. Their already constructed colimit map gives the universal map H(A) → S.

Local maps with the same base map have the same residue map, because κ(H(A)) = κ(A). On an affine pointed neighborhood, uniqueness of the actual Henselian étale lift then makes their section maps equal. Every germ admits such an affine refinement, proving uniqueness on the original colimit.

Imports8

Nyll.EtaleFundamentalGroups.StrictHenselian.OrdinaryHenselization
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkChangeField
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkHenselianMap
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkFlat
Nyll.SchemeTheory.Etale.HenselianLocalSection
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Mathlib.RingTheory.RingHom.Etale

Imported by3

def

ordinaryHenselizationLift

L41 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationLift

Documentation

The actual local map out of the residue-pointed étale colimit.

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 S : Type u} [CommRing A] [IsLocalRing A]
  [CommRing S] [HenselianLocalRing S] (f : A →+* S) [IsLocalHom f]

Lean source · statement

def ordinaryHenselizationLift : ordinaryHenselization A →+* S

instance

ordinaryHenselizationLift_isLocalHom

L46 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationLift_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 S : Type u} [CommRing A] [IsLocalRing A]
  [CommRing S] [HenselianLocalRing S] (f : A →+* S) [IsLocalHom f]

Lean source · full declaration

instance ordinaryHenselizationLift_isLocalHom :
    IsLocalHom (ordinaryHenselizationLift f) where
  map_nonunit a ha :=
    (geometricStalkChangeField_isLocalHom (IsLocalRing.residue A)
      (IsLocalRing.ResidueField.map f)).map_nonunit a
        ((geometricStalkToHenselian_isLocalHom f).map_nonunit _ ha)

theorem

ordinaryHenselizationLift_comp_map

L54 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationLift_comp_map

Documentation

The universal map extends the specified original local ring map.

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 S : Type u} [CommRing A] [IsLocalRing A]
  [CommRing S] [HenselianLocalRing S] (f : A →+* S) [IsLocalHom f]

Lean source · statement

theorem ordinaryHenselizationLift_comp_map :
    (ordinaryHenselizationLift f).comp (ordinaryHenselizationMap A) = f

theorem

ordinaryHenselization_localMap_residue

L75 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselization_localMap_residue

Documentation

Localness and the original base map determine the residue of every map out of the ordinary henselization.

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 S : Type u} [CommRing A] [IsLocalRing A]
  [CommRing S] [HenselianLocalRing S] (f : A →+* S) [IsLocalHom f]

Lean source · statement

theorem ordinaryHenselization_localMap_residue
    (g : ordinaryHenselization A →+* S) [IsLocalHom g]
    (hg : g.comp (ordinaryHenselizationMap A) = f) :
    (IsLocalRing.residue S).comp g = (IsLocalRing.ResidueField.map f).comp
      (geometricStalkEvaluation
        (Spec.map (CommRingCat.ofHom (IsLocalRing.residue A)))).hom

theorem

henselian_etale_ringHom_ext

L113 ↗

EtaleFundamentalGroups.StrictHenselian.henselian_etale_ringHom_ext

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {A S : Type u} [CommRing A] [IsLocalRing A]
  [CommRing S] [HenselianLocalRing S] (f : A →+* S) [IsLocalHom f]
omit [IsLocalRing A] [IsLocalHom f] in

Lean source · statement

theorem henselian_etale_ringHom_ext
    {B : Type u} [CommRing B] (β : A →+* B) (hβ : β.Etale)
    (g h : B →+* S) (hg : g.comp β = f) (hh : h.comp β = f)
    (hresidue : (IsLocalRing.residue S).comp g = (IsLocalRing.residue S).comp h) :
    g = h

theorem

ordinaryHenselizationLift_unique

L152 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationLift_unique

Documentation

Two local maps out of the actual ordinary henselization agreeing on the original ring are equal. Affine refinements reduce this to genuine unique étale lifts over the Henselian target.

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 S : Type u} [CommRing A] [IsLocalRing A]
  [CommRing S] [HenselianLocalRing S] (f : A →+* S) [IsLocalHom f]

Lean source · statement

theorem ordinaryHenselizationLift_unique
    (g : ordinaryHenselization A →+* S) [IsLocalHom g]
    (hg : g.comp (ordinaryHenselizationMap A) = f) :
    g = ordinaryHenselizationLift f

theorem

ordinaryHenselization_existsUnique_lift

L201 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselization_existsUnique_lift

Documentation

The ordinary henselization satisfies its universal property among local maps to Henselian local rings, with the original base map unchanged.

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 S : Type u} [CommRing A] [IsLocalRing A]
  [CommRing S] [HenselianLocalRing S] (f : A →+* S) [IsLocalHom f]

Lean source · statement

theorem ordinaryHenselization_existsUnique_lift :
    ∃! g : ordinaryHenselization A →+* S,
      IsLocalHom g ∧ g.comp (ordinaryHenselizationMap A) = f

Module documentation

The universal property of the constructed ordinary henselization

Declarations

ordinaryHenselizationLift

ordinaryHenselizationLift_isLocalHom

ordinaryHenselizationLift_comp_map

ordinaryHenselization_localMap_residue

henselian_etale_ringHom_ext

ordinaryHenselizationLift_unique

ordinaryHenselization_existsUnique_lift