Module

LocallyConnectedRestriction.lean

Nyll.EtaleFundamentalGroups.Purity.LocallyConnectedRestriction

2 declarations indexed from sourceView source ↗

Module documentation

Dense-open full faithfulness from local connectedness

Connected punctured strict stalks give full faithfulness of restriction when every quasi-compact open has finitely many irreducible components. The proof uses the existing finite etale internal Hom representer and the constructed global section extension. The Noetherian-space statement is the resulting special case; no locally Noetherian ring hypothesis occurs.

These are the original Stacks Project statements 0BQG and 0BQF. The dense open need not be retrocompact, and the base need not be normal or reduced.

Imports9

Nyll.EtaleFundamentalGroups.Purity.LocallyConnectedSectionExtension
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Nyll.SchemeTheory.FiniteEtale.DensePullback
Nyll.SchemeTheory.WeilRestriction.FiniteEtale
Nyll.SchemeTheory.WeilRestriction.Sheaf
Mathlib.CategoryTheory.Functor.FullyFaithful
Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Mathlib.CategoryTheory.Yoneda
Mathlib.Topology.NoetherianSpace

Imported by2

def

denseOpenPullbackFullyFaithful_of_finite_components

L43 ↗

AlgebraicGeometry.FiniteEtale.denseOpenPullbackFullyFaithful_of_finite_components

Documentation

Original finite-component 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_finite_components
    {S : Scheme.{u}}
    (hfin : ∀ A : S.Opens, IsCompact (A : Set S) →
      (irreducibleComponents A.toScheme).Finite)
    (U : S.Opens) (hU : Dense (U : 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

def

denseOpenPullbackFullyFaithful_of_noetherianSpace

L134 ↗

AlgebraicGeometry.FiniteEtale.denseOpenPullbackFullyFaithful_of_noetherianSpace