Module

GeometricStalkResidueClosure.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkResidueClosure

8 declarations indexed from sourceView source ↗

Module documentation

Identifying the geometric stalk's residue field with the chosen closure

Let the geometric field be a separably closed separable algebraic extension of the residue field of a local ring. Every element of that field is a simple root of its minimal polynomial. Lift the coefficients to the local ring and then to its actual geometric étale stalk. The standard étale root construction produces a germ with exactly the prescribed value at the geometric point.

Consequently evaluation induces a bijection from the stalk's residue field to the chosen separable closure. For residue characteristic zero this applies to the algebraic closure used by the manuscript. No residue-field comparison is supplied as an assumption.

Imports6

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkStructure
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkResidueSeparable
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Mathlib.FieldTheory.Separable
Mathlib.FieldTheory.SeparableClosure
Mathlib.Algebra.Polynomial.Lifts

Imported by3

theorem

geometricStalkResidueEmbedding_mem_range_of_isSeparable

L40 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkResidueEmbedding_mem_range_of_isSeparable

Documentation

Every element separable over the base residue field lies in the actual stalk residue image. The simple-root construction does not require the whole geometric overfield to be separable over that residue field.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleFundamentalGroups.StrictHenselian
universe u

Lean source · statement

theorem geometricStalkResidueEmbedding_mem_range_of_isSeparable
    (R Ω : Type u) [CommRing R] [IsLocalRing R] [Field Ω] [IsSepClosed Ω]
    [Algebra (IsLocalRing.ResidueField R) Ω]
    (α : Ω) (hsepα : IsSeparable (IsLocalRing.ResidueField R) α) :
    α ∈ Set.range (geometricStalkResidueEmbedding
      (Spec.map (CommRingCat.ofHom
        ((algebraMap (IsLocalRing.ResidueField R) Ω).comp
          (IsLocalRing.residue R)))))

theorem

geometricStalkResidueEmbedding_bijective

L86 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkResidueEmbedding_bijective

Documentation

The residue embedding of the actual geometric étale stalk is onto a chosen separable closure, by the actual simple-root preimages above.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleFundamentalGroups.StrictHenselian
universe u

Lean source · statement

theorem geometricStalkResidueEmbedding_bijective
    (R Ω : Type u) [CommRing R] [IsLocalRing R] [Field Ω] [IsSepClosed Ω]
    [Algebra (IsLocalRing.ResidueField R) Ω]
    [Algebra.IsSeparable (IsLocalRing.ResidueField R) Ω] :
    Function.Bijective (geometricStalkResidueEmbedding
      (Spec.map (CommRingCat.ofHom
        ((algebraMap (IsLocalRing.ResidueField R) Ω).comp
          (IsLocalRing.residue R)))))

def

geometricStalkResidueAlgHom

L100 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkResidueAlgHom

Documentation

The actual residue embedding is linear over the original residue field, as witnessed on residues of original coefficients.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleFundamentalGroups.StrictHenselian
universe u

Lean source · full declaration

