NYLL
Module

GeometricStalkHenselianRigidity.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkHenselianRigidity
3 declarations indexed from sourceView source ↗

Module documentation

Rigidity of the actual map to a strictly Henselian target

An endomorphism of the target that preserves the base map and its residue map fixes every actual pointed-neighborhood lift. Naturality of global sections then fixes their section maps, and the defining presheaf-fiber colimit fixes the constructed ring homomorphism.

No normalization comparison, inertia action, or fixed-image identification is assumed here.

Imports13
Imported by2

Declarations

theorem

geometricNeighborhoodHenselianLift_comp_endomorphism

L46 ↗
EtaleFundamentalGroups.StrictHenselian.geometricNeighborhoodHenselianLift_comp_endomorphism
Documentation

Precomposing an actual pointed lift with a base-preserving, residue-trivial target endomorphism leaves that lift unchanged.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  [IsSepClosed (IsLocalRing.ResidueField S)] (f : R →+* S)
Lean source · statement
theorem geometricNeighborhoodHenselianLift_comp_endomorphism
    (τ : S →+* S) (hbase : τ.comp f = f)
    (hresidue : (IsLocalRing.residue S).comp τ = IsLocalRing.residue S)
    (W : (Spec (.of R)).Etale)
    (t : (Scheme.pointSmallEtale (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue S).comp f)))).fiber.obj W) :
    Spec.map (CommRingCat.ofHom τ) ≫ geometricNeighborhoodHenselianLift f W t =
      geometricNeighborhoodHenselianLift f W t
theorem

geometricStalkGerm_henselian_comp_endomorphism

L103 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkGerm_henselian_comp_endomorphism
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  [IsSepClosed (IsLocalRing.ResidueField S)] (f : R →+* S)
Lean source · statement
theorem geometricStalkGerm_henselian_comp_endomorphism
    (τ : S →+* S) (hbase : τ.comp f = f)
    (hresidue : (IsLocalRing.residue S).comp τ = IsLocalRing.residue S)
    (W : (Spec (.of R)).Etale)
    (t : (Scheme.pointSmallEtale (Spec.map (CommRingCat.ofHom
      ((IsLocalRing.residue S).comp f)))).fiber.obj W) :
    (geometricStalkGerm (Spec.map (CommRingCat.ofHom
        ((IsLocalRing.residue S).comp f))) W t ≫
        CommRingCat.ofHom (geometricStalkToHenselian f)) ≫ CommRingCat.ofHom τ =
      geometricStalkGerm (Spec.map (CommRingCat.ofHom
        ((IsLocalRing.residue S).comp f))) W t ≫
        CommRingCat.ofHom (geometricStalkToHenselian f)
theorem

geometricStalkToHenselian_comp_endomorphism

L135 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkToHenselian_comp_endomorphism
Documentation

The actual geometric-stalk map is fixed by every target endomorphism that preserves its base map and acts trivially after reduction.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R S : Type u} [CommRing R] [CommRing S] [HenselianLocalRing S]
  [IsSepClosed (IsLocalRing.ResidueField S)] (f : R →+* S)
Lean source · statement
theorem geometricStalkToHenselian_comp_endomorphism
    (τ : S →+* S) (hbase : τ.comp f = f)
    (hresidue : (IsLocalRing.residue S).comp τ = IsLocalRing.residue S) :
    τ.comp (geometricStalkToHenselian f) = geometricStalkToHenselian f

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