Module

ProperHenselianFullyFaithful.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ProperHenselianFullyFaithful

2 declarations indexed from sourceView source ↗

Module documentation

Full faithfulness over an arbitrary henselian local base

This proves the full-faithfulness part of the proper henselian-local comparison without a Noetherian hypothesis. Essential surjectivity, and hence the full equivalence in Stacks 0A48, is separate.

Fullness uses the existing finite étale internal Hom and henselian section lift. Faithfulness is supplied by the arbitrary-local proper closed-fibre comparison. The proper morphism is not assumed flat.

Imports4

Nyll.SchemeTheory.FiniteEtale.ProperHenselianSections
Nyll.SchemeTheory.FiniteEtale.ProperClosedFiberFaithful
Nyll.SchemeTheory.FiniteEtale.FullOfSectionDescent
Mathlib.CategoryTheory.Functor.FullyFaithful

Imported by1

Nyll.EtaleFundamentalGroups.FiniteEtale.All

theorem

pullback_full_closedFiber_of_isProper_of_henselianLocalRing

L35 ↗

AlgebraicGeometry.FiniteEtale.pullback_full_closedFiber_of_isProper_of_henselianLocalRing

Documentation

Henselian lifting of sections of the actual finite étale internal Hom makes the canonical closed-fibre pullback full over any henselian local ring.

Source context 5 commands

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

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

Lean source · full declaration

theorem pullback_full_closedFiber_of_isProper_of_henselianLocalRing
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f] :
    (FiniteEtale.pullback
      (pullback.fst f (Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))))).Full where
  map_surjective := (pullback_full_of_section_descent
    (pullback.fst f (Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))))
    (fun W a ha =>
      exists_section_of_isFinite_of_etale_of_isProper_of_henselianLocalRing
        f W.hom a ha)).map_surjective

def

pullbackFullyFaithful_closedFiber_of_isProper_of_henselianLocalRing

L48 ↗

AlgebraicGeometry.FiniteEtale.pullbackFullyFaithful_closedFiber_of_isProper_of_henselianLocalRing