NYLL
Module

PointedEtale.lean

Nyll.SchemeTheory.FiniteEtale.Henselian.PointedEtale
5 declarations indexed from sourceView source ↗

Module documentation

Pointed etale neighborhoods of Henselian local rings

An etale neighborhood of a Henselian local ring is trivial at a chosen point when that point has the same residue field as the base. The algebra need not be module-finite: standard-etale structure near the point supplies one simple root, and Hensel's lemma identifies that root with a base element.

The file also compares the residue-field map attached to a prime ideal with the local residue-field map after localization. This is the form needed for the residue-field bijection produced by Tag 00UJ.

Imports2
  • Mathlib.RingTheory.Henselian
  • Mathlib.RingTheory.Unramified.LocalStructure
Imported by10

Declarations

theorem

isLocalHom_algebraMap_localizationAtPrime_of_liesOver_maximalIdeal

L33 ↗
EtaleFundamentalGroups.isLocalHom_algebraMap_localizationAtPrime_of_liesOver_maximalIdeal
Documentation

If a prime lies over the maximal ideal of a local base, the canonical map from the base to the localization at that prime is local.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u v
Lean source · statement
theorem isLocalHom_algebraMap_localizationAtPrime_of_liesOver_maximalIdeal
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [IsLocalRing R] (P : Ideal S) [P.IsPrime]
    [P.LiesOver (IsLocalRing.maximalIdeal R)] :
    IsLocalHom (algebraMap R (Localization.AtPrime P))
def

localizationAtMaximalIdealAlgEquiv

L47 ↗
EtaleFundamentalGroups.localizationAtMaximalIdealAlgEquiv
Documentation

A local ring is canonically isomorphic to its localization at its maximal ideal.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u v
Lean source · statement
def localizationAtMaximalIdealAlgEquiv
    (R : Type u) [CommRing R] [IsLocalRing R] :
    R ≃ₐ[R] Localization.AtPrime (IsLocalRing.maximalIdeal R)
theorem

localResidueFieldMap_bijective_of_residueFieldMap_bijective

L58 ↗
EtaleFundamentalGroups.localResidueFieldMap_bijective_of_residueFieldMap_bijective
Documentation

A bijection between the ideal-theoretic residue fields at m_R and P induces a bijection on the residue fields of the local map R → S_P.

The source comparison is the canonical equivalence R ≃ R_{m_R}.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u v
Lean source · full declaration
theorem localResidueFieldMap_bijective_of_residueFieldMap_bijective
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [IsLocalRing R] (P : Ideal S) [P.IsPrime]
    [P.LiesOver (IsLocalRing.maximalIdeal R)]
    (hres : Function.Bijective
      (Ideal.ResidueField.mapₐ (IsLocalRing.maximalIdeal R) P
        (Algebra.ofId R S) (P.over_def (IsLocalRing.maximalIdeal R)))) :
    letI :=
      isLocalHom_algebraMap_localizationAtPrime_of_liesOver_maximalIdeal
        (R := R) (S := S) P
    Function.Bijective
      (IsLocalRing.ResidueField.map
        (algebraMap R (Localization.AtPrime P))) := by
  let m := IsLocalRing.maximalIdeal R
  let T := Localization.AtPrime P
  let : IsLocalHom (algebraMap R T) :=
    isLocalHom_algebraMap_localizationAtPrime_of_liesOver_maximalIdeal
      (R := R) (S := S) P
  let e : R ≃ₐ[R] Localization.AtPrime m :=
    localizationAtMaximalIdealAlgEquiv R
  let f : Localization.AtPrime m →+* T :=
    Localization.localRingHom m P (algebraMap R S) (P.over_def m)
  have hcomp : f.comp e.toRingHom = algebraMap R T := by
    ext x
    change f (e x) = algebraMap R T x
    have hex : e x = algebraMap R (Localization.AtPrime m) x := by
      simpa using e.commutes x
    rw [hex, Localization.localRingHom_to_map]
    exact IsScalarTower.algebraMap_apply R S T x
  let : IsLocalHom e.toRingEquiv.toRingHom := by
    have h : IsLocalHom e.toRingEquiv := inferInstance
    exact ⟨h.map_nonunit⟩
  have he : Function.Bijective
      (IsLocalRing.ResidueField.map e.toRingHom) :=
    (IsLocalRing.ResidueField.mapEquiv e.toRingEquiv).bijective
  have hf : Function.Bijective (IsLocalRing.ResidueField.map f) := by
    change Function.Bijective
      (Ideal.ResidueField.map m P (algebraMap R S) (P.over_def m)) at hres
    exact hres
  have hmap :
      IsLocalRing.ResidueField.map (algebraMap R T) =
        (IsLocalRing.ResidueField.map f).comp
          (IsLocalRing.ResidueField.map e.toRingHom) := by
    ext z
    obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective z
    rw [IsLocalRing.ResidueField.map_residue,
      RingHom.comp_apply, IsLocalRing.ResidueField.map_residue,
      IsLocalRing.ResidueField.map_residue]
    exact congrArg (IsLocalRing.residue T)
      (DFunLike.congr_fun hcomp x).symm
  rw [hmap]
  exact hf.comp he
theorem

algebraMap_localizationAtPrime_bijective_of_henselian_of_etale_of_residueFieldMap_bijective

L117 ↗
EtaleFundamentalGroups.algebraMap_localizationAtPrime_bijective_of_henselian_of_etale_of_residueFieldMap_bijective
Documentation

A pointed etale neighborhood of a Henselian local ring, with unchanged residue field at the chosen prime, has trivial local ring.

No module-finiteness assumption on S is used. Tag 00UE supplies a standard-etale neighborhood of P; Hensel's lemma moves its distinguished simple root into R, and localization clears the remaining denominators.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u v
Lean source · statement
theorem algebraMap_localizationAtPrime_bijective_of_henselian_of_etale_of_residueFieldMap_bijective
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [HenselianLocalRing R] [Algebra.Etale R S]
    (P : Ideal S) [P.IsPrime]
    [P.LiesOver (IsLocalRing.maximalIdeal R)]
    (hres : Function.Bijective
      (Ideal.ResidueField.mapₐ (IsLocalRing.maximalIdeal R) P
        (Algebra.ofId R S) (P.over_def (IsLocalRing.maximalIdeal R)))) :
    Function.Bijective (algebraMap R (Localization.AtPrime P))
def

henselianPointedEtaleLocalizationAlgEquiv

L277 ↗
EtaleFundamentalGroups.henselianPointedEtaleLocalizationAlgEquiv
Documentation

The explicit base-algebra equivalence associated to a pointed etale neighborhood with unchanged residue field.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe u v
Lean source · statement
def henselianPointedEtaleLocalizationAlgEquiv
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    [HenselianLocalRing R] [Algebra.Etale R S]
    (P : Ideal S) [P.IsPrime]
    [P.LiesOver (IsLocalRing.maximalIdeal R)]
    (hres : Function.Bijective
      (Ideal.ResidueField.mapₐ (IsLocalRing.maximalIdeal R) P
        (Algebra.ofId R S) (P.over_def (IsLocalRing.maximalIdeal R)))) :
    R ≃ₐ[R] Localization.AtPrime P

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.