NYLL
Module

Core.lean

Nyll.SchemeTheory.FiniteEtale.Henselian.ChosenFactor.Core
4 declarations indexed from sourceView source ↗

Module documentation

A uniquely chosen finite étale factor over a strictly Henselian local ring

Tag 00UJ isolates a finite idempotent factor with a unique prime over the chosen closed point. Once local purity has made that factor étale, the uniqueness makes the factor local. Faithful flatness is then produced from flatness and the local algebra map, so the connected strict-Henselian splitting theorem applies without a separate faithfulness hypothesis.

Imports4
Imported by4

Declarations

theorem

algebraMap_bijective_of_unique_prime_over_maximal_of_strictHenselian

L34 ↗
EtaleFundamentalGroups.algebraMap_bijective_of_unique_prime_over_maximal_of_strictHenselian
Documentation

A finite étale algebra with a unique prime over the closed point of a strictly Henselian local base is the base ring itself.

The unique-prime input is exactly the output supplied for the chosen finite idempotent factor by Tag 00UJ. Localness, local-hom status, and faithful flatness are conclusions internal to the proof.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem algebraMap_bijective_of_unique_prime_over_maximal_of_strictHenselian
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [HenselianLocalRing R] [Module.Finite R S] [Algebra.Etale R S]
    [IsSepClosed (IsLocalRing.ResidueField R)]
    (q : Ideal S) [q.IsPrime]
    [q.LiesOver (IsLocalRing.maximalIdeal R)]
    (hunique : ∀ Q : Ideal S, Q.IsPrime →
      Q.LiesOver (IsLocalRing.maximalIdeal R) → Q = q) :
    Function.Bijective (algebraMap R S)
def

strictHenselianChosenFactorAlgEquiv

L75 ↗
EtaleFundamentalGroups.strictHenselianChosenFactorAlgEquiv
Documentation

The explicit base-algebra equivalence for the uniquely chosen finite étale factor over a strictly Henselian local base.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u
Lean source · statement
def strictHenselianChosenFactorAlgEquiv
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [HenselianLocalRing R] [Module.Finite R S] [Algebra.Etale R S]
    [IsSepClosed (IsLocalRing.ResidueField R)]
    (q : Ideal S) [q.IsPrime]
    [q.LiesOver (IsLocalRing.maximalIdeal R)]
    (hunique : ∀ Q : Ideal S, Q.IsPrime →
      Q.LiesOver (IsLocalRing.maximalIdeal R) → Q = q) :
    R ≃ₐ[R] S
theorem

algebraMap_bijective_away_of_unique_prime_over_maximal_of_strictHenselian

L95 ↗
EtaleFundamentalGroups.algebraMap_bijective_away_of_unique_prime_over_maximal_of_strictHenselian
Documentation

The finite Away-factor isolated by Tag 00UJ is the strict-Henselian base once it is étale and the Tag 00UJ prime is the unique prime over the closed point that avoids the inverted element.

This statement performs the localization-prime transport: no separate localness, local-hom, faithful-flatness, or unique-prime assertion on the localized factor is assumed.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem algebraMap_bijective_away_of_unique_prime_over_maximal_of_strictHenselian
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [HenselianLocalRing R] [IsSepClosed (IsLocalRing.ResidueField R)]
    (e : A)
    [Module.Finite R (Localization.Away e)]
    [Algebra.Etale R (Localization.Away e)]
    (P : Ideal A) [P.IsPrime]
    [P.LiesOver (IsLocalRing.maximalIdeal R)]
    (heP : e ∉ P)
    (hunique : ∀ Q : Ideal A, Q.IsPrime →
      Q.LiesOver (IsLocalRing.maximalIdeal R) → e ∉ Q → Q = P) :
    Function.Bijective (algebraMap R (Localization.Away e))
def

strictHenselianAwayChosenFactorAlgEquiv

L146 ↗
EtaleFundamentalGroups.strictHenselianAwayChosenFactorAlgEquiv
Documentation

The explicit algebra equivalence for the Away-factor version of the Tag 00UJ strict-Henselian splitting consumer.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u
Lean source · statement
def strictHenselianAwayChosenFactorAlgEquiv
    {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    [HenselianLocalRing R] [IsSepClosed (IsLocalRing.ResidueField R)]
    (e : A)
    [Module.Finite R (Localization.Away e)]
    [Algebra.Etale R (Localization.Away e)]
    (P : Ideal A) [P.IsPrime]
    [P.LiesOver (IsLocalRing.maximalIdeal R)]
    (heP : e ∉ P)
    (hunique : ∀ Q : Ideal A, Q.IsPrime →
      Q.LiesOver (IsLocalRing.maximalIdeal R) → e ∉ Q → Q = P) :
    R ≃ₐ[R] Localization.Away e

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