NYLL
Module

PuncturedStrictStalk.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedStrictStalk
1 declaration indexed from sourceView source ↗

Module documentation

Full faithfulness from connected punctured strict henselization

For an arbitrary local ring, connectedness of its actual punctured geometric étale stalk makes restriction to the punctured local spectrum fully faithful on finite étale schemes. The finite étale internal Hom turns a morphism on the puncture into a section. Actual strict-stalk fpqc descent extends that section, and naturality of the same representer recovers the original map.

This is the original arbitrary-local-ring statement of Stacks Project 0BLQ. The puncture need not be quasi-compact. No domain, reducedness, normality, Noetherianity, or dimension hypothesis is imposed.

Imports11
Imported by1

Declarations

def

puncturedSpectrumPullbackFullyFaithful_of_connected_geometricStalk

L45 ↗
AlgebraicGeometry.FiniteEtale.puncturedSpectrumPullbackFullyFaithful_of_connected_geometricStalk
Documentation

Restriction to the puncture of an arbitrary local ring is fully faithful when the puncture of its actual strict stalk is connected.

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits EtaleFundamentalGroups.StrictHenselian
open scoped MonoidalCategory
namespace AlgebraicGeometry.FiniteEtale
universe u
Lean source · statement
def puncturedSpectrumPullbackFullyFaithful_of_connected_geometricStalk
    {R Ω : Type u} [CommRing R] [IsLocalRing R] [Field Ω] [IsSepClosed Ω]
    (φ : R →+* Ω) [IsLocalHom φ]
    [ConnectedSpace
      (Scheme.puncturedSpectrum
        (geometricStalk
          (Spec.map (CommRingCat.ofHom φ))))] :
    (FiniteEtale.pullback (Scheme.puncturedSpectrumInclusion R)).FullyFaithful

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