Module

OrdinaryHenselizationEmbedding.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.OrdinaryHenselizationEmbedding

2 declarations indexed from sourceView source ↗

Module documentation

Embedding the actual ordinary henselization

For a normal local domain, the original geometric-stalk algebraicity and domain proofs apply at its ordinary residue-field point. An injective local base map into a Henselian target therefore induces an injective universal map. Every local target endomorphism fixing the base fixes this image, by the already proved ordinary universal property.

Imports4

Imported by3

theorem

ordinaryHenselizationLift_comp_endomorphism

L36 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationLift_comp_endomorphism

Documentation

The actual universal map is fixed by every local endomorphism of the target fixing the original base ring. No condition on the target residue field action is required for the ordinary henselization.

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 {A S : Type u} [CommRing A] [IsLocalRing A]
  [CommRing S] [HenselianLocalRing S] (f : A →+* S) [IsLocalHom f]

Lean source · statement

theorem ordinaryHenselizationLift_comp_endomorphism
    (τ : S →+* S) [IsLocalHom τ] (hbase : τ.comp f = f) :
    τ.comp (ordinaryHenselizationLift f) = ordinaryHenselizationLift f

theorem

ordinaryHenselizationLift_injective

L44 ↗

EtaleFundamentalGroups.StrictHenselian.ordinaryHenselizationLift_injective