Module

GeometricStalkHenselianEtaleRange.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkHenselianEtaleRange

3 declarations indexed from sourceView source ↗

Module documentation

Actual affine étale representatives in the Henselian stalk-map range

An étale algebra map to the strict target gives a pointed affine étale neighborhood by reduction. Uniqueness of the actual pointed Henselian lift identifies its section map with that algebra map. Its germ therefore supplies an actual preimage in the geometric stalk. No comparison or surjectivity is assumed, and no new colimit is constructed.

Imports10

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalk
Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkHenselianMap
Nyll.SchemeTheory.Affine.SpecSectionMap
Nyll.SchemeTheory.Etale.HenselianLocalSection
Mathlib.Algebra.Category.Ring.Basic
Mathlib.Algebra.Ring.Hom.Defs
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Mathlib.RingTheory.RingHom.Etale

Imported by2

theorem

geometricStalkToHenselian_affine_factorization

L39 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkToHenselian_affine_factorization

Documentation

The actual affine germ factors the prescribed map once the genuine pointed lift has been identified. The source-algebra structure and the construction of the point stay outside this section-ring scope.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u

Lean source · statement

theorem geometricStalkToHenselian_affine_factorization
    {R S B : Type u} [CommRing R] [CommRing S] [CommRing B]
    [HenselianLocalRing S] [IsSepClosed (IsLocalRing.ResidueField S)]
    (f : R →+* S) (e : Spec (.of B) ⟶ Spec (.of R)) [Etale e]
    (t : (Scheme.pointSmallEtale (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue S).comp f)))).fiber.obj (Scheme.Etale.mk e))
    (g : B →+* S)
    (hlift : geometricNeighborhoodHenselianLift f (Scheme.Etale.mk e) t =
      Spec.map (CommRingCat.ofHom g)) :
    ∃ j : CommRingCat.of B ⟶ geometricStalk (Spec.map (CommRingCat.ofHom
        ((IsLocalRing.residue S).comp f))),
      j ≫ CommRingCat.ofHom (geometricStalkToHenselian f) = CommRingCat.ofHom g

theorem

geometricStalkToHenselian_factorization_of_etale

L71 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkToHenselian_factorization_of_etale

Documentation

A compatible map from an actual étale algebra into the strict target factors through the actual geometric stalk. Its point and lift equation are constructed from the original algebra map and its proved base square.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u

Lean source · statement

theorem geometricStalkToHenselian_factorization_of_etale
    {R S B : Type u} [CommRing R] [CommRing S] [CommRing B]
    [HenselianLocalRing S] [IsSepClosed (IsLocalRing.ResidueField S)]
    [Algebra R B] [Algebra.Etale R B]
    (f : R →+* S) (g : B →+* S)
    (hbase : g.comp (algebraMap R B) = f) :
    ∃ j : B →+* geometricStalk (Spec.map (CommRingCat.ofHom
        ((IsLocalRing.residue S).comp f))),
      (geometricStalkToHenselian f).comp j = g

theorem

geometricStalkToHenselian_exists_preimage_of_etale

L120 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkToHenselian_exists_preimage_of_etale

Documentation

Elementwise preimages are extracted in a ring-only scope, after the actual affine factorization has been constructed.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u

Lean source · statement

theorem geometricStalkToHenselian_exists_preimage_of_etale
    {R S B : Type u} [CommRing R] [CommRing S] [CommRing B]
    [HenselianLocalRing S] [IsSepClosed (IsLocalRing.ResidueField S)]
    [Algebra R B] [Algebra.Etale R B]
    (f : R →+* S) (g : B →+* S)
    (hbase : g.comp (algebraMap R B) = f) (b : B) :
    ∃ a : geometricStalk (Spec.map (CommRingCat.ofHom
        ((IsLocalRing.residue S).comp f))),
      geometricStalkToHenselian f a = g b

Module documentation

Actual affine étale representatives in the Henselian stalk-map range

Declarations

geometricStalkToHenselian_affine_factorization

geometricStalkToHenselian_factorization_of_etale

geometricStalkToHenselian_exists_preimage_of_etale