NYLL
Module

HenselianSectionFactor.lean

Nyll.SchemeTheory.Normalization.HenselianSectionFactor
1 declaration indexed from sourceView source ↗

Module documentation

An integral factor extending an étale section over a Henselian pair

The section first selects a finite factor in the special fiber of the integral closure. A principal neighborhood identifies the integral closure with the étale algebra. The cyclic idempotent of this factor lifts by the Henselian axiom, and the principal-localization comparison identifies its lifted factors.

Imports9
Imported by2

Declarations

theorem

exists_integral_idempotent_factor_of_etale_quotientSection

L38 ↗
Algebra.exists_integral_idempotent_factor_of_etale_quotientSection
Documentation

An étale section over the quotient of a Henselian pair selects an integral idempotent factor whose special fiber is generated by its unit over the base.

Source context 4 commands

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

@[expose] public section
open AlgebraicGeometry
universe u
namespace Algebra
Lean source · statement
theorem exists_integral_idempotent_factor_of_etale_quotientSection
    {R B : Type u} [CommRing R] [CommRing B] [Algebra R B] [Algebra.Etale R B]
    (I : Ideal R) [HenselianRing R I] (σ : B →ₐ[R] R ⧸ I) :
    ∃ e : B, IsIdempotentElem e ∧ σ e = 1 ∧
      Algebra.IsIntegral R (B ⧸ Ideal.span {1 - e}) ∧
      Function.Surjective (algebraMap (R ⧸ I)
        ((B ⧸ Ideal.span {1 - e}) ⧸
          I.map (algebraMap R (B ⧸ Ideal.span {1 - e}))))

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