def geometricStalkResidueAlgHom
    (R Ω : Type u) [CommRing R] [IsLocalRing R] [Field Ω] [IsSepClosed Ω]
    [Algebra (IsLocalRing.ResidueField R) Ω] :
    let φ := (algebraMap (IsLocalRing.ResidueField R) Ω).comp (IsLocalRing.residue R)
    let : Algebra R (geometricStalk (Spec.map (CommRingCat.ofHom φ))) :=
      (geometricStalkStructureMap φ).toAlgebra
    let : IsLocalHom (algebraMap R (geometricStalk (Spec.map (CommRingCat.ofHom φ)))) := by
      change IsLocalHom (geometricStalkStructureMap φ)
      exact geometricStalkStructureMap_isLocalHom φ
    IsLocalRing.ResidueField (geometricStalk (Spec.map (CommRingCat.ofHom φ))) →ₐ[
      IsLocalRing.ResidueField R] Ω := by
  intro φ actualStructureAlgebra actualStructureLocal
  refine { geometricStalkResidueEmbedding (Spec.map (CommRingCat.ofHom φ)) with
    commutes' := ?_ }
  intro x
  obtain ⟨a, rfl⟩ := IsLocalRing.residue_surjective (R := R) x
  change geometricStalkEvaluation (Spec.map (CommRingCat.ofHom φ))
    (geometricStalkStructureMap φ a) = algebraMap (IsLocalRing.ResidueField R) Ω
      (IsLocalRing.residue R a)
  exact geometricStalkStructureMap_evaluation_apply φ a

theorem

geometricStalkResidueEmbedding_mem_range_iff

L123 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkResidueEmbedding_mem_range_iff

Documentation

The image of the actual geometric-stalk residue consists exactly of separable elements over the original residue field.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleFundamentalGroups.StrictHenselian
universe u

Lean source · statement

theorem geometricStalkResidueEmbedding_mem_range_iff
    (R Ω : Type u) [CommRing R] [IsLocalRing R] [Field Ω] [IsSepClosed Ω]
    [Algebra (IsLocalRing.ResidueField R) Ω] (α : Ω) :
    α ∈ Set.range (geometricStalkResidueEmbedding
      (Spec.map (CommRingCat.ofHom
        ((algebraMap (IsLocalRing.ResidueField R) Ω).comp (IsLocalRing.residue R))))) ↔
      IsSeparable (IsLocalRing.ResidueField R) α

theorem

geometricStalkResidueAlgHom_fieldRange

L148 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkResidueAlgHom_fieldRange

Documentation

The actual residue image is precisely the separable part of the geometric field. In particular this statement applies to the normalization residue field even when it contains inseparable elements over the base residue field.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleFundamentalGroups.StrictHenselian
universe u

Lean source · full declaration

theorem geometricStalkResidueAlgHom_fieldRange
    (R Ω : Type u) [CommRing R] [IsLocalRing R] [Field Ω] [IsSepClosed Ω]
    [Algebra (IsLocalRing.ResidueField R) Ω] :
    let φ := (algebraMap (IsLocalRing.ResidueField R) Ω).comp (IsLocalRing.residue R)
    let : Algebra R (geometricStalk (Spec.map (CommRingCat.ofHom φ))) :=
      (geometricStalkStructureMap φ).toAlgebra
    let : IsLocalHom (algebraMap R (geometricStalk (Spec.map (CommRingCat.ofHom φ)))) := by
      change IsLocalHom (geometricStalkStructureMap φ)
      exact geometricStalkStructureMap_isLocalHom φ
    (geometricStalkResidueAlgHom R Ω).fieldRange =
      separableClosure (IsLocalRing.ResidueField R) Ω := by
  intro φ actualStructureAlgebra actualStructureLocal
  apply IntermediateField.ext
  intro α
  exact geometricStalkResidueEmbedding_mem_range_iff R Ω α

def

geometricStalkResidueSeparableClosureEquiv

L166 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkResidueSeparableClosureEquiv

Documentation

The constructed stalk residue is the actual separable closure inside the chosen geometric field, with the original residue coefficient action.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleFundamentalGroups.StrictHenselian
universe u

Lean source · full declaration

def geometricStalkResidueSeparableClosureEquiv
    (R Ω : Type u) [CommRing R] [IsLocalRing R] [Field Ω] [IsSepClosed Ω]
    [Algebra (IsLocalRing.ResidueField R) Ω] :
    let φ := (algebraMap (IsLocalRing.ResidueField R) Ω).comp (IsLocalRing.residue R)
    let : Algebra R (geometricStalk (Spec.map (CommRingCat.ofHom φ))) :=
      (geometricStalkStructureMap φ).toAlgebra
    let : IsLocalHom (algebraMap R (geometricStalk (Spec.map (CommRingCat.ofHom φ)))) := by
      change IsLocalHom (geometricStalkStructureMap φ)
      exact geometricStalkStructureMap_isLocalHom φ
    IsLocalRing.ResidueField (geometricStalk (Spec.map (CommRingCat.ofHom φ))) ≃ₐ[
      IsLocalRing.ResidueField R] separableClosure (IsLocalRing.ResidueField R) Ω := by
  intro φ actualStructureAlgebra actualStructureLocal
  exact (geometricStalkResidueAlgHom R Ω).equivFieldRange.trans
    (IntermediateField.equivOfEq (geometricStalkResidueAlgHom_fieldRange R Ω))

theorem

geometricStalkResidueSeparableClosureEquiv_apply

L183 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkResidueSeparableClosureEquiv_apply

Documentation

The residue comparison retains the literal embedding into the chosen geometric field.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleFundamentalGroups.StrictHenselian
universe u

Lean source · full declaration

theorem geometricStalkResidueSeparableClosureEquiv_apply
    (R Ω : Type u) [CommRing R] [IsLocalRing R] [Field Ω] [IsSepClosed Ω]
    [Algebra (IsLocalRing.ResidueField R) Ω] :
    let φ := (algebraMap (IsLocalRing.ResidueField R) Ω).comp (IsLocalRing.residue R)
    let : Algebra R (geometricStalk (Spec.map (CommRingCat.ofHom φ))) :=
      (geometricStalkStructureMap φ).toAlgebra
    let : IsLocalHom (algebraMap R (geometricStalk (Spec.map (CommRingCat.ofHom φ)))) := by
      change IsLocalHom (geometricStalkStructureMap φ)
      exact geometricStalkStructureMap_isLocalHom φ
    ∀ x : IsLocalRing.ResidueField (geometricStalk (Spec.map (CommRingCat.ofHom φ))),
      ((geometricStalkResidueSeparableClosureEquiv R Ω x :
        separableClosure (IsLocalRing.ResidueField R) Ω) : Ω) =
          geometricStalkResidueEmbedding (Spec.map (CommRingCat.ofHom φ)) x := by
  intro φ actualStructureAlgebra actualStructureLocal x
  rfl

def

geometricStalkResidueAlgebraicClosureEquiv

L202 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkResidueAlgebraicClosureEquiv

Documentation

In residue characteristic zero the residue field of the constructed geometric stalk is canonically identified with the very algebraic closure used to define its closed geometric point.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Polynomial
namespace EtaleFundamentalGroups.StrictHenselian
universe u

Lean source · statement

def geometricStalkResidueAlgebraicClosureEquiv
    (R : Type u) [CommRing R] [IsLocalRing R]
    [CharZero (IsLocalRing.ResidueField R)] :
    IsLocalRing.ResidueField
      (geometricStalk (Spec.map (CommRingCat.ofHom
        ((algebraMap (IsLocalRing.ResidueField R)
            (AlgebraicClosure (IsLocalRing.ResidueField R))).comp
          (IsLocalRing.residue R))))) ≃+*
      AlgebraicClosure (IsLocalRing.ResidueField R)

Module documentation

Identifying the geometric stalk's residue field with the chosen closure

Declarations