NYLL
Module

HenselianIntegralSection.lean

Nyll.SchemeTheory.Normalization.HenselianIntegralSection
2 declarations indexed from sourceView source ↗

Module documentation

Étale sections after integral extension of a Henselian pair

Normalization selects an idempotent in the special fiber. Its integral closure is integral over the original Henselian base, so this idempotent lifts there. The resulting factor is integral and étale over the new base, and Jacobson conservativity identifies it with that base. No Henselian hypothesis on the integral extension is used in the construction.

Imports11
Imported by2

Declarations

theorem

exists_integral_factor_of_integral_henselian_base

L39 ↗
Algebra.exists_integral_factor_of_integral_henselian_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_factor_of_integral_henselian_base
    {R B D : Type u} [CommRing R] [CommRing B] [CommRing D]
    [Algebra R B] [Algebra.IsIntegral R B] [Algebra B D] [Algebra.Etale B D]
    (I : Ideal R) [HenselianRing R I]
    (σ : D →ₐ[B] B ⧸ I.map (algebraMap R B)) :
    ∃ e : D, IsIdempotentElem e ∧ σ e = 1 ∧
      Algebra.IsIntegral B (D ⧸ Ideal.span {1 - e}) ∧
      Function.Surjective (algebraMap (B ⧸ I.map (algebraMap R B))
        ((D ⧸ Ideal.span {1 - e}) ⧸
          (I.map (algebraMap R B)).map (algebraMap B (D ⧸ Ideal.span {1 - e}))))
theorem

exists_lift_section_of_isIntegral_henselian_base

L133 ↗
Algebra.Etale.exists_lift_section_of_isIntegral_henselian_base
Documentation

Étale sections lift after any integral extension of a Henselian pair. The integral extension need not be finite, local, or complete.

Source context 5 commands

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

@[expose] public section
open AlgebraicGeometry
universe u
namespace Algebra
namespace Etale
Lean source · statement
theorem exists_lift_section_of_isIntegral_henselian_base
    {R B D : Type u} [CommRing R] [CommRing B] [CommRing D]
    [Algebra R B] [Algebra.IsIntegral R B] [Algebra B D] [Algebra.Etale B D]
    (I : Ideal R) [HenselianRing R I]
    (σ : D →ₐ[B] B ⧸ I.map (algebraMap R B)) :
    ∃ τ : D →ₐ[B] B,
      (Ideal.Quotient.mkₐ B (I.map (algebraMap R B))).comp τ = σ

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