NYLL
Module

HenselianEtaleSection.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.HenselianEtaleSection
1 declaration indexed from sourceView source ↗

Module documentation

Lifting étale sections over a Henselian pair

A section over the quotient selects an integral idempotent factor of the étale algebra. This factor is finite étale, and its special fiber is generated by the base. The section makes its structural map injective on the special fiber, so Jacobson conservativity identifies the factor with the base itself. The original section therefore lifts. Unramified rigidity gives uniqueness.

This proves the étale-section lifting implication used in Stacks Tag 09XI for the native general HenselianRing R I class.

Imports5
Imported by4

Declarations

theorem

bijective_comp_quotient_of_henselian

L36 ↗
Algebra.Etale.bijective_comp_quotient_of_henselian
Documentation

Reduction over a Henselian pair gives a bijection on sections of every étale algebra. No finiteness as a module, locality, or completeness is assumed.

Source context 3 commands

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

@[expose] public section
universe u
namespace Algebra.Etale
Lean source · statement
theorem bijective_comp_quotient_of_henselian
    {R B : Type u} [CommRing R] [CommRing B] [Algebra R B] [Algebra.Etale R B]
    (I : Ideal R) [HenselianRing R I] :
    Function.Bijective
      ((Ideal.Quotient.mkₐ R I).comp : (B →ₐ[R] R) → B →ₐ[R] R ⧸ I)

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