Nyll.EtaleFundamentalGroups.Purity.RetrocompactRestriction

Module documentation

Full faithfulness over a retrocompact dense open

The finite etale internal Hom turns lifting a morphism into extending a section. The constructed global extension applies exactly to the original hypotheses of Stacks 0BSA: retrocompactness, closed complement points, and connected punctured strict stalks. The ambient scheme is arbitrary.

def

denseOpenPullbackFullyFaithful_of_retrocompact_closed_complement

L39 ↗

AlgebraicGeometry.FiniteEtale.denseOpenPullbackFullyFaithful_of_retrocompact_closed_complement

Documentation

Original retrocompact local connectedness criterion for restriction of finite etale covers.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits TopologicalSpace
open EtaleFundamentalGroups.StrictHenselian
open scoped MonoidalCategory
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

def denseOpenPullbackFullyFaithful_of_retrocompact_closed_complement
    {S : Scheme.{u}}
    (U : S.Opens) [QuasiCompact U.ι] (hU : Dense (U : Set S))
    (hclosed : ∀ x : S, x ∉ U → IsClosed ({x} : Set S))
    (Ω : S → Type u) [∀ x : S, Field (Ω x)] [∀ x : S, IsSepClosed (Ω x)]
    (φ : ∀ x : S, S.presheaf.stalk x →+* Ω x) [∀ x : S, IsLocalHom (φ x)]
    (hconn : ∀ x : S, x ∉ U → ConnectedSpace (Scheme.puncturedSpectrum
      (geometricStalk (Spec.map (CommRingCat.ofHom (φ x)))))) :
    (FiniteEtale.pullback U.ι).FullyFaithful

Module documentation

Full faithfulness over a retrocompact dense open

Declarations

denseOpenPullbackFullyFaithful_of_retrocompact_closed_complement